X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fcic%2Funshare.ml;fp=components%2Fcic%2Funshare.ml;h=405e1d586f8974221878f49832ffc22ade5b075b;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/cic/unshare.ml b/components/cic/unshare.ml new file mode 100644 index 000000000..405e1d586 --- /dev/null +++ b/components/cic/unshare.ml @@ -0,0 +1,214 @@ +(* Copyright (C) 2000, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id$ *) + +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) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (unshare t) + ) 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) + | C.Prod (n,s,t) -> C.Prod (n, unshare s, unshare t) + | C.Lambda (n,s,t) -> C.Lambda (n, unshare s, unshare t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unshare s, unshare ty, unshare t) + | C.Appl l -> C.Appl (List.map unshare l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst + in + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,unshare t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, unshare outty, unshare t, + List.map unshare pl) + | C.Fix (i, fl) -> + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, unshare ty, unshare bo)) + 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) +;;