Changeset 2773 for extracted/toRTLabs.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (8 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/toRTLabs.ml

    r2743 r2773  
    9595open Globalenvs
    9696
     97open CostLabel
     98
     99open FrontEndOps
     100
     101open Cminor_syntax
     102
    97103open BitVectorTrie
    98 
    99 open CostLabel
    100 
    101 open FrontEndOps
    102 
    103 open Cminor_syntax
    104104
    105105open Graphs
     
    121121  List.foldr (fun idt rsengen ->
    122122    let { Types.fst = id; Types.snd = ty } = idt in
    123     let { Types.fst = eta2917; Types.snd = gen0 } = rsengen in
    124     let { Types.fst = rs; Types.snd = en0 } = eta2917 in
     123    let { Types.fst = eta1690; Types.snd = gen0 } = rsengen in
     124    let { Types.fst = rs; Types.snd = en0 } = eta1690 in
    125125    let { Types.fst = r; Types.snd = gen' } =
    126126      Identifiers.fresh PreIdentifiers.RegisterTag gen0
     
    133133
    134134(** val lookup_reg : env -> AST.ident -> AST.typ -> Registers.register **)
    135 let lookup_reg e0 id ty =
    136   (Identifiers.lookup_present PreIdentifiers.SymbolTag e0 id).Types.fst
     135let lookup_reg e id ty =
     136  (Identifiers.lookup_present PreIdentifiers.SymbolTag e id).Types.fst
    137137
    138138type fixed = { fx_gotos : Identifiers.identifier_set; fx_env : env;
     
    142142    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    143143    fixed -> 'a1 **)
    144 let rec fixed_rect_Type4 h_mk_fixed x_15343 =
     144let rec fixed_rect_Type4 h_mk_fixed x_10525 =
    145145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    146     x_15343
     146    x_10525
    147147  in
    148148  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    151151    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    152152    fixed -> 'a1 **)
    153 let rec fixed_rect_Type5 h_mk_fixed x_15345 =
     153let rec fixed_rect_Type5 h_mk_fixed x_10527 =
    154154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    155     x_15345
     155    x_10527
    156156  in
    157157  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    160160    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    161161    fixed -> 'a1 **)
    162 let rec fixed_rect_Type3 h_mk_fixed x_15347 =
     162let rec fixed_rect_Type3 h_mk_fixed x_10529 =
    163163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    164     x_15347
     164    x_10529
    165165  in
    166166  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    169169    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    170170    fixed -> 'a1 **)
    171 let rec fixed_rect_Type2 h_mk_fixed x_15349 =
     171let rec fixed_rect_Type2 h_mk_fixed x_10531 =
    172172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    173     x_15349
     173    x_10531
    174174  in
    175175  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    178178    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    179179    fixed -> 'a1 **)
    180 let rec fixed_rect_Type1 h_mk_fixed x_15351 =
     180let rec fixed_rect_Type1 h_mk_fixed x_10533 =
    181181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    182     x_15351
     182    x_10533
    183183  in
    184184  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    187187    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    188188    fixed -> 'a1 **)
    189 let rec fixed_rect_Type0 h_mk_fixed x_15353 =
     189let rec fixed_rect_Type0 h_mk_fixed x_10535 =
    190190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    191     x_15353
     191    x_10535
    192192  in
    193193  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    257257    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    258258    -> goto_map -> 'a1 **)
    259 let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_15369 =
    260   let gm_map = x_15369 in h_mk_goto_map gm_map __ __
     259let rec goto_map_rect_Type4 fx g h_mk_goto_map x_10551 =
     260  let gm_map = x_10551 in h_mk_goto_map gm_map __ __
    261261
    262262(** val goto_map_rect_Type5 :
     
    264264    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    265265    -> goto_map -> 'a1 **)
    266 let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_15371 =
    267   let gm_map = x_15371 in h_mk_goto_map gm_map __ __
     266let rec goto_map_rect_Type5 fx g h_mk_goto_map x_10553 =
     267  let gm_map = x_10553 in h_mk_goto_map gm_map __ __
    268268
    269269(** val goto_map_rect_Type3 :
     
    271271    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    272272    -> goto_map -> 'a1 **)
    273 let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_15373 =
    274   let gm_map = x_15373 in h_mk_goto_map gm_map __ __
     273let rec goto_map_rect_Type3 fx g h_mk_goto_map x_10555 =
     274  let gm_map = x_10555 in h_mk_goto_map gm_map __ __
    275275
    276276(** val goto_map_rect_Type2 :
     
    278278    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    279279    -> goto_map -> 'a1 **)
    280 let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_15375 =
    281   let gm_map = x_15375 in h_mk_goto_map gm_map __ __
     280let rec goto_map_rect_Type2 fx g h_mk_goto_map x_10557 =
     281  let gm_map = x_10557 in h_mk_goto_map gm_map __ __
    282282
    283283(** val goto_map_rect_Type1 :
     
    285285    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    286286    -> goto_map -> 'a1 **)
    287 let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_15377 =
    288   let gm_map = x_15377 in h_mk_goto_map gm_map __ __
     287let rec goto_map_rect_Type1 fx g h_mk_goto_map x_10559 =
     288  let gm_map = x_10559 in h_mk_goto_map gm_map __ __
    289289
    290290(** val goto_map_rect_Type0 :
     
    292292    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    293293    -> goto_map -> 'a1 **)
    294 let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_15379 =
    295   let gm_map = x_15379 in h_mk_goto_map gm_map __ __
     294let rec goto_map_rect_Type0 fx g h_mk_goto_map x_10561 =
     295  let gm_map = x_10561 in h_mk_goto_map gm_map __ __
    296296
    297297(** val gm_map :
    298298    fixed -> RTLabs_syntax.statement Graphs.graph -> goto_map ->
    299299    PreIdentifiers.identifier Identifiers.identifier_map **)
    300 let rec gm_map fx g0 xxx =
     300let rec gm_map fx g xxx =
    301301  let yyy = xxx in yyy
    302302
     
    401401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    402402    -> 'a1 **)
    403 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15397 =
     403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_10579 =
    404404  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    405405    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    406406    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    407407    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    408     x_15397
     408    x_10579
    409409  in
    410410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    419419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    420420    -> 'a1 **)
    421 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15399 =
     421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_10581 =
    422422  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    423423    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    424424    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    425425    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    426     x_15399
     426    x_10581
    427427  in
    428428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    437437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    438438    -> 'a1 **)
    439 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15401 =
     439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_10583 =
    440440  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    441441    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    442442    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    443443    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    444     x_15401
     444    x_10583
    445445  in
    446446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    455455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    456456    -> 'a1 **)
    457 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15403 =
     457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_10585 =
    458458  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    459459    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    460460    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    461461    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    462     x_15403
     462    x_10585
    463463  in
    464464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    473473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    474474    -> 'a1 **)
    475 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15405 =
     475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_10587 =
    476476  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    477477    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    478478    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    479479    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    480     x_15405
     480    x_10587
    481481  in
    482482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    491491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    492492    -> 'a1 **)
    493 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15407 =
     493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_10589 =
    494494  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    495495    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    496496    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    497497    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    498     x_15407
     498    x_10589
    499499  in
    500500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    706706    partial_fn Types.sig0 **)
    707707let add_fresh_to_graph fx s f =
    708   (let { Types.fst = l; Types.snd = g0 } =
     708  (let { Types.fst = l; Types.snd = g } =
    709709     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
    710710   in
    711711  (fun _ ->
    712712  let s1 = s (Types.pi1 f.pf_entry) in
    713   { pf_labgen = g0; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
     713  { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params = f.pf_params;
    714714  pf_locals = f.pf_locals; pf_result = f.pf_result; pf_stacksize =
    715715  f.pf_stacksize; pf_graph =
     
    722722    Registers.register Types.sig0) Types.dPair **)
    723723let fresh_reg fx f ty =
    724   let { Types.fst = r; Types.snd = g0 } =
     724  let { Types.fst = r; Types.snd = g } =
    725725    Identifiers.fresh PreIdentifiers.RegisterTag f.pf_reggen
    726726  in
    727   let f' = { pf_labgen = f.pf_labgen; pf_reggen = g0; pf_params =
    728     f.pf_params; pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty },
    729     f.pf_locals)); pf_result =
     727  let f' = { pf_labgen = f.pf_labgen; pf_reggen = g; pf_params = f.pf_params;
     728    pf_locals = (List.Cons ({ Types.fst = r; Types.snd = ty }, f.pf_locals));
     729    pf_result =
    730730    ((match fx.fx_rettyp with
    731731      | Types.None -> Obj.magic __
     
    741741    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn -> (partial_fn
    742742    Types.sig0, Registers.register Types.sig0) Types.dPair **)
    743 let choose_reg fx ty e0 f =
    744   (match e0 with
     743let choose_reg fx ty e f =
     744  (match e with
    745745   | Cminor_syntax.Id (t, i) ->
    746746     (fun _ -> { Types.dpi1 = f; Types.dpi2 = (lookup_reg fx.fx_env i t) })
     
    777777    Types.sig0) Types.dPair **)
    778778let choose_regs fx es f =
    779   foldr_all' (fun e0 _ tl acc ->
     779  foldr_all' (fun e _ tl acc ->
    780780    let { Types.dpi1 = f1; Types.dpi2 = rs } = acc in
    781     (let { Types.dpi1 = t; Types.dpi2 = e1 } = e0 in
     781    (let { Types.dpi1 = t; Types.dpi2 = e0 } = e in
    782782    (fun _ ->
    783783    let { Types.dpi1 = f'; Types.dpi2 = r } =
    784       choose_reg fx t e1 (Types.pi1 f1)
     784      choose_reg fx t e0 (Types.pi1 f1)
    785785    in
    786786    { Types.dpi1 = (Types.pi1 f'); Types.dpi2 = (List.Cons ((Types.pi1 r),
     
    874874    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    875875    fn_con_because -> 'a1 **)
    876 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15483 = function
     876let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10665 = function
    877877| Fn_con_eq f -> h_fn_con_eq f
    878878| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    884884    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    885885    fn_con_because -> 'a1 **)
    886 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15490 = function
     886let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10672 = function
    887887| Fn_con_eq f -> h_fn_con_eq f
    888888| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    894894    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    895895    fn_con_because -> 'a1 **)
    896 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15497 = function
     896let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10679 = function
    897897| Fn_con_eq f -> h_fn_con_eq f
    898898| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    904904    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    905905    fn_con_because -> 'a1 **)
    906 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15504 = function
     906let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10686 = function
    907907| Fn_con_eq f -> h_fn_con_eq f
    908908| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    914914    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    915915    fn_con_because -> 'a1 **)
    916 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15511 = function
     916let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10693 = function
    917917| Fn_con_eq f -> h_fn_con_eq f
    918918| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    924924    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    925925    fn_con_because -> 'a1 **)
    926 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15518 = function
     926let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_10700 = function
    927927| Fn_con_eq f -> h_fn_con_eq f
    928928| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    999999    fixed -> AST.typ -> Cminor_syntax.expr -> partial_fn ->
    10001000    Registers.register Types.sig0 -> partial_fn Types.sig0 **)
    1001 let rec add_expr fx ty e0 f dst =
    1002   (match e0 with
     1001let rec add_expr fx ty e f dst =
     1002  (match e with
    10031003   | Cminor_syntax.Id (t, i) ->
    10041004     (fun _ dst0 ->
     
    10151015         (add_fresh_to_graph fx (fun x0 -> RTLabs_syntax.St_const (x,
    10161016           (Types.pi1 dst0), c, x0)) f))
    1017    | Cminor_syntax.Op1 (t, t', op0, e') ->
     1017   | Cminor_syntax.Op1 (t, t', op, e') ->
    10181018     (fun _ dst0 ->
    10191019       let { Types.dpi1 = f0; Types.dpi2 = r } = choose_reg fx t e' f in
    10201020       let f1 =
    1021          add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op0,
     1021         add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_op1 (t', t, op,
    10221022           (Types.pi1 dst0), (Types.pi1 r), x)) (Types.pi1 f0)
    10231023       in
    10241024       let f2 = add_expr fx t e' (Types.pi1 f1) (Types.pi1 r) in Types.pi1 f2)
    1025    | Cminor_syntax.Op2 (x, x0, x1, op0, e1, e2) ->
     1025   | Cminor_syntax.Op2 (x, x0, x1, op, e1, e2) ->
    10261026     (fun _ dst0 ->
    1027        let { Types.dpi1 = f0; Types.dpi2 = r5 } = choose_reg fx x e1 f in
    1028        let { Types.dpi1 = f1; Types.dpi2 = r6 } =
     1027       let { Types.dpi1 = f0; Types.dpi2 = r1 } = choose_reg fx x e1 f in
     1028       let { Types.dpi1 = f1; Types.dpi2 = r2 } =
    10291029         choose_reg fx x0 e2 (Types.pi1 f0)
    10301030       in
    10311031       let f2 =
    10321032         add_fresh_to_graph fx (fun x2 -> RTLabs_syntax.St_op2 (x1, x, x0,
    1033            op0, (Types.pi1 dst0), (Types.pi1 r5), (Types.pi1 r6), x2))
     1033           op, (Types.pi1 dst0), (Types.pi1 r1), (Types.pi1 r2), x2))
    10341034           (Types.pi1 f1)
    10351035       in
    1036        let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r6) in
    1037        let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r5) in
     1036       let f3 = add_expr fx x0 e2 (Types.pi1 f2) (Types.pi1 r2) in
     1037       let f4 = add_expr fx x e1 (Types.pi1 f3) (Types.pi1 r1) in
    10381038       Types.pi1 f4)
    10391039   | Cminor_syntax.Mem (t, e') ->
     
    10881088       | List.Nil -> (fun _ -> f)
    10891089       | List.Cons (x1, x2) -> (fun _ -> assert false (* absurd case *)))
    1090    | List.Cons (e0, et) ->
     1090   | List.Cons (e, et) ->
    10911091     (fun _ ->
    10921092       match dsts with
     
    10951095         (fun _ _ ->
    10961096           let f' = add_exprs fx et rt f in
    1097            (let { Types.dpi1 = ty; Types.dpi2 = e1 } = e0 in
     1097           (let { Types.dpi1 = ty; Types.dpi2 = e0 } = e in
    10981098           (fun _ _ ->
    1099            let f'' = add_expr fx ty e1 (Types.pi1 f') r in Types.pi1 f'')) __
     1099           let f'' = add_expr fx ty e0 (Types.pi1 f') r in Types.pi1 f'')) __
    11001100             __))) __ __ __
     1101
     1102(** val stmt_inv_rect_Type4 :
     1103    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
     1104let rec stmt_inv_rect_Type4 fx s h_mk_stmt_inv =
     1105  h_mk_stmt_inv __ __ __
    11011106
    11021107(** val stmt_inv_rect_Type5 :
     
    11051110  h_mk_stmt_inv __ __ __
    11061111
    1107 (** val stmt_inv_rect_Type6 :
     1112(** val stmt_inv_rect_Type3 :
    11081113    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
    1109 let rec stmt_inv_rect_Type6 fx s h_mk_stmt_inv =
     1114let rec stmt_inv_rect_Type3 fx s h_mk_stmt_inv =
    11101115  h_mk_stmt_inv __ __ __
    11111116
    1112 (** val stmt_inv_rect_Type7 :
     1117(** val stmt_inv_rect_Type2 :
    11131118    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
    1114 let rec stmt_inv_rect_Type7 fx s h_mk_stmt_inv =
     1119let rec stmt_inv_rect_Type2 fx s h_mk_stmt_inv =
    11151120  h_mk_stmt_inv __ __ __
    11161121
    1117 (** val stmt_inv_rect_Type8 :
     1122(** val stmt_inv_rect_Type1 :
    11181123    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
    1119 let rec stmt_inv_rect_Type8 fx s h_mk_stmt_inv =
     1124let rec stmt_inv_rect_Type1 fx s h_mk_stmt_inv =
    11201125  h_mk_stmt_inv __ __ __
    11211126
    1122 (** val stmt_inv_rect_Type9 :
     1127(** val stmt_inv_rect_Type0 :
    11231128    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
    1124 let rec stmt_inv_rect_Type9 fx s h_mk_stmt_inv =
    1125   h_mk_stmt_inv __ __ __
    1126 
    1127 (** val stmt_inv_rect_Type10 :
    1128     fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
    1129 let rec stmt_inv_rect_Type10 fx s h_mk_stmt_inv =
     1129let rec stmt_inv_rect_Type0 fx s h_mk_stmt_inv =
    11301130  h_mk_stmt_inv __ __ __
    11311131
     
    11331133    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    11341134let stmt_inv_inv_rect_Type4 x1 x2 h1 =
    1135   let hcut = stmt_inv_rect_Type5 x1 x2 h1 in hcut __
     1135  let hcut = stmt_inv_rect_Type4 x1 x2 h1 in hcut __
    11361136
    11371137(** val stmt_inv_inv_rect_Type3 :
    11381138    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    11391139let stmt_inv_inv_rect_Type3 x1 x2 h1 =
    1140   let hcut = stmt_inv_rect_Type7 x1 x2 h1 in hcut __
     1140  let hcut = stmt_inv_rect_Type3 x1 x2 h1 in hcut __
    11411141
    11421142(** val stmt_inv_inv_rect_Type2 :
    11431143    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    11441144let stmt_inv_inv_rect_Type2 x1 x2 h1 =
    1145   let hcut = stmt_inv_rect_Type8 x1 x2 h1 in hcut __
     1145  let hcut = stmt_inv_rect_Type2 x1 x2 h1 in hcut __
    11461146
    11471147(** val stmt_inv_inv_rect_Type1 :
    11481148    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    11491149let stmt_inv_inv_rect_Type1 x1 x2 h1 =
    1150   let hcut = stmt_inv_rect_Type9 x1 x2 h1 in hcut __
     1150  let hcut = stmt_inv_rect_Type1 x1 x2 h1 in hcut __
    11511151
    11521152(** val stmt_inv_inv_rect_Type0 :
    11531153    fixed -> Cminor_syntax.stmt -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
    11541154let stmt_inv_inv_rect_Type0 x1 x2 h1 =
    1155   let hcut = stmt_inv_rect_Type10 x1 x2 h1 in hcut __
     1155  let hcut = stmt_inv_rect_Type0 x1 x2 h1 in hcut __
    11561156
    11571157(** val stmt_inv_discr : fixed -> Cminor_syntax.stmt -> __ **)
     
    11971197   | Types.None -> (fun _ -> Types.pi1 f1)
    11981198   | Types.Some et ->
    1199      let { Types.dpi1 = ty; Types.dpi2 = e0 } = et in
     1199     let { Types.dpi1 = ty; Types.dpi2 = e } = et in
    12001200     (fun _ ->
    12011201     (match fx.fx_rettyp with
     
    12031203      | Types.Some t ->
    12041204        (fun _ r ->
    1205           let r5 = Obj.magic r in
    1206           let f2 = add_expr fx ty e0 (Types.pi1 f1) r5 in Types.pi1 f2)) __
     1205          let r0 = Obj.magic r in
     1206          let f2 = add_expr fx ty e (Types.pi1 f1) r0 in Types.pi1 f2)) __
    12071207       (Types.pi1 f1).pf_result)) __
    12081208
     
    12201220    fixed -> partial_fn -> PreIdentifiers.identifier -> partial_fn Types.sig0 **)
    12211221let add_goto_dummy fx f dest =
    1222   (let { Types.fst = l; Types.snd = g0 } =
     1222  (let { Types.fst = l; Types.snd = g } =
    12231223     Identifiers.fresh PreIdentifiers.LabelTag f.pf_labgen
    12241224   in
    1225   (fun _ -> { pf_labgen = g0; pf_reggen = f.pf_reggen; pf_params =
     1225  (fun _ -> { pf_labgen = g; pf_reggen = f.pf_reggen; pf_params =
    12261226  f.pf_params; pf_locals = f.pf_locals; pf_result = f.pf_result;
    12271227  pf_stacksize = f.pf_stacksize; pf_graph =
     
    12371237  (match s with
    12381238   | Cminor_syntax.St_skip -> (fun _ -> f)
    1239    | Cminor_syntax.St_assign (t, x, e0) ->
     1239   | Cminor_syntax.St_assign (t, x, e) ->
    12401240     (fun _ ->
    12411241       let dst = lookup_reg fx.fx_env x t in
    1242        Types.pi1 (add_expr fx t e0 f dst))
     1242       Types.pi1 (add_expr fx t e f dst))
    12431243   | Cminor_syntax.St_store (t, e1, e2) ->
    12441244     (fun _ ->
     
    12551255       in
    12561256       Types.pi1 (add_expr fx t e2 (Types.pi1 f3) (Types.pi1 val_reg)))
    1257    | Cminor_syntax.St_call (return_opt_id, e0, args) ->
     1257   | Cminor_syntax.St_call (return_opt_id, e, args) ->
    12581258     (fun _ ->
    12591259       let return_opt_reg =
     
    12681268       in
    12691269       let f1 =
    1270          match expr_is_Id AST.ASTptr e0 with
     1270         match expr_is_Id AST.ASTptr e with
    12711271         | Types.None ->
    12721272           let { Types.dpi1 = f1; Types.dpi2 = fnr } =
    1273              choose_reg fx AST.ASTptr e0 (Types.pi1 f0)
     1273             choose_reg fx AST.ASTptr e (Types.pi1 f0)
    12741274           in
    12751275           let f2 =
     
    12791279           in
    12801280           Types.pi1
    1281              (add_expr fx AST.ASTptr e0 (Types.pi1 f2) (Types.pi1 fnr))
     1281             (add_expr fx AST.ASTptr e (Types.pi1 f2) (Types.pi1 fnr))
    12821282         | Types.Some id ->
    12831283           add_fresh_to_graph fx (fun x -> RTLabs_syntax.St_call_id (id,
     
    12891289       let f2 = add_stmt fx s2 f in
    12901290       let f1 = add_stmt fx s1 (Types.pi1 f2) in Types.pi1 f1)
    1291    | Cminor_syntax.St_ifthenelse (x, x0, e0, s1, s2) ->
     1291   | Cminor_syntax.St_ifthenelse (x, x0, e, s1, s2) ->
    12921292     (fun _ ->
    12931293       let l_next = f.pf_entry in
     
    12971297       let f1 = add_stmt fx s1 (Types.pi1 f0) in
    12981298       let { Types.dpi1 = f3; Types.dpi2 = r } =
    1299          choose_reg fx (AST.ASTint (x, x0)) e0 (Types.pi1 f1)
     1299         choose_reg fx (AST.ASTint (x, x0)) e (Types.pi1 f1)
    13001300       in
    13011301       let f4 =
     
    13041304       in
    13051305       Types.pi1
    1306          (add_expr fx (AST.ASTint (x, x0)) e0 (Types.pi1 f4) (Types.pi1 r)))
     1306         (add_expr fx (AST.ASTint (x, x0)) e (Types.pi1 f4) (Types.pi1 r)))
    13071307   | Cminor_syntax.St_return opt_e -> (fun _ -> add_return fx opt_e f)
    13081308   | Cminor_syntax.St_label (l, s') ->
     
    13321332  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13331333  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1334   (let { Types.fst = eta3144; Types.snd = reggen1 } =
     1334  (let { Types.fst = eta1917; Types.snd = reggen1 } =
    13351335     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13361336       f.Cminor_syntax.f_params
    13371337   in
    1338   let { Types.fst = params; Types.snd = env1 } = eta3144 in
     1338  let { Types.fst = params; Types.snd = env1 } = eta1917 in
    13391339  (fun _ ->
    1340   (let { Types.fst = eta3143; Types.snd = reggen2 } =
     1340  (let { Types.fst = eta1916; Types.snd = reggen2 } =
    13411341     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13421342   in
    1343   let { Types.fst = locals0; Types.snd = env0 } = eta3143 in
     1343  let { Types.fst = locals0; Types.snd = env0 } = eta1916 in
    13441344  (fun _ ->
    13451345  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset for help on using the changeset viewer.