summaryrefslogtreecommitdiff
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml294
1 files changed, 153 insertions, 141 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index beb80d03..3fe51b5a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: himsg.ml,v 1.86.2.4 2004/12/03 18:45:53 herbelin Exp $ *)
+(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *)
open Pp
open Util
@@ -21,18 +21,20 @@ open Sign
open Environ
open Pretype_errors
open Type_errors
+open Indrec
open Reduction
open Cases
open Logic
open Printer
-open Ast
open Rawterm
+open Evd
-let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"")
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
-let prterm c = quote (prterm c)
-let prterm_env e c = quote (prterm_env e c)
-let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t)
+let pr_lconstr c = quote (pr_lconstr c)
+let pr_lconstr_env e c = quote (pr_lconstr_env e c)
+let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
+let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
let nth i =
let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
@@ -56,20 +58,20 @@ let explain_unbound_var ctx v =
let explain_not_type ctx j =
let pe = pr_ne_context_of (str"In environment") ctx in
- let pc,pt = prjudge_env ctx j in
+ let pc,pt = pr_ljudge_env ctx j in
pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
str"has type" ++ spc () ++ pt ++ spc () ++
str"which should be Set, Prop or Type."
let explain_bad_assumption ctx j =
let pe = pr_ne_context_of (str"In environment") ctx in
- let pc,pt = prjudge_env ctx j in
+ let pc,pt = pr_ljudge_env ctx j in
pe ++ str "cannot declare a variable or hypothesis over the term" ++
brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++
str "because this term is not a type."
let explain_reference_variables c =
- let pc = prterm c in
+ let pc = pr_lconstr c in
str "the constant" ++ spc () ++ pc ++ spc () ++
str "refers to variables which are not in the context"
@@ -82,12 +84,11 @@ let rec pr_disjunction pr = function
let explain_elim_arity ctx ind aritylst c pj okinds =
let ctx = make_all_name_different ctx in
let pi = pr_inductive ctx ind in
- let pc = prterm_env ctx c in
- let ppt = prterm_env ctx pj.uj_type in
+ let pc = pr_lconstr_env ctx c in
let msg = match okinds with
| Some(kp,ki,explanation) ->
- let pki = prterm_env ctx ki in
- let pkp = prterm_env ctx kp in
+ let pki = pr_lconstr_env ctx ki in
+ let pkp = pr_lconstr_env ctx kp in
let explanation = match explanation with
| NonInformativeToInformative ->
"proofs can be eliminated only to build proofs"
@@ -106,29 +107,19 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
hov 0 (
str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
str "in the inductive type " ++ spc() ++ quote pi ++
- (if !Options.v7 then
- let pp = prterm_env ctx pj.uj_val in
- let ppar = pr_disjunction (prterm_env ctx) aritylst in
- let ppt = prterm_env ctx pj.uj_type in
- fnl () ++
- str "The elimination predicate" ++ brk(1,1) ++ pp ++ spc () ++
- str "has arity" ++ brk(1,1) ++ ppt ++ fnl () ++
- str "It should be " ++ brk(1,1) ++ ppar
- else
- let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
+ (let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
(list_uniquize (List.map (fun ar ->
family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in
- let ppar = pr_disjunction (prterm_env ctx) sorts in
- let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in
+ let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in
+ let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in
str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++
spc () ++ str "while it should be " ++ ppar))
++ fnl () ++ msg
-
-
+
let explain_case_not_inductive ctx cj =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx cj.uj_val in
- let pct = prterm_env ctx cj.uj_type in
+ let pc = pr_lconstr_env ctx cj.uj_val in
+ let pct = pr_lconstr_env ctx cj.uj_type in
match kind_of_term cj.uj_type with
| Evar _ ->
str "Cannot infer a type for this expression"
@@ -139,26 +130,30 @@ let explain_case_not_inductive ctx cj =
let explain_number_branches ctx cj expn =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx cj.uj_val in
- let pct = prterm_env ctx cj.uj_type in
+ let pc = pr_lconstr_env ctx cj.uj_val in
+ let pct = pr_lconstr_env ctx cj.uj_type in
str "Matching on term" ++ brk(1,1) ++ pc ++ spc () ++
str "of type" ++ brk(1,1) ++ pct ++ spc () ++
str "expects " ++ int expn ++ str " branches"
+let ordinal n =
+ let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+ string_of_int n ^ s
+
let explain_ill_formed_branch ctx c i actty expty =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx c in
- let pa = prterm_env ctx actty in
- let pe = prterm_env ctx expty in
+ let pc = pr_lconstr_env ctx c in
+ let pa = pr_lconstr_env ctx actty in
+ let pe = pr_lconstr_env ctx expty in
str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
- spc () ++ str "the branch " ++ int (i+1) ++
- str " has type" ++ brk(1,1) ++ pa ++ spc () ++
+ spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++
+ brk(1,1) ++ pa ++ spc () ++
str "which should be" ++ brk(1,1) ++ pe
let explain_generalization ctx (name,var) j =
let pe = pr_ne_context_of (str "In environment") ctx in
- let pv = prtype_env ctx var in
- let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
+ let pv = pr_ltype_env ctx var in
+ let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in
str"Illegal generalization: " ++ pe ++
str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++
@@ -167,17 +162,18 @@ let explain_generalization ctx (name,var) j =
let explain_actual_type ctx j pt =
let pe = pr_ne_context_of (str "In environment") ctx in
- let (pc,pct) = prjudge_env ctx j in
- let pt = prterm_env ctx pt in
+ let (pc,pct) = pr_ljudge_env ctx j in
+ let pt = pr_lconstr_env ctx pt in
pe ++
str "The term" ++ brk(1,1) ++ pc ++ spc () ++
str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
str "while it is expected to have type" ++ brk(1,1) ++ pt
let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
+ let ctx = make_all_name_different ctx in
let randl = Array.to_list randl in
(* let pe = pr_ne_context_of (str"in environment") ctx in*)
- let pr,prt = prjudge_env ctx rator in
+ let pr,prt = pr_ljudge_env ctx rator in
let term_string1,term_string2 =
if List.length randl > 1 then
str "terms", (str"The "++nth n++str" term")
@@ -185,7 +181,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
str "term", str "This term" in
let appl = prlist_with_sep pr_fnl
(fun c ->
- let pc,pct = prjudge_env ctx c in
+ let pc,pct = pr_ljudge_env ctx c in
hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
@@ -193,19 +189,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
str"of type" ++ brk(1,1) ++ prt ++ spc () ++
str"cannot be applied to the " ++ term_string1 ++ fnl () ++
str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++
- brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++
- str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
+ brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++
+ str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp
let explain_cant_apply_not_functional ctx rator randl =
+ let ctx = make_all_name_different ctx in
let randl = Array.to_list randl in
(* let pe = pr_ne_context_of (str"in environment") ctx in*)
- let pr = prterm_env ctx rator.uj_val in
- let prt = prterm_env ctx rator.uj_type in
+ let pr = pr_lconstr_env ctx rator.uj_val in
+ let prt = pr_lconstr_env ctx rator.uj_type in
let term_string = if List.length randl > 1 then "terms" else "term" in
let appl = prlist_with_sep pr_fnl
(fun c ->
- let pc = prterm_env ctx c.uj_val in
- let pct = prterm_env ctx c.uj_type in
+ let pc = pr_lconstr_env ctx c.uj_val in
+ let pct = pr_lconstr_env ctx c.uj_type in
hov 2 (pc ++ spc () ++ str": " ++ pct)) randl
in
str"Illegal application (Non-functional construction): " ++
@@ -216,14 +213,14 @@ let explain_cant_apply_not_functional ctx rator randl =
str" " ++ v 0 appl
let explain_unexpected_type ctx actual_type expected_type =
- let pract = prterm_env ctx actual_type in
- let prexp = prterm_env ctx expected_type in
+ let pract = pr_lconstr_env ctx actual_type in
+ let prexp = pr_lconstr_env ctx expected_type in
str"This type is" ++ spc () ++ pract ++ spc () ++
str "but is expected to be" ++
spc () ++ prexp
let explain_not_product ctx c =
- let pr = prterm_env ctx c in
+ let pr = pr_lconstr_env ctx c in
str"The type of this term is a product," ++ spc () ++
str"but it is casted with type" ++
brk(1,1) ++ pr
@@ -241,8 +238,9 @@ let explain_ill_formed_rec_body ctx err names i =
(* Fixpoint guard errors *)
| NotEnoughAbstractionInFixBody ->
str "Not enough abstractions in the definition"
- | RecursionNotOnInductiveType ->
- str "Recursive definition on a non inductive type"
+ | RecursionNotOnInductiveType c ->
+ str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++
+ str "which should be an inductive type"
| RecursionOnIllegalTerm(j,arg,le,lt) ->
let called =
match names.(j) with
@@ -262,7 +260,7 @@ let explain_ill_formed_rec_body ctx err names i =
prlist_with_sep pr_spc (pr_db ctx) lt in
str "Recursive call to " ++ called ++ spc() ++
str "has principal argument equal to" ++ spc() ++
- prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars
+ pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars
| NotEnoughArgumentsForFixCall j ->
let called =
@@ -273,31 +271,31 @@ let explain_ill_formed_rec_body ctx err names i =
(* CoFixpoint guard errors *)
| CodomainNotInductiveType c ->
- str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++
+ str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++
str "which should be a coinductive type"
| NestedRecursiveOccurrences ->
str "nested recursive occurrences"
| UnguardedRecursiveCall c ->
- str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c
+ str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c
| RecCallInTypeOfAbstraction c ->
str "recursive call forbidden in the domain of an abstraction:" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInNonRecArgOfConstructor c ->
str "recursive call on a non-recursive argument of constructor" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInTypeOfDef c ->
str "recursive call forbidden in the type of a recursive definition" ++
- spc() ++ prterm_env ctx c
+ spc() ++ pr_lconstr_env ctx c
| RecCallInCaseFun c ->
- str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c
+ str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c
| RecCallInCaseArg c ->
str "recursive call in the argument of cases in" ++ spc() ++
- prterm_env ctx c
+ pr_lconstr_env ctx c
| RecCallInCasePred c ->
str "recursive call in the type of cases in" ++ spc() ++
- prterm_env ctx c
+ pr_lconstr_env ctx c
| NotGuardedForm c ->
- str "sub-expression " ++ prterm_env ctx c ++ spc() ++
+ str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
str "not in guarded form" ++ spc()++
str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)"
in
@@ -307,8 +305,8 @@ let explain_ill_formed_rec_body ctx err names i =
let explain_ill_typed_rec_body ctx i names vdefj vargs =
let ctx = make_all_name_different ctx in
- let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
- let pv = prterm_env ctx vargs.(i) in
+ let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in
+ let pv = pr_lconstr_env ctx vargs.(i) in
str"The " ++
(if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++
str"recursive definition" ++ spc () ++ pvd ++ spc () ++
@@ -317,19 +315,19 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs =
(*
let explain_not_inductive ctx c =
let ctx = make_all_name_different ctx in
- let pc = prterm_env ctx c in
+ let pc = pr_lconstr_env ctx c in
str"The term" ++ brk(1,1) ++ pc ++ spc () ++
str "is not an inductive definition"
*)
let explain_cant_find_case_type ctx c =
let ctx = make_all_name_different ctx in
- let pe = prterm_env ctx c in
+ let pe = pr_lconstr_env ctx c in
hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe)
let explain_occur_check ctx ev rhs =
let ctx = make_all_name_different ctx in
let id = Evd.string_of_existential ev in
- let pt = prterm_env ctx rhs in
+ let pt = pr_lconstr_env ctx rhs in
str"Occur check failed: tried to define " ++ str id ++
str" with term" ++ brk(1,1) ++ pt
@@ -342,14 +340,10 @@ let explain_hole_kind env = function
| BinderType Anonymous ->
str "a type for this anonymous binder"
| ImplicitArg (c,(n,ido)) ->
- if !Options.v7 then
- str "the " ++ pr_ord n ++
- str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
- else
- let id = out_some ido in
- str "an instance for the implicit parameter " ++
- pr_id id ++ spc () ++ str "of" ++
- spc () ++ Nametab.pr_global_env Idset.empty c
+ let id = out_some ido in
+ str "an instance for the implicit parameter " ++
+ pr_id id ++ spc () ++ str "of" ++
+ spc () ++ Nametab.pr_global_env Idset.empty c
| InternalHole ->
str "a term for an internal placeholder"
| TomatchTypeParameter (tyi,n) ->
@@ -361,7 +355,7 @@ let explain_not_clean ctx ev t k =
let ctx = make_all_name_different ctx in
let c = mkRel (Intset.choose (free_rels t)) in
let id = Evd.string_of_existential ev in
- let var = prterm_env ctx c in
+ let var = pr_lconstr_env ctx c in
str"Tried to define " ++ explain_hole_kind ctx k ++
str" (" ++ str id ++ str ")" ++ spc() ++
str"with a term using variable " ++ var ++ spc () ++
@@ -377,18 +371,36 @@ let explain_var_not_found ctx id =
spc () ++ str "in the current" ++ spc () ++ str "environment"
let explain_wrong_case_info ctx ind ci =
- let ctx = make_all_name_different ctx in
- let pi = prterm (mkInd ind) in
+ let pi = pr_lconstr (mkInd ind) in
if ci.ci_ind = ind then
str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++
spc () ++ str"has invalid information"
else
- let pc = prterm (mkInd ci.ci_ind) in
+ let pc = pr_lconstr (mkInd ci.ci_ind) in
str"A term of inductive type" ++ spc () ++ pi ++ spc () ++
str"was given to a pattern-matching expression on the inductive type" ++
spc () ++ pc
+let explain_cannot_unify m n =
+ let pm = pr_lconstr m in
+ let pn = pr_lconstr n in
+ str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
+ str"with" ++ brk(1,1) ++ pn
+
+let explain_refiner_cannot_generalize ty =
+ str "Cannot find a well-typed generalisation of the goal with type : " ++
+ pr_lconstr ty
+
+let explain_no_occurrence_found c =
+ str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal"
+
+let explain_cannot_unify_binding_type m n =
+ let pm = pr_lconstr m in
+ let pn = pr_lconstr n in
+ str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
+ str "which should be unifiable with" ++ brk(1,1) ++ pn
+
let explain_type_error ctx err =
let ctx = make_all_name_different ctx in
match err with
@@ -445,93 +457,74 @@ let explain_pretype_error ctx err =
explain_unexpected_type ctx actual expected
| NotProduct c ->
explain_not_product ctx c
+ | CannotUnify (m,n) -> explain_cannot_unify m n
+ | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+ | NoOccurrenceFound c -> explain_no_occurrence_found c
+ | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
(* Refiner errors *)
let explain_refiner_bad_type arg ty conclty =
str"refiner was given an argument" ++ brk(1,1) ++
- prterm arg ++ spc () ++
- str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++
- str"instead of" ++ brk(1,1) ++ prterm conclty
+ pr_lconstr arg ++ spc () ++
+ str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
+ str"instead of" ++ brk(1,1) ++ pr_lconstr conclty
let explain_refiner_occur_meta t =
- str"cannot refine with term" ++ brk(1,1) ++ prterm t ++
+ str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++
spc () ++ str"because there are metavariables, and it is" ++
spc () ++ str"neither an application nor a Case"
let explain_refiner_occur_meta_goal t =
- str"generated subgoal" ++ brk(1,1) ++ prterm t ++
+ str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++
spc () ++ str"has metavariables in it"
-let explain_refiner_cannot_applt t harg =
+let explain_refiner_cannot_apply t harg =
str"in refiner, a term of type " ++ brk(1,1) ++
- prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
- prterm harg
-
-let explain_cannot_unify m n =
- let pm = prterm m in
- let pn = prterm n in
- str"Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
- str"with" ++ brk(1,1) ++ pn
-
-let explain_cannot_unify_binding_type m n =
- let pm = prterm m in
- let pn = prterm n in
- str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
- str "which should be unifiable with" ++ brk(1,1) ++ pn
-
-let explain_refiner_cannot_generalize ty =
- str "Cannot find a well-typed generalisation of the goal with type : " ++
- prterm ty
+ pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
+ pr_lconstr harg
let explain_refiner_not_well_typed c =
- str"The term " ++ prterm c ++ str" is not well-typed"
+ str"The term " ++ pr_lconstr c ++ str" is not well-typed"
let explain_intro_needs_product () =
str "Introduction tactics needs products"
let explain_does_not_occur_in c hyp =
- str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++
+ str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++
spc () ++ pr_id hyp
let explain_non_linear_proof c =
- str "cannot refine with term" ++ brk(1,1) ++ prterm c ++
+ str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
spc () ++ str"because a metavariable has several occurrences"
-let explain_no_occurrence_found c =
- str "Found no subterm matching " ++ prterm c ++ str " in the current goal"
-
let explain_refiner_error = function
| BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
| OccurMeta t -> explain_refiner_occur_meta t
| OccurMetaGoal t -> explain_refiner_occur_meta_goal t
- | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
- | CannotUnify (m,n) -> explain_cannot_unify m n
- | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
- | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+ | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
| NotWellTyped c -> explain_refiner_not_well_typed c
| IntroNeedsProduct -> explain_intro_needs_product ()
| DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
| NonLinearProof c -> explain_non_linear_proof c
- | NoOccurrenceFound c -> explain_no_occurrence_found c
(* Inductive errors *)
let error_non_strictly_positive env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
brk(1,1) ++ pc
let error_ill_formed_inductive env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "Not enough arguments applied to the " ++ pv ++
str " in" ++ brk(1,1) ++ pc
let error_ill_formed_constructor env c v =
- let pc = prterm_env env c in
- let pv = prterm_env env v in
+ let pc = pr_lconstr_env env c in
+ let pv = pr_lconstr_env env v in
str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++
str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv
@@ -544,9 +537,9 @@ let str_of_nth n =
| _ -> "th")
let error_bad_ind_parameters env c n v1 v2 =
- let pc = prterm_env_at_top env c in
- let pv1 = prterm_env env v1 in
- let pv2 = prterm_env env v2 in
+ let pc = pr_lconstr_env_at_top env c in
+ let pv1 = pr_lconstr_env env v1 in
+ let pv2 = pr_lconstr_env env v2 in
str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++
str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc
@@ -583,10 +576,11 @@ let error_bad_induction dep indid kind =
str "is not allowed"
let error_not_mutual_in_scheme () =
- str "Induction schemes is concerned only with mutually inductive types"
+ str "Induction schemes are concerned only with distinct mutually inductive types"
+
+(* Inductive constructions errors *)
let explain_inductive_error = function
- (* These are errors related to inductive constructions *)
| NonPos (env,c,v) -> error_non_strictly_positive env c v
| NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v
| NotConstructor (env,c,v) -> error_ill_formed_constructor env c v
@@ -596,7 +590,10 @@ let explain_inductive_error = function
| SameNamesOverlap idl -> error_same_names_overlap idl
| NotAnArity id -> error_not_an_arity id
| BadEntry -> error_bad_entry ()
- (* These are errors related to recursors *)
+
+(* Recursion schemes errors *)
+
+let explain_recursion_scheme_error = function
| NotAllowedCaseAnalysis (dep,k,i) ->
error_not_allowed_case_analysis dep k i
| BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
@@ -606,7 +603,7 @@ let explain_inductive_error = function
let explain_bad_pattern ctx cstr ty =
let ctx = make_all_name_different ctx in
- let pt = prterm_env ctx ty in
+ let pt = pr_lconstr_env ctx ty in
let pc = pr_constructor ctx cstr in
str "Found the constructor " ++ pc ++ brk(1,1) ++
str "while matching a term of type " ++ pt ++ brk(1,1) ++
@@ -620,31 +617,38 @@ let explain_bad_constructor ctx cstr ind =
str "while a constructor of " ++ pi ++ brk(1,1) ++
str "is expected"
-let explain_wrong_numarg_of_constructor ctx cstr n =
- let pc = pr_constructor ctx cstr in
- str "The constructor " ++ pc ++ str " expects " ++
- (if n = 0 then str "no argument." else if n = 1 then str "1 argument."
- else (int n ++ str " arguments."))
+let decline_string n s =
+ if n = 0 then "no "^s
+ else if n = 1 then "1 "^s
+ else (string_of_int n^" "^s^"s")
+
+let explain_wrong_numarg_constructor ctx cstr n =
+ str "The constructor " ++ pr_constructor ctx cstr ++
+ str " expects " ++ str (decline_string n "argument")
+
+let explain_wrong_numarg_inductive ctx ind n =
+ str "The inductive type " ++ pr_inductive ctx ind ++
+ str " expects " ++ str (decline_string n "argument")
let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity=
let ctx = make_all_name_different ctx in
- let pp = prterm_env ctx pred in
+ let pp = pr_lconstr_env ctx pred in
str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
str "should be of arity" ++ spc () ++
- prterm_env ctx nondep_arity ++ spc () ++
+ pr_lconstr_env ctx nondep_arity ++ spc () ++
str "(for non dependent case) or" ++
- spc () ++ prterm_env ctx dep_arity ++ spc () ++ str "(for dependent case)."
+ spc () ++ pr_lconstr_env ctx dep_arity ++ spc () ++ str "(for dependent case)."
let explain_needs_inversion ctx x t =
let ctx = make_all_name_different ctx in
- let px = prterm_env ctx x in
- let pt = prterm_env ctx t in
+ let px = pr_lconstr_env ctx x in
+ let pt = pr_lconstr_env ctx t in
str "Sorry, I need inversion to compile pattern matching of term " ++
px ++ str " of type: " ++ pt
let explain_unused_clause env pats =
- let s = if List.length pats > 1 then "s" else "" in
(* Without localisation
+ let s = if List.length pats > 1 then "s" else "" in
(str ("Unused clause with pattern"^s) ++ spc () ++
hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
*)
@@ -659,7 +663,7 @@ let explain_cannot_infer_predicate ctx typs =
let ctx = make_all_name_different ctx in
let pr_branch (cstr,typ) =
let cstr,_ = decompose_app cstr in
- str "For " ++ prterm_env ctx cstr ++ str " : " ++ prterm_env ctx typ
+ str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ
in
str "Unable to unify the types found in the branches:" ++
spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
@@ -670,7 +674,9 @@ let explain_pattern_matching_error env = function
| BadConstructor (c,ind) ->
explain_bad_constructor env c ind
| WrongNumargConstructor (c,n) ->
- explain_wrong_numarg_of_constructor env c n
+ explain_wrong_numarg_constructor env c n
+ | WrongNumargInductive (c,n) ->
+ explain_wrong_numarg_inductive env c n
| WrongPredicateArity (pred,n,dep) ->
explain_wrong_predicate_arity env pred n dep
| NeedsInversion (x,t) ->
@@ -681,3 +687,9 @@ let explain_pattern_matching_error env = function
explain_non_exhaustive env tms
| CannotInferPredicate typs ->
explain_cannot_infer_predicate env typs
+
+let explain_reduction_tactic_error = function
+ | Tacred.InvalidAbstraction (env,c,(env',e)) ->
+ str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++
+ spc() ++ str "is not well typed." ++ fnl () ++
+ explain_type_error env' e