aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml76
1 files changed, 56 insertions, 20 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c4d2a2a496..f51d3bfdfb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -131,7 +131,11 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
| NApp (t1, a1), NApp (t2, a2) -> aux vars renaming t1 t2; List.iter2 (aux vars renaming) a1 a2
| NLambda (na1, t1, u1), NLambda (na2, t2, u2)
| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- aux vars renaming t1 t2;
+ (match t1, t2 with
+ | None, None -> ()
+ | Some _, None -> if lt then strictly_lt := true
+ | Some t1, Some t2 -> aux vars renaming t1 t2
+ | None, Some _ -> raise Exit);
let renaming = check_eq_name vars renaming na1 na2 in
aux vars renaming u1 u2
| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
@@ -272,11 +276,25 @@ let default_binder_status_fun = {
slide = (fun x -> x);
}
+let test_implicit_argument_mark bk =
+ if not (Glob_ops.binding_kind_eq bk Explicit) then
+ user_err (Pp.str "Unexpected implicit argument mark.")
+
+let test_pattern_cast = function
+ | None -> ()
+ | Some t -> user_err ?loc:t.CAst.loc (Pp.str "Unsupported pattern cast.")
+
let protect g e na =
- let e',disjpat,na = g e na in
+ let e',disjpat,na,bk,t = g e na None in
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
+ test_implicit_argument_mark bk;
+ test_pattern_cast t;
e',na
+let set_anonymous_type na = function
+ | None -> DAst.make @@ GHole (Evar_kinds.BinderType na, IntroAnonymous, None)
+ | Some t -> t
+
let apply_cases_pattern_term ?loc (ids,disjpat) tm c =
let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
@@ -302,15 +320,21 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e = h.switch_lambda e in
- let e',disjpat,na = g e na in GLambda (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let ty = Option.map (f (h.restart_prod e)) ty in
+ let e',disjpat,na',bk,ty = g e na ty in
+ GLambda (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NProd (na,ty,c) ->
let e = h.switch_prod e in
- let e',disjpat,na = g e na in GProd (na,Explicit,f (h.restart_prod e) ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
+ let ty = Option.map (f (h.restart_prod e)) ty in
+ let e',disjpat,na',bk,ty = g e na ty in
+ GProd (na',bk,set_anonymous_type na ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
| NLetIn (na,b,t,c) ->
- let e',disjpat,na = g e na in
+ let t = Option.map (f (h.restart_prod e)) t in
+ let e',disjpat,na,bk,t = g e na t in
+ test_implicit_argument_mark bk;
(match disjpat with
- | None -> GLetIn (na,f (h.restart_lambda e) b,Option.map (f (h.restart_prod e)) t,f e' c)
- | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
+ | None -> GLetIn (na,f (h.restart_lambda e) b,t,f e' c)
+ | Some (disjpat,_id) -> test_pattern_cast t; DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e = h.no e in
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
@@ -323,7 +347,11 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
e',Some (CAst.make ?loc (ind,nal')) in
let e',na' = protect g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
- let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in
+ let fold (idl,e) na =
+ let (e,disjpat,na,bk,t) = g e na None in
+ test_implicit_argument_mark bk;
+ test_pattern_cast t;
+ ((Name.cons na idl,e),disjpat,na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
@@ -356,7 +384,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
- glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),None,id)) aux () x
+ glob_constr_of_notation_constr_with_binders ?loc (fun () id t -> ((),None,id,Explicit,t)) aux () x
in aux () x
(******************************************************************************)
@@ -551,8 +579,8 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GApp (g,args) ->
(* Treat applicative notes as binary nodes *)
let a,args = List.sep_last args in mkNApp1 (aux (DAst.make (GApp (g, args))), aux a)
- | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
- | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
+ | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux_type ty,aux c)
+ | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux_type ty,aux c)
| GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
| GCases (sty,rtntypopt,tml,eqnl) ->
let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
@@ -589,6 +617,9 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
) x
+ and aux_type t = DAst.with_val (function
+ | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+ | _ -> Some (aux t)) t
in
let t = aux a in
(* Side effect *)
@@ -697,13 +728,13 @@ let rec subst_notation_constr subst bound raw =
NList (id1,id2,r1',r2',b)
| NLambda (n,r1,r2) ->
- let r1' = subst_notation_constr subst bound r1
+ let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
and r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
NLambda (n,r1',r2')
| NProd (n,r1,r2) ->
- let r1' = subst_notation_constr subst bound r1
+ let r1' = Option.Smart.map (subst_notation_constr subst bound) r1
and r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && r2' == r2 then raw else
NProd (n,r1',r2')
@@ -819,7 +850,7 @@ let abstract_return_type_context_glob_constr tml rtn =
let abstract_return_type_context_notation_constr tml rtn =
abstract_return_type_context snd
- (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
+ (fun na c -> NLambda(na,None,c)) tml rtn
let rec push_pattern_binders vars pat =
match DAst.get pat with
@@ -852,6 +883,7 @@ let is_onlybinding_pattern_like_meta isvar id metas =
| _,NtnTypeBinder (NtnBinderParsedAsConstr
(AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+ | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
| _ -> false
with Not_found -> false
@@ -1325,9 +1357,9 @@ let rec match_ inner u alp metas sigma a1 a2 =
List.fold_left2 (match_ may_use_eta u alp metas)
(match_hd u alp metas sigma f1 f2) l1 l2
| GLambda (na1,bk1,t1,b1), NLambda (na2,t2,b2) ->
- match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2
+ match_extended_binders false u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
| GProd (na1,bk1,t1,b1), NProd (na2,t2,b2) ->
- match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in u alp metas sigma t1 t2) b1 b2
+ match_extended_binders true u alp metas na1 na2 bk1 t1 (match_in_type u alp metas sigma t1 t2) b1 b2
| GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
| GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
@@ -1396,14 +1428,14 @@ let rec match_ inner u alp metas sigma a1 a2 =
otherwise how to ensure it corresponds to a well-typed eta-expansion;
we make an exception for types which are metavariables: this is useful e.g.
to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
- | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+ | _b1, NLambda (Name id as na,(None | Some (NVar _) as t2),b2) when inner ->
let avoid =
Id.Set.union (free_glob_vars a1) (* as in Namegen: *) (glob_visible_short_qualid a1) in
let id' = Namegen.next_ident_away id avoid in
let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),IntroAnonymous,None) in
let sigma = match t2 with
- | NHole _ -> sigma
- | NVar id2 -> bind_term_env alp sigma id2 t1
+ | None -> sigma
+ | Some (NVar id2) -> bind_term_env alp sigma id2 t1
| _ -> assert false in
let (alp,sigma) =
if is_bindinglist_meta id metas then
@@ -1423,6 +1455,10 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
| GCast _ | GInt _ | GFloat _ | GArray _), _ -> raise No_match
+and match_in_type u alp metas sigma t = function
+ | None -> sigma
+ | Some t' -> match_in u alp metas sigma t t'
+
and match_in u = match_ true u
and match_hd u = match_ false u
@@ -1497,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
let v = glob_constr_of_cases_pattern (Global.env()) pat in
(((vars,v),scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
(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.25.1) at 2026-01-31 15:22:07 +0000