General recursive definitions on well founded orders support

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

5 files changed, 67 insertions, 18 deletions

diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index b9dcb1a89..c2a5141cc 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -398,7 +398,7 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 			   in
 			   let key = mknewexist () in
 			     prog_info.evm <- Evd.add prog_info.evm key evarinfo;
-			     mkApp (cf, [| x; mkEvar(key, evar_args ctx) |])
+			     mkApp (cf, [| x; mkEvar(key, evar_args ctx') |])
 		       | _ -> mkApp (cf, [| x |]))
 		| None -> mkApp (cf, [| x |])
 	  in
@@ -510,8 +510,7 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 
 let global_kind :  Decl_kinds.global_kind = Decl_kinds.IsDefinition
 let goal_kind = Decl_kinds.IsGlobal Decl_kinds.DefinitionBody
-
-
+  
 let make_fixpoint t id term = 
   let typ =
     mkProd (Name t.arg_name, t.arg_type,
@@ -538,19 +537,38 @@ let subtac recursive id (s, t) =
     trace (str "Begin infer_type of given spec");
     let coqtype, coqtype', coqtype'', prog_info, ctx, coqctx =
       match recursive with
-	  Some (n, t) -> 
+	  Some (n, t, rel, proof) -> 
 	    let t' = infer_type [] t in
 	    let namen = Name n in
 	    let coqt = infer_type [namen, t'] s in
 	    let t'', _ = rewrite_type prog_info [] t' in
 	    let coqt', _ = rewrite_type prog_info [namen, None, t''] coqt in
 	    let ftype = mkLambda (namen, t'', coqt') in
+	    let proof = 
+	      match proof with
+		  ManualProof p -> p (* Check that t is a proof of well_founded rel *)
+		| AutoProof ->
+		    (try Lazy.force (Hashtbl.find wf_relations rel)
+		     with Not_found ->
+		       msg_warning
+			 (str "No proof found for relation " 
+			  ++ my_print_constr [] rel);
+		       raise Not_found)
+		| ExistentialProof ->
+		    let wf_rel = mkApp (Lazy.force well_founded, [| t''; rel |]) in
+		    let key = mknewexist () in
+		      prog_info.evm <- Evd.add prog_info.evm key 
+			{ Evd.evar_concl = wf_rel;
+			  Evd.evar_hyps = [];
+			  Evd.evar_body = Evd.Evar_empty };
+		      mkEvar (key, [| |])
+	    in
 	    let prog_info = 
 	      let rec_info = 
 		{ arg_name = n;
 		  arg_type = t'';
-		  wf_relation = Lazy.force lt;
-		  wf_proof = Lazy.force lt_wf;
+		  wf_relation = rel;
+		  wf_proof = proof;
 		  f_type = ftype;
 		}
 	      in { prog_info with rec_info = Some rec_info }
diff --git a/contrib/subtac/rewrite.mli b/contrib/subtac/rewrite.mli
index 3f8bfb136..17660e14a 100644
--- a/contrib/subtac/rewrite.mli
+++ b/contrib/subtac/rewrite.mli
@@ -1,3 +1,3 @@
 val subtac :
-  (Names.identifier * Sast.type_loc) option -> 
+  (Names.identifier * Sast.type_loc * Term.constr * Scoq.wf_proof_type) option -> 
   Names.identifier -> Sast.type_loc * Sast.term_loc -> unit
diff --git a/contrib/subtac/sast.ml b/contrib/subtac/sast.ml
index a447992e0..4d0ca759d 100644
--- a/contrib/subtac/sast.ml
+++ b/contrib/subtac/sast.ml
@@ -3,8 +3,6 @@ open Util
 
 type const = CNat of int | CInt of int | CBool of bool
   
-
-
 type term = 
     SIdent of identifier located
   | SLambda of (identifier located * type_ located) * term located
diff --git a/contrib/subtac/scoq.ml b/contrib/subtac/scoq.ml
index 67547389c..52acb845d 100644
--- a/contrib/subtac/scoq.ml
+++ b/contrib/subtac/scoq.ml
@@ -25,9 +25,7 @@ let existSind = lazy (gen_constant "subtac" ["Init"; "Specif"] "sigS")
 let existS = lazy (build_sigma_set ())
 
 (* orders *)
-let lt = lazy (gen_constant "subtac" ["Init"; "Peano"] "lt")
-let lt_wf = lazy (gen_constant "subtac" ["Arith"; "Wf_nat"] "lt_wf")
-
+let well_founded = lazy (gen_constant "subtac" ["Init"; "Wf"] "well_founded")
 let fix = lazy (gen_constant "subtac" ["Init"; "Wf"] "Fix")
 
 let extconstr = Constrextern.extern_constr true (Global.env ())
@@ -56,3 +54,19 @@ let debug_msg n s =
 let trace s = 
   if !debug_level < 2 then msgnl s
   else ()
+
+let wf_relations = Hashtbl.create 10
+
+let std_relations () = 
+  let add k v = Hashtbl.add wf_relations k v in
+    add (gen_constant "subtac" ["Init"; "Peano"] "lt")
+      (lazy (gen_constant "subtac" ["Arith"; "Wf_nat"] "lt_wf"))
+      
+let std_relations = Lazy.lazy_from_fun std_relations
+
+type wf_proof_type = 
+    AutoProof 
+  | ManualProof of Term.constr 
+  | ExistentialProof
+
+let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4
index b2dffa28f..229c308a4 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/sparser.ml4
@@ -40,6 +40,7 @@ module Subtac =
     (* types *)
     let subtac_spec : type_loc Gram.Entry.e = gec "subtac_spec"
     let subtac_term : term_loc Gram.Entry.e = gec "subtac_term"
+    let subtac_wf_proof_type : Scoq.wf_proof_type Gram.Entry.e = gec "subtac_wf_proof_type"
 
     (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
     (* admissible notation "(x t)" 
@@ -86,7 +87,7 @@ open Coqast
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: subtac_spec subtac_term;
+  GLOBAL: subtac_spec subtac_term subtac_wf_proof_type;
 
   (* Types ******************************************************************)
   subtac_spec: 
@@ -221,11 +222,20 @@ GEXTEND Gram
       ] ]
   ;
 
+  subtac_wf_proof_type:
+    [ [ IDENT "proof"; t = Constr.constr -> 
+	  Scoq.ManualProof (Scoq.constr_of t)
+      | IDENT "auto" -> Scoq.AutoProof
+      | -> Scoq.ExistentialProof
+      ]
+    ]
+  ;
   END
 else (* Developped with Coq 8.0 *) ()
 
 type type_loc_argtype = (type_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 type term_loc_argtype = (term_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type wf_proof_type_argtype = (Scoq.wf_proof_type, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 
 let (wit_subtac_spec : type_loc_argtype),
   (globwit_subtac_spec : type_loc_argtype),
@@ -237,13 +247,22 @@ let (wit_subtac_term : term_loc_argtype),
   (rawwit_subtac_term  : term_loc_argtype) =
   Genarg.create_arg "subtac_term"
 
+let (wit_subtac_wf_proof_type : wf_proof_type_argtype),
+  (globwit_subtac_wf_proof_type : wf_proof_type_argtype),
+  (rawwit_subtac_wf_proof_type : wf_proof_type_argtype) =
+  Genarg.create_arg "subtac_wf_proof_type"
 
 VERNAC COMMAND EXTEND SubtacRec
-    [ "Recursive" "program" ident(id) "(" ident(recid) ":" subtac_spec(rect) ")" ":" subtac_spec(s) ":=" subtac_term(t) ] -> 
-      [ Rewrite.subtac (Some (recid, rect)) id (s, t) ]
+[ "Recursive" "program" ident(id) 
+  "(" ident(recid) ":" subtac_spec(rect) ")" 
+  "using" constr(wf_relation)
+  subtac_wf_proof_type(wf)
+  ":" subtac_spec(s) ":=" subtac_term(t) ] -> 
+  [ Rewrite.subtac (Some (recid, rect, 
+			  Scoq.constr_of wf_relation, wf)) id (s, t) ]
 END
-
+  
 VERNAC COMMAND EXTEND Subtac
-  [ "Program" ident(id) ":" subtac_spec(s) ":=" subtac_term(t) ] -> 
-    [ Rewrite.subtac None id (s, t) ]
+[ "Program" ident(id) ":" subtac_spec(s) ":=" subtac_term(t) ] -> 
+[ Rewrite.subtac None id (s, t) ]
 END