diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 23:20:18 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-09 23:20:18 +0000 |
commit | baa3e16836c3f0daf24ba47aadbdee525762d6ec (patch) | |
tree | 4841eb29be562802e06f9aa3f72ccda37daa5814 | |
parent | 35c127288df53b8561d13082738806fa44049a1a (diff) |
Ajout des messages d'erreurs de Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | kernel/environ.mli | 1 | ||||
-rw-r--r-- | kernel/inductive.ml | 2 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | kernel/term.ml | 4 | ||||
-rw-r--r-- | kernel/term.mli | 4 | ||||
-rw-r--r-- | kernel/type_errors.ml | 5 | ||||
-rw-r--r-- | kernel/type_errors.mli | 5 | ||||
-rw-r--r-- | parsing/astterm.ml | 2 | ||||
-rw-r--r-- | parsing/printer.ml | 60 | ||||
-rw-r--r-- | parsing/printer.mli | 5 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 18 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 19 | ||||
-rw-r--r-- | pretyping/retyping.ml | 6 | ||||
-rw-r--r-- | pretyping/retyping.mli | 1 | ||||
-rwxr-xr-x | syntax/PPCommand.v | 28 | ||||
-rw-r--r-- | toplevel/himsg.ml | 37 |
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); |