summaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml83
1 files changed, 45 insertions, 38 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 55e532dc..7a525f84 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -13,9 +13,10 @@ open CErrors
open Util
open Names
open Nameops
+open Constr
open Globnames
open Decl_kinds
-open Misctypes
+open Namegen
open Glob_term
open Glob_ops
open Mod_subst
@@ -28,7 +29,7 @@ open Notation_term
let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
-| NRef gr1, NRef gr2 -> eq_gr gr1 gr2
+| NRef gr1, NRef gr2 -> GlobRef.equal gr1 gr2
| NVar id1, NVar id2 -> (
match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
| Some n,Some m -> Int.equal n m
@@ -85,12 +86,12 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
Array.equal (eq_notation_constr vars) us1 us2 &&
Array.equal (eq_notation_constr vars) rs1 rs2
| NSort s1, NSort s2 ->
- Miscops.glob_sort_eq s1 s2
+ glob_sort_eq s1 s2
| NCast (t1, c1), NCast (t2, c2) ->
(eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _), _ -> false
+ | NRec _ | NSort _ | NCast _ ), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -152,10 +153,12 @@ let protect g e na =
if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern.");
e',na
-let apply_cases_pattern ?loc ((ids,disjpat),id) c =
- let tm = DAst.make ?loc (GVar id) in
+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 (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+ DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
+
+let apply_cases_pattern ?loc (ids_disjpat,id) c =
+ apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c
let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
@@ -181,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',disjpat,na = g e na in
(match disjpat with
| None -> GLetIn (na,f e b,Option.map (f e) t,f e' c)
- | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c)))
+ | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c)))
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
@@ -213,7 +216,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
- | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
+ | NCast (c,k) -> GCast (f e c,map_cast_type (f e) k)
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
@@ -430,7 +433,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
user_err Pp.(str "Binders marked as implicit not allowed in notations.");
add_name found na; (na,Option.map aux oc,aux b))) dll in
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
- | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+ | GCast (c,k) -> NCast (aux c,map_cast_type aux k)
| GSort s -> NSort s
| GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
@@ -505,7 +508,9 @@ let notation_constr_of_glob_constr nenv a =
let notation_constr_of_constr avoiding t =
let t = EConstr.of_constr t in
- let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = Detyping.detype Detyping.Now false avoiding env evd t in
let nenv = {
ninterp_var_type = Id.Map.empty;
ninterp_rec_vars = Id.Map.empty;
@@ -517,7 +522,7 @@ let rec subst_pat subst pat =
| PatVar _ -> pat
| PatCstr (((kn,i),j),cpl,n) ->
let kn' = subst_mind subst kn
- and cpl' = List.smartmap (subst_pat subst) cpl in
+ and cpl' = List.Smart.map (subst_pat subst) cpl in
if kn' == kn && cpl' == cpl then pat else
DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
@@ -532,7 +537,7 @@ let rec subst_notation_constr subst bound raw =
| NApp (r,rl) ->
let r' = subst_notation_constr subst bound r
- and rl' = List.smartmap (subst_notation_constr subst bound) rl in
+ and rl' = List.Smart.map (subst_notation_constr subst bound) rl in
if r' == r && rl' == rl then raw else
NApp(r',rl')
@@ -562,14 +567,14 @@ let rec subst_notation_constr subst bound raw =
| NLetIn (n,r1,t,r2) ->
let r1' = subst_notation_constr subst bound r1 in
- let t' = Option.smartmap (subst_notation_constr subst bound) t in
+ let t' = Option.Smart.map (subst_notation_constr subst bound) t in
let r2' = subst_notation_constr subst bound r2 in
if r1' == r1 && t == t' && r2' == r2 then raw else
NLetIn (n,r1',t',r2')
| NCases (sty,rtntypopt,rl,branches) ->
- let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
- and rl' = List.smartmap
+ let rtntypopt' = Option.Smart.map (subst_notation_constr subst bound) rtntypopt
+ and rl' = List.Smart.map
(fun (a,(n,signopt) as x) ->
let a' = subst_notation_constr subst bound a in
let signopt' = Option.map (fun ((indkn,i),nal as z) ->
@@ -577,9 +582,9 @@ let rec subst_notation_constr subst bound raw =
if indkn == indkn' then z else ((indkn',i),nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
rl
- and branches' = List.smartmap
+ and branches' = List.Smart.map
(fun (cpl,r as branch) ->
- let cpl' = List.smartmap (subst_pat subst) cpl
+ let cpl' = List.Smart.map (subst_pat subst) cpl
and r' = subst_notation_constr subst bound r in
if cpl' == cpl && r' == r then branch else
(cpl',r'))
@@ -590,14 +595,14 @@ let rec subst_notation_constr subst bound raw =
NCases (sty,rtntypopt',rl',branches')
| NLetTuple (nal,(na,po),b,c) ->
- let po' = Option.smartmap (subst_notation_constr subst bound) po
+ let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b' = subst_notation_constr subst bound b
and c' = subst_notation_constr subst bound c in
if po' == po && b' == b && c' == c then raw else
NLetTuple (nal,(na,po'),b',c')
| NIf (c,(na,po),b1,b2) ->
- let po' = Option.smartmap (subst_notation_constr subst bound) po
+ let po' = Option.Smart.map (subst_notation_constr subst bound) po
and b1' = subst_notation_constr subst bound b1
and b2' = subst_notation_constr subst bound b2
and c' = subst_notation_constr subst bound c in
@@ -606,12 +611,12 @@ let rec subst_notation_constr subst bound raw =
| NRec (fk,idl,dll,tl,bl) ->
let dll' =
- Array.smartmap (List.smartmap (fun (na,oc,b as x) ->
- let oc' = Option.smartmap (subst_notation_constr subst bound) oc in
+ Array.Smart.map (List.Smart.map (fun (na,oc,b as x) ->
+ let oc' = Option.Smart.map (subst_notation_constr subst bound) oc in
let b' = subst_notation_constr subst bound b in
if oc' == oc && b' == b then x else (na,oc',b'))) dll in
- let tl' = Array.smartmap (subst_notation_constr subst bound) tl in
- let bl' = Array.smartmap (subst_notation_constr subst bound) bl in
+ let tl' = Array.Smart.map (subst_notation_constr subst bound) tl in
+ let bl' = Array.Smart.map (subst_notation_constr subst bound) bl in
if dll' == dll && tl' == tl && bl' == bl then raw else
NRec (fk,idl,dll',tl',bl')
@@ -624,13 +629,13 @@ let rec subst_notation_constr subst bound raw =
if nref == ref then knd else Evar_kinds.ImplicitArg (nref, i, b)
| _ -> knd
in
- let nsolve = Option.smartmap (Genintern.generic_substitute subst) solve in
+ let nsolve = Option.Smart.map (Genintern.generic_substitute subst) solve in
if nsolve == solve && nknd == knd then raw
else NHole (nknd, naming, nsolve)
| NCast (r1,k) ->
let r1' = subst_notation_constr subst bound r1 in
- let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
+ let k' = smartmap_cast_type (subst_notation_constr subst bound) k in
if r1' == r1 && k' == k then raw else NCast(r1',k')
let subst_interpretation subst (metas,pat) =
@@ -651,11 +656,11 @@ let abstract_return_type_context pi mklam tml rtno =
let abstract_return_type_context_glob_constr tml rtn =
abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal)
(fun na c -> DAst.make @@
- GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
+ GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,IntroAnonymous,None),c)) 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, Misctypes.IntroAnonymous, None),c)) tml rtn
+ (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, IntroAnonymous, None),c)) tml rtn
let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -672,7 +677,7 @@ let is_onlybinding_meta id metas =
let is_onlybinding_pattern_like_meta isvar id metas =
try match Id.List.assoc id metas with
| _,NtnTypeBinder (NtnBinderParsedAsConstr
- (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ (AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
| _ -> false
with Not_found -> false
@@ -887,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
| GVar id' ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
- | _ -> anomaly (str "A term which can be a binder has to be a variable.")
+ | t ->
+ (* The term is a non-variable pattern *)
+ raise No_match
with Not_found ->
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
@@ -995,9 +1002,9 @@ let remove_sigma x (terms,termlists,binders,binderlists) =
let remove_bindinglist_sigma x (terms,termlists,binders,binderlists) =
(terms,termlists,binders,Id.List.remove_assoc x binderlists)
-let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas
+let add_ldots_var metas = (ldots_var,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas
-let add_meta_bindinglist x metas = (x,((None,[]),NtnTypeBinderList))::metas
+let add_meta_bindinglist x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeBinderList))::metas
(* This tells if letins in the middle of binders should be included in
the sequence of binders *)
@@ -1042,7 +1049,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
let alp,sigma = bind_bindinglist_env alp sigma x bl in
match_fun alp metas sigma rest termin
-let add_meta_term x metas = (x,((None,[]),NtnTypeConstr))::metas
+let add_meta_term x metas = (x,((Constrexpr.InConstrEntrySomeLevel,(None,[])),NtnTypeConstr))::metas (* Should reuse the scope of the partner of x! *)
let match_termlist match_fun alp metas sigma rest x y iter termin revert =
let rec aux sigma acc rest =
@@ -1111,7 +1118,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching compositionally *)
| GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
- | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
@@ -1179,7 +1186,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GCast(t1, c1), NCast(t2, c2) ->
match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
| GSort (GType _), NSort (GType _) when not u -> sigma
- | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
+ | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -1193,7 +1200,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
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'),Misctypes.IntroAnonymous,None) 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
@@ -1207,7 +1214,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _), _ -> raise No_match
+ | GCast _ ), _ -> raise No_match
and match_in u = match_ true u
@@ -1223,7 +1230,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
let store, get = set_temporary_memory () in
match na1, DAst.get b1, na2 with
(* Matching individual binders as part of a recursive pattern *)
- | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
+ | Name p, GCases (Constr.LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
(match get () with
| [{CAst.v=(ids,disj_of_patl,b1)}] ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 18:41:20 +0000