-module EmptyC =
- struct
- let metasenv = []
- let subst = []
- let context = []
- end
-
-module CB = NCicBlob.NCicBlob(EmptyC)
-module P = NCicParamod(EmptyC)
-
-type state = P.state
-let empty_state = P.empty_state
-
-let forward_infer_step s t ty =
- let bag = P.bag_of_state s in
- 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)
-;;
-
-let index_obj s uri =
- let obj = NCicEnvironment.get_checked_obj 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
- | (_,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
-;;
-
-let demod rdb metasenv subst context s goal =
- (* 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
-;;
-
-let paramod rdb metasenv subst context s goal =
- (* let stamp = Unix.gettimeofday () in *)
- match P.nparamod ~useage:true ~max_steps:max_int
- ~timeout:(Unix.gettimeofday () +. 300.0) 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
-;;
-
-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
-;;
-
-let is_equation metasenv subst context ty =
- let hty, _, _ =
- NCicMetaSubst.saturate ~delta:0 metasenv subst context
- ty 0
- in match hty with
- | NCic.Appl (eq ::tl) when eq = CB.eqP -> true
- | _ -> false
-;;