auto rewritten with only one tail recursive function.

[helm.git] / components / tactics / proofEngineHelpers.ml

diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml
index 177471c7403a4d9eb2da538289f76e5e718f0681..2a637135351516703b6e83e8c500ef467e11687a 100644 (file)
--- a/components/tactics/proofEngineHelpers.ml
+++ b/components/tactics/proofEngineHelpers.ml
@@ -648,3 +648,36 @@ let split_with_whd (c, t) =
       | v                   -> aux true a n c (CicReduction.whd c v)
     in
     aux false [] 0 c t
+
+
+  (* menv sorting *)
+module OT = 
+  struct 
+    type t = Cic.conjecture
+    let compare (i,_,_) (j,_,_) = Pervasives.compare i j
+  end
+module MS = HTopoSort.Make(OT)
+let relations_of_menv m c =
+  let i, ctx, ty = c in
+  let m = List.filter (fun (j,_,_) -> j <> i) m in
+  let m_ty = List.map fst (CicUtil.metas_of_term ty) in
+  let m_ctx = 
+    List.flatten
+      (List.map 
+        (function 
+         | None -> []
+         | Some (_,Cic.Decl t)
+         | Some (_,Cic.Def (t,None)) -> 
+             List.map fst (CicUtil.metas_of_term ty)
+         | Some (_,Cic.Def (t,Some ty)) -> 
+             List.map fst (CicUtil.metas_of_term ty) @
+             List.map fst (CicUtil.metas_of_term t))
+        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 (m : Cic.metasenv) =
+  (MS.topological_sort m (relations_of_menv m) : Cic.metasenv)
+;;
+