\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
- List.find (fun (index', _, _, _) -> index = index') metasenv
- with Not_found -> raise (Meta_not_found index)
+ List.assoc n metasenv
+ with Not_found -> raise (Meta_not_found n)
| NCic.Match (_,oty,t,pl) -> List.fold_left (f k) (f k (f k acc oty) t) pl
;;
| 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
-;;
-
if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
| NCic.Lambda (n,s,t) as orig ->
let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
if t1 == t && s1 == s then orig else NCic.Prod (n,s1,t1)
| NCic.Lambda (n,s,t) as orig ->
let s1 = f k s in let t1 = f (g (n,NCic.Decl s) k) t in
| NCic.LetIn (n,ty,t,b) as orig ->
let ty1 = f k ty in let t1 = f k t in
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 ->
| NCic.LetIn (n,ty,t,b) as orig ->
let ty1 = f k ty in let t1 = f k t in
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 ->
if oty1 == oty && t1 == t && pl1 == pl then orig
else NCic.Match(r,oty1,t1,pl1)
;;
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
-;;
-