From 12f96bd48b460d06f9858a334ee7c52d6831712f Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 19 Feb 2010 07:19:01 +0000 Subject: [PATCH] Added an implicit parameter to branch_tac to allow branching on a single goal. --- .../components/binaries/transcript/.depend | 5 + .../grafite_engine/grafiteEngine.ml | 4 +- .../components/ng_paramodulation/nCicBlob.ml | 5 +- .../components/ng_paramodulation/nCicProof.ml | 284 +++++--- .../components/ng_paramodulation/paramod.ml | 6 +- helm/software/components/ng_tactics/nAuto.ml | 2 +- .../components/ng_tactics/nDestructTac.ml | 2 +- .../components/ng_tactics/nTactics.ml | 7 +- .../components/ng_tactics/nTactics.mli | 2 +- helm/software/components/ng_tactics/nnAuto.ml | 672 ++++++++++-------- 10 files changed, 568 insertions(+), 421 deletions(-) diff --git a/helm/software/components/binaries/transcript/.depend b/helm/software/components/binaries/transcript/.depend index bb6f22a64..87d1ed25c 100644 --- a/helm/software/components/binaries/transcript/.depend +++ b/helm/software/components/binaries/transcript/.depend @@ -1,6 +1,11 @@ gallina8Parser.cmi: types.cmo grafiteParser.cmi: types.cmo grafite.cmi: types.cmo +engine.cmi: +types.cmo: +types.cmx: +options.cmo: +options.cmx: gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi gallina8Lexer.cmo: options.cmo gallina8Parser.cmi diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 73118fa56..239d30d2d 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -752,7 +752,7 @@ let eval_ng_punct (_text, _prefix_len, punct) = match punct with | GrafiteAst.Dot _ -> NTactics.dot_tac | GrafiteAst.Semicolon _ -> fun x -> x - | GrafiteAst.Branch _ -> NTactics.branch_tac + | GrafiteAst.Branch _ -> NTactics.branch_tac ~force:false | GrafiteAst.Shift _ -> NTactics.shift_tac | GrafiteAst.Pos (_,l) -> NTactics.pos_tac l | GrafiteAst.Wildcard _ -> NTactics.wildcard_tac @@ -779,7 +779,7 @@ let eval_ng_tac tac = | GrafiteAst.NAuto (_loc, (l,a)) -> NAuto.auto_tac ~params:(List.map (fun x -> "",0,x) l,a) - | GrafiteAst.NBranch _ -> NTactics.branch_tac + | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false | GrafiteAst.NCases (_loc, what, where) -> NTactics.cases_tac ~what:(text,prefix_len,what) diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 6c6e07101..c1c7a9071 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -101,10 +101,11 @@ with type t = NCic.term and type input = NCic.term = struct let is_eq = function | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt -> - Some (ty,l,r) + Some (ty,l,r) +(* | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r] when eq equivalence_relation eqt && eq setoid_eq eqt2 -> - Some (ty,l,r) + Some (ty,l,r) *) | _ -> None let pp t = diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index 0bc4dc2c2..b80ac7e9c 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -21,19 +21,19 @@ let default_sig = function | 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";*) @@ -43,25 +43,25 @@ let set_reference_of_oxuri reference_of_oxuri = 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 ;; @@ -90,6 +90,7 @@ let debug c _ = c;; extract t ;; + let mk_predicate hole_type amount ft p1 vl = let rec aux t p = match p with @@ -98,16 +99,16 @@ let debug c _ = c;; 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 = @@ -122,29 +123,100 @@ let debug c _ = c;; 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 @@ -177,68 +249,94 @@ let debug c _ = c;; | 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 = @@ -249,42 +347,40 @@ let debug c _ = c;; 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 ;; diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index f7bc2eac9..0558e89c7 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -367,13 +367,15 @@ module Paramod (B : Orderings.Blob) = struct (List.iter (fun x -> ignore - (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x)) + (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x)); + Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x)) g_passives); ignore (List.iter (fun x -> ignore - (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x)) + (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x)); + Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x)) (g_actives@g_passives)); raise (Stop (Timeout (maxvar,bag))) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index ad9c155ca..53c87673b 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1675,7 +1675,7 @@ let group_by_tac ~eq_predicate ~action:tactic status = let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in List.map (fun x -> List.assoc x l2) l1 in - NTactics.block_tac ([ NTactics.branch_tac ] + NTactics.block_tac ([ NTactics.branch_tac ~force:false] @ HExtlib.list_concat ~sep:[NTactics.shift_tac] (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes) diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml index b2faf6d96..103791c03 100644 --- a/helm/software/components/ng_tactics/nDestructTac.ml +++ b/helm/software/components/ng_tactics/nDestructTac.ml @@ -283,7 +283,7 @@ let discriminate_tac ~context cur_eq status = leftno m)) (nbranches-1) [] in if nbranches > 1 then - NTactics.branch_tac:: branches @ [NTactics.merge_tac] + NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac] else branches in diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 10fa168d4..f5ae3a721 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -46,13 +46,14 @@ let dot_tac status = status#set_stack gstatus ;; -let branch_tac status = +let branch_tac ?(force=false) status = let gstatus = match status#stack with | [] -> assert false | (g, t, k, tag) :: s -> match init_pos g with (* TODO *) - | [] | [ _ ] -> fail (lazy "too few goals to branch") + | [] -> fail (lazy "empty goals") + | [_] when (not force) -> fail (lazy "too few goals to branch") | loc :: loc_tl -> ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s in @@ -644,7 +645,7 @@ let assert_tac seqs status = | [seq] -> assert0_tac seq | _ -> block_tac - (branch_tac:: + ((branch_tac ~force:false):: HExtlib.list_concat ~sep:[shift_tac] (List.map (fun seq -> [assert0_tac seq]) seqs)@ [merge_tac]) diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index efb4e843c..74bbcbcb4 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -12,7 +12,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) val dot_tac: 's NTacStatus.tactic -val branch_tac: 's NTacStatus.tactic +val branch_tac: ?force:bool -> 's NTacStatus.tactic val shift_tac: 's NTacStatus.tactic val pos_tac: int list -> 's NTacStatus.tactic val case_tac: string -> 's NTacStatus.tactic diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index e45873bc8..f64bb20ac 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -12,15 +12,10 @@ 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 () @@ -69,9 +64,9 @@ let is_a_fact status ty = 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;; @@ -79,7 +74,7 @@ let is_a_fact_obj s uri = 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 @@ -113,35 +108,35 @@ let solve fast status eq_cache goal = 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 @@ -168,6 +163,7 @@ let auto_eq_check eq_cache 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 @@ -177,17 +173,17 @@ let index_local_equations eq_cache status = (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 ;; @@ -235,7 +231,7 @@ let demod_tac ~params s = 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) ;; @@ -244,9 +240,9 @@ let args_for_context ?(k=1) ctx = 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 @@ -266,11 +262,11 @@ let refresh metasenv = (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 @@ -282,24 +278,24 @@ let close_metasenv metasenv subst = 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 ;; @@ -314,13 +310,13 @@ let ground_instances status gl = 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 @@ -331,11 +327,11 @@ let replace_meta i args target = 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 @@ -354,8 +350,8 @@ let close_wrt_metasenv subst = (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 @@ -984,10 +980,10 @@ let smart_applicative_case dbd 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 @@ -1048,14 +1044,14 @@ let prunable_for_size flags s m todo = | (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 @@ -1075,22 +1071,22 @@ let prunable ty 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); @@ -1101,8 +1097,8 @@ let prunable menv subst ty todo = 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 @@ -1131,8 +1127,8 @@ let 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 @@ -1176,8 +1172,8 @@ let auto dbd flags metasenv tables universe cache context metasenv gl = 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 @@ -1210,11 +1206,11 @@ let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goa 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 @@ -1280,7 +1276,7 @@ let smart_apply t unit_eq status g = 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 @@ -1355,6 +1351,19 @@ let add_to_th t c ty = 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 -> @@ -1400,7 +1409,7 @@ type flags = { 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 } @@ -1479,7 +1488,7 @@ let height_of_goals status = (* 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; @@ -1494,11 +1503,11 @@ let only signature _context candidate = 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 ;; @@ -1519,11 +1528,11 @@ let try_candidate ?(smart=0) flags depth status eq_cache t = 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)) @@ -1540,32 +1549,34 @@ let get_candidates ?(smart=true) status cache signature gty = | 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 @@ -1587,7 +1598,7 @@ let applicative_case depth signature status flags gty (cache:cache) = (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 *) @@ -1599,13 +1610,13 @@ let applicative_case depth signature status flags gty (cache:cache) = 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 @@ -1614,17 +1625,17 @@ let applicative_case depth signature status flags gty (cache:cache) = 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 ;; @@ -1635,7 +1646,7 @@ exception Found (* 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 @@ -1645,32 +1656,32 @@ let is_subsumed depth status gty cache = 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) ;; @@ -1701,23 +1712,22 @@ let intro ~depth status facts name = 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 ;; @@ -1734,6 +1744,9 @@ let reduce ~depth status g = (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]) ;; @@ -1745,15 +1758,18 @@ let do_something signature flags status g depth gty cache = 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 ;; @@ -1766,8 +1782,8 @@ let pp_goals status l = 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) ;; @@ -1787,20 +1803,20 @@ let sort_tac status = | [] -> 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 ;; @@ -1811,11 +1827,11 @@ let clean_up_tac status = | [] -> 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 ;; @@ -1826,144 +1842,167 @@ let focus_tac focus status = | [] -> 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 @@ -2013,18 +2052,21 @@ let auto_tac ~params:(_univ,flags) status = 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 -- 2.39.2