Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Author:
campbell
Message:

Port Clight semantics to the new-new matita syntax.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Globalenvs.ma

    r485 r487  
    4040
    4141(* FIXME: unimplemented stuff in AST.ma
    42 naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V).
    43 naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W).
    44 naxiom match_program: ∀A,B,V,W:Type. program A V → program B W → Prop.
     42axiom transform_partial_program: ∀A,B,V:Type[0]. (A → res B) → program A V → res (program B V).
     43axiom transform_partial_program2: ∀A,B,V,W:Type[0]. (A → res B) → (V → res W) → program A V → res (program B W).
     44axiom match_program: ∀A,B,V,W:Type[0]. program A V → program B W → Prop.
    4545*)
    4646
    47 nrecord GENV : Type[2] ≝ {
     47record GENV : Type[2] ≝ {
    4848(* * ** Types and operations *)
    4949
    50   genv_t : Type → Type;
     50  genv_t : Type[0] → Type[0];
    5151   (* * The type of global environments.  The parameter [F] is the type
    5252       of function descriptions. *)
    5353
    54   globalenv: ∀F,V: Type. program F V → res (genv_t F);
     54  globalenv: ∀F,V: Type[0]. program F V → res (genv_t F);
    5555   (* * Return the global environment for the given program. *)
    5656
    57   init_mem: ∀F,V: Type. program F V → res mem;
     57  init_mem: ∀F,V: Type[0]. program F V → res mem;
    5858   (* * Return the initial memory state for the given program. *)
    5959
    60   find_funct_ptr: ∀F: Type. genv_t F → block → option F;
     60  find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F;
    6161   (* * Return the function description associated with the given address,
    6262       if any. *)
    6363
    64   find_funct: ∀F: Type. genv_t F → val → option F;
     64  find_funct: ∀F: Type[0]. genv_t F → val → option F;
    6565   (* * Same as [find_funct_ptr] but the function address is given as
    6666       a value, which must be a pointer with offset 0. *)
    6767
    68   find_symbol: ∀F: Type. genv_t F → ident → option (region × block)(*;
     68  find_symbol: ∀F: Type[0]. genv_t F → ident → option (region × block)(*;
    6969   (* * Return the address of the given global symbol, if any. *)
    7070
     
    7272
    7373  find_funct_inv:
    74     ∀F: Type. ∀ge: genv_t F. ∀v: val. ∀f: F.
     74    ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F.
    7575    find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero;
    7676  find_funct_find_funct_ptr:
    77     ∀F: Type. ∀ge: genv_t F. ∀sp. ∀b: block.
     77    ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block.
    7878    find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b;
    7979
    8080  find_symbol_exists:
    81     ∀F,V: Type. ∀p: program F V.
     81    ∀F,V: Type[0]. ∀p: program F V.
    8282           ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V.
    8383    in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) →
    8484    ∃b. find_symbol ? (globalenv ?? p) id = Some ? b;
    8585  find_funct_ptr_exists:
    86     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀f: F.
     86    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F.
    8787    list_norepet ? (prog_funct_names ?? p) →
    8888    list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) →
     
    9292
    9393  find_funct_ptr_inversion:
    94     ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
     94    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
    9595    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    9696    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
    9797  find_funct_inversion:
    98     ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
     98    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
    9999    find_funct ? (globalenv ?? p) v = Some ? f →
    100100    ∃id. in_list ? 〈id, f〉 (prog_funct ?? p);
    101101  find_funct_ptr_symbol_inversion:
    102     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
     102    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.
    103103    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 →
    104104    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
     
    106106
    107107  find_funct_ptr_prop:
    108     ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
     108    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.
    109109    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
    110110    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    111111    P f;
    112112  find_funct_prop:
    113     ∀F,V: Type. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
     113    ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.
    114114    (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) →
    115115    find_funct ? (globalenv ?? p) v = Some ? f →
     
    117117
    118118  initmem_nullptr:
    119     ∀F,V: Type. ∀p: program F V.
     119    ∀F,V: Type[0]. ∀p: program F V.
    120120    let m ≝ init_mem ?? p in
    121121    valid_block m nullptr ∧
    122122    (blocks m) nullptr = empty_block 0 0 Any;
    123123(*  initmem_inject_neutral:
    124     ∀F,V: Type. ∀p: program F V.
     124    ∀F,V: Type[0]. ∀p: program F V.
    125125    mem_inject_neutral (init_mem ?? p);*)
    126126  find_funct_ptr_negative:
    127     ∀F,V: Type. ∀p: program F V. ∀b: block. ∀f: F.
     127    ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F.
    128128    find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0;
    129129  find_symbol_not_fresh:
    130     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
     130    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
    131131    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p);
    132132  find_symbol_not_nullptr:
    133     ∀F,V: Type. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
     133    ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.
    134134    find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr;
    135135  global_addresses_distinct:
    136     ∀F,V: Type. ∀p: program F V. ∀id1,id2,b1,b2.
     136    ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2.
    137137    id1≠id2 →
    138138    find_symbol ? (globalenv ?? p) id1 = Some ? b1 →
     
    144144
    145145  find_funct_ptr_transf:
    146     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     146    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    147147    ∀b: block. ∀f: A.
    148148    find_funct_ptr ? (globalenv ?? p) b = Some ? f →
    149149    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);
    150150  find_funct_transf:
    151     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     151    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    152152    ∀v: val. ∀f: A.
    153153    find_funct ? (globalenv ?? p) v = Some ? f →
    154154    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);
    155155  find_symbol_transf:
    156     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     156    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    157157    ∀s: ident.
    158158    find_symbol ? (globalenv ?? (transform_program … transf p)) s =
    159159    find_symbol ? (globalenv ?? p) s;
    160160  init_mem_transf:
    161     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     161    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    162162    init_mem ?? (transform_program … transf p) = init_mem ?? p;
    163163  find_funct_ptr_rev_transf:
    164     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     164    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    165165    ∀b : block. ∀tf : B.
    166166    find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf →
    167167    ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf;
    168168  find_funct_rev_transf:
    169     ∀A,B,V: Type. ∀transf: A → B. ∀p: program A V.
     169    ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.
    170170    ∀v : val. ∀tf : B.
    171171    find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf →
     
    176176
    177177  find_funct_ptr_transf_partial:
    178     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     178    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    179179    transform_partial_program … transf p = OK ? p' →
    180180    ∀b: block. ∀f: A.
     
    183183    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f';
    184184  find_funct_transf_partial:
    185     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     185    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    186186    transform_partial_program … transf p = OK ? p' →
    187187    ∀v: val. ∀f: A.
     
    190190    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f';
    191191  find_symbol_transf_partial:
    192     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     192    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    193193    transform_partial_program … transf p = OK ? p' →
    194194    ∀s: ident.
    195195    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
    196196  init_mem_transf_partial:
    197     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     197    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    198198    transform_partial_program … transf p = OK ? p' →
    199199    init_mem ?? p' = init_mem ?? p;
    200200  find_funct_ptr_rev_transf_partial:
    201     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     201    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    202202    transform_partial_program … transf p = OK ? p' →
    203203    ∀b : block. ∀tf : B.
     
    206206      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf;
    207207  find_funct_rev_transf_partial:
    208     ∀A,B,V: Type. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
     208    ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V.
    209209    transform_partial_program … transf p = OK ? p' →
    210210    ∀v : val. ∀tf : B.
     
    214214
    215215  find_funct_ptr_transf_partial2:
    216     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     216    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    217217           ∀p: program A V. ∀p': program B W.
    218218    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
     
    222222    find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f';
    223223  find_funct_transf_partial2:
    224     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     224    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    225225           ∀p: program A V. ∀p': program B W.
    226226    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
     
    230230    find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f';
    231231  find_symbol_transf_partial2:
    232     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     232    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    233233           ∀p: program A V. ∀p': program B W.
    234234    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
     
    236236    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
    237237  init_mem_transf_partial2:
    238     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     238    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    239239           ∀p: program A V. ∀p': program B W.
    240240    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
    241241    init_mem ?? p' = init_mem ?? p;
    242242  find_funct_ptr_rev_transf_partial2:
    243     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     243    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    244244           ∀p: program A V. ∀p': program B W.
    245245    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
     
    249249      find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf;
    250250  find_funct_rev_transf_partial2:
    251     ∀A,B,V,W: Type. ∀transf_fun: A → res B. ∀transf_var: V → res W.
     251    ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W.
    252252           ∀p: program A V. ∀p': program B W.
    253253    transform_partial_program2 … transf_fun transf_var p = OK ? p' →
     
    261261
    262262  find_funct_ptr_match:
    263     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     263    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    264264           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    265265    match_program … match_fun match_var p p' →
     
    269269    find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf;
    270270  find_funct_ptr_rev_match:
    271     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     271    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    272272           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    273273    match_program … match_fun match_var p p' →
     
    277277    find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf;
    278278  find_funct_match:
    279     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     279    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    280280           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    281281    match_program … match_fun match_var p p' →
     
    284284    ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf;
    285285  find_funct_rev_match:
    286     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     286    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    287287           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    288288    match_program … match_fun match_var p p' →
     
    291291    ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf;
    292292  find_symbol_match:
    293     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     293    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    294294           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    295295    match_program … match_fun match_var p p' →
     
    297297    find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s;
    298298  init_mem_match:
    299     ∀A,B,V,W: Type. ∀match_fun: A → B → Prop.
     299    ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop.
    300300           ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W.
    301301    match_program … match_fun match_var p p' →
     
    304304
    305305
    306 nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝
     306let rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l : A ≝
    307307match l with
    308308[ nil ⇒ a
     
    314314(* XXX: temporary definition
    315315   NB: only global functions, no global variables *)
    316 nrecord genv (F:Type) : Type ≝ {
     316record genv (F:Type[0]) : Type[0] ≝ {
    317317  functions: block → option F;
    318318  nextfunction: Z;
     
    327327Section GENV.
    328328
    329 Variable F: Type.                    (* The type of functions *)
     329Variable F: Type[0].                    (* The type of functions *)
    330330Variable V: Type.                    (* The type of information over variables *)
    331331
     
    339339*)
    340340
    341 ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝
     341definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝
    342342λF,name_fun,g.
    343343  let b ≝ nextfunction ? g in
     
    346346            ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉 | inr _ ⇒ (symbols ? g i) ]).
    347347
    348 ndefinition add_symbol : ∀F:Type. ident → region → block → genv F → genv F ≝
     348definition add_symbol : ∀F:Type[0]. ident → region → block → genv F → genv F ≝
    349349λF,name,bsp,b,g.
    350350  mk_genv F (functions ? g)
     
    387387*)
    388388(* Construct environment and initial memory store *)
    389 ndefinition empty_mem ≝ empty. (* XXX*)
    390 ndefinition empty : ∀F. genv F ≝
     389definition empty_mem ≝ empty. (* XXX*)
     390definition empty : ∀F. genv F ≝
    391391  λF. mk_genv F (λ_. None ?) (-1) (λ_. None ?).
    392392(*  mkgenv (ZMap.init None) (-1) (PTree.empty block).*)
    393393
    394 ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝
     394definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝
    395395λF,init,fns.
    396396  foldr ?? (add_funct F) init fns.
     
    398398(* init *)
    399399
    400 ndefinition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
     400definition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝
    401401λF,ge,m,r,b,p,id.
    402402  match id with
     
    415415  ].
    416416
    417 ndefinition size_init_data : init_data → Z ≝
     417definition size_init_data : init_data → Z ≝
    418418 λi_data.match i_data with
    419419  [ Init_int8 _ ⇒ 1
     
    426426  | Init_addrof r _ _ ⇒ size_pointer r].
    427427
    428 nlet rec store_init_data_list (F:Type) (ge:genv F)
     428let rec store_init_data_list (F:Type[0]) (ge:genv F)
    429429                              (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data)
    430430                              on idl : option mem ≝
     
    438438  ].
    439439
    440 ndefinition size_init_data_list : list init_data → Z ≝
     440definition size_init_data_list : list init_data → Z ≝
    441441  λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data.
    442442
     
    444444nremark size_init_data_list_pos:
    445445  ∀i_data. OZ ≤ size_init_data_list i_data.
    446 #i_data;nelim i_data;//;
    447 #a;#tl;ncut (OZ ≤ size_init_data a)
    448 ##[ncases a;nnormalize;//;
    449    #x;ncases x;nnormalize;//;
     446#i_data;elim i_data;//;
     447#a;#tl;cut (OZ ≤ size_init_data a)
     448##[cases a;normalize;//;
     449   #x;cases x;normalize;//;
    450450##|#Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl));
    451    ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
    452    ##[ncases (size_init_data a) in Hsize IH;
     451   cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)
     452   ##[cases (size_init_data a) in Hsize IH;
    453453      ##[##1,2:/3/
    454       ##|nnormalize;#n;#Hfalse;nelim Hfalse]
    455    ##|#Hdisc;ncases Hdisc
     454      ##|normalize;#n;#Hfalse;elim Hfalse]
     455   ##|#Hdisc;cases Hdisc
    456456      ##[#Heq;nrewrite > Heq;//;
    457       ##|#Heq;ncases Heq;#x;#Heq2;nrewrite > Heq2;
     457      ##|#Heq;cases Heq;#x;#Heq2;nrewrite > Heq2;
    458458         (* TODO: arithmetics *) napply daemon]
    459459   ##]
    460460##]
    461 nqed.
     461qed.
    462462*)
    463463
    464 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝
     464definition alloc_init_data : mem → list init_data → region → mem × block ≝
    465465  λm,i_data,bcl.
    466466  〈mk_mem (update ? (nextblock m)
     
    473473(* init *)
    474474
    475 ndefinition add_globals : ∀F,V:Type.
     475definition add_globals : ∀F,V:Type[0].
    476476       genv F × mem → list (ident × (list init_data) × region × V) →
    477477       res (genv F × mem) ≝
     
    479479  foldl ??
    480480    (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V.
    481       match id_init with [ mk_pair id_init1 info ⇒
    482       match id_init1 with [ mk_pair id_init2 r ⇒
    483       match id_init2 with [ mk_pair id init ⇒
     481      match id_init with [ pair id_init1 info ⇒
     482      match id_init1 with [ pair id_init2 r ⇒
     483      match id_init2 with [ pair id init ⇒
    484484        do 〈g,st〉 ← g_st;
    485         match alloc_init_data st init r with [ mk_pair st' b ⇒
     485        match alloc_init_data st init r with [ pair st' b ⇒
    486486          let g' ≝ add_symbol ? id r b g in
    487487          do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init);
     
    490490    (OK ? init_env) vars.
    491491
    492 ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝
     492definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝
    493493λF,V,p.
    494494  add_globals F V
     
    496496   (prog_vars ?? p).
    497497
    498 ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F) ≝
     498definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝
    499499λF,V,p.
    500500  do 〈g,m〉 ← globalenv_initmem F V p;
    501501    OK ? g.
    502 ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝
     502definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝
    503503λF,V,p.
    504504  do 〈g,m〉 ← globalenv_initmem F V p;
     
    508508
    509509
    510 ndefinition Genv : GENV ≝ mk_GENV
     510definition Genv : GENV ≝ mk_GENV
    511511  genv  (* genv_t *)
    512512  globalenv_
     
    523523.
    524524(*
    525 ##[ #A B C transf p b f; nelim p; #fns main vars;
    526     nelim fns;
    527     ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct;
    528     ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);
     525##[ #A B C transf p b f; elim p; #fns main vars;
     526    elim fns;
     527    ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct;
     528    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?);
    529529        nrewrite > (?:nextfunction ?? = length ? t);
    530         ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
    531             nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     530        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
     531            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
    532532        ##| nrewrite > (?:nextfunction ?? = length ? t);
    533           ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;
    534               nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
    535           ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??%?);
    536             ##[ #H; ndestruct (H); //;
     533          ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
     534              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     535          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?);
     536            ##[ #H; destruct (H); //;
    537537            ##| #H; napply IH; napply H;
    538538            ##]
     
    540540        ##]
    541541    ##]
    542 ##| #A B C transf p v f; nelim v;
    543     ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    544     ##| ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    545     ##| #pcl b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);
    546         nwhd in ⊢ (??%? → ??%?);
    547         ##[ nelim p; #fns main vars; nelim fns;
    548           ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;
    549           ##| #h t; nelim h; #f fn IH;
    550               nwhd in ⊢ (??%? → ??%?);
     542##| #A B C transf p v f; elim v;
     543    ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
     544    ##| ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct;
     545    ##| #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero);
     546        whd in ⊢ (??%? → ??%?);
     547        ##[ elim p; #fns main vars; elim fns;
     548          ##[ whd in ⊢ (??%? → ??%?); #H; destruct;
     549          ##| #h t; elim h; #f fn IH;
     550              whd in ⊢ (??%? → ??%?);
    551551              nrewrite > (?:nextfunction ?? = length ? t);
    552               ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
    553                 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     552              ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
     553                nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
    554554              ##| nrewrite > (?:nextfunction ?? = length ? t);
    555                 ##[ ##2: nelim t; ##[ //; ##| #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;
    556                 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
    557                 ##| napply eqZb_elim; #e; nwhd in ⊢ (??%? → ??%?); #H;
    558                   ##[ ndestruct (H); //;
     555                ##[ ##2: elim t; ##[ //; ##| #h t IH; whd in ⊢ (??%?); nrewrite > IH;
     556                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     557                ##| napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H;
     558                  ##[ destruct (H); //;
    559559                  ##| napply IH; napply H;
    560560                  ##]
     
    562562              ##]
    563563          ##]
    564        ##| #H; ndestruct;
     564       ##| #H; destruct;
    565565       ##]
    566566    ##]
    567 ##| #A B C transf p id; nelim p; #fns main vars;
    568     nelim fns;
    569     ##[ nnormalize; //
    570     ##| #h t; nelim h; #fid fd; nwhd in ⊢ (??%% → ??%%); #IH;
    571         nelim (ident_eq fid id); #e;
    572         ##[ nwhd in ⊢ (??%%);
     567##| #A B C transf p id; elim p; #fns main vars;
     568    elim fns;
     569    ##[ normalize; //
     570    ##| #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH;
     571        elim (ident_eq fid id); #e;
     572        ##[ whd in ⊢ (??%%);
    573573          nrewrite > (?:nextfunction ?? = length ? t);
    574           ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
    575               nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     574          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
     575              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
    576576          ##| nrewrite > (?:nextfunction ?? = length ? t);
    577             ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
    578                 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     577            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     578                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
    579579            ##| //
    580580            ##]
    581581          ##]
    582         ##| nwhd in ⊢ (??%%); nrewrite > IH; napply refl;
     582        ##| whd in ⊢ (??%%); nrewrite > IH; napply refl;
    583583        ##]
    584584    ##]
    585585##| //;
    586 ##| #A B C transf p b tf; nelim p; #fns main vars;
    587     nelim fns;
    588     ##[ nnormalize; #H; ndestruct;
    589     ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     586##| #A B C transf p b tf; elim p; #fns main vars;
     587    elim fns;
     588    ##[ normalize; #H; destruct;
     589    ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
    590590        nrewrite > (?:nextfunction ?? = length ? t);
    591         ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
    592             nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     591        ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
     592            nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
    593593        ##| nrewrite > (?:nextfunction ?? = length ? t);
    594           ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
    595               nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
    596           ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
    597             ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;
     594          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     595              whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     596          ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     597            ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
    598598            ##| #H; napply IH; napply H;
    599599            ##]
     
    601601        ##]
    602602    ##]
    603 ##| #A B C transf p v tf; nelim p; #fns main vars; nelim v;
    604   ##[ nnormalize; #H; ndestruct;
    605   ##| ##2,3: #x; nnormalize; #H; ndestruct;
    606   ##| #pcl b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);
    607     ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
    608       nelim fns;
    609       ##[ nnormalize; #H; ndestruct;
    610       ##| #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
     603##| #A B C transf p v tf; elim p; #fns main vars; elim v;
     604  ##[ normalize; #H; destruct;
     605  ##| ##2,3: #x; normalize; #H; destruct;
     606  ##| #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero);
     607    ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     608      elim fns;
     609      ##[ normalize; #H; destruct;
     610      ##| #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
    611611          nrewrite > (?:nextfunction ?? = length ? t);
    612           ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;
    613               nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
     612          ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH;
     613              nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]
    614614          ##| nrewrite > (?:nextfunction ?? = length ? t);
    615             ##[ ##2: nelim t; ##[ //; ##| #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
    616                 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
    617             ##| napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));
    618               ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;
     615            ##[ ##2: elim t; ##[ //; ##| #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;
     616                whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]
     617            ##| napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?));
     618              ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //;
    619619              ##| #H; napply IH; napply H;
    620620              ##]
     
    622622          ##]
    623623      ##]
    624     ##| nnormalize; #H; ndestruct;
     624    ##| normalize; #H; destruct;
    625625    ##]
    626626 ##]
    627 ##] nqed.
     627##] qed.
    628628         
    629629
     
    10121012Lemma add_functs_match:
    10131013  forall (fns: list (ident * A)) (tfns: list (ident * B)),
    1014   list_forall2 (match_funct_entry match_fun) fns tfns →
     1014  list_forall2 (match_funct_etry match_fun) fns tfns →
    10151015  let r := add_functs (empty A) fns in
    10161016  let tr := add_functs (empty B) tfns in
     
    10411041Lemma add_functs_rev_match:
    10421042  forall (fns: list (ident * A)) (tfns: list (ident * B)),
    1043   list_forall2 (match_funct_entry match_fun) fns tfns →
     1043  list_forall2 (match_funct_etry match_fun) fns tfns →
    10441044  let r := add_functs (empty A) fns in
    10451045  let tr := add_functs (empty B) tfns in
     
    10721072         (vars: list (ident * list init_data * V))
    10731073         (tvars: list (ident * list init_data * W)),
    1074   list_forall2 (match_var_entry match_var) vars tvars →
     1074  list_forall2 (match_var_etry match_var) vars tvars →
    10751075  snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars).
    10761076Proof.
     
    10911091  forall (vars: list (ident * list init_data * V))
    10921092         (tvars: list (ident * list init_data * W)),
    1093   list_forall2 (match_var_entry match_var) vars tvars →
     1093  list_forall2 (match_var_etry match_var) vars tvars →
    10941094  symbols (fst (add_globals (g1, m) vars)) =
    10951095  symbols (fst (add_globals (g2, m) tvars)).
Note: See TracChangeset for help on using the changeset viewer.