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

    r2743 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
     
    149147       | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
    150148       | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
    151     (Util.foldl (fun s0 e0 ->
     149    (Util.foldl (fun s0 e ->
    152150      Identifiers.union_set PreIdentifiers.SymbolTag s0
    153         (gather_mem_vars_expr e0))
     151        (gather_mem_vars_expr e))
    154152      (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
    155153| Csyntax.Ssequence (s1, s2) ->
     
    200198    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    201199let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
    202 | Global x_13003 -> h_Global x_13003
    203 | Stack x_13004 -> h_Stack x_13004
     200| Global x_8081 -> h_Global x_8081
     201| Stack x_8082 -> h_Stack x_8082
    204202| Local -> h_Local
    205203
     
    207205    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    208206let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
    209 | Global x_13009 -> h_Global x_13009
    210 | Stack x_13010 -> h_Stack x_13010
     207| Global x_8087 -> h_Global x_8087
     208| Stack x_8088 -> h_Stack x_8088
    211209| Local -> h_Local
    212210
     
    214212    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    215213let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
    216 | Global x_13015 -> h_Global x_13015
    217 | Stack x_13016 -> h_Stack x_13016
     214| Global x_8093 -> h_Global x_8093
     215| Stack x_8094 -> h_Stack x_8094
    218216| Local -> h_Local
    219217
     
    221219    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    222220let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
    223 | Global x_13021 -> h_Global x_13021
    224 | Stack x_13022 -> h_Stack x_13022
     221| Global x_8099 -> h_Global x_8099
     222| Stack x_8100 -> h_Stack x_8100
    225223| Local -> h_Local
    226224
     
    228226    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    229227let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
    230 | Global x_13027 -> h_Global x_13027
    231 | Stack x_13028 -> h_Stack x_13028
     228| Global x_8105 -> h_Global x_8105
     229| Stack x_8106 -> h_Stack x_8106
    232230| Local -> h_Local
    233231
     
    235233    (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
    236234let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
    237 | Global x_13033 -> h_Global x_13033
    238 | Stack x_13034 -> h_Stack x_13034
     235| Global x_8111 -> h_Global x_8111
     236| Stack x_8112 -> h_Stack x_8112
    239237| Local -> h_Local
    240238
     
    295293    ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
    296294    (PreIdentifiers.SymbolTag, id)), List.Nil))))
    297     (Identifiers.lookup0 PreIdentifiers.SymbolTag vars id)
     295    (Identifiers.lookup PreIdentifiers.SymbolTag vars id)
    298296
    299297(** val always_alloc : Csyntax.type0 -> Bool.bool **)
     
    326324      let { Types.fst = c; Types.snd = stack_high0 } =
    327325        match Bool.orb (always_alloc ty)
    328                 (Identifiers.member0 PreIdentifiers.SymbolTag mem_vars id) with
     326                (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with
    329327        | Bool.True ->
    330328          { Types.fst = (Stack stack_high); Types.snd =
     
    373371(** val region_should_eq :
    374372    AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **)
    375 let region_should_eq clearme r5 x =
     373let region_should_eq clearme r2 x =
    376374  (match clearme with
    377375   | AST.XData ->
     
    386384       | AST.XData ->
    387385         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    388        | AST.Code -> (fun _ p -> Errors.OK p))) r5 __ x
     386       | AST.Code -> (fun _ p -> Errors.OK p))) r2 __ x
    389387
    390388(** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **)
     
    424422    Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
    425423    Cminor_syntax.expr **)
    426 let fix_ptr_type ty n e0 =
    427   e0
     424let fix_ptr_type ty n e =
     425  e
    428426
    429427(** val translate_add :
     
    451449         (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
    452450         (FrontEndOps.Ointconst (AST.I16, AST.Signed,
    453          (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))))))
     451         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))
    454452   | ClassifyOp.Add_case_ip (n, sz, sg, ty) ->
    455453     (fun e1 e2 ->
     
    463461         AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
    464462         AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
    465          (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))),
     463         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))),
    466464         (fix_ptr_type ty n e2))))
    467465   | ClassifyOp.Add_default (x, x0) ->
     
    493491         sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
    494492         sg)), (FrontEndOps.Ointconst (AST.I16, sg,
    495          (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))))))))
     493         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))))
    496494   | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) ->
    497495     (fun e1 e2 ->
     
    510508           (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
    511509           (FrontEndOps.Ointconst (AST.I32, AST.Unsigned,
    512            (AST.repr0 AST.I32 (Csyntax.sizeof ty10))))))))))
     510           (AST.repr AST.I32 (Csyntax.sizeof ty10))))))))))
    513511       | Csyntax.Tpointer x ->
    514512         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    615613(** val complete_cmp :
    616614    Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
    617 let complete_cmp ty' e0 =
     615let complete_cmp ty' e =
    618616  match ty' with
    619617  | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    621619    Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)),
    622620      (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz,
    623       sg)), e0))
     621      sg)), e))
    624622  | Csyntax.Tpointer x ->
    625623    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    668666    AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
    669667    Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
    670 let translate_misc_aop ty1 ty2 ty' op0 =
     668let translate_misc_aop ty1 ty2 ty' op =
    671669  let ty1' = Csyntax.typ_of_type ty1 in
    672670  let ty2' = Csyntax.typ_of_type ty2 in
     
    677675         (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))),
    678676         (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz,
    679          sg)), (op0 sz sg), e1, e2)))
     677         sg)), (op sz sg), e1, e2)))
    680678   | ClassifyOp.Aop_default (x, x0) ->
    681679     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
     
    685683    Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 ->
    686684    Cminor_syntax.expr Errors.res **)
    687 let translate_binop op0 ty1 e1 ty2 e2 ty =
     685let translate_binop op ty1 e1 ty2 e2 ty =
    688686  let ty' = Csyntax.typ_of_type ty in
    689   (match op0 with
     687  (match op with
    690688   | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2
    691689   | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2
     
    707705   | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2
    708706   | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2
    709    | Csyntax.One0 -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
     707   | Csyntax.One -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
    710708   | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2
    711709   | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2
     
    721719    (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    722720  | Csyntax.Tint (sz1, sg1) ->
    723     (fun e0 ->
     721    (fun e ->
    724722      match ty2 with
    725723      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    727725        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint
    728726          (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)),
    729           (Types.pi1 e0)))
     727          (Types.pi1 e)))
    730728      | Csyntax.Tpointer x ->
    731729        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
    732           (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0)))
     730          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
    733731      | Csyntax.Tarray (x, x0) ->
    734732        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
    735           (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0)))
     733          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
    736734      | Csyntax.Tfunction (x, x0) ->
    737735        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    743741        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    744742  | Csyntax.Tpointer x ->
    745     (fun e0 ->
     743    (fun e ->
    746744      match ty2 with
    747745      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    748746      | Csyntax.Tint (sz2, sg2) ->
    749747        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
    750           (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0)))
    751       | Csyntax.Tpointer x0 -> Errors.OK e0
    752       | Csyntax.Tarray (x0, x1) -> Errors.OK e0
     748          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
     749      | Csyntax.Tpointer x0 -> Errors.OK e
     750      | Csyntax.Tarray (x0, x1) -> Errors.OK e
    753751      | Csyntax.Tfunction (x0, x1) ->
    754752        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    760758        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    761759  | Csyntax.Tarray (x, x0) ->
    762     (fun e0 ->
     760    (fun e ->
    763761      match ty2 with
    764762      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    765763      | Csyntax.Tint (sz2, sg2) ->
    766764        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
    767           (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0)))
    768       | Csyntax.Tpointer x1 -> Errors.OK e0
    769       | Csyntax.Tarray (x1, x2) -> Errors.OK e0
     765          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
     766      | Csyntax.Tpointer x1 -> Errors.OK e
     767      | Csyntax.Tarray (x1, x2) -> Errors.OK e
    770768      | Csyntax.Tfunction (x1, x2) ->
    771769        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    793791let cm_one sz sg =
    794792  Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
    795     (AST.repr0 sz (Nat.S Nat.O)))))
     793    (AST.repr sz (Nat.S Nat.O)))))
    796794
    797795(** val translate_expr :
     
    879877           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
    880878         | AST.ASTptr -> Obj.magic (Errors.OK e1')))
    881    | Csyntax.Eunop (op0, e1) ->
    882      (match op0 with
     879   | Csyntax.Eunop (op, e1) ->
     880     (match op with
    883881      | Csyntax.Onotbool ->
    884882        (fun _ ->
     
    900898                          (translate_unop
    901899                            (Csyntax.typ_of_type (Csyntax.typeof e1))
    902                             (Csyntax.typ_of_type ty) op0)) (fun op' ->
     900                            (Csyntax.typ_of_type ty) op)) (fun op' ->
    903901                        Monad.m_bind0 (Monad.max_def Errors.res0)
    904902                          (Obj.magic (translate_expr vars e1)) (fun e1' ->
     
    916914              (Obj.magic
    917915                (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
    918                   (Csyntax.typ_of_type ty) op0)) (fun op' ->
     916                  (Csyntax.typ_of_type ty) op)) (fun op' ->
    919917              Monad.m_bind0 (Monad.max_def Errors.res0)
    920918                (Obj.magic (translate_expr vars e1)) (fun e1' ->
     
    928926              (Obj.magic
    929927                (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
    930                   (Csyntax.typ_of_type ty) op0)) (fun op' ->
     928                  (Csyntax.typ_of_type ty) op)) (fun op' ->
    931929              Monad.m_bind0 (Monad.max_def Errors.res0)
    932930                (Obj.magic (translate_expr vars e1)) (fun e1' ->
     
    934932                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
    935933                  (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __
    936    | Csyntax.Ebinop (op0, e1, e2) ->
     934   | Csyntax.Ebinop (op, e1, e2) ->
    937935     Obj.magic
    938936       (Monad.m_bind0 (Monad.max_def Errors.res0)
     
    942940           Obj.magic
    943941             (Errors.bind_eq
    944                (translate_binop op0 (Csyntax.typeof e1) (Types.pi1 e1')
     942               (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1')
    945943                 (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ ->
    946944               Errors.OK e')))))
     
    10651063        Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
    10661064          (FrontEndOps.Ointconst (sz, sg,
    1067           (AST.repr0 sz (Csyntax.sizeof ty1))))))
     1065          (AST.repr sz (Csyntax.sizeof ty1))))))
    10681066      | Csyntax.Tpointer x ->
    10691067        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
     
    11031101                  (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
    11041102                  AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
    1105                   (AST.repr0 AST.I16 off))))))))))
     1103                  (AST.repr AST.I16 off))))))))))
    11061104              | Csyntax.By_reference ->
    11071105                Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
     
    11101108                  (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
    11111109                  (FrontEndOps.Ointconst (AST.I16, AST.Signed,
    1112                   (AST.repr0 AST.I16 off))))))))
     1110                  (AST.repr AST.I16 off))))))))
    11131111              | Csyntax.By_nothing x0 ->
    11141112                Obj.magic (Errors.Error
     
    12071205                (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
    12081206                (FrontEndOps.Ointconst (AST.I16, AST.Signed,
    1209                 (AST.repr0 AST.I16 off)))))))))))
     1207                (AST.repr AST.I16 off)))))))))))
    12101208      | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
    12111209      | Csyntax.Tcomp_ptr x0 ->
     
    12231221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
    12241222| IdDest (id, ty) -> h_IdDest id ty __
    1225 | MemDest x_14489 -> h_MemDest x_14489
     1223| MemDest x_9567 -> h_MemDest x_9567
    12261224
    12271225(** val destination_rect_Type5 :
     
    12301228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
    12311229| IdDest (id, ty) -> h_IdDest id ty __
    1232 | MemDest x_14494 -> h_MemDest x_14494
     1230| MemDest x_9572 -> h_MemDest x_9572
    12331231
    12341232(** val destination_rect_Type3 :
     
    12371235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
    12381236| IdDest (id, ty) -> h_IdDest id ty __
    1239 | MemDest x_14499 -> h_MemDest x_14499
     1237| MemDest x_9577 -> h_MemDest x_9577
    12401238
    12411239(** val destination_rect_Type2 :
     
    12441242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
    12451243| IdDest (id, ty) -> h_IdDest id ty __
    1246 | MemDest x_14504 -> h_MemDest x_14504
     1244| MemDest x_9582 -> h_MemDest x_9582
    12471245
    12481246(** val destination_rect_Type1 :
     
    12511249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
    12521250| IdDest (id, ty) -> h_IdDest id ty __
    1253 | MemDest x_14509 -> h_MemDest x_14509
     1251| MemDest x_9587 -> h_MemDest x_9587
    12541252
    12551253(** val destination_rect_Type0 :
     
    12581256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
    12591257| IdDest (id, ty) -> h_IdDest id ty __
    1260 | MemDest x_14514 -> h_MemDest x_14514
     1258| MemDest x_9592 -> h_MemDest x_9592
    12611259
    12621260(** val destination_inv_rect_Type4 :
     
    13761374  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
    13771375    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
    1378     (Identifiers.lookup0 PreIdentifiers.SymbolTag lbls l)
    1379 
    1380 type fresh_list_for_univ = __
     1376    (Identifiers.lookup PreIdentifiers.SymbolTag lbls l)
    13811377
    13821378type labgen = { labuniverse : Identifiers.universe;
     
    13861382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13871383    'a1) -> labgen -> 'a1 **)
    1388 let rec labgen_rect_Type4 h_mk_labgen x_14549 =
    1389   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1390     x_14549
     1384let rec labgen_rect_Type4 h_mk_labgen x_9627 =
     1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9627
    13911386  in
    13921387  h_mk_labgen labuniverse0 label_genlist0 __
     
    13951390    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    13961391    'a1) -> labgen -> 'a1 **)
    1397 let rec labgen_rect_Type5 h_mk_labgen x_14551 =
    1398   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1399     x_14551
     1392let rec labgen_rect_Type5 h_mk_labgen x_9629 =
     1393  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9629
    14001394  in
    14011395  h_mk_labgen labuniverse0 label_genlist0 __
     
    14041398    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14051399    'a1) -> labgen -> 'a1 **)
    1406 let rec labgen_rect_Type3 h_mk_labgen x_14553 =
    1407   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1408     x_14553
     1400let rec labgen_rect_Type3 h_mk_labgen x_9631 =
     1401  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9631
    14091402  in
    14101403  h_mk_labgen labuniverse0 label_genlist0 __
     
    14131406    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14141407    'a1) -> labgen -> 'a1 **)
    1415 let rec labgen_rect_Type2 h_mk_labgen x_14555 =
    1416   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1417     x_14555
     1408let rec labgen_rect_Type2 h_mk_labgen x_9633 =
     1409  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9633
    14181410  in
    14191411  h_mk_labgen labuniverse0 label_genlist0 __
     
    14221414    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14231415    'a1) -> labgen -> 'a1 **)
    1424 let rec labgen_rect_Type1 h_mk_labgen x_14557 =
    1425   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1426     x_14557
     1416let rec labgen_rect_Type1 h_mk_labgen x_9635 =
     1417  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9635
    14271418  in
    14281419  h_mk_labgen labuniverse0 label_genlist0 __
     
    14311422    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
    14321423    'a1) -> labgen -> 'a1 **)
    1433 let rec labgen_rect_Type0 h_mk_labgen x_14559 =
    1434   let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
    1435     x_14559
     1424let rec labgen_rect_Type0 h_mk_labgen x_9637 =
     1425  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = x_9637
    14361426  in
    14371427  h_mk_labgen labuniverse0 label_genlist0 __
     
    15371527    var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
    15381528    Types.sig0 Errors.res **)
    1539 let translate_expr_sigma v e0 =
     1529let translate_expr_sigma v e =
    15401530  Obj.magic
    15411531    (Monad.m_bind0 (Monad.max_def Errors.res0)
    1542       (Obj.magic (translate_expr v e0)) (fun e' ->
     1532      (Obj.magic (translate_expr v e)) (fun e' ->
    15431533      Obj.magic (Errors.OK { Types.dpi1 =
    1544         (Csyntax.typ_of_type (Csyntax.typeof e0)); Types.dpi2 =
     1534        (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 =
    15451535        (Types.pi1 e') })))
    15461536
     
    15581548    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15591549    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1560 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14575 =
    1561   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14575 in
     1550let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_9653 =
     1551  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9653 in
    15621552  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15631553
     
    15651555    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15661556    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1567 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14577 =
    1568   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14577 in
     1557let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_9655 =
     1558  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9655 in
    15691559  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15701560
     
    15721562    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15731563    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1574 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14579 =
    1575   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14579 in
     1564let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_9657 =
     1565  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9657 in
    15761566  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15771567
     
    15791569    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15801570    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1581 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14581 =
    1582   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14581 in
     1571let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_9659 =
     1572  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9659 in
    15831573  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15841574
     
    15861576    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15871577    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1588 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14583 =
    1589   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14583 in
     1578let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_9661 =
     1579  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9661 in
    15901580  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15911581
     
    15931583    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
    15941584    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
    1595 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14585 =
    1596   let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14585 in
     1585let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_9663 =
     1586  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_9663 in
    15971587  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
    15981588
     
    16501640(** val alloc_tmp :
    16511641    var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **)
    1652 let alloc_tmp vars ty g0 =
     1642let alloc_tmp vars ty g =
    16531643  (let { Types.fst = tmp; Types.snd = u } =
    1654      Identifiers.fresh PreIdentifiers.SymbolTag g0.tmp_universe
     1644     Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe
    16551645   in
    16561646  (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
    1657   (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g0.tmp_env)) } })) __
     1647  (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __
    16581648
    16591649(** val mklabels :
     
    16781668let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
    16791669| DoNotConvert -> h_DoNotConvert
    1680 | ConvertTo (x_14607, x_14606) -> h_ConvertTo x_14607 x_14606
     1670| ConvertTo (x_9685, x_9684) -> h_ConvertTo x_9685 x_9684
    16811671
    16821672(** val convert_flag_rect_Type5 :
     
    16851675let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
    16861676| DoNotConvert -> h_DoNotConvert
    1687 | ConvertTo (x_14612, x_14611) -> h_ConvertTo x_14612 x_14611
     1677| ConvertTo (x_9690, x_9689) -> h_ConvertTo x_9690 x_9689
    16881678
    16891679(** val convert_flag_rect_Type3 :
     
    16921682let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
    16931683| DoNotConvert -> h_DoNotConvert
    1694 | ConvertTo (x_14617, x_14616) -> h_ConvertTo x_14617 x_14616
     1684| ConvertTo (x_9695, x_9694) -> h_ConvertTo x_9695 x_9694
    16951685
    16961686(** val convert_flag_rect_Type2 :
     
    16991689let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
    17001690| DoNotConvert -> h_DoNotConvert
    1701 | ConvertTo (x_14622, x_14621) -> h_ConvertTo x_14622 x_14621
     1691| ConvertTo (x_9700, x_9699) -> h_ConvertTo x_9700 x_9699
    17021692
    17031693(** val convert_flag_rect_Type1 :
     
    17061696let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
    17071697| DoNotConvert -> h_DoNotConvert
    1708 | ConvertTo (x_14627, x_14626) -> h_ConvertTo x_14627 x_14626
     1698| ConvertTo (x_9705, x_9704) -> h_ConvertTo x_9705 x_9704
    17091699
    17101700(** val convert_flag_rect_Type0 :
     
    17131703let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
    17141704| DoNotConvert -> h_DoNotConvert
    1715 | ConvertTo (x_14632, x_14631) -> h_ConvertTo x_14632 x_14631
     1705| ConvertTo (x_9710, x_9709) -> h_ConvertTo x_9710 x_9709
    17161706
    17171707(** val convert_flag_inv_rect_Type4 :
     
    20312021    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
    20322022    Types.prod Types.sig0 Errors.res **)
    2033 let alloc_params vars lbls statement0 uv ul rettyp params s =
     2023let alloc_params vars lbls statement uv ul rettyp params s =
    20342024  Util.foldl (fun su it ->
    20352025    let { Types.fst = id; Types.snd = ty } = it in
    20362026    Obj.magic
    20372027      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
    2038         (fun eta2887 ->
    2039         let result = eta2887 in
     2028        (fun eta1212 ->
     2029        let result = eta1212 in
    20402030        (let { Types.fst = fgens1; Types.snd = s0 } = result in
    20412031        (fun _ ->
     
    21602150  (match l with
    21612151   | List.Nil -> (fun _ -> Errors.OK List.Nil)
    2162    | List.Cons (hd0, tl) ->
     2152   | List.Cons (hd, tl) ->
    21632153     (fun _ ->
    21642154       Obj.magic
    2165          (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd0 __)
     2155         (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __)
    21662156           (fun b_hd ->
    21672157           Monad.m_bind0 (Monad.max_def Errors.res0)
Note: See TracChangeset for help on using the changeset viewer.