diff options
-rw-r--r-- | .depend | 16 | ||||
-rw-r--r-- | Makefile | 10 | ||||
-rw-r--r-- | doc/macros.tex | 2 | ||||
-rw-r--r-- | kernel/term.mli | 2 | ||||
-rw-r--r-- | kernel/type_errors.mli | 2 | ||||
-rw-r--r-- | parsing/g_minicoq.ml4 | 3 | ||||
-rw-r--r-- | parsing/g_minicoq.mli | 3 | ||||
-rw-r--r-- | toplevel/himsg.ml | 162 | ||||
-rw-r--r-- | toplevel/himsg.mli | 20 | ||||
-rw-r--r-- | toplevel/minicoq.ml | 25 |
10 files changed, 147 insertions, 98 deletions
@@ -187,15 +187,15 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \ - kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmi \ - kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ - /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/typing.cmi \ - lib/util.cmi + kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmi \ + kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/type_errors.cmi \ + kernel/typing.cmi lib/util.cmi toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \ - kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmx \ - kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ - /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/typing.cmx \ - lib/util.cmx + kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmx \ + kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ + /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/type_errors.cmx \ + kernel/typing.cmx lib/util.cmx parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \ /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \ @@ -10,7 +10,8 @@ noargument: @echo " make cleanall" @echo or make archclean -INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB) +INCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel \ + -I $(CAMLP4LIB) BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG) OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF) @@ -71,7 +72,8 @@ coqtop.byte: $(CMO) # minicoq MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \ - parsing/lexer.cmo parsing/g_minicoq.cmo toplevel/minicoq.cmo + parsing/lexer.cmo parsing/g_minicoq.cmo \ + toplevel/himsg.cmo toplevel/minicoq.cmo minicoq: $(MINICOQCMO) $(OCAMLC) $(INCLUDES) -o minicoq -custom $(CMA) $(MINICOQCMO) \ @@ -89,7 +91,9 @@ doc: doc/coq.tex LPLIB = lib/doc.tex $(LIB:.cmo=.mli) LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli) LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli) -LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) +LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli) +LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \ + $(LPTOPLEVEL) doc/coq.tex: $(LPFILES) ocamlweb -o doc/coq.tex $(LPFILES) diff --git a/doc/macros.tex b/doc/macros.tex index 5a4a2e74d..cfed9a713 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -3,3 +3,5 @@ \newcommand{\Coq}{\textsf{Coq}} \newcommand{\CCI}{Calculus of Inductive Constructions} + +\newcommand{\citesec}[1]{\textbf{\ref{#1}}}
\ No newline at end of file diff --git a/kernel/term.mli b/kernel/term.mli index 6ef98691f..7c1ee1d33 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -45,7 +45,7 @@ val mk_Prop : sorts (*s The type [constr] of the terms of CCI is obtained by instanciating the generic terms (type [term], - see \ref{generic_terms}) on the above operators, themselves instanciated + see \citesec{generic_terms}) on the above operators, themselves instanciated on the above sorts. *) type constr = sorts oper term diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 3a3e1488e..6632c172f 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -9,7 +9,7 @@ open Sign open Environ (*i*) -(* Type errors. *) +(* Type errors. \label{typeerrors} *) type type_error = | UnboundRel of int diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index 1e5b610c6..ae26e3f3c 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -7,6 +7,7 @@ open Names open Univ open Generic open Term +open Sign let lexer = { Token.func = Lexer.func; @@ -170,4 +171,4 @@ let rec pp bv = function | Rel n -> print_rel bv n | _ -> [< 'sTR"<???>" >] -let pr_term = pp [] +let pr_term _ ctx = pp (List.map fst (get_rels ctx)) diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli index 77dbb5c71..289706fdb 100644 --- a/parsing/g_minicoq.mli +++ b/parsing/g_minicoq.mli @@ -2,6 +2,7 @@ open Pp open Names open Term +open Sign val term : constr Grammar.Entry.e @@ -16,4 +17,4 @@ type command = val command : command Grammar.Entry.e -val pr_term : constr -> std_ppcmds +val pr_term : path_kind -> context -> constr -> std_ppcmds 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 () = |