Work with binder lists, problem of tycons

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

5 files changed, 129 insertions, 57 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 3574cfeae8..99727e5f25 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -43,6 +43,7 @@ let subst_evars evs n t =
 (* 	     mkVar (id_of_string ("Evar" ^ string_of_int k));*)
   	     mkRel (evar_index k + depth)  
 	   in
+	     (* Evar arguments are created in inverse order *)
 	   let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in
 	     mkApp (ex, Array.of_list args)
 	 with Not_found -> 
diff --git a/contrib/subtac/interp.ml b/contrib/subtac/interp.ml
index 3b638df021..3de0615aa6 100644
--- a/contrib/subtac/interp.ml
+++ b/contrib/subtac/interp.ml
@@ -40,7 +40,7 @@ open Context
 open Eterm
 
 type recursion_info = {
-  arg_name: identifier;
+  arg_name: name;
   arg_type: types; (* A *)
   wf_relation: constr; (* R : A -> A -> Prop *)
   wf_proof: constr; (* : well_founded R *)
@@ -475,8 +475,9 @@ and pretype_type valcon env isevars lvar = function
 	| Some v ->
 	    if e_cumul env isevars v tj.utj_val then tj
 	    else
-	      error_unexpected_type_loc
-                (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+	      (debug 2 (str "here we are");
+	       error_unexpected_type_loc
+                 (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v)
 
 
 type typing_constraint = OfType of types option | IsType
@@ -580,84 +581,112 @@ let make_fixpoint t id term =
   let term' = mkLambda (Name id, t.f_fulltype, term) in
     mkApp (Lazy.force fix, 
 	   [| t.arg_type; t.wf_relation; t.wf_proof; t.f_type; 
-	      mkLambda (Name t.arg_name, t.arg_type, term') |])       
+	      mkLambda (t.arg_name, t.arg_type, term') |])       
 
 let merge_evms x y = 
   Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y
 
-let interp env isevars c = 
-  let j = pretype empty_tycon env isevars ([],[]) c in
+let interp env isevars c tycon = 
+  let j = pretype tycon env isevars ([],[]) c in
     j.uj_val, j.uj_type
 
-let subtac' recursive id env (s, t) =
+let find_with_index x l =
+  let rec aux i = function
+      (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+let subtac' recursive id l env (s, t) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
   try
     let evd = ref (create_evar_defs Evd.empty) in
     let nonimplicit = ref Gset.empty in
-    let coqintern evd = Constrintern.intern_constr (evars_of evd) env in
-    let coqinterp evd = Constrintern.interp_constr (evars_of evd) env in
-    let s, t = coqintern !evd s, coqintern !evd t in
+    let coqintern evd env = Constrintern.intern_constr (evars_of evd) env in
+    let coqinterp evd env = Constrintern.interp_constr (evars_of evd) env in
+    let rec env_with_binders ((env, rels) as acc) = function
+	Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
+	  let rawdef = coqintern !evd env def in
+	  let coqdef, deftyp = interp env evd rawdef empty_tycon in
+	  let reldecl = (name, Some coqdef, deftyp) in
+	    env_with_binders (push_rel reldecl env, reldecl :: rels) tl
+      | Topconstr.LocalRawAssum (bl, typ) :: tl ->
+	  let rawtyp = coqintern !evd env typ in
+	  let coqtyp, typtyp = interp env evd rawtyp empty_tycon in
+	  let acc = 
+	    List.fold_left (fun (env, rels) (loc, name) -> 
+			      let reldecl = (name, None, coqtyp) in
+				(push_rel reldecl env, 
+				 reldecl :: rels))
+	      (env, rels) bl
+	  in
+	    env_with_binders acc tl
+      | [] -> acc
+    in
+    trace (str "Creating env with binders");
+    let env', binders_rel = env_with_binders (env, []) l in
+    trace (str "New env created:" ++ my_print_context env');
+    let s, t = coqintern !evd env' s, coqintern !evd env' t in
     trace (str "Begin infer_type of given spec");
-    let coqtype, rec_info, ctx =
+    let coqtype, rec_info, env' =
       match recursive with
-	  Some (n, t, rel, proof) -> 
-	    let coqrel = coqinterp !evd rel in
-	    let t', ttyp = interp env evd (coqintern !evd t) in
-	    let namen = Name n in
-	    let coqs, styp = interp (push_rel (namen, None, t') env) evd s in
-	    let ftype = mkProd (namen, t', coqs) in
+	  Some (StructRec id) ->
+	    assert(false)
+	| Some (WfRec (rel, (loc, n))) ->
+	    let coqrel = coqinterp !evd env rel in
+	    let coqs, styp = interp env' evd s empty_tycon in
+	    let index, (_, _, ntype) = find_with_index n (rel_context env') in
+	    let ntype = lift index ntype in
+	    let argtype = 
+	      mkApp ((Lazy.force sig_).intro, 
+		     [| ntype;
+			mkLambda (n, ntype, 
+				  mkApp (coqrel, [| mkRel 1; mkRel (index + 2)|])) |])
+	    in
+	    let ftype = mkProd (n, argtype, lift 1 coqs) in
 	    let fulltype =
-	      mkProd (namen, t',
+	      mkProd (n, argtype,
 		      mkProd(Anonymous,
 			     mkApp (coqrel, [| mkRel 1; mkRel 2 |]),
 			     Term.subst1 (mkRel 2) coqs))
 	    in
 	    let proof = 
-	      match proof with
-		  ManualProof p -> (* TODO: Check that t is a proof of well_founded rel *)
-		    coqinterp !evd p
-		| AutoProof ->
-		    (try Lazy.force (Hashtbl.find wf_relations coqrel)
-		     with Not_found ->
-		       msg_warning
-			 (str "No proof found for relation " 
-			  ++ my_print_constr env coqrel);
-		       raise Not_found)
-		| ExistentialProof ->
-		    let wf_rel = mkApp (Lazy.force well_founded, [| t'; coqrel |]) in
-		      make_existential dummy_loc env nonimplicit evd wf_rel
+	      let wf_rel = mkApp (Lazy.force well_founded, [| ntype; coqrel |]) in
+		make_existential dummy_loc env nonimplicit evd wf_rel (* TODO use env before rec arg *)
 	    in
 	    let rec_info = 
 	      { arg_name = n;
-		arg_type = t';
+		arg_type = ntype;
 		wf_relation = coqrel;
 		wf_proof = proof;
 		f_type = ftype;
 		f_fulltype = fulltype;
 	      }
 	    in 
-	    let coqctx = push_rel (namen, None, t') (push_rel (Name id, None, ftype) env) in 
-	      coqs, Some rec_info, coqctx
+	    let env' = push_rel (Name id, None, ftype) env' in 
+	      coqs, Some rec_info, env'
 	| None ->
-	    let coqs, _ = interp env evd s in
-	      coqs, None, env
+	    let coqs, _ = interp env' evd s empty_tycon in
+	      coqs, None, env'
     in
-    trace (str "Interpreted type: " ++ my_print_constr env coqtype);
-    let coqt, ttyp = interp env evd t in
-    trace (str "Interpreted term: " ++ my_print_constr env coqt ++ spc () ++
-	   str "Infered type: " ++ my_print_constr env ttyp);
-    let coercespec = Subtac_coercion.coerce dummy_loc env nonimplicit evd ttyp coqtype in
+    trace (str "Interpreted type: " ++ my_print_constr env' coqtype);
+    let coqt, ttyp = interp env' evd t empty_tycon in
+    trace (str "Interpreted term: " ++ my_print_constr env' coqt ++ spc () ++
+	   str "Infered type: " ++ my_print_constr env' ttyp);
+    let coercespec = Subtac_coercion.coerce dummy_loc env' nonimplicit evd ttyp coqtype in
     trace (str "Specs coercion successfull");
     let realt = app_opt coercespec coqt in
-    trace (str "Term Specs coercion successfull: " ++ my_print_constr env realt);
+    trace (str "Term Specs coercion successfull: " ++ my_print_constr env' realt);
     let realt = 
       match rec_info with
 	  Some t -> make_fixpoint t id realt
 	| None -> realt
     in
-      (try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !evd));
-       with Not_found -> trace (str "Not found in pr_evar_map"));
+    (try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !evd));
+     with Not_found -> trace (str "Not found in pr_evar_map"));
+    let realt = it_mkLambda_or_LetIn realt binders_rel and
+      coqtype = it_mkProd_or_LetIn coqtype binders_rel
+    in
     let realt = Evarutil.nf_evar (evars_of !evd) realt in
     let coqtype = Evarutil.nf_evar (evars_of !evd) coqtype in
     trace (str "Coq term: " ++ my_print_constr env realt ++ spc ()
@@ -710,9 +739,19 @@ let subtac' recursive id env (s, t) =
     | Pretype_errors.PretypeError (env, e) ->
 	debug 2 (Himsg.explain_pretype_error env e)
 	  
+    | Stdpp.Exc_located (loc, e) ->
+	debug 2 (str "Parsing exception: ");
+	(match e with
+	   | Type_errors.TypeError (env, e) ->
+	       debug 2 (Himsg.explain_type_error env e)
+		 
+	   | Pretype_errors.PretypeError (env, e) ->
+	       debug 2 (Himsg.explain_pretype_error env e)
+	   | e -> raise e)
+  
     | e -> 
-	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e));
-	raise e
+	msg_warning (str "Uncatched exception: " ++ str (Printexc.to_string e))
+	
 
-let subtac recursive id env (s, t) =
-  subtac' recursive id (Global.env ()) (s, t)
+let subtac recursive id l env (s, t) =
+  subtac' recursive id l (Global.env ()) (s, t)
diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml
index 3e8bec6242..799e8e6802 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/scoq.ml
@@ -3,6 +3,7 @@ open Libnames
 open Coqlib
 open Term
 open Names
+open Util
 
 let init_constant dir s = gen_constant "Subtac" dir s
 
@@ -74,6 +75,12 @@ type wf_proof_type =
   | ManualProof of Topconstr.constr_expr
   | ExistentialProof
 
+type recursion_order =
+  | StructRec of name located
+  | WfRec of Topconstr.constr_expr * name located
+
+type binders = Topconstr.local_binder list
+
 let app_opt c e = 
   match c with
       Some constr -> constr e
@@ -112,3 +119,4 @@ let non_instanciated_map env nonimplicit evd =
 	       debug 2 (str " and is an implicit");
 	       Pretype_errors.error_unsolvable_implicit loc env evm k)
       Evd.empty (Evarutil.non_instantiated evm)
+
diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4
index 38ef0a7aaa..987ab04888 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/sparser.ml4
@@ -31,12 +31,15 @@ open Topconstr
 module Gram = Pcoq.Gram
 module Constr = Pcoq.Constr
 module Tactic = Pcoq.Tactic
+module Prim = Pcoq.Prim
 
 module Subtac =
   struct
     let gec s = Gram.Entry.create ("Subtac."^s)
     (* types *)
     let subtac_wf_proof_type : Scoq.wf_proof_type Gram.Entry.e = gec "subtac_wf_proof_type"
+    let subtac_binders : Scoq.binders Gram.Entry.e = gec "subtac_binders"
+    let subtac_fixannot : Scoq.recursion_order option Gram.Entry.e = gec "subtac_fixannot"
 
     (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
     (* admissible notation "(x t)" 
@@ -81,7 +84,7 @@ open Subtac
 open Util
 
 GEXTEND Gram
-  GLOBAL: subtac_wf_proof_type;
+  GLOBAL: subtac_wf_proof_type subtac_binders subtac_fixannot;
  
   subtac_wf_proof_type:
     [ [ IDENT "proof"; t = Constr.constr -> 
@@ -90,6 +93,15 @@ GEXTEND Gram
       | -> Scoq.ExistentialProof
       ]
     ]
+    ;
+  
+  subtac_fixannot:
+    [ [ "{"; IDENT "struct"; id=Prim.name; "}" -> Some (Scoq.StructRec id)
+      | "{"; IDENT "wf"; rel= Constr.constr; id=Prim.name; "}" -> Some (Scoq.WfRec (rel, id))
+      | -> None ] ]
+  ;
+
+  subtac_binders: [ [ bl = LIST0 Constr.binder_let -> bl ] ]
   ;
   END
 
@@ -100,16 +112,27 @@ let (wit_subtac_wf_proof_type : wf_proof_type_argtype),
   (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) =
   Genarg.create_arg "subtac_wf_proof_type"
 
+type subtac_binders_argtype = (Scoq.binders, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+
+let (wit_subtac_binders : subtac_binders_argtype),
+  (globwit_subtac_binders : subtac_binders_argtype),
+  (rawwit_subtac_binders : subtac_binders_argtype) =
+  Genarg.create_arg "subtac_binders"
+
+type subtac_fixannot_argtype = (Scoq.recursion_order, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+
+let (wit_subtac_fixannot : subtac_fixannot_argtype),
+  (globwit_subtac_fixannot : subtac_fixannot_argtype),
+  (rawwit_subtac_fixannot : subtac_fixannot_argtype) =
+  Genarg.create_arg "subtac_fixannot"
+
 VERNAC COMMAND EXTEND SubtacRec
-[ "Recursive" "program" ident(id) 
-  "(" ident(recid) ":" constr(rect) ")" 
-  "using" constr(wf_relation)
-    subtac_wf_proof_type(wf)
-  ":" constr(s) ":=" constr(t) ] -> 
-  [ Interp.subtac (Some (recid, rect, wf_relation, wf)) id Environ.empty_env (s, t) ]
+[ "Recursive" "program" ident(id) subtac_binders(l) subtac_fixannot(f)
+    ":" lconstr(s) ":=" lconstr(t) ] -> 
+  [ Interp.subtac (Some f) id l Environ.empty_env (s, t) ]
 END
   
 VERNAC COMMAND EXTEND Subtac
-[ "Program" ident(id) ":" operconstr(s) ":=" constr(t) ] -> 
-  [ Interp.subtac None id Environ.empty_env (s, t) ]
+[ "Program" ident(id) subtac_binders(l) ":" lconstr(s) ":=" lconstr(t) ] -> 
+  [ Interp.subtac None id l Environ.empty_env (s, t) ]
 END
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 513842150c..d65e95a5d5 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -359,6 +359,7 @@ let inh_conv_coerce_to loc env nonimplicit isevars cj t =
 	coerce_itf loc env nonimplicit isevars cj t
       with NoCoercion ->
 	let sigma = evars_of isevars in
+	  debug 2 (str "No coercion found");
 	  error_actual_type_loc loc env sigma cj t
   in
   (evd',{ uj_val = cj'.uj_val; uj_type = t })