aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml75
1 files changed, 39 insertions, 36 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index a0d69ce79..ab0bf9c6f 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,7 +86,7 @@ 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
| NProj (p1, c1), NProj (p2, c2) ->
@@ -157,7 +158,7 @@ let protect g e na =
let apply_cases_pattern ?loc ((ids,disjpat),id) c =
let tm = DAst.make ?loc (GVar id) in
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 glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let lt x = DAst.make ?loc x in lt @@ match nc with
@@ -165,15 +166,15 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NApp (a,args) -> GApp (f e a, List.map (f e) args)
| NList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NBinderList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let innerl = (ldots_var,t)::(if swap then [y, lt @@ GVar x] else []) in
let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ let outerl = (ldots_var,inner)::(if swap then [] else [y, lt @@ GVar x]) in
DAst.get (subst_glob_vars outerl it)
| NLambda (na,ty,c) ->
let e',disjpat,na = g e na in GLambda (na,Explicit,f e ty,Option.fold_right (apply_cases_pattern ?loc) disjpat (f e' c))
@@ -210,12 +211,12 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
let e',na = protect g e na in
GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
- let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+ let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
let e,na = protect g e na in
(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)
@@ -433,7 +434,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;
@@ -509,7 +510,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;
@@ -521,7 +524,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)
@@ -536,7 +539,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')
@@ -566,14 +569,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) ->
@@ -581,9 +584,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'))
@@ -594,14 +597,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
@@ -610,12 +613,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')
@@ -628,13 +631,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')
| NProj (p, c) ->
@@ -663,11 +666,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
@@ -684,7 +687,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
@@ -1123,7 +1126,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 =
@@ -1191,7 +1194,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
@@ -1205,7 +1208,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
@@ -1238,7 +1241,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)}] ->
@@ -1335,10 +1338,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
| PatVar Anonymous, NHole _ -> sigma,(0,[])
- | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
sigma,(0,l)
- | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
+ | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
when eq_constructor r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 04:37:52 +0000