Subtac: traitement correct des existentielles et de la récursion.

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

6 files changed, 227 insertions, 31 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
new file mode 100644
index 000000000..4f86af1e8
--- /dev/null
+++ b/contrib/subtac/eterm.ml
@@ -0,0 +1,118 @@
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+open Term
+open Names
+open Sutils
+open Evd
+open List
+open Pp
+(** Substitute evar references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_evars evs n t = 
+  let evar_index id = 
+    let idx = list_assoc_index id evs in
+      idx + 1
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Evar (k, args) ->
+	(try 
+	   msgnl (str "Evar " ++ int k ++ str " found");
+	   let ex = 
+(* 	     mkVar (id_of_string ("Evar" ^ string_of_int k));*)
+  	     mkRel (evar_index k + depth)  
+	   in
+	   let args = Array.map (map_constr_with_binders succ substrec depth) args in
+	     mkApp (ex, args)
+	 with Not_found -> 
+	   msgnl (str "Evar " ++ int k ++ str " not found!!!");
+	   c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+      
+(** Substitute variable references in t using De Bruijn indices, 
+  where n binders were passed through. *)
+let subst_vars acc n t = 
+  let var_index id = 
+    let idx = list_index id acc in
+      idx + 1
+  in
+  let rec substrec depth c = match kind_of_term c with
+    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
+    | _ -> map_constr_with_binders succ substrec depth c
+  in 
+    substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+  to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+  Changes evars and hypothesis references to De Bruijn indices.
+*)
+let etype_of_evar evs ev =
+  let rec aux acc n = function
+      (id, copt, t) :: tl ->
+	let t' = subst_evars evs n t in
+	let t'' = subst_vars acc 0 t' in
+ 	  mkNamedProd_or_LetIn (id, copt, t'') (aux (id :: acc) (succ n) tl)
+    | [] ->
+	let t' = subst_evars evs n ev.evar_concl in
+	  subst_vars acc 0 t'	
+  in aux [] 0 (rev ev.evar_hyps)
+
+
+open Tacticals
+    
+let eterm evm t = 
+  (* 'Serialize' the evars, we assume that the types of the existentials
+     refer to previous existentials in the list only *)
+  let evl = to_list evm in
+  let evts = 
+    (* Remove existential variables in types and build the corresponding products *)
+    fold_left 
+      (fun l (id, y) -> 
+	 let y' = (id, etype_of_evar l y) in
+	   y' :: l) 
+      [] evl 
+  in 
+  let t' = (* Substitute evar refs in the term to De Bruijn indices *)
+    subst_evars evts 0 t 
+  in
+  let t'' = 
+    (* Make the lambdas 'generalizing' the existential variables *)
+    fold_left
+      (fun acc (id, c) ->
+	 mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
+		   c, acc))
+      t' evts
+      
+
+  in
+  let declare_evar (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      ignore(Declare.declare_variable id (Names.empty_dirpath, Declare.SectionLocalAssum c,
+					  Decl_kinds.IsAssumption Decl_kinds.Definitional))
+  in
+  let declare_assert acc (id, c) =
+    let id = id_of_string ("Evar" ^ string_of_int id) in
+      tclTHEN acc (Tactics.assert_tac false (Name id) c)
+  in
+    msgnl (str "Term constructed in Eterm" ++
+	   Termops.print_constr_env (Global.env ()) t'');
+   Tactics.apply_term (Reduction.nf_betaiota t'') (map (fun _ -> Evarutil.mk_new_meta ()) evts)
+    (* t'' *)
+    (* Hack: push evars as assumptions in the global env *)
+(*     iter declare_evar evts; *)
+(*     Tactics.apply t' *)
+    (*tclTHEN (fold_left declare_assert tclIDTAC evts) (Tactics.apply t')*)
+       
+open Tacmach
+
+let etermtac (evm, t) = 
+  let t' = eterm evm t in
+    t'
+(*     Tactics.apply (Reduction.nf_betaiota t') 
+    Tactics.exact (Reduction.nf_betaiota t')*)
diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli
new file mode 100644
index 000000000..bcb9b4c56
--- /dev/null
+++ b/contrib/subtac/eterm.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Tacmach
+
+val etermtac : Evd.open_constr -> tactic
diff --git a/contrib/subtac/g_eterm.ml4 b/contrib/subtac/g_eterm.ml4
new file mode 100644
index 000000000..7b4bc31b4
--- /dev/null
+++ b/contrib/subtac/g_eterm.ml4
@@ -0,0 +1,27 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Eterm
+
+TACTIC EXTEND Eterm
+  [ "Eterm" ] -> [ 
+    (fun gl ->
+       let evm = Tacmach.project gl and t = Tacmach.pf_concl gl in
+         Eterm.etermtac (evm, t) gl) ]
+END
diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml
index c2a5141cc..c9a0a78c7 100644
--- a/contrib/subtac/rewrite.ml
+++ b/contrib/subtac/rewrite.ml
@@ -16,6 +16,7 @@ type recursion_info = {
   wf_relation: constr; (* R : A -> A -> Prop *)
   wf_proof: constr; (* : well_founded R *)
   f_type: types; (* f: A -> Set *)
+  f_fulltype: types; (* Type with argument and wf proof product first *)
 }
 
 let id_of_name = function
@@ -86,9 +87,36 @@ let unlift n c =
     else aux (pred n) (Termops.pop acc)
   in aux n c
 
+let filter_defs l = List.filter (fun (_, c, _) -> c = None) l
+
 let evar_args ctx = 
-  let len = List.length ctx in
-    Array.init len (fun i -> mkRel (succ i))
+  let n = List.length ctx in
+  let rec aux acc i = function
+      (_, c, _) :: tl ->
+	(match c with
+	   | None -> aux (mkRel i :: acc) (succ i) tl
+	   | Some _ -> aux acc (succ i) tl)
+    | [] -> acc
+  in Array.of_list (aux [] 1 ctx)
+      
+let evar_ctx prog_info ctx = 
+  let ctx' = 
+    match prog_info.rec_info with
+      Some ri ->
+	let len = List.length ctx in
+	assert(len >= 2);
+	let rec aux l acc = function
+	    0 ->
+	      (match l with
+		   (id, _, recf) :: arg :: [] -> arg :: (id, None, ri.f_fulltype) :: acc
+		 | _ -> assert(false))
+	  | n -> (match l with
+		      hd :: tl -> aux tl (hd :: acc) (pred n)
+		    | _ -> assert(false))
+	in
+	  List.rev (aux ctx [] (len - 2))	    
+    | None -> ctx
+  in filter_defs ctx'
 
 let if_branches c = 
   match kind_of_term c with
@@ -321,7 +349,7 @@ and subset_coerce prog_info ctx x y =
 		let ctx', pcx' = subst_ctx ctx pcx in
 		  cx, {
 		    Evd.evar_concl = pcx';
-		    Evd.evar_hyps = ctx';
+		    Evd.evar_hyps = evar_ctx prog_info ctx';
 		    Evd.evar_body = Evd.Evar_empty;
 		  }
 	      in
@@ -392,13 +420,13 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 			   let evarinfo = 
 			     { 
 			       Evd.evar_concl = proof;
-			       Evd.evar_hyps = ctx';
+			       Evd.evar_hyps = evar_ctx prog_info ctx';
 			       Evd.evar_body = Evd.Evar_empty;
 			     }
 			   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
@@ -410,9 +438,9 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 	    t, t'
 	      
       | DSum ((x, t), (t', u), stype) ->
-	  let ct, ctt = rewrite_term prog_info ctx t in
+	  let ct, ctt = rewrite_term prog_info ctx t in	    
 	  let ctxterm = (snd x, Some ct, ctt) :: ctx in
-	  let ctxtype = (snd x, None, ctt) :: ctx in
+	  let ctxtype = (snd x, Some ct, ctt) :: ctx in
 	  let ct', tt' = rewrite_term prog_info ctxterm t' in
 	  let cu, _ = rewrite_type prog_info ctxtype u in
 	  let coercet' = coerce prog_info ctxtype tt' cu in
@@ -450,10 +478,10 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 	      in aux [] ctx (List.rev l)
 	    in
 	      let ce', et' = aux ctx' e' in
-	      let et' = unlift (pred (List.length l)) 
-		(mkLambda (Anonymous, et, et')) in
+	      let et' = mkLambda (Anonymous, et, 
+				  unlift (pred (List.length l)) et') in
 		debug 1 (str "Let tuple, type of e': " ++
-		       my_print_constr ctx' et');
+			   my_print_constr ctx' et');
 
 	  let ind = destInd (Lazy.force existSind) in
 	  let ci = Inductiveops.make_default_case_info 
@@ -480,7 +508,7 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 	    debug 1 (str "Let tuple term: " ++ my_print_constr ctx lambda);
 	    lambda, et'
 	      
-      | DIfThenElse (b, e, e', t) ->
+      | DIfThenElse (b, e, e', tif) ->
 	  let name = Name (id_of_string "H") in
 	  let (cb, tb) = aux ctx b in
 	    (match if_branches tb with
@@ -498,8 +526,8 @@ and rewrite_term prog_info ctx (t : dterm_loc) : Term.constr * Term.types =
 		   and false_case = 
 		     mkLambda (name, f, ce')
 		   in
-		     (mkCase (ci, lam, cb, [| true_case; false_case |])), 
-		   (Termops.pop te)
+		     (mkCase (ci, lam, cb, [| true_case; false_case |])),
+		       (Termops.pop te)
 	       | None -> failwith ("Ill-typed if"))
 	       
 
@@ -512,22 +540,10 @@ 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,
-	    mkProd(Anonymous,
-		   mkApp (t.wf_relation, [| mkRel 1; mkRel 2 |]),
-		   mkApp (t.f_type, [| mkRel 2 |])))
-  in
-  let term' = 
-    mkLambda (Name id, typ, term)
-  in
-  let fix = 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')
-		   |]) 
-  in fix
+  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') |])       
 
 let subtac recursive id (s, t) =
   check_required_library ["Coq";"Init";"Datatypes"];
@@ -544,6 +560,12 @@ let subtac recursive id (s, t) =
 	    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 fulltype =
+	      mkProd (namen, t'',
+		      mkProd(Anonymous,
+			     mkApp (rel, [| mkRel 1; mkRel 2 |]),
+			     Term.subst1 (mkRel 2) coqt'))
+	    in
 	    let proof = 
 	      match proof with
 		  ManualProof p -> p (* Check that t is a proof of well_founded rel *)
@@ -570,6 +592,7 @@ let subtac recursive id (s, t) =
 		  wf_relation = rel;
 		  wf_proof = proof;
 		  f_type = ftype;
+		  f_fulltype = fulltype;
 		}
 	      in { prog_info with rec_info = Some rec_info }
 	    in
@@ -611,11 +634,12 @@ let subtac recursive id (s, t) =
 	  Some t -> make_fixpoint t id realt
 	| None -> realt
     in
-    trace (str "Term after reduction" ++ my_print_constr coqctx realt);
+    trace (str "Coq term" ++ my_print_constr [] realt);
+    trace (str "Coq type" ++ my_print_constr [] coqtype'');
     let evm = prog_info.evm in
     (try trace (str "Original evar map: " ++ Evd.pr_evar_map evm);
      with Not_found -> trace (str "Not found in pr_evar_map"));
-    let tac = Refine.refine (evm, realt) in 
+    let tac = Eterm.etermtac (evm, realt) in 
     msgnl (str "Starting proof");
     Command.start_proof id goal_kind coqtype'' (fun _ _ -> ());
     msgnl (str "Started proof");
diff --git a/contrib/subtac/sutils.ml b/contrib/subtac/sutils.ml
new file mode 100644
index 000000000..64365b676
--- /dev/null
+++ b/contrib/subtac/sutils.ml
@@ -0,0 +1,11 @@
+let list_index x l =
+  let rec aux i = function
+      y :: tl -> if x = y then i else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
+
+let list_assoc_index x l =
+  let rec aux i = function
+      (y, _) :: tl -> if x = y then i else aux (succ i) tl
+    | [] -> raise Not_found
+  in aux 0 l
diff --git a/contrib/subtac/sutils.mli b/contrib/subtac/sutils.mli
new file mode 100644
index 000000000..00dd00b1c
--- /dev/null
+++ b/contrib/subtac/sutils.mli
@@ -0,0 +1,3 @@
+val list_index : 'a -> 'a list -> int
+val list_assoc_index : 'a -> ('a * 'b) list -> int
+