\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-(* $Id: nCicSubstitution.ml 8135 2008-02-13 15:35:43Z tassi $ *)
+(* $Id$ *)
exception Subst_not_found of int
exception Meta_not_found of int
| NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
;;
-let sharing_map f l =
- let unchanged = ref true in
- let rec aux b = function
- | [] as t -> unchanged := b; t
- | he::tl ->
- let he1 = f he in
- he1 :: aux (b && he1 == he) tl
- in
- let l1 = aux true l in
- if !unchanged then l else l1
-;;
-
let map g k f = function
| NCic.Meta _ -> assert false
| NCic.Implicit _
| NCic.Rel _ as t -> t
| NCic.Appl [] | NCic.Appl [_] -> assert false
| NCic.Appl l as orig ->
- (match sharing_map (f k) l with
+ (match HExtlib.sharing_map (f k) l with
| NCic.Appl l :: tl -> NCic.Appl (l@tl)
| l1 when l == l1 -> orig
| l1 -> NCic.Appl l1)
let b1 = f (g (n,NCic.Def (t,ty)) k) b in
if ty1 == ty && t1 == t && b1 == b then orig else NCic.LetIn (n,ty1,t1,b1)
| NCic.Match (r,oty,t,pl) as orig ->
- let oty1 = f k oty in let t1 = f k t in let pl1 = sharing_map (f k) pl in
+ let oty1 = f k oty in let t1 = f k t in let pl1 = HExtlib.sharing_map (f k) pl in
if oty1 == oty && t1 == t && pl1 == pl then orig
else NCic.Match(r,oty1,t1,pl1)
;;
-
-exception NotClosed
-
-let is_closed t =
- try
- let rec aux k _ = function
- | NCic.Rel n when n > k -> raise NotClosed
- | NCic.Meta (_, (s, NCic.Irl n)) when not (n+s <= k) -> raise NotClosed
- | NCic.Meta (_, (s, NCic.Ctx l)) -> List.iter (aux (k+s) ()) l
- | _ -> fold (fun _ k -> k + 1) k aux () t
- in
- aux 0 () t; true
- with NotClosed -> false
-;;
-