From: Andrea Asperti Date: Fri, 4 Dec 2009 08:45:24 +0000 (+0000) Subject: Indexing local context for paramod. X-Git-Tag: make_still_working~3182 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0232b651c37511743ce9e99d517a41adac3a7064;p=helm.git Indexing local context for paramod. --- diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend index ef100f742..587b29a3a 100644 --- a/helm/software/components/ng_tactics/.depend +++ b/helm/software/components/ng_tactics/.depend @@ -1,5 +1,6 @@ nTactics.cmi: nTacStatus.cmi andOrTree.cmi: zipTree.cmi +nnAuto.cmi: nTacStatus.cmi nAuto.cmi: nTacStatus.cmi nInversion.cmi: nTacStatus.cmi nDestructTac.cmi: nTacStatus.cmi @@ -15,8 +16,12 @@ zipTree.cmo: zipTree.cmi zipTree.cmx: zipTree.cmi andOrTree.cmo: zipTree.cmi andOrTree.cmi andOrTree.cmx: zipTree.cmx andOrTree.cmi -nAuto.cmo: zipTree.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi nAuto.cmi -nAuto.cmx: zipTree.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx nAuto.cmi +nnAuto.cmo: nTactics.cmi nTacStatus.cmi nnAuto.cmi +nnAuto.cmx: nTactics.cmx nTacStatus.cmx nnAuto.cmi +nAuto.cmo: zipTree.cmi nnAuto.cmi nTactics.cmi nTacStatus.cmi andOrTree.cmi \ + nAuto.cmi +nAuto.cmx: zipTree.cmx nnAuto.cmx nTactics.cmx nTacStatus.cmx andOrTree.cmx \ + nAuto.cmi nInversion.cmo: nTactics.cmi nCicElim.cmi nInversion.cmi nInversion.cmx: nTactics.cmx nCicElim.cmx nInversion.cmi nDestructTac.cmo: nTactics.cmi nTacStatus.cmi nDestructTac.cmi diff --git a/helm/software/components/ng_tactics/Makefile b/helm/software/components/ng_tactics/Makefile index 6bb0ac3ee..e83858e7e 100644 --- a/helm/software/components/ng_tactics/Makefile +++ b/helm/software/components/ng_tactics/Makefile @@ -7,6 +7,7 @@ INTERFACE_FILES = \ nTactics.mli \ zipTree.mli \ andOrTree.mli \ + nnAuto.mli \ nAuto.mli \ nInversion.mli \ nDestructTac.mli diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index 640128616..25f4e0fc7 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -13,7 +13,7 @@ open Printf -let debug = ref false +let debug = ref true let debug_print ?(depth=0) s = if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else () let debug_do f = if !debug then f () else () @@ -1499,7 +1499,7 @@ let auto_main flags signature (pos : 'a and_pos) cache = status pos cache and attack pos cache and_item = - show pos; (* uncomment to show the tree *) + (* show pos; uncomment to show the tree *) match and_item with | _, S _ -> assert false (* next would close the proof or give a D *) | _, L _ -> assert false (* L is a final solution *) @@ -1618,6 +1618,40 @@ let auto_tac ~params:(_univ,flags) status = up_to depth depth ;; +let rec rm_assoc n = function + | [] -> assert false + | (x,i)::tl when n=x -> i,tl + | p::tl -> let i,tl = rm_assoc n tl in i,p::tl +;; + +let merge canonicals elements n m = + let cn,canonicals = rm_assoc n canonicals in + let cm,canonicals = rm_assoc m canonicals in + let ln,elements = rm_assoc cn elements in + let lm,elements = rm_assoc cm elements in + let canonicals = + (n,cm)::(m,cm)::List.map + (fun (x,xc) as p -> + if xc = cn then (x,cm) else p) canonicals + in + let elements = (cn,ln@lm)::elements + in + canonicals,elements +;; + +let clusters f l = + let canonicals = List.map (fun x -> (x,x)) l in + let elements = List.map (fun x -> (x,[x])) l in + List.fold_left + (fun (canonicals,elements) x -> + let dep = f x in + List.fold_left + (fun (canonicals,elements) d -> + merge canonicals elements d x) + (canonicals,elements) dep) + (canonicals,elements) l +;; + let group_by_tac ~eq_predicate ~action:tactic status = let goals = head_goals status#stack in if List.length goals < 2 then tactic status @@ -1674,7 +1708,11 @@ let auto_tac ~params = (* ========================= dispatching of auto/auto_paramod ============ *) let auto_tac ~params:(_,flags as params) = if List.mem_assoc "paramodulation" flags then - auto_paramod_tac ~params + auto_paramod_tac ~params + else if List.mem_assoc "fast_paramod" flags then + NnAuto.fast_eq_check_tac ~params + else if List.mem_assoc "slir" flags then + NnAuto.auto_tac ~params else auto_tac ~params ;; diff --git a/helm/software/components/ng_tactics/nTactics.mli b/helm/software/components/ng_tactics/nTactics.mli index 4af0c3fb7..efb4e843c 100644 --- a/helm/software/components/ng_tactics/nTactics.mli +++ b/helm/software/components/ng_tactics/nTactics.mli @@ -74,6 +74,7 @@ val atomic_tac : [> `NoTag ]) list NTacStatus.status -> (< auto_cache : NCicLibrary.automation_cache; + eq_cache : NCicLibrary.unit_eq_cache; coerc_db : NCicCoercion.db; dump : NCicLibrary.obj list; lstatus : LexiconEngine.lexicon_status; obj : NCic.obj; set_coerc_db : NCicCoercion.db -> 'c; diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 0ff4ddbe5..827c1dc46 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -53,6 +53,25 @@ let auto_paramod_tac ~params status = NTactics.distribute_tac (auto_paramod ~params) status ;; +let fast_eq_check ~params status goal = + let gty = get_goalty status goal in + let n,h,metasenv,subst,o = status#obj in + let eq_cache = status#eq_cache in + let status,t = term_of_cic_term status gty (ctx_of gty) in + match + NCicParamod.fast_eq_check status metasenv subst (ctx_of gty) + eq_cache (NCic.Rel ~-1,t) + with + | [] -> raise (Error (lazy "no proof found",None)) + | (pt, metasenv, subst)::_ -> + let status = status#set_obj (n,h,metasenv,subst,o) in + instantiate status goal (mk_cic_term (ctx_of gty) pt) +;; + +let fast_eq_check_tac ~params = + NTactics.distribute_tac (fast_eq_check ~params) +;; + (*************** subsumption ****************) module IntSet = Set.Make(struct type t = int let compare = compare end) (* exceptions *) @@ -1367,6 +1386,22 @@ let equational_and_applicative_case elems, cache ;; +(* warning: ctx is supposed to be already instantiated w.r.t subst *) +let index_local_equations eq_cache ctx = + let c = ref 0 in + List.fold_left + (fun cache _ -> + c:= !c+1; + let t = NCic.Rel 1 in + try + let ty = NCicTypeChecker.typeof [] [] ctx t in + NCicParamod.forward_infer_step eq_cache t ty + with + | NCicTypeChecker.TypeCheckerFailure _ + | NCicTypeChecker.AssertFailure _ -> eq_cache) + eq_cache ctx +;; + let rec guess_name name ctx = if name = "_" then guess_name "auto" ctx else if not (List.mem_assoc name ctx) then name else