let tempi_type_of_aux = ref 0.0;;
*)
+let newmeta =
+ let maxmeta = ref 0 in
+ fun () -> incr maxmeta; !maxmeta
+;;
exception NotInTheList;;
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
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 ->
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
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
*)
let delift_rels subst metasenv n t =
delift_rels_from subst metasenv 1 n t
-
+*)
*)
(* $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) ->
| 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 *)
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
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)
+ *)
projects / helm.git / commitdiff