X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=8c827a7598c9ce8b98ef08fd9c5c0a61ae59c5a9;hb=846c22b353bed991d0504818fa58e5ed65dec670;hp=fd3fd5f794101b84ad230c8d347e056bfa44fed1;hpb=f1c4852a4359cf278ed00d73d608856ff46bafbb;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index fd3fd5f79..8c827a759 100644
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -25,12 +25,7 @@ let map_term_fold_a g k f a = function
     let fire_beta, upto = 
       match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 
     in
-    let a,l1 = 
-      (* sharing fold? *)
-      List.fold_right 
-        (fun t (a,l) -> let a,t = f k a t in a, t :: l) 
-        l (a,[])
-    in
+    let a,l1 = HExtlib.sharing_map_acc (f k) a l in
     a, if l1 == l then orig else 
        let t =
         match l1 with
@@ -51,10 +46,7 @@ let map_term_fold_a g k f a = function
      a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
  | C.Match (r,oty,t,pl) as orig -> 
      let a,oty1 = f k a oty in let a,t1 = f k a t in 
-     let a,pl1 = 
-       (* sharing fold? *)
-       List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[])
-     in
+     let a,pl1 = HExtlib.sharing_map_acc (f k) a pl in
      a, if oty1 == oty && t1 == t && pl1 == pl then orig 
         else C.Match(r,oty1,t1,pl1)
 ;;
@@ -168,17 +160,20 @@ let clean_or_fix_dependent_abstrations ctx t =
     aux (List.map fst ctx) t
 ;;
 
-let rec fire_projection_redex () = function
+let rec fire_projection_redex on_args = function
   | C.Meta _ as t -> t
   | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot->
-      let l = List.map (fire_projection_redex ()) ol in
+      let l= if on_args then List.map (fire_projection_redex true) ol else ol in
       let t = if l == ol then ot else C.Appl l in
       let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in
       let conclude () =
-        let l' = HExtlib.sharing_map (fire_projection_redex ()) l in
-        if l == l' then t else C.Appl l'
+        if on_args then 
+          let l' = HExtlib.sharing_map (fire_projection_redex true) l in
+          if l == l' then t else C.Appl l'
+        else
+          t (* ot is the same *) 
       in
-      if (*pragma <> `Projection ||*) List.length args < rno then conclude ()
+      if pragma <> `Projection || List.length args <= rno then conclude ()
       else
         (match List.nth args rno with
         | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) ->
@@ -187,15 +182,18 @@ let rec fire_projection_redex () = function
             (match NCicReduction.head_beta_reduce ~delta:max_int t with
             | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])->
                   let _,kargs = HExtlib.split_nth leftno kargs in
-                  NCicReduction.head_beta_reduce 
-                    ~delta:max_int (C.Appl (pat :: kargs))
+        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
-                  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 -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t
+  | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t
+  | t -> t
 ;;
 
 let apply_subst ?(fix_projections=false) subst context t = 
@@ -217,7 +215,7 @@ let apply_subst ?(fix_projections=false) subst context t =
                    apply_subst subst () (NCicSubstitution.lift n t)) l))))
   | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
  in
- (if fix_projections then fire_projection_redex () else fun x -> x)
+ (if fix_projections then fire_projection_redex true else fun x -> x)
     (clean_or_fix_dependent_abstrations context (apply_subst subst () t))
 ;;
 
@@ -246,3 +244,40 @@ 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
+;;
+