diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrexpr_ops.ml | 16 | ||||
| -rw-r--r-- | interp/constrintern.ml | 153 | ||||
| -rw-r--r-- | interp/constrintern.mli | 13 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 10 | ||||
| -rw-r--r-- | interp/notation_term.ml | 3 | ||||
| -rw-r--r-- | interp/smartlocate.ml | 8 | ||||
| -rw-r--r-- | interp/smartlocate.mli | 5 |
7 files changed, 119 insertions, 89 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index f02874253e..ddd689bee0 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -261,11 +261,9 @@ and cast_expr_eq c1 c2 = match c1, c2 with | CastConv t1, CastConv t2 | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> constr_expr_eq t1 t2 -| CastCoerce, CastCoerce -> true | CastConv _, _ | CastVM _, _ -| CastNative _, _ -| CastCoerce, _ -> false +| CastNative _, _ -> false let constr_loc c = CAst.(c.loc) let cases_pattern_expr_loc cp = CAst.(cp.loc) @@ -283,10 +281,13 @@ let local_binders_loc bll = match bll with (** Folds and maps *) let is_constructor id = - try Globnames.isConstructRef - (Smartlocate.global_of_extended_global - (Nametab.locate_extended (qualid_of_ident id))) - with Not_found -> false + match + Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id)) + with + | exception Not_found -> false + | None -> false + | Some gref -> Globnames.isConstructRef gref let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with | CPatRecord l -> @@ -343,7 +344,6 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CLetIn (na,a,t,b) -> f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b - | CCast (a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bl,bll)) -> (* The following is an approximation: we don't know exactly if an ident is binding nor to which subterms bindings apply *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 958e1408f8..68dd96e44b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -273,40 +273,54 @@ let make_current_scope tmp scopes = match tmp, scopes with | Some tmp_scope, scopes -> tmp_scope :: scopes | None, scopes -> scopes -let pr_scope_stack = function - | [] -> str "the empty scope stack" - | [a] -> str "scope " ++ str a - | l -> str "scope stack " ++ +let pr_scope_stack begin_of_sentence l = + let bstr x = + if begin_of_sentence then str (CString.capitalize_ascii x) else str x in + match l with + | [] -> bstr "the empty scope stack" + | [a] -> bstr "scope " ++ str a + | l -> bstr "scope stack " ++ str "[" ++ prlist_with_sep pr_comma str l ++ str "]" -let error_inconsistent_scope ?loc id scopes1 scopes2 = - user_err ?loc ~hdr:"set_var_scope" - (Id.print id ++ str " is here used in " ++ - pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ - pr_scope_stack scopes1) +let warn_inconsistent_scope = + CWarnings.create ~name:"inconsistent-scopes" ~category:"syntax" + (fun (id,scopes1,scopes2) -> + (str "Argument " ++ Id.print id ++ + strbrk " was previously inferred to be in " ++ + pr_scope_stack false scopes1 ++ + strbrk " but is here used in " ++ + pr_scope_stack false scopes2 ++ + strbrk ". " ++ + pr_scope_stack true scopes1 ++ + strbrk " will be used at parsing time unless you override it by" ++ + strbrk " annotating the argument with an explicit scope of choice.")) let error_expect_binder_notation_type ?loc id = user_err ?loc (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") -let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars = +let set_notation_var_scope ?loc id (tmp_scope,subscopes as scopes) ntnvars = try - let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in - if istermvar then begin - (* scopes have no effect on the interpretation of identifiers *) - (match !idscopes with + let _,idscopes,typ = Id.Map.find id ntnvars in + match typ with + | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id + | Notation_term.NtnInternTypeAny principal -> + match !idscopes with | None -> idscopes := Some scopes | Some (tmp_scope', subscopes') -> let s' = make_current_scope tmp_scope' subscopes' in let s = make_current_scope tmp_scope subscopes in - if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s); - (match typ with - | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id - | Notation_term.NtnInternTypeAny -> ()) - end - else - used_as_binder := true + if Option.is_empty principal && not (List.equal String.equal s' s) then + warn_inconsistent_scope ?loc (id,s',s) + with Not_found -> + (* Not in a notation *) + () + +let set_var_is_binder ?loc id ntnvars = + try + let used_as_binder,_,_ = Id.Map.find id ntnvars in + used_as_binder := true with Not_found -> (* Not in a notation *) () @@ -484,7 +498,7 @@ let push_name_env ntnvars implargs env = | { loc; v = Name id } -> if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; - set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars; + set_var_is_binder ?loc id ntnvars; let uid = var_uid id in Dumpglob.dump_binding ?loc uid; pure_push_name_env (id,(Variable,implargs,[],uid)) env @@ -1064,7 +1078,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = (* Is [id] a notation variable *) if Id.Map.mem id ntnvars then begin - if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars; + if not (Id.Map.mem id env.impls) then set_notation_var_scope ?loc id (env.tmp_scope,env.scopes) ntnvars; gvar (loc,id) us end else @@ -1130,14 +1144,54 @@ let intern_reference qid = in Smartlocate.global_of_extended_global r +let intern_sort_name ~local_univs = function + | CSProp -> GSProp + | CProp -> GProp + | CSet -> GSet + | CRawType u -> GRawUniv u + | CType qid -> + let is_id = qualid_is_ident qid in + let local = if not is_id then None + else Id.Map.find_opt (qualid_basename qid) local_univs.bound + in + match local with + | Some u -> GUniv u + | None -> + try GUniv (Univ.Level.make (Nametab.locate_universe qid)) + with Not_found -> + if is_id && local_univs.unb_univs + then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) + else + CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") + +let intern_sort ~local_univs s = + map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s + +let intern_instance ~local_univs us = + Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us + +let intern_name_alias = function + | { CAst.v = CRef(qid,u) } -> + let r = + try Some (intern_extended_global_of_qualid qid) + with Not_found -> None + in + Option.bind r Smartlocate.global_of_extended_global |> + Option.map (fun r -> r, intern_instance ~local_univs:empty_local_univs u) + | _ -> None + let intern_projection qid = - try - match Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) with - | GlobRef.ConstRef c as gr -> - (gr, Structure.find_from_projection c) - | _ -> raise Not_found - with Not_found -> - Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + match + Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) |> + Option.map (function + | GlobRef.ConstRef c as x -> x, Structure.find_from_projection c + | _ -> raise Not_found) + with + | exception Not_found -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | None -> + Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid)) + | Some x -> x (**********************************************************************) (* Interpreting references *) @@ -1182,37 +1236,6 @@ let glob_sort_of_level (level: glob_level) : glob_sort = | UAnonymous {rigid} -> UAnonymous {rigid} | UNamed id -> UNamed [id,0] -let intern_sort_name ~local_univs = function - | CSProp -> GSProp - | CProp -> GProp - | CSet -> GSet - | CRawType u -> GRawUniv u - | CType qid -> - let is_id = qualid_is_ident qid in - let local = if not is_id then None - else Id.Map.find_opt (qualid_basename qid) local_univs.bound - in - match local with - | Some u -> GUniv u - | None -> - try GUniv (Univ.Level.make (Nametab.locate_universe qid)) - with Not_found -> - if is_id && local_univs.unb_univs - then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid)) - else - CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".") - -let intern_sort ~local_univs s = - map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s - -let intern_instance ~local_univs us = - Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us - -let try_interp_name_alias = function - | [], { CAst.v = CRef (ref,u) } -> - NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u) - | _ -> raise Not_found - (* Is it a global reference or a syntactic definition? *) let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let loc = qid.loc in @@ -1843,7 +1866,7 @@ let rec intern_pat genv ntnvars aliases pat = intern_cstr_with_all_args loc c true [] pl | RCPatAtom (Some ({loc;v=id},scopes)) -> let aliases = merge_aliases aliases (make ?loc @@ Name id) in - set_var_scope ?loc id false scopes ntnvars; + set_var_is_binder ?loc id ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom None -> let { alias_ids = ids; alias_map = asubst; } = aliases in @@ -2561,7 +2584,11 @@ let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (function + | (NtnInternTypeAny None | NtnInternTypeOnlyBinder) as typ -> (ref false, ref None, typ) + | NtnInternTypeAny (Some scope) as typ -> + (ref false, ref (Some (Some scope,[])), typ) + ) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in let c = internalize env {ids; unb = false; diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 65b63962d0..379bd61070 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -147,12 +147,13 @@ val interp_constr_pattern : env -> evar_map -> ?expected_type:typing_constraint -> constr_pattern_expr -> constr_pattern -(** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : qualid -> GlobRef.t +(** Returns None if it's a syndef not bound to a name, raises an error + if not existing *) +val intern_reference : qualid -> GlobRef.t option -(** For syntactic definitions: check if abbreviation to a name - and avoid early insertion of maximal implicit arguments *) -val try_interp_name_alias : 'a list * constr_expr -> notation_constr +(** Returns None if not a reference or a syndef not bound to a name *) +val intern_name_alias : + constr_expr -> (GlobRef.t * Glob_term.glob_level list option) option (** Expands abbreviations (syndef); raise an error if not existing *) val interp_reference : ltac_sign -> qualid -> glob_constr @@ -174,7 +175,7 @@ val interp_context_evars : (** Locating references of constructions, possibly via a syntactic definition (these functions do not modify the glob file) *) -val locate_reference : Libnames.qualid -> GlobRef.t +val locate_reference : Libnames.qualid -> GlobRef.t option val is_global : Id.t -> bool (** Interprets a term as the left-hand side of a notation. The returned map is diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ea5e2a1ad4..313a9e85a4 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -35,9 +35,8 @@ let rec alpha_var id1 id2 = function let cast_type_iter2 f t1 t2 = match t1, t2 with | CastConv t1, CastConv t2 -> f t1 t2 | CastVM t1, CastVM t2 -> f t1 t2 - | CastCoerce, CastCoerce -> () | CastNative t1, CastNative t2 -> f t1 t2 - | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit + | (CastConv _ | CastVM _ | CastNative _), _ -> raise Exit (* used to update the notation variable with the local variables used in NList and NBinderList, since the iterator has its own variable *) @@ -681,7 +680,7 @@ let check_variables_and_reversibility nenv str " position as part of a recursive pattern.") in let check_type x typ = match typ with - | NtnInternTypeAny -> + | NtnInternTypeAny _ -> begin try check_pair "term" x (Id.Map.find x recvars) foundrec with Not_found -> check_bound x @@ -1319,12 +1318,9 @@ let match_cast match_fun sigma c1 c2 = | CastVM t1, CastVM t2 | CastNative t1, CastNative t2 -> match_fun sigma t1 t2 - | CastCoerce, CastCoerce -> - sigma | CastConv _, _ | CastVM _, _ - | CastNative _, _ - | CastCoerce, _ -> raise No_match + | CastNative _, _ -> raise No_match let does_not_come_from_already_eta_expanded_var glob = (* This is hack to avoid looping on a rule with rhs of the form *) diff --git a/interp/notation_term.ml b/interp/notation_term.ml index 2979447cf8..ec7165f854 100644 --- a/interp/notation_term.ml +++ b/interp/notation_term.ml @@ -91,7 +91,8 @@ type notation_var_instance_type = in a recursive pattern x..y, both x and y carry the individual type of each element of the list x..y *) type notation_var_internalization_type = - | NtnInternTypeAny | NtnInternTypeOnlyBinder + | NtnInternTypeAny of scope_name option + | NtnInternTypeOnlyBinder (** This characterizes to what a notation is interpreted to *) type interpretation = diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 91d05f7317..56b3cd9815 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -33,7 +33,7 @@ let global_of_extended_global_head = function | _ -> raise Not_found in head_of syn_def -let global_of_extended_global = function +let global_of_extended_global_exn = function | TrueGlobal ref -> ref | SynDef kn -> match search_syntactic_definition kn with @@ -45,11 +45,15 @@ let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref - else global_of_extended_global ref + else global_of_extended_global_exn ref with Not_found -> user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") +let global_of_extended_global x = + try Some (global_of_extended_global_exn x) + with Not_found -> None + let global_constant_with_alias qid = try match locate_global_with_alias qid with | Names.GlobRef.ConstRef c -> c diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 26f2a4f36d..abf9839c9e 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -19,8 +19,9 @@ open Globnames val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t -(** Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> GlobRef.t +(** Extract a global_reference from a reference that can be an "alias". + If the reference points to a more complex term, we return None *) +val global_of_extended_global : extended_global_reference -> GlobRef.t option (** Locate a reference taking into account possible "alias" notations. May raise [Nametab.GlobalizationError _] for an unknown reference, |