retablissement minicoq (pour Jacek)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7

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 = {