X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=1d8f6c49e3527ceccacc3a32a2952d7bd2252ec0;hb=fa6d1f3df955464343b365114be1071fc0b0cd18;hp=b48db58ecbafcd15fcb3af9cff1d740b2daeb6f7;hpb=ab72456f3d53035e6942f1cafa225d6759acf655;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index b48db58ec..1d8f6c49e 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -244,3 +244,69 @@ let rec apply_subst_metasenv subst = function
 (* 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)
+;;