Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/common/AST.ma

    r1064 r1153  
    282282  prog_funct: list (ident × F);
    283283  prog_main: ident;
    284   prog_vars: list (ident × (list init_data) × region × V)
     284  prog_vars: list (ident × region × V)
    285285}.
    286286
     
    290290
    291291definition prog_var_names ≝ λF,V: Type[0]. λp: program F V.
    292   map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p).
     292  map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ?? p).
    293293
    294294(* * * Generic transformations over programs *)
  • Deliverables/D3.3/id-lookup-branch/common/Errors.ma

    r1102 r1153  
    162162  constructor. auto. auto.
    163163Qed.
    164 
     164*)
     165
     166(* A monadic fold_left2 *)
     167
     168axiom WrongLength: String.
     169
     170let rec mfold_left2
     171  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
     172  (left: list B) (right: list C) on left: res A ≝
     173  match left with
     174  [ nil ⇒
     175    match right with
     176    [ nil ⇒ accu
     177    | cons hd tl ⇒ Error ? (msg WrongLength)
     178    ]
     179  | cons hd tl ⇒
     180    match right with
     181    [ nil ⇒ Error ? (msg WrongLength)
     182    | cons hd' tl' ⇒
     183       do accu ← accu;
     184       mfold_left2 … f (f accu hd hd') tl tl'
     185    ]
     186  ].
     187
     188(*
    165189(** * Reasoning over monadic computations *)
    166190
  • Deliverables/D3.3/id-lookup-branch/common/Globalenvs.ma

    r961 r1153  
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
     54  globalenv: ∀F,V: Type[0]. (V → list init_data) → program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type[0]. program F V → res mem;
     57  init_mem: ∀F,V: Type[0]. (V → list init_data) → program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
     
    486486
    487487definition add_globals : ∀F,V:Type[0].
    488        genv F × mem → list (ident × (list init_data) × region × V) →
     488       (V → (list init_data)) →
     489       genv F × mem → list (ident × region × V) →
    489490       res (genv F × mem) ≝
    490 λF,V,init_env,vars.
     491λF,V,extract_init,init_env,vars.
    491492  foldl ??
    492     (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    493       match id_init with [ pair id_init1 info ⇒
    494       match id_init1 with [ pair id_init2 r ⇒
    495       match id_init2 with [ pair id init ⇒
     493    (λg_st: res (genv F × mem). λid_init: ident × region × V.
     494      let 〈id, r, init_info〉 ≝ id_init in
     495      let init ≝ extract_init init_info in
    496496        do 〈g,st〉 ← g_st;
    497497        match alloc_init_data st init r with [ pair st' b ⇒
     
    499499          do st'' ← opt_to_res ? (msg InitDataStoreFailed) (store_init_data_list F g' st' b OZ init);
    500500            OK ? 〈g', st''〉
    501         ] ] ] ])
     501        ] )
    502502    (OK ? init_env) vars.
    503503
    504 definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
    505 λF,V,p.
    506   add_globals F V
    507    〈add_functs ? (empty …) (prog_funct F V p), empty_mem〉
     504definition globalenv_initmem : ∀F,V:Type[0]. (V → (list init_data)) → program F V → res (genv F × mem) ≝
     505λF,V,init_info,p.
     506  add_globals F V init_info
     507   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉
    508508   (prog_vars ?? p).
    509509
    510 definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
    511 λF,V,p.
    512   do 〈g,m〉 ← globalenv_initmem F V p;
     510definition globalenv_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (genv F) ≝
     511λF,V,i,p.
     512  do 〈g,m〉 ← globalenv_initmem F V i p;
    513513    OK ? g.
    514 definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
    515 λF,V,p.
    516   do 〈g,m〉 ← globalenv_initmem F V p;
     514definition init_mem_ : ∀F,V:Type[0]. (V → list init_data) → program F V → res (mem) ≝
     515λF,V,i,p.
     516  do 〈g,m〉 ← globalenv_initmem F V i p;
    517517    OK ? m.
    518518
  • Deliverables/D3.3/id-lookup-branch/common/Registers.ma

    r1049 r1153  
    1616
    1717axiom register_ord: register → register → order.
    18 
    19 (* dpm: fix the Register/register mismatch *)
    20 axiom Register_of_register: register → Register.
    21 axiom register_of_Register: Register → register.
Note: See TracChangeset for help on using the changeset viewer.