Changeset 2773 for extracted/costInj.ml


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

    r2743 r2773  
    1717open StructuredTraces
    1818
     19open BitVectorTrie
     20
    1921open Graphs
    2022
     
    2830
    2931open SmallstepExec
    30 
    31 open BitVectorTrie
    3232
    3333open CostLabel
     
    142142    RTLabs_syntax.statement Graphs.graph -> PreIdentifiers.identifier
    143143    Identifiers.identifier_map Types.option **)
    144 let reverse_label_map g0 =
    145   Identifiers.foldi0 PreIdentifiers.LabelTag (fun l s m ->
     144let reverse_label_map g =
     145  Identifiers.foldi PreIdentifiers.LabelTag (fun l s m ->
    146146    match m with
    147147    | Types.None -> Types.None
     
    150150       | Types.None -> Types.Some m0
    151151       | Types.Some cl ->
    152          (match Identifiers.lookup0 PreIdentifiers.CostTag m0 cl with
     152         (match Identifiers.lookup PreIdentifiers.CostTag m0 cl with
    153153          | Types.None ->
    154154            Types.Some (Identifiers.add PreIdentifiers.CostTag m0 cl l)
    155           | Types.Some x -> Types.None))) g0 (Types.Some
     155          | Types.Some x -> Types.None))) g (Types.Some
    156156    (Identifiers.empty_map PreIdentifiers.CostTag))
    157157
     
    165165    RTLabs_syntax.rTLabs_program -> Bool.bool **)
    166166let check_program_cost_injectivity p =
    167   Lists.all0 (fun x ->
     167  Lists.all (fun x ->
    168168    match x.Types.snd with
    169169    | AST.Internal f -> check_fun_inj f
Note: See TracChangeset for help on using the changeset viewer.