aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml75
-rw-r--r--interp/notation.ml13
-rw-r--r--interp/notation_ops.ml28
3 files changed, 83 insertions, 33 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 379d09e89..158ac24b2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -549,6 +549,18 @@ let is_var store pat =
| PatVar na -> store na; true
| _ -> false
+let out_var pat =
+ match pat.CAst.v with
+ | CPatAtom (Some (Ident (_,id))) -> Name id
+ | 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 (st,Anonymous), Misctypes.IntroAnonymous, None))
+
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
| Anonymous -> (renaming,env), None, Anonymous
| Name id ->
@@ -564,13 +576,21 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
with Not_found ->
try
(* Trying to associate a pattern *)
- let pat,scopes = Id.Map.find id binders in
+ let pat,(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
- let pat, na = match disjpat with
- | [pat] when is_var store pat -> let na = get () in None, na
- | _ -> Some ((List.map snd ids,disjpat),id), snd na in
- (renaming,env), pat, na
+ if onlyident then
+ (* Do not try to interpret a variable as a constructor *)
+ let na = out_var pat in
+ let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in
+ (renaming,env), None, na
+ else
+ (* Interpret as a pattern *)
+ let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ let pat, na =
+ match disjpat with
+ | [pat] when is_var store pat -> let na = get () in None, na
+ | _ -> Some ((List.map snd ids,disjpat),id), snd na in
+ (renaming,env), pat, na
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -688,12 +708,15 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
let gc = intern nenv c in
(gc, Some c)
in
- let mk_env' (c, (tmp_scope, subscopes)) =
+ let mk_env' (c, (onlyident,(tmp_scope,subscopes))) =
let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in
- let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
- match disjpat with
- | [pat] -> (glob_constr_of_cases_pattern pat, None)
- | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
+ if onlyident then
+ let na = out_var 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 pat, None)
+ | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.CAst.loc ()
in
let terms = Id.Map.map mk_env terms in
let binders = Id.Map.map mk_env' binders in
@@ -744,15 +767,18 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
scopes = subscopes @ env.scopes} a
with Not_found ->
try
- let pat,scopes = Id.Map.find id binders in
+ let pat,(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
(* We deactivate impls to avoid the check on hidden parameters *)
(* and since we are only interested in the pattern as a term *)
let env = reset_hidden_inductive_implicit_test env in
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
- match disjpat with
- | [pat] -> glob_constr_of_cases_pattern pat
- | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
+ if onlyident then
+ term_of_name (out_var pat)
+ else
+ let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ match disjpat with
+ | [pat] -> glob_constr_of_cases_pattern pat
+ | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
with Not_found ->
try
match binderopt with
@@ -774,6 +800,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
into a substitution for interpretation and based on binding/constr
distinction *)
+let cases_pattern_of_name (loc,na) =
+ let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in
+ CAst.make ?loc (CPatAtom atom)
+
let split_by_type ids subst =
let bind id scl l s =
match l with
@@ -785,12 +815,17 @@ let split_by_type ids subst =
| NtnTypeConstr ->
let terms,terms' = bind id scl terms terms' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnParsedAsConstr ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+ let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+ let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
+ (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+ | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
- let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,scl) binders' in
+ let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
- let binders,binders' = bind id scl binders binders' in
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
+ let onlyident = (x = NtnParsedAsIdent) in
+ let binders,binders' = bind id (onlyident,scl) binders binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeConstrList ->
let termlists,termlists' = bind id scl termlists termlists' in
diff --git a/interp/notation.ml b/interp/notation.ml
index 13ff960f6..ea7ef21b1 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -97,9 +97,10 @@ let constr_entry_key_eq eq v1 v2 = match v1, v2 with
| ETBigint, ETBigint -> true
| ETBinder b1, ETBinder b2 -> b1 == b2
| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETPattern n1, ETPattern n2 -> Option.equal Int.equal n1 n2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _), _ -> false
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
@@ -626,10 +627,10 @@ let availability_of_prim_token n printer_scope local_scopes =
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
- | NtnParsedAsConstr, NtnParsedAsConstr -> true
- | NtnParsedAsIdent, NtnParsedAsIdent -> true
- | NtnParsedAsPattern, NtnParsedAsPattern -> true
- | (NtnParsedAsConstr | NtnParsedAsIdent | NtnParsedAsPattern), _ -> false
+| NtnParsedAsIdent, NtnParsedAsIdent -> true
+| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
+| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
+| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 44073c3b5..c65f4785e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -671,12 +671,20 @@ let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
with Not_found -> false
+let is_onlybinding_strict_meta id metas =
+ try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsPattern true) -> true | _ -> false
+ with Not_found -> false
+
let is_onlybinding_meta id metas =
try match Id.List.assoc id metas with _,NtnTypeBinder _ -> true | _ -> false
with Not_found -> false
-let is_onlybinding_pattern_like_meta id metas =
- try match Id.List.assoc id metas with _,NtnTypeBinder (NtnParsedAsConstr | NtnParsedAsPattern) -> true | _ -> false
+let is_onlybinding_pattern_like_meta isvar id metas =
+ try match Id.List.assoc id metas with
+ | _,NtnTypeBinder (NtnBinderParsedAsConstr
+ (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+ | _ -> false
with Not_found -> false
let is_bindinglist_meta id metas =
@@ -962,6 +970,8 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
| _ -> raise No_match
let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
+ | (na1,Name id2) when is_onlybinding_strict_meta id2 metas ->
+ raise No_match
| (na1,Name id2) when is_onlybinding_meta id2 metas ->
bind_binding_env alp sigma id2 [DAst.make (PatVar na1)]
| (Name id1,Name id2) when is_term_meta id2 metas ->
@@ -977,7 +987,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1 pat2 =
match DAst.get pat1, DAst.get pat2 with
- | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta id2 metas ->
+ | PatVar _, PatVar (Name id2) when is_onlybinding_pattern_like_meta true id2 metas ->
+ bind_binding_env alp sigma id2 [pat1]
+ | _, PatVar (Name id2) when is_onlybinding_pattern_like_meta false id2 metas ->
bind_binding_env alp sigma id2 [pat1]
| PatVar na1, PatVar na2 -> match_names metas acc na1 na2
| _, PatVar Anonymous when allow_catchall -> acc
@@ -1093,7 +1105,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
match DAst.get a1, a2 with
(* Matching notation variable *)
| r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
- | r1, NVar id2 when is_onlybinding_pattern_like_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | GVar _, NVar id2 when is_onlybinding_pattern_like_meta true id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | r1, NVar id2 when is_onlybinding_pattern_like_meta false id2 metas -> bind_binding_as_term_env alp sigma id2 a1
+ | GVar _, NVar id2 when is_onlybinding_strict_meta id2 metas -> raise No_match
| GVar _, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 a1
| r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
@@ -1232,7 +1246,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
match_in u alp metas sigma b1 b2
| _ -> assert false)
| Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
- when is_gvar p e && is_onlybinding_pattern_like_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
+ when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
(match get () with
| [(_,(ids,disj_of_patl,b1))] ->
let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
@@ -1276,13 +1290,13 @@ let match_notation_constr u c (metas,pat) =
| NtnTypeConstr ->
let term = try Id.List.assoc x terms with Not_found -> raise No_match in
((term, scl)::terms',termlists',binders',binderlists')
- | NtnTypeBinder NtnParsedAsConstr ->
+ | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
(match Id.List.assoc x binders with
| [pat] ->
let v = glob_constr_of_cases_pattern pat in
((v,scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
(terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:26:15 +0000