Skip to content

Commit

Permalink
Remove useless errors
Browse files Browse the repository at this point in the history 
Most of these errors were used by the legacy typechecker and are not
relevant anymore.
  • Loading branch information
@Halbaroth
Halbaroth committed Oct 22, 2024
1 parent 7ee9629 commit e2db0bb
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 211 deletions.
164 changes: 0 additions & 164 deletions src/lib/structures/errors.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,53 +28,9 @@
open Format

type typing_error =
| BitvExtract of int*int
| BitvExtractRange of int*int
| NonPositiveBitvType of int
| ClashType of string
| ClashLabel of string * string
| ClashParam of string
| TypeDuplicateVar of string
| UnboundedVar of string
| UnknownType of string
| WrongArity of string * int
| SymbAlreadyDefined of string
| SymbUndefined of string
| NotAPropVar of string
| NotAPredicate of string
| Unification of Ty.t * Ty.t
| ShouldBeApply of string
| WrongNumberofArgs of string
| ShouldHaveType of Ty.t * Ty.t
| ShouldHaveTypeIntorReal of Ty.t
| ShouldHaveTypeInt of Ty.t
| ShouldHaveTypeBitv of Ty.t
| ArrayIndexShouldHaveTypeInt
| ShouldHaveTypeArray
| ShouldHaveTypeRecord of Ty.t
| ShouldBeARecord
| ShouldHaveLabel of string * string
| NoLabelInType of Hstring.t * Ty.t
| ShouldHaveTypeProp
| NoRecordType of Hstring.t
| DuplicateLabel of Hstring.t
| DuplicatePattern of string
| WrongLabel of Hstring.t * Ty.t
| WrongNumberOfLabels
| Notrigger
| CannotGeneralize
| SyntaxError
| ThExtError of string
| ThSemTriggerError
| WrongDeclInTheory
| ShouldBeADT of Ty.t
| MatchNotExhaustive of Hstring.t list
| MatchUnusedCases of Hstring.t list
| NotAdtConstr of string * Ty.t
| BadPopCommand of {pushed : int; to_pop : int}
| ShouldBePositive of int
| PolymorphicEnum of string
| ShouldBeIntLiteral of string

type run_error =
| Invalid_steps_count of int
Expand All @@ -92,9 +48,6 @@ type model_error =
| Subst_not_model_term of Expr.t

type error =
| Parser_error of string
| Lexical_error of Loc.t * string
| Syntax_error of Loc.t * string
| Typing_error of Loc.t * typing_error
| Run_error of run_error
| Warning_as_error
Expand Down Expand Up @@ -123,121 +76,12 @@ let forbidden_command mode cmd_name =
error (Mode_error (mode, Forbidden_command cmd_name))

let report_typing_error fmt = function
| BitvExtract(i,j) ->
fprintf fmt "bitvector extraction malformed (%d>%d)" i j
| BitvExtractRange(n,j) ->
fprintf fmt "extraction out of range (%d>%d)" j n
| NonPositiveBitvType(n) ->
fprintf fmt "non positive bitvector size (%d)" n
| ClashType s ->
fprintf fmt "the type %s is already defined" s
| ClashParam s ->
fprintf fmt "parameter %s is bound twice" s
| ClashLabel (s,t) ->
fprintf fmt "the label %s already appears in type %s" s t
| CannotGeneralize ->
fprintf fmt "cannot generalize the type of this expression"
| TypeDuplicateVar s ->
fprintf fmt "duplicate type variable %s" s
| UnboundedVar s ->
fprintf fmt "unbounded variable %s" s
| UnknownType s ->
fprintf fmt "unknown type %s" s
| WrongArity(s,n) ->
fprintf fmt "the type %s has %d arguments" s n
| SymbAlreadyDefined s ->
fprintf fmt "the symbol %s is already defined" s
| SymbUndefined s ->
fprintf fmt "undefined symbol %s" s
| NotAPropVar s ->
fprintf fmt "%s is not a propositional variable" s
| NotAPredicate s ->
fprintf fmt "%s is not a predicate" s
| Unification(t1,t2) ->
fprintf fmt "%a and %a cannot be unified" Ty.print t1 Ty.print t2
| ShouldBeApply s ->
fprintf fmt "%s is a function symbol, it should be applied" s
| WrongNumberofArgs s ->
fprintf fmt "Wrong number of arguments when applying %s" s
| ShouldHaveType(ty1,ty2) ->
fprintf fmt "this expression has type %a but is here used with type %a"
Ty.print ty1 Ty.print ty2
| ShouldHaveTypeBitv t ->
fprintf fmt "this expression has type %a but it should be a bitvector"
Ty.print t
| ShouldHaveTypeIntorReal t ->
fprintf fmt
"this expression has type %a but it should have type int or real"
Ty.print t
| ShouldHaveTypeInt t ->
fprintf fmt
"this expression has type %a but it should have type int"
Ty.print t
| ShouldHaveTypeArray ->
fprintf fmt "this expression should have type farray"
| ShouldHaveTypeRecord t ->
fprintf fmt "this expression has type %a but it should have a record type"
Ty.print t
| ShouldBeARecord ->
fprintf fmt "this expression should have a record type"
| ShouldHaveLabel (s, a) ->
fprintf fmt "this expression has type %s which has no label %s" s a
| NoLabelInType (lb, ty) ->
fprintf fmt "no label %s in type %a" (Hstring.view lb) Ty.print ty
| ShouldHaveTypeProp ->
fprintf fmt "this expression should have type prop"
| NoRecordType s ->
fprintf fmt "no record type has label %s" (Hstring.view s)
| DuplicateLabel s ->
fprintf fmt "label %s is defined several times" (Hstring.view s)
| DuplicatePattern s ->
fprintf fmt "pattern %s is bound several times" s
| WrongLabel (s, ty) ->
fprintf fmt "wrong label %s in type %a" (Hstring.view s) Ty.print ty
| WrongNumberOfLabels ->
fprintf fmt "wrong number of labels"
| ArrayIndexShouldHaveTypeInt ->
fprintf fmt "index of arrays should hava type int"
| Notrigger ->
fprintf fmt "No trigger for this lemma"
| SyntaxError ->
fprintf fmt "syntax error"
| ThExtError s ->
fprintf fmt "Theory extension %S not recognized" s
| ThSemTriggerError ->
fprintf fmt "Semantic triggers are only allowed inside Theories"
| WrongDeclInTheory ->
fprintf fmt
"Currently, this kind of declarations are not allowed inside theories"
| ShouldBeADT ty ->
fprintf fmt "%a is not an algebraic, a record or an enumeration datatype"
Ty.print ty
| MatchNotExhaustive missing ->
fprintf fmt
"Pattern-matching is not exhaustive. These cases are missing: %a"
(Util.print_list ~sep:" |" ~pp:Hstring.print) missing
| MatchUnusedCases dead ->
fprintf fmt
"Pattern-matching contains unreachable cases. These cases are\
removed: %a"
(Util.print_list ~sep:" |" ~pp:Hstring.print) dead
| NotAdtConstr (lbl, ty) ->
fprintf fmt
"The identifiant %s is not a constructor of an algebraic data type. \
Its type is %a" lbl Ty.print ty
| BadPopCommand {pushed; to_pop} ->
fprintf fmt
"Cannot pop %d assertion contexts. Only %d have been pushed"
to_pop pushed
| ShouldBePositive n ->
fprintf fmt
"This integer : %d should be positive" n
| PolymorphicEnum n ->
fprintf fmt
"Polymorphic enum definition for %s is not supported" n
| ShouldBeIntLiteral s ->
fprintf fmt
"This expression : %s should be an integer constant" s

let report_run_error fmt = function
| Invalid_steps_count i ->
Expand Down Expand Up @@ -270,14 +114,6 @@ let report_model_error ppf = function
Fmt.pf ppf "The expression %a is not a model term" Expr.print e

let report fmt = function
| Parser_error s ->
Format.fprintf fmt "Parser Error: %s" s;
| Lexical_error (l,s) ->
Loc.report fmt l;
Format.fprintf fmt "Lexical Error: %s" s;
| Syntax_error (l,s) ->
Loc.report fmt l;
Format.fprintf fmt "Syntax Error: %s" s;
| Typing_error (l,e) ->
Loc.report fmt l;
Format.fprintf fmt "Typing Error: ";
Expand Down
47 changes: 0 additions & 47 deletions src/lib/structures/errors.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,53 +34,9 @@

(** Error that can be raised by the typechecker *)
type typing_error =
| BitvExtract of int*int
| BitvExtractRange of int*int
| NonPositiveBitvType of int
| ClashType of string
| ClashLabel of string * string
| ClashParam of string
| TypeDuplicateVar of string
| UnboundedVar of string
| UnknownType of string
| WrongArity of string * int
| SymbAlreadyDefined of string
| SymbUndefined of string
| NotAPropVar of string
| NotAPredicate of string
| Unification of Ty.t * Ty.t
| ShouldBeApply of string
| WrongNumberofArgs of string
| ShouldHaveType of Ty.t * Ty.t
| ShouldHaveTypeIntorReal of Ty.t
| ShouldHaveTypeInt of Ty.t
| ShouldHaveTypeBitv of Ty.t
| ArrayIndexShouldHaveTypeInt
| ShouldHaveTypeArray
| ShouldHaveTypeRecord of Ty.t
| ShouldBeARecord
| ShouldHaveLabel of string * string
| NoLabelInType of Hstring.t * Ty.t
| ShouldHaveTypeProp
| NoRecordType of Hstring.t
| DuplicateLabel of Hstring.t
| DuplicatePattern of string
| WrongLabel of Hstring.t * Ty.t
| WrongNumberOfLabels
| Notrigger
| CannotGeneralize
| SyntaxError
| ThExtError of string
| ThSemTriggerError
| WrongDeclInTheory
| ShouldBeADT of Ty.t
| MatchNotExhaustive of Hstring.t list
| MatchUnusedCases of Hstring.t list
| NotAdtConstr of string * Ty.t
| BadPopCommand of {pushed : int; to_pop : int}
| ShouldBePositive of int
| PolymorphicEnum of string
| ShouldBeIntLiteral of string

(** Errors that can be raised at solving*)
type run_error =
Expand All @@ -102,9 +58,6 @@ type model_error =

(** All types of error that can be raised *)
type error =
| Parser_error of string (** Error used at parser loading *)
| Lexical_error of Loc.t * string (** Error used by the lexer *)
| Syntax_error of Loc.t * string (** Error used by the parser*)
| Typing_error of Loc.t * typing_error (** Error used at typing *)
| Run_error of run_error (** Error used during solving *)
| Warning_as_error
Expand Down

0 comments on commit e2db0bb

Please sign in to comment.