patch to make it compile with recent OCaml versions

[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.ml

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 771f3070bda456a9ae31c91000bf96b553fc4492..022482b0a9e60c44e20398d586b74bd9ddaa9e2a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -175,21 +175,23 @@ let rec fire_projection_redex on_args = function
       in
       if pragma <> `Projection || List.length args <= rno then conclude ()
       else
-        (match List.nth args rno with
+        (match List.nth l (rno+1) with
         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
-            let t = C.Appl (fbody::args) in
+            let t = C.Appl (fbody::List.tl l) in
             (match NCicReduction.head_beta_reduce ~delta:max_int t with
-            | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
+             | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
+                ::kargs),[pat])->
                   let _,kargs = HExtlib.split_nth leftno kargs in
-        fire_projection_redex false 
-                  (NCicReduction.head_beta_reduce 
-                    ~delta:max_int (C.Appl (pat :: kargs)))
-            | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) ->
+                   fire_projection_redex false 
+                    (NCicReduction.head_beta_reduce 
+                      ~delta:max_int (C.Appl (pat :: kargs)))
+            | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))
+               ::kargs),[pat]) :: args) ->
                   let _,kargs = HExtlib.split_nth leftno kargs in
-        fire_projection_redex false 
-                  (NCicReduction.head_beta_reduce 
-                    ~delta:max_int (C.Appl (pat :: kargs @ args)))
+                   fire_projection_redex false 
+                    (NCicReduction.head_beta_reduce 
+                      ~delta:max_int (C.Appl (pat :: kargs @ args)))
             | _ -> conclude ()) 
         | _ -> conclude ())
   | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
@@ -264,8 +266,14 @@ let rec replace_in_metasenv i f = function
   | 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 
+  (newkind :> NCic.meta_attr) :: List.filter (fun x -> not (is_kind x)) attrs 
 ;;
 
 let max_kind k1 k2 = 
@@ -275,3 +283,68 @@ 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)
+;;
+
+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 -> ()
+    | C.Implicit _ -> ()
+    | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
+    | C.Meta (mno,(s,l)) ->
+         (try
+            (* possible optimization here: try does_not_occur on l and
+               perform substitution only if DoesOccur is raised *)
+            let _,_,term,_ = NCicUtils.lookup_subst mno subst in
+            aux (k-s) () (NCicSubstitution.subst_meta (0,l) term)
+          with NCicUtils.Subst_not_found _ -> () (*match l with
+          | C.Irl len -> if not (n+k >= s+len || s > nn+k) then raise DoesOccur
+          | C.Ctx lc -> List.iter (aux (k-s) ()) lc*))
+    | t -> NCicUtils.fold (fun _ k -> k + 1) k aux () t
+  in
+   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
+;;