From b15d4e404a516948be88c59ab85b3d34b339161f Mon Sep 17 00:00:00 2001 From: coq Date: Tue, 5 Apr 2005 13:17:46 +0000 Subject: Problemes de renommage regles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6914 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/dp/dp.ml | 75 ++++++++++++++++++++++++++++++++++------------------- contrib/dp/fol.mli | 4 +-- contrib/dp/g_dp.ml4 | 10 +++++++ 3 files changed, 60 insertions(+), 29 deletions(-) diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml index 77a15a5d2..1076a48ba 100644 --- a/contrib/dp/dp.ml +++ b/contrib/dp/dp.ml @@ -12,6 +12,7 @@ open Nameops open Termops open Coqlib open Hipattern +open Libnames let logic_dir = ["Coq";"Logic";"Decidable"] let coq_modules = @@ -44,21 +45,44 @@ exception NotProp (* not first-order expressions *) exception NotFO +(* Renaming of Coq globals *) + +let global_names = Hashtbl.create 97 +let used_names = Hashtbl.create 97 + +let rename_global r = + try + Hashtbl.find global_names r + with Not_found -> + let rec loop id = + if Hashtbl.mem used_names id then + loop (lift_ident id) + else begin + Hashtbl.add used_names id (); + let s = string_of_id id in + Hashtbl.add global_names r s; + s + end + in + loop (Nametab.id_of_global r) + (* assumption: t:Set *) -let rec tr_type env t = - if t = Lazy.force coq_Z then [], "INT" - else if is_Prop t then [], "BOOLEAN" - else if is_Set t then [], "TYPE" - else if is_imp_term t then - begin match match_with_imp_term t with +let rec 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" + else if is_imp_term ty then + begin match match_with_imp_term ty with | Some (t1, t2) -> begin match tr_type env t1, tr_type env t2 with - | ([], t1), (l2, t2) -> t1 :: l2, t2 + | ([], t1'), (l2, t2') -> t1' :: l2, t2' | _ -> raise NotFO end | _ -> assert false end - (* else if then *) - else raise NotFO + else match kind_of_term ty with + | Var id -> [], rename_global (VarRef id) + | Ind i -> [], rename_global (IndRef i) + | _ -> raise NotFO (* assumption : p:Z *) let rec fol_term_of_positive p = @@ -70,7 +94,7 @@ let rec fol_term_of_positive p = | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> Mult (Cst 2, (fol_term_of_positive a)) | Var id -> - Tvar (string_of_id id) + Tvar (rename_global (VarRef id)) | _ -> assert false @@ -87,7 +111,6 @@ let lookup t r = match Hashtbl.find t r with | Gfo d -> d let rec tr_global_type gl id ty = - let id = string_of_id id in if is_Prop ty then DeclPred (id, []) else if is_Set ty then @@ -96,11 +119,12 @@ let rec tr_global_type gl id ty = let s = pf_type_of gl ty in if is_Prop s then Assert (id, tr_formula gl ty) - else if is_Set s then - let l,t = tr_type (pf_env gl) ty in DeclVar (id, l, t) else - (* TODO: traiter les symboles de predicats *) - raise NotFO + let l,t = tr_type (pf_env gl) ty in + if is_Set s then DeclVar (id, l, t) + else if t = "BOOLEAN" then + DeclPred(id, l) + else raise NotFO and tr_global gl = function | Libnames.VarRef id -> @@ -111,7 +135,7 @@ and tr_global gl = function with Not_found -> try let ty = Global.type_of_global r in - let id = Nametab.id_of_global r in + let id = rename_global r in let d = tr_global_type gl id ty in Hashtbl.add globals r (Gfo d); globals_stack := d :: !globals_stack; @@ -120,13 +144,12 @@ and tr_global gl = function Hashtbl.add globals r Gnot_fo; raise NotFO - (* assumption: t:T:Set *) and tr_term gl t = match kind_of_term t with | Var id -> - Tvar (string_of_id id) + Tvar (rename_global (VarRef id)) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> Plus (tr_term gl a, tr_term gl b) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> @@ -135,8 +158,6 @@ and tr_term gl t = Mult (tr_term gl a, tr_term gl b) | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> Div (tr_term gl a, tr_term gl b) - | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> - Div (tr_term gl a, tr_term gl b) | Term.Construct _ when t = Lazy.force coq_Z0 -> Cst 0 | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> @@ -148,7 +169,7 @@ and tr_term gl t = begin try let r = Libnames.reference_of_constr f in match tr_global gl r with - | DeclVar (s, _, _) -> App (s, List.map (tr_term gl) cl) + | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term gl) cl) | _ -> raise NotFO with Not_found -> raise NotFO @@ -159,7 +180,7 @@ and tr_formula gl f = let c, args = decompose_app f in match kind_of_term c, args with | Var id, [] -> - Fvar (string_of_id id) + Fvar (rename_global (VarRef id)) | _, [t;a;b] when c = build_coq_eq () -> (* TODO: verifier type t *) Fatom (Eq (tr_term gl a, tr_term gl b)) @@ -185,9 +206,9 @@ and tr_formula gl f = if is_imp_term f then Imp (tr_formula gl a, tr_formula gl b) else - assert false (*TODO Forall *) + assert false (* TODO Forall *) | _, [a] when c = build_coq_ex () -> - assert false (*TODO Exists (tr_formula gl a)*) + assert false (* TODO Exists (tr_formula gl a) *) | _ -> begin try let r = Libnames.reference_of_constr c in @@ -201,10 +222,10 @@ and tr_formula gl f = let tr_goal gl = Hashtbl.clear locals; - let env = pf_env gl in let tr_one_hyp (id, ty) = try - let d = tr_global_type gl id ty in + let s = rename_global (VarRef id) in + let d = tr_global_type gl s ty in Hashtbl.add locals id (Gfo d); d with NotFO -> @@ -230,7 +251,7 @@ let call_prover prover q = match prover with let dp prover gl = let concl_type = pf_type_of gl (pf_concl gl) in - if not (is_Prop concl_type) then error "Goal is not a Prop"; + if not (is_Prop concl_type) then error "Conclusion is not a Prop"; try let q = tr_goal gl in begin match call_prover prover q with diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli index 42df3d48f..cce593cf4 100644 --- a/contrib/dp/fol.mli +++ b/contrib/dp/fol.mli @@ -31,8 +31,8 @@ and form = | And of form * form | Or of form * form | Not of form - | Forall of form - | Exists of form + | Forall of string * (typ list * typ) * form + | Exists of string * (typ list * typ) * form | True | False diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4 index 6a984dda3..b85775597 100644 --- a/contrib/dp/g_dp.ml4 +++ b/contrib/dp/g_dp.ml4 @@ -16,6 +16,16 @@ TACTIC EXTEND Simplify [ "simplify" ] -> [ simplify ] END +(* +TACTIC EXTEND CVCLite + [ "cvcl" ] -> [ cvc_lite ] +END + +TACTIC EXTEND Harvey + [ "harvey" ] -> [ harvey ] +END +*) + (* should be part of basic tactics syntax *) TACTIC EXTEND admit [ "admit" ] -> [ Tactics.admit_as_an_axiom ] -- cgit v1.2.3