dp: ajout des prédicats de sortes

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

6 files changed, 133 insertions, 55 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 6b1987b9a..67bed7604 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -104,20 +104,6 @@ let rec eta_expanse t vars env i =
       | _ -> 
 	  assert false
 
-(* assumption : p:Z *)
-let rec fol_term_of_positive p =
-  match kind_of_term p with
-    | Term.Construct _ when p = Lazy.force coq_xH ->
-	Cst 1
-    | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
-	Plus (Mult (Cst 2, (fol_term_of_positive a)), Cst 1)
-    | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
-	Mult (Cst 2, (fol_term_of_positive a))
-    | Var id ->
-	Fol.App (rename_global (VarRef id), [])
-    | _ -> 
-	assert false
-
 (* Coq global references *)
 
 type global = Gnot_fo | Gfo of Fol.hyp
@@ -190,8 +176,22 @@ let rec_names_for c =
        | Anonymous ->
 	   raise Not_found)
 
+(* assumption : p:Z *)
+let rec fol_term_of_positive env p =
+  match kind_of_term p with
+    | Term.Construct _ when p = Lazy.force coq_xH ->
+	Cst 1
+    | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+	Plus (Mult (Cst 2, (fol_term_of_positive env a)), Cst 1)
+    | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+	Mult (Cst 2, (fol_term_of_positive env a))
+    | Var id ->
+	Fol.App (string_of_id id, [])
+    | _ ->
+	tr_term [] env p
+
 (* assumption: t:Set or Type *)
-let rec tr_type env ty =
+and tr_type env ty =
   if ty = Lazy.force coq_Z then [], "INT"
   else if is_Prop ty then [], "BOOLEAN"
   else if is_Set ty then [], "TYPE"
@@ -229,7 +229,13 @@ let rec tr_type env ty =
 		  with NotFO ->
 		    ());
 	     [], id
-	 | _ -> raise NotFO (* constant type definition *)
+	 | _ -> 
+	     let id = rename_global r in
+	     let d = DeclType id in
+	     add_global r (Gfo d);
+	     globals_stack := d :: !globals_stack;
+	     [], id
+	     (* TODO: constant type definition *)
        end)
     with Not_found -> raise NotFO
 
@@ -350,6 +356,11 @@ and axiomatize_body env r id d = match r with
 	    () (* Coq axiom *)
       end
   | IndRef i ->
+      (*iter_all_constructors i
+        (let rc = reference_of_constr c in
+match tr_global c with
+  | DeclVar(idc, l, _) ->
+      (fun _ c -> List.map (fun co -> ) (liste des constructeurs à partir de c non compris));*)
       begin match d with
 	| DeclPred _ ->
 	    iter_all_constructors i
@@ -361,7 +372,7 @@ and axiomatize_body env r id d = match r with
 		     | _ -> assert false
 		   end
 		 with NotFO ->
-		   ())
+		   ());
 	| DeclType _ -> raise NotFO
 	| _ -> assert false
       end
@@ -382,8 +393,7 @@ and equations_for_case env id vars bv ci e br = match kind_of_term e with
 		   let b = substl (List.map mkVar rec_vars) b in
 		   let rec_vars = List.rev rec_vars in
 		   let bv = bv @ rec_vars in
-		   let rec_vars = List.map (fun x -> string_of_id x)
-				    rec_vars in
+		   let rec_vars = List.map string_of_id rec_vars in
 		   let fol_var x =
 		     Fol.App (x, []) in
 		   let fol_rec_vars = List.map fol_var rec_vars in
@@ -432,9 +442,9 @@ and tr_term bv env t =
     | Term.Construct _ when t = Lazy.force coq_Z0 ->
 	Cst 0
     | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
-	fol_term_of_positive a
+	fol_term_of_positive env a
     | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
-	Moins (Cst 0, (fol_term_of_positive a))
+	Moins (Cst 0, (fol_term_of_positive env a))
     | Term.Var id when List.mem id bv ->
 	App (string_of_id id, [])
     | _ ->
@@ -450,6 +460,16 @@ and tr_term bv env t =
 	  raise NotFO
 	end
 
+and quantifiers n a b bv env =
+  let vars, env = coq_rename_vars env [n,a] in
+  let id = match vars with [x] -> x | _ -> assert false in
+  let b = subst1 (mkVar id) b in
+  let t = match tr_type env a with
+    | [], t -> t
+    | _ -> raise NotFO
+  in
+  let bv = id :: bv in
+  id, t, bv, env, b
 
 (* assumption: f is of type Prop *)
 and tr_formula bv env f =
@@ -488,24 +508,13 @@ and tr_formula bv env f =
 	if is_imp_term f then
 	  Imp (tr_formula bv env a, tr_formula bv env b)
 	else
-	  let vars, env = coq_rename_vars env [n,a] in
-	  let id = match vars with [x] -> x | _ -> assert false in
-	  let b = subst1 (mkVar id) b in
-	  let t = match tr_type env a with
-	    | [], t -> t
-	    | _ -> raise NotFO
-	  in
-	  let bv = id :: bv in
+	  let id, t, bv, env, b = quantifiers n a b bv env in
 	  Forall (string_of_id id, t, tr_formula bv env b)
     | _, [_; a] when c = build_coq_ex () ->
 	begin match kind_of_term a with
-	  | Lambda(Name n, ty, t) ->
-	      let id = string_of_id n in
-	      (match tr_type env ty with
-		 | [], ty ->
-		     let t = subst1 (mkVar n) t in
-		     Exists (id, ty, tr_formula (n::bv) env t)
-		 | l, _ -> raise NotFO)
+	  | Lambda(n, a, b) ->
+	      let id, t, bv, env, b = quantifiers n a b bv env in
+	      Exists (string_of_id id, t, tr_formula bv env b)
 	  | _ -> assert false
 		(* a must be a Lambda since we are in the ex case *) end
     | _ ->
@@ -546,10 +555,10 @@ let tr_goal gl =
 type prover = Simplify | CVCLite | Harvey | Zenon
 
 let call_prover prover q = match prover with
-  | Simplify -> Dp_simplify.call q
+  | Simplify -> Dp_simplify.call (Dp_sorts.query q)
   | CVCLite -> Dp_cvcl.call q
   | Harvey -> error "haRVey not yet interfaced"
-  | Zenon -> Dp_zenon.call q
+  | Zenon -> Dp_zenon.call (Dp_sorts.query q)
   
 let dp prover gl =
   let concl_type = pf_type_of gl (pf_concl gl) in
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index 3015b03e0..d5376b8df 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -21,6 +21,7 @@ let rec print_list sep print fmt = function
   | x :: r -> print fmt x; sep fmt (); print_list sep print fmt r
 
 let space fmt () = fprintf fmt "@ "
+let comma fmt () = fprintf fmt ",@ "
 
 let rec print_term fmt = function
   | Cst n -> 
@@ -73,22 +74,27 @@ let rec print_predicate fmt p =
   | Exists (id, _, p) -> 
       fprintf fmt "@[(EXISTS (%a)@ %a)@]" ident id pp p
 
-let rec string_of_type_list  = function
-  | [] -> ""
-  | e :: l' -> e ^ " -> " ^ (string_of_type_list l')
+(**
+let rec string_list l = match l with
+    [] -> ""
+  | [e] -> e
+  | e::l' -> e ^ " " ^ (string_list l')
+**)
 
 let print_query fmt (decls,concl) =
   let print_decl = function
     | DeclVar (id, [], t) ->
-	fprintf fmt "@[;; %s: %s@]@\n" id t
+	fprintf fmt "@[;; %s : %s@]@\n"	id t
     | DeclVar (id, l, t) ->
-	fprintf fmt "@[;; %s: %s%s@]@\n"
-	  id (string_of_type_list l) t
+	fprintf fmt "@[;; %s : %a -> %s@]@\n" 
+	  id (print_list comma pp_print_string) l t
+    | DeclPred (id, []) ->
+	fprintf fmt "@[;; %s : BOOLEAN @]@\n" id
     | DeclPred (id, l) -> 
-	fprintf fmt "@[;; %s: %sBOOLEAN@]@\n"
-	  id (string_of_type_list l)
+	fprintf fmt "@[;; %s : %a -> BOOLEAN@]@\n" 
+	  id (print_list comma pp_print_string) l
     | DeclType id ->
-	fprintf fmt "@[;; %s: TYPE@]@\n" id
+	fprintf fmt "@[;; %s : TYPE@]@\n" id
     | Assert (id, f)  -> 
 	fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
   in
@@ -109,5 +115,3 @@ let call q =
   let out = Sys.command cmd in
   if out = 0 then Valid else if out = 1 then Invalid else Timeout
   (* TODO: effacer le fichier f et le fichier out *)
-
-
diff --git a/contrib/dp/dp_sorts.ml b/contrib/dp/dp_sorts.ml
new file mode 100644
index 000000000..7dbdfa561
--- /dev/null
+++ b/contrib/dp/dp_sorts.ml
@@ -0,0 +1,51 @@
+
+open Fol
+
+let term_has_sort x s = Fatom (Pred ("%sort_" ^ s, [x]))
+
+let has_sort x s = term_has_sort (App (x, [])) s
+
+let rec form = function
+  | True | False | Fatom _ as f -> f
+  | Imp (f1, f2) -> Imp (form f1, form f2)
+  | And (f1, f2) -> And (form f1, form f2)
+  | Or (f1, f2) -> Or (form f1, form f2)
+  | Not f -> Not (form f)
+  | Forall (x, ("INT" as t), f) -> Forall (x, t, form f)
+  | Forall (x, t, f) -> Forall (x, t, Imp (has_sort x t, form f))
+  | Exists (x, ("INT" as t), f) -> Exists (x, t, form f)
+  | Exists (x, t, f) -> Exists (x, t, Imp (has_sort x t, form f))
+
+let sort_ax = let r = ref 0 in fun () -> incr r; "sort_ax_" ^ string_of_int !r
+
+let hyp acc = function
+  | Assert (id, f) -> 
+      (Assert (id, form f)) :: acc
+  | DeclVar (id, _, "INT") as d ->
+      d :: acc
+  | DeclVar (id, [], t) as d -> 
+      (Assert (sort_ax (), has_sort id t)) :: d :: acc
+  | DeclVar (id, l, t) as d -> 
+      let n = ref 0 in
+      let xi = 
+	List.fold_left 
+	  (fun l t -> incr n; ("x" ^ string_of_int !n, t) :: l) [] l
+      in
+      let f =
+	List.fold_left
+	  (fun f (x,t) -> if t = "INT" then f else Imp (has_sort x t, f))
+	  (term_has_sort 
+	     (App (id, List.rev_map (fun (x,_) -> App (x,[])) xi)) t)
+	  xi 
+      in
+      let f = List.fold_left (fun f (x,t) -> Forall (x, t, f)) f xi in
+      (Assert (sort_ax (), f)) :: d :: acc
+  | DeclPred _ as d ->
+      d :: acc
+  | DeclType t as d ->
+      (DeclPred ("%sort_" ^ t, [t])) :: d :: acc
+
+let query (hyps, f) =
+  let hyps' = List.fold_left hyp [] hyps in
+  List.rev hyps', form f
+
diff --git a/contrib/dp/dp_sorts.mli b/contrib/dp/dp_sorts.mli
new file mode 100644
index 000000000..9e74f9973
--- /dev/null
+++ b/contrib/dp/dp_sorts.mli
@@ -0,0 +1,4 @@
+
+open Fol
+
+val query : query -> query
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 074df6722..7adc6f382 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -34,5 +34,5 @@ TACTIC EXTEND admit
 END
 
 VERNAC COMMAND EXTEND Dp_hint 
-  [ "Dp" ne_global_list(l) ] -> [ dp_hint l ]
+  [ "Dp_hint" ne_global_list(l) ] -> [ dp_hint l ]
 END
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index ef6d177cd..99a169d7e 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -52,6 +52,7 @@ Qed.
 
 
 Goal 2*x + 10 = 18 -> x = 4.
+
 simplify.
 Qed.
 
@@ -72,8 +73,6 @@ Qed.
 
 (* No decision procedure can solve this problem 
   Goal forall (x a b : Z), a * x + b = 0 -> x = - b/a.
-  simplify.
-  Qed.
 *)
 
 
@@ -131,10 +130,10 @@ Parameter add : nat -> nat -> nat.
 Axiom add_0 : forall (n : nat), add 0%nat n = n.
 Axiom add_S : forall (n1 n2 : nat), add (S n1) n2 = S (add n1 n2).
 
-Dp add_0.
-Dp add_S.
+Dp_hint add_0.
+Dp_hint add_S.
 
-(* Simplify can't prove this goal before the tiemout 
+(* Simplify can't prove this goal before the timeout 
    unlike zenon *)
 
 Goal forall n : nat, add n 0 = n.
@@ -183,6 +182,17 @@ zenon.
 Qed.
 
 
+(* sorts issues *)
+
+Parameter foo : Set.         
+Parameter f : nat -> foo -> foo -> nat.
+Parameter g : foo -> foo.
+Goal (forall x:foo, f 0 x x = O) -> forall y, f 0 (g y) (g y) = O.
+simplify.      
+Qed.
+
+
+
 (* Anonymous mutually recursive functions : no equations are produced
 
 Definition mrf :=