Changeset 2773 for extracted/label.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/label.ml

    r2717 r2773  
    11open Preamble
    22
    3 open BitVectorTrie
    4 
    53open CostLabel
    64
     
    2119open Extralib
    2220
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
    2347open Setoids
    2448
     
    2650
    2751open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    5452
    5553open Extranat
     
    109107  List.append (Types.option_map_def labels_of_expr List.Nil oe)
    110108    (List.append (labels_of_expr e1)
    111       (Util.foldl (fun ls e0 -> List.append (labels_of_expr e0) ls) List.Nil
     109      (Util.foldl (fun ls e -> List.append (labels_of_expr e) ls) List.Nil
    112110        es))
    113111| Csyntax.Ssequence (s1, s2) ->
     
    185183    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
    186184    Identifiers.universe) Types.prod **)
    187 let add_cost_expr e0 gen =
     185let add_cost_expr e gen =
    188186  let { Types.fst = l; Types.snd = gen0 } =
    189187    Identifiers.fresh PreIdentifiers.CostTag gen
    190188  in
    191   { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e0)),
    192   (Csyntax.typeof e0))); Types.snd = gen0 }
     189  { Types.fst = (Csyntax.Expr ((Csyntax.Ecost (l, e)), (Csyntax.typeof e)));
     190  Types.snd = gen0 }
    193191
    194192(** val const_int : AST.intsize -> Nat.nat -> Csyntax.expr **)
    195193let const_int sz n =
    196   Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr0 sz n))), (Csyntax.Tint
     194  Csyntax.Expr ((Csyntax.Econst_int (sz, (AST.repr sz n))), (Csyntax.Tint
    197195    (sz, AST.Signed)))
    198196
     
    200198    Csyntax.expr -> Identifiers.universe -> (Csyntax.expr,
    201199    Identifiers.universe) Types.prod **)
    202 let rec label_expr e0 costgen =
    203   let Csyntax.Expr (ed, ty) = e0 in
     200let rec label_expr e costgen =
     201  let Csyntax.Expr (ed, ty) = e in
    204202  let { Types.fst = ed0; Types.snd = costgen0 } =
    205203    label_expr_descr ed costgen ty
     
    209207    Csyntax.expr_descr -> Identifiers.universe -> Csyntax.type0 ->
    210208    (Csyntax.expr_descr, Identifiers.universe) Types.prod **)
    211 and label_expr_descr e0 costgen ty =
    212   match e0 with
    213   | Csyntax.Econst_int (x, x0) -> { Types.fst = e0; Types.snd = costgen }
    214   | Csyntax.Evar x -> { Types.fst = e0; Types.snd = costgen }
     209and label_expr_descr e costgen ty =
     210  match e with
     211  | Csyntax.Econst_int (x, x0) -> { Types.fst = e; Types.snd = costgen }
     212  | Csyntax.Evar x -> { Types.fst = e; Types.snd = costgen }
    215213  | Csyntax.Ederef e' ->
    216214    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
     
    219217    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    220218    { Types.fst = (Csyntax.Eaddrof e'0); Types.snd = costgen0 }
    221   | Csyntax.Eunop (op0, e') ->
     219  | Csyntax.Eunop (op, e') ->
    222220    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
    223     { Types.fst = (Csyntax.Eunop (op0, e'0)); Types.snd = costgen0 }
    224   | Csyntax.Ebinop (op0, e1, e2) ->
     221    { Types.fst = (Csyntax.Eunop (op, e'0)); Types.snd = costgen0 }
     222  | Csyntax.Ebinop (op, e1, e2) ->
    225223    let { Types.fst = e10; Types.snd = costgen0 } = label_expr e1 costgen in
    226224    let { Types.fst = e20; Types.snd = costgen1 } = label_expr e2 costgen0 in
    227     { Types.fst = (Csyntax.Ebinop (op0, e10, e20)); Types.snd = costgen1 }
     225    { Types.fst = (Csyntax.Ebinop (op, e10, e20)); Types.snd = costgen1 }
    228226  | Csyntax.Ecast (ty0, e') ->
    229227    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
     
    505503       { Types.fst = (Csyntax.Econdition (e10, et0, e21)); Types.snd =
    506504       costgen5 })
    507   | Csyntax.Esizeof x -> { Types.fst = e0; Types.snd = costgen }
     505  | Csyntax.Esizeof x -> { Types.fst = e; Types.snd = costgen }
    508506  | Csyntax.Efield (e', id) ->
    509507    let { Types.fst = e'0; Types.snd = costgen0 } = label_expr e' costgen in
     
    519517  match l with
    520518  | List.Nil -> { Types.fst = List.Nil; Types.snd = costgen }
    521   | List.Cons (e0, es) ->
    522     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     519  | List.Cons (e, es) ->
     520    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    523521    let { Types.fst = es0; Types.snd = costgen1 } = label_exprs es costgen0
    524522    in
    525     { Types.fst = (List.Cons (e1, es0)); Types.snd = costgen1 }
     523    { Types.fst = (List.Cons (e0, es0)); Types.snd = costgen1 }
    526524
    527525(** val label_opt_expr :
     
    531529  match oe with
    532530  | Types.None -> { Types.fst = Types.None; Types.snd = costgen }
    533   | Types.Some e0 ->
    534     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
    535     { Types.fst = (Types.Some e1); Types.snd = costgen0 }
     531  | Types.Some e ->
     532    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
     533    { Types.fst = (Types.Some e0); Types.snd = costgen0 }
    536534
    537535(** val label_statement :
     
    565563    in
    566564    { Types.fst = (Csyntax.Ssequence (s10, s20)); Types.snd = costgen1 }
    567   | Csyntax.Sifthenelse (e0, s1, s2) ->
    568     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     565  | Csyntax.Sifthenelse (e, s1, s2) ->
     566    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    569567    let { Types.fst = s10; Types.snd = costgen1 } =
    570568      label_statement s1 costgen0
     
    579577      add_cost_before s20 costgen3
    580578    in
    581     { Types.fst = (Csyntax.Sifthenelse (e1, s11, s21)); Types.snd =
     579    { Types.fst = (Csyntax.Sifthenelse (e0, s11, s21)); Types.snd =
    582580    costgen4 }
    583   | Csyntax.Swhile (e0, s') ->
    584     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     581  | Csyntax.Swhile (e, s') ->
     582    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    585583    let { Types.fst = s'0; Types.snd = costgen1 } =
    586584      label_statement s' costgen0
     
    590588    in
    591589    let { Types.fst = s0; Types.snd = costgen3 } =
    592       add_cost_after (Csyntax.Swhile (e1, s'1)) costgen2
     590      add_cost_after (Csyntax.Swhile (e0, s'1)) costgen2
    593591    in
    594592    { Types.fst = s0; Types.snd = costgen3 }
    595   | Csyntax.Sdowhile (e0, s') ->
    596     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     593  | Csyntax.Sdowhile (e, s') ->
     594    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    597595    let { Types.fst = s'0; Types.snd = costgen1 } =
    598596      label_statement s' costgen0
     
    602600    in
    603601    let { Types.fst = s0; Types.snd = costgen3 } =
    604       add_cost_after (Csyntax.Sdowhile (e1, s'1)) costgen2
     602      add_cost_after (Csyntax.Sdowhile (e0, s'1)) costgen2
    605603    in
    606604    { Types.fst = s0; Types.snd = costgen3 }
    607   | Csyntax.Sfor (s1, e0, s2, s3) ->
    608     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     605  | Csyntax.Sfor (s1, e, s2, s3) ->
     606    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    609607    let { Types.fst = s10; Types.snd = costgen1 } =
    610608      label_statement s1 costgen0
     
    620618    in
    621619    let { Types.fst = s0; Types.snd = costgen5 } =
    622       add_cost_after (Csyntax.Sfor (s10, e1, s20, s31)) costgen4
     620      add_cost_after (Csyntax.Sfor (s10, e0, s20, s31)) costgen4
    623621    in
    624622    { Types.fst = s0; Types.snd = costgen5 }
     
    631629    in
    632630    { Types.fst = (Csyntax.Sreturn opt_e0); Types.snd = costgen0 }
    633   | Csyntax.Sswitch (e0, ls) ->
    634     let { Types.fst = e1; Types.snd = costgen0 } = label_expr e0 costgen in
     631  | Csyntax.Sswitch (e, ls) ->
     632    let { Types.fst = e0; Types.snd = costgen0 } = label_expr e costgen in
    635633    let { Types.fst = ls0; Types.snd = costgen1 } =
    636634      label_lstatements ls costgen0
    637635    in
    638     { Types.fst = (Csyntax.Sswitch (e1, ls0)); Types.snd = costgen1 }
     636    { Types.fst = (Csyntax.Sswitch (e0, ls0)); Types.snd = costgen1 }
    639637  | Csyntax.Slabel (l, s') ->
    640638    let { Types.fst = s'0; Types.snd = costgen0 } =
Note: See TracChangeset for help on using the changeset viewer.