Ignore:
Timestamp:
Feb 25, 2013, 9:54:49 PM (7 years ago)
Author:
sacerdot
Message:

Exported again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/globalenvs.ml

    r2717 r2730  
    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_6504 =
     100let rec genv_t_rect_Type4 h_mk_genv_t x_2466 =
    101101  let { functions = functions0; nextfunction = nextfunction0; symbols =
    102     symbols0 } = x_6504
     102    symbols0 } = x_2466
    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_6506 =
     109let rec genv_t_rect_Type5 h_mk_genv_t x_2468 =
    110110  let { functions = functions0; nextfunction = nextfunction0; symbols =
    111     symbols0 } = x_6506
     111    symbols0 } = x_2468
    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_6508 =
     118let rec genv_t_rect_Type3 h_mk_genv_t x_2470 =
    119119  let { functions = functions0; nextfunction = nextfunction0; symbols =
    120     symbols0 } = x_6508
     120    symbols0 } = x_2470
    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_6510 =
     127let rec genv_t_rect_Type2 h_mk_genv_t x_2472 =
    128128  let { functions = functions0; nextfunction = nextfunction0; symbols =
    129     symbols0 } = x_6510
     129    symbols0 } = x_2472
    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_6512 =
     136let rec genv_t_rect_Type1 h_mk_genv_t x_2474 =
    137137  let { functions = functions0; nextfunction = nextfunction0; symbols =
    138     symbols0 } = x_6512
     138    symbols0 } = x_2474
    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_6514 =
     145let rec genv_t_rect_Type0 h_mk_genv_t x_2476 =
    146146  let { functions = functions0; nextfunction = nextfunction0; symbols =
    147     symbols0 } = x_6514
     147    symbols0 } = x_2476
    148148  in
    149149  h_mk_genv_t functions0 nextfunction0 symbols0 __
     
    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 = eta860; Types.snd = init_info } = id_init in
     317    let { Types.fst = id; Types.snd = r } = eta860 in
    318318    let init = extract_init init_info in
    319319    let { Types.fst = g0; Types.snd = st } = g_st in
     
    330330let init_globals extract_init g0 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 = eta861; Types.snd = init_info } = id_init in
     333    let { Types.fst = id; Types.snd = r } = eta861 in
    334334    let init = extract_init init_info in
    335335    Obj.magic
     
    405405   | Types.None -> (fun _ -> assert false (* absurd case *))
    406406   | Types.Some id -> (fun _ -> id)) __
     407
     408(** val symbol_of_function_block' :
     409    'a1 genv_t -> Pointers.block -> 'a1 -> AST.ident **)
     410let symbol_of_function_block' ge b f =
     411  symbol_of_function_block ge b
     412
     413(** val find_funct_ptr_id :
     414    'a1 genv_t -> Pointers.block -> ('a1, AST.ident) Types.prod Types.option **)
     415let find_funct_ptr_id ge b =
     416  (match find_funct_ptr ge b with
     417   | Types.None -> (fun _ -> Types.None)
     418   | Types.Some f ->
     419     (fun _ -> Types.Some { Types.fst = f; Types.snd =
     420       (symbol_of_function_block' ge b f) })) __
     421
     422(** val symbol_of_function_val : 'a1 genv_t -> Values.val0 -> AST.ident **)
     423let symbol_of_function_val ge v =
     424  (match v with
     425   | Values.Vundef -> (fun _ -> assert false (* absurd case *))
     426   | Values.Vint (x, x0) -> (fun _ -> assert false (* absurd case *))
     427   | Values.Vnull -> (fun _ -> assert false (* absurd case *))
     428   | Values.Vptr p ->
     429     (fun _ -> symbol_of_function_block ge p.Pointers.pblock)) __
     430
     431(** val symbol_of_function_val' :
     432    'a1 genv_t -> Values.val0 -> 'a1 -> AST.ident **)
     433let symbol_of_function_val' ge v f =
     434  symbol_of_function_val ge v
     435
     436(** val find_funct_id :
     437    'a1 genv_t -> Values.val0 -> ('a1, AST.ident) Types.prod Types.option **)
     438let find_funct_id ge v =
     439  (match find_funct ge v with
     440   | Types.None -> (fun _ -> Types.None)
     441   | Types.Some f ->
     442     (fun _ -> Types.Some { Types.fst = f; Types.snd =
     443       (symbol_of_function_val' ge v f) })) __
    407444
    408445(** val nat_plus_pos : Nat.nat -> Positive.pos -> Positive.pos **)
     
    442479
    443480(** val related_globals_rect_Type4 :
    444     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    445     'a3 **)
    446 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
    447   h_mk_related_globals __ __ __
    448 
    449 (** val related_globals_rect_Type5 :
    450     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    451     'a3 **)
    452 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
    453   h_mk_related_globals __ __ __
    454 
    455 (** val related_globals_rect_Type3 :
    456     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    457     'a3 **)
    458 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
    459   h_mk_related_globals __ __ __
    460 
    461 (** val related_globals_rect_Type2 :
    462     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    463     'a3 **)
    464 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
    465   h_mk_related_globals __ __ __
    466 
    467 (** val related_globals_rect_Type1 :
    468     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    469     'a3 **)
    470 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
    471   h_mk_related_globals __ __ __
    472 
    473 (** val related_globals_rect_Type0 :
    474     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> 'a3) ->
    475     'a3 **)
    476 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
    477   h_mk_related_globals __ __ __
    478 
    479 (** val related_globals_inv_rect_Type4 :
    480481    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    481482    -> 'a3 **)
     483let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
     484  h_mk_related_globals __ __ __ __
     485
     486(** val related_globals_rect_Type5 :
     487    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
     488    -> 'a3 **)
     489let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
     490  h_mk_related_globals __ __ __ __
     491
     492(** val related_globals_rect_Type3 :
     493    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
     494    -> 'a3 **)
     495let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
     496  h_mk_related_globals __ __ __ __
     497
     498(** val related_globals_rect_Type2 :
     499    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
     500    -> 'a3 **)
     501let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
     502  h_mk_related_globals __ __ __ __
     503
     504(** val related_globals_rect_Type1 :
     505    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
     506    -> 'a3 **)
     507let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
     508  h_mk_related_globals __ __ __ __
     509
     510(** val related_globals_rect_Type0 :
     511    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
     512    -> 'a3 **)
     513let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
     514  h_mk_related_globals __ __ __ __
     515
     516(** val related_globals_inv_rect_Type4 :
     517    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
     518    -> 'a3) -> 'a3 **)
    482519let related_globals_inv_rect_Type4 x3 x4 x5 h1 =
    483520  let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __
    484521
    485522(** val related_globals_inv_rect_Type3 :
    486     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    487     -> 'a3 **)
     523    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
     524    -> 'a3) -> 'a3 **)
    488525let related_globals_inv_rect_Type3 x3 x4 x5 h1 =
    489526  let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __
    490527
    491528(** val related_globals_inv_rect_Type2 :
    492     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    493     -> 'a3 **)
     529    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
     530    -> 'a3) -> 'a3 **)
    494531let related_globals_inv_rect_Type2 x3 x4 x5 h1 =
    495532  let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __
    496533
    497534(** val related_globals_inv_rect_Type1 :
    498     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    499     -> 'a3 **)
     535    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
     536    -> 'a3) -> 'a3 **)
    500537let related_globals_inv_rect_Type1 x3 x4 x5 h1 =
    501538  let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __
    502539
    503540(** val related_globals_inv_rect_Type0 :
    504     ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> 'a3)
    505     -> 'a3 **)
     541    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __ -> __ -> __ -> __
     542    -> 'a3) -> 'a3 **)
    506543let related_globals_inv_rect_Type0 x3 x4 x5 h1 =
    507544  let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __
     
    510547    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
    511548let related_globals_discr a3 a4 a5 =
    512   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
     549  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
    513550
    514551(** val related_globals_jmdiscr :
    515552    ('a1 -> 'a2) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
    516553let related_globals_jmdiscr a3 a4 a5 =
    517   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
     554  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
    518555
    519556(** val related_globals_gen_rect_Type4 :
    520557    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    521558    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    522     __ -> __ -> 'a3) -> 'a3 **)
     559    __ -> __ -> __ -> 'a3) -> 'a3 **)
    523560let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen =
    524   h_mk_related_globals_gen __ __ __
     561  h_mk_related_globals_gen __ __ __ __
    525562
    526563(** val related_globals_gen_rect_Type5 :
    527564    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    528565    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    529     __ -> __ -> 'a3) -> 'a3 **)
     566    __ -> __ -> __ -> 'a3) -> 'a3 **)
    530567let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen =
    531   h_mk_related_globals_gen __ __ __
     568  h_mk_related_globals_gen __ __ __ __
    532569
    533570(** val related_globals_gen_rect_Type3 :
    534571    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    535572    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    536     __ -> __ -> 'a3) -> 'a3 **)
     573    __ -> __ -> __ -> 'a3) -> 'a3 **)
    537574let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen =
    538   h_mk_related_globals_gen __ __ __
     575  h_mk_related_globals_gen __ __ __ __
    539576
    540577(** val related_globals_gen_rect_Type2 :
    541578    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    542579    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    543     __ -> __ -> 'a3) -> 'a3 **)
     580    __ -> __ -> __ -> 'a3) -> 'a3 **)
    544581let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen =
    545   h_mk_related_globals_gen __ __ __
     582  h_mk_related_globals_gen __ __ __ __
    546583
    547584(** val related_globals_gen_rect_Type1 :
    548585    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    549586    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    550     __ -> __ -> 'a3) -> 'a3 **)
     587    __ -> __ -> __ -> 'a3) -> 'a3 **)
    551588let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen =
    552   h_mk_related_globals_gen __ __ __
     589  h_mk_related_globals_gen __ __ __ __
    553590
    554591(** val related_globals_gen_rect_Type0 :
    555592    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    556593    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    557     __ -> __ -> 'a3) -> 'a3 **)
     594    __ -> __ -> __ -> 'a3) -> 'a3 **)
    558595let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen =
    559   h_mk_related_globals_gen __ __ __
     596  h_mk_related_globals_gen __ __ __ __
    560597
    561598(** val related_globals_gen_inv_rect_Type4 :
    562599    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    563600    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    564     __ -> __ -> __ -> 'a3) -> 'a3 **)
     601    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    565602let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 =
    566603  let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __
     
    569606    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    570607    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    571     __ -> __ -> __ -> 'a3) -> 'a3 **)
     608    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    572609let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 =
    573610  let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __
     
    576613    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    577614    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    578     __ -> __ -> __ -> 'a3) -> 'a3 **)
     615    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    579616let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 =
    580617  let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __
     
    583620    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    584621    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    585     __ -> __ -> __ -> 'a3) -> 'a3 **)
     622    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    586623let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 =
    587624  let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __
     
    590627    PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    591628    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ ->
    592     __ -> __ -> __ -> 'a3) -> 'a3 **)
     629    __ -> __ -> __ -> __ -> 'a3) -> 'a3 **)
    593630let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 =
    594631  let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __
     
    598635    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
    599636let related_globals_gen_discr a1 a4 a5 a6 =
    600   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
     637  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
    601638
    602639(** val related_globals_gen_jmdiscr :
     
    604641    Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __ **)
    605642let related_globals_gen_jmdiscr a1 a4 a5 a6 =
    606   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
     643  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __ __)) __
    607644
    608645open Extra_bool
Note: See TracChangeset for help on using the changeset viewer.