From 0ac9511b210cecee1d3e99deb509a0466a005ab7 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 24 Jun 2005 12:56:46 +0000 Subject: dp: ajout des prédicats de sortes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7165 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/dp/dp.ml | 85 ++++++++++++++++++++++++++--------------------- contrib/dp/dp_simplify.ml | 26 +++++++++------ contrib/dp/dp_sorts.ml | 51 ++++++++++++++++++++++++++++ contrib/dp/dp_sorts.mli | 4 +++ contrib/dp/g_dp.ml4 | 2 +- contrib/dp/tests.v | 20 ++++++++--- 6 files changed, 133 insertions(+), 55 deletions(-) create mode 100644 contrib/dp/dp_sorts.ml create mode 100644 contrib/dp/dp_sorts.mli (limited to 'contrib') 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 := -- cgit v1.2.3