NCicProof.set_default_sig()
;;
-let debug _ = ();;
+let noprint _ = ();;
let print s = prerr_endline (Lazy.force s);;
-let debug = print;;
+let debug = noprint;;
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 ?(demod=false) rdb metasenv subst context (bag,i,fo_subst,l) =
+let readback status ?(demod=false) 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,prooftype = NCicProof.mk_proof ~demod bag i fo_subst l in
+ let proofterm,prooftype = NCicProof.mk_proof status ~demod bag i fo_subst l in
(* debug (lazy (Printf.sprintf "Got proof term in %fs"
(Unix.gettimeofday() -. stamp))); *)
(*
in
aux 0 metasenv proofterm
in *)
- debug (lazy (NCicPp.ppterm ~metasenv ~subst ~context proofterm));
+ debug (lazy (status#ppterm ~metasenv ~subst ~context proofterm));
(*
let stamp = Unix.gettimeofday () in
let metasenv, subst, proofterm, _prooftype =
NCicRefiner.typeof
- (rdb#set_coerc_db NCicCoercion.empty_db)
+ (status#set_coerc_db NCicCoercion.empty_db)
metasenv subst context proofterm None
in
print (lazy (Printf.sprintf "Refined in %fs"
*)
proofterm, prooftype, metasenv, subst
-let nparamod rdb metasenv subst context t table =
+let nparamod status metasenv subst context t table =
let module C =
struct
let metasenv = metasenv
let context = context
end
in
- let module B = B(C) in
+ (*let module B = B(C) in*)
let module P = NCicParamod(C) in
- let module Pp = Pp.Pp(B) in
+ (*let module Pp = Pp.Pp(B) in*)
let bag, maxvar = Terms.empty_bag, 0 in
let (bag,maxvar), goals =
HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
| P.Unsatisfiable solutions ->
- List.map (readback rdb metasenv subst context) solutions
+ List.map (readback status metasenv subst context) solutions
;;
module EmptyC =
type state = P.state
let empty_state = P.empty_state
-let forward_infer_step s t ty =
+exception NotEmbeddable
+
+let not_embeddable status subst context ty =
+ let rec aux = function
+ | NCic.Meta _
+ | NCic.Const _
+ | NCic.Rel _
+ | NCic.Sort _ -> ()
+ | NCic.Appl l -> List.iter aux l
+ | t ->
+ (* cannot embed a blob term containing metas *)
+ if (NCicUntrusted.metas_of_term status subst context t = [])
+ then ()
+ else raise NotEmbeddable
+ in
+ try aux ty; noprint (lazy ("Embeddable")); false
+ with NotEmbeddable -> debug (lazy ("Not embeddable")); true
+;;
+
+let tooflex (_,l,_,_) =
+ match l with
+ | Terms.Equation (l,r,_,o) ->
+ (match l,r,o with
+ | (Terms.Var _ | Terms.Node (Terms.Var _::_)), _, (Terms.Incomparable | Terms.Invertible) -> true
+ | _, (Terms.Var _ | Terms.Node (Terms.Var _::_)),(Terms.Incomparable | Terms.Invertible) -> true
+ | _ -> false)
+ | _ -> false
+;;
+
+let forward_infer_step0 status metasenv subst context s t ty =
let bag = P.bag_of_state s in
+ let not_embed =
+ let sty,_,_ =
+ NCicMetaSubst.saturate status ~delta:0 metasenv subst context ty 0 in
+ not_embeddable status subst context sty in
+ if not_embed then (debug (lazy "theorem not embeddable"); s,None)
+ else
let bag,clause = P.mk_passive bag (t,ty) in
if Terms.is_eq_clause clause then
- P.forward_infer_step (P.replace_bag s bag) clause 0
- else (debug (lazy "not eq"); s)
+ if tooflex clause then (debug (lazy "pruning tooflex"); s,None)
+ else
+ P.forward_infer_step (P.replace_bag s bag) clause 0, Some clause
+ else (debug (lazy "not eq"); s,None)
+;;
+
+let forward_infer_step status metasenv subst context s t ty =
+ fst (forward_infer_step0 status metasenv subst context s t ty)
;;
-let index_obj s uri =
- let obj = NCicEnvironment.get_checked_obj uri in
+let index_obj status s uri =
+ let obj = NCicEnvironment.get_checked_obj status uri in
debug (lazy ("indexing : " ^ (NUri.string_of_uri uri)));
debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri)))));
match obj with
| (_,_,[],[],NCic.Constant(_,_,None,ty,_)) ->
let nref = NReference.reference_of_spec uri NReference.Decl in
- forward_infer_step s (NCic.Const nref) ty
+ forward_infer_step0 status [] [] [] s (NCic.Const nref) ty
| (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) ->
let nref = NReference.reference_of_spec uri (NReference.Def d) in
- forward_infer_step s (NCic.Const nref) ty
- | _ -> s
+ forward_infer_step0 status [] [] [] s (NCic.Const nref) ty
+ | _ -> s,None
;;
-let demod rdb metasenv subst context s goal =
+let demod status metasenv subst context s goal =
+ if not_embeddable status subst context (snd goal) then [] else
(* let stamp = Unix.gettimeofday () in *)
match P.demod 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 ~demod:true rdb metasenv subst context) solutions
+ List.map (readback ~demod:true status metasenv subst context) solutions
;;
-let paramod rdb metasenv subst context s goal =
+let paramod status metasenv subst context s goal =
+ if not_embeddable status subst context (snd goal) then [] else
(* let stamp = Unix.gettimeofday () in *)
match P.nparamod ~useage:true ~max_steps:max_int
~timeout:(Unix.gettimeofday () +. 300.0) s goal with
| P.Unsatisfiable solutions ->
(* print (lazy (Printf.sprintf "Got solutions in %fs"
(Unix.gettimeofday() -. stamp))); *)
- List.map (readback rdb metasenv subst context) solutions
+ List.map (readback status metasenv subst context) solutions
;;
-let fast_eq_check rdb metasenv subst context s goal =
+let fast_eq_check status metasenv subst context s goal =
+ if not_embeddable status subst context (snd goal) then [] else
(* 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
+ List.map (readback status metasenv subst context) solutions
;;
-let is_equation metasenv subst context ty =
+let is_equation status metasenv subst context ty =
let hty, _, _ =
- NCicMetaSubst.saturate ~delta:0 metasenv subst context
+ NCicMetaSubst.saturate status ~delta:0 metasenv subst context
ty 0
in match hty with
- | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
+ | NCic.Appl (eq ::_) when eq = CB.eqP -> true
| _ -> false
;;
(*
-let demodulate rdb metasenv subst context s goal =
+let demodulate status 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
+ List.map (readback status metasenv subst context) solutions
;;
*)
projects / helm.git / blobdiff