let print s = prerr_endline (Lazy.force s);;
let debug = noprint;;
-module B(C : NCicBlob.NCicContext): Orderings.Blob
+module B : Orderings.Blob
with type t = NCic.term and type input = NCic.term
- = Orderings.LPO(NCicBlob.NCicBlob(C))
+ = Orderings.LPO(NCicBlob.NCicBlob)
-module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
+module NCicParamod = Paramod.Paramod(B)
let readback status ?(demod=false) metasenv subst context (bag,i,fo_subst,l) =
(*
proofterm, prooftype, metasenv, subst
let nparamod status metasenv subst context t table =
- let module C =
- struct
- let metasenv = metasenv
- let subst = subst
- let context = context
- end
- in
- let module B = B(C) in
- let module P = NCicParamod(C) in
+ let module P = NCicParamod in
let module Pp = Pp.Pp(B) in
let bag, maxvar = Terms.empty_bag, 0 in
+ let saturate (t,ty) =
+ NCicBlob.saturate status metasenv subst context t ty in
let (bag,maxvar), goals =
- HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
+ HExtlib.list_mapi_acc
+ (fun x _ a -> P.mk_goal a (saturate x)) (bag,maxvar) [t]
in
- let (bag,maxvar), passives =
- HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
+ let (bag,maxvar), passives =
+ HExtlib.list_mapi_acc
+ (fun x _ a -> P.mk_passive a (saturate x)) (bag,maxvar) table
in
match
P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
List.map (readback status metasenv subst context) solutions
;;
-module EmptyC =
- struct
- let metasenv = []
- let subst = []
- let context = []
- end
-
-module CB = NCicBlob.NCicBlob(EmptyC)
-module P = NCicParamod(EmptyC)
+module CB = NCicBlob.NCicBlob
+module P = NCicParamod
type state = P.state
let empty_state = P.empty_state
-let forward_infer_step s t ty =
+let size_of_state = P.size_of_state
+
+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.Incomparable | Terms.Invertible) -> true
+ | _, Terms.Var _,(Terms.Incomparable | Terms.Invertible) -> true
+ | _ -> false)
+ | _ -> false
+;;
+
+let forward_infer_step status metasenv subst context s t ty =
let bag = P.bag_of_state s in
- let bag,clause = P.mk_passive bag (t,ty) in
+ let saturate (t,ty) =
+ NCicBlob.saturate status metasenv subst context t ty in
+ if not_embeddable status subst context ty
+ then (debug (lazy ("theorem not embeddable")); s)
+ else
+ let bag,clause = P.mk_passive bag (saturate (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)
+ else P.forward_infer_step (P.replace_bag s bag) clause 0
+ else ((*print (lazy "not eq");*) s)
;;
let index_obj status s 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_step 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
+ forward_infer_step status [] [] [] s (NCic.Const nref) ty
| _ -> s
;;
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 _ -> []
let paramod status metasenv subst context s goal =
(* let stamp = Unix.gettimeofday () in *)
+ if not_embeddable status subst context (snd goal) then [] else
match P.nparamod ~useage:true ~max_steps:max_int
~timeout:(Unix.gettimeofday () +. 300.0) s goal with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
;;
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 _ -> []
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 ::tl) when eq = CB.eqP() -> true
| _ -> false
;;