Changeset 1599 for src/Clight/Cexec.ma


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.

File:
1 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)
Note: See TracChangeset for help on using the changeset viewer.