diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 95 |
1 files changed, 52 insertions, 43 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index b0303a30..a07f5c84 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reserve.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* Reserved names *) open Util @@ -17,23 +15,44 @@ open Nameops open Summary open Libobject open Lib +open Topconstr +open Libnames + +type key = + | RefKey of global_reference + | Oth let reserve_table = ref Idmap.empty +let reserve_revtable = ref Gmapl.empty + +let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *) + | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args) + | AList (_,_,AApp (ARef ref,args),_,_) + | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args) + | ARef ref -> RefKey(canonical_gr ref), None + | _ -> Oth, None let cache_reserved_type (_,(id,t)) = - reserve_table := Idmap.add id t !reserve_table + let key = fst (aconstr_key t) in + reserve_table := Idmap.add id t !reserve_table; + reserve_revtable := Gmapl.add key (t,id) !reserve_revtable -let (in_reserved, _) = +let in_reserved : identifier * aconstr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } +let freeze_reserved () = (!reserve_table,!reserve_revtable) +let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr +let init_reserved () = + reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty + let _ = Summary.declare_summary "reserved-type" - { Summary.freeze_function = (fun () -> !reserve_table); - Summary.unfreeze_function = (fun r -> reserve_table := r); - Summary.init_function = (fun () -> reserve_table := Idmap.empty) } + { Summary.freeze_function = freeze_reserved; + Summary.unfreeze_function = unfreeze_reserved; + Summary.init_function = init_reserved } -let declare_reserved_type (loc,id) t = +let declare_reserved_type_binding (loc,id) t = if id <> root_of_id id then user_err_loc(loc,"declare_reserved_type", (pr_id id ++ str @@ -45,46 +64,36 @@ let declare_reserved_type (loc,id) t = with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) +let declare_reserved_type idl t = + List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl) + let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table -open Rawterm - -let rec unloc = function - | RVar (_,id) -> RVar (dummy_loc,id) - | RApp (_,g,args) -> RApp (dummy_loc,unloc g, List.map unloc args) - | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c) - | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c) - | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,sty,rtntypopt,tml,pl) -> - RCases (dummy_loc,sty, - (Option.map unloc rtntypopt), - List.map (fun (tm,x) -> (unloc tm,x)) tml, - List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | RLetTuple (_,nal,(na,po),b,c) -> - RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) - | RIf (_,c,(na,po),b1,b2) -> - RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) - | RRec (_,fk,idl,bl,tyl,bv) -> - RRec (dummy_loc,fk,idl, - Array.map (List.map - (fun (na,k,obd,ty) -> (na,k,Option.map unloc obd, unloc ty))) - bl, - Array.map unloc tyl, - Array.map unloc bv) - | RCast (_,c, CastConv (k,t)) -> RCast (dummy_loc,unloc c, CastConv (k,unloc t)) - | RCast (_,c, CastCoerce) -> RCast (dummy_loc,unloc c, CastCoerce) - | RSort (_,x) -> RSort (dummy_loc,x) - | RHole (_,x) -> RHole (dummy_loc,x) - | RRef (_,x) -> RRef (dummy_loc,x) - | REvar (_,x,l) -> REvar (dummy_loc,x,l) - | RPatVar (_,x) -> RPatVar (dummy_loc,x) - | RDynamic (_,x) -> RDynamic (dummy_loc,x) +let constr_key c = + try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c)))) + with Not_found -> Oth + +let revert_reserved_type t = + try + let l = Gmapl.find (constr_key t) !reserve_revtable in + let t = Detyping.detype false [] [] t in + list_try_find + (fun (pat,id) -> + try let _ = match_aconstr false t ([],pat) in Name id + with No_match -> failwith "") l + with Not_found | Failure _ -> Anonymous + +let _ = Namegen.set_reserved_typed_name revert_reserved_type + +open Glob_term let anonymize_if_reserved na t = match na with | Name id as na -> (try - if not !Flags.raw_print & unloc t = find_reserved_type id - then RHole (dummy_loc,Evd.BinderType na) + if not !Flags.raw_print & + (try aconstr_of_glob_constr [] [] t = find_reserved_type id + with UserError _ -> false) + then GHole (dummy_loc,Evd.BinderType na) else t with Not_found -> t) | Anonymous -> t |