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

    r2743 r2773  
    8080
    8181open Values
    82 
    83 open BitVectorTrie
    8482
    8583open CostLabel
     
    9189    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9290let rec eventval_rect_Type4 h_EVint = function
    93 | EVint (sz, x_5485) -> h_EVint sz x_5485
     91| EVint (sz, x_993) -> h_EVint sz x_993
    9492
    9593(** val eventval_rect_Type5 :
    9694    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    9795let rec eventval_rect_Type5 h_EVint = function
    98 | EVint (sz, x_5488) -> h_EVint sz x_5488
     96| EVint (sz, x_996) -> h_EVint sz x_996
    9997
    10098(** val eventval_rect_Type3 :
    10199    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    102100let rec eventval_rect_Type3 h_EVint = function
    103 | EVint (sz, x_5491) -> h_EVint sz x_5491
     101| EVint (sz, x_999) -> h_EVint sz x_999
    104102
    105103(** val eventval_rect_Type2 :
    106104    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    107105let rec eventval_rect_Type2 h_EVint = function
    108 | EVint (sz, x_5494) -> h_EVint sz x_5494
     106| EVint (sz, x_1002) -> h_EVint sz x_1002
    109107
    110108(** val eventval_rect_Type1 :
    111109    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    112110let rec eventval_rect_Type1 h_EVint = function
    113 | EVint (sz, x_5497) -> h_EVint sz x_5497
     111| EVint (sz, x_1005) -> h_EVint sz x_1005
    114112
    115113(** val eventval_rect_Type0 :
    116114    (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
    117115let rec eventval_rect_Type0 h_EVint = function
    118 | EVint (sz, x_5500) -> h_EVint sz x_5500
     116| EVint (sz, x_1008) -> h_EVint sz x_1008
    119117
    120118(** val eventval_inv_rect_Type4 :
     
    161159    eventval -> 'a1) -> event -> 'a1 **)
    162160let rec event_rect_Type4 h_EVcost h_EVextcall = function
    163 | EVcost x_5525 -> h_EVcost x_5525
     161| EVcost x_1033 -> h_EVcost x_1033
    164162| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    165163
     
    168166    eventval -> 'a1) -> event -> 'a1 **)
    169167let rec event_rect_Type5 h_EVcost h_EVextcall = function
    170 | EVcost x_5529 -> h_EVcost x_5529
     168| EVcost x_1037 -> h_EVcost x_1037
    171169| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    172170
     
    175173    eventval -> 'a1) -> event -> 'a1 **)
    176174let rec event_rect_Type3 h_EVcost h_EVextcall = function
    177 | EVcost x_5533 -> h_EVcost x_5533
     175| EVcost x_1041 -> h_EVcost x_1041
    178176| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    179177
     
    182180    eventval -> 'a1) -> event -> 'a1 **)
    183181let rec event_rect_Type2 h_EVcost h_EVextcall = function
    184 | EVcost x_5537 -> h_EVcost x_5537
     182| EVcost x_1045 -> h_EVcost x_1045
    185183| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    186184
     
    189187    eventval -> 'a1) -> event -> 'a1 **)
    190188let rec event_rect_Type1 h_EVcost h_EVextcall = function
    191 | EVcost x_5541 -> h_EVcost x_5541
     189| EVcost x_1049 -> h_EVcost x_1049
    192190| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    193191
     
    196194    eventval -> 'a1) -> event -> 'a1 **)
    197195let rec event_rect_Type0 h_EVcost h_EVextcall = function
    198 | EVcost x_5545 -> h_EVcost x_5545
     196| EVcost x_1053 -> h_EVcost x_1053
    199197| EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
    200198
     
    254252
    255253(** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
    256 let eextcall name args res1 =
    257   List.Cons ((EVextcall (name, args, res1)), List.Nil)
     254let eextcall name args res =
     255  List.Cons ((EVextcall (name, args, res)), List.Nil)
    258256
    259257(** val eapp : trace -> trace -> trace **)
     
    310308(** val remove_costs : trace -> trace **)
    311309let remove_costs =
    312   List.filter (fun e1 ->
    313     match e1 with
     310  List.filter (fun e ->
     311    match e with
    314312    | EVcost x -> Bool.False
    315313    | EVextcall (x, x0, x1) -> Bool.True)
     
    366364  (match t with
    367365   | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
    368    | List.Cons (e1, t') ->
     366   | List.Cons (e, t') ->
    369367     (fun _ ->
    370368       (match t' with
    371         | List.Nil -> (fun _ -> { Types.fst = e1; Types.snd = t0 })
     369        | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
    372370        | List.Cons (e', t'') ->
    373           (fun _ -> { Types.fst = e1; Types.snd = (lazy (Econsinf' (t',
     371          (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
    374372            t0))) })) __)) __
    375373
     
    377375let rec traceinf_of_traceinf' t' =
    378376  let Econsinf' (t, t'') = Lazy.force t' in
    379   let { Types.fst = e1; Types.snd = tl } = split_traceinf' t t'' in
    380   lazy (Econsinf (e1, (traceinf_of_traceinf' tl)))
    381 
     377  let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
     378  lazy (Econsinf (e, (traceinf_of_traceinf' tl)))
     379
Note: See TracChangeset for help on using the changeset viewer.