aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/dp/dp.ml126
-rw-r--r--contrib/dp/dp.mli1
-rw-r--r--contrib/dp/dp_simplify.ml16
-rw-r--r--contrib/dp/dp_zenon.ml103
-rw-r--r--contrib/dp/dp_zenon.mli4
-rw-r--r--contrib/dp/g_dp.ml44
6 files changed, 213 insertions, 41 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 9dc538c78..975c1e59c 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -70,7 +70,8 @@ let rename_global r =
loop (Nametab.id_of_global r)
let foralls =
- List.fold_right (fun (x,t) p -> Forall (rename_global (VarRef x), t, p))
+ 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"))
@@ -146,7 +147,35 @@ let lookup_local r = match Hashtbl.find locals r with
| Gnot_fo -> raise NotFO
| Gfo d -> d
-(* assumption: t:Set *)
+let iter_all_constructors i f =
+ let _, oib = Global.lookup_inductive i in
+ Array.iteri
+ (fun j tj -> f (mkConstruct (i, j+1)))
+ oib.mind_nf_lc
+
+(* injection c [t1,...,tn] adds the injection axiom
+ forall x1:t1,...,xn:tn,y1:t1,...,yn:tn.
+ c(x1,...,xn)=c(y1,...,yn) -> x1=y1 /\ ... /\ xn=yn *)
+
+let injection c l =
+ let i = ref 0 in
+ let var s = incr i; id_of_string (s ^ string_of_int !i) in
+ let xl = List.map (fun t -> rename_global (VarRef (var "x")), t) l in
+ i := 0;
+ let yl = List.map (fun t -> rename_global (VarRef (var "y")), t) l in
+ let f =
+ List.fold_right2
+ (fun (x,_) (y,_) p -> And (Fatom (Eq (App (x,[]),App (y,[]))), p))
+ xl yl True
+ in
+ let vars = List.map (fun (x,_) -> App(x,[])) in
+ let f = Imp (Fatom (Eq (App (c, vars xl), App (c, vars yl))), f) in
+ let foralls = List.fold_right (fun (x,t) p -> Forall (x, t, p)) in
+ let f = foralls xl (foralls yl f) in
+ let ax = Assert ("injection_" ^ c, f) in
+ globals_stack := ax :: !globals_stack
+
+(* assumption: t:Set or Type *)
let rec tr_type env ty =
if ty = Lazy.force coq_Z then [], "INT"
else if is_Prop ty then [], "BOOLEAN"
@@ -159,34 +188,35 @@ let rec tr_type env ty =
end
| _ -> assert false
end
- else let r = global_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*)
+ else
+ try let r = global_of_constr ty in
+ (try
+ begin match lookup_global r with
+ | DeclType id -> [], id
+ | _ -> assert false (* assumption: t:Set *)
+ end
+ with Not_found ->
+ begin match r with
+ | IndRef i ->
+ let id = rename_global r in
+ let d = DeclType id in
+ add_global r (Gfo d);
+ globals_stack := d :: !globals_stack;
+ iter_all_constructors i
+ (fun c ->
+ let rc = global_of_constr c in
+ try
+ begin match tr_global env rc with
+ | DeclVar (idc, [], _) -> ()
+ | DeclVar (idc, al, _) -> injection idc al
+ | _ -> assert false
+ end
+ with NotFO ->
+ ());
+ [], id
+ | _ -> raise NotFO (* constant type definition *)
+ end)
+ with Not_found -> raise NotFO
and tr_global_type env id ty =
if is_Prop ty then
@@ -198,8 +228,8 @@ and tr_global_type env id ty =
if is_Prop s then
Assert (id, tr_formula [] env ty)
else
- let l,t = tr_type env ty in
- if is_Set s then DeclVar (id, l, t)
+ let l,t = tr_type env ty in
+ if is_Set s then DeclVar(id, l, t)
else if t = "BOOLEAN" then
DeclPred(id, l)
else raise NotFO
@@ -215,8 +245,11 @@ and tr_global env r = match r with
let ty = Global.type_of_global r in
let id = rename_global r in
let d = tr_global_type env id ty in
- add_global r (Gfo d);
- globals_stack := d :: !globals_stack;
+ (* r can be already declared if it is a constructor *)
+ if not (mem_global r) then begin
+ add_global r (Gfo d);
+ globals_stack := d :: !globals_stack
+ end;
begin try axiomatize_body env r id d with NotFO -> () end;
d
with NotFO ->
@@ -224,7 +257,7 @@ and tr_global env r = match r with
raise NotFO
and axiomatize_body env r id d = match r with
- | VarRef ident ->
+ | VarRef _ ->
assert false
| ConstRef c ->
begin match (Global.lookup_constant c).const_body with
@@ -247,7 +280,8 @@ and axiomatize_body env r id d = match r with
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 = Fol.App (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
@@ -270,6 +304,22 @@ and axiomatize_body env r id d = match r with
| None ->
() (* Coq axiom *)
end
+ | IndRef i ->
+ begin match d with
+ | DeclPred _ ->
+ iter_all_constructors i
+ (fun c ->
+ let rc = reference_of_constr c in
+ try
+ begin match tr_global env rc with
+ | Assert _ -> ()
+ | _ -> assert false
+ end
+ with NotFO ->
+ ())
+ | DeclType _ -> raise NotFO
+ | _ -> assert false
+ end
| _ -> ()
@@ -384,12 +434,13 @@ let tr_goal gl =
hyps, c
-type prover = Simplify | CVCLite | Harvey
+type prover = Simplify | CVCLite | Harvey | Zenon
let call_prover prover q = match prover with
| Simplify -> Dp_simplify.call q
| CVCLite -> error "CVC Lite not yet interfaced"
| Harvey -> error "haRVey not yet interfaced"
+ | Zenon -> Dp_zenon.call q
let dp prover gl =
let concl_type = pf_type_of gl (pf_concl gl) in
@@ -409,6 +460,7 @@ let dp prover gl =
let simplify = tclTHEN intros (dp Simplify)
let cvc_lite = dp CVCLite
let harvey = dp Harvey
+let zenon = tclTHEN intros (dp Zenon)
let dp_hint l =
let env = Global.env () in
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index c5517cac8..3dad469c6 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -5,6 +5,7 @@ open Proof_type
val simplify : tactic
val cvc_lite : tactic
val harvey : tactic
+val zenon : tactic
val dp_hint : reference list -> unit
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index c330b9617..0a7bd0701 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -66,12 +66,20 @@ let rec print_predicate fmt 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, _, _) ->
- fprintf fmt "@[;; %s: <var>@]@\n" id
- | DeclPred (id, _) ->
- fprintf fmt "@[;; %s: <predicate>@]@\n" id
+ | 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) ->
diff --git a/contrib/dp/dp_zenon.ml b/contrib/dp/dp_zenon.ml
new file mode 100644
index 000000000..ef9499bf9
--- /dev/null
+++ b/contrib/dp/dp_zenon.ml
@@ -0,0 +1,103 @@
+
+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 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 space 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@ %a)@]" pp a pp b
+ | Or (a, b) ->
+ fprintf fmt "@[(\\/@ %a@ %a)@]" pp a pp b
+ | Not a ->
+ fprintf fmt "@[(-.@ %a)@]" pp a
+ | Forall (id, t, p) ->
+ fprintf fmt "@[(A. ((%s \"%s\")@ %a))@]" id t pp p
+ | Exists (id, t, p) ->
+ fprintf fmt "@[(E. ((%s \"%s\")@ %a))@]" id t pp p
+
+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 "@[\"%s\" %a@]@\n" id print_predicate f
+ in
+ List.iter print_decl decls;
+ fprintf fmt "$goal %a@." print_predicate concl
+
+let call q =
+ let f = Filename.temp_file "coq_dp" ".sx" 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 zenon %s > out 2>&1 && grep -q PROOF-FOUND 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 if out = 137 then Timeout
+ else Util.anomaly "malformed Zenon input file"
+ (* TODO: effacer le fichier f et le fichier out *)
+
+
diff --git a/contrib/dp/dp_zenon.mli b/contrib/dp/dp_zenon.mli
new file mode 100644
index 000000000..03b6d3475
--- /dev/null
+++ b/contrib/dp/dp_zenon.mli
@@ -0,0 +1,4 @@
+
+open Fol
+
+val call : query -> prover_answer
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index e6667a95b..074df6722 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -24,6 +24,10 @@ TACTIC EXTEND Harvey
[ "harvey" ] -> [ harvey ]
END
+TACTIC EXTEND Zenon
+ [ "zenon" ] -> [ zenon ]
+END
+
(* should be part of basic tactics syntax *)
TACTIC EXTEND admit
[ "admit" ] -> [ Tactics.admit_as_an_axiom ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 19:03:19 +0000