X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicUntrusted.ml;h=1d8f6c49e3527ceccacc3a32a2952d7bd2252ec0;hb=0431f79f14bbf2cdc38c099cacba3a2f71363d7b;hp=4dcf01c53b1a43f2793cf29ca374e456cbdba62c;hpb=7bc72d8afaebb1d2070a26b07f9bf4242b648e2c;p=helm.git

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 4dcf01c53..1d8f6c49e 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)
 ;;
@@ -95,3 +87,226 @@ let mk_appl he args =
   | NCic.Appl l -> NCic.Appl (l@args)
   | _ -> NCic.Appl (he::args)
 ;;
+
+let map_obj_kind ?(skip_body=false) f =
+ let do_bo f x = if skip_body then x else f x in
+ function
+    NCic.Constant (relev,name,bo,ty,attrs) ->
+     NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
+  | NCic.Fixpoint (ind,fl,attrs) ->
+     let fl =
+      List.map
+       (function (relevance,name,recno,ty,bo) -> 
+          relevance,name,recno,f ty,do_bo f bo)
+       fl
+     in
+      NCic.Fixpoint (ind,fl,attrs)
+  | NCic.Inductive (is_ind,lno,itl,attrs) ->
+      let itl = 
+        List.map
+         (fun (relevance,name,ty,cl) ->
+           let cl = 
+             List.map (fun (relevance, name, ty) ->
+                relevance, name, f ty)
+             cl
+           in
+           relevance, name, f ty, cl)
+         itl
+      in
+      NCic.Inductive (is_ind,lno,itl,attrs)
+;;
+
+exception Occurr;;
+
+let clean_or_fix_dependent_abstrations ctx t =
+  let occurrs_1 t =
+    let rec aux n _ = function
+      | NCic.Meta _ -> ()
+      | NCic.Rel i when i = n + 1 -> raise Occurr
+      | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
+    in
+    try aux 0 () t; false
+    with Occurr -> true
+  in
+  let fresh ctx name = 
+    if not (List.mem name ctx) then name 
+    else
+     let rec aux i =
+       let attempt = name ^ string_of_int i in
+       if List.mem attempt ctx then aux (i+1) 
+       else attempt
+     in 
+      aux 0
+  in
+  let rec aux ctx = function
+  | NCic.Meta _ as t -> t
+  | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
+      let name = fresh ctx (String.sub name 1 (String.length name-1)) in
+      NCic.Prod (name,aux ctx s, aux (name::ctx) t)
+  | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
+      NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
+  | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
+  | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
+      let name = fresh ctx ("_"^name) in
+      NCic.Prod (name, aux ctx s, aux (name::ctx) t)
+  | NCic.Prod (name,s,t) when List.mem name ctx ->
+      let name = fresh ctx name in
+      NCic.Prod (name, aux ctx s, aux (name::ctx) t)
+  | NCic.Lambda (name,s,t) when List.mem name ctx ->
+      let name = fresh ctx name in
+      NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
+  | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t
+  in
+    aux (List.map fst ctx) t
+;;
+
+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= 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 () =
+        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 ()
+      else
+        (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::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])->
+                  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) ->
+                  let _,kargs = HExtlib.split_nth leftno kargs in
+        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
+  | t -> t
+;;
+
+let apply_subst ?(fix_projections=false) subst context t = 
+ let rec apply_subst subst () =
+ function
+    NCic.Meta (i,lc) ->
+     (try
+       let _,_,t,_ = NCicUtils.lookup_subst i subst in
+       let t = NCicSubstitution.subst_meta lc t in
+        apply_subst subst () t
+      with
+       NCicUtils.Subst_not_found j when j = i ->
+        match lc with
+           _,NCic.Irl _ -> NCic.Meta (i,lc)
+         | n,NCic.Ctx l ->
+            NCic.Meta
+             (i,(0,NCic.Ctx
+                 (List.map (fun 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 true else fun x -> x)
+    (clean_or_fix_dependent_abstrations context (apply_subst subst () t))
+;;
+
+let apply_subst_context ~fix_projections subst context =
+  let apply_subst = apply_subst ~fix_projections in
+  let rec aux c = function 
+    | [] -> []
+    | (name,NCic.Decl t as e) :: tl -> 
+        (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
+    | (name,NCic.Def (t1,t2) as e) :: tl -> 
+        (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) :: 
+          aux (e::c) tl
+  in
+    List.rev (aux [] (List.rev context))
+;;
+
+let rec apply_subst_metasenv subst = function
+  | [] -> []
+  | (i,_) :: _ when List.mem_assoc i subst -> assert false
+  | (i,(name,ctx,ty)) :: tl ->
+      (i,(name,apply_subst_context ~fix_projections:true subst ctx,
+               apply_subst ~fix_projections:true subst ctx ty)) ::
+         apply_subst_metasenv subst tl
+;;
+
+(* 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)
+;;