From 5cbd03ea1aef33b66c1db22b2de2d9d2f95acb14 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 15:16:33 +0000
Subject: [PATCH] added function to fresh types

---
 helm/software/components/cic/unshare.ml  | 123 +++++++++++++++++++++++
 helm/software/components/cic/unshare.mli |   1 +
 2 files changed, 124 insertions(+)

diff --git a/helm/software/components/cic/unshare.ml b/helm/software/components/cic/unshare.ml
index 3205e4f62..405e1d586 100644
--- a/helm/software/components/cic/unshare.ml
+++ b/helm/software/components/cic/unshare.ml
@@ -89,3 +89,126 @@ let unshare ?(fresh_univs=false) t =
  in
   unshare t
 ;;
+
+let sharing_map f l =
+  let unchanged = ref true in
+  let rec aux b = function
+    | [] as t -> unchanged := b; t
+    | he::tl ->
+        let he1 = f he in
+        he1 :: aux (b && he1 == he) tl
+  in
+  let l1 = aux true l in
+  if !unchanged then l else l1
+;;
+
+let fresh_univs t =
+ let module C = Cic in
+ let rec unshare =
+  function
+   | C.Sort (C.Type u) when not (CicUniv.is_anon u) -> C.Sort (C.Type (CicUniv.fresh ()))
+   | C.Sort _ | C.Implicit _ | C.Var _ | C.Rel _ as t -> t
+   | C.Meta (i,l) as orig -> 
+      let l' = sharing_map 
+        (function None -> None | Some t -> Some (unshare t)) l
+      in
+      if l == l' then orig else C.Meta(i,l')
+   | C.Cast (te,ty) as orig -> 
+      let te' = unshare te in 
+      let ty' = unshare ty in
+      if te' == te && ty' == ty then orig else C.Cast(te', ty')
+   | C.Prod (n,s,t) as orig -> 
+      let s' = unshare s in             
+      let t' = unshare t in             
+      if s' == s && t' == t then orig else C.Prod(n,s',t')
+   | C.Lambda (n,s,t) as orig -> 
+      let s' = unshare s in             
+      let t' = unshare t in             
+      if s' == s && t' == t then orig else C.Lambda(n,s',t')
+   | C.LetIn (n,s,ty,t) as orig ->
+      let s' = unshare s in             
+      let t' = unshare t in             
+      let ty' = unshare ty in             
+      if t' == t && ty' == ty && s' == s then orig else C.LetIn (n, s', ty', t')
+   | C.Appl l as orig -> 
+      let l' = sharing_map unshare l in 
+      if l == l' then orig else C.Appl l'
+   | C.Const (uri,exp_named_subst) as orig ->
+      let exp_named_subst' = 
+        sharing_map 
+          (fun (uri,t as orig) -> 
+            let t' = unshare t in 
+            if t == t' then orig else (uri,t')) 
+          exp_named_subst
+      in
+      if exp_named_subst' == exp_named_subst then orig
+      else C.Const (uri,exp_named_subst')
+   | C.MutInd (uri,tyno,exp_named_subst) as orig ->
+      let exp_named_subst' = 
+        sharing_map 
+          (fun (uri,t as orig) -> 
+            let t' = unshare t in 
+            if t == t' then orig else (uri,t')) 
+          exp_named_subst
+      in
+      if exp_named_subst' == exp_named_subst then orig
+      else C.MutInd (uri,tyno,exp_named_subst')
+   | C.MutConstruct (uri,tyno,consno,exp_named_subst) as orig ->
+      let exp_named_subst' = 
+        sharing_map 
+          (fun (uri,t as orig) -> 
+            let t' = unshare t in 
+            if t == t' then orig else (uri,t')) 
+          exp_named_subst
+      in
+      if exp_named_subst' == exp_named_subst then orig
+      else C.MutConstruct (uri,tyno,consno,exp_named_subst')
+   | C.MutCase (sp,i,outty,t,pl) as orig ->
+      let t' = unshare t in 
+      let pl' = sharing_map unshare pl in
+      let outty' = unshare outty in
+      if t' == t && pl' == pl && outty' == outty then orig
+      else C.MutCase (sp, i, outty', t', pl')
+   | C.Fix (i, fl) as orig ->
+      let fl' =
+       sharing_map
+        (fun (name, i, ty, bo as orig) -> 
+           let ty' = unshare ty in
+           let bo' = unshare bo in
+           if ty' == ty && bo' == bo then orig else name,i,ty',bo')
+         fl
+      in
+      if fl' == fl then orig else C.Fix (i, fl')
+   | C.CoFix (i, fl) as orig ->
+      let fl' =
+       sharing_map
+        (fun (name, ty, bo as orig) -> 
+           let ty' = unshare ty in
+           let bo' = unshare bo in
+           if ty' == ty && bo' == bo then orig else name,ty',bo')
+         fl
+      in
+      if fl' == fl then orig else C.CoFix (i, fl')
+ in
+  unshare t
+;;
+
+let fresh_types = 
+  let module C = Cic in
+  let unshare = fresh_univs in      
+  function
+   | C.Constant (name,te,ty,exp,att) ->
+        C.Constant (name,HExtlib.map_option unshare te,
+          unshare ty,exp,att)
+   | C.CurrentProof _ -> assert false
+   | C.Variable _ -> assert false
+   | C.InductiveDefinition (itl,u,i,att) ->
+        C.InductiveDefinition
+          (List.map 
+            (fun (name,b,t,cl) -> 
+               name,b,unshare t,
+               List.map 
+                 (fun (name,t) -> name, unshare t) 
+                 cl) 
+            itl,u,i,att)
+;;
diff --git a/helm/software/components/cic/unshare.mli b/helm/software/components/cic/unshare.mli
index a40be17ba..0dffb532e 100644
--- a/helm/software/components/cic/unshare.mli
+++ b/helm/software/components/cic/unshare.mli
@@ -24,3 +24,4 @@
  *)
 
 val unshare : ?fresh_univs:bool -> Cic.term -> Cic.term
+val fresh_types: Cic.obj -> Cic.obj
-- 
2.39.2