From ba18968685be05d370bb0a82fc3f5e403cdced9f Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 21 Jul 2000 17:31:35 +0000 Subject: retablissement minicoq (pour Jacek) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.ml | 3 --- kernel/safe_typing.mli | 14 ++++---------- parsing/g_minicoq.ml4 | 3 ++- toplevel/fhimsg.ml | 45 ++++++++++++++++++++++++--------------------- toplevel/fhimsg.mli | 6 ------ toplevel/minicoq.ml | 7 ++++++- 6 files changed, 36 insertions(+), 42 deletions(-) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 48692008c..d4b610a8e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -463,6 +463,3 @@ let import = import let env_of_safe_env e = e -(*s Machines with information. *) - -type information = Logic | Inf of unsafe_judgment diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4ed912d4c..5f6b9b073 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -53,16 +53,17 @@ val import : compiled_env -> safe_environment -> safe_environment val env_of_safe_env : safe_environment -> env -(*i For debug -(*s Typing without information. *) + +(*s Typing judgments (only used in minicoq). *) + type judgment val j_val : judgment -> constr val j_type : judgment -> constr val safe_machine : safe_environment -> constr -> judgment * constraints -val safe_machine_type : safe_environment -> constr -> typed_type * constraints +(*i For debug val fix_machine : safe_environment -> constr -> judgment * constraints val fix_machine_type : safe_environment -> constr -> typed_type * constraints @@ -71,14 +72,7 @@ val unsafe_machine_type : safe_environment -> constr -> typed_type * constraints val type_of : safe_environment -> constr -> constr -(*i obsolète val type_of_type : safe_environment -> constr -> constr val unsafe_type_of : safe_environment -> constr -> constr i*) - -(*s Typing with information (extraction). *) - -type information = Logic | Inf of judgment -i*) - diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4 index bf75cdd38..c14c5d034 100644 --- a/parsing/g_minicoq.ml4 +++ b/parsing/g_minicoq.ml4 @@ -176,4 +176,5 @@ let rec pp bv = function | Rel n -> print_rel bv n | _ -> [< 'sTR"" >] -let pr_term _ ctx = pp (List.map fst (get_rels ctx)) +let pr_term _ ctx = pp (it_dbenv (fun l n _ -> n::l) [] ctx) + diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml index 486962748..dcc0a8697 100644 --- a/toplevel/fhimsg.ml +++ b/toplevel/fhimsg.ml @@ -10,6 +10,7 @@ open Sign open Environ open Type_errors open Reduction +open G_minicoq module type Printer = sig val pr_term : path_kind -> context -> constr -> std_ppcmds @@ -18,14 +19,14 @@ 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 + let ptyp = P.pr_term k (gLOB sign) (body_of_type typ) 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 >] + [< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env (body_of_type ty) >] | Name id,ty -> - [< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env ty.body >] + [< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env (body_of_type ty) >] let sign_it_with f sign e = snd (sign_it @@ -127,7 +128,7 @@ let explain_ill_formed_branch k ctx c i actty expty = let explain_generalization k ctx (name,var) c = let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in - let pv = P.pr_term k ctx var.body in + let pv = P.pr_term k ctx (body_of_type var) in let pc = P.pr_term k (add_rel (name,var) ctx) c in [< 'sTR"Illegal generalization: "; pe; 'fNL; 'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC; @@ -146,15 +147,15 @@ let explain_actual_type k ctx c ct pt = 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 pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in + let pr = pr_term k ctx rator.uj_val in + let prt = pr_term k ctx (body_of_type 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 + let pc = pr_term k ctx c.uj_val in + let pct = pr_term k ctx (body_of_type c.uj_type) in hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in [< 'sTR"Illegal application (Type Error): "; pe; 'fNL; @@ -163,19 +164,19 @@ let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl = '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 >] + pr_term k ctx actualtyp; + 'sTR" should be of type "; pr_term k 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 pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in + let pr = pr_term k ctx rator.uj_val in + let prt = pr_term k ctx (body_of_type 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 + let pc = pr_term k ctx c.uj_val in + let pct = pr_term k ctx (body_of_type c.uj_type) in hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl in [< 'sTR"Illegal application (Non-functional construction): "; pe; 'fNL; @@ -197,7 +198,7 @@ let explain_ill_formed_rec_body k ctx str lna i vdefs = 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 pvdt = P.pr_term k ctx (body_of_type (vdefj.(i)).uj_type) in let pv = P.pr_term k ctx (body_of_type vargs.(i)) in [< 'sTR"The " ; if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">]; @@ -242,13 +243,13 @@ let explain_type_error k ctx = function | UnboundRel n -> explain_unbound_rel k ctx n | NotAType c -> - explain_not_type k ctx c + explain_not_type k ctx c.uj_val | BadAssumption c -> explain_bad_assumption k ctx c | ReferenceVariables id -> explain_reference_variables id | ElimArity (ind, aritylst, c, p, pt, okinds) -> - explain_elim_arity k ctx ind aritylst c p pt okinds + explain_elim_arity k ctx (mkMutInd ind) aritylst c p pt okinds | CaseNotInductive (c, ct) -> explain_case_not_inductive k ctx c ct | NumberBranches (c, ct, n) -> @@ -256,11 +257,11 @@ let explain_type_error k ctx = function | IllFormedBranch (c, i, actty, expty) -> explain_ill_formed_branch k ctx c i actty expty | Generalization (nvar, c) -> - explain_generalization k ctx nvar c + explain_generalization k ctx nvar c.uj_val | ActualType (c, ct, pt) -> explain_actual_type k ctx c ct pt | CantApplyBadType (s, rator, randl) -> - explain_cant_apply_bad_type k ctx n rator randl + explain_cant_apply_bad_type k ctx s rator randl | CantApplyNonFunctional (rator, randl) -> explain_cant_apply_not_functional k ctx rator randl | IllFormedRecBody (i, lna, vdefj, vargs) -> @@ -271,6 +272,8 @@ let explain_type_error k ctx = function explain_not_inductive k ctx c | MLCase (mes,c,ct,br,brt) -> explain_ml_case k ctx mes c ct br brt + | _ -> + [< 'sTR "Unknown type error (TODO)" >] let explain_refiner_bad_type k ctx arg ty conclty = errorlabstrm "Logic.conv_leq_goal" diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli index ff3eac8ee..eb8d61553 100644 --- a/toplevel/fhimsg.mli +++ b/toplevel/fhimsg.mli @@ -31,8 +31,6 @@ 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 - val explain_not_type : path_kind -> context -> constr -> std_ppcmds val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds @@ -58,10 +56,6 @@ val explain_generalization : val explain_actual_type : path_kind -> context -> constr -> constr -> constr -> std_ppcmds -val explain_cant_apply : - path_kind -> context -> string -> unsafe_judgment - -> unsafe_judgment list -> std_ppcmds - val explain_ill_formed_rec_body : path_kind -> context -> std_ppcmds -> name list -> int -> constr array -> std_ppcmds diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 7df256f19..59253eb07 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -69,6 +69,11 @@ let variable id t = mSGNL (hOV 0 [< 'sTR"variable"; 'sPC; print_id id; 'sPC; 'sTR"is declared"; 'fNL >]) +let put_DLAMSV lna lc = + match lna with + | [] -> anomaly "put_DLAM" + | na::lrest -> List.fold_left (fun c na -> DLAM(na,c)) (DLAMV(na,lc)) lrest + let inductive par inds = let nparams = List.length par in let bvpar = List.rev (List.map (fun (id,_) -> Name id) par) in @@ -79,7 +84,7 @@ let inductive par inds = let cv = Array.of_list (List.map snd cl) in let cv = Array.map (fun c -> prod_it (globalize bv c) par) cv in let c = put_DLAMSV name_inds cv in - (id, prod_it (globalize bvpar ar) par, List.map fst cl, c) + (id, prod_it (globalize bvpar ar) par, List.map fst cl, [c]) in let inds = List.map one_inductive inds in let mie = { -- cgit v1.2.3