diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr.ml | 12 | ||||
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 | ||||
| -rw-r--r-- | interp/constrextern.ml | 87 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.mli | 14 | ||||
| -rw-r--r-- | interp/declare.ml | 32 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 1 | ||||
| -rw-r--r-- | interp/impargs.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.mli | 1 | ||||
| -rw-r--r-- | interp/notation.ml | 325 | ||||
| -rw-r--r-- | interp/notation.mli | 23 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 12 | ||||
| -rw-r--r-- | interp/notation_term.ml | 4 |
13 files changed, 328 insertions, 192 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index 77d612cfd9..757d186c8b 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -80,8 +80,8 @@ type cases_pattern_expr_r = and cases_pattern_expr = cases_pattern_expr_r CAst.t and cases_pattern_notation_substitution = - cases_pattern_expr list * (** for constr subterms *) - cases_pattern_expr list list (** for recursive notations *) + cases_pattern_expr list * (* for constr subterms *) + cases_pattern_expr list list (* for recursive notations *) and constr_expr_r = | CRef of qualid * instance_expr option @@ -142,10 +142,10 @@ and local_binder_expr = | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = - constr_expr list * (** for constr subterms *) - constr_expr list list * (** for recursive notations *) - cases_pattern_expr list * (** for binders *) - local_binder_expr list list (** for binder lists (recursive notations) *) + constr_expr list * (* for constr subterms *) + constr_expr list list * (* for recursive notations *) + cases_pattern_expr list * (* for binders *) + local_binder_expr list list (* for binder lists (recursive notations) *) type constr_pattern_expr = constr_expr diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 3a4969a3ee..3a5af1dd5f 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -140,7 +140,7 @@ let rec constr_expr_eq e1 e2 = in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> - (** Don't care about the case_style *) + (* Don't care about the case_style *) Option.equal constr_expr_eq r1 r2 && List.equal case_expr_eq a1 a2 && List.equal branch_expr_eq brl1 brl2 @@ -220,7 +220,7 @@ and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> - (** Don't care about the [binder_kind] *) + (* Don't care about the [binder_kind] *) List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -258,7 +258,6 @@ let local_binders_loc bll = match bll with | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll)) (** Folds and maps *) - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 25f2526f74..0d0b6158d9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -110,13 +110,13 @@ let deactivate_notation nr = (* shouldn't we check wether it is well defined? *) inactive_notations_table := IRuleSet.add nr !inactive_notations_table | NotationRule (scopt, ntn) -> - match availability_of_notation (scopt, ntn) (scopt, []) with - | None -> user_err ~hdr:"Notation" + if not (exists_notation_interpretation_in_scope scopt ntn) then + user_err ~hdr:"Notation" (pr_notation ntn ++ spc () ++ str "does not exist" ++ (match scopt with | None -> spc () ++ str "in the empty scope." | Some _ -> show_scope scopt ++ str ".")) - | Some _ -> + else if IRuleSet.mem nr !inactive_notations_table then Feedback.msg_warning (str "Notation" ++ spc () ++ pr_notation ntn ++ spc () @@ -263,6 +263,11 @@ let rec insert_pat_coercion ?loc l c = match l with | [] -> c | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[]) +let add_lonely keyrule seen = + match keyrule with + | NotationRule (None,ntn) -> ntn::seen + | SynDefRule _ | NotationRule (Some _,_) -> seen + (**********************************************************************) (* conversion of references *) @@ -387,8 +392,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_pattern allscopes vars pat - (uninterp_cases_pattern_notations pat) + extern_notation_pattern allscopes [] vars pat + (uninterp_cases_pattern_notations scopes pat) with No_match -> let loc = pat.CAst.loc in match DAst.get pat with @@ -441,18 +446,15 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = insert_pat_coercion coercion pat and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) - (custom, (tmp_scope, scopes) as allscopes) vars = + (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars = function - | NotationRule (sc,ntn) -> + | NotationRule (sc,ntn),key,need_delim -> begin match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) (tmp_scope,scopes) with - (* Uninterpretation is not allowed in current context *) - | None -> raise No_match - (* Uninterpretation is allowed in current context *) - | Some (scopt,key) -> + let key = if need_delim || List.mem ntn lonely_seen then key else None in + let scopt = match key with Some _ -> sc | _ -> None in let scopes' = Option.List.cons scopt scopes in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -474,7 +476,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (insert_pat_delimiters ?loc (make_pat_notation ?loc ntn (l,ll) l2') key) end - | SynDefRule kn -> + | SynDefRule kn,key,need_delim -> + assert (key = None && need_delim = false); match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> @@ -492,9 +495,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) -and extern_notation_pattern allscopes vars t = function +and extern_notation_pattern allscopes lonely_seen vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> try if is_inactive_rule keyrule then raise No_match; let loc = t.loc in @@ -502,22 +505,27 @@ and extern_notation_pattern allscopes vars t = function | PatCstr (cstr,args,na) -> let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in let p = apply_notation_to_pattern ?loc (ConstructRef cstr) - (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in + (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars + (keyrule,key,need_delim) in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with - No_match -> extern_notation_pattern allscopes vars t rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation_pattern allscopes lonely_seen vars t rules -let rec extern_notation_ind_pattern allscopes vars ind args = function +let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> try if is_inactive_rule keyrule then raise No_match; apply_notation_to_pattern (IndRef ind) - (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule + (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim) with - No_match -> extern_notation_ind_pattern allscopes vars ind args rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation_ind_pattern allscopes lonely_seen vars ind args rules let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and @@ -529,8 +537,8 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args = else try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation_ind_pattern allscopes vars ind args - (uninterp_ind_pattern_notations ind) + extern_notation_ind_pattern allscopes [] vars ind args + (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 allscopes vars) args in @@ -760,32 +768,32 @@ let extern_ref vars ref us = let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None) -let rec extern inctx scopes vars r = +let rec extern inctx (custom,scopes as allscopes) vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + extern_optimal (extern_possible_prim_token allscopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal - (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r)) r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with - | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) + | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id) | c -> - match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with + match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - let scopes = (InConstrEntrySomeLevel, snd scopes) in + let scopes = (InConstrEntrySomeLevel, scopes) in let c = match c with (* The remaining cases are only for the constr entry *) @@ -797,7 +805,7 @@ let rec extern inctx scopes vars r = | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) | GEvar (n,l) -> - extern_evar n (List.map (on_snd (extern false scopes vars)) l) + extern_evar n (List.map (on_snd (extern false allscopes vars)) l) | GPatVar kind -> if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else @@ -952,7 +960,7 @@ let rec extern inctx scopes vars r = | GSort s -> CSort (extern_glob_sort s) - | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *) + | GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *) | GCast (c, c') -> CCast (sub_extern true scopes vars c, @@ -1056,9 +1064,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in make ?loc (pll,extern inctx scopes vars c) -and extern_notation (custom,scopes as allscopes) vars t = function +and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function | [] -> raise No_match - | (keyrule,pat,n as _rule)::rules -> + | (keyrule,pat,n as _rule,key,need_delim)::rules -> let loc = Glob_ops.loc_of_glob_constr t in try if is_inactive_rule keyrule then raise No_match; @@ -1106,11 +1114,8 @@ and extern_notation (custom,scopes as allscopes) vars t = function (match availability_of_entry_coercion custom (fst ntn) with | None -> raise No_match | Some coercion -> - match availability_of_notation (sc,ntn) scopes with - (* Uninterpretation is not allowed in current context *) - | None -> raise No_match - (* Uninterpretation is allowed in current context *) - | Some (scopt,key) -> + let key = if need_delim || List.mem ntn lonely_seen then key else None in + let scopt = match key with Some _ -> sc | None -> None in let scopes' = Option.List.cons scopt (snd scopes) in let l = List.map (fun (c,(subentry,(scopt,scl))) -> @@ -1146,7 +1151,9 @@ and extern_notation (custom,scopes as allscopes) vars t = function let args = extern_args (extern true) vars args in CAst.make ?loc @@ explicitize false argsimpls (None,e) args with - No_match -> extern_notation allscopes vars t rules + No_match -> + let lonely_seen = add_lonely keyrule lonely_seen in + extern_notation allscopes lonely_seen vars t rules and extern_recursion_order scopes vars = function GStructRec -> CStructRec diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6313f2d7ba..40922b5c35 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1507,7 +1507,7 @@ let drop_notations_pattern looked_for genv = let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found in - (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) + (* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes)) | GHole (_,_,_) -> RCPatAtom (None) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 035e4bc644..61acd09d65 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -45,13 +45,15 @@ type var_internalization_type = type var_internalization_data = var_internalization_type * - (** type of the "free" variable, for coqdoc, e.g. while typing the - constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + (* type of the "free" variable, for coqdoc, e.g. while typing the + constructor of JMeq, "JMeq" behaves as a variable of type Inductive *) + Id.t list * - (** impargs to automatically add to the variable, e.g. for "JMeq A a B b" - in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) - Impargs.implicit_status list * (** signature of impargs of the variable *) - Notation_term.scope_name option list (** subscopes of the args of the variable *) + (* impargs to automatically add to the variable, e.g. for "JMeq A a B b" + in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *) + + Impargs.implicit_status list * (* signature of impargs of the variable *) + Notation_term.scope_name option list (* subscopes of the args of the variable *) (** A map of free variables to their implicit arguments and scopes *) type internalization_env = var_internalization_data Id.Map.t diff --git a/interp/declare.ml b/interp/declare.ml index 1e972d3e35..a0ebc3775e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -56,7 +56,7 @@ let load_constant i ((sp,kn), obj) = (* Opening means making the name without its module qualification available *) let open_constant i ((sp,kn), obj) = - (** Never open a local definition *) + (* Never open a local definition *) if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in @@ -166,9 +166,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e export_seff || not de.const_entry_opaque || is_poly de -> - (** This globally defines the side-effects in the environment. We mark - exported constants as being side-effect not to redeclare them at - caching time. *) + (* This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) let de, export = Global.export_private_constants ~in_section de in export, ConstantEntry (PureEntry, DefinitionEntry de) | _ -> [], ConstantEntry (EffectEntry, cd) @@ -191,7 +191,6 @@ let declare_definition ?(internal=UserIndividualRequest) (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) (** Declaration of section variables and local definitions *) - type section_variable_entry = | SectionLocalDef of Safe_typing.private_constants definition_entry | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) @@ -214,16 +213,16 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - (** The body should already have been forced upstream because it is a - section-local definition, but it's not enforced by typing *) + (* The body should already have been forced upstream because it is a + section-local definition, but it's not enforced by typing *) let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in - (** We must declare the universe constraints before type-checking the - term. *) + (* We must declare the universe constraints before type-checking the + term. *) let () = Global.push_context_set (not poly) univs in let se = { secdef_body = body; @@ -262,7 +261,6 @@ let declare_variable id obj = oname (** Declaration of inductive blocks *) - let declare_inductive_argument_scopes kn mie = List.iteri (fun i {mind_entry_consnames=lc} -> Notation.declare_ref_arguments_scope Evd.empty (IndRef (kn,i)); @@ -360,7 +358,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter let id = Label.to_id label in let univs = match univs with | Monomorphic_ind_entry _ -> - (** Global constraints already defined through the inductive *) + (* Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty | Polymorphic_ind_entry (nas, ctx) -> Polymorphic_const_entry (nas, ctx) @@ -469,7 +467,7 @@ type universe_source = | QualifiedUniv of Id.t (* global universe introduced by some global value *) | UnqualifiedUniv (* other global universe *) -type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list +type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list let check_exists sp = if Nametab.exists_universe sp then @@ -511,7 +509,7 @@ let input_univ_names : universe_name_decl -> Libobject.obj = load_function = load_univ_names; open_function = open_univ_names; discharge_function = discharge_univ_names; - subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a); + 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 = @@ -540,12 +538,8 @@ let do_universe poly l = user_err ~hdr:"Constraint" (str"Cannot declare polymorphic universes outside sections") in - let l = - List.map (fun {CAst.v=id} -> - let lev = UnivGen.new_univ_id () in - (id, lev)) l - in - let ctx = List.fold_left (fun ctx (_,(dp,i)) -> Univ.LSet.add (Univ.Level.make dp i) ctx) + let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in + let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx) Univ.LSet.empty l, Univ.Constraint.empty in let () = declare_universe_context poly ctx in diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 931d05a975..554da7603f 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -18,6 +18,7 @@ val dump : unit -> bool val noglob : unit -> unit val dump_into_file : string -> unit (** special handling of "stdout" *) + val dump_to_dotglob : unit -> unit val feedback_glob : unit -> unit diff --git a/interp/impargs.ml b/interp/impargs.ml index d024a9e808..8a89bcdf26 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -448,7 +448,7 @@ let compute_mib_implicits flags kn = Array.to_list (Array.mapi (* No need to lift, arities contain no de Bruijn *) (fun i mip -> - (** No need to care about constraints here *) + (* No need to care about constraints here *) let ty, _ = Typeops.type_of_global_in_context env (IndRef (kn,i)) in Context.Rel.Declaration.LocalAssum (Name mip.mind_typename, ty)) mib.mind_packets) in diff --git a/interp/impargs.mli b/interp/impargs.mli index ea5aa90f68..4afc2af5e9 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -65,6 +65,7 @@ type implicit_explanation = operational only if [conclusion_matters] is true. *) type maximal_insertion = bool (** true = maximal contextual insertion *) + type force_inference = bool (** true = always infer, never turn into evar/subgoal *) type implicit_status = (Id.t * implicit_explanation * diff --git a/interp/notation.ml b/interp/notation.ml index 6a305c24af..c866929234 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -21,6 +21,7 @@ open Notation_term open Glob_term open Glob_ops open Context.Named.Declaration +open Classops (*i*) @@ -156,6 +157,8 @@ let scope_eq s1 s2 = match s1, s2 with | Scope _, SingleNotation _ | SingleNotation _, Scope _ -> false +(* Scopes for interpretation *) + let scope_stack = ref [] let current_scopes () = !scope_stack @@ -165,14 +168,91 @@ let scope_is_open_in_scopes sc l = let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack) +(* Uninterpretation tables *) + +type interp_rule = + | NotationRule of scope_name option * notation + | SynDefRule of KerName.t + +type scoped_notation_rule_core = scope_name * notation * interpretation * int option +type notation_rule_core = interp_rule * interpretation * int option +type notation_rule = notation_rule_core * delimiters option * bool + +(* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) + +type uninterp_scope_elem = + | UninterpScope of scope_name + | UninterpSingle of notation_rule_core + +let uninterp_scope_eq_weak s1 s2 = match s1, s2 with +| UninterpScope s1, UninterpScope s2 -> String.equal s1 s2 +| UninterpSingle s1, UninterpSingle s2 -> false +| (UninterpSingle _ | UninterpScope _), _ -> false + +module ScopeOrd = + struct + type t = scope_name option + let compare = Pervasives.compare + end + +module ScopeMap = CMap.Make(ScopeOrd) + +let uninterp_scope_stack = ref [] + +let push_uninterp_scope sc scopes = UninterpScope sc :: scopes + +let push_uninterp_scopes = List.fold_right push_uninterp_scope + +(**********************************************************************) +(* Mapping classes to scopes *) + +type scope_class = cl_typ + +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord + +let compute_scope_class sigma t = + let (cl,_,_) = find_class_type sigma t in + cl + +module ScopeClassOrd = +struct + type t = scope_class + let compare = scope_class_compare +end + +module ScopeClassMap = Map.Make(ScopeClassOrd) + +let initial_scope_class_map : scope_name ScopeClassMap.t = + ScopeClassMap.empty + +let scope_class_map = ref initial_scope_class_map + +let declare_scope_class sc cl = + scope_class_map := ScopeClassMap.add cl sc !scope_class_map + +let find_scope_class cl = + ScopeClassMap.find cl !scope_class_map + +let find_scope_class_opt = function + | None -> None + | Some cl -> try Some (find_scope_class cl) with Not_found -> None + +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + (* TODO: push nat_scope, z_scope, ... in scopes summary *) (* Exportation of scopes *) let open_scope i (_,(local,op,sc)) = - if Int.equal i 1 then + if Int.equal i 1 then begin scope_stack := - if op then sc :: !scope_stack - else List.except scope_eq sc !scope_stack + if op then Scope sc :: !scope_stack + else List.except scope_eq (Scope sc) !scope_stack; + uninterp_scope_stack := + if op then UninterpScope sc :: !uninterp_scope_stack + else List.except uninterp_scope_eq_weak (UninterpScope sc) !uninterp_scope_stack + end let cache_scope o = open_scope 1 o @@ -187,7 +267,7 @@ let discharge_scope (_,(local,_,_ as o)) = let classify_scope (local,_,_ as o) = if local then Dispose else Substitute o -let inScope : bool * bool * scope_elem -> obj = +let inScope : bool * bool * scope_name -> obj = declare_object {(default_object "SCOPE") with cache_function = cache_scope; open_function = open_scope; @@ -196,7 +276,7 @@ let inScope : bool * bool * scope_elem -> obj = classify_function = classify_scope } let open_close_scope (local,opening,sc) = - Lib.add_anonymous_leaf (inScope (local,opening,Scope (normalize_scope sc))) + Lib.add_anonymous_leaf (inScope (local,opening,normalize_scope sc)) let empty_scope_stack = [] @@ -204,9 +284,20 @@ let push_scope sc scopes = Scope sc :: scopes let push_scopes = List.fold_right push_scope +let make_type_scope_soft tmp_scope = + if Option.equal String.equal tmp_scope (current_type_scope_name ()) then + true, None + else + false, tmp_scope + let make_current_scopes (tmp_scope,scopes) = Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) +let make_current_uninterp_scopes (tmp_scope,scopes) = + let istyp,tmp_scope = make_type_scope_soft tmp_scope in + istyp,Option.fold_right push_uninterp_scope tmp_scope + (push_uninterp_scopes scopes !uninterp_scope_stack) + (**********************************************************************) (* Delimiters *) @@ -217,7 +308,7 @@ let declare_delimiters scope key = | None -> scope_map := String.Map.add scope newsc !scope_map | Some oldkey when String.equal oldkey key -> () | Some oldkey -> - (** FIXME: implement multikey scopes? *) + (* FIXME: implement multikey scopes? *) Flags.if_verbose Feedback.msg_info (str "Overwriting previous delimiting key " ++ str oldkey ++ str " in scope " ++ str scope); scope_map := String.Map.add scope newsc !scope_map @@ -250,40 +341,80 @@ let find_delimiters_scope ?loc key = user_err ?loc ~hdr:"find_delimiters" (str "Unknown scope delimiting key " ++ str key ++ str ".") -(* Uninterpretation tables *) - -type interp_rule = - | NotationRule of scope_name option * notation - | SynDefRule of KerName.t - (* We define keys for glob_constr and aconstr to split the syntax entries according to the key of the pattern (adapted from Chet Murthy by HH) *) type key = | RefKey of GlobRef.t + | LambdaKey + | ProdKey | Oth let key_compare k1 k2 = match k1, k2 with | RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2 -| RefKey _, Oth -> -1 -| Oth, RefKey _ -> 1 -| Oth, Oth -> 0 +| RefKey _, _ -> -1 +| _, RefKey _ -> 1 +| k1, k2 -> Pervasives.compare k1 k2 module KeyOrd = struct type t = key let compare = key_compare end module KeyMap = Map.Make(KeyOrd) -type notation_rule = interp_rule * interpretation * int option - -let keymap_add key interp map = - let old = try KeyMap.find key map with Not_found -> [] in - KeyMap.add key (interp :: old) map +let keymap_add key sc interp (scope_map,global_map) = + (* Adding to scope keymap for printing based on open scopes *) + let oldkeymap = try ScopeMap.find sc scope_map with Not_found -> KeyMap.empty in + let oldscmap = try KeyMap.find key oldkeymap with Not_found -> [] in + let newscmap = KeyMap.add key (interp :: oldscmap) oldkeymap in + let scope_map = ScopeMap.add sc newscmap scope_map in + (* Adding to global keymap of scoped notations in case the scope is not open *) + let global_map = match interp with + | NotationRule (Some sc,ntn), interp, c -> + let oldglobalkeymap = try KeyMap.find key global_map with Not_found -> [] in + KeyMap.add key ((sc,ntn,interp,c) :: oldglobalkeymap) global_map + | (NotationRule (None,_) | SynDefRule _), _, _ -> global_map in + (scope_map, global_map) + +let keymap_extract istype keys sc map = + let keymap = + try ScopeMap.find (Some sc) map + with Not_found -> KeyMap.empty in + let delim = + if istype && Option.equal String.equal (Some sc) (current_type_scope_name ()) then + (* A type is re-interpreted with type_scope on top, so never need a delimiter *) + None + else + (* Pass the delimiter so that it can be used if ever the notation is masked *) + (String.Map.find sc !scope_map).delimiters in + let add_scope rule = (rule,delim,false) in + List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys + +let find_with_delimiters istype = function + | None -> + None + | Some _ as scope when istype && Option.equal String.equal scope (current_type_scope_name ()) -> + (* This is in case type_scope (which by default is open in the + initial state) has been explicitly closed *) + Some None + | Some scope -> + match (String.Map.find scope !scope_map).delimiters with + | Some key -> Some (Some key) + | None -> None -let keymap_find key map = - try KeyMap.find key map - with Not_found -> [] +let rec keymap_extract_remainder istype scope_seen = function + | [] -> [] + | (sc,ntn,interp,c) :: l -> + if String.Set.mem sc scope_seen then keymap_extract_remainder istype scope_seen l + else + match find_with_delimiters istype (Some sc) with + | None -> keymap_extract_remainder istype scope_seen l + | Some delim -> + let rule = (NotationRule (Some sc, ntn), interp, c) in + (rule,delim,true) :: keymap_extract_remainder istype scope_seen l (* Scopes table : interpretation -> scope_name *) -let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) +let notations_key_table = + ref ((ScopeMap.empty, KeyMap.empty) : + notation_rule_core list KeyMap.t ScopeMap.t * + scoped_notation_rule_core list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -295,12 +426,14 @@ let glob_prim_constr_key c = match DAst.get c with | _ -> None let glob_constr_keys c = match DAst.get c with + | GRef (ref,_) -> [RefKey (canonical_gr ref)] | GApp (c, _) -> begin match DAst.get c with | GRef (ref, _) -> [RefKey (canonical_gr ref); Oth] | _ -> [Oth] end - | GRef (ref,_) -> [RefKey (canonical_gr ref)] + | GLambda _ -> [LambdaKey] + | GProd _ -> [ProdKey] | _ -> [Oth] let cases_pattern_key c = match DAst.get c with @@ -314,6 +447,8 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *) RefKey (canonical_gr ref), Some (List.length args) | NRef ref -> RefKey(canonical_gr ref), None | NApp (_,args) -> Oth, Some (List.length args) + | NLambda _ | NBinderList (_,_,NLambda _,_,_) | NList (_,_,NLambda _,_,_) -> LambdaKey, None + | NProd _ | NBinderList (_,_,NProd _,_,_) | NList (_,_,NProd _,_,_) -> ProdKey, None | _ -> Oth, None (**********************************************************************) @@ -956,37 +1091,31 @@ let check_required_module ?loc sc (sp,d) = (* Look if some notation or numeral printer in [scope] can be used in the scope stack [scopes], and if yes, using delimiters or not *) -let find_with_delimiters = function - | None -> None - | Some scope -> - match (String.Map.find scope !scope_map).delimiters with - | Some key -> Some (Some scope, Some key) - | None -> None - -let rec find_without_delimiters find (ntn_scope,ntn) = function - | Scope scope :: scopes -> +let rec find_without_delimiters find (istype,ntn_scope,ntn as ntndata) = function + | UninterpScope scope :: scopes -> (* Is the expected ntn/numpr attached to the most recently open scope? *) begin match ntn_scope with | Some scope' when String.equal scope scope' -> - Some (None,None) + Some None | _ -> (* If the most recently open scope has a notation/numeral printer but not the expected one then we need delimiters *) if find scope then - find_with_delimiters ntn_scope + find_with_delimiters istype ntn_scope else - find_without_delimiters find (ntn_scope,ntn) scopes + find_without_delimiters find ntndata scopes end - | SingleNotation ntn' :: scopes -> + | UninterpSingle (NotationRule (_,ntn'),_,_) :: scopes -> begin match ntn_scope, ntn with | None, Some ntn when notation_eq ntn ntn' -> - Some (None, None) + Some None | _ -> - find_without_delimiters find (ntn_scope,ntn) scopes + find_without_delimiters find ntndata scopes end + | UninterpSingle (SynDefRule _,_,_) :: scopes -> find_without_delimiters find ntndata scopes | [] -> (* Can we switch to [scope]? Yes if it has defined delimiters *) - find_with_delimiters ntn_scope + find_with_delimiters istype ntn_scope (* The mapping between notations and their interpretation *) @@ -1019,9 +1148,19 @@ let declare_notation_interpretation ntn scopt pat df ~onlyprint = | Some _ -> () end +let scope_of_rule = function + | NotationRule (None,_) | SynDefRule _ -> None + | NotationRule (Some sc as sco,_) -> sco + +let uninterp_scope_to_add pat n = function + | NotationRule (None,_) | SynDefRule _ as rule -> Some (UninterpSingle (rule,pat,n)) + | NotationRule (Some sc,_) -> None + let declare_uninterpretation rule (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_add key (rule,pat,n) !notations_key_table + let sc = scope_of_rule rule in + notations_key_table := keymap_add key sc (rule,pat,n) !notations_key_table; + uninterp_scope_stack := Option.List.cons (uninterp_scope_to_add pat n rule) !uninterp_scope_stack let rec find_interpretation ntn find = function | [] -> raise Not_found @@ -1100,20 +1239,29 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) +let extract_notations (istype,scopes) keys = + if keys == [] then [] (* shortcut *) else + let scope_map, global_map = !notations_key_table in + let rec aux scopes seen = + match scopes with + | UninterpScope sc :: scopes -> keymap_extract istype keys sc scope_map @ aux scopes (String.Set.add sc seen) + | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes seen + | [] -> + let find key = try KeyMap.find key global_map with Not_found -> [] in + keymap_extract_remainder istype seen (List.flatten (List.map find keys)) + in aux scopes String.Set.empty -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table +let uninterp_notations scopes c = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes (glob_constr_keys c) -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes [cases_pattern_key c] -let availability_of_notation (ntn_scope,ntn) scopes = - let f scope = - NotationMap.mem ntn (String.Map.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes) +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_uninterp_scopes scopes in + extract_notations scopes [RefKey (canonical_gr (IndRef ind))] (* We support coercions from a custom entry at some level to an entry at some level (possibly the same), and from and to the constr entry. E.g.: @@ -1270,13 +1418,11 @@ let availability_of_prim_token n printer_scope local_scopes = | _ -> false with Not_found -> false in - let scopes = make_current_scopes local_scopes in - Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) + let istype,scopes = make_current_uninterp_scopes local_scopes in + find_without_delimiters f (istype,Some printer_scope,None) scopes (* Miscellaneous *) -let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 - let notation_binder_source_eq s1 s2 = match s1, s2 with | NtnParsedAsIdent, NtnParsedAsIdent -> true | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2 @@ -1290,9 +1436,10 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeBinder _ | NtnTypeConstrList | NtnTypeBinderList), _ -> false -let var_attributes_eq (_, ((entry1, sc1), tp1)) (_, ((entry2, sc2), tp2)) = +let var_attributes_eq (_, ((entry1, (tmpsc1, scl1)), tp1)) (_, ((entry2, (tmpsc2, scl2)), tp2)) = notation_entry_level_eq entry1 entry2 && - pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && + Option.equal String.equal tmpsc1 tmpsc2 && + List.equal String.equal scl1 scl2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = @@ -1307,44 +1454,15 @@ let exists_notation_in_scope scopt ntn onlyprint r = interpretation_eq n.not_interp r with Not_found -> false -let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false - -(**********************************************************************) -(* Mapping classes to scopes *) - -open Classops - -type scope_class = cl_typ - -let scope_class_compare : scope_class -> scope_class -> int = - cl_typ_ord - -let compute_scope_class sigma t = - let (cl,_,_) = find_class_type sigma t in - cl - -module ScopeClassOrd = -struct - type t = scope_class - let compare = scope_class_compare -end - -module ScopeClassMap = Map.Make(ScopeClassOrd) - -let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.empty - -let scope_class_map = ref initial_scope_class_map - -let declare_scope_class sc cl = - scope_class_map := ScopeClassMap.add cl sc !scope_class_map - -let find_scope_class cl = - ScopeClassMap.find cl !scope_class_map +let exists_notation_interpretation_in_scope scopt ntn = + let scope = match scopt with Some s -> s | None -> default_scope in + try + let sc = String.Map.find scope !scope_map in + let _ = NotationMap.find ntn sc.notations in + true + with Not_found -> false -let find_scope_class_opt = function - | None -> None - | Some cl -> try Some (find_scope_class cl) with Not_found -> None +let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Special scopes associated to arguments of a global reference *) @@ -1366,9 +1484,6 @@ let compute_arguments_scope sigma t = fst (compute_arguments_scope_full sigma t) let compute_type_scope sigma t = find_scope_class_opt (try Some (compute_scope_class sigma t) with Not_found -> None) -let current_type_scope_name () = - find_scope_class_opt (Some CL_SORT) - let scope_class_of_class (x : cl_typ) : scope_class = x @@ -1725,7 +1840,7 @@ let locate_notation prglob ntn scope = str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in - prlist + prlist_with_sep fnl (fun (sc,r,(_,df)) -> hov 0 ( pr_notation_info prglob df r ++ @@ -1788,17 +1903,18 @@ let pr_visibility prglob = function (* Synchronisation with reset *) let freeze _ = - (!scope_map, !scope_stack, !arguments_scope, + (!scope_map, !scope_stack, !uninterp_scope_stack, !arguments_scope, !delimiters_map, !notations_key_table, !scope_class_map, !prim_token_interp_infos, !prim_token_uninterp_infos, !entry_coercion_map, !entry_has_global_map, !entry_has_ident_map) -let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = +let unfreeze (scm,scs,uscs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = scope_map := scm; scope_stack := scs; - delimiters_map := dlm; + uninterp_scope_stack := uscs; arguments_scope := asc; + delimiters_map := dlm; notations_key_table := fkm; scope_class_map := clsc; prim_token_interp_infos := ptii; @@ -1809,8 +1925,9 @@ let unfreeze (scm,scs,asc,dlm,fkm,clsc,ptii,ptui,coe,globs,ids) = let init () = init_scope_map (); + uninterp_scope_stack := []; delimiters_map := String.Map.empty; - notations_key_table := KeyMap.empty; + notations_key_table := (ScopeMap.empty,KeyMap.empty); scope_class_map := initial_scope_class_map; prim_token_interp_infos := String.Map.empty; prim_token_uninterp_infos := GlobRef.Map.empty diff --git a/interp/notation.mli b/interp/notation.mli index c0ff1a1ac3..75034cad70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -54,7 +54,7 @@ val scope_is_open : scope_name -> bool (** Open scope *) val open_close_scope : - (** locality *) bool * (* open *) bool * scope_name -> unit + (* locality *) bool * (* open *) bool * scope_name -> unit (** Extend a list of scopes *) val empty_scope_stack : scopes @@ -219,18 +219,28 @@ val declare_uninterpretation : interp_rule -> interpretation -> unit val interp_notation : ?loc:Loc.t -> notation -> subscopes -> interpretation * (notation_location * scope_name option) -type notation_rule = interp_rule * interpretation * int option +type notation_rule_core = + interp_rule (* kind of notation *) + * interpretation (* pattern associated to the notation *) + * int option (* number of expected arguments *) + +type notation_rule = + notation_rule_core + * delimiters option (* delimiter to possibly add *) + * bool (* true if the delimiter is mandatory *) (** 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 : subscopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list +(* (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first argument is itself not None if a delimiters is needed *) val availability_of_notation : scope_name option * notation -> subscopes -> (scope_name option * delimiters option) option + *) (** {6 Miscellaneous} *) @@ -241,6 +251,9 @@ val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) -> val exists_notation_in_scope : scope_name option -> notation -> bool -> interpretation -> bool +(** Checks for already existing notations *) +val exists_notation_interpretation_in_scope : scope_name option -> notation -> bool + (** Declares and looks for scopes associated to arguments of a global ref *) val declare_arguments_scope : bool (** true=local *) -> GlobRef.t -> scope_name option list -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7a525f84a5..8d225fe683 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -37,7 +37,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | _ -> false) | NApp (t1, a1), NApp (t2, a2) -> (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 -| NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) +| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *) | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 && b1 == b2 @@ -51,7 +51,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> Name.equal na1 na2 && eq_notation_constr vars b1 b2 && Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) +| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && (eq_notation_constr vars) t1 t2 @@ -75,7 +75,7 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Option.equal (eq_notation_constr vars) o1 o2 && (eq_notation_constr vars) u1 u2 && (eq_notation_constr vars) r1 r2 -| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) +| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *) let eq (na1, o1, t1) (na2, o2, t2) = Name.equal na1 na2 && Option.equal (eq_notation_constr vars) o1 o2 && @@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw = match raw with | NRef ref -> let ref',t = subst_global subst ref in - if ref' == ref then raw else - fst (notation_constr_of_constr bound t) + if ref' == ref then raw else (match t with + | None -> NRef ref' + | Some t -> + fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value)) | NVar _ -> raw diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 5fb0ca1b43..0ef1f267f6 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -20,13 +20,13 @@ open Glob_term as well as non global expressions such as existential variables. *) type notation_constr = - (** Part common to [glob_constr] and [cases_pattern] *) + (* Part common to [glob_constr] and [cases_pattern] *) | NRef of GlobRef.t | NVar of Id.t | NApp of notation_constr * notation_constr list | NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool - (** Part only in [glob_constr] *) + (* Part only in [glob_constr] *) | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool |