diff options
| -rw-r--r-- | kernel/type_errors.ml | 11 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 13 | ||||
| -rw-r--r-- | kernel/typeops.ml | 13 | ||||
| -rw-r--r-- | parsing/astterm.ml | 33 | ||||
| -rw-r--r-- | parsing/printer.ml | 15 | ||||
| -rw-r--r-- | parsing/printer.mli | 8 | ||||
| -rw-r--r-- | parsing/termast.ml | 56 | ||||
| -rw-r--r-- | parsing/termast.mli | 8 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 12 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 10 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 12 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 | ||||
| -rw-r--r-- | toplevel/fhimsg.ml | 52 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 57 |
15 files changed, 194 insertions, 110 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 8ca7135aa..a4661433e 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -22,7 +22,9 @@ type type_error = | IllFormedBranch of constr * int * constr * constr | Generalization of (name * typed_type) * constr | ActualType of constr * constr * constr - | CantAply of string * unsafe_judgment * unsafe_judgment list + | CantApplyBadType of (int * constr * constr) + * unsafe_judgment * unsafe_judgment list + | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list | IllFormedRecBody of std_ppcmds * name list * int * constr array | IllTypedRecBody of int * name list * unsafe_judgment array * typed_type array @@ -73,8 +75,11 @@ let error_generalization k env nvar c = let error_actual_type k env c actty expty = raise (TypeError (k, context env, ActualType (c,actty,expty))) -let error_cant_apply k env s rator randl = - raise (TypeError (k, context env, CantAply (s,rator,randl))) +let error_cant_apply_not_functional k env rator randl = + raise (TypeError (k, context env, CantApplyNonFunctional (rator,randl))) + +let error_cant_apply_bad_type k env t rator randl = + raise (TypeError (k, context env, CantApplyBadType (t,rator,randl))) let error_ill_formed_rec_body k env str lna i vdefs = raise (TypeError (k, context env, IllFormedRecBody (str,lna,i,vdefs))) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 7ffbd312e..a97541980 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -24,7 +24,9 @@ type type_error = | IllFormedBranch of constr * int * constr * constr | Generalization of (name * typed_type) * constr | ActualType of constr * constr * constr - | CantAply of string * unsafe_judgment * unsafe_judgment list + | CantApplyBadType of (int * constr * constr) + * unsafe_judgment * unsafe_judgment list + | CantApplyNonFunctional of unsafe_judgment * unsafe_judgment list | IllFormedRecBody of std_ppcmds * name list * int * constr array | IllTypedRecBody of int * name list * unsafe_judgment array * typed_type array @@ -71,9 +73,12 @@ val error_generalization : val error_actual_type : path_kind -> env -> constr -> constr -> constr -> 'b -val error_cant_apply : - path_kind -> env -> string -> unsafe_judgment - -> unsafe_judgment list -> 'b +val error_cant_apply_not_functional : + path_kind -> env -> unsafe_judgment -> unsafe_judgment list -> 'b + +val error_cant_apply_bad_type : + path_kind -> env -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment list -> 'b val error_ill_formed_rec_body : path_kind -> env -> std_ppcmds diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 6c7e1bbe5..1a6c1d885 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -317,7 +317,7 @@ let cast_rel env sigma cj tj = (* Type of an application. *) let apply_rel_list env sigma nocheck argjl funj = - let rec apply_rec typ cst = function + let rec apply_rec n typ cst = function | [] -> { uj_val = applist (j_val_only funj, List.map j_val_only argjl); uj_type = typ; @@ -327,18 +327,19 @@ let apply_rel_list env sigma nocheck argjl funj = match whd_betadeltaiota env sigma typ with | DOP2(Prod,c1,DLAM(_,c2)) -> if nocheck then - apply_rec (subst1 hj.uj_val c2) cst restjl + apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl else (try let c = conv_leq env sigma hj.uj_type c1 in let cst' = Constraint.union cst c in - apply_rec (subst1 hj.uj_val c2) cst' restjl + apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl with NotConvertible -> - error_cant_apply CCI env "Type Error" funj argjl) + error_cant_apply_bad_type CCI env (n,hj.uj_type,c1) + funj argjl) | _ -> - error_cant_apply CCI env "Non-functional construction" funj argjl + error_cant_apply_not_functional CCI env funj argjl in - apply_rec funj.uj_type Constraint.empty argjl + apply_rec 1 funj.uj_type Constraint.empty argjl (* Fixpoints. *) diff --git a/parsing/astterm.ml b/parsing/astterm.ml index dcc0177a2..ad4e07dc8 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -125,11 +125,25 @@ let dbize_ctxt ctxt = (function | Nvar (loc,s) -> (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *) - VAR (ident_of_nvar loc s) + RRef (loc, RVar (ident_of_nvar loc s)) | _ -> anomaly "Bad ast for local ctxt of a global reference") ctxt in Array.of_list l +let dbize_constr_ctxt = + Array.map + (function + | VAR id -> + (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *) + RRef (dummy_loc, RVar id) + | _ -> anomaly "Bad ast for local ctxt of a global reference") + +let dbize_rawconstr_ctxt = + Array.map + (function + | RRef (_, RVar id) -> VAR id + | _ -> anomaly "Bad ast for local ctxt of a global reference") + let dbize_global loc = function | ("CONST", sp::ctxt) -> RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt)) @@ -145,10 +159,11 @@ let dbize_global loc = function [< 'sTR "Bad ast for this global a reference">]) let ref_from_constr = function - | DOPN (Const sp,ctxt) -> RConst (sp, ctxt) - | DOPN (Evar ev,ctxt) -> REVar (ev, ctxt) - | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j), ctxt) - | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), ctxt) + | DOPN (Const sp,ctxt) -> RConst (sp, dbize_constr_ctxt ctxt) + | DOPN (Evar ev,ctxt) -> REVar (ev, dbize_constr_ctxt ctxt) + | DOPN (MutConstruct (spi,j),ctxt) -> + RConstruct ((spi,j), dbize_constr_ctxt ctxt) + | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), dbize_constr_ctxt ctxt) | VAR id -> RVar id (* utilisé pour coe_value (tmp) *) | _ -> anomaly "Not a reference" @@ -630,10 +645,10 @@ let ctxt_of_ids ids = Array.of_list (List.map (function id -> VAR id) ids) let rec pat_of_ref metas vars = function - | RConst (sp,ctxt) -> RConst (sp, ctxt) - | RInd (ip,ctxt) -> RInd (ip, ctxt) - | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt) - | REVar (n,ctxt) -> REVar (n, ctxt) + | RConst (sp,ctxt) -> RConst (sp, dbize_rawconstr_ctxt ctxt) + | RInd (ip,ctxt) -> RInd (ip, dbize_rawconstr_ctxt ctxt) + | RConstruct(cp,ctxt) ->RConstruct(cp, dbize_rawconstr_ctxt ctxt) + | REVar (n,ctxt) -> REVar (n, dbize_rawconstr_ctxt ctxt) | RAbst _ -> error "pattern_of_rawconstr: not implemented" | RVar _ -> assert false (* Capturé dans pattern_of_raw *) diff --git a/parsing/printer.ml b/parsing/printer.ml index bad9c3866..5a4f8ae5b 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -119,16 +119,17 @@ let fprtype a = (* For compatibility *) let fterm0 = fprterm_env -let pr_constant cst = gentermpr (ast_of_constant cst) -let pr_existential ev = gentermpr (ast_of_existential ev) -let pr_inductive ind = gentermpr (ast_of_inductive ind) -let pr_constructor cstr = gentermpr (ast_of_constructor cstr) +let pr_constant env cst = gentermpr (ast_of_constant (unitize_env env) cst) +let pr_existential env ev = gentermpr (ast_of_existential (unitize_env env) ev) +let pr_inductive env ind = gentermpr (ast_of_inductive (unitize_env env) ind) +let pr_constructor env cstr = + gentermpr (ast_of_constructor (unitize_env env) cstr) open Pattern let pr_ref_label = function (* On triche sur le contexte *) - | ConstNode sp -> pr_constant (sp,[||]) - | IndNode sp -> pr_inductive (sp,[||]) - | CstrNode sp -> pr_constructor (sp,[||]) + | ConstNode sp -> pr_constant (Global.context()) (sp,[||]) + | IndNode sp -> pr_inductive (Global.context()) (sp,[||]) + | CstrNode sp -> pr_constructor (Global.context()) (sp,[||]) | VarNode id -> print_id id let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t) diff --git a/parsing/printer.mli b/parsing/printer.mli index d6e785c8f..75ac36c08 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -22,10 +22,10 @@ val prtype : typed_type -> std_ppcmds val pr_rawterm : Rawterm.rawconstr -> std_ppcmds val pr_cases_pattern : Rawterm.cases_pattern -> std_ppcmds -val pr_constant : constant -> std_ppcmds -val pr_existential : existential -> std_ppcmds -val pr_constructor : constructor -> std_ppcmds -val pr_inductive : inductive -> std_ppcmds +val pr_constant : 'a assumptions -> constant -> std_ppcmds +val pr_existential : 'a assumptions -> existential -> std_ppcmds +val pr_constructor : 'a assumptions -> constructor -> std_ppcmds +val pr_inductive : 'a assumptions -> inductive -> std_ppcmds val pr_ref_label : constr_label -> std_ppcmds val pr_pattern : constr_pattern -> std_ppcmds val pr_pattern_env : 'a assumptions -> constr_pattern -> std_ppcmds diff --git a/parsing/termast.ml b/parsing/termast.ml index f4b707193..9adc75473 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -86,48 +86,44 @@ let stringopt_of_name = function | Name id -> Some (string_of_id id) | Anonymous -> None -let ast_of_constant_ref (sp,ids) = +let ast_of_constant_ref pr (sp,ids) = let a = ope("CONST", [path_section dummy_loc sp]) in - if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids)) + if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) else a -let ast_of_constant (ev,ids) = ast_of_constant_ref (ev,ids_of_ctxt ids) - -let ast_of_existential_ref (ev,ids) = +let ast_of_existential_ref pr (ev,ids) = let a = ope("EVAR", [num ev]) in if !print_arguments or !print_evar_arguments then - ope("INSTANCE",a::(List.map ast_of_ident ids)) + ope("INSTANCE",a::(array_map_to_list pr ids)) else a -let ast_of_existential (ev,ids) = ast_of_existential_ref (ev,ids_of_ctxt ids) - -let ast_of_constructor_ref (((sp,tyi),n) as cstr_sp,ids) = +let ast_of_constructor_ref pr (((sp,tyi),n) as cstr_sp,ids) = let a = ope("MUTCONSTRUCT",[path_section dummy_loc sp; num tyi; num n]) in - if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids)) + if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) else a -let ast_of_constructor (ev,ids) = ast_of_constructor_ref (ev,ids_of_ctxt ids) - -let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) = +let ast_of_inductive_ref pr ((sp,tyi) as ind_sp,ids) = let a = ope("MUTIND", [path_section dummy_loc sp; num tyi]) in - if !print_arguments then ope("INSTANCE",a::(List.map ast_of_ident ids)) + if !print_arguments then ope("INSTANCE",a::(array_map_to_list pr ids)) else a -let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt) - -let ast_of_ref = function - | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_ctxt ctxt) +let ast_of_ref pr = function + | RConst (sp,ctxt) -> ast_of_constant_ref pr (sp,ctxt) | RAbst (sp) -> ope("ABST", (path_section dummy_loc sp) ::(List.map ast_of_ident (* on triche *) [])) - | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt) - | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt) + | RInd (ind,ctxt) -> ast_of_inductive_ref pr (ind,ctxt) + | RConstruct (cstr,ctxt) -> ast_of_constructor_ref pr (cstr,ctxt) | RVar id -> ast_of_ident id - | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt) + | REVar (ev,ctxt) -> ast_of_existential_ref pr (ev,ctxt) + + (**********************************************************************) (* conversion of patterns *) +let adapt (cstr_sp,ctxt) = (cstr_sp,Array.of_list ctxt) + let rec ast_of_cases_pattern = function (* loc is thrown away for printing *) | PatVar (loc,Name id) -> nvar (string_of_id id) | PatVar (loc,Anonymous) -> nvar "_" @@ -135,10 +131,12 @@ let rec ast_of_cases_pattern = function (* loc is thrown away for printing *) let args = List.map ast_of_cases_pattern args in ope("PATTAS", [nvar (string_of_id id); - ope("PATTCONSTRUCT", (ast_of_constructor_ref cstr)::args)]) + ope("PATTCONSTRUCT", + (ast_of_constructor_ref ast_of_ident (adapt cstr))::args)]) | PatCstr(loc,cstr,args,Anonymous) -> ope("PATTCONSTRUCT", - (ast_of_constructor_ref cstr)::List.map ast_of_cases_pattern args) + (ast_of_constructor_ref ast_of_ident (adapt cstr)):: + List.map ast_of_cases_pattern args) let ast_dependent na aty = match na with @@ -205,7 +203,7 @@ let ast_of_app impl f args = *) let rec ast_of_raw = function - | RRef (_,ref) -> ast_of_ref ref + | RRef (_,ref) -> ast_of_ref ast_of_raw ref | RMeta (_,n) -> ope("META",[num n]) | RApp (_,f,args) -> let (f,args) = @@ -737,8 +735,16 @@ let ast_of_constr at_top env t = with Detyping.StillDLAM -> old_bdize at_top env t' +let ast_of_constant env = ast_of_constant_ref (ast_of_constr false env) + +let ast_of_existential env = ast_of_existential_ref (ast_of_constr false env) + +let ast_of_inductive env = ast_of_inductive_ref (ast_of_constr false env) + +let ast_of_constructor env = ast_of_constructor_ref (ast_of_constr false env) + let rec ast_of_pattern env = function - | PRef ref -> ast_of_ref ref + | PRef ref -> ast_of_ref (ast_of_constr false env) ref | PRel n -> (try match fst (lookup_rel n env) with | Name id -> ast_of_ident id diff --git a/parsing/termast.mli b/parsing/termast.mli index e0b8069d9..7961ee7fb 100644 --- a/parsing/termast.mli +++ b/parsing/termast.mli @@ -25,10 +25,10 @@ val ast_of_constr : bool -> unit assumptions -> constr -> Coqast.t val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t i*) -val ast_of_constant : constant -> Coqast.t -val ast_of_existential : existential -> Coqast.t -val ast_of_constructor : constructor -> Coqast.t -val ast_of_inductive : inductive -> Coqast.t +val ast_of_constant : unit assumptions -> constant -> Coqast.t +val ast_of_existential : unit assumptions -> existential -> Coqast.t +val ast_of_constructor : unit assumptions -> constructor -> Coqast.t +val ast_of_inductive : unit assumptions -> inductive -> Coqast.t (* For debugging *) val print_implicits : bool ref diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 15577dd9e..c98eeab16 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -167,7 +167,7 @@ let inh_cast_rel env isevars cj tj = uj_kind = whd_betadeltaiota env !isevars tj.uj_type } let inh_apply_rel_list nocheck env isevars argjl funj vtcon = - let rec apply_rec acc typ = function + let rec apply_rec n acc typ = function | [] -> let resj = { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); @@ -190,14 +190,14 @@ let inh_apply_rel_list nocheck env isevars argjl funj vtcon = (try inh_conv_coerce_to env isevars c1 hj with Failure _ | Not_found -> - error_cant_apply CCI env "Type Error" - (j_nf_ise env !isevars funj) + error_cant_apply_bad_type CCI env (n,c1,hj.uj_type) + (j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl)) in - apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl + apply_rec (n+1) (hj'::acc) (subst1 hj'.uj_val c2) restjl | _ -> - error_cant_apply CCI env "Non-functional construction" + error_cant_apply_not_functional CCI env (j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl) in - apply_rec [] funj.uj_type argjl + apply_rec 1 [] funj.uj_type argjl diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 34ffa2f95..901e60b8c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -314,13 +314,15 @@ let rec detype avoid env t = | IsAppL (f,args) -> RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args) | IsConst (sp,cl) -> - RRef(dummy_loc,RConst(sp,cl)) + RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) | IsEvar (ev,cl) -> - RRef(dummy_loc,REVar(ev,cl)) + RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" - | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,cl)) - | IsMutConstruct (cstr_sp,cl) -> RRef (dummy_loc,RConstruct (cstr_sp,cl)) + | IsMutInd (ind_sp,cl) -> + RRef (dummy_loc,RInd (ind_sp,Array.map (detype avoid env) cl)) + | IsMutConstruct (cstr_sp,cl) -> + RRef (dummy_loc,RConstruct (cstr_sp,Array.map (detype avoid env) cl)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2f059f6c1..5d64f6e23 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -212,11 +212,11 @@ let pretype_var loc env lvar id = let trad_metamap = ref [] let trad_nocheck = ref false -let pretype_ref loc isevars env lvar = function +let pretype_ref pretype loc isevars env lvar = function | RVar id -> pretype_var loc env lvar id | RConst (sp,ctxt) -> - let cst = (sp,ctxt_of_ids ctxt) in + let cst = (sp,Array.map pretype ctxt) in make_judge (mkConst cst) (type_of_constant env !isevars cst) | RAbst sp -> failwith "Pretype: abst doit disparaître" @@ -246,11 +246,11 @@ let pretype_ref loc isevars env lvar = function make_judge cstr (type_of_existential env !isevars cstr) *) | RInd (ind_sp,ctxt) -> - let ind = (ind_sp,ctxt_of_ids ctxt) in + let ind = (ind_sp,Array.map pretype ctxt) in make_judge (mkMutInd ind) (type_of_inductive env !isevars ind) | RConstruct (cstr_sp,ctxt) -> - let cstr = (cstr_sp,ctxt_of_ids ctxt) in + let cstr = (cstr_sp,Array.map pretype ctxt) in let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind} @@ -266,7 +266,9 @@ let rec pretype vtcon env isevars lvar lmeta cstr = match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | RRef (loc,ref) -> - pretype_ref loc isevars env lvar ref + pretype_ref + (fun c -> (pretype empty_tycon env isevars lvar lmeta c).uj_val) + loc isevars env lvar ref | RMeta (loc,n) -> (try diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 78b87426f..a3382f5cd 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -23,7 +23,7 @@ type rawsort = RProp of Term.contents | RType (*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*) type rawconstr = - | RRef of loc * constr array reference + | RRef of loc * rawconstr array reference | RMeta of loc * int | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 1cff2989f..5fb28fea0 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -21,7 +21,7 @@ type cases_pattern = type rawsort = RProp of Term.contents | RType type rawconstr = - | RRef of loc * constr array reference + | RRef of loc * rawconstr array reference | RMeta of loc * int | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 45a922d7f..49a50b485 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -148,23 +148,45 @@ let explain_actual_type k ctx c ct pt = 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL; 'sTR"Actually, it has type" ; 'bRK(1,1); pct >] -let explain_cant_apply k ctx s rator randl = - let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in - let pr = P.pr_term k ctx rator.uj_val in - let prt = P.pr_term k ctx rator.uj_type in +let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl = + let ctx = make_all_name_different ctx in + let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in + let pr = prterm_env ctx rator.uj_val in + let prt = prterm_env ctx rator.uj_type in + let term_string = if List.length randl > 1 then "terms" else "term" in + let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" 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 + hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl + in + [< 'sTR"Illegal application (Type Error): "; pe; 'fNL; + 'sTR"The term"; 'bRK(1,1); pr; 'sPC; + 'sTR"of type"; 'bRK(1,1); prt; 'sPC ; + 'sTR("cannot be applied to the "^term_string); 'fNL; + 'sTR" "; v 0 appl; 'fNL; + 'sTR"The ";'iNT n; 'sTR (many^" term of type "); + prterm_env ctx actualtyp; + 'sTR" should be of type "; prterm_env ctx exptyp >] + +let explain_cant_apply_not_functional k ctx rator randl = + let ctx = make_all_name_different ctx in + let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in + let pr = prterm_env ctx rator.uj_val in + let prt = prterm_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 = P.pr_term k ctx c.uj_val in - let pct = P.pr_term k ctx c.uj_type in - hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl + 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 + hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in - [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL; + [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL; 'sTR"The term"; 'bRK(1,1); pr; 'sPC; 'sTR"of type"; 'bRK(1,1); prt; 'sPC ; 'sTR("cannot be applied to the "^term_string); 'fNL; - 'sTR" "; v 0 appl >] + 'sTR" "; v 0 appl; 'fNL >] (* (co)fixpoints *) let explain_ill_formed_rec_body k ctx str lna i vdefs = @@ -243,8 +265,10 @@ let explain_type_error k ctx = function explain_generalization k ctx nvar c | ActualType (c, ct, pt) -> explain_actual_type k ctx c ct pt - | CantAply (s, rator, randl) -> - explain_cant_apply k ctx s rator randl + | CantApplyBadType (s, rator, randl) -> + explain_cant_apply_bad_type k ctx n rator randl + | CantApplyNonFunctional (rator, randl) -> + explain_cant_apply_not_functional k ctx rator randl | IllFormedRecBody (i, lna, vdefj, vargs) -> explain_ill_formed_rec_body k ctx i lna vdefj vargs | IllTypedRecBody (i, lna, vdefj, vargs) -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 644616dd2..b824c20ab 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -59,7 +59,7 @@ let msg_bad_elimination ctx k = function [<>] let explain_elim_arity k ctx ind aritylst c p pt okinds = - let pi = pr_inductive ind in + let pi = pr_inductive ctx ind in let ppar = prlist_with_sep pr_coma (prterm_env ctx) aritylst in let pc = prterm_env ctx c in let pp = prterm_env ctx p in @@ -115,24 +115,45 @@ let explain_actual_type k ctx c ct pt = 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL; 'sTR"Actually, it has type" ; 'bRK(1,1); pct >] -let explain_cant_apply k ctx s rator randl = +let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl = let ctx = make_all_name_different ctx in let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in let pr = prterm_env ctx rator.uj_val in let prt = prterm_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 - hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl + let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" 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 + hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in - [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL; + [< 'sTR"Illegal application (Type Error): "; pe; 'fNL; 'sTR"The term"; 'bRK(1,1); pr; 'sPC; 'sTR"of type"; 'bRK(1,1); prt; 'sPC ; 'sTR("cannot be applied to the "^term_string); 'fNL; - 'sTR" "; v 0 appl >] + 'sTR" "; v 0 appl; 'fNL; + 'sTR"The ";'iNT n; 'sTR (many^" term of type "); + prterm_env ctx actualtyp; + 'sTR" should be coercible to type "; prterm_env ctx exptyp >] + +let explain_cant_apply_not_functional k ctx rator randl = + let ctx = make_all_name_different ctx in + let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in + let pr = prterm_env ctx rator.uj_val in + let prt = prterm_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 + hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl + in + [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL; + 'sTR"The term"; 'bRK(1,1); pr; 'sPC; + 'sTR"of type"; 'bRK(1,1); prt; 'sPC ; + 'sTR("cannot be applied to the "^term_string); 'fNL; + 'sTR" "; v 0 appl; 'fNL >] (* (co)fixpoints *) let explain_ill_formed_rec_body k ctx str lna i vdefs = @@ -215,15 +236,15 @@ let explain_var_not_found k ctx id = (* 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 + let pi = pr_inductive ctx ind in + let pc = pr_constructor ctx cstr in + let pt = pr_inductive ctx (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 + let pc = pr_constructor ctx (cstr,[||]) in [<'sTR "The constructor "; pc; 'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">] @@ -264,8 +285,10 @@ let explain_type_error k ctx = function explain_generalization k ctx nvar c | ActualType (c, ct, pt) -> explain_actual_type k ctx c ct pt - | CantAply (s, rator, randl) -> - explain_cant_apply k ctx s rator randl + | CantApplyBadType (t, rator, randl) -> + explain_cant_apply_bad_type k ctx t rator randl + | CantApplyNonFunctional (rator, randl) -> + explain_cant_apply_not_functional k ctx rator randl | IllFormedRecBody (i, lna, vdefj, vargs) -> explain_ill_formed_rec_body k ctx i lna vdefj vargs | IllTypedRecBody (i, lna, vdefj, vargs) -> @@ -390,7 +413,7 @@ let error_not_allowed_case_analysis dep kind i = [< 'sTR (if dep then "Dependent" else "Non Dependent"); 'sTR " case analysis on sort: "; print_sort kind; 'fNL; 'sTR "is not allowed for inductive definition: "; - pr_inductive i >] + pr_inductive (Global.context()) i >] let error_bad_induction dep indid kind = [<'sTR (if dep then "Dependent" else "Non dependend"); |