aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/environ.mli1
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/term.ml4
-rw-r--r--kernel/term.mli4
-rw-r--r--kernel/type_errors.ml5
-rw-r--r--kernel/type_errors.mli5
-rw-r--r--parsing/astterm.ml2
-rw-r--r--parsing/printer.ml60
-rw-r--r--parsing/printer.mli5
-rw-r--r--pretyping/pretype_errors.ml18
-rw-r--r--pretyping/pretype_errors.mli19
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/retyping.mli1
-rwxr-xr-xsyntax/PPCommand.v28
-rw-r--r--toplevel/himsg.ml37
16 files changed, 165 insertions, 34 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 3c4dd633e..cfcdf2d36 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -48,6 +48,7 @@ val lookup_mind : section_path -> env -> mutual_inductive_body
val lookup_mind_specif : constr -> env -> mind_specif
val id_of_global : env -> sorts oper -> identifier
+
val id_of_name_using_hdchar : env -> constr -> name -> identifier
val named_hd : env -> constr -> name -> name
val prod_name : env -> name * constr * constr -> constr
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 5ab2886a9..6ae5bb931 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -157,3 +157,5 @@ let mind_check_lc params mie =
if not (List.length lna = ntypes) then raise (InductiveError BadEntry)
in
List.iter check_lc mie.mind_entry_inds
+
+let inductive_of_constructor (ind_sp,i) = ind_sp
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 1f1d5927f..63e85a539 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -106,3 +106,5 @@ val mind_extract_and_check_params :
val mind_extract_params : int -> constr -> (name * constr) list * constr
val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit
+
+val inductive_of_constructor : constructor_path -> inductive_path
diff --git a/kernel/term.ml b/kernel/term.ml
index 38dbc3765..8e9c94c71 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -11,6 +11,8 @@ open Univ
(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
+type existential_key = int
+
type 'a oper =
(* DOP0 *)
| Meta of int
@@ -19,7 +21,7 @@ type 'a oper =
| Cast | Prod | Lambda
(* DOPN *)
| AppL | Const of section_path | Abst of section_path
- | Evar of int
+ | Evar of existential_key
| MutInd of inductive_path
| MutConstruct of constructor_path
| MutCase of case_info
diff --git a/kernel/term.mli b/kernel/term.mli
index 6e7101ad3..869e65ca4 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -11,12 +11,14 @@ open Generic
['a] is the type of sorts. ([XTRA] is an extra slot, for putting in
whatever sort of operator we need for whatever sort of application.) *)
+type existential_key = int
+
type 'a oper =
| Meta of int
| Sort of 'a
| Cast | Prod | Lambda
| AppL | Const of section_path | Abst of section_path
- | Evar of int
+ | Evar of existential_key
| MutInd of inductive_path
| MutConstruct of constructor_path
| MutCase of case_info
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f3cb78205..89174d1bf 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -31,6 +31,11 @@ type type_error =
| CantFindCaseType of constr
| OccurCheck of int * constr
| NotClean of int * constr
+ (* Pattern-matching errors *)
+ | BadConstructor of constructor_path * inductive_path
+ | WrongNumargConstructor of constructor_path * int
+ | WrongPredicateArity of constr * int * int
+ | NeedsInversion of constr * constr
exception TypeError of path_kind * context * type_error
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 70f444987..aaf278c27 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -33,6 +33,11 @@ type type_error =
| CantFindCaseType of constr
| OccurCheck of int * constr
| NotClean of int * constr
+ (* Pattern-matching errors *)
+ | BadConstructor of constructor_path * inductive_path
+ | WrongNumargConstructor of constructor_path * int
+ | WrongPredicateArity of constr * int * int
+ | NeedsInversion of constr * constr
exception TypeError of path_kind * context * type_error
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 8b4c371d1..3739a43c5 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -108,7 +108,7 @@ let dbize_ctxt =
let dbize_global loc = function
| ("CONST", sp::ctxt) ->
RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
- | ("EVAR", (Num (_,ev))::ctxt) ->
+ | ("EVAR", (Num (_,ev))::ctxt) ->
RRef (loc,REVar (ev,dbize_ctxt ctxt))
| ("MUTIND", sp::Num(_,tyi)::ctxt) ->
RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
diff --git a/parsing/printer.ml b/parsing/printer.ml
index e7d53dabb..dc17ae479 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -6,6 +6,7 @@ open Util
open Names
open Term
open Sign
+open Environ
open Global
open Declare
open Coqast
@@ -31,42 +32,45 @@ let with_implicits f x =
with e ->
Termast.print_implicits := oimpl; raise e
-let pr_global dflt k oper =
- try
- let id = id_of_global oper in
- if is_existential_oper oper then
- [< 'sTR (string_of_id id) >]
- else
- let (oper',_) = global_operator (Nametab.sp_of_id k id) id in
- if oper = oper' then
- [< 'sTR(string_of_id id) >]
- else
- dflt
- with
- | Failure _ | Not_found ->
- [< 'sTR"[Error printing " ; dflt ; 'sTR"]" >]
- | _ ->
- [< 'sTR"Error [Nasty error printing " ; dflt ; 'sTR"]" >]
+let pr_qualified sp id =
+ if Nametab.sp_of_id (kind_of_path sp) id = sp
+ then [< 'sTR(string_of_id id) >]
+ else [< 'sTR(string_of_path sp) >]
+
+let pr_constant sp = pr_qualified sp (basename sp)
+
+let pr_existential ev = [< 'sTR ("?" ^ string_of_int ev) >]
+
+let pr_inductive (sp,tyi as ind_sp) =
+ let id = id_of_global (MutInd ind_sp) in
+ pr_qualified sp id
+
+let pr_constructor ((sp,tyi),i as cstr_sp) =
+ let id = id_of_global (MutConstruct cstr_sp) in
+ pr_qualified sp id
+
+(*
+let pr_global k oper =
+ let id = id_of_global oper in
+ [< 'sTR (string_of_id id) >]
+*)
let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >]
let globpr k gt = match gt with
| Nvar(_,s) -> [< 'sTR s >]
+ | Node(_,"EVAR", (Num (_,ev))::_) ->
+ if !print_arguments then dfltpr gt
+ else pr_existential ev
| Node(_,"CONST",(Path(_,sl,s))::_) ->
- if !print_arguments then
- dfltpr gt
- else
- pr_global (dfltpr gt) k (Const (section_path sl s))
+ if !print_arguments then dfltpr gt
+ else pr_constant (section_path sl s)
| Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) ->
- if !print_arguments then
- (dfltpr gt)
- else
- pr_global (dfltpr gt) k (MutInd(section_path sl s,tyi))
+ if !print_arguments then (dfltpr gt)
+ else pr_inductive (section_path sl s,tyi)
| Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) ->
- if !print_arguments then
- (dfltpr gt)
- else
- pr_global (dfltpr gt) k (MutConstruct((section_path sl s,tyi),i))
+ if !print_arguments then (dfltpr gt)
+ else pr_constructor ((section_path sl s,tyi),i)
| gt -> dfltpr gt
let apply_prec = Some (("Term",(9,0,0)),Extend.L)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index a87f15deb..217ec6197 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -27,6 +27,11 @@ val pr_ne_env : std_ppcmds -> path_kind -> context -> std_ppcmds
val prrawterm : Rawterm.rawconstr -> std_ppcmds
val prpattern : Rawterm.pattern -> std_ppcmds
+val pr_constant : section_path -> std_ppcmds
+val pr_existential : existential_key -> std_ppcmds
+val pr_constructor : constructor_path -> std_ppcmds
+val pr_inductive : inductive_path -> std_ppcmds
+
val pr_sign : var_context -> std_ppcmds
val pr_env_opt : context -> std_ppcmds
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index c3baf8ea0..083b94df0 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,6 +18,24 @@ let error_ill_formed_branch k env c i actty expty =
let error_number_branches_loc loc k env c ct expn =
raise (PretypeError (loc, k, context env, NumberBranches (c,ct,expn)))
+let error_case_not_inductive_loc loc k env c ct =
+ raise (PretypeError (loc, k, context env, CaseNotInductive (c,ct)))
+
+(* Pattern-matching errors *)
+
+let error_bad_constructor_loc loc k cstr ind =
+ raise (PretypeError (loc, k, Global.context(), BadConstructor (cstr,ind)))
+
+let error_wrong_numarg_constructor_loc loc k c n =
+ raise (PretypeError (loc, k, Global.context(), WrongNumargConstructor (c,n)))
+
+let error_wrong_predicate_arity_loc loc k env c n1 n2 =
+ raise (PretypeError (loc, k, context env, WrongPredicateArity (c,n1,n2)))
+
+let error_needs_inversion k env x t =
+ raise (TypeError (k, context env, NeedsInversion (x,t)))
+
+
let error_ill_formed_branch_loc loc k env c i actty expty =
raise (PretypeError (loc, k, context env, IllFormedBranch (c,i,actty,expty)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 33238ecd9..6d39fdd31 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,6 +24,25 @@ val error_ill_formed_branch_loc :
val error_number_branches_loc :
loc -> path_kind -> env -> constr -> constr -> int -> 'b
+val error_case_not_inductive_loc :
+ loc -> path_kind -> env -> constr -> constr -> 'b
+
+(* Pattern-matching errors *)
+
+val error_bad_constructor_loc :
+ loc -> path_kind -> constructor_path -> inductive_path -> 'b
+
+val error_wrong_numarg_constructor_loc :
+ loc -> path_kind -> constructor_path -> int -> 'b
+
+val error_wrong_predicate_arity_loc :
+ loc -> path_kind -> env -> constr -> int -> int -> 'b
+
+val error_needs_inversion : path_kind -> env -> constr -> constr -> 'a
+
+
+(* Implicit arguments synthesis errors *)
+
val error_occur_check : path_kind -> env -> int -> constr -> 'a
val error_not_clean : path_kind -> env -> int -> constr -> 'a
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4978d7b11..07ea18cdf 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,6 +18,7 @@ type mutind =
{fullmind : constr;
mind : mutind_id;
nparams : int;
+ nrealargs : int;
nconstr : int;
params : constr list;
realargs : constr list;
@@ -28,13 +29,14 @@ let try_mutind_of env sigma ty =
let (mind,largs) = find_mrectype env sigma ty in
let mispec = lookup_mind_specif mind env in
let nparams = mis_nparams mispec in
- let (params,proper_args) = list_chop nparams largs in
+ let (params,realargs) = list_chop nparams largs in
{fullmind = ty;
mind = (let (sp,i,cv) = destMutInd mind in (sp,i),cv);
nparams = nparams;
+ nrealargs = List.length realargs;
nconstr = mis_nconstr mispec;
params = params;
- realargs = proper_args;
+ realargs = realargs;
arity = Instantiate.mis_arity mispec}
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index ce9ea7390..354771e6e 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -33,6 +33,7 @@ type mutind = {
fullmind : constr;
mind : mutind_id;
nparams : int;
+ nrealargs : int;
nconstr : int;
params : constr list;
realargs : constr list;
diff --git a/syntax/PPCommand.v b/syntax/PPCommand.v
index 0033807bd..7df18f7be 100755
--- a/syntax/PPCommand.v
+++ b/syntax/PPCommand.v
@@ -71,7 +71,7 @@ Syntax constr
(* Things parsed in command7 *)
(* Things parsed in command8 *)
level 8:
-
+(*
lambda [(LAMBDA $Dom $Body)]
-> [(LAMBOX (BINDERS) (LAMBDA $Dom $Body))]
| lambdalist [(LAMBDALIST $c $body)]
@@ -93,6 +93,32 @@ Syntax constr
-> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)]
| lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)]
-> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
+*)
+ lambda [(LAMBDA $Dom [$x]$Body)]
+ -> [(LAMBOX (BINDERS (BINDER $Dom $x)) $Body)]
+ | lambda_anon [(LAMBDA $Dom [<>]$Body)]
+ -> [(LAMBOX (BINDERS (BINDER $Dom _)) $Body)]
+ | lambdalist [(LAMBDALIST $c [$x]$body)]
+ -> [(LAMLBOX (BINDERS) $c (IDS $x) $body)]
+ | lambdalist_anon [(LAMBDALIST $c [<>]$body)]
+ -> [(LAMLBOX (BINDERS) $c (IDS _) $body)]
+
+ | formated_lambda [(LAMBOX $pbi $t)]
+ -> [ [<hov 0> "[" [<hv 0> $pbi] "]" [0 1] $t:E ] ]
+
+ | lambda_cons [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [$x]$body))]
+ -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom $x)) $body)]
+ | lambda_cons_anon [(LAMBOX (BINDERS ($LIST $acc)) (LAMBDA $Dom [<>]$body))]
+ -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $Dom _)) $body)]
+ | lambdal_start [(LAMBOX $pbi (LAMBDALIST $Dom $Body))]
+ -> [(LAMLBOX $pbi $Dom (IDS) $Body)]
+
+ | lambdal_end [(LAMLBOX (BINDERS ($LIST $acc)) $c (IDS ($LIST $ids)) $t)]
+ -> [(LAMBOX (BINDERS ($LIST $acc) (BINDER $c ($LIST $ids))) $t)]
+ | lambdal_cons_anon [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [<>]$body)]
+ -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) _) $body)]
+ | lambdal_cons [(LAMLBOX $pbi $c (IDS ($LIST $ids)) [$id]$body)]
+ -> [(LAMLBOX $pbi $c (IDS ($LIST $ids) $id) $body)]
| pi [<<($x : $A)$B>>] -> [(PRODBOX (BINDERS) <<($x : $A)$B>>)]
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 97d61ef38..a124d1446 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -201,6 +201,34 @@ let explain_not_clean k ctx ev t =
'sTR" with a term using variable "; var; 'sPC;
'sTR"which is not in its scope." >]
+(* Pattern-matching errors *)
+let explain_bad_constructor k ctx cstr ind =
+ let pi = pr_inductive ind in
+ let pc = pr_constructor cstr in
+ let pt = pr_inductive (inductive_of_constructor cstr) in
+ [< 'sTR "Expecting a constructor in inductive type "; pi; 'bRK(1,1) ;
+ 'sTR " but found the constructor " ; pc; 'bRK(1,1) ;
+ 'sTR " in inductive type "; pt >]
+
+let explain_wrong_numarg_of_constructor k ctx cstr n =
+ let pc = pr_constructor cstr in
+ [<'sTR "The constructor "; pc;
+ 'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">]
+
+let explain_wrong_predicate_arity k ctx pred nondep_arity dep_arity=
+ let pp = gentermpr k ctx pred in
+ [<'sTR "The elimination predicate " ; pp; 'cUT;
+ 'sTR "should be of arity " ;
+ 'iNT nondep_arity ; 'sTR " (for non dependent case) or " ;
+ 'iNT dep_arity ; 'sTR " (for dependent case).">]
+
+let explain_needs_inversion k ctx x t =
+ let px = gentermpr k ctx x in
+ let pt = gentermpr k ctx t in
+ [< 'sTR "Sorry, I need inversion to compile pattern matching of term ";
+ px ; 'sTR " of type: "; pt>]
+
+
let explain_type_error k ctx = function
| UnboundRel n ->
explain_unbound_rel k ctx n
@@ -240,6 +268,15 @@ let explain_type_error k ctx = function
explain_occur_check k ctx n c
| NotClean (n,c) ->
explain_not_clean k ctx n c
+ (* Pattern-matching errors *)
+ | BadConstructor (c,ind) ->
+ explain_bad_constructor k ctx c ind
+ | WrongNumargConstructor (c,n) ->
+ explain_wrong_numarg_of_constructor k ctx c n
+ | WrongPredicateArity (pred,n,dep) ->
+ explain_wrong_predicate_arity k ctx pred n dep
+ | NeedsInversion (x,t) ->
+ explain_needs_inversion k ctx x t
let explain_refiner_bad_type k ctx arg ty conclty =
[< 'sTR"refiner was given an argument"; 'bRK(1,1);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 14:48:37 +0000