diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-04-04 14:49:06 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-04-04 14:49:06 +0200 |
commit | 16536fd734d6a7aaa6ff85f56cef629df74ce36a (patch) | |
tree | a9ffc8d0830c7c826ea164b5267f95985365fe63 /interp/notation.ml | |
parent | 5569a06d062f913c66cbcb8bd01d4505e603d321 (diff) | |
parent | 6aa58955515dff338ea85d59073dfc0d0c7648ab (diff) |
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into JasonGross-trunk-function_scope
Diffstat (limited to 'interp/notation.ml')
-rw-r--r-- | interp/notation.ml | 44 |
1 files changed, 16 insertions, 28 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index ab0dcbeb7..b8f4f3201 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -65,11 +65,9 @@ let empty_scope = { } let default_scope = "" (* empty name, not available from outside *) -let type_scope = "type_scope" (* special scope used for interpreting types *) let init_scope_map () = - scope_map := String.Map.add default_scope empty_scope !scope_map; - scope_map := String.Map.add type_scope empty_scope !scope_map + scope_map := String.Map.add default_scope empty_scope !scope_map (**********************************************************************) (* Operations on scopes *) @@ -559,23 +557,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -type scope_class = ScopeRef of global_reference | ScopeSort +open Classops -let scope_class_compare sc1 sc2 = match sc1, sc2 with -| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2 -| ScopeRef _, ScopeSort -> -1 -| ScopeSort, ScopeRef _ -> 1 -| ScopeSort, ScopeSort -> 0 +type scope_class = cl_typ -let scope_class_of_reference x = ScopeRef x +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord let compute_scope_class t = - let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in - match kind_of_term t' with - | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') - | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p)) - | Sort _ -> ScopeSort - | _ -> raise Not_found + let (cl,_,_) = find_class_type Evd.empty t in + cl module ScopeClassOrd = struct @@ -586,7 +577,7 @@ end module ScopeClassMap = Map.Make(ScopeClassOrd) let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty + ScopeClassMap.empty let scope_class_map = ref initial_scope_class_map @@ -620,8 +611,11 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t) let compute_type_scope t = find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) -let compute_scope_of_global ref = - find_scope_class_opt (Some (ScopeRef ref)) +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + +let scope_class_of_class (x : cl_typ) : scope_class = + x (** Updating a scope list, thanks to a list of argument classes and the current Bind Scope base. When some current scope @@ -653,12 +647,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_scope_class subst cs = match cs with - | ScopeSort -> Some cs - | ScopeRef t -> - let (t',c) = subst_global subst t in - if t == t' then Some cs - else try Some (compute_scope_class c) with Not_found -> None +let subst_scope_class subst cs = + try Some (subst_cl_typ subst cs) with Not_found -> None let subst_arguments_scope (subst,(req,r,scl,cls)) = let r' = fst (subst_global subst r) in @@ -791,9 +781,7 @@ let pr_delimiters_info = function let classes_of_scope sc = ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map [] -let pr_scope_class = function - | ScopeSort -> str "Sort" - | ScopeRef t -> pr_global_env Id.Set.empty t +let pr_scope_class = pr_class let pr_scope_classes sc = let l = classes_of_scope sc in |