dtlc

dependently-typed lambda calculus toy
git clone git://git.rr3.xyz/dtlc
Log | Files | Refs | README | LICENSE

error.ml (3491B)

      1 module F = Format
      2 open Node
      3 module I = Internal
      4 module P = Pretty
      5 
      6 type error = error' node
      7 and error' =
      8 | LexerNameIndexTooBig
      9 | LexerInvalidNumberTerminator
     10 | LexerNoRule
     11 
     12 | ParserInvalidTerm
     13 | ParserInvalidPatt
     14 | ParserEmptyDomain
     15 | ParserNoRule
     16 
     17 | DesugarDuplicateTag of Name.Tag.t
     18 | DesugarDataAndData
     19 
     20 | ElabApplyNonFunction of I.term
     21 | ElabNonInferablePatt
     22 | ElabUnifyFail of I.term * I.term
     23 | ElabUnexpectedTag of Name.Tag.t
     24 | ElabNoLetAnnot of error
     25 | ElabBinderCycle of Name.Var.t list
     26 | ElabUnannotImplicitIsType of error
     27 | ElabNoBinderAnnot of error
     28 | ElabDuplicateName of Name.Var.t
     29 | ElabArityMismatch
     30 | ElabCantInferData
     31 | ElabDataPattRefutable
     32 | ElabUnboundVar of Name.Var.t * int
     33 | ElabFnArityMismatch
     34 | ElabFnPlicityMismatch
     35 | ElabNonExhaustiveMatch
     36 | ElabRedundantCase
     37 | ElabCantInferMatch
     38 | ElabExpectedFnType of I.term
     39 | ElabExpectedDataType of I.term
     40 
     41 let rec pp_print ppf {loc; data = e} =
     42 	F.fprintf ppf "@[<v>[%a] %a@]"
     43 		Loc.pp_print loc
     44 		pp_print' e
     45 
     46 and pp_print' ppf = function
     47 | LexerNameIndexTooBig ->
     48 	F.pp_print_string ppf "name index too big"
     49 | LexerInvalidNumberTerminator ->
     50 	F.pp_print_string ppf "invalid character after number literal"
     51 | LexerNoRule ->
     52 	F.pp_print_string ppf "lexical error"
     53 
     54 | ParserInvalidTerm ->
     55 	F.pp_print_string ppf "invalid term"
     56 | ParserInvalidPatt ->
     57 	F.pp_print_string ppf "invalid pattern"
     58 | ParserEmptyDomain ->
     59 	F.pp_print_string ppf "empty domain"
     60 | ParserNoRule ->
     61 	F.pp_print_string ppf "syntax error"
     62 
     63 | DesugarDuplicateTag tag ->
     64 	F.fprintf ppf "%s: %a"
     65 		"duplicate constructor: "
     66 		Name.Tag.pp_print tag
     67 | DesugarDataAndData ->
     68 	F.pp_print_string ppf "conjunction of two data patterns"
     69 
     70 | ElabApplyNonFunction typ ->
     71 	F.fprintf ppf "@[<4>%s@ %a@]"
     72 		"attempt to apply non-function of inferred type"
     73 		(Pretty.pp_print_term 0) typ
     74 | ElabNonInferablePatt ->
     75 	F.pp_print_string ppf "non-inferable pattern"
     76 | ElabUnifyFail (expected, inferred) ->
     77 	F.fprintf ppf
     78 		"\
     79 			expected type@;<0 4>\
     80 				%a@,\
     81 			does not unify with inferred type@;<0 4>\
     82 				%a@,\
     83 		"
     84 		(P.pp_print_term 0) expected
     85 		(P.pp_print_term 0) inferred
     86 
     87 (* TODO *)
     88 | ElabCantInferData           -> F.pp_print_string ppf "ErrCantInferData"
     89 | ElabNoLetAnnot _            -> F.pp_print_string ppf "ErrNoLetAnnot"
     90 | ElabNoBinderAnnot _         -> F.pp_print_string ppf "ErrNoBinderAnnot"
     91 | ElabUnannotImplicitIsType _ -> F.pp_print_string ppf "ErrUnannotImplicitIsType"
     92 | ElabDataPattRefutable       -> F.pp_print_string ppf "ErrDataPattRefutable"
     93 | ElabBinderCycle _           -> F.pp_print_string ppf "ErrBinderCycle"
     94 | ElabArityMismatch           -> F.pp_print_string ppf "ErrArityMismatch"
     95 | ElabUnboundVar _            -> F.pp_print_string ppf "ErrUnboundVar"
     96 | ElabFnArityMismatch         -> F.pp_print_string ppf "ErrFnArityMismatch"
     97 | ElabFnPlicityMismatch       -> F.pp_print_string ppf "ErrFnPlicityMismatch"
     98 | ElabUnexpectedTag _         -> F.pp_print_string ppf "ErrUnexpectedTag"
     99 | ElabDuplicateName _         -> F.pp_print_string ppf "ErrDuplicateName"
    100 | ElabNonExhaustiveMatch      -> F.pp_print_string ppf "ElabNonExhaustiveMatch" 
    101 | ElabRedundantCase           -> F.pp_print_string ppf "ElabRedundantCase"
    102 | ElabCantInferMatch          -> F.pp_print_string ppf "ElabCantInferMatch"
    103 | ElabExpectedFnType _        -> F.pp_print_string ppf "ErrExpectedFnType"
    104 | ElabExpectedDataType _      -> F.pp_print_string ppf "ErrExpectedDataType"
    105 
    106 exception Exn of error
    107 
    108 let abort
    109 : 'a. Loc.t -> error' -> 'a
    110 = fun loc e -> raise (Exn (loc @$ e))