Changeset 886


Ignore:
Timestamp:
Jun 6, 2011, 1:27:59 PM (8 years ago)
Author:
campbell
Message:

Put types into parameter and variable lists in Cminor.
Temporarily breaks translation to RTLabs.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r882 r886  
    698698
    699699
    700 definition is_pointer : type → bool ≝
    701 λty.
    702   match ty with
    703   [ Tpointer _ _ ⇒ true
    704   | Tfunction _ _ ⇒ true
    705   | _ ⇒ false
    706   ].
    707 
    708700definition bigid1 ≝ an_identifier SymbolTag [[
    709701false;true;false;false;
     
    717709false;false;false;true]].
    718710
     711(* FIXME: the temporary handling is nonsense, I'm afraid. *)
    719712definition translate_function : list (ident×region) → function → res internal_function ≝
    720713λglobals, f.
     
    722715  let tmp ≝ bigid1 in (* FIXME *)
    723716  let tmpp ≝ bigid2 in (* FIXME *)
    724   let p_ptrs ≝ filter ? (λx. is_pointer (\snd x)) (fn_params f) in
    725   let v_ptrs ≝ (filter ? (λx. is_pointer (\snd x)) (fn_vars f)) in
    726717  do s ← translate_statement vartypes tmp tmpp (fn_body f);
    727718  OK ? (mk_internal_function
    728     (signature_of_type (type_of_params (fn_params f)) (fn_return f))
    729     (map ?? (fst ??) (fn_params f))
    730     (tmp::tmpp::(map ?? (fst ??) (fn_vars f)))
    731     (tmpp::(map ?? (fst ??) p_ptrs) @ (map ?? (fst ??) v_ptrs))
     719    (opttyp_of_type (fn_return f))
     720    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
     721    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
    732722    stacksize
    733723    s).
  • src/Cminor/semantics.ma

    r881 r886  
    131131axiom WrongNumberOfParameters : String.
    132132
    133 let rec bind_params (vs:list val) (ids:list ident) : res env ≝
     133(* TODO: perhaps should do a little type checking? *)
     134let rec bind_params (vs:list val) (ids:list (ident×typ)) : res env ≝
    134135match vs with
    135136[ nil ⇒ match ids with [ nil ⇒ OK ? (empty_map ??) | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     
    137138    match ids with
    138139    [ nil ⇒ Error ? (msg WrongNumberOfParameters)
    139     | cons id idt ⇒
     140    | cons idh idt ⇒
     141        let 〈id,ty〉 ≝ idh in
    140142        do en ← bind_params vt idt;
    141143        OK ? (add ?? en id v)
     
    143145].
    144146
    145 definition init_locals : env → list ident → env ≝
    146 foldr ?? (λid,en. add ?? en id Vundef).
     147(* TODO: perhaps should do a little type checking? *)
     148definition init_locals : env → list (ident×typ) → env ≝
     149foldr ?? (λidty,en. add ?? en (\fst idty) Vundef).
    147150
    148151axiom FailedStore : String.
  • src/Cminor/syntax.ma

    r881 r886  
    3434
    3535record internal_function : Type[0] ≝
    36 { f_sig       : signature
    37 ; f_params    : list ident
    38 ; f_vars      : list ident
    39 ; f_ptrs      : list ident
     36{ f_return    : option typ
     37; f_params    : list (ident × typ)
     38; f_vars      : list (ident × typ)
    4039; f_stacksize : nat
    4140; f_body      : stmt
Note: See TracChangeset for help on using the changeset viewer.