Changeset 1599 for src/Clight


Ignore:
Timestamp:
Dec 13, 2011, 1:34:37 AM (8 years ago)
Author:
sacerdot
Message:

Start of merging of stuff into the standard library of Matita.

Location:
src/Clight
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1545 r1599  
    145145
    146146definition load_value_of_type' ≝
    147 λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
     147λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
    148148
    149149axiom BadlyTypedTerm : String.
     
    185185      match ty with
    186186      [ Tpointer r _ ⇒
    187         match lo with [ pair loc ofs ⇒
     187        let 〈loc,ofs〉 ≝ lo in
    188188          match pointer_compat_dec loc r with
    189189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
    190190          | inr _ ⇒ Error ? (msg TypeMismatch)
    191191          ]
    192         ]
    193192      | _ ⇒ Error ? (msg BadlyTypedTerm)
    194193      ]
     
    294293[ nil ⇒ 〈en, m〉
    295294| cons h vars ⇒
    296   match h with [ pair id ty ⇒
    297     match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
     295  let 〈id,ty〉 ≝ h in
     296  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
    298297      exec_alloc_variables (add ?? en id b1) m1 vars
    299 ]]].
     298].
    300299
    301300axiom WrongNumberOfParameters : String.
     
    306305  match params with
    307306  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
    308   | cons idty params' ⇒ match idty with [ pair id ty ⇒
     307  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
    309308      match vs with
    310309      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
     
    314313          exec_bind_parameters e m1 params' vl
    315314      ]
    316   ] ].
     315  ].
    317316
    318317let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
     
    338337definition store_value_of_type' ≝
    339338λty,m,l,v.
    340 match l with [ pair loc ofs ⇒
    341   store_value_of_type ty m loc ofs v ].
     339let 〈loc,ofs〉 ≝ l in
     340  store_value_of_type ty m loc ofs v.
    342341
    343342axiom NonsenseState : String.
     
    465464  | Sgoto lbl ⇒
    466465      match find_label lbl (fn_body f) (call_cont k) with
    467       [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
     466      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
    468467      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
    469468      ]
     
    473472  match f0 with
    474473  [ CL_Internal f ⇒
    475     match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
     474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
    476475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
    477476      ret ? 〈E0, State f (fn_body f) k e m2〉
    478     ]
    479477  | CL_External f argtys retty ⇒
    480478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
     
    488486    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
    489487    | Some r' ⇒
    490       match r' with [ pair l ty ⇒
     488      let 〈l,ty〉 ≝ r' in
    491489          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
    492490          ret ? 〈E0, (State f Sskip k' e m')〉
    493       ]
    494491    ]
    495492  | _ ⇒ Wrong ??? (msg NonsenseState)
  • src/Clight/Csyntax.ma

    r1224 r1599  
    327327  match params with
    328328  [ nil ⇒ Tnil
    329   | cons h rem ⇒ match h with [ pair id ty ⇒ Tcons ty (type_of_params rem) ]
     329  | cons h rem ⇒ let 〈id,ty〉 ≝ h in Tcons ty (type_of_params rem)
    330330  ].
    331331
  • src/Clight/casts.ma

    r1516 r1599  
    7676
    7777lemma split_left : ∀A,m,n,h,t.
    78   split A (S m) n (h:::t) = let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉.
     78  split A (S m) n (h:::t) = (let 〈l,r〉 ≝ split A m n t in 〈h:::l,r〉).
    7979#A #m #n #h #t normalize >split_eq' @refl
    8080qed.
  • src/Clight/test/search.c.ma

    r1238 r1599  
    215215@refl
    216216qed.
     217
     218example csc: True.
     219letin yyy ≝ (
     220let xxx ≝ (clight_to_cminor myprog) in
     221do p ← xxx ; cminor_to_rtlabs p)
     222normalize in yyy;
     223include "RTLabs/RTLabsToRTL.ma".
     224
     225example csc: True.
     226letin xxx ≝ (clight_to_cminor myprog)
     227letin yyy ≝ (do p ← xxx ; cminor_to_rtlabs p)
     228letin zzz ≝ (do p ← yyy ; rtlabs_to_rtl p)
     229@⊥ normalize in xxx;
  • src/Clight/test/sum.test.ma

    r1332 r1599  
    3333@refl
    3434qed.
     35
     36include "RTLabs/RTLabsToRTL.ma".
     37include alias "basics/lists/list.ma".
     38
     39definition take_out: ∀A. res A → A ≝
     40 λA,a. match a with [ OK x ⇒ x | Error _ ⇒ ?].
     41cases daemon
     42qed.
     43
     44example CSC: True.
     45letin xxx ≝
     46 (let p ≝ take_out … (clight_to_cminor myprog) in
     47  let p ≝ take_out … (cminor_to_rtlabs p) in
     48(*   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)) *)
     49  let p ≝ rtlabs_to_rtl p in
     50   (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ joint_if_code … f]) (prog_funct … p))
     51 )
     52[2: cases daemon]
     53normalize in xxx;
     54
     55
     56[2:
     57  OK (list (codeT (prog_var_names … p) (rtl_params (prog_var_names … p)))) (list_map … (λx. match (\snd x) return λ_.codeT (prog_var_names … p) (rtl_params ?) with [External _ ⇒ ? | Internal f ⇒ ?(*joint_if_code ? (rtl_params ?) f*)]) (prog_funct … p)))
     58(*  OK ? (map … (λx. match (\snd x) with [External _ ⇒ ? | Internal f ⇒ f_graph … f]) (prog_funct … p)))
     59*)
     60[2: check (joint_if_code (prog_var_names … p) ? f) |3: cases daemon  ]
     61normalize in xxx
     62
Note: See TracChangeset for help on using the changeset viewer.