aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/dp')
-rw-r--r--contrib/dp/dp.ml232
-rw-r--r--contrib/dp/dp.mli6
-rw-r--r--contrib/dp/dp_simplify.ml10
-rw-r--r--contrib/dp/fol.mli1
-rw-r--r--contrib/dp/g_dp.ml46
5 files changed, 182 insertions, 73 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 961dd1c4c..24744e768 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -6,6 +6,8 @@ open Util
open Pp
open Term
open Tacmach
+open Tactics
+open Tacticals
open Fol
open Names
open Nameops
@@ -70,6 +72,10 @@ let rename_global r =
let foralls =
List.fold_right (fun (x,t) p -> Forall (rename_global (VarRef x), t, p))
+let fresh_var = function
+ | Anonymous -> rename_global (VarRef (id_of_string "x"))
+ | Name x -> rename_global (VarRef x)
+
(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
env names, and returns the new variables together with the new
environment *)
@@ -82,23 +88,20 @@ let coq_rename_vars env vars =
id :: newvars, Environ.push_named (id, None, t) newenv)
vars ([],env)
-(* assumption: t:Set *)
-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'
- | _ -> raise NotFO
- end
- | _ -> assert false
- end
- else match kind_of_term ty with
- | Var id -> [], rename_global (VarRef id)
- | Ind i -> [], rename_global (IndRef i)
- | _ -> raise NotFO
+let rec eta_expanse t vars env i =
+ assert (i >= 0);
+ if i = 0 then
+ t, vars, env
+ else
+ match kind_of_term (Typing.type_of env Evd.empty t) with
+ | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
+ let avoid = ids_of_named_context (Environ.named_context env) in
+ let id = next_name_away n avoid in
+ let env' = Environ.push_named (id, None, a) env in
+ let t' = mkApp (t, [| mkVar id |]) in
+ eta_expanse t' (id :: vars) env' (pred i)
+ | _ ->
+ assert false
(* assumption : p:Z *)
let rec fol_term_of_positive p =
@@ -110,7 +113,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 (rename_global (VarRef id))
+ Fol.App (rename_global (VarRef id), [])
| _ ->
assert false
@@ -118,15 +121,74 @@ let rec fol_term_of_positive p =
type global = Gnot_fo | Gfo of Fol.hyp
-let globals = Hashtbl.create 97
+let globals = ref Refmap.empty
let globals_stack = ref []
+
+(* synchronization *)
+let () =
+ Summary.declare_summary "Dp globals"
+ { Summary.freeze_function = (fun () -> !globals, !globals_stack);
+ Summary.unfreeze_function =
+ (fun (g,s) -> globals := g; globals_stack := s);
+ Summary.init_function = (fun () -> ());
+ Summary.survive_module = false;
+ Summary.survive_section = false }
+
+let add_global r d = globals := Refmap.add r d !globals
+let mem_global r = Refmap.mem r !globals
+let lookup_global r = match Refmap.find r !globals with
+ | Gnot_fo -> raise NotFO
+ | Gfo d -> d
+
let locals = Hashtbl.create 97
-let lookup t r = match Hashtbl.find t r with
+let lookup_local r = match Hashtbl.find locals r with
| Gnot_fo -> raise NotFO
| Gfo d -> d
-let rec tr_global_type env id ty =
+(* assumption: t:Set *)
+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'
+ | _ -> raise NotFO
+ end
+ | _ -> assert false
+ end
+ else let r = reference_of_constr ty in
+ try
+ begin match lookup_global r with
+ | DeclType id -> [], id
+ | _ -> assert false (* ty is a type for sure ? *)
+ end
+ with Not_found ->
+ let id = rename_global r in
+ let d = DeclType id in
+ add_global r (Gfo d);
+ globals_stack := d :: !globals_stack;
+ [], id
+ (*begin match r with
+ | IndRef i ->
+ let _, oib = Global.lookup_inductive i in
+ let construct_types = oib.mind_nf_lc in
+ let rec axiomatize_all_constr l =
+ begin match l with
+ | [] -> ()
+ | r::l' ->
+ axiomatize_body env r (rename_global r)
+ (tr_global_type r);
+ axiomatize_all_constr l'
+ end in
+ axiomatize_all_constr (list_of_array construct_types);
+ [], id
+ | _ -> assert false (* TODO constant type definition ? *)
+ end*)
+
+and tr_global_type env id ty =
if is_Prop ty then
DeclPred (id, [])
else if is_Set ty then
@@ -134,7 +196,7 @@ let rec tr_global_type env id ty =
else
let s = Typing.type_of env Evd.empty ty in
if is_Prop s then
- Assert (id, tr_formula env ty)
+ Assert (id, tr_formula [] env ty)
else
let l,t = tr_type env ty in
if is_Set s then DeclVar (id, l, t)
@@ -143,56 +205,57 @@ let rec tr_global_type env id ty =
else raise NotFO
and tr_global env r = match r with
- | Libnames.VarRef id ->
- lookup locals id
+ | VarRef id ->
+ lookup_local id
| r ->
try
- lookup globals r
+ lookup_global r
with Not_found ->
try
let ty = Global.type_of_global r in
let id = rename_global r in
let d = tr_global_type env id ty in
- Hashtbl.add globals r (Gfo d);
+ add_global r (Gfo d);
globals_stack := d :: !globals_stack;
begin try axiomatize_body env r id d with NotFO -> () end;
d
with NotFO ->
- Hashtbl.add globals r Gnot_fo;
+ add_global r Gnot_fo;
raise NotFO
and axiomatize_body env r id d = match r with
- | Libnames.VarRef ident ->
+ | VarRef ident ->
assert false
- | Libnames.ConstRef c ->
+ | ConstRef c ->
begin match (Global.lookup_constant c).const_body with
| Some b ->
let b = force b in
let id, ax = match d with
| DeclPred (id, []) ->
- let value = tr_formula env b in
+ let value = tr_formula [] env b in
id, And (Imp (Fatom (Pred (id, [])), value),
Imp (value, Fatom (Pred (id, []))))
| DeclVar (id, [], _) ->
- let value = tr_term env b in
- id, Fatom (Eq (Tvar id, value))
+ let value = tr_term [] env b in
+ id, Fatom (Eq (Fol.App (id, []), value))
| DeclVar (id, l, _) | DeclPred (id, l) ->
let vars,t = decompose_lam b in
let n = List.length l in
let k = List.length vars in
assert (k <= n);
- if k < n then raise NotFO; (* TODO: eta-expanser *)
let vars,env = coq_rename_vars env vars in
let t = substl (List.map mkVar vars) t in
+ let t,vars,env = eta_expanse t vars env (n-k) in
let vars = List.rev vars in
- let fol_var x = Tvar (rename_global (VarRef x)) in
+ let fol_var x = Fol.App (rename_global (VarRef x), []) in
let fol_vars = List.map fol_var vars in
let vars = List.combine vars l in
+ let bv = List.map fst vars in
let p = match d with
| DeclVar _ ->
- Fatom (Eq (App (id, fol_vars), tr_term env t))
+ Fatom (Eq (App (id, fol_vars), tr_term bv env t))
| DeclPred _ ->
- let value = tr_formula env t in
+ let value = tr_formula bv env t in
And (Imp (Fatom (Pred (id, fol_vars)), value),
Imp (value, Fatom (Pred (id, fol_vars))))
| _ ->
@@ -210,39 +273,40 @@ and axiomatize_body env r id d = match r with
| _ -> ()
-
(* assumption: t:T:Set *)
-and tr_term env t =
+and tr_term bv env t =
match kind_of_term t with
- | Var id ->
- Tvar (rename_global (VarRef id))
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus ->
- Plus (tr_term env a, tr_term env b)
+ Plus (tr_term bv env a, tr_term bv env b)
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus ->
- Moins (tr_term env a, tr_term env b)
+ Moins (tr_term bv env a, tr_term bv env b)
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult ->
- Mult (tr_term env a, tr_term env b)
+ Mult (tr_term bv env a, tr_term bv env b)
| Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv ->
- Div (tr_term env a, tr_term env b)
+ Div (tr_term bv env a, tr_term bv env b)
| 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
| Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
Moins (Cst 0, (fol_term_of_positive a))
+ | Term.Var id when List.mem id bv ->
+ App (string_of_id id, [])
| _ ->
let f, cl = decompose_app t in
begin try
- let r = Libnames.reference_of_constr f in
+ let r = reference_of_constr f in
match tr_global env r with
- | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term env) cl)
- | _ -> raise NotFO
+ | DeclVar (s, _, _) ->
+ Fol.App (s, List.map (tr_term bv env) cl)
+ | _ ->
+ raise NotFO
with Not_found ->
raise NotFO
end
(* assumption: f is of type Prop *)
-and tr_formula env f =
+and tr_formula bv env f =
let c, args = decompose_app f in
match kind_of_term c, args with
| Var id, [] ->
@@ -250,39 +314,49 @@ and tr_formula env f =
| _, [t;a;b] when c = build_coq_eq () ->
(*let ty = pf_type_of gl t in
if is_Set ty then*)
- Fatom (Eq (tr_term env a, tr_term env b))
+ Fatom (Eq (tr_term bv env a, tr_term bv env b))
(*else raise NotFO*)
| _, [a;b] when c = Lazy.force coq_Zle ->
- Fatom (Le (tr_term env a, tr_term env b))
+ Fatom (Le (tr_term bv env a, tr_term bv env b))
| _, [a;b] when c = Lazy.force coq_Zlt ->
- Fatom (Lt (tr_term env a, tr_term env b))
+ Fatom (Lt (tr_term bv env a, tr_term bv env b))
| _, [a;b] when c = Lazy.force coq_Zge ->
- Fatom (Ge (tr_term env a, tr_term env b))
+ Fatom (Ge (tr_term bv env a, tr_term bv env b))
| _, [a;b] when c = Lazy.force coq_Zgt ->
- Fatom (Gt (tr_term env a, tr_term env b))
+ Fatom (Gt (tr_term bv env a, tr_term bv env b))
| _, [] when c = build_coq_False () ->
False
| _, [] when c = build_coq_True () ->
True
| _, [a] when c = build_coq_not () ->
- Not (tr_formula env a)
+ Not (tr_formula bv env a)
| _, [a;b] when c = build_coq_and () ->
- And (tr_formula env a, tr_formula env b)
+ And (tr_formula bv env a, tr_formula bv env b)
| _, [a;b] when c = build_coq_or () ->
- Or (tr_formula env a, tr_formula env b)
- | Prod (_, a, b), _ ->
+ Or (tr_formula bv env a, tr_formula bv env b)
+ | Prod (n, a, b), _ ->
if is_imp_term f then
- Imp (tr_formula env a, tr_formula env b)
+ Imp (tr_formula bv env a, tr_formula bv env b)
else
- assert false (* TODO Forall *)
+ 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
+ Forall (string_of_id id, t, tr_formula bv env b)
| _, [a] when c = build_coq_ex () ->
- assert false (* TODO Exists (tr_formula env a) *)
+ assert false (* TODO Exists (tr_formula bv env a) *)
| _ ->
begin try
- let r = Libnames.reference_of_constr c in
+ let r = reference_of_constr c in
match tr_global env r with
- | DeclPred (s, _) -> Fatom (Pred (s, List.map (tr_term env) args))
- | _ -> raise NotFO
+ | DeclPred (s, _) ->
+ Fatom (Pred (s, List.map (tr_term bv env) args))
+ | _ ->
+ raise NotFO
with Not_found ->
raise NotFO
end
@@ -305,8 +379,8 @@ let tr_goal gl =
(fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
(pf_hyps_types gl) []
in
- let c = tr_formula (pf_env gl) (pf_concl gl) in
- let hyps = List.rev_append !globals_stack hyps in
+ let c = tr_formula [] (pf_env gl) (pf_concl gl) in
+ let hyps = List.rev_append !globals_stack (List.rev hyps) in
hyps, c
@@ -332,6 +406,32 @@ let dp prover gl =
error "Not a first order goal"
-let simplify = dp Simplify
+let simplify = tclTHEN intros (dp Simplify)
let cvc_lite = dp CVCLite
let harvey = dp Harvey
+
+let dp_hint l =
+ let env = Global.env () in
+ let one_hint (qid,r) =
+ if not (mem_global r) then begin
+ let ty = Global.type_of_global r in
+ let s = Typing.type_of env Evd.empty ty in
+ if is_Prop s then
+ try
+ let id = rename_global r in
+ let d = Assert (id, tr_formula [] env ty) in
+ add_global r (Gfo d);
+ globals_stack := d :: !globals_stack
+ with NotFO ->
+ add_global r Gnot_fo;
+ msg_warning
+ (pr_reference qid ++
+ str " ignored (not a first order proposition)")
+ else begin
+ add_global r Gnot_fo;
+ msg_warning
+ (pr_reference qid ++ str " ignored (not a proposition)")
+ end
+ end
+ in
+ List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 40a523089..c5517cac8 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -1,5 +1,11 @@
+open Libnames
open Proof_type
val simplify : tactic
+val cvc_lite : tactic
+val harvey : tactic
+
+val dp_hint : reference list -> unit
+
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index 35c80e72a..c330b9617 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -10,8 +10,6 @@ let rec print_list sep print fmt = function
let space fmt () = fprintf fmt "@ "
let rec print_term fmt = function
- | Tvar id ->
- fprintf fmt "%s" id
| Cst n ->
fprintf fmt "%d" n
| Plus (a, b) ->
@@ -70,8 +68,12 @@ let rec print_predicate fmt p =
let print_query fmt (decls,concl) =
let print_decl = function
- | DeclVar _ | DeclPred _ | DeclType _ ->
- ()
+ | DeclVar (id, _, _) ->
+ fprintf fmt "@[;; %s: <var>@]@\n" id
+ | DeclPred (id, _) ->
+ fprintf fmt "@[;; %s: <predicate>@]@\n" id
+ | DeclType id ->
+ fprintf fmt "@[;; %s: TYPE@]@\n" id
| Assert (id, f) ->
fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
in
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index 2cbe62284..02c73e301 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -8,7 +8,6 @@ type typ = string
type term =
| Cst of int
- | Tvar of string
| Plus of term * term
| Moins of term * term
| Mult of term * term
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index b85775597..e6667a95b 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -16,7 +16,6 @@ TACTIC EXTEND Simplify
[ "simplify" ] -> [ simplify ]
END
-(*
TACTIC EXTEND CVCLite
[ "cvcl" ] -> [ cvc_lite ]
END
@@ -24,9 +23,12 @@ END
TACTIC EXTEND Harvey
[ "harvey" ] -> [ harvey ]
END
-*)
(* should be part of basic tactics syntax *)
TACTIC EXTEND admit
[ "admit" ] -> [ Tactics.admit_as_an_axiom ]
END
+
+VERNAC COMMAND EXTEND Dp_hint
+ [ "Dp" ne_global_list(l) ] -> [ dp_hint l ]
+END
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 16:47:35 +0000