Added a "sort_metasenv" function.

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 8c827a7598c9ce8b98ef08fd9c5c0a61ae59c5a9..1d8f6c49e3527ceccacc3a32a2952d7bd2252ec0 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -281,3 +281,32 @@ let max_kind k1 k2 =
   | _ -> `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)
+;;

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index bb5aa304974cbebe30fcd993e7d9adb91af1fab8..cb0b54b82ef18e72451b275c3e7912989e46cbb7 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -19,6 +19,7 @@ val map_obj_kind:
   ?skip_body:bool -> (NCic.term -> NCic.term) -> NCic.obj_kind -> NCic.obj_kind
 
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
+val sort_metasenv: NCic.substitution -> NCic.metasenv -> NCic.metasenv
 
 type meta_kind = [ `IsSort | `IsType | `IsTerm ]
 val kind_of_meta: NCic.meta_attrs -> meta_kind