From 5e46e876ff3b3d94d357135fc7b7685620ca114a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jun 2005 14:56:24 +0000 Subject: [PATCH] changed select so that it returns a list of pairs --- helm/ocaml/cic/cicUtil.ml | 30 ++++++++++++++++-------------- helm/ocaml/cic/cicUtil.mli | 5 +++-- 2 files changed, 19 insertions(+), 16 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index a3649ca36..289d6d983 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -174,43 +174,46 @@ let uri_of_term = function | _ -> raise (Invalid_argument "uri_of_term") let select ~term ~context = - let rec aux context term = + (* i is the number of binder traversed *) + let rec aux i context term = match (context, term) with - | Cic.Implicit (Some `Hole), t -> [t] + | Cic.Implicit (Some `Hole), t -> [i,t] | Cic.Implicit None,_ -> [] | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) -> List.concat (List.map2 (fun t1 t2 -> - (match (t1, t2) with Some t1, Some t2 -> aux t1 t2 | _ -> [])) + (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> [])) ctxt1 ctxt2) - | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux te1 te2 @ aux ty1 ty2 + | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2 | Cic.Prod (_, s1, t1), Cic.Prod (_, s2, t2) | Cic.Lambda (_, s1, t1), Cic.Lambda (_, s2, t2) - | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> aux s1 s2 @ aux t1 t2 - | Cic.Appl terms1, Cic.Appl terms2 -> auxs terms1 terms2 + | Cic.LetIn (_, s1, t1), Cic.LetIn (_, s2, t2) -> + aux i s1 s2 @ aux (i+1) t1 t2 + | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2 | Cic.Var (_, subst1), Cic.Var (_, subst2) | Cic.Const (_, subst1), Cic.Const (_, subst2) | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2) | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) -> - auxs (List.map snd subst1) (List.map snd subst2) + auxs i (List.map snd subst1) (List.map snd subst2) | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) -> - aux out1 out2 @ aux t1 t2 @ auxs pat1 pat2 + aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2 | Cic.Fix (_, funs1), Cic.Fix (_, funs2) -> List.concat (List.map2 - (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2) + (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> + aux i ty1 ty2 @ aux i bo1 bo2) funs1 funs2) | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) -> List.concat (List.map2 - (fun (_, ty1, bo1) (_, ty2, bo2) -> aux ty1 ty2 @ aux bo1 bo2) + (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2) funs1 funs2) | _ -> assert false - and auxs terms1 terms2 = (* as aux for list of terms *) - List.concat (List.map2 aux terms1 terms2) + and auxs i terms1 terms2 = (* as aux for list of terms *) + List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2) in - aux context term + aux 0 context term let context_of ?(equality=(==)) ~term terms = let (===) x y = equality x y in @@ -282,7 +285,6 @@ let attributes_of_obj = function | Cic.CurrentProof (_, _, _, _, _, attributes) | Cic.InductiveDefinition (_, _, _, attributes) -> attributes - let rec mk_rels howmany from = match howmany with | 0 -> [] diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index a64a983f7..60c14f8a6 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -67,8 +67,9 @@ val context_of: Cic.term (** select all subterms of a given term matching a given context (i.e. subtrees -* rooted at context's holes *) -val select: term:Cic.term -> context:Cic.term -> Cic.term list +* rooted at context's holes. The first component is the number of binder the +* term is below *) +val select: term:Cic.term -> context:Cic.term -> (int * Cic.term) list (** mk_rels [howmany] [from] * creates a list of [howmany] rels starting from [from] in decreasing order *) -- 2.39.2