X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=0fbea89affeb2879d9ad01a80533899a05ea4e1d;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=82f7cef800fc8874467d972dd40f2c29bb0d22e2;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 82f7cef80..0fbea89af 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -175,23 +175,21 @@ let rec fire_projection_redex on_args = function
       in
       if pragma <> `Projection || List.length args <= rno then conclude ()
       else
-        (match List.nth l (rno+1) with
+        (match List.nth args rno with
         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
             let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *)
-            let t = C.Appl (fbody::List.tl l) in
+            let t = C.Appl (fbody::args) 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
@@ -273,7 +271,7 @@ let rec replace_in_subst i f = function
 ;;
           
 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 = 
@@ -283,68 +281,3 @@ 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
-;;