diff options
author | 1999-09-10 16:11:21 +0000 | |
---|---|---|
committer | 1999-09-10 16:11:21 +0000 | |
commit | 6f79401e9d1a3d632a84b6087c429ee217db0d2a (patch) | |
tree | ead8984175b97a1a82d3905f32bcd9277504f7df /toplevel | |
parent | 3d3d0b85bd18ecfaf54d9645c4789409545d1a8f (diff) |
affichage des erreurs de typage dans minicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@73 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/himsg.ml | 162 | ||||
-rw-r--r-- | toplevel/himsg.mli | 20 | ||||
-rw-r--r-- | toplevel/minicoq.ml | 25 |
3 files changed, 124 insertions, 83 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 220297d7f..6ed2851e3 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -13,39 +13,73 @@ open Reduction module type Printer = sig val pr_term : path_kind -> context -> constr -> std_ppcmds - val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds end module Make = functor (P : Printer) -> struct + let print_decl k sign (s,typ) = + let ptyp = P.pr_term k (gLOB sign) typ.body in + [< 'sPC; print_id s; 'sTR" : "; ptyp >] + + let print_binding k env = function + | Anonymous,ty -> + [< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env ty.body >] + | Name id,ty -> + [< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env ty.body >] + + let sign_it_with f sign e = + snd (sign_it + (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e)) + sign (nil_sign,e)) + + let dbenv_it_with f env e = + snd (dbenv_it + (fun na t (env,e) -> (add_rel (na,t) env, f na t env e)) + env (gLOB(get_globals env),e)) + + let pr_env k env = + let sign_env = + sign_it_with + (fun id t sign pps -> + let pidt = print_decl k sign (id,t) in [< pps ; 'fNL ; pidt >]) + (get_globals env) [< >] + in + let db_env = + dbenv_it_with + (fun na t env pps -> + let pnat = print_binding k env (na,t) in [< pps ; 'fNL ; pnat >]) + env [< >] + in + [< sign_env; db_env >] + + let pr_ne_ctx header k = function + | ENVIRON (([],[]),[]) -> [< >] + | env -> [< header; pr_env k env >] + + let explain_unbound_rel k ctx n = - let pe = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in - errorlabstrm "unbound rel" - [< 'sTR"Unbound reference: "; pe; 'fNL; - 'sTR"The reference "; 'iNT n; 'sTR" is free" >] + let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in + [< 'sTR"Unbound reference: "; pe; 'fNL; + 'sTR"The reference "; 'iNT n; 'sTR" is free" >] let explain_cant_execute k ctx c = let tc = P.pr_term k ctx c in - errorlabstrm "Cannot execute" - [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >] + [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >] let explain_not_type k ctx c = - let pe = P.pr_ne_ctx [< 'sTR"In environment" >] k ctx in + let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in let pc = P.pr_term k ctx c in - errorlabstrm "Not a type" - [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC; - 'sTR"should be typed by Set, Prop or Type." >];; + [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC; + 'sTR"should be typed by Set, Prop or Type." >];; let explain_bad_assumption k ctx c = let pc = P.pr_term k ctx c in - errorlabstrm "Bad assumption" - [< 'sTR "Cannot declare a variable or hypothesis over the term"; - 'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];; + [< 'sTR "Cannot declare a variable or hypothesis over the term"; + 'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];; let explain_reference_variables id = - errorlabstrm "construct_reference" - [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; - 'sTR "refers to variables which are not in the context" >] + [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; + 'sTR "refers to variables which are not in the context" >] let msg_bad_elimination ctx k = function | Some(ki,kp,explanation) -> @@ -56,7 +90,8 @@ let msg_bad_elimination ctx k = function pki; 'bRK(1,0); 'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL; 'sTR "because"; 'sPC; 'sTR explanation >]) - | None -> [<>] + | None -> + [<>] let explain_elim_arity k ctx ind aritylst c p pt okinds = let pi = P.pr_term k ctx ind in @@ -64,63 +99,57 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds = let pc = P.pr_term k ctx c in let pp = P.pr_term k ctx p in let ppt = P.pr_term k ctx pt in - errorlabstrm "incorrect elimimnation arity" - [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC; - 'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL; - 'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC; - 'sTR "has type"; 'bRK(1,1); ppt; 'fNL; - 'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL; - msg_bad_elimination ctx k okinds >] + [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC; + 'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL; + 'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC; + 'sTR "has type"; 'bRK(1,1); ppt; 'fNL; + 'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL; + msg_bad_elimination ctx k okinds >] let explain_case_not_inductive k ctx c ct = let pc = P.pr_term k ctx c in let pct = P.pr_term k ctx ct in - errorlabstrm "Cases on non inductive type" - [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; - 'sTR "has type"; 'bRK(1,1); pct; 'sPC; - 'sTR "which is not an inductive definition" >] - + [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; + 'sTR "has type"; 'bRK(1,1); pct; 'sPC; + 'sTR "which is not an inductive definition" >] + let explain_number_branches k ctx c ct expn = let pc = P.pr_term k ctx c in let pct = P.pr_term k ctx ct in - errorlabstrm "Cases with wrong number of cases" - [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ; - 'sTR "of type"; 'bRK(1,1); pct; 'sPC; - 'sTR "expects "; 'iNT expn; 'sTR " branches" >] + [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ; + 'sTR "of type"; 'bRK(1,1); pct; 'sPC; + 'sTR "expects "; 'iNT expn; 'sTR " branches" >] let explain_ill_formed_branch k ctx c i actty expty = let pc = P.pr_term k ctx c in let pa = P.pr_term k ctx actty in let pe = P.pr_term k ctx expty in - errorlabstrm "Ill-formed branches" - [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc; - 'sPC; 'sTR "the branch " ; 'iNT (i+1); - 'sTR " has type"; 'bRK(1,1); pa ; 'sPC; - 'sTR "which should be:"; 'bRK(1,1); pe >] + [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc; + 'sPC; 'sTR "the branch " ; 'iNT (i+1); + 'sTR " has type"; 'bRK(1,1); pa ; 'sPC; + 'sTR "which should be:"; 'bRK(1,1); pe >] let explain_generalization k ctx (name,var) c = - let pe = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in + let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in let pv = P.pr_term k ctx var.body in let pc = P.pr_term k (add_rel (name,var) ctx) c in - errorlabstrm "P.rel" - [< 'sTR"Illegal generalization: "; pe; 'fNL; - 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC; - 'sTR"over"; 'bRK(1,1); pc; 'sPC; - 'sTR"which should be typed by Set, Prop or Type." >] + [< 'sTR"Illegal generalization: "; pe; 'fNL; + 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC; + 'sTR"over"; 'bRK(1,1); pc; 'sPC; + 'sTR"which should be typed by Set, Prop or Type." >] let explain_actual_type k ctx c ct pt = - let pe = P.pr_ne_ctx [< 'sTR"In environment" >] k ctx in + let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in let pc = P.pr_term k ctx c in let pct = P.pr_term k ctx ct in let pt = P.pr_term k ctx pt in - errorlabstrm "Bad cast" - [< pe; 'fNL; - 'sTR"The term"; 'bRK(1,1); pc ; 'sPC ; - 'sTR"does not have type"; 'bRK(1,1); pt; 'fNL; - 'sTR"Actually, it has type" ; 'bRK(1,1); pct >] + [< pe; 'fNL; + 'sTR"The term"; 'bRK(1,1); pc ; 'sPC ; + '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 = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in + 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 term_string = if List.length randl > 1 then "terms" else "term" in @@ -131,31 +160,28 @@ let explain_cant_apply k ctx s rator randl = let pct = P.pr_term k ctx c.uj_type in hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in - errorlabstrm "Illegal application" - [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; 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"Illegal application ("; 'sTR s; 'sTR"): "; 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 >] (* (co)fixpoints *) let explain_ill_formed_rec_body k ctx str lna i vdefs = let pvd = P.pr_term k ctx vdefs.(i) in - errorlabstrm "Ill-formed rec body" - [< str; 'fNL; 'sTR"The "; - if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">]; - 'sTR"recursive definition"; 'sPC ; pvd; 'sPC; - 'sTR "is not well-formed" >] + [< str; 'fNL; 'sTR"The "; + if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">]; + 'sTR"recursive definition"; 'sPC ; pvd; 'sPC; + 'sTR "is not well-formed" >] let explain_ill_typed_rec_body k ctx i lna vdefj vargs = let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in let pv = P.pr_term k ctx (body_of_type vargs.(i)) in - errorlabstrm "Ill-typed rec body" - [< 'sTR"The " ; - if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">]; - 'sTR"recursive definition" ; 'sPC; pvd; 'sPC; - 'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >] + [< 'sTR"The " ; + if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">]; + 'sTR"recursive definition" ; 'sPC; pvd; 'sPC; + 'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >] let explain_type_error k ctx = function | UnboundRel n -> diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 081e23ebd..5c5548c2a 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -11,15 +11,24 @@ open Type_errors (*i*) (* This module provides functions to explain the various typing errors. - It is parameterized by functions to pretty-print terms and contexts. *) + It is parameterized by a function to pretty-print a term in a given + context. *) module type Printer = sig val pr_term : path_kind -> context -> constr -> std_ppcmds - val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds end +(*s The result is a module which provides a function [explain_type_error] + to explain a type error for a given kind in a given context, which are + usually the three arguments carried by the exception [TypeError] + (see \citesec{typeerrors}). *) + module Make (P : Printer) : sig +val explain_type_error : path_kind -> context -> type_error -> std_ppcmds + +val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds + val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds val explain_cant_execute : path_kind -> context -> constr -> std_ppcmds @@ -28,7 +37,7 @@ val explain_not_type : path_kind -> context -> constr -> std_ppcmds val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds -val explain_reference_variables : identifier -> 'a +val explain_reference_variables : identifier -> std_ppcmds val explain_elim_arity : path_kind -> context -> constr -> constr list -> constr @@ -47,8 +56,7 @@ val explain_generalization : path_kind -> context -> name * typed_type -> constr -> std_ppcmds val explain_actual_type : - path_kind -> context -> constr -> constr -> constr -> - std_ppcmds + path_kind -> context -> constr -> constr -> constr -> std_ppcmds val explain_cant_apply : path_kind -> context -> string -> unsafe_judgment @@ -62,6 +70,4 @@ val explain_ill_typed_rec_body : path_kind -> context -> int -> name list -> unsafe_judgment array -> typed_type array -> std_ppcmds -val explain_type_error : path_kind -> context -> type_error -> std_ppcmds - end diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index a58ce94a6..5e1c3ca58 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -9,6 +9,7 @@ open Term open Sign open Constant open Inductive +open Type_errors open Typing open G_minicoq @@ -44,7 +45,8 @@ let check c = let c = globalize [] c in let (j,u) = safe_machine !env c in let ty = j_type j in - mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 (pr_term ty); 'fNL >]) + let pty = pr_term CCI (context !env) ty in + mSGNL (hOV 0 [< 'sTR" :"; 'sPC; hOV 0 pty; 'fNL >]) let definition id ty c = let c = globalize [] c in @@ -107,19 +109,26 @@ let parse_file f = with | End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0 | exn -> close_in c; raise exn - + +module Explain = Himsg.Make(struct let pr_term = pr_term end) + +let rec explain_exn = function + | TypeError (k,ctx,te) -> + mSGNL (hOV 0 [< 'sTR "type error:"; 'sPC; + Explain.explain_type_error k ctx te; 'fNL >]) + | Stdpp.Exc_located (_,exn) -> + explain_exn exn + | exn -> + mSGNL (hOV 0 [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]) + let top () = let cs = Stream.of_channel stdin in while true do try let c = Grammar.Entry.parse command cs in execute c with - | End_of_file | Stdpp.Exc_located (_, End_of_file) -> - exit 0 - | Stdpp.Exc_located (_,exn) -> - mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >] - | exn -> - mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >] + | End_of_file | Stdpp.Exc_located (_, End_of_file) -> exit 0 + | exn -> explain_exn exn done let main () = |