let fire_beta, upto =
match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0
in
- let a,l1 =
- (* sharing fold? *)
- List.fold_right
- (fun t (a,l) -> let a,t = f k a t in a, t :: l)
- l (a,[])
- in
+ let a,l1 = HExtlib.sharing_map_acc (f k) a l in
a, if l1 == l then orig else
let t =
match l1 with
a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
| C.Match (r,oty,t,pl) as orig ->
let a,oty1 = f k a oty in let a,t1 = f k a t in
- let a,pl1 =
- (* sharing fold? *)
- List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[])
- in
+ let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in
a, if oty1 == oty && t1 == t && pl1 == pl then orig
else C.Match(r,oty1,t1,pl1)
;;
(* hide optional arg *)
let apply_subst s c t = apply_subst s c t;;
+
+type meta_kind = [ `IsSort | `IsType | `IsTerm ]
+
+let is_kind x = x = `IsSort || x = `IsType || x = `IsTerm ;;
+
+let kind_of_meta l =
+ try
+ (match List.find is_kind l with
+ | `IsSort | `IsType | `IsTerm as x -> x
+ | _ -> assert false)
+ with
+ Not_found -> assert false
+;;
+
+let rec replace_in_metasenv i f = function
+ | [] -> assert false
+ | (j,e)::tl when j=i -> (i,f e) :: tl
+ | x::tl -> x :: replace_in_metasenv i f tl
+;;
+
+let rec replace_in_subst i f = function
+ | [] -> assert false
+ | (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
+;;
+
+let max_kind k1 k2 =
+ match k1, k2 with
+ | `IsSort, _ | _, `IsSort -> `IsSort
+ | `IsType, _ | _, `IsType -> `IsType
+ | _ -> `IsTerm
+;;
+
+module OT =
+ struct
+ type t = int * NCic.conjecture
+ let compare (i,_) (j,_) = Pervasives.compare i j
+ end
+
+module MS = HTopoSort.Make(OT)
+let relations_of_menv subst m c =
+ let i, (_, ctx, ty) = c in
+ let m = List.filter (fun (j,_) -> j <> i) m in
+ let m_ty = metas_of_term subst ctx ty in
+ let m_ctx =
+ snd
+ (List.fold_right
+ (fun i (ctx,res) ->
+ (i::ctx),
+ (match i with
+ | _,NCic.Decl ty -> metas_of_term subst ctx ty
+ | _,NCic.Def (t,ty) ->
+ metas_of_term subst ctx ty @ metas_of_term subst ctx t) @ res)
+ ctx ([],[]))
+ in
+ let metas = HExtlib.list_uniq (List.sort compare (m_ty @ m_ctx)) in
+ List.filter (fun (i,_) -> List.exists ((=) i) metas) m
+;;
+
+let sort_metasenv subst (m : NCic.metasenv) =
+ (MS.topological_sort m (relations_of_menv subst m) : NCic.metasenv)
+;;