From: Enrico Tassi Date: Fri, 19 Sep 2008 11:35:37 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~4759 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6e785555b301cc1abe1671de3bd970aebebce71a;p=helm.git snapshot --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 57a1b7be7..121131f4d 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -145,6 +145,10 @@ let tempi_subst = ref 0.0;; let tempi_type_of_aux = ref 0.0;; *) +let newmeta = + let maxmeta = ref 0 in + fun () -> incr maxmeta; !maxmeta +;; exception NotInTheList;; @@ -160,340 +164,113 @@ let position n (shift, lc) = in aux 1 tl ;; -(* + exception Occur;; -let rec force_does_not_occur subst to_be_restricted t = - let module C = Cic in - let more_to_be_restricted = ref [] in +let rec force_does_not_occur metasenv subst restrictions t = let rec aux k = function - C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur - | C.Rel _ - | C.Sort _ as t -> t - | C.Implicit _ -> assert false - | C.Meta (n, l) -> - (* we do not retrieve the term associated to ?n in subst since *) - (* in this way we can restrict if something goes wrong *) + | C.Rel r when List.mem (r - k) restrictions -> raise Occur + | C.Meta (n, l) as t -> + (* we ignore the subst since restrict will take care of already + * instantiated/restricted metavariabels *) + let more_to_be_restricted = ref [] in let l' = let i = ref 0 in - List.map - (function t -> + HExtlib.map_option + (fun t -> incr i ; - match t with - None -> None - | Some t -> - try - Some (aux k t) - with Occur -> - more_to_be_restricted := (n,!i) :: !more_to_be_restricted; - None) + try + let (*subst, metasenv,*) t = aux k t in Some t + with Occur -> + more_to_be_restricted := !i :: !more_to_be_restricted; None) l in - C.Meta (n, l') - | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) - | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest) - | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest) - | C.LetIn (name,so,ty,dest) -> - C.LetIn (name, aux k so, aux k ty, aux (k+1) dest) - | C.Appl l -> C.Appl (List.map (aux k) l) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Var (uri, exp_named_subst') - | C.Const (uri, exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.Const (uri, exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.MutInd (uri, tyno, exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst - in - C.MutConstruct (uri, tyno, consno, exp_named_subst') - | C.MutCase (uri,tyno,out,te,pl) -> - C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl) - | C.Fix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl - in - C.Fix (i, fl') - | C.CoFix (i,fl) -> - let len = List.length fl in - let k_plus_len = k + len in - let fl' = - List.map - (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl - in - C.CoFix (i, fl') - in - let res = aux 0 t in - (!more_to_be_restricted, res) - -let rec restrict subst to_be_restricted metasenv = - match to_be_restricted with - | [] -> metasenv, subst - | _ -> - let names_of_context_indexes context indexes = - String.concat ", " - (List.map - (fun i -> - try - match List.nth context (i-1) with - | None -> assert false - | Some (n, _) -> CicPp.ppname n - with - Failure _ -> assert false - ) indexes) - in - let force_does_not_occur_in_context to_be_restricted = function - | None -> [], None - | Some (name, Cic.Decl t) -> - let (more_to_be_restricted, t') = - force_does_not_occur subst to_be_restricted t - in - more_to_be_restricted, Some (name, Cic.Decl t') - | Some (name, Cic.Def (bo, ty)) -> - let (more_to_be_restricted, bo') = - force_does_not_occur subst to_be_restricted bo - in - let more_to_be_restricted, ty' = - let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty + if !more_to_be_restricted = [] then + if l = l' then t else NCic.Meta (n, l') + else + let metasenv, subst, newmeta = + restrict metasenv subst n !more_to_be_restricted in - more_to_be_restricted @ more_to_be_restricted', - ty' - in - more_to_be_restricted, Some (name, Cic.Def (bo', ty')) - in - let rec erase i to_be_restricted n = function - | [] -> [], to_be_restricted, [] - | hd::tl -> - let more_to_be_restricted,restricted,tl' = - erase (i+1) to_be_restricted n tl - in - let restrict_me = List.mem i restricted in - if restrict_me then - more_to_be_restricted, restricted, None:: tl' - else - (try - let more_to_be_restricted', hd' = - let delifted_restricted = - let rec aux = - function - [] -> [] - | j::tl when j > i -> (j - i)::aux tl - | _::tl -> aux tl - in - aux restricted - in - force_does_not_occur_in_context delifted_restricted hd - in - more_to_be_restricted @ more_to_be_restricted', - restricted, hd' :: tl' - with Occur -> - more_to_be_restricted, (i :: restricted), None :: tl') - in - let (more_to_be_restricted, metasenv) = (* restrict metasenv *) - List.fold_right - (fun (n, context, t) (more, metasenv) -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [],[],context - else - erase 1 to_be_restricted n context - in - try - let more_to_be_restricted', t' = - force_does_not_occur subst restricted t - in - let metasenv' = (n, context', t') :: metasenv in - (more @ more_to_be_restricted @ more_to_be_restricted', - metasenv') - with Occur -> - raise (MetaSubstFailure (lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" - n (names_of_context_indexes context to_be_restricted))))) - metasenv ([], []) - in - let (more_to_be_restricted', subst) = (* restrict subst *) - List.fold_right - (* TODO: cambiare dopo l'aggiunta del ty *) - (fun (n, (context, term,ty)) (more, subst') -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - (try - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [], [], context - else - erase 1 to_be_restricted n context - in - let more_to_be_restricted', term' = - force_does_not_occur subst restricted term - in - let more_to_be_restricted'', ty' = - force_does_not_occur subst restricted ty in - let subst' = (n, (context', term',ty')) :: subst' in - let more = - more @ more_to_be_restricted - @ more_to_be_restricted'@more_to_be_restricted'' in - (more, subst') - with Occur -> - let error_msg = lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" - n (names_of_context_indexes context to_be_restricted) n - (ppterm ~metasenv subst term)) - in - (* DEBUG - debug_print (lazy error_msg); - debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); - debug_print (lazy ("subst = \n" ^ (ppsubst subst))); - debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) - raise (MetaSubstFailure error_msg))) - subst ([], []) - in - restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv -;; -*) + (*metasenv, subst,*) NCic.Meta (newmeta, l') + | t -> NCicUtils.map (fun _ k -> k+1) k aux t + in + aux 0 t -let newmeta = - let maxmeta = ref 0 in - fun () -> incr maxmeta; !maxmeta -;; +and force_does_not_occur_in_context metasenv subst restrictions = function + | name, NCic.Decl t as orig -> + let metasenv, subst, t' = + force_does_not_occur metasenv subst restrictions t + in + metasenv, subst, (if t == t' then orig else (name,NCic.Decl t')) + | name, NCic.Def (bo, ty) as orig -> + let metasenv, subst, bo' = + force_does_not_occur metasenv subst restrictions bo in + let metasenv, subst, ty' = + force_does_not_occur metasenv subst restrictions ty in + metasenv, subst, + (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty'))) -let restrict metasenv subst i to_be_restricted = - let force_does_not_occur_in_context to_be_restricted = function - | None -> [], None - | Some (name, Cic.Decl t) -> - let (more_to_be_restricted, t') = - force_does_not_occur subst to_be_restricted t - in - more_to_be_restricted, Some (name, Cic.Decl t') - | Some (name, Cic.Def (bo, ty)) -> - let (more_to_be_restricted, bo') = - force_does_not_occur subst to_be_restricted bo - in - let more_to_be_restricted, ty' = - let more_to_be_restricted', ty' = - force_does_not_occur subst to_be_restricted ty - in - more_to_be_restricted @ more_to_be_restricted', - ty' - in - more_to_be_restricted, Some (name, Cic.Def (bo', ty')) - in - let rec erase i to_be_restricted n = function - | [] -> [], to_be_restricted, [] - | hd::tl -> - let more_to_be_restricted,restricted,tl' = - erase (i+1) to_be_restricted n tl - in - let restrict_me = List.mem i restricted in - if restrict_me then - more_to_be_restricted, restricted, None:: tl' - else - (try - let more_to_be_restricted', hd' = - let delifted_restricted = - let rec aux = - function - [] -> [] - | j::tl when j > i -> (j - i)::aux tl - | _::tl -> aux tl - in - aux restricted - in - force_does_not_occur_in_context delifted_restricted hd - in - more_to_be_restricted @ more_to_be_restricted', - restricted, hd' :: tl' - with Occur -> - more_to_be_restricted, (i :: restricted), None :: tl') - in - let (more_to_be_restricted, metasenv) = (* restrict metasenv *) - List.fold_right - (fun (n, context, t) (more, metasenv) -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [],[],context - else - erase 1 to_be_restricted n context - in +and erase_in_context metasenv subst pos restrictions = function + | [] -> metasenv, subst, restrictions, [] + | hd::tl as orig -> + let metasenv, subst, restricted, tl' = + erase_in_context metasenv subst (i+1) restrictions tl in + if List.mem i restricted then + metasenv, subst, restricted, tl' + else try - let more_to_be_restricted', t' = - force_does_not_occur subst restricted t + let metasenv, subst, hd' = + let delifted_restricted = List.map ((+) ~-i) restricted in + force_does_not_occur_in_context + metasenv susbst delifted_restricted hd in - let metasenv' = (n, context', t') :: metasenv in - (more @ more_to_be_restricted @ more_to_be_restricted', - metasenv') + metasenv, subst, restricted, + (if hd' == hd && tl' == tl then orig else (hd' :: tl')) with Occur -> - raise (MetaSubstFailure (lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" - n (names_of_context_indexes context to_be_restricted))))) - metasenv ([], []) - in - let (more_to_be_restricted', subst) = (* restrict subst *) - List.fold_right - (* TODO: cambiare dopo l'aggiunta del ty *) - (fun (n, (context, term,ty)) (more, subst') -> - let to_be_restricted = - List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted) - in - (try - let (more_to_be_restricted, restricted, context') = - (* just an optimization *) - if to_be_restricted = [] then - [], [], context - else - erase 1 to_be_restricted n context - in - let more_to_be_restricted', term' = - force_does_not_occur subst restricted term - in - let more_to_be_restricted'', ty' = - force_does_not_occur subst restricted ty in - let subst' = (n, (context', term',ty')) :: subst' in - let more = - more @ more_to_be_restricted - @ more_to_be_restricted'@more_to_be_restricted'' in - (more, subst') - with Occur -> - let error_msg = lazy (sprintf - "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" - n (names_of_context_indexes context to_be_restricted) n - (ppterm ~metasenv subst term)) - in - (* DEBUG - debug_print (lazy error_msg); - debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); - debug_print (lazy ("subst = \n" ^ (ppsubst subst))); - debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) - raise (MetaSubstFailure error_msg))) - subst ([], []) - in - restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv -;; -*) -;; + metasenv, subst, (i :: restricted), tl' + +and restrict metasenv subst i restrictions = + assert (restrictions <> []); + try + let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in + try + let name, ctx, ty = NCicUtils.lookup_meta i metasenv in + let metasenv, subst, restrictions, newctx = + erase_in_context metasenv subst 1 restrictions in + let metasenv, subst, _ = + force_does_not_occur metasenv subst restrictions ty in + let metasenv, subst, _ = + force_does_not_occur metasenv subst restrictions bo in + (* we don't care newly generated bo/tys since up to subst they are + * convertible (only metas are substituted for metas *) + metasenv, subst, ? + with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf + ("Cannot restrict the context of the metavariable ?%d over "^^ + "the hypotheses %s since ?%d is already instantiated "^^ + "with %s and at least one of the hypotheses occurs in "^^ + "the substituted term" i (String.concat ", " + (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i + (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))) + with NCicUtils.Subst_not_found _ -> + try + let name, ctx, ty = NCicUtils.lookup_meta i metasenv in + let metasenv, subst, restrictions, newctx = + erase_in_context metasenv subst 1 restrictions in + let metasenv, subst, newty = + force_does_not_occur metasenv subst restrictions ty in + let j = newmeta () in + let metasenv_entry = j, (name, newctx, newty) in + let subst_entry = i,(name,ctx, NCic.Meta (j, irl - restrictions), ty) in + List.map + (fun (n,x) as orig -> if i = n then metasenv_entry else orig) metasenv, + subst_entry :: subst, j + with + | NCicUtils.Meta_not_found _ -> assert false + | Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf + ("Cannot restrict the context of the metavariable ?%d "^^ + "over the hypotheses %s since metavariable's type depends "^^ + "on at least one of them" i (String.concat ", " + (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))) (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), otherwise the occur check does not make sense in case of unification @@ -532,11 +309,14 @@ let delift metasenv subst context n l t = match lc, lc1 with | NCic.Irl len, NCic.Irl len1 when shift1 < shift || len1 + shift1 > len + shift -> - (* new meta with shortened l1 - (1 -> shift - shift1 /\ shift + len + 1 -> shift1+len1) - subst += (i,new meta) - restrict checks (deleted entry cannot occur in the type...) - return that meta *) + let restrictions = + HExtlib.list_seq 1 (shift - shift1) @ + HExtlib.list_seq (shift+len+1) (shift1+len1) + in + let subst, metasenv, newmeta = + restrict metasenv subst i restrictions + in + (* return that meta *) assert false | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig | NCic.Irl len, NCic.Irl len1 -> @@ -562,113 +342,7 @@ let delift metasenv subst context n l t = metasenv, subst, t ;; - - let to_be_restricted = ref [] in - let rec deliftaux k = - let module C = Cic in - function - | C.Rel m as t-> - if m <=k then - t - else - (try - match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> - (try - C.Rel ((position (m-k) l) + k) - with - NotInTheList -> - (*CSC: Hmmm. This bit of reduction is not in the spirit of *) - (*CSC: first order unification. Does it help or does it harm? *) - (*CSC: ANSWER: it hurts performances since it is possible to *) - (*CSC: have an exponential explosion of the size of the proof.*) - (*CSC: However, without this bit of reduction some "apply" in *) - (*CSC: the library fail (e.g. nat/nth_prime.ma). *) - deliftaux k (S.lift m t)) - | Some (_,C.Decl t) -> - C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) - with - Failure _ -> - raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l1) as t -> - (try - let (_,t,_) = CicUtil.lookup_subst i subst in - deliftaux k (CicSubstitution.subst_meta l1 t) - with CicUtil.Subst_not_found _ -> - (* see the top level invariant *) - if (i = n) then - raise (MetaSubstFailure (lazy (sprintf - "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm ~metasenv subst t)))) - else - begin - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := - (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') - end) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,ty,t) -> - C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, i, deliftaux k outty, deliftaux k t, - List.map (deliftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> - (name, i, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) +(* in let res = try @@ -708,7 +382,9 @@ debug_print(lazy (sprintf let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst ;; +*) +(* (* delifts a term t of n levels strating from k, that is changes (Rel m) * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails *) @@ -846,5 +522,5 @@ let delift_rels_from subst metasenv k n = let delift_rels subst metasenv n t = delift_rels_from subst metasenv 1 n t - +*) diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.ml b/helm/software/components/ng_refiner/nDiscriminationTree.ml index fb9b4c021..d3a334a59 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.ml +++ b/helm/software/components/ng_refiner/nDiscriminationTree.ml @@ -24,23 +24,9 @@ *) (* $Id$ *) - -type path_string_elem = - | Constant of NUri.uri * int (* name, arity *) - | Bound of int * int (* rel, arity *) - | Variable (* arity is 0 *) - | Proposition (* arity is 0 *) - | Datatype (* arity is 0 *) - | Dead (* arity is 0 *) -;; - -let arity_of = function - | Constant (_,a) - | Bound (_,a) -> a - | _ -> 0 -;; - -type path = path_string_elem list;; +(* +module NCicIndexable : Discrimination_tree.Indexable +with type input = NCic.term and type constant_name = NUri.uri = struct let ppelem = function | Constant (uri,arity) -> @@ -53,7 +39,7 @@ let ppelem = function | Dead -> "Dead" ;; -let path_string_of_term_with_jl = +let path_string_of = let rec aux arity = function | NCic.Appl ((NCic.Meta _|NCic.Implicit _)::_) -> [Variable] | NCic.Appl (NCic.Lambda _ :: _) -> [Variable] (* maybe we should b-reduce *) @@ -73,7 +59,7 @@ let path_string_of_term_with_jl = aux 0 ;; -let compare_elem e1 e2 = +let compare e1 e2 = match e1,e2 with | Constant (u1,a1),Constant (u2,a2) -> let x = NUri.compare u1 u2 in @@ -83,104 +69,8 @@ let compare_elem e1 e2 = let string_of_path l = String.concat "." (List.map ppelem l) ;; -module DiscriminationTreeIndexing = - functor (A:Set.S) -> - struct - - module OrderedPathStringElement = struct - type t = path_string_elem - let compare = compare_elem - end - - module PSMap = Map.Make(OrderedPathStringElement);; - - type key = PSMap.key - - module DiscriminationTree = Trie.Make(PSMap);; - - type t = A.t DiscriminationTree.t - - let empty = DiscriminationTree.empty;; - - let iter dt f = DiscriminationTree.iter (fun p x -> f p x) dt;; - - let index tree term info = - let ps = path_string_of_term_with_jl term in - let ps_set = - try DiscriminationTree.find ps tree with Not_found -> A.empty - in - DiscriminationTree.add ps (A.add info ps_set) tree - ;; - - let remove_index tree term info = - let ps = path_string_of_term_with_jl term in - try - let ps_set = A.remove info (DiscriminationTree.find ps tree) in - if A.is_empty ps_set then DiscriminationTree.remove ps tree - else DiscriminationTree.add ps ps_set tree - with Not_found -> tree - ;; - - let in_index tree term test = - let ps = path_string_of_term_with_jl term in - try - let ps_set = DiscriminationTree.find ps tree in - A.exists test ps_set - with Not_found -> false - ;; - - (* You have h(f(x,g(y,z)),t) whose path_string_of_term_with_jl is - (h,2).(f,2).(x,0).(g,2).(y,0).(z,0).(t,0) and you are at f and want to - skip all its progeny, thus you want to reach t. - - You need to skip as many elements as the sum of all arieties contained - in the progeny of f. - - The input ariety is the one of f while the path is x.g....t - Should be the equivalent of after_t in the literature (handbook A.R.) - *) - let rec skip arity path = - if arity = 0 then path else match path with - | [] -> assert false - | m::tl -> skip (arity-1+arity_of m) tl - ;; - - (* the equivalent of skip, but on the index, thus the list of trees - that are rooted just after the term represented by the tree root - are returned (we are skipping the root) *) - let skip_root = function DiscriminationTree.Node (_, map) -> - let rec get n = function DiscriminationTree.Node (_, m) as tree -> - if n = 0 then [tree] else - PSMap.fold (fun k v res -> (get (n-1 + arity_of k) v) @ res) m [] - in - PSMap.fold (fun k v res -> (get (arity_of k) v) @ res) map [] - ;; - - let retrieve unif tree term = - let path = path_string_of_term_with_jl term in - let rec retrieve path tree = - match tree, path with - | DiscriminationTree.Node (Some s, _), [] -> s - | DiscriminationTree.Node (None, _), [] -> A.empty - | DiscriminationTree.Node _, Variable::path when unif -> - List.fold_left A.union A.empty - (List.map (retrieve path) (skip_root tree)) - | DiscriminationTree.Node (_, map), node::path -> - A.union - (if not unif && node = Variable then A.empty else - try retrieve path (PSMap.find node map) - with Not_found -> A.empty) - (try - match PSMap.find Variable map,skip (arity_of node) path with - | DiscriminationTree.Node (Some s, _), [] -> s - | n, path -> retrieve path n - with Not_found -> A.empty) - in - retrieve path tree - ;; - - let retrieve_generalizations tree term = retrieve false tree term;; - let retrieve_unifiables tree term = retrieve true tree term;; - end -;; +end +module DiscriminationTree = + Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable) + *) diff --git a/helm/software/components/ng_refiner/nDiscriminationTree.mli b/helm/software/components/ng_refiner/nDiscriminationTree.mli index 1205fe38c..29fdbb68e 100644 --- a/helm/software/components/ng_refiner/nDiscriminationTree.mli +++ b/helm/software/components/ng_refiner/nDiscriminationTree.mli @@ -23,23 +23,10 @@ * http://cs.unibo.it/helm/. *) -type path - -val string_of_path : path -> string - -module DiscriminationTreeIndexing : - functor (A : Set.S) -> - sig - - type t - val iter : t -> (path -> A.t -> unit) -> unit - - val empty : t - val index : t -> NCic.term -> A.elt -> t - val remove_index : t -> NCic.term -> A.elt -> t - val in_index : t -> NCic.term -> (A.elt -> bool) -> bool - val retrieve_generalizations : t -> NCic.term -> A.t - val retrieve_unifiables : t -> NCic.term -> A.t - end - +(* +module NCicIndexable : Discrimination_tree.Indexable +with type input = NCic.term and type constant_name = NUri.uri +module DiscriminationTree : + Discrimination_tree.DiscriminationTreeIndexing(NCicIndexable) +*)