| Eq ->
let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
let ref = NReference.reference_of_spec uri (NReference.Ind(true,0,2)) in
- NCic.Const ref
+ NCic.Const ref
| EqInd_l ->
let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_l.con" in
let ref = NReference.reference_of_spec uri (NReference.Def(1)) in
- NCic.Const ref
+ NCic.Const ref
| EqInd_r ->
let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/rewrite_r.con" in
let ref = NReference.reference_of_spec uri (NReference.Def(3)) in
- NCic.Const ref
+ NCic.Const ref
| Refl ->
let uri = NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq.ind" in
let ref = NReference.reference_of_spec uri (NReference.Con(0,1,2)) in
- NCic.Const ref
+ NCic.Const ref
let set_default_sig () =
(*prerr_endline "setting default sig";*)
prerr_endline "setting oxuri in nCicProof";
let nsig = function
| Eq ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1)"))
| EqInd_l ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_ind.con"))
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_ind.con"))
| EqInd_r ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq_elim_r.con"))
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq_elim_r.con"))
| Refl ->
- NCic.Const
- (reference_of_oxuri
- (UriManager.uri_of_string
- "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
+ NCic.Const
+ (reference_of_oxuri
+ (UriManager.uri_of_string
+ "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)"))
in eqsig:= nsig
;;
extract t
;;
+
let mk_predicate hole_type amount ft p1 vl =
let rec aux t p =
match p with
match t with
| Terms.Leaf _
| Terms.Var _ ->
- let module Pp =
- Pp.Pp(NCicBlob.NCicBlob(
- struct
- let metasenv = [] let subst = [] let context = []
- end))
- in
+ let module NCicBlob = NCicBlob.NCicBlob(
+ struct
+ let metasenv = [] let subst = [] let context = []
+ end)
+ in
+ let module Pp = Pp.Pp(NCicBlob) in
prerr_endline ("term: " ^ Pp.pp_foterm ft);
prerr_endline ("path: " ^ String.concat ","
(List.map string_of_int p1));
- prerr_endline ("leading to: " ^ Pp.pp_foterm t);
+ prerr_endline ("leading to: " ^ Pp.pp_foterm t);
assert false
| Terms.Node l ->
let l =
NCic.Lambda("x", hole_type, aux ft (List.rev p1))
;;
+ let dag =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/prop1.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,4)) in
+ NCic.Const ref
+ ;;
+
+ (*
+ let eq_setoid =
+ let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) in
+ NCic.Const ref
+ ;;
+ *)
+
+ let sym eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/sym.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism1 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism1.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; eq];
+ ;;
+
+ let eq_morphism2 eq =
+ let u= NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq_is_morphism2.con" in
+ let u = NReference.reference_of_spec u (NReference.Def 4) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Term; NCic.Implicit `Term;
+ NCic.Implicit `Term; eq; NCic.Implicit `Term];
+ ;;
+
+ let trans eq p =
+ let u= NUri.uri_of_string "cic:/matita/ng/properties/relations/trans.con" in
+ let u = NReference.reference_of_spec u (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const u; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term; NCic.Implicit `Term; NCic.Implicit `Term; eq]
+ ;;
+
+ let iff1 eq p =
+ let uri = NUri.uri_of_string "cic:/matita/ng/logic/connectives/if.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,2,1)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Type;
+ eq; p];
+ ;;
+
(*
- let mk_morphism eq amount ft p1 vl =
+ let mk_refl = function
+ | NCic.Appl [_; _; x; _] ->
+ let uri= NUri.uri_of_string "cic:/matita/ng/properties/relations/refl.con" in
+ let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,3)) in
+ NCic.Appl[NCic.Const ref; NCic.Implicit `Type; NCic.Implicit `Term;
+ NCic.Implicit `Term(*x*)]
+ | _ -> assert false
+*)
+
+ let mk_refl = function
+ | NCic.Appl [_; ty; l; _]
+ -> NCic.Appl [eq_refl();ty;l]
+ | _ -> assert false
+
+
+ let mk_morphism eq amount ft pl vl =
let rec aux t p =
match p with
| [] -> eq
| n::tl ->
+ prerr_endline (string_of_int n);
match t with
| Terms.Leaf _
| Terms.Var _ -> assert false
- | Terms.Node l ->
- let dag,arity = ____ in
- let l =
- HExtlib.list_rev_mapi_filter
- (fun t i ->
- if i < arity then None
- else if i = n then Some (aux t tl)
- else Some (NCic.Appl [refl ...]))
- l
- in
- NCic.Appl (dag::l)
+ | Terms.Node [] -> assert false
+ | Terms.Node [ Terms.Leaf eqt ; _; l; r ]
+ when (eqP ()) = eqt ->
+ if n=2 then eq_morphism1 (aux l tl)
+ else eq_morphism2 (aux r tl)
+ | Terms.Node (f::l) ->
+ snd (
+ List.fold_left
+ (fun (i,acc) t ->
+ i+1,
+ let f = extract amount vl f in
+ if i = n then
+ let imp = NCic.Implicit `Term in
+ NCic.Appl (dag::imp::imp::imp(* f *)::imp::imp::
+ [aux t tl])
+ else
+ NCicUntrusted.mk_appl acc [extract amount vl t]
+ ) (1,extract amount vl f) l)
in aux ft (List.rev pl)
;;
-*)
let mk_proof (bag : NCic.term Terms.bag) mp subst steps =
let module Subst = FoSubst in
| Terms.Equation (l,r,ty,_) ->
Terms.Node [ Terms.Leaf eqP(); ty; l; r]
in
- lit, vl, proof
+ lit, vl, proof
in
- let mk_refl = function
- | NCic.Appl [_; ty; l; _]
- -> NCic.Appl [eq_refl();ty;l]
- | _ -> assert false
- in
let proof_type =
let lit,_,_ = get_literal mp in
let lit = Subst.apply_subst subst lit in
- extract 0 [] lit in
+ extract 0 [] lit in
let rec aux ongoal seen = function
| [] -> NCic.Rel 1
| id :: tl ->
let amount = List.length seen in
let lit,vl,proof = get_literal id in
if not ongoal && id = mp then
- let lit = Subst.apply_subst subst lit in
+ let lit = Subst.apply_subst subst lit in
let eq_ty = extract amount [] lit in
- let refl = mk_refl eq_ty in
+ let refl = mk_refl eq_ty in
(*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
- (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
+ (* (NCic.LetIn ("clause_" ^ string_of_int id, eq_ty, refl,
aux true ((id,([],lit))::seen) (id::tl))) *)
- NCicSubstitution.subst
- ~avoid_beta_redexes:true ~no_implicit:false refl
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false refl
(aux true ((id,([],lit))::seen) (id::tl))
else
match proof with
| Terms.Exact _ when tl=[] ->
- (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
- aux ongoal seen tl
+ (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
+ aux ongoal seen tl
| Terms.Step _ when tl=[] -> assert false
| Terms.Exact ft ->
- (* prerr_endline ("Exact for " ^ (string_of_int id));*)
+ (* prerr_endline ("Exact for " ^ (string_of_int id));*)
(*
NCic.LetIn ("clause_" ^ string_of_int id,
close_with_forall vl (extract amount vl lit),
close_with_lambdas vl (extract amount vl ft),
aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
- *)
+ *)
NCicSubstitution.subst
- ~avoid_beta_redexes:true ~no_implicit:false
- (close_with_lambdas vl (extract amount vl ft))
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl (extract amount vl ft))
(aux ongoal
((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
| Terms.Step (_, id1, id2, dir, pos, subst) ->
let id, id1,(lit,vl,proof) =
- if ongoal then id1,id,get_literal id1
- else id,id1,(lit,vl,proof)
- in
- let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
+ if ongoal then id1,id,get_literal id1
+ else id,id1,(lit,vl,proof)
+ in
+ let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
let proof_of_id id =
let vars = List.rev (vars_of id seen) in
let args = List.map (Subst.apply_subst subst) vars in
let args = List.map (extract amount vl) args in
- let rel_for_id = NCic.Rel (List.length vl + position id seen) in
- if args = [] then rel_for_id
+ let rel_for_id = NCic.Rel (List.length vl + position id seen) in
+ if args = [] then rel_for_id
else NCic.Appl (rel_for_id::args)
in
let p_id1 = proof_of_id id1 in
let p_id2 = proof_of_id id2 in
+(*
+ let morphism, l, r =
+ let p =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ p_id2
+ else sym p_id2 in
+ let id1_ty = ty_of id1 seen in
+ let id2_ty,l,r =
+ match ty_of id2 seen with
+ | Terms.Node [ _; t; l; r ] ->
+ extract amount vl (Subst.apply_subst subst t),
+ extract amount vl (Subst.apply_subst subst l),
+ extract amount vl (Subst.apply_subst subst r)
+ | _ -> assert false
+ in
+ (*prerr_endline "mk_predicate :";
+ if ongoal then prerr_endline "ongoal=true"
+ else prerr_endline "ongoal=false";
+ prerr_endline ("id=" ^ string_of_int id);
+ prerr_endline ("id1=" ^ string_of_int id1);
+ prerr_endline ("id2=" ^ string_of_int id2);
+ prerr_endline ("Positions :" ^
+ (String.concat ", "
+ (List.map string_of_int pos)));*)
+ mk_morphism
+ p amount (Subst.apply_subst subst id1_ty) pos vl,
+ l,r
+ in
+ let rewrite_step = iff1 morphism p_id1
+ in
+*)
let pred, hole_type, l, r =
let id1_ty = ty_of id1 seen in
let id2_ty,l,r =
extract amount vl (Subst.apply_subst subst r)
| _ -> assert false
in
- (*prerr_endline "mk_predicate :";
- if ongoal then prerr_endline "ongoal=true"
- else prerr_endline "ongoal=false";
- prerr_endline ("id=" ^ string_of_int id);
- prerr_endline ("id1=" ^ string_of_int id1);
- prerr_endline ("id2=" ^ string_of_int id2);
- prerr_endline ("Positions :" ^
- (String.concat ", "
- (List.map string_of_int pos)));*)
+ (*prerr_endline "mk_predicate :";
+ if ongoal then prerr_endline "ongoal=true"
+ else prerr_endline "ongoal=false";
+ prerr_endline ("id=" ^ string_of_int id);
+ prerr_endline ("id1=" ^ string_of_int id1);
+ prerr_endline ("id2=" ^ string_of_int id2);
+ prerr_endline ("Positions :" ^
+ (String.concat ", "
+ (List.map string_of_int pos)));*)
mk_predicate
id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
id2_ty,
l,r
in
- let l, r, eq_ind =
- if (ongoal=true) = (dir=Terms.Left2Right) then
- r,l,eq_ind_r ()
- else
- l,r,eq_ind ()
- in
- let body = aux ongoal
- ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
- in
- if NCicUntrusted.count_occurrences [] 0 body <= 1 then
- NCicSubstitution.subst
- ~avoid_beta_redexes:true ~no_implicit:false
- (close_with_lambdas vl (NCic.Appl
- [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]))
- body
+ let rewrite_step =
+ if (ongoal=true) = (dir=Terms.Left2Right) then
+ NCic.Appl
+ [eq_ind_r(); hole_type; r; pred; p_id1; l; p_id2]
else
- NCic.LetIn ("clause_" ^ string_of_int id,
- close_with_forall vl (extract amount vl lit),
- (* NCic.Implicit `Type, *)
- close_with_lambdas vl (NCic.Appl
- [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
- body)
+ NCic.Appl
+ [ eq_ind(); hole_type; l; pred; p_id1; r; p_id2]
+ in
+ let body = aux ongoal
+ ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl
+ in
+ if NCicUntrusted.count_occurrences [] 0 body <= 1 then
+ NCicSubstitution.subst
+ ~avoid_beta_redexes:true ~no_implicit:false
+ (close_with_lambdas vl rewrite_step) body
+ else
+ NCic.LetIn ("clause_" ^ string_of_int id,
+ close_with_forall vl (extract amount vl lit),
+ (* NCic.Implicit `Type, *)
+ close_with_lambdas vl rewrite_step, body)
in
aux false [] steps, proof_type
;;
open Printf
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 = ()
-(*
+let print ?(depth=0) s =
prerr_endline (String.make depth '\t'^Lazy.force s)
-*)
+let debug_print ?(depth=0) s =
+ if !debug then print ~depth s else ()
let debug_do f = if !debug then f () else ()
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)
+ match m with
+ | NCic.Meta(i,_) -> IntSet.add i acc
+ | _ -> assert false)
IntSet.empty metas
in IntSet.subset menv clos;;
let obj = NCicEnvironment.get_checked_obj uri in
match obj with
| (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
- is_a_fact s (mk_cic_term [] ty)
+ is_a_fact s (mk_cic_term [] ty)
(* aggiungere i costruttori *)
| _ -> false
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
- debug_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
- (* the previous code is much less expensive than directly refining
- pt with expected type pty
- in
- prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
- 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))
+ NCicRefiner.typeof status
+ (* (status#set_coerc_db NCicCoercion.empty_db) *)
+ metasenv subst ctx pt None in
+ debug_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
+ (* the previous code is much less expensive than directly refining
+ pt with expected type pty
+ in
+ prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
+ 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.RefineFailure msg
| NCicRefiner.Uncertain msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- snd (Lazy.force msg))); None
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ snd (Lazy.force msg))); None
| NCicRefiner.AssertFailure msg ->
- debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
- Lazy.force msg)); None
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ Lazy.force msg)); None
| _ -> None
in
HExtlib.filter_map build_status
(* warning: ctx is supposed to be already instantiated w.r.t subst *)
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
(fun eq_cache _ ->
c:= !c+1;
let t = NCic.Rel !c in
- try
- let ty = NCicTypeChecker.typeof [] [] ctx t 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)
+ 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 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
with
| None, tables ->
(* if normal application fails we try to be smart *)
- (match try_smart_candidate dbd goalty
+ (match try_smart_candidate dbd goalty
tables subst fake_proof goalno depth context cand
- with
- | None, tables -> tables, elems
+ with
+ | None, tables -> tables, elems
| Some x, tables -> tables, x::elems)
| Some x, tables -> tables, x::elems)
(tables,[]) candidates
| (S _)::tl -> aux b tl
| (D (_,_,T))::tl -> aux b tl
| (D g)::tl ->
- (match calculate_goal_ty g s m with
+ (match calculate_goal_ty g s m with
| None -> aux b tl
- | Some (canonical_ctx, gty) ->
+ | 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)
+ ~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 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*))
+ (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
+ (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
+ (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 (CicMetaSubst.ppsubst ~metasenv:menv variant);
prerr_endline "---------- menv";
prerr_endline (CicMetaSubst.ppmetasenv [] menv);
- no_progress variant tl) *)
- else false))
+ no_progress variant tl) *)
+ else false))
| _::tl -> no_progress variant tl
in
aux todo
let signature =
List.fold_left
(fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
)
MetadataConstraints.UriManagerSet.empty gl
in
let signature =
List.fold_left
(fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataQuery.signature_of metasenv g)
)
MetadataConstraints.UriManagerSet.empty gl
in
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)
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph
+ in
+ MetadataConstraints.UriManagerSet.union set
+ (MetadataConstraints.constants_of ty)
)
signature univ
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
+ fast_eq_check unit_eq status j
with
| Error _ as e -> debug_print (lazy "error"); raise e
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 ->
type cache =
{facts : th_cache; (* positive results *)
- under_inspection : th_cache; (* to prune looping *)
+ under_inspection : cic_term list * th_cache; (* to prune looping *)
unit_eq : NCicParamod.state
}
(* 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=[])
+let init_cache ?(facts=[]) ?(under_inspection=[],[])
?(unit_eq=NCicParamod.empty_state) _ =
{facts = facts;
under_inspection = under_inspection;
let height = fast_height_of_term candidate_ty in
let rc = signature >= height in
if rc = false then
- prerr_endline ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
- ~metasenv:[] candidate ^ ": " ^ string_of_int height)
+ debug_print (lazy ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height))
else
- prerr_endline ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
- ~metasenv:[] candidate ^ ": " ^ string_of_int height);
+ debug_print (lazy ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
+ ~metasenv:[] candidate ^ ": " ^ string_of_int height));
rc
;;
else (* smart = 2: both *)
try NTactics.apply_tac ("",0,t) status
with Error _ ->
- smart_apply_auto ("",0,t) eq_cache status in
+ 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)
+ (debug_print ~depth (lazy "pruned immediately"); None)
else
(incr candidate_no;
Some ((!candidate_no,t),status))
| NCic.Const r -> Ast.NRef r | _ -> assert false in
let _, raw_gty = term_of_cic_term status gty context in
let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty in
+ universe raw_gty in
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)) @
+ (NDiscriminationTree.TermSet.elements global)) @
List.map t_ast (Ncic_termSet.elements local) in
let candidates = together cands local_cands in
let smart_candidates =
if smart then
match raw_gty with
- | NCic.Appl (hd::tl) ->
+ | NCic.Appl (hd::tl) ->
let weak_gty =
- 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
- | _ -> []
+ 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
+ | _ -> []
else []
in
candidates, smart_candidates
(lazy ("candidates: " ^ string_of_int (List.length candidates)));
debug_print ~depth
(lazy ("smart candidates: " ^
- string_of_int (List.length smart_candidates)));
+ string_of_int (List.length smart_candidates)));
(*
let sm = 0 in
let smart_candidates = [] in *)
let elems =
List.fold_left
(fun elems cand ->
- if (only_one && (elems <> [])) then elems
- else
- if (maxd && 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 cand with
+ if (only_one && (elems <> [])) then elems
+ else
+ if (maxd && 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 cand with
| None -> elems
| Some x -> x::elems)
[] candidates
if only_one && elems <> [] then elems
else
List.fold_left
- (fun elems cand ->
- if (only_one && (elems <> [])) then elems
- else
- if (maxd && not(is_a_fact_ast status subst metasenv context cand))
- then (debug_print (lazy "pruned: not a fact"); elems)
- else
+ (fun elems cand ->
+ if (only_one && (elems <> [])) then elems
+ else
+ if (maxd && 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 cand with
+ flags depth status cache.unit_eq cand with
| None -> elems
| Some x -> x::elems)
- [] smart_candidates
+ [] smart_candidates
in
elems@more_elems
;;
(* gty is supposed to be meta-closed *)
let is_subsumed depth status gty cache =
if cache=[] then false else (
- debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
+ print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
let n,h,metasenv,subst,obj = status#obj in
let ctx = ctx_of gty in
let _ , target = term_of_cic_term status gty ctx 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 rec intros_facts ~depth status facts =
match is_prod status with
| Some(name) ->
- let status,facts =
- intro ~depth status facts name
- in intros_facts ~depth status facts
+ let status,facts =
+ intro ~depth status facts name
+ in intros_facts ~depth status facts
| _ -> status, facts
;;
let rec intros ~depth status (cache:cache) =
match is_prod status with
| Some _ ->
- let status,facts =
- intros_facts ~depth status cache.facts
- in
- (* we reindex the equation from scratch *)
- let unit_eq =
- index_local_equations status#eq_cache status in
- (* under_inspection must be set to empty *)
- status, init_cache ~facts ~unit_eq ()
+ let status,facts =
+ intros_facts ~depth status cache.facts
+ in
+ (* we reindex the equation from scratch *)
+ let unit_eq =
+ index_local_equations status#eq_cache status in
+ status, init_cache ~facts ~unit_eq ()
| _ -> status, cache
;;
(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])
;;
let l1 =
List.map
(fun s ->
- incr candidate_no;
- ((!candidate_no,Ast.Ident("__paramod",None)),s))
- (auto_eq_check cache.unit_eq status) in
+ incr candidate_no;
+ ((!candidate_no,Ast.Ident("__paramod",None)),s))
+ (auto_eq_check cache.unit_eq status)
+ in
let l2 =
- if (l1 <> []) then []
- else applicative_case depth signature status flags gty cache
+ (* if (l1 <> []) then [] else *)
+ applicative_case depth signature status flags gty cache
(* fast paramodulation *)
in
(* 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
;;
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
+ (* we need to mark it as a BranchTag, otherwise cannot merge later *)
+ (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 open_goals level status =
+ let rec aux level gs =
+ if level = 0 then []
+ else match gs with
+ | [] -> assert false
+ | _ :: s -> head_goals gs @ aux (level-1) s
+ in
+ aux level status#stack
+;;
+
let rec auto_clusters ?(top=false)
flags signature cache depth status : unit =
- debug_print ~depth (lazy "entering auto clusters");
+ debug_print ~depth (lazy ("entering auto clusters at depth " ^
+ (string_of_int depth)));
(* ignore(Unix.select [] [] [] 0.01); *)
let status = clean_up_tac status in
let goals = head_goals status#stack in
- if goals = [] then raise (Proved status)
- else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ if goals = [] then
+ if depth = 0 then raise (Proved status)
+ else
+ let status = NTactics.merge_tac status in
+ auto_clusters flags signature (cache:cache) (depth-1) status
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 goals)));
- let classes = HExtlib.clusters (deps status) goals in
+ String.concat "," (List.map string_of_int all_goals)));
+ let classes = HExtlib.clusters (deps status) all_goals in
let classes = if top then List.rev classes else classes in
debug_print ~depth
- (lazy
- (String.concat "\n"
- (List.map
- (fun l ->
- ("cluster:" ^ String.concat "," (List.map string_of_int l)))
- classes)));
+ (lazy
+ (String.concat "\n"
+ (List.map
+ (fun l ->
+ ("cluster:" ^ String.concat "," (List.map string_of_int l)))
+ classes)));
let status,b =
- List.fold_left
- (fun (status,b) gl ->
- let status = focus_tac gl status in
- try
+ List.fold_left
+ (fun (status,b) gl ->
+ 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
debug_print ~depth (lazy ("focusing on" ^
- String.concat "," (List.map string_of_int gl)));
- auto_main flags signature cache depth status; assert false
- with
- | Proved(status) -> (NTactics.merge_tac status,true)
- | Gaveup _ when top -> (NTactics.merge_tac status,b)
- )
- (status,false) classes
+ String.concat "," (List.map string_of_int gl)));
+ auto_main flags signature cache depth fstatus; assert false
+ with
+ | Proved(status) ->
+ let status = NTactics.merge_tac status in
+ let lnew = List.length status#stack in
+ assert (lold = lnew);
+ (status,true)
+ | Gaveup _ when top -> (status,b)
+ )
+ (status,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) else raise (Gaveup IntSet.empty)
and
-
-(* the goals returned upon failure are an unsatisfiable subset
- of the initial head goals in the stack *)
-
+
+(* BRAND NEW VERSION *)
auto_main flags signature (cache:cache) depth status: unit =
debug_print ~depth (lazy "entering auto main");
+ 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
- | [] -> raise (Proved status)
+ | [] when depth = 0 -> raise (Proved status)
+ | [] ->
+ let status = NTactics.merge_tac status in
+ let cache =
+ let l,tree = cache.under_inspection in
+ match l with
+ | [] -> assert false
+ | a::tl -> let tree = rm_from_th a tree a in
+ {cache with under_inspection = tl,tree}
+ in
+ auto_clusters flags signature (cache:cache) (depth-1) status
| orig::_ ->
- let ng = List.length goals in
+ let ng = List.length goals in
if ng > flags.maxwidth then
- (debug_print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
- else let branch = ng>1 in
- if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
+ (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
+ else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
else
- let status =
- if branch then NTactics.branch_tac status
- else status in
+ let status = NTactics.branch_tac ~force:true status in
let status, cache = intros ~depth status cache 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 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 cache.under_inspection then
- (debug_print (lazy "SUBSUMED");
- raise (Gaveup IntSet.add g IntSet.empty))
- else
+ debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
+ if is_subsumed depth status closegty (snd cache.under_inspection) then
+ (print ~depth (lazy "SUBSUMED");
+ raise (Gaveup IntSet.add g IntSet.empty))
+ else
let do_flags =
- {flags with last = flags.last && (not branch)} in
- let alternatives, cache =
+ {flags with last = flags.last && ng=1} in
+ let alternatives, cache =
do_something signature do_flags status g depth gty cache in
- let loop_cache =
- let under_inspection =
- add_to_th closegty cache.under_inspection closegty in
- {cache with under_inspection = under_inspection} 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.Ident("__whd",None) then depth,cache
- else depth+1, loop_cache in
- debug_print (~depth:depth')
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
- let flags' =
- {flags with maxwidth = flags.maxwidth - ng +1} in
- (* sistemare *)
- let flags' =
- {flags' with last = flags'.last && (not branch)} in
- debug_print
- (lazy ("auto last: " ^ (string_of_bool flags'.last)));
- try auto_clusters flags' signature loop_cache
- depth' status; unsat
- with
- | Proved status ->
- debug_print (~depth:depth') (lazy "proved");
- if branch then
- let status = NTactics.merge_tac status
- in
- (* old cache, here *)
- let flags =
- {flags with maxwidth = flags.maxwidth - 1} in
- 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
- else raise (Proved status)
- | 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 orig unsat)
-;;
-
+ 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) then depth, cache
+ else depth+1,loop_cache in
+ try
+ auto_clusters flags signature (cache:cache) depth status
+ with Gaveup _ ->
+ debug_print ~depth (lazy "Failed");())
+ alternatives;
+ raise (Gaveup IntSet.empty)
+;;
+
let int name l def =
try int_of_string (List.assoc name l)
with Failure _ | Not_found -> def
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
- with
- | Gaveup _ -> up_to (x+1) y
- | Proved s ->
+ 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 ->
debug_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
- oldstatus#set_status s
+ let s = s#set_stack stack in
+ oldstatus#set_status s
in
let s = up_to depth depth in
debug_print(lazy
projects / helm.git / commitdiff