nasty change in the lexer/parser:

[helm.git] / helm / software / components / ng_kernel / nCicUntrusted.ml

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml
index 95f40da5368ff06fe99991f33dc372c3d67f6d57..baae7f9c2f7486e1561b3ad6a47eddaeb7522c5b 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.ml
+++ b/helm/software/components/ng_kernel/nCicUntrusted.ml
@@ -96,14 +96,16 @@ let mk_appl he args =
   | _ -> NCic.Appl (he::args)
 ;;
 
-let map_obj_kind f =
+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,HExtlib.map_option f bo, f 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,f bo)
+       (function (relevance,name,recno,ty,bo) -> 
+          relevance,name,recno,f ty,do_bo f bo)
        fl
      in
       NCic.Fixpoint (ind,fl,attrs)
@@ -122,7 +124,51 @@ let map_obj_kind f =
       NCic.Inductive (is_ind,lno,itl,attrs)
 ;;
 
-let apply_subst subst t = 
+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) ->
@@ -141,6 +187,25 @@ let apply_subst subst t =
                    apply_subst subst () (NCicSubstitution.lift n t)) l))))
   | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
  in
-  apply_subst subst () t
+  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
+;;