Skip to content

Commit

Permalink
Remove useless errors (#1261)
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 authored Oct 22, 2024
1 parent 7ee9629 commit 35c0f14
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 35c0f14

Please sign in to comment.