parameter sintax added to axiom statement

[helm.git] / helm / software / components / cic / unshare.ml

diff --git a/helm/software/components/cic/unshare.ml b/helm/software/components/cic/unshare.ml
index e4d2cc74a43951cc64ad8c99677100e39b1d5d75..405e1d586f8974221878f49832ffc22ade5b075b 100644 (file)
--- a/helm/software/components/cic/unshare.ml
+++ b/helm/software/components/cic/unshare.ml
@@ -25,8 +25,9 @@
 
 (* $Id$ *)
 
-let rec unshare =
+let unshare ?(fresh_univs=false) t =
  let module C = Cic in
+ let rec unshare =
   function
      C.Rel m -> C.Rel m
    | C.Var (uri,exp_named_subst) ->
@@ -43,6 +44,8 @@ let rec unshare =
         ) l
       in
        C.Meta(i,l')
+   | C.Sort s when not fresh_univs -> C.Sort s
+   | C.Sort (C.Type _) -> C.Sort (C.Type (CicUniv.fresh ()))
    | C.Sort s -> C.Sort s
    | C.Implicit info -> C.Implicit info
    | C.Cast (te,ty) -> C.Cast (unshare te, unshare ty)
@@ -83,3 +86,129 @@ let rec unshare =
          fl
       in
        C.CoFix (i, liftedfl)
+ 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)
+;;