aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml33
-rw-r--r--interp/constrexpr_ops.ml202
-rw-r--r--interp/constrexpr_ops.mli11
-rw-r--r--interp/constrextern.ml165
-rw-r--r--interp/constrextern.mli12
-rw-r--r--interp/constrintern.ml516
-rw-r--r--interp/constrintern.mli23
-rw-r--r--interp/dumpglob.ml32
-rw-r--r--interp/dumpglob.mli12
-rw-r--r--interp/implicit_quantifiers.ml4
-rw-r--r--interp/modintern.ml2
-rw-r--r--interp/notation.ml476
-rw-r--r--interp/notation.mli50
-rw-r--r--interp/notation_ops.ml506
-rw-r--r--interp/notation_ops.mli16
-rw-r--r--interp/notation_term.ml11
-rw-r--r--interp/numTok.mli30
-rw-r--r--interp/reserve.ml4
-rw-r--r--interp/smartlocate.ml38
-rw-r--r--interp/smartlocate.mli12
-rw-r--r--interp/stdarg.ml3
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/syntax_def.ml6
-rw-r--r--interp/syntax_def.mli2
24 files changed, 1465 insertions, 703 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d14d156ffc..b14c325f69 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -13,10 +13,26 @@ open Libnames
(** {6 Concrete syntax for terms } *)
-(** [constr_expr] is the abstract syntax tree produced by the parser *)
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
+(** Universes *)
+type sort_name_expr =
+ | CSProp | CProp | CSet
+ | CType of qualid
+ | CRawType of Univ.Level.t (** Universes like "foo.1" have no qualid form *)
+
+type univ_level_expr = sort_name_expr Glob_term.glob_sort_gen
+type sort_expr = (sort_name_expr * int) list Glob_term.glob_sort_gen
+
+type instance_expr = univ_level_expr list
+
+(** Constraints don't have anonymous universes *)
+type univ_constraint_expr = sort_name_expr * Univ.constraint_type * sort_name_expr
+
+type universe_decl_expr = (lident list, univ_constraint_expr list) UState.gen_universe_decl
+type cumul_univ_decl_expr =
+ ((lident * Univ.Variance.t option) list, univ_constraint_expr list) UState.gen_universe_decl
type ident_decl = lident * universe_decl_expr option
+type cumul_ident_decl = lident * cumul_univ_decl_expr option
type name_decl = lname * universe_decl_expr option
type notation_with_optional_scope = LastLonelyNotation | NotationInScope of string
@@ -58,11 +74,10 @@ type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
type prim_token =
- | Numeral of NumTok.Signed.t
+ | Number of NumTok.Signed.t
| String of string
-type instance_expr = Glob_term.glob_level list
-
+(** [constr_expr] is the abstract syntax tree produced by the parser *)
type cases_pattern_expr_r =
| CPatAlias of cases_pattern_expr * lname
| CPatCstr of qualid
@@ -80,6 +95,8 @@ type cases_pattern_expr_r =
| CPatCast of cases_pattern_expr * constr_expr
and cases_pattern_expr = cases_pattern_expr_r CAst.t
+and kinded_cases_pattern_expr = cases_pattern_expr * Glob_term.binding_kind
+
and cases_pattern_notation_substitution =
cases_pattern_expr list * (* for constr subterms *)
cases_pattern_expr list list (* for recursive notations *)
@@ -109,7 +126,7 @@ and constr_expr_r =
| CHole of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
| CPatVar of Pattern.patvar
| CEvar of Glob_term.existential_name CAst.t * (lident * constr_expr) list
- | CSort of Glob_term.glob_sort
+ | CSort of sort_expr
| CCast of constr_expr * constr_expr Glob_term.cast_type
| CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
| CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
@@ -142,12 +159,12 @@ and recursion_order_expr = recursion_order_expr_r CAst.t
and local_binder_expr =
| CLocalAssum of lname list * binder_kind * constr_expr
| CLocalDef of lname * constr_expr * constr_expr option
- | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
+ | CLocalPattern of cases_pattern_expr
and constr_notation_substitution =
constr_expr list * (* for constr subterms *)
constr_expr list list * (* for recursive notations *)
- cases_pattern_expr list * (* for binders *)
+ kinded_cases_pattern_expr list * (* for binders *)
local_binder_expr list list (* for binder lists (recursive notations) *)
type constr_pattern_expr = constr_expr
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7075d082ee..f02874253e 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -18,6 +18,25 @@ open Glob_term
open Notation
open Constrexpr
+(***********)
+(* Universes *)
+
+let sort_name_expr_eq c1 c2 = match c1, c2 with
+ | CSProp, CSProp
+ | CProp, CProp
+ | CSet, CSet -> true
+ | CType q1, CType q2 -> Libnames.qualid_eq q1 q2
+ | CRawType u1, CRawType u2 -> Univ.Level.equal u1 u2
+ | (CSProp|CProp|CSet|CType _|CRawType _), _ -> false
+
+let univ_level_expr_eq u1 u2 =
+ Glob_ops.glob_sort_gen_eq sort_name_expr_eq u1 u2
+
+let sort_expr_eq u1 u2 =
+ Glob_ops.glob_sort_gen_eq
+ (List.equal (fun (x,m) (y,n) -> sort_name_expr_eq x y && Int.equal m n))
+ u1 u2
+
(***********************)
(* For binders parsing *)
@@ -44,13 +63,13 @@ let names_of_local_binders bl =
(**********************************************************************)
(* Functions on constr_expr *)
-(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+(* Note: redundant Number representations, such as -0 and +0 (and others),
are considered different here. *)
let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2
+| Number n1, Number n2 -> NumTok.Signed.equal n1 n2
| String s1, String s2 -> String.equal s1 s2
-| (Numeral _ | String _), _ -> false
+| (Number _ | String _), _ -> false
let explicitation_eq ex1 ex2 = match ex1, ex2 with
| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
@@ -59,13 +78,11 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
Id.equal id1 id2
| _ -> false
-let eq_ast f { CAst.v = x } { CAst.v = y } = f x y
-
let rec cases_pattern_expr_eq p1 p2 =
if CAst.(p1.v == p2.v) then true
else match CAst.(p1.v, p2.v) with
| CPatAlias(a1,i1), CPatAlias(a2,i2) ->
- eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
+ CAst.eq Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
qualid_eq c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -94,6 +111,9 @@ and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) =
List.equal cases_pattern_expr_eq s1 s2 &&
List.equal (List.equal cases_pattern_expr_eq) n1 n2
+let kinded_cases_pattern_expr_eq (p1,bk1) (p2,bk2) =
+ cases_pattern_expr_eq p1 p2 && Glob_ops.binding_kind_eq bk1 bk2
+
let eq_universes u1 u2 =
match u1, u2 with
| None, None -> true
@@ -105,10 +125,10 @@ let rec constr_expr_eq e1 e2 =
else match CAst.(e1.v, e2.v) with
| CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2
| CFix(id1,fl1), CFix(id2,fl2) ->
- eq_ast Id.equal id1 id2 &&
+ lident_eq id1 id2 &&
List.equal fix_expr_eq fl1 fl2
| CCoFix(id1,fl1), CCoFix(id2,fl2) ->
- eq_ast Id.equal id1 id2 &&
+ lident_eq id1 id2 &&
List.equal cofix_expr_eq fl1 fl2
| CProdN(bl1,a1), CProdN(bl2,a2) ->
List.equal local_binder_eq bl1 bl2 &&
@@ -117,7 +137,7 @@ let rec constr_expr_eq e1 e2 =
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2
| CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
- eq_ast Name.equal na1 na2 &&
+ CAst.eq Name.equal na1 na2 &&
constr_expr_eq a1 a2 &&
Option.equal constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
@@ -141,14 +161,14 @@ let rec constr_expr_eq e1 e2 =
List.equal case_expr_eq a1 a2 &&
List.equal branch_expr_eq brl1 brl2
| CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
- List.equal (eq_ast Name.equal) n1 n2 &&
- Option.equal (eq_ast Name.equal) m1 m2 &&
+ List.equal (CAst.eq Name.equal) n1 n2 &&
+ Option.equal (CAst.eq Name.equal) m1 m2 &&
Option.equal constr_expr_eq e1 e2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
| CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
constr_expr_eq e1 e2 &&
- Option.equal (eq_ast Name.equal) n1 n2 &&
+ Option.equal (CAst.eq Name.equal) n1 n2 &&
Option.equal constr_expr_eq r1 r2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq f1 f2
@@ -158,7 +178,7 @@ let rec constr_expr_eq e1 e2 =
| CEvar (id1, c1), CEvar (id2, c2) ->
Id.equal id1.CAst.v id2.CAst.v && List.equal instance_eq c1 c2
| CSort s1, CSort s2 ->
- Glob_ops.glob_sort_eq s1 s2
+ sort_expr_eq s1 s2
| CCast(t1,c1), CCast(t2,c2) ->
constr_expr_eq t1 t2 && cast_expr_eq c1 c2
| CNotation(inscope1, n1, s1), CNotation(inscope2, n2, s2) ->
@@ -184,12 +204,12 @@ let rec constr_expr_eq e1 e2 =
| CGeneralization _ | CDelimiters _ | CArray _), _ -> false
and args_eq (a1,e1) (a2,e2) =
- Option.equal (eq_ast explicitation_eq) e1 e2 &&
+ Option.equal (CAst.eq explicitation_eq) e1 e2 &&
constr_expr_eq a1 a2
and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
constr_expr_eq e1 e2 &&
- Option.equal (eq_ast Name.equal) n1 n2 &&
+ Option.equal (CAst.eq Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
@@ -197,41 +217,41 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
constr_expr_eq e1 e2
and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
- (eq_ast Id.equal id1 id2) &&
+ (lident_eq id1 id2) &&
Option.equal recursion_order_expr_eq r1 r2 &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
- (eq_ast Id.equal id1 id2) &&
+ (lident_eq id1 id2) &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
and recursion_order_expr_eq_r r1 r2 = match r1, r2 with
- | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
+ | CStructRec i1, CStructRec i2 -> lident_eq i1 i2
| CWfRec (i1,e1), CWfRec (i2,e2) ->
constr_expr_eq e1 e2
| CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
- Option.equal (eq_ast Id.equal) i1 i2 &&
+ Option.equal lident_eq i1 i2 &&
constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
| _ -> false
-and recursion_order_expr_eq r1 r2 = eq_ast recursion_order_expr_eq_r r1 r2
+and recursion_order_expr_eq r1 r2 = CAst.eq recursion_order_expr_eq_r r1 r2
and local_binder_eq l1 l2 = match l1, l2 with
| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
- eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
+ CAst.eq Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
(* Don't care about the [binder_kind] *)
- List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
+ List.equal (CAst.eq Name.equal) n1 n2 && constr_expr_eq e1 e2
| _ -> false
and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
List.equal constr_expr_eq e1 e2 &&
List.equal (List.equal constr_expr_eq) el1 el2 &&
- List.equal cases_pattern_expr_eq b1 b2 &&
+ List.equal kinded_cases_pattern_expr_eq b1 b2 &&
List.equal (List.equal local_binder_eq) bl1 bl2
and instance_eq (x1,c1) (x2,c2) =
@@ -268,39 +288,37 @@ let is_constructor id =
(Nametab.locate_extended (qualid_of_ident id)))
with Not_found -> false
-let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
+let rec cases_pattern_fold_names f h nacc pt = match CAst.(pt.v) with
| CPatRecord l ->
- List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
- | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
+ List.fold_left (fun nacc (r, cp) -> cases_pattern_fold_names f h nacc cp) nacc l
+ | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right (fun na (n,acc) -> (f na n,acc)) na (cases_pattern_fold_names f h nacc pat)
| CPatOr (patl) ->
- List.fold_left (cases_pattern_fold_names f) a patl
+ List.fold_left (cases_pattern_fold_names f h) nacc patl
| CPatCstr (_,patl1,patl2) ->
- List.fold_left (cases_pattern_fold_names f)
- (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
+ List.fold_left (cases_pattern_fold_names f h)
+ (Option.fold_left (List.fold_left (cases_pattern_fold_names f h)) nacc patl1) patl2
| CPatNotation (_,_,(patl,patll),patl') ->
- List.fold_left (cases_pattern_fold_names f)
- (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
- | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
+ List.fold_left (cases_pattern_fold_names f h)
+ (List.fold_left (cases_pattern_fold_names f h) nacc (patl@List.flatten patll)) patl'
+ | CPatDelimiters (_,pat) -> cases_pattern_fold_names f h nacc pat
| CPatAtom (Some qid)
when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
- f (qualid_basename qid) a
- | CPatPrim _ | CPatAtom _ -> a
- | CPatCast ({CAst.loc},_) ->
- CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
- (Pp.strbrk "Casts are not supported here.")
-
-let ids_of_pattern =
- cases_pattern_fold_names Id.Set.add Id.Set.empty
-
-let ids_of_pattern_list =
- List.fold_left
- (List.fold_left (cases_pattern_fold_names Id.Set.add))
- Id.Set.empty
+ let (n, acc) = nacc in
+ (f (qualid_basename qid) n, acc)
+ | CPatPrim _ | CPatAtom _ -> nacc
+ | CPatCast (p,t) ->
+ let (n, acc) = nacc in
+ cases_pattern_fold_names f h (n, h acc t) p
+
+let ids_of_pattern_list p =
+ fst (List.fold_left
+ (List.fold_left (cases_pattern_fold_names Id.Set.add (fun () _ -> ())))
+ (Id.Set.empty,()) p)
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_, ona, indnal) l ->
- Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+ Option.fold_right (fun t ids -> fst (cases_pattern_fold_names Id.Set.add (fun () _ -> ()) (ids,()) t))
indnal
(Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
tms Id.Set.empty
@@ -312,9 +330,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function
f n (fold_local_binders g f n' acc b l) t
| CLocalDef ( { v = na },c,t)::l ->
Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
- | CLocalPattern { v = pat,t }::l ->
- let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
- Option.fold_left (f n) acc t
+ | CLocalPattern pat :: l ->
+ let n, acc = cases_pattern_fold_names g (f n) (n,acc) pat in
+ fold_local_binders g f n acc b l
| [] ->
f n acc b
@@ -378,10 +396,42 @@ let names_of_constr_expr c =
let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
+let rec fold_map_cases_pattern f h acc (CAst.{v=pt;loc} as p) = match pt with
+ | CPatRecord l ->
+ let acc, l = List.fold_left_map (fun acc (r, cp) -> let acc, cp = fold_map_cases_pattern f h acc cp in acc, (r, cp)) acc l in
+ acc, CAst.make ?loc (CPatRecord l)
+ | CPatAlias (pat,({CAst.v=na} as lna)) ->
+ let acc, p = fold_map_cases_pattern f h acc pat in
+ let acc = Name.fold_right f na acc in
+ acc, CAst.make ?loc (CPatAlias (pat,lna))
+ | CPatOr patl ->
+ let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+ acc, CAst.make ?loc (CPatOr patl)
+ | CPatCstr (c,patl1,patl2) ->
+ let acc, patl1 = Option.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patl1 in
+ let acc, patl2 = List.fold_left_map (fold_map_cases_pattern f h) acc patl2 in
+ acc, CAst.make ?loc (CPatCstr (c,patl1,patl2))
+ | CPatNotation (sc,ntn,(patl,patll),patl') ->
+ let acc, patl = List.fold_left_map (fold_map_cases_pattern f h) acc patl in
+ let acc, patll = List.fold_left_map (List.fold_left_map (fold_map_cases_pattern f h)) acc patll in
+ let acc, patl' = List.fold_left_map (fold_map_cases_pattern f h) acc patl' in
+ acc, CAst.make ?loc (CPatNotation (sc,ntn,(patl,patll),patl'))
+ | CPatDelimiters (d,pat) ->
+ let acc, p = fold_map_cases_pattern f h acc pat in
+ acc, CAst.make ?loc (CPatDelimiters (d,pat))
+ | CPatAtom (Some qid)
+ when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) ->
+ f (qualid_basename qid) acc, p
+ | CPatPrim _ | CPatAtom _ -> (acc,p)
+ | CPatCast (pat,t) ->
+ let acc, pat = fold_map_cases_pattern f h acc pat in
+ let t = h acc t in
+ acc, CAst.make ?loc (CPatCast (pat,t))
+
(* Used in correctness and interface *)
let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
-let map_local_binders f g e bl =
+let fold_map_local_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
let open CAst in
let h (e,bl) = function
@@ -389,9 +439,9 @@ let map_local_binders f g e bl =
(map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
| CLocalDef( { loc ; v = na } as cna ,c,ty) ->
(Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
- | CLocalPattern { loc; v = pat,t } ->
- let ids = ids_of_pattern pat in
- (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
+ | CLocalPattern pat ->
+ let e, pat = fold_map_cases_pattern g f e pat in
+ (e, CLocalPattern pat::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
@@ -400,16 +450,16 @@ let map_constr_expr_with_binders g f e = CAst.map (function
| CApp ((p,a),l) ->
CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
| CProdN (bl,b) ->
- let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
+ let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
| CLambdaN (bl,b) ->
- let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
+ let (e,bl) = fold_map_local_binders f g e bl in CLambdaN (bl,f e b)
| CLetIn (na,a,t,b) ->
CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
| CCast (a,c) -> CCast (f e a, Glob_ops.map_cast_type (f e) c)
| CNotation (inscope,n,(l,ll,bl,bll)) ->
(* This is an approximation because we don't know what binds what *)
CNotation (inscope,n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
- List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
+ List.map (fun bl -> snd (fold_map_local_binders f g e bl)) bll))
| CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
| CDelimiters (s,a) -> CDelimiters (s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
@@ -431,7 +481,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (id,dl) ->
CFix (id,List.map (fun (id,n,bl,t,d) ->
- let (e',bl') = map_local_binders f g e bl in
+ let (e',bl') = fold_map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
@@ -439,7 +489,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
(id,n,bl',t',d')) dl)
| CCoFix (id,dl) ->
CCoFix (id,List.map (fun (id,bl,t,d) ->
- let (e',bl') = map_local_binders f g e bl in
+ let (e',bl') = fold_map_local_binders f g e bl in
let t' = f e' t in
let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
let d' = f e'' d in
@@ -472,7 +522,7 @@ let locs_of_notation ?loc locs ntn =
let ntn_loc ?loc (args,argslist,binders,binderslist) =
locs_of_notation ?loc
(List.map constr_loc (args@List.flatten argslist)@
- List.map cases_pattern_expr_loc binders@
+ List.map (fun (x,_) -> cases_pattern_expr_loc x) binders@
List.map local_binders_loc binderslist)
let patntn_loc ?loc (args,argslist) =
@@ -614,37 +664,3 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
| _ ->
CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
(str "This expression should be coercible to a pattern.")) c
-
-(** Local universe and constraint declarations. *)
-
-let interp_univ_constraints env evd cstrs =
- let interp (evd,cstrs) (u, d, u') =
- let ul = Pretyping.interp_known_glob_level evd u in
- let u'l = Pretyping.interp_known_glob_level evd u' in
- let cstr = (ul,d,u'l) in
- let cstrs' = Univ.Constraint.add cstr cstrs in
- try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
- evd, cstrs'
- with Univ.UniverseInconsistency e as exn ->
- let _, info = Exninfo.capture exn in
- CErrors.user_err ~hdr:"interp_constraint" ~info
- (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
- in
- List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
- let open UState in
- let pl : lident list = decl.univdecl_instance in
- let evd = Evd.from_ctx (UState.make_with_initial_binders ~lbound:(Environ.universes_lbound env)
- (Environ.universes env) pl) in
- let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
- let decl = { univdecl_instance = pl;
- univdecl_extensible_instance = decl.univdecl_extensible_instance;
- univdecl_constraints = cstrs;
- univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
- in evd, decl
-
-let interp_univ_decl_opt env l =
- match l with
- | None -> Evd.from_env env, UState.default_univ_decl
- | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index edf52c93e8..ffa7c8ec10 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -16,6 +16,10 @@ open Constrexpr
(** {6 Equalities on [constr_expr] related types} *)
+val sort_name_expr_eq : sort_name_expr -> sort_name_expr -> bool
+val univ_level_expr_eq : univ_level_expr -> univ_level_expr -> bool
+val sort_expr_eq : sort_expr -> sort_expr -> bool
+
val explicitation_eq : explicitation -> explicitation -> bool
(** Equality on [explicitation]. *)
@@ -123,10 +127,3 @@ val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> notation -
(** For cases pattern parsing errors *)
val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
-
-(** Local universe and constraint declarations. *)
-val interp_univ_decl : Environ.env -> universe_decl_expr ->
- Evd.evar_map * UState.universe_decl
-
-val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
- Evd.evar_map * UState.universe_decl
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7bf1c58148..3969c7ea1f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,7 +85,7 @@ let is_reserved_type na t =
| Name id ->
try
let pat = Reserve.find_reserved_type id in
- let _ = match_notation_constr false t ([],pat) in
+ let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([],pat) in
true
with Not_found | No_match -> false
@@ -357,18 +357,18 @@ let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l bl =
match snd ntn,List.map destprim l with
(* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
- | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
+ | "- _", [Some (Number p)] when not (NumTok.Signed.is_zero p) ->
assert (bl=[]);
mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
| (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
- | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
+ | Some n -> mkprim (loc, Number (NumTok.SMinus,n))
| None -> mknot (loc,ntn,l,bl) end
| (InConstrEntry,[Terminal x]), [] ->
begin match NumTok.Unsigned.parse_string x with
- | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
+ | Some n -> mkprim (loc, Number (NumTok.SPlus,n))
| None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
@@ -800,19 +800,21 @@ let extern_args extern env args =
let match_coercion_app c = match DAst.get c with
| GApp (r, args) ->
begin match DAst.get r with
- | GRef (r,_) -> Some (c.CAst.loc, r, 0, args)
+ | GRef (r,_) -> Some (c.CAst.loc, r, args)
| _ -> None
end
| _ -> None
let remove_one_coercion inctx c =
try match match_coercion_app c with
- | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
+ | Some (loc,r,args) when not (!Flags.raw_print || !print_coercions) ->
let nargs = List.length args in
(match Coercionops.hide_coercion r with
- | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+ | Some nparams when
+ let inctx = inctx || (* coercion to funclass implying being in context *) nparams+1 < nargs in
+ nparams < nargs && inctx ->
(* We skip the coercion *)
- let l = List.skipn (n - pars) args in
+ let l = List.skipn nparams args in
let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
(* Don't flatten App's in case of funclass so that
(atomic) notations on [a] work; should be compatible
@@ -824,7 +826,7 @@ let remove_one_coercion inctx c =
have been made explicit to match *)
let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
let inctx = inctx || not (List.is_empty l) in
- Some (n-pars+1, inctx, a')
+ Some (nparams+1, inctx, a')
| _ -> None)
| _ -> None
with Not_found ->
@@ -867,7 +869,7 @@ let filter_enough_applied nargs l =
| Some nargs ->
List.filter (fun (keyrule,pat,n as _rule) ->
match n with
- | AppBoundedNotation n -> n > nargs
+ | AppBoundedNotation n -> n >= nargs
| AppUnboundedNotation | NotAppNotation -> false) l
(* Helper function for safe and optimal printing of primitive tokens *)
@@ -915,28 +917,50 @@ let extern_float f scopes =
let hex = !Flags.raw_print || not (get_printing_float ()) in
if hex then Float64.to_hex_string f else Float64.to_string f in
let n = NumTok.Signed.of_string s in
- extern_prim_token_delimiter_if_required (Numeral n)
+ extern_prim_token_delimiter_if_required (Number n)
"float" "float_scope" scopes
(**********************************************************************)
(* mapping glob_constr to constr_expr *)
-let extern_glob_sort = function
+type extern_env = Id.Set.t * UnivNames.universe_binders
+let extern_env env sigma = vars_of_env env, Evd.universe_binders sigma
+let empty_extern_env = Id.Set.empty, Id.Map.empty
+
+let extern_glob_sort_name uvars = function
+ | GSProp -> CSProp
+ | GProp -> CProp
+ | GSet -> CSet
+ | GLocalUniv u -> CType (qualid_of_lident u)
+ | GRawUniv u -> CRawType u
+ | GUniv u -> begin match UnivNames.qualid_of_level uvars u with
+ | Some qid -> CType qid
+ | None -> CRawType u
+ end
+
+let extern_glob_sort uvars =
+ map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars)))
+
+(** wrapper to handle print_universes: don't forget small univs *)
+let extern_glob_sort uvars = function
(* In case we print a glob_constr w/o having passed through detyping *)
- | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+ | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> extern_glob_sort uvars u
| UNamed _ when not !print_universes -> UAnonymous {rigid=true}
- | UNamed _ | UAnonymous _ as u -> u
+ | UNamed _ | UAnonymous _ as u -> extern_glob_sort uvars u
-let extern_universes = function
- | Some _ as l when !print_universes -> l
+let extern_instance uvars = function
+ | Some l when !print_universes ->
+ Some (List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) l)
| _ -> None
-let extern_ref vars ref us =
+let extern_ref (vars,uvars) ref us =
extern_global (select_stronger_impargs (implicits_of_global ref))
- (extern_reference vars ref) (extern_universes us)
+ (extern_reference vars ref) (extern_instance uvars us)
let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
+let add_vname (vars,uvars) na = add_vname vars na, uvars
+
let rec extern inctx ?impargs scopes vars r =
match remove_one_coercion inctx (flatten_application r) with
| Some (nargs,inctx,r') ->
@@ -993,7 +1017,7 @@ let rec extern inctx ?impargs scopes vars r =
(* Otherwise... *)
extern_applied_ref inctx
(select_stronger_impargs (implicits_of_global ref))
- (ref,extern_reference ?loc vars ref) (extern_universes us) args)
+ (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args)
| _ ->
let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
let head = sub_extern false scopes vars f in
@@ -1013,7 +1037,8 @@ let rec extern inctx ?impargs scopes vars r =
| GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (Name.fold_right Id.Set.add)
- (cases_predicate_names tml) vars in
+ (cases_predicate_names tml) (fst vars) in
+ let vars' = vars', snd vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na, DAst.get tm with
@@ -1033,7 +1058,7 @@ let rec extern inctx ?impargs scopes vars r =
Option.map (fun {CAst.loc;v=(ind,nal)} ->
let args = List.map (fun x -> DAst.make @@ PatVar x) nal in
let fullargs = add_cpatt_for_params ind args in
- extern_ind_pattern_in_scope scopes vars ind fullargs
+ extern_ind_pattern_in_scope scopes (fst vars) ind fullargs
) x))
tml
in
@@ -1056,7 +1081,7 @@ let rec extern inctx ?impargs scopes vars r =
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
| GRec (fk,idv,blv,tyv,bv) ->
- let vars' = Array.fold_right Id.Set.add idv vars in
+ let vars' = on_fst (Array.fold_right Id.Set.add idv) vars in
(match fk with
| GFix (nv,n) ->
let listdecl =
@@ -1064,8 +1089,8 @@ let rec extern inctx ?impargs scopes vars r =
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
- let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
- let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
+ let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in
+ let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in
let n =
match nv.(i) with
| None -> None
@@ -1080,14 +1105,14 @@ let rec extern inctx ?impargs scopes vars r =
Array.mapi (fun i fi ->
let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
let (_,ids,bl) = extern_local_binder scopes vars bl in
- let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
- let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
+ let vars0 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars in
+ let vars1 = on_fst (List.fold_right (Name.fold_right Id.Set.add) ids) vars' in
((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern true scopes vars1 bv.(i))) idv
in
CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
- | GSort s -> CSort (extern_glob_sort s)
+ | GSort s -> CSort (extern_glob_sort (snd vars) s)
| GHole (e,naming,_) -> CHole (Some e, naming, None) (* TODO: extern tactics. *)
@@ -1097,13 +1122,13 @@ let rec extern inctx ?impargs scopes vars r =
| GInt i ->
extern_prim_token_delimiter_if_required
- (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i)))
+ (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
"int63" "int63_scope" (snd scopes)
| GFloat f -> extern_float f (snd scopes)
| GArray(u,t,def,ty) ->
- CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
+ CArray(extern_instance (snd vars) u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
in insert_entry_coercion coercion (CAst.make ?loc c)
@@ -1125,8 +1150,8 @@ and factorize_prod ?impargs scopes vars na bk t c =
let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = extern_typ scopes vars b in
- let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+ let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in
+ let binder = CLocalPattern p in
(match b.v with
| CProdN (bl,b) -> CProdN (binder::bl,b)
| _ -> CProdN ([binder],b))
@@ -1166,8 +1191,8 @@ and factorize_lambda inctx scopes vars na bk t c =
let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
let b = sub_extern inctx scopes vars b in
- let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in
- let binder = CLocalPattern (make ?loc:c.loc (p,None)) in
+ let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes (fst vars)) disjpat) in
+ let binder = CLocalPattern p in
(match b.v with
| CLambdaN (bl,b) -> CLambdaN (binder::bl,b)
| _ -> CLambdaN ([binder],b))
@@ -1194,7 +1219,7 @@ and extern_local_binder scopes vars = function
match DAst.get b with
| GLocalDef (na,bk,bd,ty) ->
let (assums,ids,l) =
- extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
+ extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in
(assums,na::ids,
CLocalDef(CAst.make na, extern false scopes vars bd,
Option.map (extern_typ scopes vars) ty) :: l)
@@ -1202,7 +1227,7 @@ and extern_local_binder scopes vars = function
| GLocalAssum (na,bk,ty) ->
let implicit_type = is_reserved_type na ty in
let ty = extern_typ scopes vars ty in
- (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
+ (match extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
when (constr_expr_eq ty ty' || implicit_type && constr_expr_eq ty' hole) &&
match na with Name id -> not (occur_var_constr_expr id ty')
@@ -1217,12 +1242,15 @@ and extern_local_binder scopes vars = function
| GLocalPattern ((p,_),_,bk,ty) ->
let ty =
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
- let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in
+ let p = mkCPatOr (List.map (extern_cases_pattern (fst vars)) p) in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
+ let p = match ty with
+ | None -> p
+ | Some ty -> CAst.make @@ (CPatCast (p,ty)) in
+ (assums,ids, CLocalPattern p :: l)
and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
- let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
+ let pll = List.map (List.map (extern_cases_pattern_in_scope scopes (fst vars))) pll in
make ?loc (pll,extern inctx scopes vars c)
and extern_notations inctx scopes vars nargs t =
@@ -1272,8 +1300,9 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
end
| AppBoundedNotation _ -> raise No_match in
(* Try matching ... *)
+ let vars, uvars = vars in
let terms,termlists,binders,binderlists =
- match_notation_constr !print_universes t pat in
+ match_notation_constr ~print_univ:(!print_universes) t ~vars pat in
(* Try availability of interpretation ... *)
match keyrule with
| NotationRule (_,ntn as specific_ntn) ->
@@ -1293,36 +1322,45 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
| Some (scopt,key) ->
let scopes' = Option.List.cons scopt (snd scopes) in
let l =
- List.map (fun (c,(subentry,(scopt,scl))) ->
+ List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
extern (* assuming no overloading: *) true
- (subentry,(scopt,scl@scopes')) vars c)
- terms in
+ (subentry,(scopt,scl@scopes')) (vars,uvars) c)
+ terms
+ in
let ll =
- List.map (fun (c,(subentry,(scopt,scl))) ->
- List.map (extern true (subentry,(scopt,scl@scopes')) vars) c)
- termlists in
+ List.map (fun ((vars,l),(subentry,(scopt,scl))) ->
+ List.map (extern true (subentry,(scopt,scl@scopes')) (vars,uvars)) l)
+ termlists
+ in
let bl =
- List.map (fun (bl,(subentry,(scopt,scl))) ->
- mkCPatOr (List.map (extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes')) vars) bl))
- binders in
+ List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
+ (mkCPatOr (List.map
+ (extern_cases_pattern_in_scope
+ (subentry,(scopt,scl@scopes')) vars)
+ bl)),
+ Explicit)
+ binders
+ in
let bll =
- List.map (fun (bl,(subentry,(scopt,scl))) ->
- pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl))
- binderlists in
+ List.map (fun ((vars,bl),(subentry,(scopt,scl))) ->
+ pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) (vars,uvars) bl))
+ binderlists
+ in
let c = make_notation loc specific_ntn (l,ll,bl,bll) in
let c = insert_entry_coercion coercion (insert_delimiters c key) in
let args = fill_arg_scopes args argsscopes allscopes in
- let args = extern_args (extern true) vars args in
+ let args = extern_args (extern true) (vars,uvars) args in
CAst.make ?loc @@ extern_applied_notation inctx nallargs argsimpls c args)
| SynDefRule kn ->
let l =
- List.map (fun (c,(subentry,(scopt,scl))) ->
- extern true (subentry,(scopt,scl@snd scopes)) vars c)
- terms in
+ List.map (fun ((vars,c),(subentry,(scopt,scl))) ->
+ extern true (subentry,(scopt,scl@snd scopes)) (vars,uvars) c)
+ terms
+ in
let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
let a = CRef (cf,None) in
let args = fill_arg_scopes args argsscopes allscopes in
- let args = extern_args (extern true) vars args in
+ let args = extern_args (extern true) (vars,uvars) args in
let c = CAst.make ?loc @@ extern_applied_syntactic_definition inctx nallargs argsimpls (a,cf) l args in
if isCRef_no_univ c.CAst.v && entry_has_global custom then c
else match availability_of_entry_coercion custom InConstrEntrySomeLevel with
@@ -1342,7 +1380,7 @@ let extern_glob_type ?impargs vars c =
let extern_constr ?lax ?(inctx=false) ?scope env sigma t =
let r = Detyping.detype Detyping.Later ?lax false Id.Set.empty env sigma t in
- let vars = vars_of_env env in
+ let vars = extern_env env sigma in
extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
let extern_constr_in_scope ?lax ?inctx scope env sigma t =
@@ -1358,16 +1396,16 @@ let extern_type ?lax ?(goal_concl_style=false) env sigma ?impargs t =
(* consideration; see namegen.ml for further details *)
let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r = Detyping.detype Detyping.Later ?lax goal_concl_style avoid env sigma t in
- extern_glob_type ?impargs (vars_of_env env) r
+ extern_glob_type ?impargs (extern_env env sigma) r
-let extern_sort sigma s = extern_glob_sort (detype_sort sigma s)
+let extern_sort sigma s = extern_glob_sort (Evd.universe_binders sigma) (detype_sort sigma s)
let extern_closed_glob ?lax ?(goal_concl_style=false) ?(inctx=false) ?scope env sigma t =
let avoid = if goal_concl_style then vars_of_env env else Id.Set.empty in
let r =
Detyping.detype_closed_glob ?lax goal_concl_style avoid env sigma t
in
- let vars = vars_of_env env in
+ let vars = extern_env env sigma in
extern inctx (InConstrEntrySomeLevel,(scope,[])) vars r
(******************************************************************)
@@ -1485,10 +1523,13 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
let extern_constr_pattern env sigma pat =
- extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
+ extern true (InConstrEntrySomeLevel,(None,[]))
+ (* XXX no vars? *)
+ (Id.Set.empty, Evd.universe_binders sigma)
+ (glob_of_pat Id.Set.empty env sigma pat)
let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
- let vars = vars_of_env env in
+ let vars = extern_env env sigma in
let a = List.map (extended_glob_local_binder_of_decl) a in
pi3 (extern_local_binder (InConstrEntrySomeLevel,(None,[])) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index f85e49d2df..298b52f0be 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -23,9 +23,12 @@ open Ltac_pretype
(** Translation of pattern, cases pattern, glob_constr and term into syntax
trees for printing *)
+type extern_env = Id.Set.t * UnivNames.universe_binders
+val extern_env : env -> Evd.evar_map -> extern_env
+
val extern_cases_pattern : Id.Set.t -> 'a cases_pattern_g -> cases_pattern_expr
-val extern_glob_constr : Id.Set.t -> 'a glob_constr_g -> constr_expr
-val extern_glob_type : ?impargs:Glob_term.binding_kind list -> Id.Set.t -> 'a glob_constr_g -> constr_expr
+val extern_glob_constr : extern_env -> 'a glob_constr_g -> constr_expr
+val extern_glob_type : ?impargs:Glob_term.binding_kind list -> extern_env -> 'a glob_constr_g -> constr_expr
val extern_constr_pattern : names_context -> Evd.evar_map ->
constr_pattern -> constr_expr
val extern_closed_glob : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool -> ?scope:scope_name ->
@@ -43,7 +46,7 @@ val extern_constr_in_scope : ?lax:bool -> ?inctx:bool -> scope_name ->
env -> Evd.evar_map -> constr -> constr_expr
val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
val extern_type : ?lax:bool -> ?goal_concl_style:bool -> env -> Evd.evar_map -> ?impargs:Glob_term.binding_kind list -> types -> constr_expr
-val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
+val extern_sort : Evd.evar_map -> Sorts.t -> sort_expr
val extern_rel_context : constr option -> env -> Evd.evar_map ->
rel_context -> local_binder_expr list
@@ -96,3 +99,6 @@ val toggle_scope_printing :
val toggle_notation_printing :
?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
+
+(** Probably shouldn't be used *)
+val empty_extern_env : extern_env
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 959b61a3d7..cf2f333596 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -254,15 +254,25 @@ let contract_curly_brackets_pat ntn (l,ll) =
(* side effect; don't inline *)
(InConstrEntry,!ntn'),(l,ll)
+type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool }
+
type intern_env = {
- ids: Names.Id.Set.t;
+ ids: Id.Set.t;
unb: bool;
+ local_univs: local_univs;
tmp_scope: Notation_term.tmp_scope_name option;
scopes: Notation_term.scope_name list;
impls: internalization_env;
binder_block_names: (abstraction_kind option (* None = unknown *) * Id.Set.t) option;
}
+type pattern_intern_env = {
+ pat_scopes: Notation_term.subscopes;
+ (* ids = Some means accept local variables; this is useful for
+ terms as patterns parsed as pattersn in notations *)
+ pat_ids: Id.Set.t option;
+}
+
(**********************************************************************)
(* Remembering the parsing scope of variables in notations *)
@@ -291,21 +301,20 @@ let error_expect_binder_notation_type ?loc id =
let set_var_scope ?loc id istermvar (tmp_scope,subscopes as scopes) ntnvars =
try
let used_as_binder,idscopes,typ = Id.Map.find id ntnvars in
- if not istermvar then used_as_binder := true;
- let () = if istermvar then
+ if istermvar then begin
(* scopes have no effect on the interpretation of identifiers *)
- begin match !idscopes with
+ (match !idscopes with
| None -> idscopes := Some scopes
| Some (tmp_scope', subscopes') ->
let s' = make_current_scope tmp_scope' subscopes' in
let s = make_current_scope tmp_scope subscopes in
- if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s
+ if not (List.equal String.equal s' s) then error_inconsistent_scope ?loc id s' s);
+ (match typ with
+ | Notation_term.NtnInternTypeOnlyBinder -> error_expect_binder_notation_type ?loc id
+ | Notation_term.NtnInternTypeAny -> ())
end
- in
- match typ with
- | Notation_term.NtnInternTypeOnlyBinder ->
- if istermvar then error_expect_binder_notation_type ?loc id
- | Notation_term.NtnInternTypeAny -> ()
+ else
+ used_as_binder := true
with Not_found ->
(* Not in a notation *)
()
@@ -317,6 +326,9 @@ let reset_tmp_scope env = {env with tmp_scope = None}
let set_env_scopes env (scopt,subscopes) =
{env with tmp_scope = scopt; scopes = subscopes @ env.scopes}
+let env_for_pattern env =
+ {pat_scopes = (env.tmp_scope, env.scopes); pat_ids = Some env.ids}
+
let mkGProd ?loc (na,bk,t) body = DAst.make ?loc @@ GProd (na, bk, t, body)
let mkGLambda ?loc (na,bk,t) body = DAst.make ?loc @@ GLambda (na, bk, t, body)
@@ -420,6 +432,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
@@ -490,15 +536,19 @@ let intern_generalized_binder intern_type ntnvars
in
let na = match na with
| Anonymous ->
- let name =
- let id =
- match ty with
- | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
- qualid_basename qid
- | _ -> default_non_dependent_ident
- in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
- in Name name
- | _ -> na in
+ let id =
+ match ty with
+ | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid ->
+ qualid_basename qid
+ | _ -> default_non_dependent_ident
+ in
+ let ids' = List.fold_left (fun ids' lid -> Id.Set.add lid.CAst.v ids') ids' fvs in
+ let id =
+ Implicit_quantifiers.make_fresh ids' (Global.env ()) id
+ in
+ Name id
+ | _ -> na
+ in
let impls = impls_type_list 1 ty' in
(push_name_env ntnvars impls env' (make ?loc na),
(make ?loc (na,b',ty')) :: List.rev bl)
@@ -539,20 +589,28 @@ 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 intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) =
+ let p,t = match p with
+ | CPatCast (p, t) -> (p, Some t)
+ | _ -> (pv, None) in
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 (env_for_pattern (reset_tmp_scope env)) 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.");
il,disjpat
in
- let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
let na = alias_of_pat (List.hd disjpat) in
+ let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars [] env (make ?loc @@ Name id)) il env in
let ienv = Name.fold_right Id.Set.remove na env.ids in
let id = Namegen.next_name_away_with_default "pat" na ienv in
let na = make ?loc @@ Name id in
- env,((disjpat,il),id),na
+ let t = match t with
+ | Some t -> t
+ | None -> CAst.make ?loc @@ CHole(Some (Evar_kinds.BinderType na.v),IntroAnonymous,None) in
+ let _, bl' = intern_assumption intern ntnvars env [na] (Default bk) t in
+ let {v=(_,bk,t)} = List.hd bl' in
+ env,((disjpat,il),id),na,bk,t
let intern_local_binder_aux intern ntnvars (env,bl) = function
| CLocalAssum(nal,bk,ty) ->
@@ -562,17 +620,9 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function
| CLocalDef( {loc; v=na} as locna,def,ty) ->
let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in
env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl
- | CLocalPattern {loc;v=(p,ty)} ->
- let tyc =
- match ty with
- | 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 bk = Default Explicit in
- let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
- let {v=(_,bk,t)} = List.hd bl' in
- (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
+ | CLocalPattern p ->
+ let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in
+ (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl)
let intern_generalization intern env ntnvars loc bk ak c =
let c = intern {env with unb = true} c in
@@ -658,52 +708,66 @@ let is_patvar c =
let is_patvar_store store pat =
match DAst.get pat with
- | PatVar na -> ignore(store na); true
+ | PatVar na -> ignore(store (CAst.make ?loc:pat.loc 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))
-
-let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) = function
- | Anonymous -> (renaming,env), None, Anonymous
+ | _ -> assert false)
+
+let canonize_type = function
+ | None -> None
+ | Some t as t' ->
+ match DAst.get t with
+ | GHole (Evar_kinds.BinderType _,IntroAnonymous,None) -> None
+ | _ -> t'
+
+let set_type ty1 ty2 =
+ match canonize_type ty1, canonize_type ty2 with
+ (* Not a meta-binding binder, we use the type given in the notation *)
+ | _, None -> ty1
+ (* A meta-binding binder meta-bound to a possibly-typed pattern *)
+ (* the binder is supposed to come w/o an explicit type in the notation *)
+ | None, Some _ -> ty2
+ | Some ty1, Some t2 ->
+ (* An explicitly typed meta-binding binder, not supposed to be a pattern; checked in interp_notation *)
+ user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.")
+
+let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty =
+ match na with
+ | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
| 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,bk,t = intern_pat test_kind ntnvars env Explicit 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
- (renaming,env), pat, na
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+ (renaming,env), pat, na.v, bk, set_type ty (Some t)
with Not_found ->
try
(* Trying to associate a pattern *)
- let pat,(onlyident,scopes) = Id.Map.find id binders in
+ let (pat,bk),(onlyident,scopes) = Id.Map.find id binders in
let env = set_env_scopes env scopes in
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
+ let ty' = DAst.make @@ GHole (Evar_kinds.BinderType na.CAst.v,IntroAnonymous,None) in
+ (renaming,env), None, na.v, bk, set_type ty (Some ty')
else
(* Interpret as a pattern *)
- let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
+ let env,((disjpat,ids),id),na,bk,t = intern_pat test_kind ntnvars env bk 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
- (renaming,env), pat, na
+ | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na in
+ (renaming,env), pat, na.v, bk, set_type ty (Some t)
with Not_found ->
(* Binders not bound in the notation do not capture variables *)
(* outside the notation (i.e. in the substitution) *)
@@ -711,7 +775,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
let renaming' =
if Id.equal id id' then renaming else Id.Map.add id id' renaming
in
- (renaming',env), None, Name id'
+ (renaming',env), None, Name id', Explicit, set_type ty None
type binder_action =
| AddLetIn of lname * constr_expr * constr_expr option
@@ -829,22 +893,23 @@ 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 mk_env' ((c,_bk), (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 test_kind =
+ if onlyident then test_kind_ident_in_notation
+ else test_kind_pattern_in_notation in
+ let _,((disjpat,_),_),_,_,_ty = intern_pat test_kind ntnvars nenv Explicit c in
+ (* TODO: use cast? *)
+ 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
@@ -866,44 +931,33 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var)
with Not_found ->
anomaly (Pp.str "Inconsistent substitution of recursive notation."))
- | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
+ | NProd (Name id, None, c') when option_mem_assoc id binderopt ->
let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c')
- | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
+ | NLambda (Name id, None, c') when option_mem_assoc id binderopt ->
let binder = snd (Option.get binderopt) in
expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c')
- (* Two special cases to keep binder name synchronous with BinderType *)
- | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
- when Name.equal na na' ->
- let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
- let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- DAst.make ?loc @@ GProd (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
- | NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
- when Name.equal na na' ->
- let subinfos,disjpat,na = traverse_binder intern_pat ntnvars subst avoid subinfos na in
- let ty = DAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- DAst.make ?loc @@ GLambda (na,Explicit,ty,Option.fold_right apply_cases_pattern disjpat (aux subst' subinfos c'))
| t ->
glob_constr_of_notation_constr_with_binders ?loc
- (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
+ (traverse_binder intern_pat ntnvars subst avoid) (aux subst') ~h:binder_status_fun subinfos t
and subst_var (terms, binderopt, _terminopt) (renaming, env) id =
(* 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 (pat,bk),(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 test_kind =
+ if onlyident then test_kind_ident_in_notation
+ else test_kind_pattern_in_notation in
+ let env,((disjpat,ids),id),na,bk,_ty = intern_pat test_kind ntnvars env bk pat in
+ (* TODO: use cast? *)
+ 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
@@ -925,6 +979,9 @@ 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_id {loc;v=id} =
+ CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+
let cases_pattern_of_name {loc;v=na} =
let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
CAst.make ?loc (CPatAtom atom)
@@ -940,16 +997,20 @@ 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 NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
+ | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | 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
+ let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
- let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
+ let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ as x) ->
- let onlyident = (x = NtnParsedAsIdent) in
+ | NtnTypeBinder NtnBinderParsedAsConstr AsName ->
+ let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+ let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
+ (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
+ let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in
let binders,binders' = bind id (onlyident,scl) binders binders' in
(terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
| NtnTypeConstrList ->
@@ -990,7 +1051,7 @@ let intern_notation intern env ntnvars loc ntn fullargs =
(* Dispatch parsing substitution to an interpretation substitution *)
let subst = split_by_type ids fullargs in
(* Instantiate the notation *)
- instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst (Id.Map.empty, env) c
+ instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst (Id.Map.empty, env) c
(**********************************************************************)
(* Discriminating between bound variables and global references *)
@@ -1102,6 +1163,32 @@ let glob_sort_of_level (level: glob_level) : glob_sort =
| UAnonymous {rigid} -> UAnonymous {rigid}
| UNamed id -> UNamed [id,0]
+let intern_sort_name ~local_univs = function
+ | CSProp -> GSProp
+ | CProp -> GProp
+ | CSet -> GSet
+ | CRawType u -> GRawUniv u
+ | CType qid ->
+ let is_id = qualid_is_ident qid in
+ let local = if not is_id then None
+ else Id.Map.find_opt (qualid_basename qid) local_univs.bound
+ in
+ match local with
+ | Some u -> GUniv u
+ | None ->
+ try GUniv (Univ.Level.make (Nametab.locate_universe qid))
+ with Not_found ->
+ if is_id && local_univs.unb_univs
+ then GLocalUniv (CAst.make ?loc:qid.loc (qualid_basename qid))
+ else
+ CErrors.user_err Pp.(str "Undeclared universe " ++ pr_qualid qid ++ str".")
+
+let intern_sort ~local_univs s =
+ map_glob_sort_gen (List.map (on_fst (intern_sort_name ~local_univs))) s
+
+let intern_instance ~local_univs us =
+ Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
+
(* Is it a global reference or a syntactic definition? *)
let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
let loc = qid.loc in
@@ -1118,7 +1205,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
check_no_explicitation args1;
let subst = split_by_type ids (List.map fst args1,[],[],[]) in
let infos = (Id.Map.empty, env) in
- let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
+ let c = instantiate_notation_constr loc intern (intern_cases_pattern_as_binder intern) ntnvars subst infos c in
let loc = c.loc in
let err () =
user_err ?loc (str "Notation " ++ pr_qualid qid
@@ -1167,6 +1254,7 @@ let check_applied_projection isproj realref qid =
let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid =
let loc = qid.CAst.loc in
+ let us = intern_instance ~local_univs:env.local_univs us in
if qualid_is_ident qid then
try
let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
@@ -1198,7 +1286,8 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
let interp_reference vars r =
let (r,_,_),_ =
intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
- {ids = Id.Set.empty; unb = false ;
+ {ids = Id.Set.empty; unb = false;
+ local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *)
tmp_scope = None; scopes = []; impls = empty_internalization_env;
binder_block_names = None}
Environ.empty_named_context_val
@@ -1570,11 +1659,11 @@ let rec subst_pat_iterator y t = DAst.(map (function
| RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
let is_non_zero c = match c with
-| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p)
| _ -> false
let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p)
| _ -> false
let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
@@ -1582,19 +1671,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 env pat =
(* 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,47 +1695,49 @@ 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
+ if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then
+ raise Not_found;
match Nametab.locate_extended qid with
| SynDef sp ->
let filter (vars,a) =
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 +1754,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 +1768,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 (Numeral (_, p)) -> p | _ -> assert false in
- let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
+ 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 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
+ let subst = 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 subst 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 +1811,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 +1820,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 +1849,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 +1861,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 env.pat_scopes pat
let rec intern_pat genv ntnvars aliases pat =
let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
@@ -1816,19 +1902,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 env 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 env pat)
let _ =
intern_cases_pattern_fwd :=
- fun ntnvars scopes p -> intern_cases_pattern (Global.env ()) ntnvars scopes empty_alias p
-
-let intern_ind_pattern genv ntnvars scopes pat =
+ fun test_kind ntnvars env p ->
+ intern_cases_pattern test_kind (Global.env ()) ntnvars env empty_alias p
+
+let intern_ind_pattern genv ntnvars env 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 env pat
+ with InternalizationError (NotAConstructor _) as exn ->
let _, info = Exninfo.capture exn in
error_bad_inductive_type ~info ()
in
@@ -1927,9 +2024,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let env = restart_lambda_binders env in
let idl_temp = Array.map
(fun (id,recarg,bl,ty,_) ->
- let recarg = Option.map (function { CAst.v = v } -> match v with
+ let recarg = Option.map (function { CAst.v = v; loc } -> match v with
| CStructRec i -> i
- | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+ | _ -> user_err ?loc Pp.(str "Well-founded induction requires Program Fixpoint or Function.")) recarg
in
let before, after = split_at_annot bl recarg in
let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
@@ -2006,8 +2103,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GLetIn (na.CAst.v, inc1, int,
intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
| CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
- let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
- intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
+ let p = match a.CAst.v with CPrim (Number (_, p)) -> p | _ -> assert false in
+ intern env (CAst.make ?loc @@ CPrim (Number (SMinus,p)))
| CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (_,ntn,args) ->
let c = intern_notation intern env ntnvars loc ntn args in
@@ -2047,9 +2144,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ntnargs in
find_appl_head_data c, args
- | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[]), args in
- apply_impargs c env impargs args_scopes
- args loc
+ | _ ->
+ assert (Option.is_empty isproj);
+ let f = intern_no_implicit env f in
+ let f, _, args_scopes = find_appl_head_data f in
+ (f,[],args_scopes), args
+ in
+ apply_impargs c env impargs args_scopes args loc
| CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -2199,12 +2300,12 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
(* end *)
| CSort s ->
DAst.make ?loc @@
- GSort s
+ GSort (intern_sort ~local_univs:env.local_univs s)
| CCast (c1, c2) ->
DAst.make ?loc @@
GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2)
| CArray(u,t,def,ty) ->
- DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty)
+ DAst.make ?loc @@ GArray(intern_instance ~local_univs:env.local_univs u, Array.map (intern env) t, intern env def, intern env ty)
)
and intern_type env = intern (set_type_scope env)
@@ -2221,7 +2322,8 @@ 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 env = { pat_ids = None; pat_scopes = (None,env.scopes) } in
+ let idsl_pll = List.map (intern_cases_pattern test_kind_tolerant globalenv ntnvars env 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
@@ -2262,7 +2364,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let match_td,typ = match t with
| Some t ->
let with_letin,(ind,ind_ids,alias_subst,l) =
- intern_ind_pattern globalenv ntnvars (None,env.scopes) t in
+ intern_ind_pattern globalenv ntnvars (env_for_pattern (set_type_scope env)) t in
let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
(* for "in Vect n", we answer (["n","n"],[(loc,"n")])
@@ -2359,8 +2461,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
and intern_args env subscopes = function
| [] -> []
| a::args ->
- let (enva,subscopes) = apply_scope_env env subscopes in
- (intern_no_implicit enva a) :: (intern_args env subscopes args)
+ let (enva,subscopes) = apply_scope_env env subscopes in
+ let a = intern_no_implicit enva a in
+ a :: (intern_args env subscopes args)
in
intern env c
@@ -2374,6 +2477,8 @@ let extract_ids env =
(Termops.ids_of_rel_context (Environ.rel_context env))
Id.Set.empty
+let bound_univs sigma = Evd.universe_binders sigma
+
let scope_of_type_kind env sigma = function
| IsType -> Notation.current_type_scope_name ()
| OfType typ -> compute_type_scope env sigma typ
@@ -2396,14 +2501,16 @@ let intern_gen kind env sigma
let tmp_scope = scope_of_type_kind env sigma kind in
let k = allowed_binder_kind_of_type_kind kind in
internalize env {ids = extract_ids env; unb = false;
- tmp_scope = tmp_scope; scopes = [];
- impls; binder_block_names = Some (k,Id.Map.domain impls)}
+ local_univs = { bound = bound_univs sigma; unb_univs = true };
+ tmp_scope = tmp_scope; scopes = [];
+ impls; binder_block_names = Some (k,Id.Map.domain impls)}
pattern_mode (ltacvars, Id.Map.empty) c
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
+ let env = {pat_ids = None; pat_scopes = (None, [])} in
+ intern_cases_pattern test_kind_tolerant globalenv Id.Map.empty env empty_alias patt
(*********************************************************************)
(* Functions to parse and interpret constructions *)
@@ -2471,13 +2578,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign)
~pattern_mode:true ~ltacvars env sigma c in
pattern_of_glob_constr c
+let interp_constr_pattern env sigma ?(expected_type=WithoutTypeConstraint) c =
+ let c = intern_gen expected_type ~pattern_mode:true env sigma c in
+ let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
+ let sigma, c = understand_tcc ~flags env sigma ~expected_type c in
+ (* FIXME: it is necessary to be unsafe here because of the way we handle
+ evars in the pretyper. Sometimes they get solved eagerly. *)
+ pattern_of_constr env sigma (EConstr.Unsafe.to_constr c)
+
let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
{ Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c =
let tmp_scope = scope_of_type_kind env sigma kind in
let impls = empty_internalization_env in
let k = allowed_binder_kind_of_type_kind kind in
internalize env
- {ids; unb = false; tmp_scope; scopes = []; impls;
+ {ids; unb = false;
+ local_univs = { bound = bound_univs sigma; unb_univs = true };
+ tmp_scope; scopes = []; impls;
binder_block_names = Some (k,Id.Set.empty)}
pattern_mode (ltacvars, vl) c
@@ -2487,8 +2604,11 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in
let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in
let c = internalize env
- {ids; unb = false; tmp_scope = None; scopes = []; impls; binder_block_names = None}
- false (empty_ltac_sign, vl) a in
+ {ids; unb = false;
+ local_univs = { bound = Id.Map.empty; unb_univs = false };
+ tmp_scope = None; scopes = []; impls; binder_block_names = None}
+ false (empty_ltac_sign, vl) a
+ in
(* Splits variables into those that are binding, bound, or both *)
(* Translate and check that [c] has all its free variables bound in [vars] *)
let a, reversible = notation_constr_of_glob_constr nenv c in
@@ -2515,7 +2635,7 @@ let interp_binder_evars env sigma na t =
let my_intern_constr env lvar acc c =
internalize env acc false lvar c
-let intern_context env impl_env binders =
+let intern_context env ~bound_univs impl_env binders =
let lvar = (empty_ltac_sign, Id.Map.empty) in
let ids =
(* We assume all ids around are parts of the prefix of the current
@@ -2526,6 +2646,7 @@ let intern_context env impl_env binders =
let (env, bl) = intern_local_binder_aux (my_intern_constr env lvar) Id.Map.empty (lenv, bl) b in
(env, bl))
({ids; unb = false;
+ local_univs = { bound = bound_univs; unb_univs = true };
tmp_scope = None; scopes = []; impls = impl_env;
binder_block_names = Some (Some AbsPi,ids)}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
@@ -2562,6 +2683,65 @@ let interp_glob_context_evars ?(program_mode=false) env sigma bl =
sigma, ((env, par), List.rev impls)
let interp_context_evars ?program_mode ?(impl_env=empty_internalization_env) env sigma params =
- let int_env,bl = intern_context env impl_env params in
+ let int_env,bl = intern_context env ~bound_univs:(bound_univs sigma) impl_env params in
let sigma, x = interp_glob_context_evars ?program_mode env sigma bl in
sigma, (int_env, x)
+
+
+(** Local universe and constraint declarations. *)
+
+let interp_known_level evd u =
+ let u = intern_sort_name ~local_univs:{bound = bound_univs evd; unb_univs=false} u in
+ Pretyping.known_glob_level evd u
+
+let interp_univ_constraints env evd cstrs =
+ let interp (evd,cstrs) (u, d, u') =
+ let ul = interp_known_level evd u in
+ let u'l = interp_known_level evd u' in
+ let cstr = (ul,d,u'l) in
+ let cstrs' = Univ.Constraint.add cstr cstrs in
+ try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+ evd, cstrs'
+ with Univ.UniverseInconsistency e as exn ->
+ let _, info = Exninfo.capture exn in
+ CErrors.user_err ~hdr:"interp_constraint" ~info
+ (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+ in
+ List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+ let open UState in
+ let binders : lident list = decl.univdecl_instance in
+ let evd = Evd.from_env ~binders env in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = {
+ univdecl_instance = binders;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+ }
+ in evd, decl
+
+let interp_cumul_univ_decl env decl =
+ let open UState in
+ let binders = List.map fst decl.univdecl_instance in
+ let variances = Array.map_of_list snd decl.univdecl_instance in
+ let evd = Evd.from_ctx (UState.from_env ~binders env) in
+ let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+ let decl = {
+ univdecl_instance = binders;
+ univdecl_extensible_instance = decl.univdecl_extensible_instance;
+ univdecl_constraints = cstrs;
+ univdecl_extensible_constraints = decl.univdecl_extensible_constraints;
+ }
+ in
+ evd, decl, variances
+
+let interp_univ_decl_opt env l =
+ match l with
+ | None -> Evd.from_env env, UState.default_univ_decl
+ | Some decl -> interp_univ_decl env decl
+
+let interp_cumul_univ_decl_opt env = function
+ | None -> Evd.from_env env, UState.default_univ_decl, [| |]
+ | Some decl -> interp_cumul_univ_decl env decl
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 898a3e09c8..f92a54e23f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -88,7 +88,8 @@ val intern_gen : typing_constraint -> env -> evar_map ->
val intern_pattern : env -> cases_pattern_expr ->
lident list * (Id.t Id.Map.t * cases_pattern) list
-val intern_context : env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
+val intern_context : env -> bound_univs:UnivNames.universe_binders ->
+ internalization_env -> local_binder_expr list -> internalization_env * glob_decl list
(** {6 Composing internalization with type inference (pretyping) } *)
@@ -136,10 +137,16 @@ val interp_type_evars_impls : ?flags:inference_flags -> env -> evar_map ->
(** Interprets constr patterns *)
+(** Without typing *)
val intern_constr_pattern :
env -> evar_map -> ?as_type:bool -> ?ltacvars:ltac_sign ->
constr_pattern_expr -> patvar list * constr_pattern
+(** With typing *)
+val interp_constr_pattern :
+ env -> evar_map -> ?expected_type:typing_constraint ->
+ constr_pattern_expr -> constr_pattern
+
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
val intern_reference : qualid -> GlobRef.t
@@ -191,3 +198,17 @@ val get_asymmetric_patterns : unit -> bool
val check_duplicate : ?loc:Loc.t -> (qualid * constr_expr) list -> unit
(** Check that a list of record field definitions doesn't contain
duplicates. *)
+
+val interp_known_level : Evd.evar_map -> sort_name_expr -> Univ.Level.t
+
+(** Local universe and constraint declarations. *)
+val interp_univ_decl : Environ.env -> universe_decl_expr ->
+ Evd.evar_map * UState.universe_decl
+
+val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
+ Evd.evar_map * UState.universe_decl
+
+val interp_cumul_univ_decl_opt : Environ.env -> cumul_univ_decl_expr option ->
+ Evd.evar_map * UState.universe_decl * Entries.variance_entry
+(** BEWARE the variance entry needs to be adjusted by
+ [ComInductive.variance_of_entry] if the instance is extensible. *)
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index d57c05788d..3ec92cf691 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -26,19 +26,29 @@ type glob_output =
| MultFiles
| File of string
-let glob_output = ref NoGlob
+let glob_output = ref []
-let dump () = !glob_output <> NoGlob
+let get_output () = match !glob_output with
+ | [] -> NoGlob
+ | g::_ -> g
-let set_glob_output mode =
- glob_output := mode
+let push_output g = glob_output := g::!glob_output
+
+let pop_output () = glob_output := match !glob_output with
+ | [] -> CErrors.anomaly (Pp.str "No output left to pop")
+ | _::ds -> ds
+
+let pause () = push_output NoGlob
+let continue = pop_output
+
+let dump () = get_output () <> NoGlob
let dump_string s =
- if dump () && !glob_output != Feedback then
+ if dump () && get_output () != Feedback then
output_string !glob_file s
let start_dump_glob ~vfile ~vofile =
- match !glob_output with
+ match get_output () with
| MultFiles ->
open_glob_file (Filename.chop_extension vofile ^ ".glob");
output_string !glob_file "DIGEST ";
@@ -51,14 +61,10 @@ let start_dump_glob ~vfile ~vofile =
()
let end_dump_glob () =
- match !glob_output with
+ match get_output () with
| MultFiles | File _ -> close_glob_file ()
| NoGlob | Feedback -> ()
-let previous_state = ref MultFiles
-let pause () = previous_state := !glob_output; glob_output := NoGlob
-let continue () = glob_output := !previous_state
-
open Decls
open Declarations
@@ -141,7 +147,7 @@ let interval loc =
loc1, loc2-1
let dump_ref ?loc filepath modpath ident ty =
- match !glob_output with
+ match get_output () with
| Feedback ->
Option.iter (fun loc ->
Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
@@ -247,7 +253,7 @@ let add_glob_kn ?loc kn =
add_glob_gen ?loc sp lib_dp "syndef"
let dump_def ?loc ty secpath id = Option.iter (fun loc ->
- if !glob_output = Feedback then
+ if get_output () = Feedback then
Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
else
let bl,el = interval loc in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index be1e3f05d2..857991cb3f 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -19,11 +19,19 @@ type glob_output =
| MultFiles (* one glob file per .v file *)
| File of string (* Single file for all coqc arguments *)
-(* Default "NoGlob" *)
-val set_glob_output : glob_output -> unit
+(** [push_output o] temporarily overrides the output location to [o].
+ The original output can be restored using [pop_output] *)
+val push_output : glob_output -> unit
+(** Restores the original output that was overridden by [push_output] *)
+val pop_output : unit -> unit
+
+(** Alias for [push_output NoGlob] *)
val pause : unit -> unit
+
+(** Deprecated alias for [pop_output] *)
val continue : unit -> unit
+[@@ocaml.deprecated "Use pop_output"]
val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 2853eef5c5..ee07fb6ed1 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -114,8 +114,8 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
ungeneralizable loc id) vars;
vars
-let rec make_fresh ids env x =
- if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x)
+let make_fresh ids env x =
+ Namegen.next_ident_away_from x (fun x -> not (is_freevar ids env x))
let next_name_away_from na avoid =
match na with
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 50f90ebea7..5f17d3e284 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -106,7 +106,7 @@ let transl_with_decl env base kind = function
| CWith_Module ({CAst.v=fqid},qid) ->
WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
| CWith_Definition ({CAst.v=fqid},udecl,c) ->
- let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
+ let sigma, udecl = interp_univ_decl_opt env udecl in
let c, ectx = interp_constr env sigma c in
let poly = lookup_polymorphism env base kind fqid in
begin match UState.check_univ_decl ~poly ectx udecl with
diff --git a/interp/notation.ml b/interp/notation.ml
index d57c4f3abf..c35ba44aa5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -32,7 +32,7 @@ open NumTok
fail if a number has no interpretation in the scope (e.g. there is
no interpretation for negative numbers in [nat]); interpreters both for
terms and patterns can be set; these interpreters are in permanent table
- [numeral_interpreter_tab]
+ [number_interpreter_tab]
- a set of ML printers for expressions denoting numbers parsable in
this scope
- a set of interpretations for infix (more generally distfix) notations
@@ -62,9 +62,11 @@ 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
| NtnParsedAsIdent, NtnParsedAsIdent -> true
+| NtnParsedAsName, NtnParsedAsName -> true
| NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
| NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _), _ -> false
+| NtnParsedAsBinder, NtnParsedAsBinder -> true
+| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
let ntpe_eq t1 t2 = match t1, t2 with
| NtnTypeConstr, NtnTypeConstr -> true
@@ -323,7 +325,7 @@ type key =
| Oth
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
@@ -341,22 +343,39 @@ type notation_rule = interp_rule * interpretation * notation_applicative_status
let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) =
x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2)
+let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) =
+ (* No need in principle to compare also_cases as it is inferred *)
+ also_cases1 = also_cases2 && notation_rule_eq rule1 rule2
+
+let adjust_application c1 c2 =
+ match c1, c2 with
+ | NApp (t1, a1), (NList (_,_,NApp (_, a2),_,_) | NApp (_, a2)) when List.length a1 >= List.length a2 ->
+ NApp (t1, List.firstn (List.length a2) a1)
+ | NApp (t1, a1), _ ->
+ t1
+ | _ -> c1
+
+let strictly_finer_interpretation_than (_,(_,(vars1,c1),_)) (_,(_,(vars2,c2),_)) =
+ let c1 = adjust_application c1 c2 in
+ Notation_ops.strictly_finer_notation_constr (List.map fst vars1, List.map fst vars2) c1 c2
+
let keymap_add key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
- (* In case of re-import, no need to keep the previous copy *)
- let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in
- KeyMap.add key (interp :: old) map
+ (* strictly finer interpretation are kept in front *)
+ let strictly_finer, rest = List.partition (fun c -> strictly_finer_interpretation_than c interp) old in
+ KeyMap.add key (strictly_finer @ interp :: rest) map
let keymap_remove key interp map =
let old = try KeyMap.find key map with Not_found -> [] in
- KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map
+ KeyMap.add key (List.remove_first (also_cases_notation_rule_eq interp) old) map
let keymap_find key map =
try KeyMap.find key map
with Not_found -> []
(* Scopes table : interpretation -> scope_name *)
-let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
+(* Boolean = for cases pattern also *)
+let notations_key_table = ref (KeyMap.empty : (bool * notation_rule) list KeyMap.t)
let glob_prim_constr_key c = match DAst.get c with
| GRef (ref, _) -> Some (canonical_gr ref)
@@ -386,6 +405,10 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
| NBinderList (_,_,NApp (NRef ref,args),_,_) ->
RefKey (canonical_gr ref), AppBoundedNotation (List.length args)
| NRef ref -> RefKey(canonical_gr ref), NotAppNotation
+ | NApp (NList (_,_,NApp (NRef ref,args),_,_), args') ->
+ RefKey (canonical_gr ref), AppBoundedNotation (List.length args + List.length args')
+ | NApp (NList (_,_,NApp (_,args),_,_), args') ->
+ Oth, AppBoundedNotation (List.length args + List.length args')
| NApp (_,args) -> Oth, AppBoundedNotation (List.length args)
| NList (_,_,NApp (NVar x,_),_,_) when x = Notation_ops.ldots_var -> Oth, AppUnboundedNotation
| _ -> Oth, NotAppNotation
@@ -446,13 +469,13 @@ module InnerPrimToken = struct
let do_interp ?loc interp primtok =
match primtok, interp with
- | Numeral n, RawNumInterp interp -> interp ?loc n
- | Numeral n, BigNumInterp interp ->
+ | Number n, RawNumInterp interp -> interp ?loc n
+ | Number n, BigNumInterp interp ->
(match NumTok.Signed.to_bigint n with
| Some n -> interp ?loc n
| None -> raise Not_found)
| String s, StringInterp interp -> interp ?loc s
- | (Numeral _ | String _),
+ | (Number _ | String _),
(RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
type uninterpreter =
@@ -466,16 +489,16 @@ module InnerPrimToken = struct
| StringUninterp f, StringUninterp f' -> f == f'
| _ -> false
- let mkNumeral n =
- Numeral (NumTok.Signed.of_bigint CDec n)
+ let mkNumber n =
+ Number (NumTok.Signed.of_bigint CDec n)
let mkString = function
| None -> None
| Some s -> if Unicode.is_utf8 s then Some (String s) else None
let do_uninterp uninterp g = match uninterp with
- | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
- | BigNumUninterp u -> Option.map mkNumeral (u g)
+ | RawNumUninterp u -> Option.map (fun (s,n) -> Number (s,n)) (u g)
+ | BigNumUninterp u -> Option.map mkNumber (u g)
| StringUninterp u -> mkString (u g)
end
@@ -495,7 +518,7 @@ let prim_token_uninterpreters =
(Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
(*******************************************************)
-(* Numeral notation interpretation *)
+(* Number notation interpretation *)
type prim_token_notation_error =
| UnexpectedTerm of Constr.t
| UnexpectedNonOptionTerm of Constr.t
@@ -519,21 +542,21 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type numeral_ty =
+type number_ty =
{ int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
- numeral : Names.inductive }
+ number : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Numeral.int + uint *)
- | UInt of int_ty (* Coq.Init.Numeral.uint *)
+ | Int of int_ty (* Coq.Init.Number.int + uint *)
+ | UInt of int_ty (* Coq.Init.Number.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
- | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+ | Number of number_ty (* Coq.Init.Number.number + uint + int *)
| DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
| DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+ | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -542,19 +565,36 @@ type string_target_kind =
type option_kind = Option | Direct
type 'target conversion_kind = 'target * option_kind
+(** A postprocessing translation [to_post] can be done after execution
+ of the [to_ty] interpreter. The reverse translation is performed
+ before the [of_ty] uninterpreter.
+
+ [to_post] is an array of [n] lists [l_i] of tuples [(f, t,
+ args)]. When the head symbol of the translated term matches one of
+ the [f] in the list [l_0] it is replaced by [t] and its arguments
+ are translated acording to [args] where [ToPostCopy] means that the
+ argument is kept unchanged and [ToPostAs k] means that the
+ argument is recursively translated according to [l_k].
+ [ToPostHole] introduces an additional implicit argument hole
+ (in the reverse translation, the corresponding argument is removed).
+ [ToPostCheck r] behaves as [ToPostCopy] except in the reverse
+ translation which fails if the copied term is not [r].
+ When [n] is null, no translation is performed. *)
+type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t
type ('target, 'warning) prim_token_notation_obj =
{ to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
+ to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array;
of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
ty_name : Libnames.qualid; (* for warnings / error messages *)
warning : 'warning }
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
module PrimTokenNotation = struct
-(** * Code shared between Numeral notation and String notation *)
+(** * Code shared between Number notation and String notation *)
(** Reduction
The constr [c] below isn't necessarily well-typed, since we
@@ -588,22 +628,69 @@ exception NotAValidPrimToken
to [constr] for the subset that concerns us.
Note that if you update [constr_of_glob], you should update the
- corresponding numeral notation *and* string notation doc in
+ corresponding number notation *and* string notation doc in
doc/sphinx/user-extensions/syntax-extensions.rst that describes
what it means for a term to be ground / to be able to be
considered for parsing. *)
-let rec constr_of_glob env sigma g = match DAst.get g with
- | Glob_term.GRef (GlobRef.ConstructRef c, _) ->
- let sigma,c = Evd.fresh_constructor_instance env sigma c in
- sigma,mkConstructU c
- | Glob_term.GRef (GlobRef.IndRef c, _) ->
- let sigma,c = Evd.fresh_inductive_instance env sigma c in
- sigma,mkIndU c
+let constr_of_globref allow_constant env sigma = function
+ | GlobRef.ConstructRef c ->
+ let sigma,c = Evd.fresh_constructor_instance env sigma c in
+ sigma,mkConstructU c
+ | GlobRef.IndRef c ->
+ let sigma,c = Evd.fresh_inductive_instance env sigma c in
+ sigma,mkIndU c
+ | GlobRef.ConstRef c when allow_constant ->
+ let sigma,c = Evd.fresh_constant_instance env sigma c in
+ sigma,mkConstU c
+ | _ -> raise NotAValidPrimToken
+
+let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get g with
+ | Glob_term.GRef (r, _) ->
+ let o = List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post in
+ begin match o with
+ | None -> constr_of_globref allow_constant env sigma r
+ | Some (r, _, a) ->
+ (* [g] is not a GApp so check that [post]
+ does not expect any actual argument
+ (i.e., [a] contains only ToPostHole since they mean "ignore arg") *)
+ if List.exists ((<>) ToPostHole) a then raise NotAValidPrimToken;
+ constr_of_globref true env sigma r
+ end
| Glob_term.GApp (gc, gcl) ->
- let sigma,c = constr_of_glob env sigma gc in
- let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
- sigma,mkApp (c, Array.of_list cl)
+ let o = match DAst.get gc with
+ | Glob_term.GRef (r, _) -> List.find_opt (fun (_,r',_) -> GlobRef.equal r r') post
+ | _ -> None in
+ begin match o with
+ | None ->
+ let sigma,c = constr_of_glob allow_constant to_post post env sigma gc in
+ let sigma,cl = List.fold_left_map (constr_of_glob allow_constant to_post post env) sigma gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ | Some (r, _, a) ->
+ let sigma,c = constr_of_globref true env sigma r in
+ let rec aux sigma a gcl = match a, gcl with
+ | [], [] -> sigma,[]
+ | ToPostCopy :: a, gc :: gcl ->
+ let sigma,c = constr_of_glob allow_constant [||] [] env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostCheck r :: a, gc :: gcl ->
+ let () = match DAst.get gc with
+ | Glob_term.GRef (r', _) when GlobRef.equal r r' -> ()
+ | _ -> raise NotAValidPrimToken in
+ let sigma,c = constr_of_glob true [||] [] env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostAs i :: a, gc :: gcl ->
+ let sigma,c = constr_of_glob allow_constant to_post to_post.(i) env sigma gc in
+ let sigma,cl = aux sigma a gcl in
+ sigma, c :: cl
+ | ToPostHole :: post, _ :: gcl -> aux sigma post gcl
+ | [], _ :: _ | _ :: _, [] -> raise NotAValidPrimToken
+ in
+ let sigma,cl = aux sigma a gcl in
+ sigma,mkApp (c, Array.of_list cl)
+ end
| Glob_term.GInt i -> sigma, mkInt i
| Glob_term.GSort gs ->
let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in
@@ -611,6 +698,10 @@ let rec constr_of_glob env sigma g = match DAst.get g with
| _ ->
raise NotAValidPrimToken
+let constr_of_glob to_post env sigma (Glob_term.AnyGlobConstr g) =
+ let post = match to_post with [||] -> [] | _ -> to_post.(0) in
+ constr_of_glob false to_post post env sigma g
+
let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
| App (c, ca) ->
let c = glob_of_constr token_kind ?loc env sigma c in
@@ -632,9 +723,38 @@ let no_such_prim_token uninterpreted_token_kind ?loc ty =
(str ("Cannot interpret this "^uninterpreted_token_kind^" as a value of type ") ++
pr_qualid ty)
-let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma c =
+let rec postprocess token_kind ?loc ty to_post post g =
+ let g', gl = match DAst.get g with Glob_term.GApp (g, gl) -> g, gl | _ -> g, [] in
+ let o =
+ match DAst.get g' with
+ | Glob_term.GRef (r, None) ->
+ List.find_opt (fun (r',_,_) -> GlobRef.equal r r') post
+ | _ -> None in
+ match o with None -> g | Some (_, r, a) ->
+ let rec f n a gl = match a, gl with
+ | [], [] -> []
+ | ToPostHole :: a, gl ->
+ let e = Evar_kinds.ImplicitArg (r, (n, None), true) in
+ let h = DAst.make ?loc (Glob_term.GHole (e, Namegen.IntroAnonymous, None)) in
+ h :: f (n+1) a gl
+ | (ToPostCopy | ToPostCheck _) :: a, g :: gl -> g :: f (n+1) a gl
+ | ToPostAs c :: a, g :: gl ->
+ postprocess token_kind ?loc ty to_post to_post.(c) g :: f (n+1) a gl
+ | [], _::_ | _::_, [] ->
+ no_such_prim_token token_kind ?loc ty
+ in
+ let gl = f 1 a gl in
+ let g = DAst.make ?loc (Glob_term.GRef (r, None)) in
+ DAst.make ?loc (Glob_term.GApp (g, gl))
+
+let glob_of_constr token_kind ty ?loc env sigma to_post c =
+ let g = glob_of_constr token_kind ?loc env sigma c in
+ match to_post with [||] -> g | _ ->
+ postprocess token_kind ?loc ty to_post to_post.(0) g
+
+let interp_option uninterpreted_token_kind token_kind ty ?loc env sigma to_post c =
match Constr.kind c with
- | App (_Some, [| _; c |]) -> glob_of_constr token_kind ?loc env sigma c
+ | App (_Some, [| _; c |]) -> glob_of_constr token_kind ty ?loc env sigma to_post c
| App (_None, [| _ |]) -> no_such_prim_token uninterpreted_token_kind ?loc ty
| x -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedNonOptionTerm c))
@@ -643,13 +763,13 @@ let uninterp_option c =
| App (_Some, [| _; x |]) -> x
| _ -> raise NotAValidPrimToken
-let uninterp to_raw o (Glob_term.AnyGlobConstr n) =
+let uninterp to_raw o n =
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,of_ty = Evd.fresh_global env sigma o.of_ty in
let of_ty = EConstr.Unsafe.to_constr of_ty in
try
- let sigma,n = constr_of_glob env sigma n in
+ let sigma,n = constr_of_glob o.to_post env sigma n in
let c = eval_constr_app env sigma of_ty n in
let c = if snd o.of_kind == Direct then c else uninterp_option c in
Some (to_raw (fst o.of_kind, c))
@@ -670,8 +790,8 @@ let rec int63_of_pos_bigint i =
(Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
-module Numeral = struct
-(** * Numeral notation *)
+module Numbers = struct
+(** * Number notation *)
open PrimTokenNotation
let warn_large_num =
@@ -727,7 +847,7 @@ let coqint_of_rawnum inds c (sign,n) =
let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
mkApp (mkConstruct (ind, pos_neg), [|uint|])
-let coqnumeral_of_rawnum inds c n =
+let coqnumber_of_rawnum inds c n =
let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in
let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in
let i = coqint_of_rawnum inds.int c i in
@@ -739,19 +859,19 @@ let coqnumeral_of_rawnum inds c n =
mkApp (mkConstruct (ind, 2), [|i; f; e|]) (* (D|Hexad)ecimalExp *)
let mkDecHex ind c n = match c with
- | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Dec *)
- | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hex *)
+ | CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *)
+ | CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *)
exception NonDecimal
-let decimal_coqnumeral_of_rawnum inds n =
+let decimal_coqnumber_of_rawnum inds n =
if NumTok.Signed.classify n <> CDec then raise NonDecimal;
- coqnumeral_of_rawnum inds CDec n
+ coqnumber_of_rawnum inds CDec n
-let coqnumeral_of_rawnum inds n =
+let coqnumber_of_rawnum inds n =
let c = NumTok.Signed.classify n in
- let n = coqnumeral_of_rawnum inds c n in
- mkDecHex inds.numeral c n
+ let n = coqnumber_of_rawnum inds c n in
+ mkDecHex inds.number c n
let decimal_coquint_of_rawnum inds n =
if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
@@ -801,7 +921,7 @@ let rawnum_of_coqint cl c =
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let rawnum_of_coqnumeral cl c =
+let rawnum_of_coqnumber cl c =
let of_ife i f e =
let n = rawnum_of_coqint cl i in
let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
@@ -815,17 +935,17 @@ let rawnum_of_coqnumeral cl c =
let destDecHex c = match Constr.kind c with
| App (c,[|c'|]) ->
(match Constr.kind c with
- | Construct ((_,1), _) (* (UInt|Int|)Dec *) -> CDec, c'
- | Construct ((_,2), _) (* (UInt|Int|)Hex *) -> CHex, c'
+ | Construct ((_,1), _) (* (UInt|Int|)Decimal *) -> CDec, c'
+ | Construct ((_,2), _) (* (UInt|Int|)Hexadecimal *) -> CHex, c'
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let decimal_rawnum_of_coqnumeral c =
- rawnum_of_coqnumeral CDec c
+let decimal_rawnum_of_coqnumber c =
+ rawnum_of_coqnumber CDec c
-let rawnum_of_coqnumeral c =
+let rawnum_of_coqnumber c =
let cl, c = destDecHex c in
- rawnum_of_coqnumeral cl c
+ rawnum_of_coqnumber cl c
let decimal_rawnum_of_coquint c =
rawnum_of_coquint CDec c
@@ -947,9 +1067,9 @@ let interp o ?loc n =
interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
| (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
no_such_prim_token "number" ?loc o.ty_name
- | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
- | Decimal numeral_ty, _ ->
- (try decimal_coqnumeral_of_rawnum numeral_ty n
+ | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
+ | Decimal number_ty, _ ->
+ (try decimal_coqnumber_of_rawnum number_ty n
with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
in
let env = Global.env () in
@@ -959,12 +1079,13 @@ let interp o ?loc n =
match o.warning, snd o.to_kind with
| Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
warn_abstract_large_num (o.ty_name,o.to_ty);
- glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
+ assert (Array.length o.to_post = 0);
+ glob_of_constr "number" o.ty_name ?loc env sigma o.to_post (mkApp (to_ty,[|c|]))
| _ ->
let res = eval_constr_app env sigma to_ty c in
match snd o.to_kind with
- | Direct -> glob_of_constr "numeral" ?loc env sigma res
- | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+ | Direct -> glob_of_constr "number" o.ty_name ?loc env sigma o.to_post res
+ | Option -> interp_option "number" "number" o.ty_name ?loc env sigma o.to_post res
let uninterp o n =
PrimTokenNotation.uninterp
@@ -973,10 +1094,10 @@ let uninterp o n =
| (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
| (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
| (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
- | (Numeral _, c) -> rawnum_of_coqnumeral c
+ | (Number _, c) -> rawnum_of_coqnumber c
| (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
| (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
- | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c
+ | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
end o n
end
@@ -1009,11 +1130,12 @@ let coqbyte_of_string ?loc byte s =
let p =
if Int.equal (String.length s) 1 then int_of_char s.[0]
else
- if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
- then int_of_string s
- else
+ let n =
+ if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+ then int_of_string s else 256 in
+ if n < 256 then n else
user_err ?loc ~hdr:"coqbyte_of_string"
- (str "Expects a single character or a three-digits ascii code.") in
+ (str "Expects a single character or a three-digit ASCII code.") in
coqbyte_of_char_code byte p
let coqbyte_of_char byte c = coqbyte_of_char_code byte (Char.code c)
@@ -1068,8 +1190,8 @@ let interp o ?loc n =
let to_ty = EConstr.Unsafe.to_constr to_ty in
let res = eval_constr_app env sigma to_ty c in
match snd o.to_kind with
- | Direct -> glob_of_constr "string" ?loc env sigma res
- | Option -> interp_option "string" "string" o.ty_name ?loc env sigma res
+ | Direct -> glob_of_constr "string" o.ty_name ?loc env sigma o.to_post res
+ | Option -> interp_option "string" "string" o.ty_name ?loc env sigma o.to_post res
let uninterp o n =
PrimTokenNotation.uninterp
@@ -1081,21 +1203,21 @@ end
(* A [prim_token_infos], which is synchronized with the document
state, either contains a unique id pointing to an unsynchronized
- prim token function, or a numeral notation object describing how to
+ prim token function, or a number notation object describing how to
interpret and uninterpret. We provide [prim_token_infos] because
we expect plugins to provide their own interpretation functions,
- rather than going through numeral notations, which are available as
+ rather than going through number notations, which are available as
a vernacular. *)
type prim_token_interp_info =
Uid of prim_token_uid
- | NumeralNotation of numeral_notation_obj
+ | NumberNotation of number_notation_obj
| StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
pt_scope : scope_name; (** Concerned scope *)
- pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
pt_required : required_module; (** Module that should be loaded first *)
pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -1119,7 +1241,7 @@ let hashtbl_check_and_set allow_overwrite uid f h eq =
| _ ->
user_err ~hdr:"prim_token_interpreter"
(str "Unique identifier " ++ str uid ++
- str " already used to register a numeral or string (un)interpreter.")
+ str " already used to register a number or string (un)interpreter.")
let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
hashtbl_check_and_set
@@ -1147,7 +1269,6 @@ let cache_prim_token_interpretation (_,infos) =
String.Map.add sc (infos.pt_required,ptii) !prim_token_interp_infos;
let add_uninterp r =
let l = try GlobRef.Map.find r !prim_token_uninterp_infos with Not_found -> [] in
- let l = List.remove_assoc_f String.equal sc l in
prim_token_uninterp_infos :=
GlobRef.Map.add r ((sc,(ptii,infos.pt_in_match)) :: l)
!prim_token_uninterp_infos in
@@ -1220,7 +1341,7 @@ let check_required_module ?loc sc (sp,d) =
(str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
str (List.last d) ++ str ".")
-(* Look if some notation or numeral printer in [scope] can be used in
+(* Look if some notation or number printer in [scope] can be used in
the scope stack [scopes], and if yes, using delimiters or not *)
let find_with_delimiters = function
@@ -1237,7 +1358,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
| NotationInScope scope' when String.equal scope scope' ->
Some (None,None)
| _ ->
- (* If the most recently open scope has a notation/numeral printer
+ (* If the most recently open scope has a notation/number printer
but not the expected one then we need delimiters *)
if find scope then
find_with_delimiters ntn_scope
@@ -1312,12 +1433,12 @@ let check_parsing_override (scopt,ntn) data = function
| OnlyParsingData (_,old_data) ->
let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
warn_override_if_needed (scopt,ntn) overridden data old_data;
- None, not overridden
+ None
| ParsingAndPrintingData (_,on_printing,old_data) ->
let overridden = not (interpretation_eq data.not_interp old_data.not_interp) in
warn_override_if_needed (scopt,ntn) overridden data old_data;
- (if on_printing then Some old_data.not_interp else None), not overridden
- | NoParsingData -> None, false
+ if on_printing then Some old_data.not_interp else None
+ | NoParsingData -> None
let check_printing_override (scopt,ntn) data parsingdata printingdata =
let parsing_update = match parsingdata with
@@ -1333,28 +1454,28 @@ let check_printing_override (scopt,ntn) data parsingdata printingdata =
exists) printingdata in
parsing_update, exists
-let remove_uninterpretation rule (metas,c as pat) =
+let remove_uninterpretation rule also_in_cases_pattern (metas,c as pat) =
let (key,n) = notation_constr_key c in
- notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table
+ notations_key_table := keymap_remove key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
-let declare_uninterpretation rule (metas,c as pat) =
+let declare_uninterpretation ?(also_in_cases_pattern=true) rule (metas,c as pat) =
let (key,n) = notation_constr_key c in
- notations_key_table := keymap_add key (rule,pat,n) !notations_key_table
+ notations_key_table := keymap_add key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table
let update_notation_data (scopt,ntn) use data table =
let (parsingdata,printingdata) =
try NotationMap.find ntn table with Not_found -> (NoParsingData, []) in
match use with
| OnlyParsing ->
- let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
- NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update, exists
+ let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (OnlyParsingData (true,data), printingdata) table, printing_update
| ParsingAndPrinting ->
- let printing_update, exists = check_parsing_override (scopt,ntn) data parsingdata in
- NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update, exists
+ let printing_update = check_parsing_override (scopt,ntn) data parsingdata in
+ NotationMap.add ntn (ParsingAndPrintingData (true,true,data), printingdata) table, printing_update
| OnlyPrinting ->
let parsingdata, exists = check_printing_override (scopt,ntn) data parsingdata printingdata in
let printingdata = if exists then printingdata else (true,data) :: printingdata in
- NotationMap.add ntn (parsingdata, printingdata) table, None, exists
+ NotationMap.add ntn (parsingdata, printingdata) table, None
let rec find_interpretation ntn find = function
| [] -> raise Not_found
@@ -1375,8 +1496,8 @@ let find_notation ntn sc =
| _ -> raise Not_found
let notation_of_prim_token = function
- | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
- | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
+ | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+ | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -1394,7 +1515,7 @@ let find_prim_token check_allowed ?loc p sc =
check_required_module ?loc sc spdir;
let interp = match info with
| Uid uid -> Hashtbl.find prim_token_interpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+ | NumberNotation o -> InnerPrimToken.RawNumInterp (Numbers.interp o)
| StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
in
let pat = InnerPrimToken.do_interp ?loc interp p in
@@ -1411,8 +1532,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
let _, info = Exninfo.capture exn in
user_err ?loc ~info ~hdr:"interp_prim_token"
((match p with
- | Numeral _ ->
- str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
+ | Number _ ->
+ str "No interpretation for number " ++ pr_notation (notation_of_prim_token p)
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
let interp_prim_token ?loc =
@@ -1448,14 +1569,17 @@ let interp_notation ?loc ntn local_scopes =
(str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
let uninterp_notations c =
- List.map_append (fun key -> keymap_find key !notations_key_table)
+ List.map_append (fun key -> List.map snd (keymap_find key !notations_key_table))
(glob_constr_keys c)
+let filter_also_for_pattern =
+ List.map_filter (function (true,x) -> Some x | _ -> None)
+
let uninterp_cases_pattern_notations c =
- keymap_find (cases_pattern_key c) !notations_key_table
+ filter_also_for_pattern (keymap_find (cases_pattern_key c) !notations_key_table)
let uninterp_ind_pattern_notations ind =
- keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table
+ filter_also_for_pattern (keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table)
let has_active_parsing_rule_in_scope ntn sc =
try
@@ -1615,7 +1739,7 @@ type entry_coercion_kind =
| IsEntryGlobal of string * int
| IsEntryIdent of string * int
-let declare_notation (scopt,ntn) pat df ~use coe deprecation =
+let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecation =
(* Register the interpretation *)
let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in
let sc = find_scope scope in
@@ -1624,23 +1748,22 @@ let declare_notation (scopt,ntn) pat df ~use coe deprecation =
not_location = df;
not_deprecation = deprecation;
} in
- let notation_update,printing_update, exists = update_notation_data (scopt,ntn) use notdata sc.notations in
- if not exists then
- let sc = { sc with notations = notation_update } in
- scope_map := String.Map.add scope sc !scope_map;
+ let notation_update,printing_update = update_notation_data (scopt,ntn) use notdata sc.notations in
+ let sc = { sc with notations = notation_update } in
+ scope_map := String.Map.add scope sc !scope_map;
(* Update the uninterpretation cache *)
begin match printing_update with
- | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat
+ | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat
| None -> ()
end;
- if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat;
+ if use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat;
(* Register visibility of lonely notations *)
- if not exists then begin match scopt with
+ begin match scopt with
| LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack
| NotationInScope _ -> ()
end;
(* Declare a possible coercion *)
- if not exists then begin match coe with
+ begin match coe with
| Some (IsEntryCoercion entry) ->
let (_,level,_) = level_of_notation ntn in
let level = match fst ntn with
@@ -1659,14 +1782,14 @@ let availability_of_prim_token n printer_scope local_scopes =
let uid = snd (String.Map.find scope !prim_token_interp_infos) in
let open InnerPrimToken in
match n, uid with
- | Constrexpr.Numeral _, NumeralNotation _ -> true
- | _, NumeralNotation _ -> false
+ | Constrexpr.Number _, NumberNotation _ -> true
+ | _, NumberNotation _ -> false
| String _, StringNotation _ -> true
| _, StringNotation _ -> false
| _, Uid uid ->
let interp = Hashtbl.find prim_token_interpreters uid in
match n, interp with
- | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+ | Constrexpr.Number _, (RawNumInterp _ | BigNumInterp _) -> true
| String _, StringInterp _ -> true
| _ -> false
with Not_found -> false
@@ -1681,7 +1804,7 @@ let rec find_uninterpretation need_delim def find = function
def
| OpenScopeItem scope :: scopes ->
(try find need_delim scope
- with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+ with Not_found -> find_uninterpretation need_delim def find scopes) (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a number notation *)
| LonelyNotationItem ntn::scopes ->
find_uninterpretation (ntn::need_delim) def find scopes
@@ -1693,7 +1816,7 @@ let uninterp_prim_token c local_scopes =
try
let uninterp = match info with
| Uid uid -> Hashtbl.find prim_token_uninterpreters uid
- | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+ | NumberNotation o -> InnerPrimToken.RawNumUninterp (Numbers.uninterp o)
| StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
in
match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
@@ -1929,12 +2052,12 @@ type symbol =
| Break of int
let rec symbol_eq s1 s2 = match s1, s2 with
-| Terminal s1, Terminal s2 -> String.equal s1 s2
-| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
-| SProdList (id1, l1), SProdList (id2, l2) ->
- Id.equal id1 id2 && List.equal symbol_eq l1 l2
-| Break i1, Break i2 -> Int.equal i1 i2
-| _ -> false
+ | Terminal s1, Terminal s2 -> String.equal s1 s2
+ | NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
+ | SProdList (id1, l1), SProdList (id2, l2) ->
+ Id.equal id1 id2 && List.equal symbol_eq l1 l2
+ | Break i1, Break i2 -> Int.equal i1 i2
+ | _ -> false
let rec string_of_symbol = function
| NonTerminal _ -> ["_"]
@@ -2096,23 +2219,114 @@ let rec raw_analyze_notation_tokens = function
| WhiteSpace n :: sl ->
Break n :: raw_analyze_notation_tokens sl
-let decompose_raw_notation ntn = raw_analyze_notation_tokens (split_notation_string ntn)
-
-let possible_notations ntn =
+let rec raw_analyze_anonymous_notation_tokens = function
+ | [] -> []
+ | String ".." :: sl -> NonTerminal Notation_ops.ldots_var :: raw_analyze_anonymous_notation_tokens sl
+ | String "_" :: sl -> NonTerminal (Id.of_string "dummy") :: raw_analyze_anonymous_notation_tokens sl
+ | String s :: sl ->
+ Terminal (String.drop_simple_quotes s) :: raw_analyze_anonymous_notation_tokens sl
+ | WhiteSpace n :: sl -> raw_analyze_anonymous_notation_tokens sl
+
+(* Interpret notations with a recursive component *)
+
+let out_nt = function NonTerminal x -> x | _ -> assert false
+
+let msg_expected_form_of_recursive_notation =
+ "In the notation, the special symbol \"..\" must occur in\na configuration of the form \"x symbs .. symbs y\"."
+
+let rec find_pattern nt xl = function
+ | Break n as x :: l, Break n' :: l' when Int.equal n n' ->
+ find_pattern nt (x::xl) (l,l')
+ | Terminal s as x :: l, Terminal s' :: l' when String.equal s s' ->
+ find_pattern nt (x::xl) (l,l')
+ | [], NonTerminal x' :: l' ->
+ (out_nt nt,x',List.rev xl),l'
+ | _, Break s :: _ | Break s :: _, _ ->
+ user_err Pp.(str ("A break occurs on one side of \"..\" but not on the other side."))
+ | _, Terminal s :: _ | Terminal s :: _, _ ->
+ user_err ~hdr:"Metasyntax.find_pattern"
+ (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
+ | _, [] ->
+ user_err Pp.(str msg_expected_form_of_recursive_notation)
+ | ((SProdList _ | NonTerminal _) :: _), _ | _, (SProdList _ :: _) ->
+ anomaly (Pp.str "Only Terminal or Break expected on left, non-SProdList on right.")
+
+let rec interp_list_parser hd = function
+ | [] -> [], List.rev hd
+ | NonTerminal id :: tl when Id.equal id Notation_ops.ldots_var ->
+ if List.is_empty hd then user_err Pp.(str msg_expected_form_of_recursive_notation);
+ let hd = List.rev hd in
+ let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
+ let xyl,tl'' = interp_list_parser [] tl' in
+ (* We remember each pair of variable denoting a recursive part to *)
+ (* remove the second copy of it afterwards *)
+ (x,y)::xyl, SProdList (x,sl) :: tl''
+ | (Terminal _ | Break _) as s :: tl ->
+ if List.is_empty hd then
+ let yl,tl' = interp_list_parser [] tl in
+ yl, s :: tl'
+ else
+ interp_list_parser (s::hd) tl
+ | NonTerminal _ as x :: tl ->
+ let xyl,tl' = interp_list_parser [x] tl in
+ xyl, List.rev_append hd tl'
+ | SProdList _ :: _ -> anomaly (Pp.str "Unexpected SProdList in interp_list_parser.")
+
+let get_notation_vars l =
+ List.map_filter (function NonTerminal id | SProdList (id,_) -> Some id | _ -> None) l
+
+let decompose_raw_notation ntn =
+ let l = split_notation_string ntn in
+ let l = raw_analyze_notation_tokens l in
+ let recvars,l = interp_list_parser [] l in
+ let vars = get_notation_vars l in
+ recvars, vars, l
+
+let interpret_notation_string ntn =
(* We collect the possible interpretations of a notation string depending on whether it is
in "x 'U' y" or "_ U _" format *)
let toks = split_notation_string ntn in
- if List.exists (function String "_" -> true | _ -> false) toks then
- (* Only "_ U _" format *)
- [ntn]
- else
- let _,ntn' = make_notation_key None (raw_analyze_notation_tokens toks) in
- if String.equal ntn ntn' then (* Only symbols *) [ntn] else [ntn;ntn']
+ let toks =
+ if
+ List.exists (function String "_" -> true | _ -> false) toks ||
+ List.for_all (function String id -> Id.is_valid id | _ -> false) toks
+ then
+ (* Only "_ U _" format *)
+ raw_analyze_anonymous_notation_tokens toks
+ else
+ (* Includes the case of only a subset of tokens or an "x 'U' y"-style format *)
+ raw_analyze_notation_tokens toks
+ in
+ let _,toks = interp_list_parser [] toks in
+ let _,ntn' = make_notation_key None toks in
+ ntn'
+
+(* Tell if a non-recursive notation is an instance of a recursive one *)
+let is_approximation ntn ntn' =
+ let rec aux toks1 toks2 = match (toks1, toks2) with
+ | Terminal s1 :: toks1, Terminal s2 :: toks2 -> String.equal s1 s2 && aux toks1 toks2
+ | NonTerminal _ :: toks1, NonTerminal _ :: toks2 -> aux toks1 toks2
+ | SProdList (_,l1) :: toks1, SProdList (_, l2) :: toks2 -> aux l1 l2 && aux toks1 toks2
+ | NonTerminal _ :: toks1, SProdList (_,l2) :: toks2 -> aux' toks1 l2 l2 toks2 || aux toks1 toks2
+ | [], [] -> true
+ | (Break _ :: _, _) | (_, Break _ :: _) -> assert false
+ | (Terminal _ | NonTerminal _ | SProdList _) :: _, _ -> false
+ | [], _ -> false
+ and aux' toks1 l2 l2full toks2 = match (toks1, l2) with
+ | Terminal s1 :: toks1, Terminal s2 :: l2 when String.equal s1 s2 -> aux' toks1 l2 l2full toks2
+ | NonTerminal _ :: toks1, [] -> aux' toks1 l2full l2full toks2 || aux toks1 toks2
+ | _ -> false
+ in
+ let _,toks = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn)) in
+ let _,toks' = interp_list_parser [] (raw_analyze_anonymous_notation_tokens (split_notation_string ntn')) in
+ aux toks toks'
let browse_notation strict ntn map =
- let ntns = possible_notations ntn in
- let find (from,ntn' as fullntn') ntn =
- if String.contains ntn ' ' then String.equal ntn ntn'
+ let ntn = interpret_notation_string ntn in
+ let find (from,ntn' as fullntn') =
+ if String.contains ntn ' ' then
+ if String.string_contains ~where:ntn' ~what:".." then is_approximation ntn ntn'
+ else String.equal ntn ntn'
else
let _,toks = decompose_notation_key fullntn' in
let get_terminals = function Terminal ntn -> Some ntn | _ -> None in
@@ -2124,7 +2338,7 @@ let browse_notation strict ntn map =
String.Map.fold
(fun scope_name sc ->
NotationMap.fold (fun ntn data l ->
- if List.exists (find ntn) ntns
+ if find ntn
then List.map (fun d -> (ntn,scope_name,d)) (extract_notation_data data) @ l
else l) sc.notations)
map [] in
diff --git a/interp/notation.mli b/interp/notation.mli
index d744ff41d9..97955bf92e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,7 +74,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
(** {6 Declare and uses back and forth an interpretation of primitive token } *)
-(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal**
+(** A number interpreter is the pair of an interpreter for **(hexa)decimal**
numbers in terms and an optional interpreter in pattern, if
non integer or negative numbers are not supported, the interpreter
must fail with an appropriate error message *)
@@ -84,7 +84,7 @@ type required_module = full_path * string list
type rawnum = NumTok.Signed.t
(** The unique id string below will be used to refer to a particular
- registered interpreter/uninterpreter of numeral or string notation.
+ registered interpreter/uninterpreter of number or string notation.
Using the same uid for different (un)interpreters will fail.
If at most one interpretation of prim token is used per scope,
then the scope name could be used as unique id. *)
@@ -106,7 +106,7 @@ val register_bignumeral_interpretation :
val register_string_interpretation :
?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
-(** * Numeral notation *)
+(** * Number notation *)
type prim_token_notation_error =
| UnexpectedTerm of Constr.t
@@ -131,21 +131,21 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
-type numeral_ty =
+type number_ty =
{ int : int_ty;
decimal : Names.inductive;
hexadecimal : Names.inductive;
- numeral : Names.inductive }
+ number : Names.inductive }
type target_kind =
- | Int of int_ty (* Coq.Init.Numeral.int + uint *)
- | UInt of int_ty (* Coq.Init.Numeral.uint *)
+ | Int of int_ty (* Coq.Init.Number.int + uint *)
+ | UInt of int_ty (* Coq.Init.Number.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
- | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+ | Number of number_ty (* Coq.Init.Number.number + uint + int *)
| DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
| DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
- | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+ | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -154,26 +154,43 @@ type string_target_kind =
type option_kind = Option | Direct
type 'target conversion_kind = 'target * option_kind
+(** A postprocessing translation [to_post] can be done after execution
+ of the [to_ty] interpreter. The reverse translation is performed
+ before the [of_ty] uninterpreter.
+
+ [to_post] is an array of [n] lists [l_i] of tuples [(f, t,
+ args)]. When the head symbol of the translated term matches one of
+ the [f] in the list [l_0] it is replaced by [t] and its arguments
+ are translated acording to [args] where [ToPostCopy] means that the
+ argument is kept unchanged and [ToPostAs k] means that the
+ argument is recursively translated according to [l_k].
+ [ToPostHole] introduces an additional implicit argument hole
+ (in the reverse translation, the corresponding argument is removed).
+ [ToPostCheck r] behaves as [ToPostCopy] except in the reverse
+ translation which fails if the copied term is not [r].
+ When [n] is null, no translation is performed. *)
+type to_post_arg = ToPostCopy | ToPostAs of int | ToPostHole | ToPostCheck of GlobRef.t
type ('target, 'warning) prim_token_notation_obj =
{ to_kind : 'target conversion_kind;
to_ty : GlobRef.t;
+ to_post : ((GlobRef.t * GlobRef.t * to_post_arg list) list) array;
of_kind : 'target conversion_kind;
of_ty : GlobRef.t;
ty_name : Libnames.qualid; (* for warnings / error messages *)
warning : 'warning }
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
type prim_token_interp_info =
Uid of prim_token_uid
- | NumeralNotation of numeral_notation_obj
+ | NumberNotation of number_notation_obj
| StringNotation of string_notation_obj
type prim_token_infos = {
pt_local : bool; (** Is this interpretation local? *)
pt_scope : scope_name; (** Concerned scope *)
- pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+ pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
pt_required : required_module; (** Module that should be loaded first *)
pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -234,7 +251,7 @@ type notation_use =
| OnlyParsing
| ParsingAndPrinting
-val declare_uninterpretation : interp_rule -> interpretation -> unit
+val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> interpretation -> unit
type entry_coercion_kind =
| IsEntryCoercion of notation_entry_level
@@ -243,6 +260,7 @@ type entry_coercion_kind =
val declare_notation : notation_with_optional_scope * notation ->
interpretation -> notation_location -> use:notation_use ->
+ also_in_cases_pattern:bool ->
entry_coercion_kind option ->
Deprecation.t option -> unit
@@ -316,8 +334,10 @@ val symbol_eq : symbol -> symbol -> bool
val make_notation_key : notation_entry -> symbol list -> notation
val decompose_notation_key : notation -> notation_entry * symbol list
-(** Decompose a notation of the form "a 'U' b" *)
-val decompose_raw_notation : string -> symbol list
+(** Decompose a notation of the form "a 'U' b" together with the lists
+ of pairs of recursive variables and the list of all variables
+ binding in the notation *)
+val decompose_raw_notation : string -> (Id.t * Id.t) list * Id.t list * symbol list
(** Prints scopes (expects a pure aconstr printer) *)
val pr_scope_class : scope_class -> Pp.t
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 354809252e..036970ce37 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -24,82 +24,186 @@ open Notation_term
(**********************************************************************)
(* Utilities *)
-(* helper for NVar, NVar case in eq_notation_constr *)
-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 =
-(vars1 == vars2 && t1 == t2) ||
-match t1, t2 with
-| 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
- | None ,None -> Id.equal id1 id2
- | _ -> false)
-| NApp (t1, a1), NApp (t2, a2) ->
- (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
-| NHole (_, _, _), NHole (_, _, _) -> true (* FIXME? *)
-| NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLambda (na1, t1, u1), NLambda (na2, t2, u2) ->
- Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NProd (na1, t1, u1), NProd (na2, t2, u2) ->
- Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NBinderList (i1, j1, t1, u1, b1), NBinderList (i2, j2, t2, u2, b2) ->
- Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2 && b1 == b2
-| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) ->
- Name.equal na1 na2 && eq_notation_constr vars b1 b2 &&
- Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2
-| NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
- let eqpat (p1, t1) (p2, t2) =
- List.equal cases_pattern_eq p1 p2 &&
- (eq_notation_constr vars) t1 t2
- in
- let eqf (t1, (na1, o1)) (t2, (na2, o2)) =
- let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in
- (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2
- in
- Option.equal (eq_notation_constr vars) o1 o2 &&
- List.equal eqf r1 r2 &&
- List.equal eqpat p1 p2
-| NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
- List.equal Name.equal nas1 nas2 &&
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) t1 t2 &&
- (eq_notation_constr vars) u1 u2
-| NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
- (eq_notation_constr vars) t1 t2 &&
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) u1 u2 &&
- (eq_notation_constr vars) r1 r2
-| NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
- let eq (na1, o1, t1) (na2, o2, t2) =
- Name.equal na1 na2 &&
- Option.equal (eq_notation_constr vars) o1 o2 &&
- (eq_notation_constr vars) t1 t2
- in
- Array.equal Id.equal ids1 ids2 &&
- Array.equal (List.equal eq) ts1 ts2 &&
- Array.equal (eq_notation_constr vars) us1 us2 &&
- Array.equal (eq_notation_constr vars) rs1 rs2
-| NSort s1, NSort 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
-| NInt i1, NInt i2 ->
- Uint63.equal i1 i2
-| NFloat f1, NFloat f2 ->
- Float64.equal f1 f2
-| NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
- Array.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) def1 def2
- && eq_notation_constr vars ty1 ty2
-| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
- | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> false
+let ldots_var = Id.of_string ".."
+
+let rec alpha_var id1 id2 = function
+ | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
+ | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
+ | _::idl -> alpha_var id1 id2 idl
+ | [] -> Id.equal id1 id2
+
+let cast_type_iter2 f t1 t2 = match t1, t2 with
+ | CastConv t1, CastConv t2 -> f t1 t2
+ | CastVM t1, CastVM t2 -> f t1 t2
+ | CastCoerce, CastCoerce -> ()
+ | CastNative t1, CastNative t2 -> f t1 t2
+ | (CastConv _ | CastVM _ | CastCoerce | CastNative _), _ -> raise Exit
+
+(* used to update the notation variable with the local variables used
+ in NList and NBinderList, since the iterator has its own variable *)
+let replace_var i j var = j :: List.remove Id.equal i var
+
+(* When [lt] is [true], tell if [t1] is a strict refinement of [t2]
+ (this is a partial order, so returning [false] does not mean that
+ [t2] is finer than [t1]); when [lt] is false, tell if [t1] is the
+ same pattern as [t2] *)
+
+let compare_notation_constr lt (vars1,vars2) t1 t2 =
+ (* this is used to reason up to order of notation variables *)
+ let alphameta = ref [] in
+ (* this becomes true when at least one subterm is detected as strictly smaller *)
+ let strictly_lt = ref false in
+ (* this is the stack of inner of iter patterns for comparison with a
+ new iteration or the tail of a recursive pattern *)
+ let tail = ref [] in
+ let check_alphameta id1 id2 =
+ try if not (Id.equal (List.assoc id1 !alphameta) id2) then raise Exit
+ with Not_found ->
+ if (List.mem_assoc id1 !alphameta) then raise Exit;
+ alphameta := (id1,id2) :: !alphameta in
+ let check_eq_id (vars1,vars2) renaming id1 id2 =
+ let ismeta1 = List.mem_f Id.equal id1 vars1 in
+ let ismeta2 = List.mem_f Id.equal id2 vars2 in
+ match ismeta1, ismeta2 with
+ | true, true -> check_alphameta id1 id2
+ | false, false -> if not (alpha_var id1 id2 renaming) then raise Exit
+ | false, true ->
+ if not lt then raise Exit
+ else
+ (* a binder which is not bound in the notation can be
+ considered as strictly more precise since it prevents the
+ notation variables in its scope to be bound by this binder;
+ i.e. it is strictly more precise in the sense that it
+ covers strictly less patterns than a notation where the
+ same binder is bound in the notation; this is hawever
+ disputable *)
+ strictly_lt := true
+ | true, false -> if not lt then raise Exit in
+ let check_eq_name vars renaming na1 na2 =
+ match na1, na2 with
+ | Name id1, Name id2 -> check_eq_id vars renaming id1 id2; (id1,id2)::renaming
+ | Anonymous, Anonymous -> renaming
+ | Anonymous, Name _ when lt -> renaming
+ | _ -> raise Exit in
+ let rec aux (vars1,vars2 as vars) renaming t1 t2 = match t1, t2 with
+ | NVar id1, NVar id2 when id1 = ldots_var && id2 = ldots_var -> ()
+ | _, NVar id2 when lt && id2 = ldots_var -> tail := t1 :: !tail
+ | NVar id1, _ when lt && id1 = ldots_var -> tail := t2 :: !tail
+ | NVar id1, NVar id2 -> check_eq_id vars renaming id1 id2
+ | NHole _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> ()
+ | NVar id1, NHole (_, _, _) when lt && List.mem_f Id.equal id1 vars1 -> ()
+ | _, NVar id2 when lt && List.mem_f Id.equal id2 vars2 -> strictly_lt := true
+ | NRef gr1, NRef gr2 when GlobRef.equal gr1 gr2 -> ()
+ | NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *)
+ | _, NHole (_, _, _) when lt -> strictly_lt := true
+ | NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+ | NBinderList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+ if b1 <> b2 then raise Exit;
+ let vars1 = replace_var i1 j1 vars1 in
+ let vars2 = replace_var i2 j2 vars2 in
+ check_alphameta i1 i2; aux (vars1,vars2) renaming iter1 iter2; aux vars renaming tail1 tail2;
+ | NBinderList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
+ | NList (i1, j1, iter1, tail1, b1), NBinderList (i2, j2, iter2, tail2, b2) ->
+ (* They may overlap on a unique iteration of them *)
+ let vars1 = replace_var i1 j1 vars1 in
+ let vars2 = replace_var i2 j2 vars2 in
+ aux (vars1,vars2) renaming iter1 iter2;
+ aux vars renaming tail1 tail2
+ | t1, NList (i2, j2, iter2, tail2, b2)
+ | t1, NBinderList (i2, j2, iter2, tail2, b2) when lt ->
+ (* checking if t1 is a finite iteration of the pattern *)
+ let vars2 = replace_var i2 j2 vars2 in
+ aux (vars1,vars2) renaming t1 iter2;
+ let t1 = List.hd !tail in
+ tail := List.tl !tail;
+ (* either matching a new iteration, or matching the tail *)
+ (try aux vars renaming t1 tail2 with Exit -> aux vars renaming t1 t2)
+ | NList (i1, j1, iter1, tail1, b1), t2
+ | NBinderList (i1, j1, iter1, tail1, b1), t2 when lt ->
+ (* we see the NList as a single iteration *)
+ let vars1 = replace_var i1 j1 vars1 in
+ aux (vars1,vars2) renaming iter1 t2;
+ let t2 = match !tail with
+ | t::rest -> tail := rest; t
+ | _ -> (* ".." is in a discarded fine-grained position *) raise Exit in
+ (* it had to be a single iteration of iter1 *)
+ aux vars renaming tail1 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) ->
+ (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) ->
+ aux vars renaming b1 b2;
+ Option.iter2 (aux vars renaming) t1 t2;(* TODO : subtyping? *)
+ let renaming = check_eq_name vars renaming na1 na2 in
+ aux vars renaming u1 u2
+ | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (* FIXME? *)
+ let check_pat (p1, t1) (p2, t2) =
+ if not (List.equal cases_pattern_eq p1 p2) then raise Exit; (* TODO: subtyping and renaming *)
+ aux vars renaming t1 t2
+ in
+ let eqf renaming (t1, (na1, o1)) (t2, (na2, o2)) =
+ aux vars renaming t1 t2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ let eq renaming (i1, n1) (i2, n2) =
+ if not (Ind.CanOrd.equal i1 i2) then raise Exit;
+ List.fold_left2 (check_eq_name vars) renaming n1 n2 in
+ Option.fold_left2 eq renaming o1 o2 in
+ let renaming = List.fold_left2 eqf renaming r1 r2 in
+ Option.iter2 (aux vars renaming) o1 o2;
+ List.iter2 check_pat p1 p2
+ | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) ->
+ aux vars renaming t1 t2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ Option.iter2 (aux vars renaming) o1 o2;
+ let renaming' = List.fold_left2 (check_eq_name vars) renaming nas1 nas2 in
+ aux vars renaming' u1 u2
+ | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) ->
+ aux vars renaming t1 t2;
+ aux vars renaming u1 u2;
+ aux vars renaming r1 r2;
+ let renaming = check_eq_name vars renaming na1 na2 in
+ Option.iter2 (aux vars renaming) o1 o2
+ | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (* FIXME? *)
+ let eq renaming (na1, o1, t1) (na2, o2, t2) =
+ Option.iter2 (aux vars renaming) o1 o2;
+ aux vars renaming t1 t2;
+ check_eq_name vars renaming na1 na2
+ in
+ let renaming = Array.fold_left2 (fun r id1 id2 -> check_eq_id vars r id1 id2; (id1,id2)::r) renaming ids1 ids2 in
+ let renamings = Array.map2 (List.fold_left2 eq renaming) ts1 ts2 in
+ Array.iter3 (aux vars) renamings us1 us2;
+ Array.iter3 (aux vars) (Array.map ((@) renaming) renamings) rs1 rs2
+ | NSort s1, NSort s2 when glob_sort_eq s1 s2 -> ()
+ | NCast (t1, c1), NCast (t2, c2) ->
+ aux vars renaming t1 t2;
+ cast_type_iter2 (aux vars renaming) c1 c2
+ | NInt i1, NInt i2 when Uint63.equal i1 i2 -> ()
+ | NFloat f1, NFloat f2 when Float64.equal f1 f2 -> ()
+ | NArray(t1,def1,ty1), NArray(t2,def2,ty2) ->
+ Array.iter2 (aux vars renaming) t1 t2;
+ aux vars renaming def1 def2;
+ aux vars renaming ty1 ty2
+ | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
+ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
+ | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _ | NArray _), _ -> raise Exit in
+ try
+ let _ = aux (vars1,vars2) [] t1 t2 in
+ if not lt then
+ (* Check that order of notation metavariables does not matter *)
+ List.iter2 check_alphameta vars1 vars2;
+ not lt || !strictly_lt
+ with Exit | (* Option.iter2: *) Option.Heterogeneous | Invalid_argument _ -> false
+
+let eq_notation_constr vars t1 t2 = t1 == t2 || compare_notation_constr false vars t1 t2
+
+let strictly_finer_notation_constr vars t1 t2 = compare_notation_constr true vars t1 t2
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -154,8 +258,6 @@ let rec subst_glob_vars l gc = DAst.map (function
| _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *)
) gc
-let ldots_var = Id.of_string ".."
-
type 'a binder_status_fun = {
no : 'a -> 'a;
restart_prod : 'a -> 'a;
@@ -174,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)
@@ -204,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') ->
@@ -225,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
@@ -258,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
(******************************************************************************)
@@ -275,6 +401,12 @@ type found_variables = {
let add_id r id = r := { !r with vars = id :: (!r).vars }
let add_name r = function Anonymous -> () | Name id -> add_id r id
+let mkNApp1 (g,a) =
+ match g with
+ (* Ensure flattening of nested applicative nodes *)
+ | NApp (g,args') -> NApp (g,args'@[a])
+ | _ -> NApp (g,[a])
+
let is_gvar id c = match DAst.get c with
| GVar id' -> Id.equal id id'
| _ -> false
@@ -443,9 +575,12 @@ let notation_constr_and_vars_of_glob_constr recvars a =
aux' c
and aux' x = DAst.with_val (function
| GVar id -> if not (Id.equal id ldots_var) then add_id found id; NVar id
- | GApp (g,args) -> NApp (aux g, List.map aux args)
- | 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)
+ | GApp (g,[]) -> NApp (aux g,[]) (* Encoding @foo *)
+ | 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_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
@@ -482,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 *)
@@ -590,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')
@@ -712,7 +850,21 @@ 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
+ | PatVar na -> Termops.add_vname vars na
+ | PatCstr (c, pl, na) -> List.fold_left push_pattern_binders (Termops.add_vname vars na) pl
+
+let rec push_context_binders vars = function
+ | [] -> vars
+ | b :: bl ->
+ let vars = match DAst.get b with
+ | GLocalAssum (na,_,_) -> Termops.add_vname vars na
+ | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars
+ | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in
+ push_context_binders vars bl
let is_term_meta id metas =
try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -729,8 +881,9 @@ 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
- (AsIdentOrPattern | AsStrictPattern)) -> true
+ (AsNameOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
+ | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
| _ -> false
with Not_found -> false
@@ -740,17 +893,11 @@ let is_bindinglist_meta id metas =
exception No_match
-let rec alpha_var id1 id2 = function
- | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
- | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
- | _::idl -> alpha_var id1 id2 idl
- | [] -> Id.equal id1 id2
-
let alpha_rename alpmetas v =
if alpmetas == [] then v
else try rename_glob_vars alpmetas v with UnsoundRenaming -> raise No_match
-let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
+let add_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var v =
(* Check that no capture of binding variables occur *)
(* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..."
with an actual term "fun z => ... z ..." when "x" is not bound in the
@@ -778,19 +925,19 @@ let add_env (alp,alpmetas) (terms,termlists,binders,binderlists) var v =
refinement *)
let v = alpha_rename alpmetas v in
(* TODO: handle the case of multiple occs in different scopes *)
- ((var,v)::terms,termlists,binders,binderlists)
+ ((var,(vars,v))::terms,termlists,binders,binderlists)
-let add_termlist_env (alp,alpmetas) (terms,termlists,binders,binderlists) var vl =
+let add_termlist_env (vars,(alp,alpmetas)) (terms,termlists,binders,binderlists) var vl =
if List.exists (fun (id,_) -> List.exists (occur_glob_constr id) vl) alp then raise No_match;
let vl = List.map (alpha_rename alpmetas) vl in
- (terms,(var,vl)::termlists,binders,binderlists)
+ (terms,(var,(vars,vl))::termlists,binders,binderlists)
-let add_binding_env alp (terms,termlists,binders,binderlists) var v =
+let add_binding_env (vars,alp) (terms,termlists,binders,binderlists) var v =
(* TODO: handle the case of multiple occs in different scopes *)
- (terms,termlists,(var,v)::binders,binderlists)
+ (terms,termlists,(var,(vars,v))::binders,binderlists)
-let add_bindinglist_env (terms,termlists,binders,binderlists) x bl =
- (terms,termlists,binders,(x,bl)::binderlists)
+let add_bindinglist_env (vars,alp) (terms,termlists,binders,binderlists) var bl =
+ (terms,termlists,binders,(var,(vars,bl))::binderlists)
let rec map_cases_pattern_name_left f = DAst.map (function
| PatVar na -> PatVar (f na)
@@ -801,7 +948,7 @@ let rec fold_cases_pattern_eq f x p p' =
let loc = p.CAst.loc in
match DAst.get p, DAst.get p' with
| PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
- | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
+ | PatCstr (c,l,na), PatCstr (c',l',na') when Construct.CanOrd.equal c c' ->
let x,l = fold_cases_pattern_list_eq f x l l' in
let x,na = f x na na' in
x, DAst.make ?loc @@ PatCstr (c,l,na)
@@ -818,7 +965,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
| PatVar na1, PatVar na2 -> Name.equal na1 na2
| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
- eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
+ Construct.CanOrd.equal c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
Name.equal na1 na2
| _ -> false
@@ -835,18 +982,19 @@ let rec pat_binder_of_term t = DAst.map (function
| _ -> raise No_match
) t
-let unify_name_upto alp na na' =
+let unify_name_upto (vars,alp) na na' =
match na, na' with
- | Anonymous, na' -> alp, na'
- | na, Anonymous -> alp, na
+ | Anonymous, na' -> (Termops.add_vname vars na',alp), na'
+ | na, Anonymous -> (Termops.add_vname vars na,alp), na
| Name id, Name id' ->
- if Id.equal id id' then alp, na'
- else (fst alp,(id,id')::snd alp), na'
+ let vars = Termops.add_vname vars na' in
+ if Id.equal id id' then (vars,alp), na'
+ else (vars,(fst alp,(id,id')::snd alp)), na'
let unify_pat_upto alp p p' =
try fold_cases_pattern_eq unify_name_upto alp p p' with Failure _ -> raise No_match
-let unify_term alp v v' =
+let unify_term (_,alp) v v' =
match DAst.get v, DAst.get v' with
| GHole _, _ -> v'
| _, GHole _ -> v
@@ -889,13 +1037,13 @@ let rec unify_binders_upto alp bl bl' =
alp, b :: bl
| _ -> raise No_match
-let unify_id alp id na' =
+let unify_id (_,alp) id na' =
match na' with
| Anonymous -> Name (rename_var (snd alp) id)
| Name id' ->
if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match
-let unify_pat alp p p' =
+let unify_pat (_,alp) p p' =
if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p'
else raise No_match
@@ -921,33 +1069,37 @@ let rec unify_terms_binders alp cl bl' =
let bind_term_env alp (terms,termlists,binders,binderlists as sigma) var v =
try
(* If already bound to a term, unify with the new term *)
- let v' = Id.List.assoc var terms in
+ let vars,v' = Id.List.assoc var terms in
let v'' = unify_term alp v v' in
if v'' == v' then sigma else
let sigma = (Id.List.remove_assoc var terms,termlists,binders,binderlists) in
- add_env alp sigma var v
+ add_env (Id.Set.union vars (fst alp),snd alp) sigma var v
with Not_found -> add_env alp sigma var v
let bind_termlist_env alp (terms,termlists,binders,binderlists as sigma) var vl =
try
(* If already bound to a list of term, unify with the new terms *)
- let vl' = Id.List.assoc var termlists in
+ let vars,vl' = Id.List.assoc var termlists in
let vl = unify_terms alp vl vl' in
let sigma = (terms,Id.List.remove_assoc var termlists,binders,binderlists) in
- add_termlist_env alp sigma var vl
+ add_termlist_env (Id.Set.union vars (fst alp),snd alp) sigma var vl
with Not_found -> add_termlist_env alp sigma var vl
let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) var id =
try
(* If already bound to a term, unify the binder and the term *)
- match DAst.get (Id.List.assoc var terms) with
- | GVar id' ->
- (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
- sigma
+ let vars',v' = Id.List.assoc var terms in
+ match DAst.get v' with
+ | GVar id' | GRef (GlobRef.VarRef id',None) ->
+ let (vars,(alpha,alpmetas)) = alp in
+ let vars = Id.Set.add id' vars in
+ let alpmetas = if not (Id.equal id id') then (id,id')::alpmetas else alpmetas in
+ (Id.Set.union vars' vars,(alpha,alpmetas)), sigma
| t ->
(* The term is a non-variable pattern *)
raise No_match
with Not_found ->
+ let alp = (Id.Set.add id (fst alp), snd alp) in
(* 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 *)
(* TODO: look at the consequences for alp *)
@@ -958,43 +1110,56 @@ let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma)
let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
try
(* If already bound to a binder, unify the term and the binder *)
- let patl' = Id.List.assoc var binders in
+ let vars,patl' = Id.List.assoc var binders in
let patl'' = List.map2 (unify_pat alp) [pat] patl' in
if patl' == patl'' then sigma
else
let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
- add_binding_env alp sigma var patl''
+ add_binding_env (Id.Set.union vars (fst alp),snd alp) sigma var patl''
with Not_found -> add_binding_env alp sigma var [pat]
let bind_binding_env alp (terms,termlists,binders,binderlists as sigma) var disjpat =
try
(* If already bound to a binder possibly *)
(* generating an alpha-renaming from unifying the new binder *)
- let disjpat' = Id.List.assoc var binders in
+ let vars,disjpat' = Id.List.assoc var binders in
+ (* if, maybe, there is eventually casts in patterns, the common types have *)
+ (* to exclude the spine of variable from the two locations they occur *)
+ let alp' = (Id.Set.union vars (fst alp),snd alp) in
let alp, disjpat = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in
let sigma = (terms,termlists,Id.List.remove_assoc var binders,binderlists) in
+ alp, add_binding_env alp' sigma var disjpat
+ with Not_found ->
+ (* Note: all patterns of the disjunction are supposed to have the same
+ variables, thus one is enough *)
+ let alp = (push_pattern_binders (fst alp) (List.hd disjpat), snd alp) in
alp, add_binding_env alp sigma var disjpat
- with Not_found -> alp, add_binding_env alp sigma var disjpat
let bind_bindinglist_env alp (terms,termlists,binders,binderlists as sigma) var bl =
let bl = List.rev bl in
try
(* If already bound to a list of binders possibly *)
(* generating an alpha-renaming from unifying the new binders *)
- let bl' = Id.List.assoc var binderlists in
+ let vars, bl' = Id.List.assoc var binderlists in
+ (* The shared subterm can be under two different spines of *)
+ (* variables (themselves bound in the notation) , so we take the *)
+ (* union of both locations *)
+ let alp' = (Id.Set.union vars (fst alp),snd alp) in
let alp, bl = unify_binders_upto alp bl bl' in
let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
- alp, add_bindinglist_env sigma var bl
+ alp, add_bindinglist_env alp' sigma var bl
with Not_found ->
- alp, add_bindinglist_env sigma var bl
+ let alp = (push_context_binders (fst alp) bl, snd alp) in
+ alp, add_bindinglist_env alp sigma var bl
let bind_bindinglist_as_termlist_env alp (terms,termlists,binders,binderlists) var cl =
try
(* If already bound to a list of binders, unify the terms and binders *)
- let bl' = Id.List.assoc var binderlists in
+ let vars,bl' = Id.List.assoc var binderlists in
let bl = unify_terms_binders alp cl bl' in
+ let alp = (Id.Set.union vars (fst alp),snd alp) in
let sigma = (terms,termlists,binders,Id.List.remove_assoc var binderlists) in
- add_bindinglist_env sigma var bl
+ add_bindinglist_env alp sigma var bl
with Not_found ->
anomaly (str "There should be a binder list bindings this list of terms.")
@@ -1028,7 +1193,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
| (Anonymous,Name id2) when is_term_meta id2 metas ->
(* We let the non-binding occurrence define the rhs *)
alp, sigma
- | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma
+ | (Name id1,Name id2) ->
+ let (vars,(alp,alpmetas)) = alp in
+ (vars,((id1,id2)::alp,alpmetas)),sigma
| (Anonymous,Anonymous) -> alp,sigma
| _ -> raise No_match
@@ -1041,7 +1208,7 @@ let rec match_cases_pattern_binders allow_catchall metas (alp,sigma as acc) pat1
| PatVar na1, PatVar na2 -> match_names metas acc na1 na2
| _, PatVar Anonymous when allow_catchall -> acc
| PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
- when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
+ when Construct.CanOrd.equal c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
List.fold_left2 (match_cases_pattern_binders false metas)
(match_names metas acc na1 na2) patl1 patl2
| _ -> raise No_match
@@ -1071,9 +1238,9 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
try
let metas = add_ldots_var (add_meta_bindinglist y metas) in
let (terms,_,_,binderlists as sigma) = match_fun alp metas sigma rest iter in
- let rest = Id.List.assoc ldots_var terms in
+ let _,rest = Id.List.assoc ldots_var terms in
let b =
- match Id.List.assoc y binderlists with [b] -> b | _ ->assert false
+ match Id.List.assoc y binderlists with _,[b] -> b | _ ->assert false
in
let sigma = remove_bindinglist_sigma y (remove_sigma ldots_var sigma) in
(* In case y is bound not only to a binder but also to a term *)
@@ -1102,18 +1269,20 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert =
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 =
+ let rec aux alp sigma acc rest =
try
let metas = add_ldots_var (add_meta_term y metas) in
let (terms,_,_,_ as sigma) = match_fun metas sigma rest iter in
- let rest = Id.List.assoc ldots_var terms in
- let t = Id.List.assoc y terms in
+ let _,rest = Id.List.assoc ldots_var terms in
+ let vars,t = Id.List.assoc y terms in
let sigma = remove_sigma y (remove_sigma ldots_var sigma) in
if !print_parentheses && not (List.is_empty acc) then raise No_match;
- aux sigma (t::acc) rest
+ (* The union is overkill at the current time because each term matches *)
+ (* at worst the same binder metavariable of the same pattern *)
+ aux (Id.Set.union vars (fst alp),snd alp) sigma (t::acc) rest
with No_match when not (List.is_empty acc) ->
- acc, match_fun metas sigma rest termin in
- let l,(terms,termlists,binders,binderlists as sigma) = aux sigma [] rest in
+ alp, acc, match_fun metas sigma rest termin in
+ let alp,l,(terms,termlists,binders,binderlists as sigma) = aux alp sigma [] rest in
let l = if revert then l else List.rev l in
if is_bindinglist_meta x metas then
(* This is a recursive pattern for both bindings and terms; it is *)
@@ -1147,16 +1316,22 @@ let does_not_come_from_already_eta_expanded_var glob =
(* checked). *)
match DAst.get glob with GVar _ -> false | _ -> true
+let is_var_term = function
+ (* The kind of expressions allowed to be both a term and a binding variable *)
+ | GVar _ -> true
+ | GRef (GlobRef.VarRef _,None) -> true
+ | _ -> false
+
let rec match_ inner u alp metas sigma a1 a2 =
let open CAst in
let loc = a1.loc in
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
- | 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_var_term r1 && 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_var_term r1 && is_onlybinding_strict_meta id2 metas -> raise No_match
+ | r1, NVar id2 when is_var_term r1 && 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
(* Matching recursive notations for terms *)
@@ -1168,7 +1343,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
match_binderlist (match_hd u) alp metas sigma a1 x y iter termin revert
(* Matching compositionally *)
- | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
+ | GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> 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
@@ -1182,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
@@ -1253,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
@@ -1280,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
@@ -1338,9 +1517,9 @@ and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)}
(alp,sigma) disjpatl1 disjpatl2 in
match_in u alp metas sigma rhs1 rhs2
-let match_notation_constr u c (metas,pat) =
+let match_notation_constr ~print_univ c ~vars (metas,pat) =
let terms,termlists,binders,binderlists =
- match_ false u ([],[]) metas ([],[],[],[]) c pat in
+ match_ false print_univ (vars,([],[])) metas ([],[],[],[]) c pat in
(* Turning substitution based on binding/constr distinction into a
substitution based on entry productions *)
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders',binderlists') ->
@@ -1350,11 +1529,11 @@ let match_notation_constr u c (metas,pat) =
((term, scl)::terms',termlists',binders',binderlists')
| NtnTypeBinder (NtnBinderParsedAsConstr _) ->
(match Id.List.assoc x binders with
- | [pat] ->
+ | vars,[pat] ->
let v = glob_constr_of_cases_pattern (Global.env()) pat in
- ((v,scl)::terms',termlists',binders',binderlists')
+ (((vars,v),scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
- | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
+ | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
(terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
| NtnTypeConstrList ->
(terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
@@ -1391,11 +1570,11 @@ 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),(false,0,[])
| PatVar Anonymous, NHole _ -> sigma,(false,0,[])
- | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when Construct.CanOrd.equal r1 r2 ->
let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
sigma,(false,0,l)
| PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
- when eq_constructor r1 r2 ->
+ when Construct.CanOrd.equal r1 r2 ->
let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
let le2 = List.length l2 in
if le2 > List.length l1
@@ -1418,10 +1597,10 @@ and match_cases_pattern_no_more_args metas sigma a1 a2 =
let match_ind_pattern metas sigma ind pats a2 =
match a2 with
- | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
+ | NRef (GlobRef.IndRef r2) when Ind.CanOrd.equal ind r2 ->
sigma,(false,0,pats)
| NApp (NRef (GlobRef.IndRef r2),l2)
- when eq_ind ind r2 ->
+ when Ind.CanOrd.equal ind r2 ->
let le2 = List.length l2 in
if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length pats
then
@@ -1436,9 +1615,8 @@ let reorder_canonically_substitution terms termlists metas =
List.fold_right (fun (x,(scl,typ)) (terms',termlists') ->
match typ with
| NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists')
- | NtnTypeBinder _ -> assert false
| NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists')
- | NtnTypeBinderList -> assert false)
+ | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation."))
metas ([],[])
let match_notation_constr_cases_pattern c (metas,pat) =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 3cc6f82ec8..e7a0429b35 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -16,6 +16,11 @@ open Glob_term
val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+val strictly_finer_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
+(** Tell if [t1] is a strict refinement of [t2]
+ (this is a partial order and returning [false] does not mean that
+ [t2] is finer than [t1]) *)
+
(** Substitution of kernel names in interpretation data *)
val subst_interpretation :
@@ -48,7 +53,7 @@ val apply_cases_pattern : ?loc:Loc.t ->
(Id.t list * cases_pattern_disjunction) * Id.t -> glob_constr -> glob_constr
val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
- ('a -> Name.t -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t) ->
+ ('a -> Name.t -> glob_constr option -> 'a * ((Id.t list * cases_pattern_disjunction) * Id.t) option * Name.t * Glob_term.binding_kind * glob_constr option) ->
('a -> notation_constr -> glob_constr) -> ?h:'a binder_status_fun ->
'a -> notation_constr -> glob_constr
@@ -63,10 +68,11 @@ exception No_match
val print_parentheses : bool ref
-val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
- ('a glob_constr_g * extended_subscopes) list * ('a glob_constr_g list * extended_subscopes) list *
- ('a cases_pattern_disjunction_g * extended_subscopes) list *
- ('a extended_glob_local_binder_g list * extended_subscopes) list
+val match_notation_constr : print_univ:bool -> 'a glob_constr_g -> vars:Id.Set.t -> interpretation ->
+ ((Id.Set.t * 'a glob_constr_g) * extended_subscopes) list *
+ ((Id.Set.t * 'a glob_constr_g list) * extended_subscopes) list *
+ ((Id.Set.t * 'a cases_pattern_disjunction_g) * extended_subscopes) list *
+ ((Id.Set.t * 'a extended_glob_local_binder_g list) * extended_subscopes) list
val match_notation_constr_cases_pattern :
'a cases_pattern_g -> interpretation ->
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 82238b71b7..c541a19bfd 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -27,8 +27,8 @@ type notation_constr =
| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
| NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
(* Part only in [glob_constr] *)
- | NLambda of Name.t * notation_constr * notation_constr
- | NProd of Name.t * notation_constr * notation_constr
+ | NLambda of Name.t * notation_constr option * notation_constr
+ | NProd of Name.t * notation_constr option * notation_constr
| NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
| NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
| NCases of Constr.case_style * notation_constr option *
@@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes
type constr_as_binder_kind =
| AsIdent
- | AsIdentOrPattern
+ | AsName
+ | AsNameOrPattern
| AsStrictPattern
type notation_binder_source =
@@ -76,8 +77,12 @@ type notation_binder_source =
| NtnParsedAsPattern of bool
(* This accepts only ident *)
| NtnParsedAsIdent
+ (* This accepts only name *)
+ | NtnParsedAsName
(* This accepts ident, or pattern, or both *)
| NtnBinderParsedAsConstr of constr_as_binder_kind
+ (* This accepts ident, _, and quoted pattern *)
+ | NtnParsedAsBinder
type notation_var_instance_type =
| NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
diff --git a/interp/numTok.mli b/interp/numTok.mli
index bcfe663dd2..386a25f042 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -8,20 +8,20 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** Numerals in different forms: signed or unsigned, possibly with
+(** Numbers in different forms: signed or unsigned, possibly with
fractional part and exponent.
- Numerals are represented using raw strings of (hexa)decimal
+ Numbers are represented using raw strings of (hexa)decimal
literals and a separate sign flag.
Note that this representation is not unique, due to possible
multiple leading or trailing zeros, and -0 = +0, for instances.
- The reason to keep the numeral exactly as it was parsed is that
- specific notations can be declared for specific numerals
+ The reason to keep the number exactly as it was parsed is that
+ specific notations can be declared for specific numbers
(e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
[Notation "2e1" := ...]). Those notations override the generic
- interpretation as numeral. So, one has to record the form of the
- numeral which exactly matches the notation. *)
+ interpretation as number. So, one has to record the form of the
+ number which exactly matches the notation. *)
type sign = SPlus | SMinus
@@ -44,7 +44,7 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val classify : t -> num_class
@@ -69,7 +69,7 @@ sig
val to_bigint : t -> Z.t
end
-(** {6 Unsigned decimal numerals } *)
+(** {6 Unsigned decimal numbers } *)
module Unsigned :
sig
@@ -80,12 +80,12 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val parse : char Stream.t -> t
- (** Parse a positive Coq numeral.
+ (** Parse a positive Coq number.
Precondition: the first char on the stream is already known to be a digit (\[0-9\]).
- Precondition: at least two extra chars after the numeral to parse.
+ Precondition: at least two extra chars after the number to parse.
The recognized syntax is:
- integer part: \[0-9\]\[0-9_\]*
@@ -97,13 +97,13 @@ sig
- exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
val parse_string : string -> t option
- (** Parse the string as a non negative Coq numeral, if possible *)
+ (** Parse the string as a non negative Coq number, if possible *)
val classify : t -> num_class
end
-(** {6 Signed decimal numerals } *)
+(** {6 Signed decimal numbers } *)
module Signed :
sig
@@ -117,10 +117,10 @@ sig
val sprint : t -> string
val print : t -> Pp.t
- (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+ (** [sprint] and [print] returns the number as it was parsed, for printing *)
val parse_string : string -> t option
- (** Parse the string as a signed Coq numeral, if possible *)
+ (** Parse the string as a signed Coq number, if possible *)
val of_int_string : string -> t
(** Convert from a string in the syntax of OCaml's int/int64 *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 4418a32645..274d3655d3 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -28,7 +28,7 @@ type key =
(** TODO: share code from Notation *)
let key_compare k1 k2 = match k1, k2 with
-| RefKey gr1, RefKey gr2 -> GlobRef.Ordered.compare gr1 gr2
+| RefKey gr1, RefKey gr2 -> GlobRef.CanOrd.compare gr1 gr2
| RefKey _, Oth -> -1
| Oth, RefKey _ -> 1
| Oth, Oth -> 0
@@ -119,7 +119,7 @@ let revert_reserved_type t =
then I've introduced a bug... *)
let filter _ pat =
try
- let _ = match_notation_constr false t ([], pat) in
+ let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in
true
with No_match -> false
in
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 33d8aa6064..46baa00c74 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -50,6 +50,16 @@ let locate_global_with_alias ?(head=false) qid =
user_err ?loc:qid.CAst.loc (pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
+let global_constant_with_alias qid =
+ try match locate_global_with_alias qid with
+ | Names.GlobRef.ConstRef c -> c
+ | ref ->
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not a reference to a constant.")
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+
let global_inductive_with_alias qid =
try match locate_global_with_alias qid with
| Names.GlobRef.IndRef ind -> ind
@@ -60,6 +70,16 @@ let global_inductive_with_alias qid =
let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid
+let global_constructor_with_alias qid =
+ try match locate_global_with_alias qid with
+ | Names.GlobRef.ConstructRef c -> c
+ | ref ->
+ user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+ (pr_qualid qid ++ spc () ++ str "is not a constructor of an inductive type.")
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+
let global_with_alias ?head qid =
try locate_global_with_alias ?head qid
with Not_found as exn ->
@@ -72,9 +92,17 @@ let smart_global ?(head = false) = let open Constrexpr in CAst.with_loc_val (fun
| ByNotation (ntn,sc) ->
Notation.interp_notation_as_global_reference ?loc ~head (fun _ -> true) ntn sc)
-let smart_global_inductive = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
- | AN r ->
- global_inductive_with_alias r
+let smart_global_kind f dest is = let open Constrexpr in CAst.with_loc_val (fun ?loc -> function
+ | AN r -> f r
| ByNotation (ntn,sc) ->
- destIndRef
- (Notation.interp_notation_as_global_reference ?loc ~head:false isIndRef ntn sc))
+ dest
+ (Notation.interp_notation_as_global_reference ?loc ~head:false is ntn sc))
+
+let smart_global_constant =
+ smart_global_kind global_constant_with_alias destConstRef isConstRef
+
+let smart_global_inductive =
+ smart_global_kind global_inductive_with_alias destIndRef isIndRef
+
+let smart_global_constructor =
+ smart_global_kind global_constructor_with_alias destConstructRef isConstructRef
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 9b24a62086..26f2a4f36d 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -28,11 +28,23 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t
a reference. *)
val global_with_alias : ?head:bool -> qualid -> GlobRef.t
+(** The same for constants *)
+val global_constant_with_alias : qualid -> Constant.t
+
(** The same for inductive types *)
val global_inductive_with_alias : qualid -> inductive
+(** The same for constructors of an inductive type *)
+val global_constructor_with_alias : qualid -> constructor
+
(** Locate a reference taking into account notations and "aliases" *)
val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t
+(** The same for constants *)
+val smart_global_constant : qualid Constrexpr.or_by_notation -> Constant.t
+
(** The same for inductive types *)
val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive
+
+(** The same for constructors of an inductive type *)
+val smart_global_constructor : qualid Constrexpr.or_by_notation -> constructor
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 70be55f843..a953ca8898 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -37,6 +37,9 @@ let wit_pre_ident : string uniform_genarg_type =
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
+let wit_nat_or_var =
+ make0 ~dyn:(val_tag (topwit wit_nat)) "nat_or_var"
+
let wit_ident =
make0 "ident"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index bd34af5543..0a8fdf53b1 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -35,6 +35,8 @@ val wit_pre_ident : string uniform_genarg_type
val wit_int_or_var : (int or_var, int or_var, int) genarg_type
+val wit_nat_or_var : (int or_var, int or_var, int) genarg_type
+
val wit_ident : Id.t uniform_genarg_type
val wit_hyp : (lident, lident, Id.t) genarg_type
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index bd3e234a91..f3ad3546ff 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -22,6 +22,7 @@ type syndef =
{ syndef_pattern : interpretation;
syndef_onlyparsing : bool;
syndef_deprecation : Deprecation.t option;
+ syndef_also_in_cases_pattern : bool;
}
let syntax_table =
@@ -52,7 +53,7 @@ let open_syntax_constant i ((sp,kn),(_local,syndef)) =
if not syndef.syndef_onlyparsing then
(* Redeclare it to be used as (short) name in case an other (distfix)
notation was declared in between *)
- Notation.declare_uninterpretation (Notation.SynDefRule kn) pat
+ Notation.declare_uninterpretation ~also_in_cases_pattern:syndef.syndef_also_in_cases_pattern (Notation.SynDefRule kn) pat
end
let cache_syntax_constant d =
@@ -81,11 +82,12 @@ let in_syntax_constant : (bool * syndef) -> obj =
subst_function = subst_syntax_constant;
classify_function = classify_syntax_constant }
-let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
+let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat =
let syndef =
{ syndef_pattern = pat;
syndef_onlyparsing = onlyparsing;
syndef_deprecation = deprecation;
+ syndef_also_in_cases_pattern = also_in_cases_pattern;
}
in
let _ = add_leaf id (in_syntax_constant (local,syndef)) in ()
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 66a3132f2a..31f685152c 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,7 +13,7 @@ open Notation_term
(** Syntactic definitions. *)
-val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
+val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Id.t ->
onlyparsing:bool -> interpretation -> unit
val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 07:09:58 +0000