X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=9c96469e55053487f64026c66184648f9a0d2684;hb=f1fc99e982ca6c9c939504c4dcf773edf582792a;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..9c96469e5 100644
--- 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
@@ -244,3 +246,91 @@ 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)
+;;
+
+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
+;;