dp: traitement des fixpoints

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

6 files changed, 348 insertions, 15 deletions

diff --git a/Makefile b/Makefile
index 49ddef7bdf..e4fd4dd164 100644
--- a/Makefile
+++ b/Makefile
@@ -246,7 +246,7 @@ RINGCMO=\
   contrib/ring/ring.cmo contrib/ring/g_ring.cmo 
 
 DPCMO=\
-  contrib/dp/dp_simplify.cmo contrib/dp/dp_zenon.cmo \
+  contrib/dp/dp_simplify.cmo contrib/dp/dp_zenon.cmo contrib/dp/dp_cvcl.cmo \
   contrib/dp/dp.cmo contrib/dp/g_dp.cmo
 
 FIELDCMO=\
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index e6565c380c..ecc9cd6be0 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -175,6 +175,21 @@ let injection c l =
   let ax = Assert ("injection_" ^ c, f) in
   globals_stack := ax :: !globals_stack
 
+(* rec_names_for c [|n1;...;nk|] builds the list of constant names for 
+   identifiers n1...nk with the same path as c, if they exist; otherwise
+   raises Not_found *)
+let rec_names_for c =
+  let mp,dp,_ = Names.repr_con c in
+  array_map_to_list
+    (function 
+       | Name id -> 
+	   let c' = Names.make_con mp dp (label_of_id id) in
+	   ignore (Global.lookup_constant c');
+	   msgnl (Ppconstrnew.pr_term (mkConst c'));
+	   c'
+       | Anonymous ->
+	   raise Not_found)
+
 (* assumption: t:Set or Type *)
 let rec tr_type env ty =
   if ty = Lazy.force coq_Z then [], "INT"
@@ -273,6 +288,22 @@ and axiomatize_body env r id d = match r with
 		     let value = tr_term [] env b in
 		     [id, Fatom (Eq (Fol.App (id, []), value))]
 		 | DeclVar (id, l, _) | DeclPred (id, l) ->
+		     let b = match kind_of_term b with
+		       (* a single recursive function *)
+		       | Fix (_, (_,_,[|b|])) -> 
+			   subst1 (mkConst c) b
+                       (* mutually recursive functions *)
+		       | Fix ((_,i), (names,_,bodies)) ->
+                           (* we only deal with named functions *)
+			   begin try
+			     let l = rec_names_for c names in
+			     substl (List.rev_map mkConst l) bodies.(i)
+			   with Not_found ->
+			     b
+			   end
+		       | _ -> 
+			   b
+		     in
 		     let vars, t = decompose_lam b in
 		     let n = List.length l in
 		     let k = List.length vars in
@@ -288,16 +319,17 @@ and axiomatize_body env r id d = match r with
 		     let fol_vars = List.map fol_var vars in
 		     let vars = List.combine vars l in
 		     begin match d with
-		       | DeclVar _ -> begin match kind_of_term t with
-			   | Case (ci, _, e, br) ->
-			       equations_for_case env id vars bv ci e br
-			   | _ -> 
-			       let p = 
-				 Fatom (Eq (App (id, fol_vars), 
-					    tr_term bv env t)) 
-			       in
-			       [id, foralls vars p]
-			 end
+		       | DeclVar _ ->
+			   begin match kind_of_term t with
+			     | Case (ci, _, e, br) ->
+				 equations_for_case env id vars bv ci e br
+			     | _ -> 
+				 let p = 
+				   Fatom (Eq (App (id, fol_vars), 
+					      tr_term bv env t)) 
+				 in
+				 [id, foralls vars p]
+			   end
 		       | DeclPred _ ->
 			   let value = tr_formula bv env t in
 			   let p = 
diff --git a/contrib/dp/dp_cvcl.ml b/contrib/dp/dp_cvcl.ml
new file mode 100644
index 0000000000..602d122038
--- /dev/null
+++ b/contrib/dp/dp_cvcl.ml
@@ -0,0 +1,107 @@
+
+open Format
+open Fol
+
+let rec print_list sep print fmt = function
+  | [] -> ()
+  | [x] -> print fmt x
+  | 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 -> 
+      fprintf fmt "%d" n
+  | Plus (a, b) ->
+      fprintf fmt "@[(%a@ +@ %a)@]" print_term a print_term b
+  | Moins (a, b) ->
+      fprintf fmt "@[(%a@ -@ %a)@]" print_term a print_term b
+  | Mult (a, b) ->
+      fprintf fmt "@[(%a@ *@ %a)@]" print_term a print_term b
+  | Div (a, b) ->
+      fprintf fmt "@[(%a@ /@ %a)@]" print_term a print_term b
+  | App (id, []) ->
+      fprintf fmt "%s" id
+  | App (id, tl) ->
+      fprintf fmt "@[(%s@(%a))@]" id print_terms tl
+
+and print_terms fmt tl = 
+  print_list comma print_term fmt tl
+
+let rec print_predicate fmt p = 
+  let pp = print_predicate in 
+  match p with
+  | True ->
+      fprintf fmt "TRUE"
+  | False ->
+      fprintf fmt "FALSE"
+  | Fatom (Eq (a, b)) ->
+      fprintf fmt "@[(%a = %a)@]" print_term a print_term b
+  | Fatom (Le (a, b)) ->
+      fprintf fmt "@[(%a@ <= %a)@]" print_term a print_term b
+  | Fatom (Lt (a, b))->
+      fprintf fmt "@[(%a@ < %a)@]" print_term a print_term b
+  | Fatom (Ge (a, b)) ->
+      fprintf fmt "@[(%a@ >= %a)@]" print_term a print_term b
+  | Fatom (Gt (a, b)) ->
+      fprintf fmt "@[(%a@ > %a)@]" print_term a print_term b
+  | Fatom (Pred (id, tl)) -> 
+      fprintf fmt "@[(%s@(%a))@]" id print_terms tl
+  | Imp (a, b) ->
+      fprintf fmt "@[(%a@ => %a)@]" pp a pp b
+  | And (a, b) ->
+      fprintf fmt "@[(%a@ AND@ %a)@]" pp a pp b
+  | Or (a, b) ->
+      fprintf fmt "@[(%a@ OR@ %a)@]" pp a pp b
+  | Not a ->
+      fprintf fmt "@[(NOT@ %a)@]" pp a
+  | Forall (id, t, p) -> 
+      fprintf fmt "@[(FORALL (%s:%s)@ %a)@]" id t pp p
+(*
+  | Exists (id,n,t,p) -> 
+      let id' = next_away id (predicate_vars p) in
+      let p' = subst_in_predicate (subst_onev n id') p in
+      fprintf fmt "@[(EXISTS (%a)@ %a)@]" Ident.print id' pp p'
+*)
+  | Exists _ ->
+      assert false (*TODO*)
+
+let rec string_of_type_list  = function
+  | [] -> ""
+  | e :: l' -> e ^ " -> " ^ (string_of_type_list l')
+
+let print_query fmt (decls,concl) =
+  let print_decl = function
+    | DeclVar (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
+    | DeclPred (id, l) -> 
+	fprintf fmt "@[%s: %sBOOLEAN@]@\n"
+	  id (string_of_type_list l)
+    | DeclType id ->
+	fprintf fmt "@[%s: TYPE@]@\n" id
+    | Assert (id, f)  -> 
+	fprintf fmt "@[ASSERT %s@\n %a@]@\n" id print_predicate f
+  in
+  List.iter print_decl decls;
+  fprintf fmt "PUSH; %a@; POP;" print_predicate concl
+
+let call q = 
+  let f = Filename.temp_file "coq_dp" ".cvc" in
+  let c = open_out f in
+  let fmt = formatter_of_out_channel c in
+  fprintf fmt "@[%a@]@." print_query q;
+  close_out c;
+  ignore (Sys.command (sprintf "cat %s" f));
+  let cmd = 
+    sprintf "timeout 10 cvcl-1.1.0 %s > out 2>&1 && grep -q -w Valid out" f
+  in
+  prerr_endline cmd; flush stderr;
+  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_cvcl.mli b/contrib/dp/dp_cvcl.mli
new file mode 100644
index 0000000000..03b6d3475e
--- /dev/null
+++ b/contrib/dp/dp_cvcl.mli
@@ -0,0 +1,4 @@
+
+open Fol
+
+val call : query -> prover_answer
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index a39facc328..fc0724dc7b 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -2,6 +2,19 @@
 open Format
 open Fol
 
+let is_simplify_ident s =
+  let is_simplify_char = function
+    | 'a'..'z' | 'A'..'Z' | '0'..'9' -> true 
+    | _ -> false
+  in
+  try 
+    String.iter (fun c -> if not (is_simplify_char c) then raise Exit) s; true
+  with Exit ->
+    false
+
+let ident fmt s =
+  if is_simplify_ident s then fprintf fmt "%s" s else fprintf fmt "|%s|" s
+
 let rec print_list sep print fmt = function
   | [] -> ()
   | [x] -> print fmt x
@@ -21,9 +34,9 @@ let rec print_term fmt = function
   | Div (a, b) ->
       fprintf fmt "@[(/@ %a@ %a)@]" print_term a print_term b
   | App (id, []) ->
-      fprintf fmt "%s" id 
+      fprintf fmt "%a" ident id
   | App (id, tl) ->
-      fprintf fmt "@[(%s@ %a)@]" id print_terms tl
+      fprintf fmt "@[(%a@ %a)@]" ident id print_terms tl
 
 and print_terms fmt tl = 
   print_list space print_term fmt tl
@@ -46,7 +59,7 @@ let rec print_predicate fmt p =
   | Fatom (Gt (a, b)) ->
       fprintf fmt "@[(> %a@ %a)@]" print_term a print_term b
   | Fatom (Pred (id, tl)) -> 
-      fprintf fmt "@[(EQ (%s@ %a) |@@true|)@]" id print_terms tl
+      fprintf fmt "@[(EQ (%a@ %a) |@@true|)@]" ident id print_terms tl
   | Imp (a, b) ->
       fprintf fmt "@[(IMPLIES@ %a@ %a)@]" pp a pp b
   | And (a, b) ->
@@ -56,7 +69,7 @@ let rec print_predicate fmt p =
   | Not a ->
       fprintf fmt "@[(NOT@ %a)@]" pp a
   | Forall (id, _, p) -> 
-      fprintf fmt "@[(FORALL (%s)@ %a)@]" id pp p
+      fprintf fmt "@[(FORALL (%a)@ %a)@]" ident id pp p
 (*
   | Exists (id,n,t,p) -> 
       let id' = next_away id (predicate_vars p) in
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
new file mode 100644
index 0000000000..6209d45390
--- /dev/null
+++ b/contrib/dp/tests.v
@@ -0,0 +1,177 @@
+Reset Initial.
+
+Require Import ZArith.
+Require Import Classical.
+
+
+(* Premier exemple avec traduction de l'égalité et du 0 *)
+
+Goal 0 = 0.
+
+simplify.
+Qed.
+
+
+(* Exemples dans le calcul propositionnel *)
+
+Parameter A C : Prop.
+
+Goal A -> A.
+
+simplify.
+Qed.
+
+
+Goal A -> (A \/ C).
+
+zenon.
+Qed.
+
+
+(* Arithmétique de base *)
+
+Parameter x y z : Z.
+
+Goal x = y -> y = z -> x = z.
+
+zenon.
+Qed.
+
+(* Ajoût de quantificateurs universels *)
+
+Goal (forall (x y : Z), x = y) -> 0 = 1.
+
+simplify.
+Qed.
+
+
+(* Définition de fonctions *) 
+
+Definition fst (x y : Z) : Z := x.
+
+Goal forall (g : Z -> Z) (x y : Z), g (fst x y) = g x.
+
+simplify.
+Qed.
+
+(* Exemple d'éta-expansion *)
+
+Definition snd_of_3 (x y z : Z) : Z := y.
+
+Definition f : Z -> Z -> Z := snd_of_3 0.
+
+Goal forall (x y z z1 : Z), snd_of_3 x y z = f y z1.
+
+simplify.
+Qed.
+
+
+(* Définition de types inductifs - appel de la fonction injection *)
+
+Inductive new : Set :=
+| B : new
+| N : new -> new.
+
+Inductive even_p : new -> Prop :=
+| even_p_B : even_p B
+| even_p_N : forall n : new, even_p n -> even_p (N (N n)).
+
+Goal even_p (N (N (N (N B)))).
+
+simplify.
+Qed.
+
+Goal even_p (N (N (N (N B)))).
+
+zenon.
+Qed.
+
+
+(* A noter que simplify ne parvient pas à résoudre ce problème
+   avant le timemout au contraire de zenon *)
+
+Definition skip_z (z : Z) (n : new) := n.
+
+Definition skip_z1 := skip_z.
+
+Goal forall (z : Z) (n : new), skip_z z n = skip_z1 z n.
+
+zenon.
+Qed.
+
+
+(* Définition d'axiomes et ajoût de dp_hint *)
+
+Parameter add : new -> new -> new.
+Axiom add_B : forall (n : new), add B n = n.
+Axiom add_N : forall (n1 n2 : new), add (N n1) n2 = N (add n1 n2).
+
+Dp add_B.
+Dp add_N.
+
+(* Encore un exemple que simplify ne résout pas avant le timeout *)
+
+Goal forall n : new, add n B = n.
+
+induction n ; zenon.
+Qed.
+
+
+Definition newPred (n : new) : new := match n with
+  | B => B
+  | N n' => n'
+end.
+
+Goal forall n : new, n <> B -> newPred (N n) <> B.
+
+zenon.
+Qed.
+
+
+Fixpoint newPlus (n m : new) {struct n} : new :=
+  match n with
+  | B => m
+  | N n' => N (newPlus n' m)
+end.
+
+Goal forall n : new, newPlus n B = n.
+
+induction n; zenon.
+Qed.
+
+
+Definition h (n : new) (z : Z) : Z := match n with
+  | B => z + 1
+  | N n' => z - 1
+end.
+
+
+
+(* mutually recursive functions *)
+
+Fixpoint even (n:nat) : bool := match n with
+  | O => true
+  | S m => odd m
+end
+with odd (n:nat) : bool := match n with
+  | O => false
+  | S m => even m
+end.
+
+Goal even (S (S O)) = true.
+zenon.
+
+(* anonymous mutually recursive functions : no equations are produced *)
+
+Definition f := 
+  fix even (n:nat) : bool := match n with
+  | O => true
+  | S m => odd m
+  end
+  with odd (n:nat) : bool := match n with
+  | O => false
+  | S m => even m
+  end for even.
+
+Goal f (S (S O)) = true.
+zenon.