open Printf
-let print ?(depth=0) s =
+let debug = ref false
+let debug_print ?(depth=0) s =
+ if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
+(* let print= debug_print *)
+ let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
-let noprint ?(depth=0) _ = ()
-let debug_print = noprint
+
+let debug_do f = if !debug then f () else ()
open Continuationals.Stack
open NTacStatus
module Ast = CicNotationPt
-
-(* ======================= statistics ========================= *)
-
let app_counter = ref 0
-module RHT = struct
- type t = NReference.reference
- let equal = (==)
- let compare = Pervasives.compare
- let hash = Hashtbl.hash
-end;;
-
-module RefHash = Hashtbl.Make(RHT);;
-
-type info = {
- nominations : int ref;
- uses: int ref;
-}
-
-let statistics: info RefHash.t = RefHash.create 503
-
-let incr_nominations tbl item =
- try
- let v = RefHash.find tbl item in incr v.nominations
- with Not_found ->
- RefHash.add tbl item {nominations = ref 1; uses = ref 0}
-
-let incr_uses tbl item =
- try
- let v = RefHash.find tbl item in incr v.uses
- with Not_found -> assert false
+(* =================================== paramod =========================== *)
+let auto_paramod ~params:(l,_) status goal =
+ let gty = get_goalty status goal in
+ let n,h,metasenv,subst,o = status#obj in
+ let status,t = term_of_cic_term status gty (ctx_of gty) in
+ let status, l =
+ List.fold_left
+ (fun (status, l) t ->
+ let status, t = disambiguate status (ctx_of gty) t None in
+ let status, ty = typeof status (ctx_of t) t in
+ let status, t = term_of_cic_term status t (ctx_of gty) in
+ let status, ty = term_of_cic_term status ty (ctx_of ty) in
+ (status, (t,ty) :: l))
+ (status,[]) l
+ in
+ match
+ NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
+ with
+ | [] -> raise (Error (lazy "no proof found",None))
+ | (pt, metasenv, subst)::_ ->
+ let status = status#set_obj (n,h,metasenv,subst,o) in
+ instantiate status goal (mk_cic_term (ctx_of gty) pt)
+;;
-let toref f tbl t =
- match t with
- | Ast.NRef n ->
- f tbl n
- | Ast.NCic _ (* local candidate *)
- | _ -> ()
+let auto_paramod_tac ~params status =
+ NTactics.distribute_tac (auto_paramod ~params) status
+;;
-let is_relevant tbl item =
- try
- let v = RefHash.find tbl item in
- if !(v.nominations) < 60 then true (* not enough info *)
- else if !(v.uses) = 0 then false
- else true
- with Not_found -> true
-
-let print_stat tbl =
- let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
- let relevance v = float !(v.uses) /. float !(v.nominations) in
- let vcompare (_,v1) (_,v2) =
- Pervasives.compare (relevance v1) (relevance v2) in
- let l = List.sort vcompare l in
- let vstring (a,v)=
- CicNotationPp.pp_term (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
- (string_of_float (relevance v)) ^
- "; uses = " ^ (string_of_int !(v.uses)) ^
- "; nom = " ^ (string_of_int !(v.nominations)) in
- lazy ("\n\nSTATISTICS:\n" ^
- String.concat "\n" (List.map vstring l))
-
-(* ======================= utility functions ========================= *)
+(*************** subsumption ****************)
module IntSet = Set.Make(struct type t = int let compare = compare end)
+(* exceptions *)
let get_sgoalty status g =
let _,_,metasenv,subst,_ = status#obj in
in closure IntSet.empty gl
;;
-(* we call a "fact" an object whose hypothesis occur in the goal
- or in types of goal-variables *)
-let branch status ty =
- let status, ty, metas = saturate ~delta:0 status ty in
- noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
- let g_metas = metas_of_term status ty in
- let clos = menv_closure status g_metas in
- (* let _,_,metasenv,_,_ = status#obj in *)
- let menv =
- List.fold_left
- (fun acc m ->
- let _, m = term_of_cic_term status m (ctx_of m) in
- match m with
- | NCic.Meta(i,_) -> IntSet.add i acc
- | _ -> assert false)
- IntSet.empty metas
- in
- (* IntSet.subset menv clos *)
- IntSet.cardinal(IntSet.diff menv clos)
-
-let is_a_fact status ty = branch status ty = 0
-
-let is_a_fact_obj s uri =
- let obj = NCicEnvironment.get_checked_obj uri in
- match obj with
- | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
- is_a_fact s (mk_cic_term [] ty)
-(* aggiungere i costruttori *)
- | _ -> false
-
-let is_a_fact_ast status subst metasenv ctx cand =
- debug_print ~depth:0
- (lazy ("------- checking " ^ CicNotationPp.pp_term cand));
- let status, t = disambiguate status ctx ("",0,cand) None in
- let status,t = term_of_cic_term status t ctx in
- let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- is_a_fact status (mk_cic_term ctx ty)
-
-let current_goal status =
- let open_goals = head_goals status#stack in
- assert (List.length open_goals = 1);
- let open_goal = List.hd open_goals in
- let gty = get_goalty status open_goal in
- let ctx = ctx_of gty in
- open_goal, ctx, gty
-
-let height_of_ref (NReference.Ref (uri, x)) =
- match x with
- | NReference.Decl
- | NReference.Ind _
- | NReference.Con _
- | NReference.CoFix _ ->
- let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
- height
- | NReference.Def h -> h
- | NReference.Fix (_,_,h) -> h
-;;
-
-(*************************** height functions ********************************)
-let fast_height_of_term t =
- let h = ref 0 in
- let rec aux =
- function
- NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
- | NCic.Meta _ -> ()
- | NCic.Rel _
- | NCic.Sort _ -> ()
- | NCic.Implicit _ -> assert false
- | NCic.Const nref ->
-(*
- prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
- ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
-*)
- h := max !h (height_of_ref nref)
- | NCic.Prod (_,t1,t2)
- | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
- | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
- | NCic.Appl l -> List.iter aux l
- | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
- in
- aux t; !h
-;;
-
-let height_of_goal g status =
- let ty = get_goalty status g in
- let context = ctx_of ty in
- let _, ty = term_of_cic_term status ty (ctx_of ty) in
- let h = ref (fast_height_of_term ty) in
- List.iter
- (function
- | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
- | _, NCic.Def (bo,ty) ->
- h := max !h (fast_height_of_term ty);
- h := max !h (fast_height_of_term bo);
- )
- context;
- !h
-;;
-
-let height_of_goals status =
- let open_goals = head_goals status#stack in
- assert (List.length open_goals > 0);
- let h = ref 1 in
- List.iter
- (fun open_goal ->
- h := max !h (height_of_goal open_goal status))
- open_goals;
- debug_print (lazy ("altezza sequente: " ^ string_of_int !h));
- !h
-;;
-
-(* =============================== paramod =========================== *)
-let solve f status eq_cache goal =
-(*
- let f =
- if fast then NCicParamod.fast_eq_check
- else NCicParamod.paramod in
-*)
- let n,h,metasenv,subst,o = status#obj in
- let gname, ctx, gty = List.assoc goal metasenv in
- let gty = NCicUntrusted.apply_subst subst ctx gty in
- let build_status (pt, _, metasenv, subst) =
- try
- debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
- let stamp = Unix.gettimeofday () in
- let metasenv, subst, pt, pty =
- (* NCicRefiner.typeof status
- (* (status#set_coerc_db NCicCoercion.empty_db) *)
- metasenv subst ctx pt None in
- print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
- debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
- let metasenv, subst =
- NCicUnification.unify status metasenv subst ctx gty pty *)
- NCicRefiner.typeof
- (status#set_coerc_db NCicCoercion.empty_db)
- metasenv subst ctx pt (Some gty)
- in
- debug_print (lazy (Printf.sprintf "Refined in %fs"
- (Unix.gettimeofday() -. stamp)));
- let status = status#set_obj (n,h,metasenv,subst,o) in
- let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
- let subst = (goal,(gname,ctx,pt,pty)) :: subst in
- Some (status#set_obj (n,h,metasenv,subst,o))
- with
- NCicRefiner.RefineFailure msg
- | NCicRefiner.Uncertain msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
- snd (Lazy.force msg) ^
- "\n in the environment\n" ^
- NCicPp.ppmetasenv subst metasenv)); None
- | NCicRefiner.AssertFailure msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- Lazy.force msg ^
- "\n in the environment\n" ^
- NCicPp.ppmetasenv subst metasenv)); None
- | _ -> None
- in
- HExtlib.filter_map build_status
- (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
-;;
-
-let fast_eq_check eq_cache status (goal:int) =
- match solve NCicParamod.fast_eq_check status eq_cache goal with
- | [] -> raise (Error (lazy "no proof found",None))
- | s::_ -> s
-;;
-
-let dist_fast_eq_check eq_cache s =
- NTactics.distribute_tac (fast_eq_check eq_cache) s
-;;
-
-let auto_eq_check eq_cache status =
- try
- let s = dist_fast_eq_check eq_cache status in
- [s]
- with
- | Error _ -> debug_print (lazy ("no paramod proof found"));[]
-;;
-
-let index_local_equations eq_cache status =
- debug_print (lazy "indexing equations");
- let open_goals = head_goals status#stack in
- let open_goal = List.hd open_goals in
- let ngty = get_goalty status open_goal in
- let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
- let c = ref 0 in
- List.fold_left
- (fun eq_cache _ ->
- c:= !c+1;
- let t = NCic.Rel !c in
- try
- let ty = NCicTypeChecker.typeof [] [] ctx t in
- if is_a_fact status (mk_cic_term ctx ty) then
- (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
- NCicParamod.forward_infer_step eq_cache t ty)
- else
- (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
- eq_cache)
- with
- | NCicTypeChecker.TypeCheckerFailure _
- | NCicTypeChecker.AssertFailure _ -> eq_cache)
- eq_cache ctx
-;;
-
-let fast_eq_check_tac ~params s =
- let unit_eq = index_local_equations s#eq_cache s in
- dist_fast_eq_check unit_eq s
-;;
-
-let paramod eq_cache status goal =
- match solve NCicParamod.paramod status eq_cache goal with
- | [] -> raise (Error (lazy "no proof found",None))
- | s::_ -> s
-;;
-
-let paramod_tac ~params s =
- let unit_eq = index_local_equations s#eq_cache s in
- NTactics.distribute_tac (paramod unit_eq) s
-;;
-
-let demod eq_cache status goal =
- match solve NCicParamod.demod status eq_cache goal with
- | [] -> raise (Error (lazy "no progress",None))
- | s::_ -> s
-;;
-
-let demod_tac ~params s =
- let unit_eq = index_local_equations s#eq_cache s in
- NTactics.distribute_tac (demod unit_eq) s
-;;
-
-(*
-let fast_eq_check_tac_all ~params eq_cache status =
- let g,_,_ = current_goal status in
- let allstates = fast_eq_check_all status eq_cache g in
- let pseudo_low_tac s _ _ = s in
- let pseudo_low_tactics =
- List.map pseudo_low_tac allstates
- in
- List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
-;;
-*)
-
-(*
-let demod status eq_cache goal =
- let n,h,metasenv,subst,o = status#obj in
- let gname, ctx, gty = List.assoc goal metasenv in
- let gty = NCicUntrusted.apply_subst subst ctx gty in
-
-let demod_tac ~params s =
- let unit_eq = index_local_equations s#eq_cache s in
- dist_fast_eq_check unit_eq s
-*)
-
-(*************** subsumption ****************)
-
let close_wrt_context =
List.fold_left
(fun ty ctx_entry ->
- match ctx_entry with
+ match ctx_entry with
| name, NCic.Decl t -> NCic.Prod(name,t,ty)
| name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
;;
let _,args =
List.fold_left
(fun (n,l) ctx_entry ->
- match ctx_entry with
- | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
- | name, NCic.Def(bo, _) -> n+1,l)
+ match ctx_entry with
+ | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
+ | name, NCic.Def(bo, _) -> n+1,l)
(k,[]) ctx in
args
(fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
let ikind = NCicUntrusted.kind_of_meta iattr in
let metasenv,j,instance,ty =
- NCicMetaSubst.mk_meta ~attrs:iattr
- metasenv ctx ~with_type:ty ikind in
+ NCicMetaSubst.mk_meta ~attrs:iattr
+ metasenv ctx ~with_type:ty ikind in
let s_entry = i,(iattr, ctx, instance, ty) in
let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
- metasenv,s_entry::subst)
+ metasenv,s_entry::subst)
(metasenv,[]) metasenv
(* close metasenv returns a ground instance of all the metas in the
let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
List.fold_left
(fun (subst,objs) (i,(iattr,ctx,ty)) ->
- let ty = NCicUntrusted.apply_subst subst ctx ty in
+ let ty = NCicUntrusted.apply_subst subst ctx ty in
let ctx =
- NCicUntrusted.apply_subst_context ~fix_projections:true
- subst ctx in
- let (uri,_,_,_,obj) as okind =
- constant_for_meta ctx ty i in
- try
- NCicEnvironment.check_and_add_obj okind;
- let iref = NReference.reference_of_spec uri NReference.Decl in
- let iterm =
- let args = args_for_context ctx in
- if args = [] then NCic.Const iref
- else NCic.Appl(NCic.Const iref::args)
- in
+ NCicUntrusted.apply_subst_context ~fix_projections:true
+ subst ctx in
+ let (uri,_,_,_,obj) as okind =
+ constant_for_meta ctx ty i in
+ try
+ NCicEnvironment.check_and_add_obj okind;
+ let iref = NReference.reference_of_spec uri NReference.Decl in
+ let iterm =
+ let args = args_for_context ctx in
+ if args = [] then NCic.Const iref
+ else NCic.Appl(NCic.Const iref::args)
+ in
(* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
- let s_entry = i, ([], ctx, iterm, ty)
- in s_entry::subst,okind::objs
- with _ -> assert false)
+ let s_entry = i, ([], ctx, iterm, ty)
+ in s_entry::subst,okind::objs
+ with _ -> assert false)
(subst,[]) metasenv
;;
try
List.iter
(fun i ->
- let (_, ctx, t, _) = List.assoc i subst in
- debug_print (lazy (NCicPp.ppterm ctx [] [] t));
- List.iter
- (fun (uri,_,_,_,_) as obj ->
- NCicEnvironment.invalidate_item (`Obj (uri, obj)))
- objs;
- ())
+ let (_, ctx, t, _) = List.assoc i subst in
+ debug_print (lazy (NCicPp.ppterm ctx [] [] t));
+ List.iter
+ (fun (uri,_,_,_,_) as obj ->
+ NCicEnvironment.invalidate_item (`Obj (uri, obj)))
+ objs;
+ ())
gl
with
Not_found -> assert false
let rec aux k = function
(* TODO: local context *)
| NCic.Meta (j,lc) when i = j ->
- (match args with
- | [] -> NCic.Rel 1
- | _ -> let args =
- List.map (NCicSubstitution.subst_meta lc) args in
- NCic.Appl(NCic.Rel k::args))
+ (match args with
+ | [] -> NCic.Rel 1
+ | _ -> let args =
+ List.map (NCicSubstitution.subst_meta lc) args in
+ NCic.Appl(NCic.Rel k::args))
| NCic.Meta (j,lc) as m ->
(match lc with
_,NCic.Irl _ -> m
(fun ty (i,(iattr,ctx,mty)) ->
let mty = NCicUntrusted.apply_subst subst ctx mty in
let ctx =
- NCicUntrusted.apply_subst_context ~fix_projections:true
- subst ctx in
+ NCicUntrusted.apply_subst_context ~fix_projections:true
+ subst ctx in
let cty = close_wrt_context mty ctx in
let name = "foo"^(string_of_int i) in
let ty = NCicSubstitution.lift 1 ty in
ctx,ty
;;
-(****************** smart application ********************)
-let saturate_to_ref metasenv subst ctx nref ty =
- let height = height_of_ref nref in
- let rec aux metasenv ty args =
- let ty,metasenv,moreargs =
- NCicMetaSubst.saturate ~delta:height metasenv subst ctx ty 0 in
- match ty with
- | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
- when nre<>nref ->
- let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
- aux metasenv bo (args@moreargs)
- | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
- when nre<>nref ->
- let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
- aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
- | _ -> ty,metasenv,(args@moreargs)
+
+(* =================================== auto =========================== *)
+(****************** AUTO ********************
+
+let calculate_timeout flags =
+ if flags.timeout = 0. then
+ (debug_print (lazy "AUTO WITH NO TIMEOUT");
+ {flags with timeout = infinity})
+ else
+ flags
+;;
+let is_equational_case goalty flags =
+ let ensure_equational t =
+ if is_an_equational_goal t then true
+ else false
in
- aux metasenv ty []
+ (flags.use_paramod && is_an_equational_goal goalty) ||
+ (flags.use_only_paramod && ensure_equational goalty)
+;;
-let smart_apply t unit_eq status g =
- let n,h,metasenv,subst,o = status#obj in
- let gname, ctx, gty = List.assoc g metasenv in
- (* let ggty = mk_cic_term context gty in *)
- let status, t = disambiguate status ctx t None in
- let status,t = term_of_cic_term status t ctx in
- let _,_,metasenv,subst,_ = status#obj in
- let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- let ty,metasenv,args =
- match gty with
- | NCic.Const(nref)
- | NCic.Appl(NCic.Const(nref)::_) ->
- saturate_to_ref metasenv subst ctx nref ty
- | _ ->
- NCicMetaSubst.saturate metasenv subst ctx ty 0 in
- let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
- let status = status#set_obj (n,h,metasenv,subst,o) in
- let pterm = if args=[] then t else
- match t with
- | NCic.Appl l -> NCic.Appl(l@args)
- | _ -> NCic.Appl(t::args)
+type menv = Cic.metasenv
+type subst = Cic.substitution
+type goal = ProofEngineTypes.goal * int * AutoTypes.sort
+let candidate_no = ref 0;;
+type candidate = int * Cic.term Lazy.t
+type cache = AutoCache.cache
+
+type fail =
+ (* the goal (mainly for depth) and key of the goal *)
+ goal * AutoCache.cache_key
+type op =
+ (* goal has to be proved *)
+ | D of goal
+ (* goal has to be cached as a success obtained using candidate as the first
+ * step *)
+ | S of goal * AutoCache.cache_key * candidate * int
+type elem =
+ (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
+ menv * subst * int * op list * op list * fail list
+type status =
+ (* list of computations that may lead to the solution: all op list will
+ * end with the same (S(g,_)) *)
+ elem list
+type auto_result =
+ (* menv, subst, alternatives, tables, cache *)
+ | Proved of menv * subst * elem list * AutomationCache.tables * cache
+ | Gaveup of AutomationCache.tables * cache
+
+
+(* the status exported to the external observer *)
+type auto_status =
+ (* context, (goal,candidate) list, and_list, history *)
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
+ (int * Cic.term * int) list * Cic.term Lazy.t list
+
+let d_prefix l =
+ let rec aux acc = function
+ | (D g)::tl -> aux (acc@[g]) tl
+ | _ -> acc
in
- noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
- noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
- let eq_coerc =
- let uri =
- NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
- let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
- NCic.Const ref
+ aux [] l
+;;
+
+let calculate_goal_ty (goalno,_,_) s m =
+ try
+ let _,cc,goalty = CicUtil.lookup_meta goalno m in
+ (* XXX applicare la subst al contesto? *)
+ Some (cc, CicMetaSubst.apply_subst s goalty)
+ with CicUtil.Meta_not_found i when i = goalno -> None
+;;
+
+let calculate_closed_goal_ty (goalno,_,_) s =
+ try
+ let cc,_,goalty = List.assoc goalno s in
+ (* XXX applicare la subst al contesto? *)
+ Some (cc, CicMetaSubst.apply_subst s goalty)
+ with Not_found ->
+ None
+;;
+
+let pp_status ctx status =
+ if debug then
+ let names = Utils.names_of_context ctx in
+ let pp x =
+ let x =
+ ProofEngineReduction.replace
+ ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
+ ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
+ in
+ CicPp.pp x names
in
- let smart =
- NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
- let smart = mk_cic_term ctx smart in
- try
- let status = instantiate status g smart in
- let _,_,metasenv,subst,_ = status#obj in
- let _,ctx,jty = List.assoc j metasenv in
- let jty = NCicUntrusted.apply_subst subst ctx jty in
- debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
- fast_eq_check unit_eq status j
- with
- | NCicEnvironment.ObjectNotFound s as e ->
- raise (Error (lazy "eq_coerc non yet defined",Some e))
- | Error _ as e -> debug_print (lazy "error"); raise e
+ let string_of_do m s (gi,_,_ as g) d =
+ match calculate_goal_ty g s m with
+ | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
+ | None -> Printf.sprintf "D(%d, _, %d)" gi d
+ in
+ let string_of_s m su k (ci,ct) gi =
+ Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
+ in
+ let string_of_ol m su l =
+ String.concat " | "
+ (List.map
+ (function
+ | D (g,d,s) -> string_of_do m su (g,d,s) d
+ | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
+ l)
+ in
+ let string_of_fl m s fl =
+ String.concat " | "
+ (List.map (fun ((i,_,_),ty) ->
+ Printf.sprintf "(%d, %s)" i (pp ty)) fl)
+ in
+ let rec aux = function
+ | [] -> ()
+ | (m,s,_,_,ol,fl)::tl ->
+ Printf.eprintf "< [%s] ;;; [%s]>\n"
+ (string_of_ol m s ol) (string_of_fl m s fl);
+ aux tl
+ in
+ Printf.eprintf "-------------------------- status -------------------\n";
+ aux status;
+ Printf.eprintf "-----------------------------------------------------\n";
+;;
+
+let auto_status = ref [] ;;
+let auto_context = ref [];;
+let in_pause = ref false;;
+let pause b = in_pause := b;;
+let cond = Condition.create ();;
+let mutex = Mutex.create ();;
+let hint = ref None;;
+let prune_hint = ref [];;
+
+let step _ = Condition.signal cond;;
+let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+ prune_hint := hint :: !prune_hint
+;;
-let smart_apply_tac t s =
- let unit_eq = index_local_equations s#eq_cache s in
- NTactics.distribute_tac (smart_apply t unit_eq) s
+let check_pause _ =
+ if !in_pause then
+ begin
+ Mutex.lock mutex;
+ Condition.wait cond mutex;
+ Mutex.unlock mutex
+ end
+;;
-let smart_apply_auto t eq_cache =
- NTactics.distribute_tac (smart_apply t eq_cache)
+let get_auto_status _ =
+ let status = !auto_status in
+ let and_list,elems,last =
+ match status with
+ | [] -> [],[],[]
+ | (m,s,_,don,gl,fail)::tl ->
+ let and_list =
+ HExtlib.filter_map
+ (fun (id,d,_ as g) ->
+ match calculate_goal_ty g s m with
+ | Some (_,x) -> Some (id,x,d) | None -> None)
+ (d_goals gl)
+ in
+ let rows =
+ (* these are the S goalsin the or list *)
+ let orlist =
+ List.map
+ (fun (m,s,_,don,gl,fail) ->
+ HExtlib.filter_map
+ (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
+ (List.rev don @ gl))
+ status
+ in
+ (* this function eats id from a list l::[id,x] returning x, l *)
+ let eat_tail_if_eq id l =
+ let rec aux (s, l) = function
+ | [] -> s, l
+ | ((id1,_,_),k1,c)::tl when id = id1 ->
+ (match s with
+ | None -> aux (Some c,l) tl
+ | Some _ -> assert false)
+ | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
+ in
+ let c, l = aux (None, []) l in
+ c, List.rev l
+ in
+ let eat_in_parallel id l =
+ let rec aux (b,eaten, new_l as acc) l =
+ match l with
+ | [] -> acc
+ | l::tl ->
+ match eat_tail_if_eq id l with
+ | None, l -> aux (b@[false], eaten, new_l@[l]) tl
+ | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
+ in
+ aux ([],[],[]) l
+ in
+ let rec eat_all rows l =
+ match l with
+ | [] -> rows
+ | elem::or_list ->
+ match List.rev elem with
+ | ((to_eat,depth,_),k,_)::next_lunch ->
+ let b, eaten, l = eat_in_parallel to_eat l in
+ let eaten = HExtlib.list_uniq eaten in
+ let eaten = List.rev eaten in
+ let b = true (* List.hd (List.rev b) *) in
+ let rows = rows @ [to_eat,k,b,depth,eaten] in
+ eat_all rows l
+ | [] -> eat_all rows or_list
+ in
+ eat_all [] (List.rev orlist)
+ in
+ let history =
+ HExtlib.filter_map
+ (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
+ gl
+ in
+(* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
+ and_list, rows, history
+ in
+ !auto_context, elems, and_list, last
+;;
+(* Works if there is no dependency over proofs *)
+let is_a_green_cut goalty =
+ CicUtil.is_meta_closed goalty
+;;
+let rec first_s = function
+ | (D _)::tl -> first_s tl
+ | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
+ | [] -> None
+;;
+let list_union l1 l2 =
+ (* TODO ottimizzare compare *)
+ HExtlib.list_uniq (List.sort compare (l1 @ l1))
+;;
+let rec eq_todo l1 l2 =
+ match l1,l2 with
+ | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
+ | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
+ when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
+ if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
+ | [],[] -> true
+ | _ -> false
+;;
+let eat_head todo id fl orlist =
+ let rec aux acc = function
+ | [] -> [], acc
+ | (m, s, _, _, todo1, fl1)::tl as orlist ->
+ let rec aux1 todo1 =
+ match first_s todo1 with
+ | None -> orlist, acc
+ | Some (((gno,_,_),_,_,_), todo11) ->
+ (* TODO confronto tra todo da ottimizzare *)
+ if gno = id && eq_todo todo11 todo then
+ aux (list_union fl1 acc) tl
+ else
+ aux1 todo11
+ in
+ aux1 todo1
+ in
+ aux fl orlist
+;;
+let close_proof p ty menv context =
+ let metas =
+ List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
+ in
+ let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
+ naif_closure p menv context
+;;
+(* XXX capire bene quando aggiungere alla cache *)
+let add_to_cache_and_del_from_orlist_if_green_cut
+ g s m cache key todo orlist fl ctx size minsize
+=
+ let cache = cache_remove_underinspection cache key in
+ (* prima per fare la irl usavamo il contesto vero e proprio e non quello
+ * canonico! XXX *)
+ match calculate_closed_goal_ty g s with
+ | None -> assert false
+ | Some (canonical_ctx , gty) ->
+ let goalno,depth,sort = g in
+ let irl = mk_irl canonical_ctx in
+ let goal = Cic.Meta(goalno, irl) in
+ let proof = CicMetaSubst.apply_subst s goal in
+ let green_proof, closed_proof =
+ let b = is_a_green_cut proof in
+ if not b then
+ b, (* close_proof proof gty m ctx *) proof
+ else
+ b, proof
+ in
+ debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
+ if is_a_green_cut key then
+ (* if the initia goal was closed, we cut alternatives *)
+ let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
+ let orlist, fl = eat_head todo goalno fl orlist in
+ let cache =
+ if size < minsize then
+ (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
+ else
+ (* if the proof is closed we cache it *)
+ if green_proof then cache_add_success cache key proof
+ else (* cache_add_success cache key closed_proof *)
+ (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
+ in
+ cache, orlist, fl, true
+ else
+ let cache =
+ debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
+ if size < minsize then
+ (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
+ (* if the substituted goal and the proof are closed we cache it *)
+ if is_a_green_cut gty then
+ if green_proof then cache_add_success cache gty proof
+ else (* cache_add_success cache gty closed_proof *)
+ (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
+ else (*
+ try
+ let ty, _ =
+ CicTypeChecker.type_of_aux' ~subst:s
+ m ctx closed_proof CicUniv.oblivion_ugraph
+ in
+ if is_a_green_cut ty then
+ cache_add_success cache ty closed_proof
+ else cache
+ with
+ | CicTypeChecker.TypeCheckerFailure _ ->*)
+ (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
+ in
+ cache, orlist, fl, false
+;;
+let close_failures (fl : fail list) (cache : cache) =
+ List.fold_left
+ (fun cache ((gno,depth,_),gty) ->
+ if CicUtil.is_meta_closed gty then
+ ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
+ cache_add_failure cache gty depth)
+ else
+ cache)
+ cache fl
+;;
+let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
+ let entry = goalno, (canonical_ctx, t,ty) in
+ assert_subst_are_disjoint subst [entry];
+ let subst = entry :: subst in
+
+ let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
-(****************** types **************)
+ subst, metasenv
+;;
+let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
+ None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
+;;
-type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
+let equational_case
+ tables cache depth fake_proof goalno goalty subst context
+ flags
+=
+ let active,passive,bag = tables in
+ let ppterm = ppterm context in
+ let status = (fake_proof,goalno) in
+ if flags.use_only_paramod then
+ begin
+ debug_print (lazy ("PARAMODULATION SU: " ^
+ string_of_int goalno ^ " " ^ ppterm goalty ));
+ let goal_steps, saturation_steps, timeout =
+ max_int,max_int,flags.timeout
+ in
+ match
+ Saturation.given_clause bag status active passive
+ goal_steps saturation_steps timeout
+ with
+ | None, active, passive, bag ->
+ [], (active,passive,bag), cache, flags
+ | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+ passive,bag ->
+ assert_subst_are_disjoint subst subst';
+ let subst = subst@subst' in
+ let open_goals =
+ order_new_goals metasenv subst open_goals ppterm
+ in
+ let open_goals =
+ List.map (fun (x,sort) -> x,depth-1,sort) open_goals
+ in
+ incr candidate_no;
+ [(!candidate_no,proof),metasenv,subst,open_goals],
+ (active,passive,bag), cache, flags
+ end
+ else
+ begin
+ debug_print (lazy ("NARROWING DEL GOAL: " ^
+ string_of_int goalno ^ " " ^ ppterm goalty ));
+ let goal_steps, saturation_steps, timeout =
+ 1,0,flags.timeout
+ in
+ match
+ Saturation.solve_narrowing bag status active passive goal_steps
+ with
+ | None, active, passive, bag ->
+ [], (active,passive,bag), cache, flags
+ | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
+ passive,bag ->
+ assert_subst_are_disjoint subst subst';
+ let subst = subst@subst' in
+ let open_goals =
+ order_new_goals metasenv subst open_goals ppterm
+ in
+ let open_goals =
+ List.map (fun (x,sort) -> x,depth-1,sort) open_goals
+ in
+ incr candidate_no;
+ [(!candidate_no,proof),metasenv,subst,open_goals],
+ (active,passive,bag), cache, flags
+ end
+(*
+ begin
+ let params = ([],["use_context","false"]) in
+ let automation_cache = {
+ AutomationCache.tables = tables ;
+ AutomationCache.univ = Universe.empty; }
+ in
+ try
+ let ((_,metasenv,subst,_,_,_),open_goals) =
-(* cartesian: term set list -> term list set *)
-let rec cartesian =
- function
- [] -> NDiscriminationTree.TermListSet.empty
- | [l] ->
- NDiscriminationTree.TermSet.fold
- (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
- | he::tl ->
- let rest = cartesian tl in
- NDiscriminationTree.TermSet.fold
- (fun x acc ->
- NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
- ) he NDiscriminationTree.TermListSet.empty
-;;
-
-(* all_keys_of_cic_type: term -> term set *)
-let all_keys_of_cic_type metasenv subst context ty =
- let saturate ty =
- (* Here we are dropping the metasenv, but this should not raise any
- exception (hopefully...) *)
- let ty,_,hyps =
- NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
+ solve_rewrite ~params ~automation_cache
+ (fake_proof, goalno)
+ in
+ let proof = lazy (Cic.Meta (-1,[])) in
+ [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
+ with ProofEngineTypes.Fail _ -> [], tables, cache, flags
+(*
+ let res = Saturation.all_subsumed bag status active passive in
+ let res' =
+ List.map
+ (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
+ assert_subst_are_disjoint subst subst';
+ let subst = subst@subst' in
+ let open_goals =
+ order_new_goals metasenv subst open_goals ppterm
+ in
+ let open_goals =
+ List.map (fun (x,sort) -> x,depth-1,sort) open_goals
+ in
+ incr candidate_no;
+ (!candidate_no,proof),metasenv,subst,open_goals)
+ res
+ in
+ res', (active,passive,bag), cache, flags
+*)
+ end
+*)
+;;
+
+let sort_new_elems =
+ List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
+ let p1 = List.length (prop_only l1) in
+ let p2 = List.length (prop_only l2) in
+ if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
+;;
+
+
+let try_candidate dbd
+ goalty tables subst fake_proof goalno depth context cand
+=
+ let ppterm = ppterm context in
+ try
+ let actives, passives, bag = tables in
+ let (_,metasenv,subst,_,_,_), open_goals =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:cand)
+ (fake_proof,goalno)
+ in
+ let tables = actives, passives,
+ Equality.push_maxmeta bag
+ (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
+ in
+ debug_print (lazy (" OK: " ^ ppterm cand));
+ let metasenv = CicRefine.pack_coercion_metasenv metasenv in
+ let open_goals = order_new_goals metasenv subst open_goals ppterm in
+ let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
+ incr candidate_no;
+ Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
+ with
+ | ProofEngineTypes.Fail s -> None,tables
+ | CicUnification.Uncertain s -> None,tables
+;;
+
+let applicative_case dbd
+ tables depth subst fake_proof goalno goalty metasenv context
+ signature universe cache flags
+=
+ (* let goalty_aux =
+ match goalty with
+ | Cic.Appl (hd::tl) ->
+ Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+ | _ -> goalty
+ in *)
+ let goalty_aux = goalty in
+ let candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty_aux
in
- ty,List.length hyps
- in
- let rec aux ty =
- match ty with
- NCic.Appl (he::tl) ->
- let tl' =
- List.map (fun ty ->
- let wty = NCicReduction.whd ~delta:0 ~subst context ty in
- if ty = wty then
- NDiscriminationTree.TermSet.add ty (aux ty)
- else
- NDiscriminationTree.TermSet.union
- (NDiscriminationTree.TermSet.add ty (aux ty))
- (NDiscriminationTree.TermSet.add wty (aux wty))
- ) tl
- in
- NDiscriminationTree.TermListSet.fold
- (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
- (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
- NDiscriminationTree.TermSet.empty
- | _ -> NDiscriminationTree.TermSet.empty
- in
- let ty,ity = saturate ty in
- let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in
- if ty = wty then
- [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
- else
- [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
- iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
+ (* if the goal is an equality we skip the congruence theorems
+ let candidates =
+ if is_equational_case goalty flags
+ then List.filter not_default_eq_term candidates
+ else candidates
+ in *)
+ let candidates = List.filter (only signature context metasenv) candidates
+ in
+ let tables, elems =
+ List.fold_left
+ (fun (tables,elems) cand ->
+ match
+ try_candidate dbd goalty
+ tables subst fake_proof goalno depth context cand
+ with
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) candidates
+ in
+ let elems = sort_new_elems elems in
+ elems, tables, cache
;;
-let all_keys_of_type status t =
- let _,_,metasenv,subst,_ = status#obj in
- let context = ctx_of t in
- let status, t = apply_subst status context t in
- let keys =
- all_keys_of_cic_type metasenv subst context
- (snd (term_of_cic_term status t context))
- in
- status,
- List.map
- (fun (intros,keys) ->
- intros,
- NDiscriminationTree.TermSet.fold
- (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
- keys Ncic_termSet.empty
- ) keys
+let try_smart_candidate dbd
+ goalty tables subst fake_proof goalno depth context cand
+=
+ let ppterm = ppterm context in
+ try
+ let params = ([],[]) in
+ let automation_cache = {
+ AutomationCache.tables = tables ;
+ AutomationCache.univ = Universe.empty; }
+ in
+ debug_print (lazy ("candidato per " ^ string_of_int goalno
+ ^ ": " ^ CicPp.ppterm cand));
+(*
+ let (_,metasenv,subst,_,_,_) = fake_proof in
+ prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
+*)
+ let ((_,metasenv,subst,_,_,_),open_goals) =
+ apply_smart ~dbd ~term:cand ~params ~automation_cache
+ (fake_proof, goalno)
+ in
+ let metasenv = CicRefine.pack_coercion_metasenv metasenv in
+ let open_goals = order_new_goals metasenv subst open_goals ppterm in
+ let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
+ incr candidate_no;
+ Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
+ with
+ | ProofEngineTypes.Fail s -> None,tables
+ | CicUnification.Uncertain s -> None,tables
+;;
+
+let smart_applicative_case dbd
+ tables depth subst fake_proof goalno goalty metasenv context signature
+ universe cache flags
+=
+ let goalty_aux =
+ match goalty with
+ | Cic.Appl (hd::tl) ->
+ Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
+ | _ -> goalty
+ in
+ let smart_candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty_aux
+ in
+ let candidates =
+ get_candidates flags.skip_trie_filtering universe cache goalty
+ in
+ let smart_candidates =
+ List.filter
+ (fun x -> not(List.mem x candidates)) smart_candidates
+ in
+ let debug_msg =
+ (lazy ("smart_candidates" ^ " = " ^
+ (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
+ debug_print debug_msg;
+ let candidates = List.filter (only signature context metasenv) candidates in
+ let smart_candidates =
+ List.filter (only signature context metasenv) smart_candidates
+ in
+(*
+ let penalty cand depth =
+ if only signature context metasenv cand then depth else ((prerr_endline (
+ "penalizzo " ^ CicPp.ppterm cand));depth -1)
+ in
+*)
+ let tables, elems =
+ List.fold_left
+ (fun (tables,elems) cand ->
+ match
+ try_candidate dbd goalty
+ tables subst fake_proof goalno depth context cand
+ with
+ | None, tables ->
+ (* if normal application fails we try to be smart *)
+ (match try_smart_candidate dbd goalty
+ tables subst fake_proof goalno depth context cand
+ with
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) candidates
+ in
+ let tables, smart_elems =
+ List.fold_left
+ (fun (tables,elems) cand ->
+ match
+ try_smart_candidate dbd goalty
+ tables subst fake_proof goalno depth context cand
+ with
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) smart_candidates
+ in
+ let elems = sort_new_elems (elems @ smart_elems) in
+ elems, tables, cache
;;
+let equational_and_applicative_case dbd
+ signature universe flags m s g gty tables cache context
+=
+ let goalno, depth, sort = g in
+ let fake_proof = mk_fake_proof m s g gty context in
+ if is_equational_case gty flags then
+ let elems,tables,cache, flags =
+ equational_case tables cache
+ depth fake_proof goalno gty s context flags
+ in
+ let more_elems, tables, cache =
+ if flags.use_only_paramod then
+ [],tables, cache
+ else
+ applicative_case dbd
+ tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ in
+ elems@more_elems, tables, cache, flags
+ else
+ let elems, tables, cache =
+ match LibraryObjects.eq_URI () with
+ | Some _ ->
+ smart_applicative_case dbd tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ | None ->
+ applicative_case dbd tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ in
+ elems, tables, cache, flags
+;;
+let rec condition_for_hint i = function
+ | [] -> false
+ | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
+ | _::tl -> condition_for_hint i tl
+;;
+let prunable_for_size flags s m todo =
+ let rec aux b = function
+ | (S _)::tl -> aux b tl
+ | (D (_,_,T))::tl -> aux b tl
+ | (D g)::tl ->
+ (match calculate_goal_ty g s m with
+ | None -> aux b tl
+ | Some (canonical_ctx, gty) ->
+ let gsize, _ =
+ Utils.weight_of_term
+ ~consider_metas:false ~count_metas_occurrences:true gty in
+ let newb = b || gsize > flags.maxgoalsizefactor in
+ aux newb tl)
+ | [] -> b
+ in
+ aux false todo
-let keys_of_type status orig_ty =
- (* Here we are dropping the metasenv (in the status), but this should not
- raise any exception (hopefully...) *)
- let _, ty, _ = saturate ~delta:max_int status orig_ty in
- let _, ty = apply_subst status (ctx_of ty) ty in
- let keys =
(*
- let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
- if orig_ty' <> orig_ty then
- let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
- [ty;ty']
- else
- [ty]
+let prunable ty todo =
+ let rec aux b = function
+ | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
+ | (D (_,_,T))::tl -> aux b tl
+ | D _::_ -> false
+ | [] -> b
+ in
+ aux false todo
+;;
*)
- [ty] in
-(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
+
+let prunable menv subst ty todo =
+ let rec aux = function
+ | (S(_,k,_,_))::tl ->
+ (match Equality.meta_convertibility_subst k ty menv with
+ | None -> aux tl
+ | Some variant ->
+ no_progress variant tl (* || aux tl*))
+ | (D (_,_,T))::tl -> aux tl
+ | _ -> false
+ and no_progress variant = function
+ | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
+ | D ((n,_,P) as g)::tl ->
+ (match calculate_goal_ty g subst menv with
+ | None -> no_progress variant tl
+ | Some (_, gty) ->
+ (match calculate_goal_ty g variant menv with
+ | None -> assert false
+ | Some (_, gty') ->
+ if gty = gty' then no_progress variant tl
+(*
+(prerr_endline (string_of_int n);
+ prerr_endline (CicPp.ppterm gty);
+ prerr_endline (CicPp.ppterm gty');
+ prerr_endline "---------- subst";
+ prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
+ prerr_endline "---------- variant";
+ prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
+ prerr_endline "---------- menv";
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ no_progress variant tl) *)
+ else false))
+ | _::tl -> no_progress variant tl
+ in
+ aux todo
+
+;;
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+ let s =
+ HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
+ in
+ List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint c l =
+ let prune = !prune_hint in
+ prune_hint := []; (* possible race... *)
+ if prune = [] then c,l
+ else
+ cache_reset_underinspection c,
+ List.filter (condition_for_prune_hint prune) l
+;;
+
+
+
+let
+ auto_all_solutions dbd tables universe cache context metasenv gl flags
+=
+ let signature =
+ List.fold_left
+ (fun set g ->
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
+ )
+ MetadataConstraints.UriManagerSet.empty gl
+ in
+ let goals = order_new_goals metasenv [] gl CicPp.ppterm in
+ let goals =
+ List.map
+ (fun (x,s) -> D (x,flags.maxdepth,s)) goals
+ in
+ let elems = [metasenv,[],1,[],goals,[]] in
+ let rec aux tables solutions cache elems flags =
+ match auto_main dbd tables context flags signature universe cache elems with
+ | Gaveup (tables,cache) ->
+ solutions,cache, tables
+ | Proved (metasenv,subst,others,tables,cache) ->
+ if Unix.gettimeofday () > flags.timeout then
+ ((subst,metasenv)::solutions), cache, tables
+ else
+ aux tables ((subst,metasenv)::solutions) cache others flags
+ in
+ let rc = aux tables [] cache elems flags in
+ match rc with
+ | [],cache,tables -> [],cache,tables
+ | solutions, cache,tables ->
+ let solutions =
+ HExtlib.filter_map
+ (fun (subst,newmetasenv) ->
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
+ in
+ if opened = [] then Some subst else None)
+ solutions
+ in
+ solutions,cache,tables
+;;
+
+(******************* AUTO ***************)
+
+
+let auto dbd flags metasenv tables universe cache context metasenv gl =
+ let initial_time = Unix.gettimeofday() in
+ let signature =
+ List.fold_left
+ (fun set g ->
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
+ )
+ MetadataConstraints.UriManagerSet.empty gl
+ in
+ let goals = order_new_goals metasenv [] gl CicPp.ppterm in
+ let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
+ let elems = [metasenv,[],1,[],goals,[]] in
+ match auto_main dbd tables context flags signature universe cache elems with
+ | Proved (metasenv,subst,_, tables,cache) ->
+ debug_print(lazy
+ ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+ Some (subst,metasenv), cache
+ | Gaveup (tables,cache) ->
+ debug_print(lazy
+ ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+ None,cache
+;;
+
+let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
+ let flags = flags_of_params params () in
+ let use_library = flags.use_library in
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library ~use_context:(not flags.skip_context)
+ automation_cache univ (proof, goal)
+ in
+ let _,metasenv,subst,_,_, _ = proof in
+ let _,context,goalty = CicUtil.lookup_meta goal metasenv in
+ let signature = MetadataQuery.signature_of metasenv goal in
+ let signature =
+ List.fold_left
+ (fun set t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph
+ in
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataConstraints.constants_of ty)
+ )
+ signature univ
+ in
+ let tables,cache =
+ if flags.close_more then
+ close_more
+ tables context (proof, goal)
+ (auto_all_solutions dbd) signature universe cache
+ else tables,cache in
+ let initial_time = Unix.gettimeofday() in
+ let (_,oldmetasenv,_,_,_, _) = proof in
+ hint := None;
+ let elem =
+ metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
+ in
+ match auto_main dbd tables context flags signature universe cache [elem] with
+ | Proved (metasenv,subst,_, tables,cache) ->
+ debug_print (lazy
+ ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
+ let proof,metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goal subst metasenv
+ in
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
+ | Gaveup (tables,cache) ->
+ debug_print
+ (lazy ("TIME:"^
+ string_of_float(Unix.gettimeofday()-.initial_time)));
+ raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
+;;
+*)
+
+(****************** types **************)
+type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
+
+let keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ let _, ty, _ = saturate ~delta:max_int status orig_ty in
+ let keys = [ty] in
let keys =
let _, ty = term_of_cic_term status ty (ctx_of ty) in
match ty with
- | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
- | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
+ | NCic.Const (NReference.Ref (_,NReference.Def h))
+ | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
when h > 0 ->
let _,ty,_= saturate status ~delta:(h-1) orig_ty in
ty::keys
status, keys
;;
-let all_keys_of_term status t =
- let status, orig_ty = typeof status (ctx_of t) t in
- all_keys_of_type status orig_ty
-;;
-
-let keys_of_term status t =
- let status, orig_ty = typeof status (ctx_of t) t in
- keys_of_type status orig_ty
-;;
-
let mk_th_cache status gl =
List.fold_left
(fun (status, acc) g ->
List.fold_left
(fun (status, i, idx) _ ->
let t = mk_cic_term ctx (NCic.Rel i) in
+ debug_print(lazy("indexing: "^ppterm status t));
let status, keys = keys_of_term status t in
- debug_print(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
let idx =
List.fold_left (fun idx k ->
InvRelDiscriminationTree.index idx k t) idx keys
replace c
;;
-let rm_from_th t c ty =
- let key_c = ctx_of t in
- if not (List.mem_assq key_c c) then assert false
- else
- let rec replace = function
- | [] -> []
- | (x, idx) :: tl when x == key_c ->
- (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
- | x :: tl -> x :: replace tl
- in
- replace c
-;;
-
let pp_idx status idx =
InvRelDiscriminationTree.iter idx
(fun k set ->
let search_in_th gty th =
let c = ctx_of gty in
let rec aux acc = function
- | [] -> (* Ncic_termSet.elements *) acc
+ | [] -> Ncic_termSet.elements acc
| (_::tl) as k ->
try
- let idx = List.assoc(*q*) k th in
+ let idx = List.assq k th in
let acc = Ncic_termSet.union acc
(InvRelDiscriminationTree.retrieve_unifiables idx gty)
in
type flags = {
do_types : bool; (* solve goals in Type *)
- last : bool; (* last goal: take first solution only *)
- candidates: Ast.term list option;
maxwidth : int;
maxsize : int;
maxdepth : int;
timeout : float;
}
-type cache =
- {facts : th_cache; (* positive results *)
- under_inspection : cic_term list * th_cache; (* to prune looping *)
- unit_eq : NCicParamod.state;
- trace: Ast.term list
- }
-
-let add_to_trace ~depth cache t =
- match t with
- | Ast.NRef _ ->
- debug_print ~depth (lazy ("Adding to trace: " ^ CicNotationPp.pp_term t));
- {cache with trace = t::cache.trace}
- | Ast.NCic _ (* local candidate *)
- | _ -> (*not an application *) cache
-
-let pptrace tr =
- (lazy ("Proof Trace: " ^ (String.concat ";"
- (List.map CicNotationPp.pp_term tr))))
-(* not used
-let remove_from_trace cache t =
- match t with
- | Ast.NRef _ ->
- (match cache.trace with
- | _::tl -> {cache with trace = tl}
- | _ -> assert false)
- | Ast.NCic _ (* local candidate *)
- | _ -> (*not an application *) cache *)
-
type sort = T | P
type goal = int * sort (* goal, depth, sort *)
type fail = goal * cic_term
exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
atoms of the input goals *)
-exception Proved of NTacStatus.tac_status * Ast.term list
+exception Proved of #NTacStatus.tac_status
(* let close_failures _ c = c;; *)
(* let prunable _ _ _ = false;; *)
(* let put_in_subst s _ _ _ = s;; *)
(* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
(* let cache_add_underinspection c _ _ = c;; *)
-
-let init_cache ?(facts=[]) ?(under_inspection=[],[])
- ?(unit_eq=NCicParamod.empty_state)
- ?(trace=[])
- _ =
- {facts = facts;
- under_inspection = under_inspection;
- unit_eq = unit_eq;
- trace = trace}
-
-let only signature _context candidate = true
-(*
- (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
- let candidate_ty =
- NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
- in
- let height = fast_height_of_term candidate_ty in
- let rc = signature >= height in
- if rc = false then
- debug_print (lazy ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
- ~metasenv:[] candidate ^ ": " ^ string_of_int height))
- else
- debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
- ~metasenv:[] candidate ^ ": " ^ string_of_int height));
-
- rc *)
-;;
+let equational_case _ _ _ _ _ _ = [];;
+let only _ _ _ = true;;
let candidate_no = ref 0;;
-let openg_no status = List.length (head_goals status#stack)
-
-let sort_candidates status ctx candidates =
- let _,_,metasenv,subst,_ = status#obj in
- let branch cand =
- let status,ct = disambiguate status ctx ("",0,cand) None in
- let status,t = term_of_cic_term status ct ctx in
- let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- let res = branch status (mk_cic_term ctx ty) in
- debug_print (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
- ^ (string_of_int res)));
- res
- in
- let candidates = List.map (fun t -> branch t,t) candidates in
- let candidates =
- List.sort (fun (a,_) (b,_) -> a - b) candidates in
- let candidates = List.map snd candidates in
- debug_print (lazy ("candidates =\n" ^ (String.concat "\n"
- (List.map CicNotationPp.pp_term candidates))));
- candidates
-
-let sort_new_elems l =
- List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
+let sort_new_elems l =
+ List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
+;;
-let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
+let try_candidate flags depth status t =
try
- debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
- let status =
- if smart= 0 then NTactics.apply_tac ("",0,t) status
- else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
- else (* smart = 2: both *)
- try NTactics.apply_tac ("",0,t) status
- with Error _ ->
- smart_apply_auto ("",0,t) eq_cache status
- in
-(*
- let og_no = openg_no status in
- if (* og_no > flags.maxwidth || *)
- ((depth + 1) = flags.maxdepth && og_no <> 0) then
- (debug_print ~depth (lazy "pruned immediately"); None)
- else *)
- (* useless
- let status, cict = disambiguate status ctx ("",0,t) None in
- let status,ct = term_of_cic_term status cict ctx in
- let _,_,metasenv,subst,_ = status#obj in
- let ty = NCicTypeChecker.typeof subst metasenv ctx ct in
- let res = branch status (mk_cic_term ctx ty) in
- if smart=1 && og_no > res then
- (print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
- ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
- print ~depth (lazy "strange application"); None)
- else *)
- (incr candidate_no;
- Some ((!candidate_no,t),status))
+ debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
+ let status = NTactics.apply_tac ("",0,t) status in
+ let open_goals = head_goals status#stack in
+ debug_print ~depth
+ (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
+ if List.length open_goals > flags.maxwidth ||
+ (depth = flags.maxdepth && open_goals <> []) then
+ (debug_print ~depth (lazy "pruned immediately"); None)
+ else
+ (incr candidate_no;
+ Some ((!candidate_no,t),status,open_goals))
with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
;;
-let sort_of subst metasenv ctx t =
- let ty = NCicTypeChecker.typeof subst metasenv ctx t in
- let metasenv',ty = NCicUnification.fix_sorts metasenv subst ty in
- assert (metasenv = metasenv');
- NCicTypeChecker.typeof subst metasenv ctx ty
-;;
-
-let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
-;;
-
-let perforate_small subst metasenv context t =
- let rec aux = function
- | NCic.Appl (hd::tl) ->
- let map t =
- let s = sort_of subst metasenv context t in
- match s with
- | NCic.Sort(NCic.Type [`Type,u])
- when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
- | _ -> aux t
- in
- NCic.Appl (hd::List.map map tl)
- | t -> t
- in
- aux t
-;;
-
-let get_cands retrieve_for diff empty gty weak_gty =
- let cands = retrieve_for gty in
- match weak_gty with
- | None -> cands, empty
- | Some weak_gty ->
- let more_cands = retrieve_for weak_gty in
- cands, diff more_cands cands
-;;
-
-let get_candidates ?(smart=true) depth flags status cache signature gty =
- let maxd = ((depth + 1) = flags.maxdepth) in
+let get_candidates status cache signature gty =
let universe = status#auto_cache in
- let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let _, raw_gty = term_of_cic_term status gty context in
- let raw_weak_gty, weak_gty =
- if smart then
- match raw_gty with
- | NCic.Appl _
- | NCic.Const _
- | NCic.Rel _ ->
- let weak = perforate_small subst metasenv context raw_gty in
- Some weak, Some (mk_cic_term context weak)
- | _ -> None,None
- else None,None
- in
- let global_cands, smart_global_cands =
- match flags.candidates with
- | Some l when (not maxd) -> l,[]
- | Some _
- | None ->
- let mapf s =
- let to_ast = function
- | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
- | NCic.Const _ -> None
- | _ -> assert false in
- HExtlib.filter_map
- to_ast (NDiscriminationTree.TermSet.elements s) in
- let g,l =
- get_cands
- (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe)
- NDiscriminationTree.TermSet.diff
- NDiscriminationTree.TermSet.empty
- raw_gty raw_weak_gty in
- mapf g, mapf l in
- let local_cands,smart_local_cands =
- let mapf s =
- let to_ast t =
- let _status, t = term_of_cic_term status t context
- in Ast.NCic t in
- List.map to_ast (Ncic_termSet.elements s) in
- let g,l =
- get_cands
- (fun ty -> search_in_th ty cache)
- Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
- mapf g, mapf l in
- sort_candidates status context (global_cands@local_cands),
- sort_candidates status context (smart_global_cands@smart_local_cands)
-;;
-
-(* old version
-let get_candidates ?(smart=true) status cache signature gty =
- let universe = status#auto_cache in
- let _,_,metasenv,subst,_ = status#obj in
- let context = ctx_of gty in
- let t_ast t =
- let _status, t = term_of_cic_term status t context
- in Ast.NCic t in
- let c_ast = function
- | NCic.Const r -> Ast.NRef r | _ -> assert false in
- let _, raw_gty = term_of_cic_term status gty context in
- let keys = all_keys_of_cic_term metasenv subst context raw_gty in
- (* we only keep those keys that do not require any intros for now *)
- let no_intros_keys = snd (List.hd keys) in
- let cands =
- NDiscriminationTree.TermSet.fold
- (fun ty acc ->
- NDiscriminationTree.TermSet.union acc
- (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe ty)
- ) no_intros_keys NDiscriminationTree.TermSet.empty in
-(* old code:
let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty in
-*)
- let local_cands =
- NDiscriminationTree.TermSet.fold
- (fun ty acc ->
- Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
- ) no_intros_keys Ncic_termSet.empty in
-(* old code:
- let local_cands = search_in_th gty cache in
-*)
- debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
- debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
- let together global local =
- List.map c_ast
- (List.filter (only signature context)
- (NDiscriminationTree.TermSet.elements global)) @
- List.map t_ast (Ncic_termSet.elements local) in
- let candidates = together cands local_cands in
- let candidates = sort_candidates status context candidates in
- let smart_candidates =
- if smart then
- match raw_gty with
- | NCic.Appl _
- | NCic.Const _
- | NCic.Rel _ ->
- let weak_gty = perforate_small subst metasenv context raw_gty in
- (*
- NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
- (List.length tl)) in *)
- let more_cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe weak_gty
- in
- let smart_cands =
- NDiscriminationTree.TermSet.diff more_cands cands in
- let cic_weak_gty = mk_cic_term context weak_gty in
- let more_local_cands = search_in_th cic_weak_gty cache in
- let smart_local_cands =
- Ncic_termSet.diff more_local_cands local_cands in
- together smart_cands smart_local_cands
- (* together more_cands more_local_cands *)
- | _ -> []
- else []
+ universe raw_gty
+ in
+ let cands =
+ List.filter (only signature context)
+ (NDiscriminationTree.TermSet.elements cands)
in
- let smart_candidates = sort_candidates status context smart_candidates in
- (* if smart then smart_candidates, []
- else candidates, [] *)
- candidates, smart_candidates
-;;
-
-let get_candidates ?(smart=true) flags status cache signature gty =
- match flags.candidates with
- | None -> get_candidates ~smart status cache signature gty
- | Some l -> l,[]
-;; *)
+ List.map (fun t ->
+ let _status, t = term_of_cic_term status t context in Ast.NCic t)
+ (search_in_th gty cache)
+ @
+ List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
+;;
let applicative_case depth signature status flags gty cache =
+ let tcache,_ = cache in
app_counter:= !app_counter+1;
- let _,_,metasenv,subst,_ = status#obj in
- let context = ctx_of gty in
- let tcache = cache.facts in
- let is_prod, is_eq =
- let status, t = term_of_cic_term status gty context in
- let t = NCicReduction.whd subst context t in
- match t with
- | NCic.Prod _ -> true, false
- | _ -> false, NCicParamod.is_equation metasenv subst context t
- in
- debug_print~depth (lazy (string_of_bool is_eq));
- (* old
- let candidates, smart_candidates =
- get_candidates ~smart:(not is_eq) depth
- flags status tcache signature gty in
- (* if the goal is an equation we avoid to apply unit equalities,
- since superposition should take care of them; refl is an
- exception since it prompts for convertibility *)
- let candidates =
- let test x = not (is_a_fact_ast status subst metasenv context x) in
- if is_eq then
- Ast.Ident("refl",None) ::List.filter test candidates
- else candidates in *)
- (* new *)
- let candidates, smart_candidates =
- get_candidates ~smart:true depth
- flags status tcache signature gty in
- (* if the goal is an equation we avoid to apply unit equalities,
- since superposition should take care of them; refl is an
- exception since it prompts for convertibility *)
- let candidates,smart_candidates =
- let test x = not (is_a_fact_ast status subst metasenv context x) in
- if is_eq then
- Ast.Ident("refl",None) ::List.filter test candidates,
- List.filter test smart_candidates
- else candidates,smart_candidates in
+ let candidates = get_candidates status tcache signature gty in
debug_print ~depth
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
- debug_print ~depth
- (lazy ("smart candidates: " ^
- string_of_int (List.length smart_candidates)));
- (*
- let sm = 0 in
- let smart_candidates = [] in *)
- let sm = if is_eq then 0 else 2 in
- let maxd = ((depth + 1) = flags.maxdepth) in
- let only_one = flags.last && maxd in
- debug_print (lazy ("only_one: " ^ (string_of_bool only_one)));
- debug_print (lazy ("maxd: " ^ (string_of_bool maxd)));
- let elems =
+ let elems =
List.fold_left
(fun elems cand ->
- if (only_one && (elems <> [])) then elems
- else
- if (maxd && not(is_prod) &
- not(is_a_fact_ast status subst metasenv context cand))
- then (debug_print (lazy "pruned: not a fact"); elems)
- else
- match try_candidate (~smart:sm)
- flags depth status cache.unit_eq context cand with
- | None -> elems
- | Some x -> x::elems)
+ match try_candidate flags depth status cand with
+ | None -> elems
+ | Some x -> x::elems)
[] candidates
in
- let more_elems =
- if only_one && elems <> [] then elems
- else
- List.fold_left
- (fun elems cand ->
- if (only_one && (elems <> [])) then elems
- else
- if (maxd && not(is_prod) &&
- not(is_a_fact_ast status subst metasenv context cand))
- then (debug_print (lazy "pruned: not a fact"); elems)
- else
- match try_candidate (~smart:1)
- flags depth status cache.unit_eq context cand with
- | None -> elems
- | Some x -> x::elems)
- [] smart_candidates
- in
- elems@more_elems
+ elems
;;
exception Found
;;
(* gty is supposed to be meta-closed *)
-let is_subsumed depth status gty cache =
+let is_subsumed depth status gty (_,cache) =
if cache=[] then false else (
debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
let n,h,metasenv,subst,obj = status#obj in
try
let idx = List.assq ctx cache in
Ncic_termSet.elements
- (InvRelDiscriminationTree.retrieve_generalizations idx gty)
+ (InvRelDiscriminationTree.retrieve_generalizations idx gty)
with Not_found -> []
in
debug_print ~depth
(lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
try
List.iter
- (fun t ->
- let _ , source = term_of_cic_term status t ctx in
- let implication =
- NCic.Prod("foo",source,target) in
- let metasenv,j,_,_ =
- NCicMetaSubst.mk_meta
- metasenv ctx ~with_type:implication `IsType in
- let status = status#set_obj (n,h,metasenv,subst,obj) in
- let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
- try
- let status = NTactics.intro_tac "foo" status in
- let status =
- NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
- in
- if (head_goals status#stack = []) then raise Found
- else ()
+ (fun t ->
+ let _ , source = term_of_cic_term status t ctx in
+ let implication =
+ NCic.Prod("foo",source,target) in
+ let metasenv,j,_,_ =
+ NCicMetaSubst.mk_meta
+ metasenv ctx ~with_type:implication `IsType in
+ let status = status#set_obj (n,h,metasenv,subst,obj) in
+ let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
+ try
+ let status = NTactics.intro_tac "foo" status in
+ let status =
+ NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
+ in
+ if (head_goals status#stack = []) then raise Found
+ else ()
with
- | Error _ -> ())
- candidates;false
+ | Error _ -> ())
+ candidates;false
with Found -> debug_print ~depth (lazy "success");true)
;;
+
+let equational_and_applicative_case
+ signature flags status g depth gty cache
+=
+ let elems =
+ if false (*is_equational_case gty flags*) then
+ let elems =
+ equational_case
+ signature status flags g gty cache
+ in
+ let more_elems =
+ applicative_case depth
+ signature status flags gty cache
+ in
+ elems@more_elems
+ else
+ let elems =
+ (*match LibraryObjects.eq_URI () with
+ | Some _ ->
+ smart_applicative_case dbd tables depth s fake_proof goalno
+ gty m context signature universe cache flags
+ | None -> *)
+ applicative_case depth
+ signature status flags gty cache
+ in
+ elems
+ in
+ let elems =
+ List.map (fun c,s,gl ->
+ c,1,1,s,List.map (fun i ->
+ let sort =
+ let gty = get_goalty s i in
+ let _, sort = typeof s (ctx_of gty) gty in
+ match term_of_cic_term s sort (ctx_of sort) with
+ | _, NCic.Sort NCic.Prop -> P
+ | _ -> T
+ in
+ i,sort) gl) elems
+ in
+ (* let elems = sort_new_elems elems in *)
+ elems, cache
+;;
+
let rec guess_name name ctx =
if name = "_" then guess_name "auto" ctx else
if not (List.mem_assoc name ctx) then name else
guess_name (name^"'") ctx
;;
-let is_prod status =
- let _, ctx, gty = current_goal status in
- let status, gty = apply_subst status ctx gty in
- let _, raw_gty = term_of_cic_term status gty ctx in
- match raw_gty with
- | NCic.Prod (name,src,_) ->
- let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
- (match snd (term_of_cic_term status src ctx) with
- | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
- | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
- let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
- (match itys with
- (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
- | [_,_,_,[_]]
- | [_,_,_,[]] -> `Inductive (guess_name name ctx)
- | _ -> `Some (guess_name name ctx))
- | _ -> `Some (guess_name name ctx))
- | _ -> `None
-
-let intro ~depth status facts name =
+let intro ~depth status (tcache,fcache) name =
let status = NTactics.intro_tac name status in
- let _, ctx, ngty = current_goal status in
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let ngty = get_goalty status open_goal in
+ let ctx = ctx_of ngty in
let t = mk_cic_term ctx (NCic.Rel 1) in
let status, keys = keys_of_term status t in
- let facts = List.fold_left (add_to_th t) facts keys in
- debug_print ~depth (lazy ("intro: "^ name));
+ let tcache = List.fold_left (add_to_th t) tcache keys in
+ debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
(* unprovability is not stable w.r.t introduction *)
- status, facts
-;;
-
-let rec intros_facts ~depth status facts =
- if List.length (head_goals status#stack) <> 1 then status, facts else
- match is_prod status with
- | `Inductive name
- | `Some(name) ->
- let status,facts =
- intro ~depth status facts name
- in intros_facts ~depth status facts
-(* | `Inductive name ->
- let status = NTactics.case1_tac name status in
- intros_facts ~depth status facts *)
- | _ -> status, facts
-;;
-
-let intros ~depth status cache =
- match is_prod status with
- | `Inductive _
- | `Some _ ->
- let trace = cache.trace in
- let status,facts =
- intros_facts ~depth status cache.facts
- in
- if head_goals status#stack = [] then
- let status = NTactics.merge_tac status in
- [(0,Ast.Ident("__intros",None)),status], cache
- else
- (* we reindex the equation from scratch *)
- let unit_eq = index_local_equations status#eq_cache status in
- let status = NTactics.merge_tac status in
- [(0,Ast.Ident("__intros",None)),status],
- init_cache ~facts ~unit_eq () ~trace
- | _ -> [],cache
-;;
-
-let reduce ~whd ~depth status g =
+ status, (tcache,[])
+;;
+
+let rec intros ~depth status cache =
+ let open_goals = head_goals status#stack in
+ assert (List.length open_goals = 1);
+ let open_goal = List.hd open_goals in
+ let gty = get_goalty status open_goal in
+ let _, raw_gty = term_of_cic_term status gty (ctx_of gty) in
+ match raw_gty with
+ | NCic.Prod (name,_,_) ->
+ let status,cache =
+ intro ~depth status cache (guess_name name (ctx_of gty))
+ in intros ~depth status cache
+ | _ -> status, cache, open_goal
+;;
+
+let reduce ~depth status g =
let n,h,metasenv,subst,o = status#obj in
let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
let ty = NCicUntrusted.apply_subst subst ctx ty in
- let ty' =
- (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty
- in
+ let ty' = NCicReduction.whd ~subst ctx ty in
if ty = ty' then []
else
(debug_print ~depth
(g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
in
let status = status#set_obj (n,h,metasenv,subst,o) in
- (* we merge to gain a depth level; the previous goal level should
- be empty *)
- let status = NTactics.merge_tac status in
incr candidate_no;
- [(!candidate_no,Ast.Ident("__whd",None)),status])
+ [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[g,P]])
;;
let do_something signature flags status g depth gty cache =
- let l0, cache = intros ~depth status cache in
- if l0 <> [] then l0, cache
- else
- (* whd *)
- let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
- (* if l <> [] then l,cache else *)
- (* backward aplications *)
- let l1 =
- List.map
- (fun s ->
- incr candidate_no;
- ((!candidate_no,Ast.Ident("__paramod",None)),s))
- (auto_eq_check cache.unit_eq status)
- in
- let l2 =
- if ((l1 <> []) && flags.last) then [] else
- applicative_case depth signature status flags gty cache
+ let l = reduce ~depth status g in
+ let l1,cache =
+ (equational_and_applicative_case
+ signature flags status g depth gty cache)
in
- (* statistics *)
- List.iter
- (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
- (* states in l1 have have an empty set of subgoals: no point to sort them *)
- debug_print ~depth
- (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
- (* l1 @ (sort_new_elems (l @ l2)), cache *)
- l1 @ (List.rev l2) @ l, cache
+ sort_new_elems (l@l1), cache
;;
let pp_goal = function
String.concat ", "
(List.map
(fun i ->
- let gty = get_goalty status i in
- NTacStatus.ppterm status gty)
+ let gty = get_goalty status i in
+ NTacStatus.ppterm status gty)
l)
;;
| [] -> assert false
| (goals, t, k, tag) :: s ->
let g = head_goals status#stack in
- let sortedg =
- (List.rev (MS.topological_sort g (deps status))) in
+ let sortedg =
+ (List.rev (MS.topological_sort g (deps status))) in
debug_print (lazy ("old g = " ^
String.concat "," (List.map string_of_int g)));
debug_print (lazy ("sorted goals = " ^
- String.concat "," (List.map string_of_int sortedg)));
- let is_it i = function
- | (_,Continuationals.Stack.Open j )
+ String.concat "," (List.map string_of_int sortedg)));
+ let is_it i = function
+ | (_,Continuationals.Stack.Open j )
| (_,Continuationals.Stack.Closed j ) -> i = j
- in
- let sorted_goals =
- List.map (fun i -> List.find (is_it i) goals) sortedg
- in
- (sorted_goals, t, k, tag) :: s
+ in
+ let sorted_goals =
+ List.map (fun i -> List.find (is_it i) goals) sortedg
+ in
+ (sorted_goals, t, k, tag) :: s
in
status#set_stack gstatus
;;
| [] -> assert false
| (g, t, k, tag) :: s ->
let is_open = function
- | (_,Continuationals.Stack.Open _) -> true
+ | (_,Continuationals.Stack.Open _) -> true
| (_,Continuationals.Stack.Closed _) -> false
- in
- let g' = List.filter is_open g in
- (g', t, k, tag) :: s
+ in
+ let g' = List.filter is_open g in
+ (g', t, k, tag) :: s
in
status#set_stack gstatus
;;
| [] -> assert false
| (g, t, k, tag) :: s ->
let in_focus = function
- | (_,Continuationals.Stack.Open i)
+ | (_,Continuationals.Stack.Open i)
| (_,Continuationals.Stack.Closed i) -> List.mem i focus
- in
+ in
let focus,others = List.partition in_focus g
- in
+ in
(* we need to mark it as a BranchTag, otherwise cannot merge later *)
- (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
+ (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
in
status#set_stack gstatus
;;
-let deep_focus_tac level focus status =
- let in_focus = function
- | (_,Continuationals.Stack.Open i)
- | (_,Continuationals.Stack.Closed i) -> List.mem i focus
- in
- let rec slice level gs =
- if level = 0 then [],[],gs else
- match gs with
- | [] -> assert false
- | (g, t, k, tag) :: s ->
- let f,o,gs = slice (level-1) s in
- let f1,o1 = List.partition in_focus g
- in
- (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
- in
- let gstatus =
- let f,o,s = slice level status#stack in f@o@s
- in
- status#set_stack gstatus
-;;
-
-let rec stack_goals level gs =
- if level = 0 then []
- else match gs with
- | [] -> assert false
- | (g,_,_,_)::s ->
- let is_open = function
- | (_,Continuationals.Stack.Open i) -> Some i
- | (_,Continuationals.Stack.Closed _) -> None
- in
- HExtlib.filter_map is_open g @ stack_goals (level-1) s
-;;
-
-let open_goals level status = stack_goals level status#stack
-;;
-
-let move_to_side level status =
-match status#stack with
- | [] -> assert false
- | (g,_,_,_)::tl ->
- let is_open = function
- | (_,Continuationals.Stack.Open i) -> Some i
- | (_,Continuationals.Stack.Closed _) -> None
- in
- let others = menv_closure status (stack_goals (level-1) tl) in
- List.for_all (fun i -> IntSet.mem i others)
- (HExtlib.filter_map is_open g)
-
-let rec auto_clusters ?(top=false)
+let rec auto_clusters
flags signature cache depth status : unit =
- debug_print ~depth (lazy ("entering auto clusters at depth " ^
- (string_of_int depth)));
- debug_print ~depth (pptrace cache.trace);
+ debug_print ~depth (lazy "entering auto clusters");
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
- if goals = [] then
- if depth = 0 then raise (Proved (status, cache.trace))
- else
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache *)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status
- else if List.length goals < 2 then
- auto_main flags signature cache depth status
+ if goals = [] then raise (Proved status)
+ else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ else if List.length goals < 2 then
+ auto_main flags signature cache depth status
else
- let all_goals = open_goals (depth+1) status in
debug_print ~depth (lazy ("goals = " ^
- String.concat "," (List.map string_of_int all_goals)));
- let classes = HExtlib.clusters (deps status) all_goals in
- List.iter
- (fun gl ->
- if List.length gl > flags.maxwidth then
- (debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
- raise (Gaveup IntSet.empty))
- else ()) classes;
- if List.length classes = 1 then
- let flags =
- {flags with last = (List.length all_goals = 1)} in
- (* no need to cluster *)
- auto_main flags signature cache depth status
- else
- let classes = if top then List.rev classes else classes in
+ String.concat "," (List.map string_of_int goals)));
+ let classes = HExtlib.clusters (deps status) goals in
debug_print ~depth
- (lazy
- (String.concat "\n"
- (List.map
- (fun l ->
- ("cluster:" ^ String.concat "," (List.map string_of_int l)))
- classes)));
- let status,trace,b =
- List.fold_left
- (fun (status,trace,b) gl ->
- let cache = {cache with trace = trace} in
- let flags =
- {flags with last = (List.length gl = 1)} in
- let lold = List.length status#stack in
- debug_print ~depth (lazy ("stack length = " ^
- (string_of_int lold)));
- let fstatus = deep_focus_tac (depth+1) gl status in
- try
+ (lazy
+ (String.concat "\n"
+ (List.map
+ (fun l ->
+ ("cluster:" ^ String.concat "," (List.map string_of_int l)))
+ classes)));
+ let status =
+ List.fold_left
+ (fun status gl ->
+ let status = focus_tac gl status in
+ try
debug_print ~depth (lazy ("focusing on" ^
- String.concat "," (List.map string_of_int gl)));
- auto_main flags signature cache depth fstatus; assert false
- with
- | Proved(status,trace) ->
- let status = NTactics.merge_tac status in
- let lnew = List.length status#stack in
- assert (lold = lnew);
- (status,trace,true)
- | Gaveup _ when top -> (status,trace,b)
- )
- (status,cache.trace,false) classes
- in
- let rec final_merge n s =
- if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
- in let status = final_merge depth status
- in if b then raise (Proved(status,trace)) else raise (Gaveup IntSet.empty)
+ String.concat "," (List.map string_of_int gl)));
+ auto_main flags signature cache depth status; status
+ with Proved(status) -> NTactics.merge_tac status)
+ status classes
+ in raise (Proved status)
and
-
-(* BRAND NEW VERSION *)
+
+(* let rec auto_main flags signature cache status k depth = *)
+
auto_main flags signature cache depth status: unit =
debug_print ~depth (lazy "entering auto main");
- debug_print ~depth (pptrace cache.trace);
- debug_print ~depth (lazy ("stack length = " ^
- (string_of_int (List.length status#stack))));
(* ignore(Unix.select [] [] [] 0.01); *)
let status = sort_tac (clean_up_tac status) in
let goals = head_goals status#stack in
match goals with
- | [] when depth = 0 -> raise (Proved (status,cache.trace))
- | [] ->
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache *)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status
- | orig::_ ->
- if depth > 0 && move_to_side depth status
- then
- let status = NTactics.merge_tac status in
- let cache =
- let l,tree = cache.under_inspection in
- match l with
- | [] -> cache (* possible because of intros that cleans the cache*)
- | a::tl -> let tree = rm_from_th a tree a in
- {cache with under_inspection = tl,tree}
- in
- auto_clusters flags signature cache (depth-1) status
- else
- let ng = List.length goals in
- (* moved inside auto_clusters *)
- if ng > flags.maxwidth then
- (print ~depth (lazy "FAIL LOCAL WIDTH"); raise (Gaveup IntSet.empty))
- else if depth = flags.maxdepth then
- raise (Gaveup IntSet.empty)
- else
- let status = NTactics.branch_tac ~force:true status in
- let g,gctx, gty = current_goal status in
- let ctx,ty = close status g in
- let closegty = mk_cic_term ctx ty in
- let status, gty = apply_subst status gctx gty in
- debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
- if is_subsumed depth status closegty (snd cache.under_inspection) then
- (debug_print ~depth (lazy "SUBSUMED");
- raise (Gaveup IntSet.add g IntSet.empty))
+ | [] -> raise (Proved status)
+ | g::tlg ->
+ if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
else
- let new_sig = height_of_goal g status in
- if new_sig < signature then
- (debug_print (lazy ("news = " ^ (string_of_int new_sig)));
- debug_print (lazy ("olds = " ^ (string_of_int signature))));
- let alternatives, cache =
+ let status =
+ if tlg=[] then status
+ else NTactics.branch_tac status in
+ let status, cache, g = intros ~depth status cache in
+ let gty = get_goalty status g in
+ let ctx,ty = close status g in
+ let closegty = mk_cic_term ctx ty in
+ let status, gty = apply_subst status (ctx_of gty) gty in
+ debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
+ if is_subsumed depth status closegty cache then
+ (debug_print (lazy "SUBSUMED");
+ raise (Gaveup IntSet.add g IntSet.empty))
+ else
+ let alternatives, cache =
do_something signature flags status g depth gty cache in
- let loop_cache =
- let l,tree = cache.under_inspection in
- let l,tree = closegty::l, add_to_th closegty tree closegty in
- {cache with under_inspection = l,tree} in
- List.iter
- (fun ((_,t),status) ->
- debug_print ~depth
- (lazy ("(re)considering goal " ^
- (string_of_int g) ^" : "^ppterm status gty));
- debug_print (~depth:depth)
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
- let depth,cache =
- if t=Ast.Ident("__whd",None) ||
- t=Ast.Ident("__intros",None)
- then depth, cache
- else depth+1,loop_cache in
- let cache = add_to_trace ~depth cache t in
- try
- auto_clusters flags signature cache depth status
- with Gaveup _ ->
- debug_print ~depth (lazy "Failed");
- ())
- alternatives;
- raise (debug_print(lazy "no more candidates"); Gaveup IntSet.empty)
+ let loop_cache =
+ let tcache,fcache = cache in
+ tcache,add_to_th closegty fcache closegty in
+ let unsat =
+ List.fold_left
+ (* the underscore information does not need to be returned
+ by do_something *)
+ (fun unsat ((_,t),_,_,status,_) ->
+ let depth',looping_cache =
+ if t=(Ast.Implicit `JustOne) then depth,cache
+ else depth+1, loop_cache in
+ debug_print (~depth:depth')
+ (lazy ("Case: " ^ CicNotationPp.pp_term t));
+ try auto_clusters flags signature loop_cache
+ depth' status; unsat
+ with
+ | Proved status ->
+ debug_print (~depth:depth') (lazy "proved");
+ if tlg=[] then raise (Proved status)
+ else
+ let status = NTactics.merge_tac status
+ in
+ ( (* old cache, here *)
+ try auto_clusters flags signature cache
+ depth status; assert false
+ with Gaveup f ->
+ debug_print ~depth
+ (lazy ("Unsat1 at depth " ^ (string_of_int depth)
+ ^ ": " ^
+ (pp_goals status (IntSet.elements f))));
+ (* TODO: cache failures *)
+ IntSet.union f unsat)
+ | Gaveup f ->
+ debug_print (~depth:depth')
+ (lazy ("Unsat2 at depth " ^ (string_of_int depth')
+ ^ ": " ^
+ (pp_goals status (IntSet.elements f))));
+ (* TODO: cache local failures *)
+ unsat)
+ IntSet.empty alternatives
+ in
+ raise (Gaveup IntSet.add g unsat)
;;
-
+
let int name l def =
try int_of_string (List.assoc name l)
with Failure _ | Not_found -> def
;;
-module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
-
-let cleanup_trace s trace =
- (* removing duplicates *)
- let trace_set =
- List.fold_left
- (fun acc t -> AstSet.add t acc)
- AstSet.empty trace in
- let trace = AstSet.elements trace_set
- (* filtering facts *)
- in List.filter
- (fun t ->
- match t with
- | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
- | _ -> false) trace
-;;
-
-let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
- let oldstatus = status in
- let status = (status:> NTacStatus.tac_status) in
+let auto_tac ~params:(_univ,flags) status =
let goals = head_goals status#stack in
- let status, facts = mk_th_cache status goals in
- let unit_eq = index_local_equations status#eq_cache status in
- let cache = init_cache ~facts ~unit_eq () in
-(* pp_th status facts; *)
+ let status, cache = mk_th_cache status goals in
+(* pp_th status cache; *)
(*
NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
debug_print (lazy(
(NDiscriminationTree.TermSet.elements t))
)));
*)
- let candidates =
- match univ with
- | None -> None
- | Some l ->
- let to_Ast t =
- let status, res = disambiguate status [] t None in
- let _,res = term_of_cic_term status res (ctx_of res)
- in Ast.NCic res
- in Some (List.map to_Ast l)
- in
let depth = int "depth" flags 3 in
let size = int "size" flags 10 in
- let width = int "width" flags 4 (* (3+List.length goals)*) in
+ let width = int "width" flags (3+List.length goals) in
(* XXX fix sort *)
-(* let goals = List.map (fun i -> (i,P)) goals in *)
- let signature = height_of_goals status in
+ let goals = List.map (fun i -> (i,P)) goals in
+ let signature = () in
let flags = {
- last = true;
- candidates = candidates;
maxwidth = width;
maxsize = size;
maxdepth = depth;
if x > y then
(print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- debug_print(lazy
+ print(lazy
("Applicative nodes:"^string_of_int !app_counter));
raise (Error (lazy "auto gave up", None)))
else
let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
let flags = { flags with maxdepth = x }
in
- try auto_clusters (~top:true) flags signature cache 0 status;assert false
-(*
- try auto_main flags signature cache 0 status;assert false
-*)
- with
- | Gaveup _ -> up_to (x+1) y
- | Proved (s,trace) ->
- debug_print (lazy ("proved at depth " ^ string_of_int x));
- List.iter (toref incr_uses statistics) trace;
- let trace = cleanup_trace s trace in
- let _ = debug_print (pptrace trace) in
+ try auto_clusters flags signature (cache,[]) 0 status;status
+ with
+ | Gaveup _ -> up_to (x+1) y
+ | Proved s ->
+ print (lazy ("proved at depth " ^ string_of_int x));
let stack =
- match s#stack with
- | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
- | _ -> assert false
+ match s#stack with
+ | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
+ | _ -> assert false
in
- let s = s#set_stack stack in
- trace_ref := trace;
- oldstatus#set_status s
+ s#set_stack stack
in
let s = up_to depth depth in
- debug_print (print_stat statistics);
- debug_print(lazy
+ print(lazy
("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- debug_print(lazy
+ print(lazy
("Applicative nodes:"^string_of_int !app_counter));
s
;;
projects / helm.git / blobdiff