diff options
Diffstat (limited to 'contrib/dp/dp.ml')
-rw-r--r-- | contrib/dp/dp.ml | 760 |
1 files changed, 760 insertions, 0 deletions
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml new file mode 100644 index 00000000..af684e6e --- /dev/null +++ b/contrib/dp/dp.ml @@ -0,0 +1,760 @@ +(* Authors: Nicolas Ayache and Jean-Christophe Filliātre *) +(* Tactics to call decision procedures *) + +(* Works in two steps: + + - first the Coq context and the current goal are translated in + Polymorphic First-Order Logic (see fol.mli in this directory) + + - then the resulting query is passed to the Why tool that translates + it to the syntax of the selected prover (Simplify, CVC Lite, haRVey, + Zenon) +*) + +open Util +open Pp +open Term +open Tacmach +open Tactics +open Tacticals +open Fol +open Names +open Nameops +open Termops +open Coqlib +open Hipattern +open Libnames +open Declarations + +let debug = ref false + +let logic_dir = ["Coq";"Logic";"Decidable"] +let coq_modules = + init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules + @ [["Coq"; "omega"; "OmegaLemmas"]] + +let constant = gen_constant_in_modules "dp" coq_modules + +let coq_Z = lazy (constant "Z") +let coq_Zplus = lazy (constant "Zplus") +let coq_Zmult = lazy (constant "Zmult") +let coq_Zopp = lazy (constant "Zopp") +let coq_Zminus = lazy (constant "Zminus") +let coq_Zdiv = lazy (constant "Zdiv") +let coq_Zs = lazy (constant "Zs") +let coq_Zgt = lazy (constant "Zgt") +let coq_Zle = lazy (constant "Zle") +let coq_Zge = lazy (constant "Zge") +let coq_Zlt = lazy (constant "Zlt") +let coq_Z0 = lazy (constant "Z0") +let coq_Zpos = lazy (constant "Zpos") +let coq_Zneg = lazy (constant "Zneg") +let coq_xH = lazy (constant "xH") +let coq_xI = lazy (constant "xI") +let coq_xO = lazy (constant "xO") + +(* not Prop typed expressions *) +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) + +let foralls = + List.fold_right + (fun (x,t) p -> Forall (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 *) +let coq_rename_vars env vars = + let avoid = ref (ids_of_named_context (Environ.named_context env)) in + List.fold_right + (fun (na,t) (newvars, newenv) -> + let id = next_name_away na !avoid in + avoid := id :: !avoid; + id :: newvars, Environ.push_named (id, None, t) newenv) + vars ([],env) + +(* extract the prenex type quantifications i.e. + type_quantifiers env (A1:Set)...(Ak:Set)t = A1...An, (env+Ai), t *) +let decomp_type_quantifiers env t = + let rec loop vars t = match kind_of_term t with + | Prod (n, a, t) when is_Set a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +(* same thing with lambda binders (for axiomatize body) *) +let decomp_type_lambdas env t = + let rec loop vars t = match kind_of_term t with + | Lambda (n, a, t) when is_Set a -> + loop ((n,a) :: vars) t + | _ -> + let vars, env = coq_rename_vars env vars in + let t = substl (List.map mkVar vars) t in + List.rev vars, env, t + in + loop [] t + +let decompose_arrows = + let rec arrows_rec l c = match kind_of_term c with + | Prod (_,t,c) when not (dependent (mkRel 1) c) -> arrows_rec (t :: l) c + | Cast (c,_,_) -> arrows_rec l c + | _ -> List.rev l, c + in + arrows_rec [] + +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 + +let rec skip_k_args k cl = match k, cl with + | 0, _ -> cl + | _, _ :: cl -> skip_k_args (k-1) cl + | _, [] -> raise NotFO + +(* Coq global references *) + +type global = Gnot_fo | Gfo of Fol.decl + +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_local r = match Hashtbl.find locals r with + | Gnot_fo -> raise NotFO + | Gfo d -> d + +let iter_all_constructors i f = + let _, oib = Global.lookup_inductive i in + Array.iteri + (fun j tj -> f j (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 = Axiom ("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 (Printer.pr_constr (mkConst c')); + c' + | Anonymous -> + raise Not_found) + +(* abstraction tables *) + +let term_abstractions = Hashtbl.create 97 + +let new_abstraction = + let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r + +(* Arithmetic constants *) + +exception NotArithConstant + +(* translates a closed Coq term p:positive into a FOL term of type int *) +let rec tr_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, tr_positive a), Cst 1) + | Term.App (f, [|a|]) when f = Lazy.force coq_xO -> + Mult (Cst 2, tr_positive a) + | Term.Cast (p, _, _) -> + tr_positive p + | _ -> + raise NotArithConstant + +(* translates a closed Coq term t:Z into a FOL term of type int *) +let rec tr_arith_constant t = match kind_of_term t with + | Term.Construct _ when t = Lazy.force coq_Z0 -> + Cst 0 + | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> + tr_positive a + | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> + Moins (Cst 0, tr_positive a) + | Term.Cast (t, _, _) -> + tr_arith_constant t + | _ -> + raise NotArithConstant + +(* translate a Coq term t:Set into a FOL type expression; + tv = list of type variables *) +and tr_type tv env t = + let t = Reductionops.nf_betadeltaiota env Evd.empty t in + if t = Lazy.force coq_Z then + Tid ("int", []) + else match kind_of_term t with + | Var x when List.mem x tv -> + Tvar (string_of_id x) + | _ -> + let f, cl = decompose_app t in + begin try + let r = global_of_constr f in + match tr_global env r with + | DeclType (id, k) -> + assert (k = List.length cl); (* since t:Set *) + Tid (id, List.map (tr_type tv env) cl) + | _ -> + raise NotFO + with + | Not_found -> + raise NotFO + | NotFO -> + (* we need to abstract some part of (f cl) *) + (*TODO*) + raise NotFO + end + +and make_term_abstraction tv env c = + let ty = Typing.type_of env Evd.empty c in + let id = new_abstraction () in + match tr_decl env id ty with + | DeclFun (id,_,_,_) as d -> + begin try + Hashtbl.find term_abstractions c + with Not_found -> + Hashtbl.add term_abstractions c id; + globals_stack := d :: !globals_stack; + id + end + | _ -> + raise NotFO + +(* translate a Coq declaration id:ty in a FOL declaration, that is either + - a type declaration : DeclType (id, n) where n:int is the type arity + - a function declaration : DeclFun (id, tl, t) ; that includes constants + - a predicate declaration : DeclPred (id, tl) + - an axiom : Axiom (id, p) + *) +and tr_decl env id ty = + let tv, env, t = decomp_type_quantifiers env ty in + if is_Set t then + DeclType (id, List.length tv) + else if is_Prop t then + DeclPred (id, List.length tv, []) + else + let s = Typing.type_of env Evd.empty t in + if is_Prop s then + Axiom (id, tr_formula tv [] env t) + else + let l, t = decompose_arrows t in + let l = List.map (tr_type tv env) l in + if is_Prop t then + DeclPred(id, List.length tv, l) + else + let s = Typing.type_of env Evd.empty t in + if is_Set s then + DeclFun(id, List.length tv, l, tr_type tv env t) + else + raise NotFO + +(* tr_global(r) = tr_decl(id(r),typeof(r)) + a cache mechanism *) +and tr_global env r = match r with + | VarRef id -> + lookup_local id + | r -> + try + lookup_global r + with Not_found -> + try + let ty = Global.type_of_global r in + let id = rename_global r in + let d = tr_decl env id ty in + (* 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 -> + add_global r Gnot_fo; + raise NotFO + +and axiomatize_body env r id d = match r with + | VarRef _ -> + assert false + | ConstRef c -> + begin match (Global.lookup_constant c).const_body with + | Some b -> + let b = force b in + let tv, env, b = decomp_type_lambdas env b in + let axioms = + (match d with + | DeclPred (id, _, []) -> + let value = tr_formula tv [] env b in + [id, Iff (Fatom (Pred (id, [])), value)] + | DeclFun (id, _, [], _) -> + let value = tr_term tv [] env b in + [id, Fatom (Eq (Fol.App (id, []), value))] + | DeclFun (id, _, l, _) | DeclPred (id, _, l) -> + Format.eprintf "axiomatize_body %S@." id; + 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 + assert (k <= n); + 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 bv = vars in + let vars = List.map (fun x -> string_of_id x) vars in + let fol_var x = + Fol.App (x, []) in + let fol_vars = List.map fol_var vars in + let vars = List.combine vars l in + begin match d with + | DeclFun _ -> + begin match kind_of_term t with + | Case (ci, _, e, br) -> + equations_for_case env id vars tv bv ci e br + | _ -> + let p = + Fatom (Eq (App (id, fol_vars), + tr_term tv bv env t)) + in + [id, foralls vars p] + end + | DeclPred _ -> + let value = tr_formula tv bv env t in + let p = Iff (Fatom (Pred (id, fol_vars)), value) in + [id, foralls vars p] + | _ -> + assert false + end + | DeclType _ -> + raise NotFO + | Axiom _ -> assert false) + in + let axioms = List.map (fun (id,ax) -> Axiom (id, ax)) axioms in + globals_stack := axioms @ !globals_stack + | None -> + () (* Coq axiom *) + end + | IndRef i -> + iter_all_constructors i + (fun _ c -> + let rc = reference_of_constr c in + try + begin match tr_global env rc with + | DeclFun (_, _, [], _) -> () + | DeclFun (idc, _, al, _) -> injection idc al + | _ -> () + end + with NotFO -> + ()) + | _ -> () + +and equations_for_case env id vars tv bv ci e br = match kind_of_term e with + | Var x when List.exists (fun (y, _) -> string_of_id x = y) vars -> + let eqs = ref [] in + iter_all_constructors ci.ci_ind + (fun j cj -> + try + let cjr = reference_of_constr cj in + begin match tr_global env cjr with + | DeclFun (idc, _, l, _) -> + let b = br.(j) in + let rec_vars, b = decompose_lam b in + let rec_vars, env = coq_rename_vars env rec_vars in + 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 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 + let fol_rec_term = App (idc, fol_rec_vars) in + let rec_vars = List.combine rec_vars l in + let fol_vars = List.map fst vars in + let fol_vars = List.map fol_var fol_vars in + let fol_vars = List.map (fun y -> match y with + | App (id, _) -> + if id = string_of_id x + then fol_rec_term + else y + | _ -> y) + fol_vars in + let vars = vars @ rec_vars in + let rec remove l e = match l with + | [] -> [] + | (y, t)::l' -> if y = string_of_id e then l' + else (y, t)::(remove l' e) in + let vars = remove vars x in + let p = + Fatom (Eq (App (id, fol_vars), + tr_term tv bv env b)) + in + eqs := (id ^ "_" ^ idc, foralls vars p) :: !eqs + | _ -> + assert false end + with NotFO -> + ()); + !eqs + | _ -> + raise NotFO + +(* assumption: t:T:Set *) +and tr_term tv bv env t = match kind_of_term t with + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> + Plus (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> + Moins (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> + Mult (tr_term tv bv env a, tr_term tv bv env b) + | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> + Div (tr_term tv bv env a, tr_term tv bv env b) + | Term.Var id when List.mem id bv -> + App (string_of_id id, []) + | _ -> + try + tr_arith_constant t + with NotArithConstant -> + let f, cl = decompose_app t in + begin try + let r = global_of_constr f in + match tr_global env r with + | DeclFun (s, k, _, _) -> + let cl = skip_k_args k cl in + Fol.App (s, List.map (tr_term tv bv env) cl) + | _ -> + raise NotFO + with + | Not_found -> + raise NotFO + | NotFO -> (* we need to abstract some part of (f cl) *) + let rec abstract app = function + | [] -> + Fol.App (make_term_abstraction tv env app, []) + | x :: l as args -> + begin try + let s = make_term_abstraction tv env app in + Fol.App (s, List.map (tr_term tv bv env) args) + with NotFO -> + abstract (applist (app, [x])) l + end + in + let app,l = match cl with + | x :: l -> applist (f, [x]), l | [] -> raise NotFO + in + abstract app l + end + +and quantifiers n a b tv 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 = tr_type tv env a in + let bv = id :: bv in + id, t, bv, env, b + +(* assumption: f is of type Prop *) +and tr_formula tv bv env f = + let c, args = decompose_app f in + match kind_of_term c, args with + | Var id, [] -> + Fatom (Pred (rename_global (VarRef id), [])) + | _, [t;a;b] when c = build_coq_eq () -> + let ty = Typing.type_of env Evd.empty t in + if is_Set ty then + let _ = tr_type tv env t in + Fatom (Eq (tr_term tv bv env a, tr_term tv bv env b)) + else + raise NotFO + | _, [a;b] when c = Lazy.force coq_Zle -> + Fatom (Le (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zlt -> + Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zge -> + Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b)) + | _, [a;b] when c = Lazy.force coq_Zgt -> + Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b)) + | _, [] when c = build_coq_False () -> + False + | _, [] when c = build_coq_True () -> + True + | _, [a] when c = build_coq_not () -> + Not (tr_formula tv bv env a) + | _, [a;b] when c = build_coq_and () -> + And (tr_formula tv bv env a, tr_formula tv bv env b) + | _, [a;b] when c = build_coq_or () -> + Or (tr_formula tv bv env a, tr_formula tv bv env b) + | Prod (n, a, b), _ -> + if is_imp_term f then + Imp (tr_formula tv bv env a, tr_formula tv bv env b) + else + let id, t, bv, env, b = quantifiers n a b tv bv env in + Forall (string_of_id id, t, tr_formula tv bv env b) + | _, [_; a] when c = build_coq_ex () -> + begin match kind_of_term a with + | Lambda(n, a, b) -> + let id, t, bv, env, b = quantifiers n a b tv bv env in + Exists (string_of_id id, t, tr_formula tv bv env b) + | _ -> + (* unusual case of the shape (ex p) *) + raise NotFO (* TODO: we could eta-expanse *) + end + | _ -> + begin try + let r = global_of_constr c in + match tr_global env r with + | DeclPred (s, k, _) -> + let args = skip_k_args k args in + Fatom (Pred (s, List.map (tr_term tv bv env) args)) + | _ -> + raise NotFO + with Not_found -> + raise NotFO + end + + +let tr_goal gl = + Hashtbl.clear locals; + let tr_one_hyp (id, ty) = + try + let s = rename_global (VarRef id) in + let d = tr_decl (pf_env gl) s ty in + Hashtbl.add locals id (Gfo d); + d + with NotFO -> + Hashtbl.add locals id Gnot_fo; + raise NotFO + in + let hyps = + List.fold_right + (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 (List.rev hyps) in + hyps, c + + +type prover = Simplify | CVCLite | Harvey | Zenon + +let remove_files = List.iter (fun f -> try Sys.remove f with _ -> ()) + +let sprintf = Format.sprintf + +let call_simplify fwhy = + if Sys.command (sprintf "why --simplify %s" fwhy) <> 0 then + anomaly ("call to why --simplify " ^ fwhy ^ " failed; please report"); + let fsx = Filename.chop_suffix fwhy ".why" ^ "_why.sx" in + let cmd = + sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" fsx + in + let out = Sys.command cmd in + let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in + if not !debug then remove_files [fwhy; fsx]; + r + +let call_zenon fwhy = + let cmd = sprintf "why --no-prelude --no-zenon-prelude --zenon %s" fwhy in + if Sys.command cmd <> 0 then + anomaly ("call to " ^ cmd ^ " failed; please report"); + let fznn = Filename.chop_suffix fwhy ".why" ^ "_why.znn" in + let cmd = + sprintf "timeout 10 zenon %s > out 2>&1 && grep -q PROOF-FOUND out" fznn + in + let out = Sys.command cmd in + let r = + if out = 0 then Valid + else if out = 1 then Invalid + else if out = 137 then Timeout + else anomaly ("malformed Zenon input file " ^ fznn) + in + if not !debug then remove_files [fwhy; fznn]; + r + +let call_cvcl fwhy = + if Sys.command (sprintf "why --cvcl %s" fwhy) <> 0 then + anomaly ("call to why --cvcl " ^ fwhy ^ " failed; please report"); + let fcvc = Filename.chop_suffix fwhy ".why" ^ "_why.cvc" in + let cmd = + sprintf "timeout 10 cvcl < %s > out 2>&1 && grep -q -w Valid out" fcvc + in + let out = Sys.command cmd in + let r = if out = 0 then Valid else if out = 1 then Invalid else Timeout in + if not !debug then remove_files [fwhy; fcvc]; + r + +let call_harvey fwhy = + if Sys.command (sprintf "why --harvey %s" fwhy) <> 0 then + anomaly ("call to why --harvey " ^ fwhy ^ " failed; please report"); + let frv = Filename.chop_suffix fwhy ".why" ^ "_why.rv" in + let out = Sys.command (sprintf "rvc -e -t %s > /dev/null 2>&1" frv) in + if out <> 0 then anomaly ("call to rvc -e -t " ^ frv ^ " failed"); + let f = Filename.chop_suffix frv ".rv" ^ "-0.baf" in + let outf = Filename.temp_file "rv" ".out" in + let out = + Sys.command (sprintf "timeout 10 rv -e\"-T 2000\" %s > %s 2>&1" f outf) + in + let r = + if out <> 0 then + Timeout + else + let cmd = + sprintf "grep \"Proof obligation in\" %s | grep -q \"is valid\"" outf + in + if Sys.command cmd = 0 then Valid else Invalid + in + if not !debug then remove_files [fwhy; frv; outf]; + r + +let call_prover prover q = + let fwhy = Filename.temp_file "coq_dp" ".why" in + Dp_why.output_file fwhy q; + if !debug then ignore (Sys.command (sprintf "cat %s" fwhy)); + match prover with + | Simplify -> call_simplify fwhy + | Zenon -> call_zenon fwhy + | CVCLite -> call_cvcl fwhy + | Harvey -> call_harvey fwhy + +let dp prover gl = + let concl_type = pf_type_of gl (pf_concl gl) in + 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 + | Valid -> Tactics.admit_as_an_axiom gl + | Invalid -> error "Invalid" + | DontKnow -> error "Don't know" + | Timeout -> error "Timeout" + end + with NotFO -> + error "Not a first order goal" + + +let simplify = tclTHEN intros (dp Simplify) +let cvc_lite = tclTHEN intros (dp CVCLite) +let harvey = dp Harvey +let zenon = tclTHEN intros (dp Zenon) + +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 = Axiom (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) |