From 024819eeb7fcd370114ceb3dffc7907db92ab640 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 2 Dec 2005 17:53:23 +0000 Subject: [PATCH] moved (and hence exported) uri rehashing functions on terms and objects to CicUtil --- helm/ocaml/cic/cicUtil.ml | 133 +++++++++++++++++ helm/ocaml/cic/cicUtil.mli | 11 +- .../cic_proof_checking/cicEnvironment.ml | 138 +----------------- 3 files changed, 141 insertions(+), 141 deletions(-) diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml index 818342515..bb356655a 100644 --- a/helm/ocaml/cic/cicUtil.ml +++ b/helm/ocaml/cic/cicUtil.ml @@ -227,3 +227,136 @@ let id_of_annterm = | Cic.AMutCase (id,_,_,_,_,_) | Cic.AFix (id,_,_) | Cic.ACoFix (id,_,_) -> id + + +let rec rehash_term = + let module C = Cic in + let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + function + | (C.Rel _) as t -> t + | C.Var (uri,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) ->(recons uri,rehash_term 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 (rehash_term t) + ) l + in + C.Meta(i,l') + | C.Sort (C.Type u) -> + CicUniv.assert_univ u; + C.Sort (C.Type (CicUniv.recons_univ u)) + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (rehash_term te, rehash_term ty) + | C.Prod (n,s,t) -> C.Prod (n, rehash_term s, rehash_term t) + | C.Lambda (n,s,t) -> C.Lambda (n, rehash_term s, rehash_term t) + | C.LetIn (n,s,t) -> C.LetIn (n, rehash_term s, rehash_term t) + | C.Appl l -> C.Appl (List.map rehash_term l) + | C.Const (uri,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst + in + C.Const (uri',exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst + in + C.MutInd (uri',tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let uri' = recons uri in + let exp_named_subst' = + List.map + (function (uri,t) -> (recons uri,rehash_term t)) exp_named_subst + in + C.MutConstruct (uri',tyno,consno,exp_named_subst') + | C.MutCase (uri,i,outty,t,pl) -> + C.MutCase (recons uri, i, rehash_term outty, rehash_term t, + List.map rehash_term pl) + | C.Fix (i, fl) -> + let liftedfl = + List.map + (fun (name, i, ty, bo) -> + (name, i, rehash_term ty, rehash_term bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, rehash_term ty, rehash_term bo)) + fl + in + C.CoFix (i, liftedfl) + +let rehash_obj = + let module C = Cic in + let recons uri = UriManager.uri_of_string (UriManager.string_of_uri uri) in + function + C.Constant (name,bo,ty,params,attrs) -> + let bo' = + match bo with + None -> None + | Some bo -> Some (rehash_term bo) + in + let ty' = rehash_term ty in + let params' = List.map recons params in + C.Constant (name, bo', ty', params',attrs) + | C.CurrentProof (name,conjs,bo,ty,params,attrs) -> + let conjs' = + List.map + (function (i,hyps,ty) -> + (i, + List.map (function + None -> None + | Some (name,C.Decl t) -> + Some (name,C.Decl (rehash_term t)) + | Some (name,C.Def (bo,ty)) -> + let ty' = + match ty with + None -> None + | Some ty'' -> Some (rehash_term ty'') + in + Some (name,C.Def (rehash_term bo, ty'))) hyps, + rehash_term ty)) + conjs + in + let bo' = rehash_term bo in + let ty' = rehash_term ty in + let params' = List.map recons params in + C.CurrentProof (name, conjs', bo', ty', params',attrs) + | C.Variable (name,bo,ty,params,attrs) -> + let bo' = + match bo with + None -> None + | Some bo -> Some (rehash_term bo) + in + let ty' = rehash_term ty in + let params' = List.map recons params in + C.Variable (name, bo', ty', params',attrs) + | C.InductiveDefinition (tl,params,paramsno,attrs) -> + let params' = List.map recons params in + let tl' = + List.map (function (name, inductive, ty, constructors) -> + name, + inductive, + rehash_term ty, + (List.map + (function (name, ty) -> name, rehash_term ty) + constructors)) + tl + in + C.InductiveDefinition (tl', params', paramsno, attrs) + diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli index 3243faec8..b6fd7459d 100644 --- a/helm/ocaml/cic/cicUtil.mli +++ b/helm/ocaml/cic/cicUtil.mli @@ -44,12 +44,6 @@ val strip_prods: int -> Cic.term -> Cic.term val term_of_uri: UriManager.uri -> Cic.term (** @raise UriManager.IllFormedUri *) val uri_of_term: Cic.term -> UriManager.uri (** @raise Invalid_argument "uri_of_term" *) -(* - (** packing/unpacking of several terms into a single one *) -val pack: Cic.term list -> Cic.term -val unpack: Cic.term -> Cic.term list -*) - val id_of_annterm: Cic.annterm -> Cic.id (** {2 Cic selectors} *) @@ -60,3 +54,8 @@ val attributes_of_obj: Cic.obj -> Cic.attribute list (** mk_rels [howmany] [from] * creates a list of [howmany] rels starting from [from] in decreasing order *) val mk_rels : int -> int -> Cic.term list + +(** {2 Uri hash consing} *) +val rehash_term: Cic.term -> Cic.term +val rehash_obj: Cic.obj -> Cic.obj + diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index 8a9bbf667..00c7f9206 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -141,140 +141,6 @@ module Cache : (* unchecked is used to store objects just fetched, nothing more. *) let unchecked_list = ref [];; - (* FIXED: should be ok even if not touched *) - (* used to hash cons uris on restore to grant URI structure unicity *) - let restore_uris = - let module C = Cic in - let recons uri = - UriManager.uri_of_string (UriManager.string_of_uri uri) - in - let rec restore_in_term = - function - | (C.Rel _) as t -> t - | C.Var (uri,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) ->(recons uri,restore_in_term 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 (restore_in_term t) - ) l - in - C.Meta(i,l') - | C.Sort (C.Type u) -> - CicUniv.assert_univ u; - C.Sort (C.Type (CicUniv.recons_univ u)) - | C.Sort _ as t -> t - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> C.Cast (restore_in_term te, restore_in_term ty) - | C.Prod (n,s,t) -> C.Prod (n, restore_in_term s, restore_in_term t) - | C.Lambda (n,s,t) -> C.Lambda (n, restore_in_term s, restore_in_term t) - | C.LetIn (n,s,t) -> C.LetIn (n, restore_in_term s, restore_in_term t) - | C.Appl l -> C.Appl (List.map restore_in_term l) - | C.Const (uri,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.Const (uri',exp_named_subst') - | C.MutInd (uri,tyno,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.MutInd (uri',tyno,exp_named_subst') - | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> - let uri' = recons uri in - let exp_named_subst' = - List.map - (function (uri,t) -> (recons uri,restore_in_term t)) exp_named_subst - in - C.MutConstruct (uri',tyno,consno,exp_named_subst') - | C.MutCase (uri,i,outty,t,pl) -> - C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t, - List.map restore_in_term pl) - | C.Fix (i, fl) -> - let liftedfl = - List.map - (fun (name, i, ty, bo) -> - (name, i, restore_in_term ty, restore_in_term bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo)) - fl - in - C.CoFix (i, liftedfl) - in - function - C.Constant (name,bo,ty,params,attrs) -> - let bo' = - match bo with - None -> None - | Some bo -> Some (restore_in_term bo) - in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.Constant (name, bo', ty', params',attrs) - | C.CurrentProof (name,conjs,bo,ty,params,attrs) -> - let conjs' = - List.map - (function (i,hyps,ty) -> - (i, - List.map (function - None -> None - | Some (name,C.Decl t) -> - Some (name,C.Decl (restore_in_term t)) - | Some (name,C.Def (bo,ty)) -> - let ty' = - match ty with - None -> None - | Some ty'' -> Some (restore_in_term ty'') - in - Some (name,C.Def (restore_in_term bo, ty'))) hyps, - restore_in_term ty)) - conjs - in - let bo' = restore_in_term bo in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.CurrentProof (name, conjs', bo', ty', params',attrs) - | C.Variable (name,bo,ty,params,attrs) -> - let bo' = - match bo with - None -> None - | Some bo -> Some (restore_in_term bo) - in - let ty' = restore_in_term ty in - let params' = List.map recons params in - C.Variable (name, bo', ty', params',attrs) - | C.InductiveDefinition (tl,params,paramsno,attrs) -> - let params' = List.map recons params in - let tl' = - List.map (function (name, inductive, ty, constructors) -> - name, - inductive, - restore_in_term ty, - (List.map - (function (name, ty) -> name, restore_in_term ty) - constructors)) - tl - in - C.InductiveDefinition (tl', params', paramsno, attrs) - ;; - let empty () = HT.clear cacheOfCookedObjects; unchecked_list := [] ; @@ -299,7 +165,9 @@ module Cache : (fun k (v,u,l) -> callback (UriManager.string_of_uri k); let reconsed_entry = - restore_uris v,CicUniv.recons_graph u,List.map CicUniv.recons_univ l + CicUtil.rehash_obj v, + CicUniv.recons_graph u, + List.map CicUniv.recons_univ l in HT.add cacheOfCookedObjects (UriManager.uri_of_string (UriManager.string_of_uri k)) -- 2.39.2