Changeset 2649 for extracted/errors.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (8 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/errors.ml

    r2601 r2649  
    2121open Positive
    2222
    23 open Char
    24 
    25 open String
    26 
    2723open PreIdentifiers
    2824
     
    3733open Option
    3834
     35open ErrorMessages
     36
    3937type errcode =
    40 | MSG of String.string
    41 | CTX of String.string * PreIdentifiers.identifier
     38| MSG of ErrorMessages.errorMessage
     39| CTX of PreIdentifiers.identifierTag * PreIdentifiers.identifier
    4240
    4341(** val errcode_rect_Type4 :
    44     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    45     'a1) -> errcode -> 'a1 **)
     42    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     43    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    4644let rec errcode_rect_Type4 h_MSG h_CTX = function
    47 | MSG x_1982 -> h_MSG x_1982
    48 | CTX (tag, x_1983) -> h_CTX tag x_1983
     45| MSG x_969 -> h_MSG x_969
     46| CTX (tag, x_970) -> h_CTX tag x_970
    4947
    5048(** val errcode_rect_Type5 :
    51     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    52     'a1) -> errcode -> 'a1 **)
     49    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     50    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    5351let rec errcode_rect_Type5 h_MSG h_CTX = function
    54 | MSG x_1987 -> h_MSG x_1987
    55 | CTX (tag, x_1988) -> h_CTX tag x_1988
     52| MSG x_974 -> h_MSG x_974
     53| CTX (tag, x_975) -> h_CTX tag x_975
    5654
    5755(** val errcode_rect_Type3 :
    58     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    59     'a1) -> errcode -> 'a1 **)
     56    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     57    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    6058let rec errcode_rect_Type3 h_MSG h_CTX = function
    61 | MSG x_1992 -> h_MSG x_1992
    62 | CTX (tag, x_1993) -> h_CTX tag x_1993
     59| MSG x_979 -> h_MSG x_979
     60| CTX (tag, x_980) -> h_CTX tag x_980
    6361
    6462(** val errcode_rect_Type2 :
    65     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    66     'a1) -> errcode -> 'a1 **)
     63    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     64    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    6765let rec errcode_rect_Type2 h_MSG h_CTX = function
    68 | MSG x_1997 -> h_MSG x_1997
    69 | CTX (tag, x_1998) -> h_CTX tag x_1998
     66| MSG x_984 -> h_MSG x_984
     67| CTX (tag, x_985) -> h_CTX tag x_985
    7068
    7169(** val errcode_rect_Type1 :
    72     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    73     'a1) -> errcode -> 'a1 **)
     70    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     71    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    7472let rec errcode_rect_Type1 h_MSG h_CTX = function
    75 | MSG x_2002 -> h_MSG x_2002
    76 | CTX (tag, x_2003) -> h_CTX tag x_2003
     73| MSG x_989 -> h_MSG x_989
     74| CTX (tag, x_990) -> h_CTX tag x_990
    7775
    7876(** val errcode_rect_Type0 :
    79     (String.string -> 'a1) -> (String.string -> PreIdentifiers.identifier ->
    80     'a1) -> errcode -> 'a1 **)
     77    (ErrorMessages.errorMessage -> 'a1) -> (PreIdentifiers.identifierTag ->
     78    PreIdentifiers.identifier -> 'a1) -> errcode -> 'a1 **)
    8179let rec errcode_rect_Type0 h_MSG h_CTX = function
    82 | MSG x_2007 -> h_MSG x_2007
    83 | CTX (tag, x_2008) -> h_CTX tag x_2008
     80| MSG x_994 -> h_MSG x_994
     81| CTX (tag, x_995) -> h_CTX tag x_995
    8482
    8583(** val errcode_inv_rect_Type4 :
    86     errcode -> (String.string -> __ -> 'a1) -> (String.string ->
    87     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
     84    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
     85    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
     86    -> 'a1 **)
    8887let errcode_inv_rect_Type4 hterm h1 h2 =
    8988  let hcut = errcode_rect_Type4 h1 h2 hterm in hcut __
    9089
    9190(** val errcode_inv_rect_Type3 :
    92     errcode -> (String.string -> __ -> 'a1) -> (String.string ->
    93     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
     91    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
     92    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
     93    -> 'a1 **)
    9494let errcode_inv_rect_Type3 hterm h1 h2 =
    9595  let hcut = errcode_rect_Type3 h1 h2 hterm in hcut __
    9696
    9797(** val errcode_inv_rect_Type2 :
    98     errcode -> (String.string -> __ -> 'a1) -> (String.string ->
    99     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
     98    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
     99    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
     100    -> 'a1 **)
    100101let errcode_inv_rect_Type2 hterm h1 h2 =
    101102  let hcut = errcode_rect_Type2 h1 h2 hterm in hcut __
    102103
    103104(** val errcode_inv_rect_Type1 :
    104     errcode -> (String.string -> __ -> 'a1) -> (String.string ->
    105     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
     105    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
     106    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
     107    -> 'a1 **)
    106108let errcode_inv_rect_Type1 hterm h1 h2 =
    107109  let hcut = errcode_rect_Type1 h1 h2 hterm in hcut __
    108110
    109111(** val errcode_inv_rect_Type0 :
    110     errcode -> (String.string -> __ -> 'a1) -> (String.string ->
    111     PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
     112    errcode -> (ErrorMessages.errorMessage -> __ -> 'a1) ->
     113    (PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> __ -> 'a1)
     114    -> 'a1 **)
    112115let errcode_inv_rect_Type0 hterm h1 h2 =
    113116  let hcut = errcode_rect_Type0 h1 h2 hterm in hcut __
     
    129132type errmsg = errcode List.list
    130133
    131 (** val msg : String.string -> errmsg **)
     134(** val msg : ErrorMessages.errorMessage -> errmsg **)
    132135let msg s =
    133136  List.Cons ((MSG s), List.Nil)
     
    140143    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    141144let rec res_rect_Type4 h_OK h_Error = function
    142 | OK x_2047 -> h_OK x_2047
    143 | Error x_2048 -> h_Error x_2048
     145| OK x_1034 -> h_OK x_1034
     146| Error x_1035 -> h_Error x_1035
    144147
    145148(** val res_rect_Type5 :
    146149    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    147150let rec res_rect_Type5 h_OK h_Error = function
    148 | OK x_2052 -> h_OK x_2052
    149 | Error x_2053 -> h_Error x_2053
     151| OK x_1039 -> h_OK x_1039
     152| Error x_1040 -> h_Error x_1040
    150153
    151154(** val res_rect_Type3 :
    152155    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    153156let rec res_rect_Type3 h_OK h_Error = function
    154 | OK x_2057 -> h_OK x_2057
    155 | Error x_2058 -> h_Error x_2058
     157| OK x_1044 -> h_OK x_1044
     158| Error x_1045 -> h_Error x_1045
    156159
    157160(** val res_rect_Type2 :
    158161    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    159162let rec res_rect_Type2 h_OK h_Error = function
    160 | OK x_2062 -> h_OK x_2062
    161 | Error x_2063 -> h_Error x_2063
     163| OK x_1049 -> h_OK x_1049
     164| Error x_1050 -> h_Error x_1050
    162165
    163166(** val res_rect_Type1 :
    164167    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    165168let rec res_rect_Type1 h_OK h_Error = function
    166 | OK x_2067 -> h_OK x_2067
    167 | Error x_2068 -> h_Error x_2068
     169| OK x_1054 -> h_OK x_1054
     170| Error x_1055 -> h_Error x_1055
    168171
    169172(** val res_rect_Type0 :
    170173    ('a1 -> 'a2) -> (errmsg -> 'a2) -> 'a1 res -> 'a2 **)
    171174let rec res_rect_Type0 h_OK h_Error = function
    172 | OK x_2072 -> h_OK x_2072
    173 | Error x_2073 -> h_Error x_2073
     175| OK x_1059 -> h_OK x_1059
     176| Error x_1060 -> h_Error x_1060
    174177
    175178(** val res_inv_rect_Type4 :
     
    233236  mfold_left_i_aux f x Nat.O
    234237
    235 (** val wrongLength : String.string **)
    236 let wrongLength = "wrong length"
    237   (*failwith "AXIOM TO BE REALIZED"*)
    238 
    239238(** val mfold_left2 :
    240239    ('a1 -> 'a2 -> 'a3 -> 'a1 res) -> 'a1 res -> 'a2 List.list -> 'a3
     
    245244    (match right with
    246245     | List.Nil -> accu
    247      | List.Cons (hd0, tl) -> Error (msg wrongLength))
     246     | List.Cons (hd0, tl) -> Error (msg ErrorMessages.WrongLength))
    248247  | List.Cons (hd0, tl) ->
    249248    (match right with
    250      | List.Nil -> Error (msg wrongLength)
     249     | List.Nil -> Error (msg ErrorMessages.WrongLength)
    251250     | List.Cons (hd', tl') ->
    252251       Obj.magic
Note: See TracChangeset for help on using the changeset viewer.