Changeset 2717 for extracted/toRTLabs.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/toRTLabs.ml

    r2649 r2717  
    6969open Identifiers
    7070
     71open Exp
     72
    7173open Arithmetic
    7274
     
    9395open Globalenvs
    9496
     97open BitVectorTrie
     98
    9599open CostLabel
    96100
     
    98102
    99103open Cminor_syntax
    100 
    101 open BitVectorTrie
    102104
    103105open Graphs
     
    119121  List.foldr (fun idt rsengen ->
    120122    let { Types.fst = id; Types.snd = ty } = idt in
    121     let { Types.fst = eta1303; Types.snd = gen0 } = rsengen in
    122     let { Types.fst = rs; Types.snd = en0 } = eta1303 in
     123    let { Types.fst = eta2892; Types.snd = gen0 } = rsengen in
     124    let { Types.fst = rs; Types.snd = en0 } = eta2892 in
    123125    let { Types.fst = r; Types.snd = gen' } =
    124126      Identifiers.fresh PreIdentifiers.RegisterTag gen0
     
    140142    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    141143    fixed -> 'a1 **)
    142 let rec fixed_rect_Type4 h_mk_fixed x_12027 =
     144let rec fixed_rect_Type4 h_mk_fixed x_15317 =
    143145  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    144     x_12027
     146    x_15317
    145147  in
    146148  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    149151    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    150152    fixed -> 'a1 **)
    151 let rec fixed_rect_Type5 h_mk_fixed x_12029 =
     153let rec fixed_rect_Type5 h_mk_fixed x_15319 =
    152154  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    153     x_12029
     155    x_15319
    154156  in
    155157  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    158160    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    159161    fixed -> 'a1 **)
    160 let rec fixed_rect_Type3 h_mk_fixed x_12031 =
     162let rec fixed_rect_Type3 h_mk_fixed x_15321 =
    161163  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    162     x_12031
     164    x_15321
    163165  in
    164166  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    167169    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    168170    fixed -> 'a1 **)
    169 let rec fixed_rect_Type2 h_mk_fixed x_12033 =
     171let rec fixed_rect_Type2 h_mk_fixed x_15323 =
    170172  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    171     x_12033
     173    x_15323
    172174  in
    173175  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    176178    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    177179    fixed -> 'a1 **)
    178 let rec fixed_rect_Type1 h_mk_fixed x_12035 =
     180let rec fixed_rect_Type1 h_mk_fixed x_15325 =
    179181  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    180     x_12035
     182    x_15325
    181183  in
    182184  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    185187    (Identifiers.identifier_set -> env -> AST.typ Types.option -> 'a1) ->
    186188    fixed -> 'a1 **)
    187 let rec fixed_rect_Type0 h_mk_fixed x_12037 =
     189let rec fixed_rect_Type0 h_mk_fixed x_15327 =
    188190  let { fx_gotos = fx_gotos0; fx_env = fx_env0; fx_rettyp = fx_rettyp0 } =
    189     x_12037
     191    x_15327
    190192  in
    191193  h_mk_fixed fx_gotos0 fx_env0 fx_rettyp0
     
    255257    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    256258    -> goto_map -> 'a1 **)
    257 let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_12053 =
    258   let gm_map = x_12053 in h_mk_goto_map gm_map __ __
     259let rec goto_map_rect_Type4 fx g0 h_mk_goto_map x_15343 =
     260  let gm_map = x_15343 in h_mk_goto_map gm_map __ __
    259261
    260262(** val goto_map_rect_Type5 :
     
    262264    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    263265    -> goto_map -> 'a1 **)
    264 let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_12055 =
    265   let gm_map = x_12055 in h_mk_goto_map gm_map __ __
     266let rec goto_map_rect_Type5 fx g0 h_mk_goto_map x_15345 =
     267  let gm_map = x_15345 in h_mk_goto_map gm_map __ __
    266268
    267269(** val goto_map_rect_Type3 :
     
    269271    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    270272    -> goto_map -> 'a1 **)
    271 let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_12057 =
    272   let gm_map = x_12057 in h_mk_goto_map gm_map __ __
     273let rec goto_map_rect_Type3 fx g0 h_mk_goto_map x_15347 =
     274  let gm_map = x_15347 in h_mk_goto_map gm_map __ __
    273275
    274276(** val goto_map_rect_Type2 :
     
    276278    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    277279    -> goto_map -> 'a1 **)
    278 let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_12059 =
    279   let gm_map = x_12059 in h_mk_goto_map gm_map __ __
     280let rec goto_map_rect_Type2 fx g0 h_mk_goto_map x_15349 =
     281  let gm_map = x_15349 in h_mk_goto_map gm_map __ __
    280282
    281283(** val goto_map_rect_Type1 :
     
    283285    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    284286    -> goto_map -> 'a1 **)
    285 let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_12061 =
    286   let gm_map = x_12061 in h_mk_goto_map gm_map __ __
     287let rec goto_map_rect_Type1 fx g0 h_mk_goto_map x_15351 =
     288  let gm_map = x_15351 in h_mk_goto_map gm_map __ __
    287289
    288290(** val goto_map_rect_Type0 :
     
    290292    (PreIdentifiers.identifier Identifiers.identifier_map -> __ -> __ -> 'a1)
    291293    -> goto_map -> 'a1 **)
    292 let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_12063 =
    293   let gm_map = x_12063 in h_mk_goto_map gm_map __ __
     294let rec goto_map_rect_Type0 fx g0 h_mk_goto_map x_15353 =
     295  let gm_map = x_15353 in h_mk_goto_map gm_map __ __
    294296
    295297(** val gm_map :
     
    399401    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    400402    -> 'a1 **)
    401 let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_12081 =
     403let rec partial_fn_rect_Type4 fx h_mk_partial_fn x_15371 =
    402404  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    403405    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    404406    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    405407    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    406     x_12081
     408    x_15371
    407409  in
    408410  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    417419    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    418420    -> 'a1 **)
    419 let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_12083 =
     421let rec partial_fn_rect_Type5 fx h_mk_partial_fn x_15373 =
    420422  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    421423    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    422424    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    423425    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    424     x_12083
     426    x_15373
    425427  in
    426428  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    435437    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    436438    -> 'a1 **)
    437 let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_12085 =
     439let rec partial_fn_rect_Type3 fx h_mk_partial_fn x_15375 =
    438440  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    439441    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    440442    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    441443    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    442     x_12085
     444    x_15375
    443445  in
    444446  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    453455    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    454456    -> 'a1 **)
    455 let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_12087 =
     457let rec partial_fn_rect_Type2 fx h_mk_partial_fn x_15377 =
    456458  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    457459    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    458460    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    459461    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    460     x_12087
     462    x_15377
    461463  in
    462464  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    471473    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    472474    -> 'a1 **)
    473 let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_12089 =
     475let rec partial_fn_rect_Type1 fx h_mk_partial_fn x_15379 =
    474476  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    475477    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    476478    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    477479    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    478     x_12089
     480    x_15379
    479481  in
    480482  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    489491    Graphs.label Types.sig0 -> Graphs.label Types.sig0 -> 'a1) -> partial_fn
    490492    -> 'a1 **)
    491 let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_12091 =
     493let rec partial_fn_rect_Type0 fx h_mk_partial_fn x_15381 =
    492494  let { pf_labgen = pf_labgen0; pf_reggen = pf_reggen0; pf_params =
    493495    pf_params0; pf_locals = pf_locals0; pf_result = pf_result0;
    494496    pf_stacksize = pf_stacksize0; pf_graph = pf_graph0; pf_gotos = pf_gotos0;
    495497    pf_labels = pf_labels0; pf_entry = pf_entry0; pf_exit = pf_exit0 } =
    496     x_12091
     498    x_15381
    497499  in
    498500  h_mk_partial_fn pf_labgen0 pf_reggen0 pf_params0 pf_locals0 pf_result0 __
     
    872874    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    873875    fn_con_because -> 'a1 **)
    874 let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12167 = function
     876let rec fn_con_because_rect_Type4 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15457 = function
    875877| Fn_con_eq f -> h_fn_con_eq f
    876878| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    882884    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    883885    fn_con_because -> 'a1 **)
    884 let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12174 = function
     886let rec fn_con_because_rect_Type5 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15464 = function
    885887| Fn_con_eq f -> h_fn_con_eq f
    886888| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    892894    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    893895    fn_con_because -> 'a1 **)
    894 let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12181 = function
     896let rec fn_con_because_rect_Type3 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15471 = function
    895897| Fn_con_eq f -> h_fn_con_eq f
    896898| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    902904    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    903905    fn_con_because -> 'a1 **)
    904 let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12188 = function
     906let rec fn_con_because_rect_Type2 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15478 = function
    905907| Fn_con_eq f -> h_fn_con_eq f
    906908| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    912914    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    913915    fn_con_because -> 'a1 **)
    914 let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12195 = function
     916let rec fn_con_because_rect_Type1 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15485 = function
    915917| Fn_con_eq f -> h_fn_con_eq f
    916918| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    922924    Cminor_syntax.stmt -> partial_fn Types.sig0 -> 'a1) -> partial_fn ->
    923925    fn_con_because -> 'a1 **)
    924 let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_12202 = function
     926let rec fn_con_because_rect_Type0 fx h_fn_con_eq h_fn_con_sig h_fn_con_addinv x_15492 = function
    925927| Fn_con_eq f -> h_fn_con_eq f
    926928| Fn_con_sig (f1, f2, f3) -> h_fn_con_sig f1 f2 __ f3
     
    13301332  let reggen0 = Identifiers.new_universe PreIdentifiers.RegisterTag in
    13311333  let cminor_labels = Cminor_syntax.labels_of f.Cminor_syntax.f_body in
    1332   (let { Types.fst = eta1530; Types.snd = reggen1 } =
     1334  (let { Types.fst = eta3119; Types.snd = reggen1 } =
    13331335     populate_env (Identifiers.empty_map PreIdentifiers.SymbolTag) reggen0
    13341336       f.Cminor_syntax.f_params
    13351337   in
    1336   let { Types.fst = params; Types.snd = env1 } = eta1530 in
     1338  let { Types.fst = params; Types.snd = env1 } = eta3119 in
    13371339  (fun _ ->
    1338   (let { Types.fst = eta1529; Types.snd = reggen2 } =
     1340  (let { Types.fst = eta3118; Types.snd = reggen2 } =
    13391341     populate_env env1 reggen1 f.Cminor_syntax.f_vars
    13401342   in
    1341   let { Types.fst = locals0; Types.snd = env0 } = eta1529 in
     1343  let { Types.fst = locals0; Types.snd = env0 } = eta3118 in
    13421344  (fun _ ->
    13431345  (let { Types.dpi1 = locals_reggen; Types.dpi2 = result } =
Note: See TracChangeset for help on using the changeset viewer.