diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 195 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 2 |
2 files changed, 115 insertions, 82 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5fb6664dd6..a3dd686121 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -420,6 +420,40 @@ let binder_status_fun = { slide = on_snd slide_binders; } +(* [test_kind_strict] rules out pattern which refers to global other + than constructors or variables; It is used in instances of notations *) + +let test_kind_pattern_in_notation ?loc = function + | GlobRef.ConstructRef _ -> () + (* We do not accept non constructors to be used as variables in + patterns *) + | GlobRef.ConstRef _ -> + user_err ?loc (str "Found a constant while a pattern was expected.") + | GlobRef.IndRef _ -> + user_err ?loc (str "Found an inductive type while a pattern was expected.") + | GlobRef.VarRef _ -> + (* we accept a section variable name to be used as pattern variable *) + raise Not_found + +let test_kind_ident_in_notation ?loc = function + | GlobRef.ConstructRef _ -> + user_err ?loc (str "Found a constructor while a variable name was expected.") + | GlobRef.ConstRef _ -> + user_err ?loc (str "Found a constant while a variable name was expected.") + | GlobRef.IndRef _ -> + user_err ?loc (str "Found an inductive type while a variable name was expected.") + | GlobRef.VarRef _ -> + (* we accept a section variable name to be used as pattern variable *) + raise Not_found + +(* [test_kind_tolerant] allow global reference names to be used as pattern variables *) + +let test_kind_tolerant ?loc = function + | GlobRef.ConstructRef _ -> () + | GlobRef.ConstRef _ | GlobRef.IndRef _ | GlobRef.VarRef _ -> + (* A non-constructor global reference in a pattern is seen as a variable *) + raise Not_found + (**) let locate_if_hole ?loc na c = match DAst.get c with @@ -539,9 +573,9 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = (push_name_env ntnvars impls env locna, (na,Explicit,term,ty)) -let intern_cases_pattern_as_binder ?loc ntnvars env p = +let intern_cases_pattern_as_binder ?loc test_kind ntnvars env p = let il,disjpat = - let (il, subst_disjpat) = !intern_cases_pattern_fwd ntnvars (None,env.scopes) p in + let (il, subst_disjpat) = !intern_cases_pattern_fwd test_kind ntnvars (None,env.scopes) p in let substl,disjpat = List.split subst_disjpat in if not (List.for_all (fun subst -> Id.Map.equal Id.equal subst Id.Map.empty) substl) then user_err ?loc (str "Unsupported nested \"as\" clause."); @@ -568,7 +602,7 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function | Some ty -> ty | None -> CAst.make ?loc @@ CHole(None,IntroAnonymous,None) in - let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in + let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc test_kind_tolerant ntnvars env p in let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in let {v=(_,bk,t)} = List.hd bl' in @@ -661,27 +695,21 @@ let is_patvar_store store pat = | PatVar na -> ignore(store na); true | _ -> false -let out_patvar pat = - match pat.v with +let out_patvar = CAst.map_with_loc (fun ?loc -> function | CPatAtom (Some qid) when qualid_is_ident qid -> Name (qualid_basename qid) | CPatAtom None -> Anonymous - | _ -> assert false - -let term_of_name = function - | Name id -> DAst.make (GVar id) - | Anonymous -> - let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in - DAst.make (GHole (Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=st }, IntroAnonymous, None)) + | _ -> assert false) let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function | Anonymous -> (renaming,env), None, Anonymous | Name id -> let store,get = set_temporary_memory () in + let test_kind = test_kind_tolerant in try (* We instantiate binder name with patterns which may be parsed as terms *) let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in let pat, na = match disjpat with | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in @@ -694,11 +722,11 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_patvar pat in - let env = push_name_env ntnvars [] env (make ?loc:pat.loc na) in - (renaming,env), None, na + let env = push_name_env ntnvars [] env na in + (renaming,env), None, na.v else (* Interpret as a pattern *) - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in + let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars env pat in let pat, na = match disjpat with | [pat] when is_patvar_store store pat -> let na = get () in None, na @@ -829,22 +857,22 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env id (c, (tmp_scope, subscopes)) map = - let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in + let mk_env id (c, scopes) map = + let nenv = set_env_scopes env scopes in try let gc = intern nenv c in Id.Map.add id (gc, None) map with Nametab.GlobalizationError _ -> map in - let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = - let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - if onlyident then - let na = out_patvar c in term_of_name na, None - else - let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in - match disjpat with - | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) - | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () + let mk_env' (c, (onlyident,scopes)) = + let nenv = set_env_scopes env scopes in + let test_kind = + if onlyident then test_kind_ident_in_notation + else test_kind_pattern_in_notation in + let _,((disjpat,_),_),_ = intern_pat test_kind ntnvars nenv c in + match disjpat with + | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None) + | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in @@ -890,20 +918,19 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try - let (a,(scopt,subscopes)) = Id.Map.find id terms in - intern {env with tmp_scope = scopt; - scopes = subscopes @ env.scopes} a + let (a,scopes) = Id.Map.find id terms in + intern (set_env_scopes env scopes) a with Not_found -> try let pat,(onlyident,scopes) = Id.Map.find id binders in - let env = set_env_scopes env scopes in - if onlyident then - term_of_name (out_patvar pat) - else - let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in - match disjpat with - | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat - | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") + let nenv = set_env_scopes env scopes in + let test_kind = + if onlyident then test_kind_ident_in_notation + else test_kind_pattern_in_notation in + let env,((disjpat,ids),id),na = intern_pat test_kind ntnvars nenv pat in + match disjpat with + | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat + | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.") with Not_found -> try match binderopt with @@ -1582,19 +1609,14 @@ let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref ~key:["Asymmetric";"Patterns"] ~value:false -let drop_notations_pattern looked_for genv = +let drop_notations_pattern (test_kind_top,test_kind_inner) genv = (* At toplevel, Constructors and Inductives are accepted, in recursive calls only constructor are allowed *) - let ensure_kind top loc g = - try - if top then looked_for g else - match g with GlobRef.ConstructRef _ -> () | _ -> raise Not_found + let ensure_kind test_kind ?loc g = + try test_kind ?loc g with Not_found -> error_invalid_pattern_notation ?loc () in - let test_kind top = - if top then looked_for else function GlobRef.ConstructRef _ -> () | _ -> raise Not_found - in (* [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)) @@ -1611,7 +1633,7 @@ let drop_notations_pattern looked_for genv = end | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in - let rec drop_syndef top scopes qid pats = + let rec drop_syndef test_kind ?loc scopes qid pats = try match Nametab.locate_extended qid with | SynDef sp -> @@ -1619,39 +1641,39 @@ let drop_notations_pattern looked_for genv = try match a with | NRef g -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) - test_kind top g; + test_kind ?loc g; let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc scopes) argscs pats) | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *) - test_kind top g; + test_kind ?loc g; let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, List.map2 (in_pat_sc scopes) argscs pats, []) | NApp (NRef g,args) -> (* Convention: do not deactivate implicit arguments and scopes for further arguments *) - test_kind top g; + test_kind ?loc g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc; let pats1,pats2 = List.chop nvars pats in let subst = split_by_type_pat vars (pats1,[]) in - let idspl1 = List.map (in_not false qid.loc scopes subst []) args in + let idspl1 = List.map (in_not test_kind_inner qid.loc scopes subst []) args in let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2) | _ -> raise Not_found with Not_found -> None in Syntax_def.search_filtered_syntactic_definition filter sp | TrueGlobal g -> - test_kind top g; + test_kind ?loc g; Dumpglob.add_glob ?loc:qid.loc g; let (_,argscs) = find_remaining_scopes [] pats g in Some (g,[],List.map2 (in_pat_sc scopes) argscs pats) with Not_found -> None - and in_pat top scopes pt = + and in_pat test_kind scopes pt = let open CAst in let loc = pt.loc in match pt.v with - | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id) + | CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id) | CPatRecord l -> let sorted_fields = sort_fields ~complete:false loc l (fun _idx fieldname constructor -> CAst.make ?loc @@ CPatAtom None) in @@ -1668,7 +1690,7 @@ let drop_notations_pattern looked_for genv = end | CPatCstr (head, None, pl) -> begin - match drop_syndef top scopes head pl with + match drop_syndef test_kind ?loc scopes head pl with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head)) end @@ -1682,37 +1704,37 @@ let drop_notations_pattern looked_for genv = in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) - DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) + DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat test_kind_inner scopes) pl, []) else (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) (* but not scopes in expl_pl *) let (argscs1,_) = find_remaining_scopes expl_pl pl g in - DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, []) + DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, []) | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a -> let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Number (SMinus,p)) scopes in + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in rcp_of_glob scopes pat | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) -> - in_pat top scopes a + in_pat test_kind scopes a | CPatNotation (_,ntn,fullargs,extrargs) -> let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df; - in_not top loc scopes (terms,termlists) extrargs c + in_not test_kind loc scopes (terms,termlists) extrargs c | CPatDelimiters (key, e) -> - in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e + in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e | CPatPrim p -> - let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in + let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in rcp_of_glob scopes pat | CPatAtom (Some id) -> begin - match drop_syndef top scopes id [] with + match drop_syndef test_kind ?loc scopes id [] with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None - | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) + | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat test_kind scopes) pl) | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns @@ -1725,8 +1747,8 @@ let drop_notations_pattern looked_for genv = This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.") - and in_pat_sc scopes x = in_pat false (x,snd scopes) - and in_not top loc scopes (subst,substlist as fullsubst) args = function + and in_pat_sc scopes x = in_pat test_kind_inner (x,snd scopes) + and in_not (test_kind:?loc:Loc.t->'a->'b) loc scopes (subst,substlist as fullsubst) args = function | NVar id -> let () = assert (List.is_empty args) in begin @@ -1734,21 +1756,21 @@ let drop_notations_pattern looked_for genv = (* of the notations *) try let (a,(scopt,subscopes)) = Id.Map.find id subst in - in_pat top (scopt,subscopes@snd scopes) a + in_pat test_kind (scopt,subscopes@snd scopes) a with Not_found -> if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> - ensure_kind top loc g; + ensure_kind test_kind ?loc g; let (_,argscs) = find_remaining_scopes [] args g in DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args) | NApp (NRef g,pl) -> - ensure_kind top loc g; + ensure_kind test_kind ?loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in - let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in + let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in let pl = add_local_defs_and_check_length loc genv g pl args in - let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in + let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in let pat = if List.length pl = 0 then (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then @@ -1763,10 +1785,10 @@ let drop_notations_pattern looked_for genv = (try (* All elements of the list are in scopes (scopt,subscopes) *) let (l,(scopt,subscopes)) = Id.Map.find x substlist in - let termin = in_not top loc scopes fullsubst [] terminator in + let termin = in_not test_kind_inner loc scopes fullsubst [] terminator in List.fold_right (fun a t -> let nsubst = Id.Map.add y (a, (scopt, subscopes)) subst in - let u = in_not false loc scopes (nsubst, substlist) [] iter in + let u = in_not test_kind_inner loc scopes (nsubst, substlist) [] iter in subst_pat_iterator ldots_var t u) (if revert then List.rev l else l) termin with Not_found -> @@ -1775,7 +1797,7 @@ let drop_notations_pattern looked_for genv = let () = assert (List.is_empty args) in DAst.make ?loc @@ RCPatAtom None | t -> error_invalid_pattern_notation ?loc () - in in_pat true + in in_pat test_kind_top let rec intern_pat genv ntnvars aliases pat = let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 = @@ -1816,19 +1838,30 @@ let rec intern_pat genv ntnvars aliases pat = check_or_pat_variables loc ids (List.tl idsl); (ids,List.flatten pl') -let intern_cases_pattern genv ntnvars scopes aliases pat = +let intern_cases_pattern test_kind genv ntnvars scopes aliases pat = intern_pat genv ntnvars aliases - (drop_notations_pattern (function GlobRef.ConstructRef _ -> () | _ -> raise Not_found) genv scopes pat) + (drop_notations_pattern (test_kind,test_kind) genv scopes pat) let _ = intern_cases_pattern_fwd := - fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p + fun test_kind ntnvars scopes p -> + intern_cases_pattern test_kind (Global.env ()) ntnvars scopes empty_alias p let intern_ind_pattern genv ntnvars scopes pat = + let test_kind_top ?loc = function + | GlobRef.IndRef _ -> () + | GlobRef.ConstructRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ -> + (* A non-inductive global reference at top is an error *) + error_invalid_pattern_notation ?loc () in + let test_kind_inner ?loc = function + | GlobRef.ConstructRef _ -> () + | GlobRef.IndRef _ | GlobRef.ConstRef _ | GlobRef.VarRef _ -> + (* A non-constructor global reference deep in a pattern is seen as a variable *) + raise Not_found in let no_not = try - drop_notations_pattern (function (GlobRef.IndRef _ | GlobRef.ConstructRef _) -> () | _ -> raise Not_found) genv scopes pat - with InternalizationError(NotAConstructor _) as exn -> + drop_notations_pattern (test_kind_top,test_kind_inner) genv scopes pat + with InternalizationError (NotAConstructor _) as exn -> let _, info = Exninfo.capture exn in error_bad_inductive_type ~info () in @@ -2221,7 +2254,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* Expands a multiple pattern into a disjunction of multiple patterns *) and intern_multiple_pattern env n pl = - let idsl_pll = List.map (intern_cases_pattern globalenv ntnvars (None,env.scopes) empty_alias) pl in + let idsl_pll = List.map (intern_cases_pattern test_kind_tolerant globalenv ntnvars (None,env.scopes) empty_alias) pl in let loc = loc_of_multiple_pattern pl in check_number_of_pattern loc n pl; product_of_cases_patterns empty_alias idsl_pll @@ -2403,7 +2436,7 @@ let intern_gen kind env sigma let intern_constr env sigma c = intern_gen WithoutTypeConstraint env sigma c let intern_type env sigma c = intern_gen IsType env sigma c let intern_pattern globalenv patt = - intern_cases_pattern globalenv Id.Map.empty (None,[]) empty_alias patt + intern_cases_pattern test_kind_tolerant globalenv Id.Map.empty (None,[]) empty_alias patt (*********************************************************************) (* Functions to parse and interpret constructions *) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 24b5dfce29..34e94d1597 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -941,7 +941,7 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) try (* If already bound to a term, unify the binder and the term *) match DAst.get (Id.List.assoc var terms) with - | GVar id' -> + | GVar id' | GRef (GlobRef.VarRef id',None) -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma | t -> |