let rec eq_foterm x y =
x == y ||
match x, y with
- | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
+ | Terms.Leaf t1, Terms.Leaf t2 -> B.eq t1 t2
| Terms.Var i, Terms.Var j -> i = j
| Terms.Node l1, Terms.Node l2 -> List.for_all2 eq_foterm l1 l2
| _ -> false
;;
let debug _ = ();;
-(* let debug s = prerr_endline (Lazy.force s);; *)
+let print s = prerr_endline (Lazy.force s);;
module B(C : NCicBlob.NCicContext): Orderings.Blob
with type t = NCic.term and type input = NCic.term
module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
-let readback rdb metasenv subst context (bag,i,l) =
+let readback rdb metasenv subst context (bag,i,fo_subst,l) =
(*
List.iter (fun x ->
print_endline (Pp.pp_unit_clause ~margin:max_int
(fst(Terms.M.find x bag)))) l;
*)
let stamp = Unix.gettimeofday () in
- let proofterm = NCicProof.mk_proof bag i l in
- debug (lazy (Printf.sprintf "Got proof term in %fs"
+ let proofterm = NCicProof.mk_proof bag i fo_subst l in
+ print (lazy (Printf.sprintf "Got proof term in %fs"
(Unix.gettimeofday() -. stamp)));
let metasenv, proofterm =
let rec aux k metasenv = function
in
aux 0 metasenv proofterm
in
- debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+ print (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+ let stamp = Unix.gettimeofday () in
let metasenv, subst, proofterm, _prooftype =
NCicRefiner.typeof
(rdb#set_coerc_db NCicCoercion.empty_db)
metasenv subst context proofterm None
in
- debug (lazy "refined!");
+ print (lazy (Printf.sprintf "Refined in %fs"
+ (Unix.gettimeofday() -. stamp)));
proofterm, metasenv, subst
let nparamod rdb metasenv subst context t table =
;;
let fast_eq_check rdb metasenv subst context s goal =
+ let stamp = Unix.gettimeofday () in
match P.fast_eq_check s goal with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
| P.Unsatisfiable solutions ->
+ print (lazy (Printf.sprintf "Got solutions in %fs"
+ (Unix.gettimeofday() -. stamp)));
List.map (readback rdb metasenv subst context) solutions
;;
type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
let eqsig = ref (fun _ -> assert false);;
-let set_sig f = eqsig:=
-f;;
-
+let set_sig f = eqsig:= f;;
+let get_sig = fun x -> !eqsig x;;
let default_sig = function
| Eq ->
in eqsig:= nsig
;;
-let debug c r = prerr_endline r; c
+(* let debug c r = prerr_endline r; c *)
+let debug c _ = c;;
- let eqP() = prerr_endline "1"; prerr_endline "1"; debug (!eqsig Eq) "eqp" ;;
- let eq_ind() = prerr_endline "2"; debug (!eqsig EqInd_l) "eq_ind" ;;
- let eq_ind_r() = prerr_endline "3"; debug (!eqsig EqInd_r) "eq_ind_r";;
- let eq_refl() = prerr_endline "4"; debug (!eqsig Refl) "refl";;
+ let eqP() = debug (!eqsig Eq) "eqp" ;;
+ let eq_ind() = debug (!eqsig EqInd_l) "eq_ind" ;;
+ let eq_ind_r() = debug (!eqsig EqInd_r) "eq_ind_r";;
+ let eq_refl() = debug (!eqsig Refl) "refl";;
let extract lift vl t =
NCic.Lambda("x", hole_type, aux ft (List.rev p1))
;;
- let mk_proof (bag : NCic.term Terms.bag) mp steps =
+ let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
let module Subst = FoSubst in
let position i l =
let rec aux = function
in
lit, vl, proof
in
+ let mk_refl = function
+ | NCic.Appl [_; ty; l; _]
+ -> NCic.Appl [eq_refl();ty;l]
+ | _ -> assert false
+ in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1
| id :: tl ->
let amount = List.length seen in
let lit,vl,proof = get_literal id in
if not ongoal && id = mp then
+ let lit = Subst.apply_subst subst lit in
+ let eq_ty = extract amount [] lit in
+ let refl = mk_refl eq_ty in
((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
- NCic.LetIn ("clause_" ^ string_of_int id,
- extract amount [] lit,
- (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
+ NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
aux true ((id,([],lit))::seen) (id::tl)))
else
match proof with
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+type eq_sig_type = Eq | EqInd_l | EqInd_r | Refl
+
val set_reference_of_oxuri: (UriManager.uri -> NReference.reference) -> unit
val set_default_sig: unit -> unit
+val get_sig: eq_sig_type -> NCic.term
-val mk_proof:NCic.term Terms.bag -> Terms.M.key -> Terms.M.key list -> NCic.term
+val mk_proof:
+ NCic.term Terms.bag
+ -> Terms.M.key
+ -> NCic.term Terms.substitution
+ -> Terms.M.key list
+ -> NCic.term
(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-(* let debug s = prerr_endline (Lazy.force s) ;; *)
+(* let debug s = prerr_endline (Lazy.force s) ;; *)
let debug _ = ();;
let monster = 100;;
type t
type input
type szsontology =
- | Unsatisfiable of (t Terms.bag * int * int list) list
+ | Unsatisfiable of
+ (t Terms.bag * int * t Terms.substitution * int list) list
| GaveUp
| Error of string
| Timeout of int * t Terms.bag
type input = B.input
type bag = B.t Terms.bag * int
type szsontology =
- | Unsatisfiable of (B.t Terms.bag * int * int list) list
+ | Unsatisfiable of
+ (B.t Terms.bag * int * B.t Terms.substitution * int list) list
| GaveUp
| Error of string
| Timeout of int * B.t Terms.bag
in
goal_narrowing iterno max_steps timeout newstatus
- let compute_result bag i =
+ let compute_result bag i subst =
let l =
let rec traverse ongoal (accg,acce) i =
match Terms.get_from_bag i bag with
(fun x ->
let cl,_,_ = Terms.get_from_bag x bag in
Pp.pp_unit_clause cl) l))));
- Unsatisfiable [ bag, i, l ]
+ Unsatisfiable [ bag, i, subst, l ]
let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
let _initial_timestamp = Unix.gettimeofday () in
given_clause ~useage ~noinfer:false
bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
with
- | Sup.Success (bag, _, (i,_,_,_)) ->
- compute_result bag i
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
| Stop (Unsatisfiable _) -> Error "solution found!"
| Stop o -> o
;;
try
goal_narrowing 0 2 None s
with
- | Sup.Success (bag, _, (i,_,_,_)) ->
- compute_result bag i
+ | Sup.Success (bag, _, (i,_,_,_),subst) ->
+ compute_result bag i subst
| Stop (Unsatisfiable _) -> Error "solution found!"
| Stop o -> o
;;
type input
type state
type szsontology =
- | Unsatisfiable of (t Terms.bag * int * int list) list
+ | Unsatisfiable of
+ (t Terms.bag * int * t Terms.substitution * int list) list
| GaveUp
| Error of string
| Timeout of int * t Terms.bag
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ exception Success of
+ B.t Terms.bag
+ * int
+ * B.t Terms.unit_clause
+ * B.t Terms.substitution
(* let debug s = prerr_endline (Lazy.force s);; *)
let debug _ = ();;
;;
(* move away *)
- let is_identity_clause ~unify = function
+ let is_identity_clause = function
| _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
- | _, Terms.Equation (l,r,_,_), vl, proof when unify ->
- (try ignore(Unif.unification (* vl *) [] l r); true
- with FoUnif.UnificationFailure _ -> false)
| _, Terms.Equation (_,_,_,_), _, _ -> false
| _, Terms.Predicate _, _, _ -> assert false
;;
+ let is_identity_goal = function
+ | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> Some []
+ | _, Terms.Equation (l,r,_,_), vl, proof ->
+ (try Some (Unif.unification (* vl *) [] l r)
+ with FoUnif.UnificationFailure _ -> None)
+ | _, Terms.Equation (_,_,_,_), _, _ -> None
+ | _, Terms.Predicate _, _, _ -> assert false
+ ;;
+
let build_new_clause bag maxvar filter rule t subst id id2 pos dir =
let maxvar, _vl, subst = Utils.relocate maxvar (Terms.vars_of_term
(Subst.apply_subst subst t)) subst in
(* demodulate and check for subsumption *)
let simplify table maxvar bag clause =
debug (lazy "simplify...");
- if is_identity_clause ~unify:false clause then bag,None
+ if is_identity_clause clause then bag,None
(* else if orphan_murder bag actives clause then bag,None *)
else let bag, clause = demodulate bag clause table in
- if is_identity_clause ~unify:false clause then bag,None
+ if is_identity_clause clause then bag,None
else
match is_subsumed ~unify:false bag maxvar clause table with
| None -> bag, Some clause
if no_demod then bag, clause else demodulate bag clause table
in
if List.exists (are_alpha_eq clause) g_actives then None
- else if (is_identity_clause ~unify:true clause)
- then raise (Success (bag, maxvar, clause))
- else
+ else match (is_identity_goal clause) with
+ | Some subst -> raise (Success (bag,maxvar,clause,subst))
+ | None ->
let (id,lit,vl,_) = clause in
(* this optimization makes sense only if we demodulated, since in
that case the clause should have been turned into an identity *)
| None -> Some (bag,clause)
| Some (bag,maxvar,cl,subst) ->
debug (lazy "Goal subsumed");
- raise (Success (bag,maxvar,cl))
+ raise (Success (bag,maxvar,cl,subst))
(*
match is_subsumed ~unify:true bag maxvar clause table with
| None -> Some (bag, clause)
sig
(* bag, maxvar, meeting point *)
- exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
+ exception Success of
+ B.t Terms.bag
+ * int
+ * B.t Terms.unit_clause
+ * B.t Terms.substitution
(* The returned active set is the input one + the selected clause *)
val infer_right :
projects / helm.git / commitdiff