| (j,e)::tl when j=i -> (i,f e) :: tl
| x::tl -> x :: replace_in_subst i f tl
;;
-
+
let set_kind newkind attrs =
- newkind :: List.filter (fun x -> not (is_kind x)) attrs
+ (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs
;;
let max_kind k1 k2 =
(MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv)
;;
-let count_occurrences ~subst context n t =
+let count_occurrences ~subst n t =
let occurrences = ref 0 in
let rec aux k _ = function
| C.Rel m when m = n+k -> incr occurrences
- | C.Rel m ->
- (try match List.nth context (m-1-k) with
- | _,C.Def (bo,_) -> aux (n-m) () bo
- | _ -> ()
- with Failure _ -> assert false)
+ | C.Rel _m -> ()
+ | C.Implicit _ -> ()
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
| C.Meta (mno,(s,l)) ->
(try
aux 0 () t;
!occurrences
;;
+
+exception Found_variable
+
+let looks_closed t =
+ let rec aux k _ = function
+ | C.Rel m when k < m -> raise Found_variable
+ | C.Rel _m -> ()
+ | C.Implicit _ -> ()
+ | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+ | C.Meta _ -> raise Found_variable
+ | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
+ in
+ try aux 0 () t; true with Found_variable -> false
+;;