Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/globalenvs.ml

    r2743 r2773  
    9898    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    9999    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    100 let rec genv_t_rect_Type4 h_mk_genv_t x_6530 =
     100let rec genv_t_rect_Type4 h_mk_genv_t x_1608 =
    101101  let { functions = functions0; nextfunction = nextfunction0; symbols =
    102     symbols0 } = x_6530
     102    symbols0 } = x_1608
    103103  in
    104104  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    107107    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    108108    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    109 let rec genv_t_rect_Type5 h_mk_genv_t x_6532 =
     109let rec genv_t_rect_Type5 h_mk_genv_t x_1610 =
    110110  let { functions = functions0; nextfunction = nextfunction0; symbols =
    111     symbols0 } = x_6532
     111    symbols0 } = x_1610
    112112  in
    113113  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    116116    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    117117    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    118 let rec genv_t_rect_Type3 h_mk_genv_t x_6534 =
     118let rec genv_t_rect_Type3 h_mk_genv_t x_1612 =
    119119  let { functions = functions0; nextfunction = nextfunction0; symbols =
    120     symbols0 } = x_6534
     120    symbols0 } = x_1612
    121121  in
    122122  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    125125    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    126126    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    127 let rec genv_t_rect_Type2 h_mk_genv_t x_6536 =
     127let rec genv_t_rect_Type2 h_mk_genv_t x_1614 =
    128128  let { functions = functions0; nextfunction = nextfunction0; symbols =
    129     symbols0 } = x_6536
     129    symbols0 } = x_1614
    130130  in
    131131  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    134134    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    135135    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    136 let rec genv_t_rect_Type1 h_mk_genv_t x_6538 =
     136let rec genv_t_rect_Type1 h_mk_genv_t x_1616 =
    137137  let { functions = functions0; nextfunction = nextfunction0; symbols =
    138     symbols0 } = x_6538
     138    symbols0 } = x_1616
    139139  in
    140140  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    143143    ('a1 PositiveMap.positive_map -> Positive.pos -> Pointers.block
    144144    Identifiers.identifier_map -> __ -> 'a2) -> 'a1 genv_t -> 'a2 **)
    145 let rec genv_t_rect_Type0 h_mk_genv_t x_6540 =
     145let rec genv_t_rect_Type0 h_mk_genv_t x_1618 =
    146146  let { functions = functions0; nextfunction = nextfunction0; symbols =
    147     symbols0 } = x_6540
     147    symbols0 } = x_1618
    148148  in
    149149  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    204204
    205205(** val drop_fn : AST.ident -> 'a1 genv_t -> 'a1 genv_t **)
    206 let drop_fn id g0 =
     206let drop_fn id g =
    207207  let fns =
    208     match Identifiers.lookup0 PreIdentifiers.SymbolTag g0.symbols id with
    209     | Types.None -> g0.functions
     208    match Identifiers.lookup PreIdentifiers.SymbolTag g.symbols id with
     209    | Types.None -> g.functions
    210210    | Types.Some b' ->
    211211      (match Pointers.block_id b' with
    212        | Z.OZ -> g0.functions
    213        | Z.Pos x -> g0.functions
    214        | Z.Neg p -> PositiveMap.pm_set p Types.None g0.functions)
     212       | Z.OZ -> g.functions
     213       | Z.Pos x -> g.functions
     214       | Z.Neg p -> PositiveMap.pm_set p Types.None g.functions)
    215215  in
    216   { functions = fns; nextfunction = g0.nextfunction; symbols =
    217   (Identifiers.remove PreIdentifiers.SymbolTag g0.symbols id) }
     216  { functions = fns; nextfunction = g.nextfunction; symbols =
     217  (Identifiers.remove PreIdentifiers.SymbolTag g.symbols id) }
    218218
    219219(** val add_funct :
    220220    (AST.ident, 'a1) Types.prod -> 'a1 genv_t -> 'a1 genv_t **)
    221 let add_funct name_fun g0 =
    222   let blk_id = g0.nextfunction in
     221let add_funct name_fun g =
     222  let blk_id = g.nextfunction in
    223223  let b = Z.Neg blk_id in
    224   let g' = drop_fn name_fun.Types.fst g0 in
     224  let g' = drop_fn name_fun.Types.fst g in
    225225  { functions = (PositiveMap.insert blk_id name_fun.Types.snd g'.functions);
    226226  nextfunction = (Positive.succ blk_id); symbols =
     
    229229(** val add_symbol :
    230230    AST.ident -> Pointers.block -> 'a1 genv_t -> 'a1 genv_t **)
    231 let add_symbol name b g0 =
    232   let g' = drop_fn name g0 in
     231let add_symbol name b g =
     232  let g' = drop_fn name g in
    233233  { functions = g'.functions; nextfunction = g'.nextfunction; symbols =
    234234  (Identifiers.add PreIdentifiers.SymbolTag g'.symbols name b) }
    235235
    236 (** val empty_mem : GenMem.mem1 **)
     236(** val empty_mem : GenMem.mem **)
    237237let empty_mem =
    238238  GenMem.empty
    239239
    240 (** val empty0 : 'a1 genv_t **)
    241 let empty0 =
     240(** val empty : 'a1 genv_t **)
     241let empty =
    242242  { functions = PositiveMap.Pm_leaf; nextfunction =
    243243    (Positive.succ_pos_of_nat (Nat.S (Nat.S Nat.O))); symbols =
     
    252252    'a1 genv_t -> AST.ident -> Pointers.block Types.option **)
    253253let find_symbol ge =
    254   Identifiers.lookup0 PreIdentifiers.SymbolTag ge.symbols
     254  Identifiers.lookup PreIdentifiers.SymbolTag ge.symbols
    255255
    256256(** val store_init_data :
    257     'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data ->
    258     GenMem.mem1 Types.option **)
     257    'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data ->
     258    GenMem.mem Types.option **)
    259259let store_init_data ge m b p id =
    260260  let ptr = { Pointers.pblock = b; Pointers.poff =
     
    280280          b'; Pointers.poff =
    281281          (Pointers.shift_offset (AST.bitsize_of_intsize AST.I16)
    282             Pointers.zero_offset (AST.repr0 AST.I16 ofs)) })))
     282            Pointers.zero_offset (AST.repr AST.I16 ofs)) })))
    283283
    284284(** val size_init_data : AST.init_data -> Nat.nat **)
     
    292292
    293293(** val store_init_data_list :
    294     'a1 genv_t -> GenMem.mem1 -> Pointers.block -> Z.z -> AST.init_data
    295     List.list -> GenMem.mem1 Types.option **)
     294    'a1 genv_t -> GenMem.mem -> Pointers.block -> Z.z -> AST.init_data
     295    List.list -> GenMem.mem Types.option **)
    296296let rec store_init_data_list ge m b p = function
    297297| List.Nil -> Types.Some m
     
    309309
    310310(** val add_globals :
    311     ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem1) Types.prod
     311    ('a2 -> AST.init_data List.list) -> ('a1 genv_t, GenMem.mem) Types.prod
    312312    -> ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list -> ('a1
    313     genv_t, GenMem.mem1) Types.prod **)
     313    genv_t, GenMem.mem) Types.prod **)
    314314let add_globals extract_init init_env vars =
    315315  Util.foldl (fun g_st id_init ->
    316     let { Types.fst = eta1792; Types.snd = init_info } = id_init in
    317     let { Types.fst = id; Types.snd = r } = eta1792 in
     316    let { Types.fst = eta117; Types.snd = init_info } = id_init in
     317    let { Types.fst = id; Types.snd = r } = eta117 in
    318318    let init = extract_init init_info in
    319     let { Types.fst = g0; Types.snd = st } = g_st in
     319    let { Types.fst = g; Types.snd = st } = g_st in
    320320    let { Types.fst = st'; Types.snd = b } =
    321321      GenMem.alloc st Z.OZ (Z.z_of_nat (size_init_data_list init))
    322322    in
    323     let g' = add_symbol id b g0 in { Types.fst = g'; Types.snd = st' })
     323    let g' = add_symbol id b g in { Types.fst = g'; Types.snd = st' })
    324324    init_env vars
    325325
    326326(** val init_globals :
    327     ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem1 ->
     327    ('a2 -> AST.init_data List.list) -> 'a1 genv_t -> GenMem.mem ->
    328328    ((AST.ident, AST.region) Types.prod, 'a2) Types.prod List.list ->
    329     GenMem.mem1 Errors.res **)
    330 let init_globals extract_init g0 m vars =
     329    GenMem.mem Errors.res **)
     330let init_globals extract_init g m vars =
    331331  Util.foldl (fun st id_init ->
    332     let { Types.fst = eta1793; Types.snd = init_info } = id_init in
    333     let { Types.fst = id; Types.snd = r } = eta1793 in
     332    let { Types.fst = eta118; Types.snd = init_info } = id_init in
     333    let { Types.fst = id; Types.snd = r } = eta118 in
    334334    let init = extract_init init_info in
    335335    Obj.magic
    336336      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic st) (fun st0 ->
    337         match find_symbol g0 id with
     337        match find_symbol g id with
    338338        | Types.None ->
    339339          Obj.magic (Errors.Error
     
    342342          Obj.magic
    343343            (Errors.opt_to_res (Errors.msg ErrorMessages.InitDataStoreFailed)
    344               (store_init_data_list g0 st0 b Z.OZ init))))) (Errors.OK m)
    345     vars
     344              (store_init_data_list g st0 b Z.OZ init))))) (Errors.OK m) vars
    346345
    347346(** val globalenv_allocmem :
    348347    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> ('a1
    349     genv_t, GenMem.mem1) Types.prod **)
     348    genv_t, GenMem.mem) Types.prod **)
    350349let globalenv_allocmem init_info p =
    351   add_globals init_info { Types.fst = (add_functs empty0 p.AST.prog_funct);
     350  add_globals init_info { Types.fst = (add_functs empty p.AST.prog_funct);
    352351    Types.snd = empty_mem } p.AST.prog_vars
    353352
     
    362361
    363362(** val init_mem :
    364     ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem1
     363    ('a2 -> AST.init_data List.list) -> ('a1, 'a2) AST.program -> GenMem.mem
    365364    Errors.res **)
    366365let init_mem i p =
    367   let { Types.fst = g0; Types.snd = m } = globalenv_allocmem i p in
    368   init_globals i g0 m p.AST.prog_vars
    369 
    370 (** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem1 **)
     366  let { Types.fst = g; Types.snd = m } = globalenv_allocmem i p in
     367  init_globals i g m p.AST.prog_vars
     368
     369(** val alloc_mem : ('a1, Nat.nat) AST.program -> GenMem.mem **)
    371370let alloc_mem p =
    372371  (globalenv_allocmem (fun n -> List.Cons ((AST.Init_space n), List.Nil)) p).Types.snd
     
    396395let symbol_for_block genv b =
    397396  Types.option_map Types.fst
    398     (Identifiers.find0 PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
     397    (Identifiers.find PreIdentifiers.SymbolTag genv.symbols (fun id b' ->
    399398      Pointers.eq_block b b'))
    400399
     
    542541
    543542(** val alloc_pair :
    544     GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
    545     GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1 **)
     543    GenMem.mem -> GenMem.mem -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem ->
     544    GenMem.mem -> Pointers.block -> __ -> 'a1) -> 'a1 **)
    546545let alloc_pair clearme m' l h l' h' x =
    547546  (let { GenMem.blocks = ct; GenMem.nextblock = nx } = clearme in
     
    549548  let { GenMem.blocks = ct'; GenMem.nextblock = nx' } = clearme0 in
    550549  (fun l0 h0 l'0 h'0 _ _ ->
    551   Extralib.eq_rect_Type0_r1 nx' (fun _ h1 ->
     550  Extralib.eq_rect_Type0_r nx' (fun _ h1 ->
    552551    h1 { GenMem.blocks =
    553552      (GenMem.update_block { GenMem.blocks = ct; GenMem.nextblock =
     
    563562      nx' }.GenMem.nextblock __) nx __))) m' l h l' h' __ __ x
    564563
    565 (** val prod_jmdiscr0 :
     564(** val prod_jmdiscr :
    566565    ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __ **)
    567 let prod_jmdiscr0 x y =
     566let prod_jmdiscr x y =
    568567  Logic.eq_rect_Type2 x
    569568    (let { Types.fst = a0; Types.snd = a10 } = x in
Note: See TracChangeset for help on using the changeset viewer.