diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 6 | ||||
| -rw-r--r-- | interp/declare.ml | 135 | ||||
| -rw-r--r-- | interp/declare.mli | 8 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 41 | ||||
| -rw-r--r-- | interp/notation.mli | 6 |
6 files changed, 142 insertions, 56 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1df24f717..bc8debd02d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -383,7 +383,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -514,7 +514,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations ind) + (uninterp_ind_pattern_notations scopes ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -734,7 +734,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_notation scopes vars r'' (uninterp_notations scopes r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) diff --git a/interp/declare.ml b/interp/declare.ml index 1b4645aff6..1aeb67afbb 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -453,28 +453,95 @@ let input_universe_context : universe_context_decl -> Libobject.obj = let declare_universe_context poly ctx = Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) -(* Discharged or not *) -type universe_decl = polymorphic * Universes.universe_binders - -let cache_universes (p, l) = - let glob = Global.global_universe_names () in - let glob', ctx = - Id.Map.fold (fun id lev ((idl,lid),ctx) -> - ((Id.Map.add id (p, lev) idl, - Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) - l (glob, Univ.ContextSet.empty) +(** Global universes are not substitutive objects but global objects + bound at the *library* or *module* level. The polymorphic flag is + used to distinguish universes declared in polymorphic sections, which + are discharged and do not remain in scope. *) + +type universe_source = + | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *) + | QualifiedUniv of Id.t (* global universe introduced by some global value *) + | UnqualifiedUniv (* other global universe *) + +type universe_decl = universe_source * Nametab.universe_id + +let add_universe src (dp, i) = + let level = Univ.Level.make dp i in + let optpoly = match src with + | BoundUniv -> Some true + | UnqualifiedUniv -> Some false + | QualifiedUniv _ -> None in - cache_universe_context (p, ctx); - Global.set_global_universe_names glob' + Option.iter (fun poly -> + let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in + Global.push_context_set poly ctx; + Universes.add_global_universe level poly; + if poly then Lib.add_section_context ctx) + optpoly -let input_universes : universe_decl -> Libobject.obj = +let check_exists sp = + let depth = sections_depth () in + let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in + if Nametab.exists_universe sp then + alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") + else () + +let qualify_univ src (sp,i as orig) = + match src with + | BoundUniv | UnqualifiedUniv -> orig + | QualifiedUniv l -> + let sp0, id = Libnames.repr_path sp in + let sp0 = DirPath.repr sp0 in + Libnames.make_path (DirPath.make (l::sp0)) id, i+1 + +let cache_universe ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,1) in + let () = check_exists sp in + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe src id + +let load_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in + let () = Nametab.push_universe (Nametab.Until i) sp id in + add_universe src id + +let open_universe i ((sp, _), (src, id)) = + let sp, i = qualify_univ src (sp,i) in + let () = Nametab.push_universe (Nametab.Exactly i) sp id in + () + +let discharge_universe = function + | _, (BoundUniv, _) -> None + | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x + +let input_universe : universe_decl -> Libobject.obj = declare_object { (default_object "Global universe name state") with - cache_function = (fun (na, pi) -> cache_universes pi); - load_function = (fun _ (_, pi) -> cache_universes pi); - discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); - classify_function = (fun a -> Keep a) } + cache_function = cache_universe; + load_function = load_universe; + open_function = open_universe; + discharge_function = discharge_universe; + subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + classify_function = (fun a -> Substitute a) } + +let declare_univ_binders gr pl = + if Global.is_polymorphic gr then + Universes.register_universe_binders gr pl + else + let l = match gr with + | ConstRef c -> Label.to_id @@ Constant.label c + | IndRef (c, _) -> Label.to_id @@ MutInd.label c + | VarRef id -> id + | ConstructRef _ -> + anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on an constructor reference") + in + Id.Map.iter (fun id lvl -> + match Univ.Level.name lvl with + | None -> () + | Some na -> + ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na)))) + pl let do_universe poly l = let in_section = Lib.sections_are_opened () in @@ -484,11 +551,14 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.fold_left (fun acc (l, id) -> - let lev = Universes.new_univ_level (Global.current_dirpath ()) in - Id.Map.add id lev acc) Id.Map.empty l + List.map (fun (l, id) -> + let lev = Universes.new_univ_id () in + (id, lev)) l in - Lib.add_anonymous_leaf (input_universes (poly, l)) + let src = if poly then BoundUniv else UnqualifiedUniv in + List.iter (fun (id,lev) -> + ignore(Lib.add_leaf id (input_universe (src, lev)))) + l type constraint_decl = polymorphic * Univ.constraints @@ -510,20 +580,15 @@ let input_constraints : constraint_decl -> Libobject.obj = discharge_function = discharge_constraints; classify_function = (fun a -> Keep a) } +let loc_of_glob_level = function + | Misctypes.GType (Misctypes.UNamed n) -> Libnames.loc_of_reference n + | _ -> None + let do_constraint poly l = - let open Misctypes in let u_of_id x = - match x with - | GProp -> Loc.tag (false, Univ.Level.prop) - | GSet -> Loc.tag (false, Univ.Level.set) - | GType None | GType (Some (_, Anonymous)) -> - user_err ~hdr:"Constraint" - (str "Cannot declare constraints on anonymous universes") - | GType (Some (loc, Name id)) -> - let names, _ = Global.global_universe_names () in - try loc, Id.Map.find id names - with Not_found -> - user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id) + let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in + let loc = loc_of_glob_level x in + loc, Universes.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -541,7 +606,7 @@ let do_constraint poly l = ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + let ploc, p, lu = u_of_id l and rloc, p', ru = u_of_id r in check_poly ?loc:ploc p rloc p'; Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l diff --git a/interp/declare.mli b/interp/declare.mli index d50d37368c..f368d164e9 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -80,13 +80,11 @@ val recursive_message : bool (** true = fixpoint *) -> val exists_name : Id.t -> bool - - (** Global universe contexts, names and constraints *) +val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit val do_universe : polymorphic -> Id.t Loc.located list -> unit -val do_constraint : polymorphic -> - (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> - unit +val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> + unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 13ed65056d..0197cf9ae2 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -72,7 +72,7 @@ open Decl_kinds let type_of_logical_kind = function | IsDefinition def -> (match def with - | Definition -> "def" + | Definition | Let -> "def" | Coercion -> "coe" | SubClass -> "subclass" | CanonicalStructure -> "canonstruc" diff --git a/interp/notation.ml b/interp/notation.ml index f36294f732..94ce2a6c8d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -526,15 +526,38 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) - -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table - -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let sort_notations scopes l = + let extract_scope l = function + | Scope sc -> List.partitioni (fun _i x -> + match x with + | NotationRule (Some sc',_),_,_ -> String.equal sc sc' + | _ -> false) l + | SingleNotation ntn -> List.partitioni (fun _i x -> + match x with + | NotationRule (None,ntn'),_,_ -> String.equal ntn ntn' + | _ -> false) l in + let rec aux l scopes = + if l == [] then [] (* shortcut *) else + match scopes with + | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes + | [] -> l in + aux l scopes + +let uninterp_notations scopes c = + let scopes = make_current_scopes scopes in + let keys = glob_constr_keys c in + let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in + sort_notations scopes maps + +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_scopes scopes in + let maps = keymap_find (cases_pattern_key c) !notations_key_table in + sort_notations scopes maps + +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_scopes scopes in + let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in + sort_notations scopes maps let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index 2066d346fe..7d055571c8 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -124,9 +124,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : local_scopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first |