X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=22845725ac05e983aec69d23bc133bd5265e2274;hb=da59a744767c799ad287489c55f2ff972f93d93c;hp=c6201ce458e48b8e03d49924603c19f23231ef22;hpb=ae3540a0dc8b1e1cccb04b811bf558fb6fff9577;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml index c6201ce45..22845725a 100644 --- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml +++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml @@ -35,6 +35,7 @@ (* *) (*****************************************************************************) +(* $Id$ *) (* ************************************************************************** * CicEnvironment SETTINGS (trust and clean_tmp) @@ -56,7 +57,7 @@ type type_checked_obj = ;; exception AlreadyCooked of string;; -exception CircularDependency of string;; +exception CircularDependency of string Lazy.t;; exception CouldNotFreeze of string;; exception CouldNotUnfreeze of string;; exception Object_not_found of UriManager.uri;; @@ -141,142 +142,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 len = List.length fl in - 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 len = List.length fl in - 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 := [] ; @@ -301,7 +166,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)) @@ -356,7 +223,7 @@ module Cache : let univ = if o = None then "NO_UNIV" else "" in print_endline (su^" "^univ)) !frozen_list; - raise (CircularDependency (UriManager.string_of_uri uri)) + raise (CircularDependency (lazy (UriManager.string_of_uri uri))) end else if HT.mem cacheOfCookedObjects uri then @@ -576,7 +443,7 @@ let set_type_checking_info ?(replace_ugraph_and_univlist=None) uri = * return the object,ugraph *) let add_trusted_uri_to_cache uri = - let o,u,_ = find_or_add_to_unchecked uri in + let _ = find_or_add_to_unchecked uri in Cache.unchecked_to_frozen uri; set_type_checking_info uri; try