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/linearise.ml

    r2717 r2773  
    99open LabelledObjects
    1010
     11open BitVectorTrie
     12
    1113open Graphs
    1214
     
    1719open Registers
    1820
    19 open BitVectorTrie
    20 
    2121open CostLabel
    2222
     
    3737open Extralib
    3838
     39open Lists
     40
     41open Identifiers
     42
     43open Integers
     44
     45open AST
     46
     47open Division
     48
     49open Exp
     50
     51open Arithmetic
     52
    3953open Setoids
    4054
     
    4256
    4357open Option
    44 
    45 open Lists
    46 
    47 open Identifiers
    48 
    49 open Integers
    50 
    51 open AST
    52 
    53 open Division
    54 
    55 open Exp
    56 
    57 open Arithmetic
    5858
    5959open Extranat
     
    115115   | Joint.CALL (x, x0, x1) -> Joint.Sequential (c, (Obj.magic Types.It))
    116116   | Joint.COND (a, ltrue) ->
    117      (match Identifiers.member0 PreIdentifiers.LabelTag visited
     117     (match Identifiers.member PreIdentifiers.LabelTag visited
    118118              (Obj.magic nxt) with
    119119      | Bool.True -> Joint.FCOND (a, ltrue, (Obj.magic nxt))
     
    133133   | Bool.False ->
    134134     Obj.magic
    135        (Monad.m_return0 (Monad.max_def Option.option0) { Types.fst = x;
     135       (Monad.m_return0 (Monad.max_def Option.option) { Types.fst = x;
    136136         Types.snd = l' }))
    137137
     
    145145    Graphs.label List.list -> Nat.nat -> Nat.nat -> Graphs.label ->
    146146    graph_visit_ret_type **)
    147 let rec graph_visit p globals g0 required visited generated visiting gen_length n entry =
    148   (match chop (fun x ->
    149            Identifiers.member0 PreIdentifiers.LabelTag visited x) visiting with
     147let rec graph_visit p globals g required visited generated visiting gen_length n entry =
     148  (match chop (fun x -> Identifiers.member PreIdentifiers.LabelTag visited x)
     149           visiting with
    150150   | Types.None ->
    151151     (fun _ -> { Types.fst = { Types.fst = visited; Types.snd = required };
     
    164164            in
    165165            let statement =
    166               Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g0)
     166              Identifiers.lookup_safe PreIdentifiers.LabelTag (Obj.magic g)
    167167                vis_hd
    168168            in
     
    190190                (match s with
    191191                 | Joint.COST_LABEL x ->
    192                    (match Identifiers.member0 PreIdentifiers.LabelTag
    193                             visited' (Obj.magic nxt) with
     192                   (match Identifiers.member PreIdentifiers.LabelTag visited'
     193                            (Obj.magic nxt) with
    194194                    | Bool.True ->
    195195                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
     
    205205                        Types.snd = List.Nil })
    206206                 | Joint.CALL (x, x0, x1) ->
    207                    (match Identifiers.member0 PreIdentifiers.LabelTag
    208                             visited' (Obj.magic nxt) with
     207                   (match Identifiers.member PreIdentifiers.LabelTag visited'
     208                            (Obj.magic nxt) with
    209209                    | Bool.True ->
    210210                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
     
    224224                     Types.snd = List.Nil }
    225225                 | Joint.Step_seq x ->
    226                    (match Identifiers.member0 PreIdentifiers.LabelTag
    227                             visited' (Obj.magic nxt) with
     226                   (match Identifiers.member PreIdentifiers.LabelTag visited'
     227                            (Obj.magic nxt) with
    228228                    | Bool.True ->
    229229                      { Types.fst = { Types.fst = (Nat.S Nat.O); Types.snd =
     
    247247                  Types.snd = List.Nil }
    248248            in
    249             graph_visit p globals g0
     249            graph_visit p globals g
    250250              (Identifiers.union_set PreIdentifiers.LabelTag
    251251                add_req_gen.Types.fst.Types.snd required') visited'
     
    258258    Joint.graph_params -> AST.ident List.list -> __ -> Graphs.label
    259259    Types.sig0 -> __ **)
    260 let branch_compress p globals g0 entry =
    261   g0
     260let branch_compress p globals g entry =
     261  g
    262262
    263263(** val filter_labels :
     
    269269    let { Types.fst = l_opt; Types.snd = x } = s in
    270270    { Types.fst =
    271     (Monad.m_bind0 (Monad.max_def Option.option0) l_opt (fun l ->
     271    (Monad.m_bind0 (Monad.max_def Option.option) l_opt (fun l ->
    272272      match test l with
    273       | Bool.True -> Monad.m_return0 (Monad.max_def Option.option0) l
     273      | Bool.True -> Monad.m_return0 (Monad.max_def Option.option) l
    274274      | Bool.False -> Obj.magic Types.None)); Types.snd = x }) (Obj.magic c)
    275275
     
    278278    Types.sig0 -> (__, Graphs.label -> Nat.nat Types.option) Types.prod
    279279    Types.sig0 **)
    280 let linearise_code p globals g0 entry_sig =
    281   let g1 = branch_compress p globals g0 entry_sig in
     280let linearise_code p globals g entry_sig =
     281  let g0 = branch_compress p globals g entry_sig in
    282282  let triple =
    283     graph_visit p globals g1 (Identifiers.empty_set PreIdentifiers.LabelTag)
     283    graph_visit p globals g0 (Identifiers.empty_set PreIdentifiers.LabelTag)
    284284      (Identifiers.empty_map PreIdentifiers.LabelTag) (Obj.magic List.Nil)
    285285      (List.Cons ((Types.pi1 entry_sig), List.Nil)) Nat.O
    286       (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g1))
     286      (Identifiers.id_map_size PreIdentifiers.LabelTag (Obj.magic g0))
    287287      (Types.pi1 entry_sig)
    288288  in
    289   let sigma0 = triple.Types.fst.Types.fst in
     289  let sigma = triple.Types.fst.Types.fst in
    290290  let required = triple.Types.fst.Types.snd in
    291291  let crev = triple.Types.snd in
     
    294294  (Obj.magic
    295295    (filter_labels PreIdentifiers.LabelTag (fun l ->
    296       Identifiers.member0 PreIdentifiers.LabelTag required l) lbld_code));
    297   Types.snd = (Identifiers.lookup0 PreIdentifiers.LabelTag sigma0) }
     296      Identifiers.member PreIdentifiers.LabelTag required l) lbld_code));
     297  Types.snd = (Identifiers.lookup PreIdentifiers.LabelTag sigma) }
    298298
    299299(** val linearise_int_fun :
     
    308308  in
    309309  let code = (Types.pi1 code_sigma).Types.fst in
    310   let sigma0 = (Types.pi1 code_sigma).Types.snd in
     310  let sigma = (Types.pi1 code_sigma).Types.snd in
    311311  let entry = Nat.O in
    312312  { Types.fst = { Joint.joint_if_luniverse =
     
    316316  (Types.pi1 f_sig).Joint.joint_if_params; Joint.joint_if_stacksize =
    317317  (Types.pi1 f_sig).Joint.joint_if_stacksize; Joint.joint_if_code = code;
    318   Joint.joint_if_entry = (Obj.magic entry) }; Types.snd = sigma0 }
     318  Joint.joint_if_entry = (Obj.magic entry) }; Types.snd = sigma }
    319319
    320320(** val linearise :
Note: See TracChangeset for help on using the changeset viewer.