]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_kernel/nCicUntrusted.ml
Huge commit with several changes:
[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.ml
index 167fd47c9e313fa5e574a9f3794d25d47cf12eb0..dc26794a1a096cb4f9575e93cf9e826cbe83989a 100644 (file)
@@ -22,15 +22,23 @@ let map_term_fold_a g k f a = function
  | C.Rel _ as t -> a,t
  | C.Appl [] | C.Appl [_] -> assert false
  | C.Appl l as orig ->
+    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
-    a, if l1 == l then orig else (match l1 with
-       | C.Appl l :: tl -> C.Appl (l@tl)
-       | _ -> C.Appl l1)
+    a, if l1 == l then orig else 
+       let t =
+        match l1 with
+         | C.Appl l :: tl -> C.Appl (l@tl)
+         | _ -> C.Appl l1
+       in
+        if fire_beta then NCicReduction.head_beta_reduce ~upto t
+        else t
  | C.Prod (n,s,t) as orig ->
      let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
      a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
@@ -72,3 +80,171 @@ let metas_of_term subst context term =
     HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
 ;;
 
+module NCicHash =
+ Hashtbl.Make
+  (struct
+    type t = C.term
+    let equal = (==)
+    let hash = Hashtbl.hash_param 100 1000 
+   end)
+;;
+
+let mk_appl he args = 
+  if args = [] then he else
+  match he with
+  | 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 apply_subst 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
+       Not_found ->
+        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
+  clean_or_fix_dependent_abstrations context (apply_subst subst () t)
+;;
+
+let apply_subst_context subst context =
+  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 subst ctx,apply_subst subst ctx ty)) ::
+         apply_subst_metasenv subst tl
+;;
+
+let height_of_term tl =
+ let h = ref 0 in
+ let get_height (NReference.Ref (uri,_)) =
+  let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
+   height in
+ let rec aux =
+  function
+     NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
+   | NCic.Meta _ -> ()
+   | NCic.Rel _
+   | NCic.Sort _ -> ()
+   | NCic.Implicit _ -> assert false
+   | NCic.Const nref -> h := max !h (get_height nref)
+   | NCic.Prod (_,t1,t2)
+   | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
+   | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
+   | NCic.Appl l -> List.iter aux l
+   | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
+ in
+  List.iter aux tl;
+  1 + !h
+;;
+
+let height_of_obj_kind uri =
+ function
+    NCic.Inductive _
+  | NCic.Constant (_,_,None,_,_)
+  | NCic.Fixpoint (false,_,_) -> 0
+  | NCic.Fixpoint (true,ifl,_) ->
+     let iflno = List.length ifl in
+      height_of_term
+       (List.fold_left
+        (fun l (_,_,_,ty,bo) ->
+          let bo = NCicTypeChecker.debruijn uri iflno [] bo in
+           ty::bo::l
+       ) [] ifl)
+  | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
+;;