aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml63
-rw-r--r--interp/constrextern.mli1
-rw-r--r--interp/constrintern.ml21
-rw-r--r--interp/constrintern.mli4
-rw-r--r--interp/dune2
-rw-r--r--interp/notation.ml91
-rw-r--r--interp/notation.mli8
-rw-r--r--interp/notation_ops.ml42
-rw-r--r--interp/notation_term.ml2
-rw-r--r--interp/numTok.ml2
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/smartlocate.ml6
-rw-r--r--interp/syntax_def.ml2
13 files changed, 152 insertions, 100 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f3ba884856..3cabf52197 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -64,7 +64,7 @@ let print_parentheses = Notation_ops.print_parentheses
(* This forces printing universe names of Type{.} *)
let print_universes = Detyping.print_universes
-(* This suppresses printing of primitive tokens (e.g. numeral) and notations *)
+(* This suppresses printing of notations *)
let print_no_symbol = ref false
(* This tells to skip types if a variable has this type by default *)
@@ -74,6 +74,9 @@ let print_use_implicit_types =
~key:["Printing";"Use";"Implicit";"Types"]
~value:true
+(* Print primitive tokens, like strings *)
+let print_raw_literal = ref false
+
(**********************************************************************)
let hole = CAst.make @@ CHole (None, IntroAnonymous, None)
@@ -434,7 +437,7 @@ let extern_record_pattern cstrsp args =
(* Better to use extern_glob_constr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
try
- if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.in_debugger || !Flags.raw_print || !print_raw_literal then raise No_match;
let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
@@ -853,6 +856,7 @@ let same_binder_type ty nal c =
(* one with no delimiter if possible) *)
let extern_possible_prim_token (custom,scopes) r =
+ if !print_raw_literal then raise No_match;
let (n,key) = uninterp_prim_token r scopes in
match availability_of_entry_coercion custom InConstrEntrySomeLevel with
| None -> raise No_match
@@ -969,7 +973,13 @@ let rec extern inctx ?impargs scopes vars r =
with No_match -> extern inctx scopes vars r')
| None ->
- try extern_notations inctx scopes vars None r
+ let r' = match DAst.get r with
+ | GInt i when Coqlib.has_ref "num.int63.wrap_int" ->
+ let wrap = Coqlib.lib_ref "num.int63.wrap_int" in
+ DAst.make (GApp (DAst.make (GRef (wrap, None)), [r]))
+ | _ -> r in
+
+ try extern_notations inctx scopes vars None r'
with No_match ->
let loc = r.CAst.loc in
@@ -1123,7 +1133,7 @@ let rec extern inctx ?impargs scopes vars r =
| GInt i ->
extern_prim_token_delimiter_if_required
- (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
+ (Number NumTok.(Signed.of_bigint CHex (Z.of_int64 (Uint63.to_int64 i))))
"int63" "int63_scope" (snd scopes)
| GFloat f -> extern_float f (snd scopes)
@@ -1255,11 +1265,12 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
make ?loc (pll,extern inctx scopes vars c)
and extern_notations inctx scopes vars nargs t =
- if !Flags.raw_print || !print_no_symbol then raise No_match;
+ if !Flags.raw_print then raise No_match;
try extern_possible_prim_token scopes t
with No_match ->
- let t = flatten_application t in
- extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+ if !print_no_symbol then raise No_match;
+ let t = flatten_application t in
+ extern_notation inctx scopes vars t (filter_enough_applied nargs (uninterp_notations t))
and extern_notation inctx (custom,scopes as allscopes) vars t rules =
match rules with
@@ -1463,23 +1474,33 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PIf (c,b1,b2) ->
GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
- | PCase ({cip_style=Constr.LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
- let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
+ | PCase ({cip_style=Constr.LetStyle},None,tm,[(0,n,b)]) ->
+ let n, b = glob_of_pat_under_context avoid env sigma (n, b) in
+ let nal = Array.to_list n in
GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
let mat = match bl, info.cip_ind with
| [], _ -> []
| _, Some ind ->
- let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
- simple_cases_matrix_of_branches ind bl'
+ let map (i, n, c) =
+ let n, c = glob_of_pat_under_context avoid env sigma (n, c) in
+ let nal = Array.to_list n in
+ let mkPatVar na = DAst.make @@ PatVar na in
+ let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
+ let ids = List.map_filter Nameops.Name.to_option nal in
+ CAst.make @@ (ids,[p],c)
+ in
+ List.map map bl
| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
in
let mat = if info.cip_extensible then mat @ [any_any_branch] else mat
in
- let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
- | PMeta None, _, _ -> (Anonymous,None),None
- | _, Some ind, Some nargs ->
- return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
+ let indnames,rtn = match p, info.cip_ind with
+ | None, _ -> (Anonymous,None),None
+ | Some p, Some ind ->
+ let nas, p = glob_of_pat_under_context avoid env sigma p in
+ let nas = Array.rev_to_list nas in
+ ((List.hd nas, Some (CAst.make (ind, List.tl nas))), Some p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
GCases (Constr.RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
@@ -1523,6 +1544,18 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
let glob_of = glob_of_pat avoid env sigma in
GArray (None, Array.map glob_of t, glob_of def, glob_of ty)
+and glob_of_pat_under_context avoid env sigma (nas, pat) =
+ let fold (avoid, env, nas, epat) na =
+ let na, avoid = compute_displayed_name_in_pattern sigma avoid na epat in
+ let env = Termops.add_name na env in
+ let epat = match epat with PLambda (_, _, p) -> p | _ -> assert false in
+ (avoid, env, na :: nas, epat)
+ in
+ let epat = Array.fold_right (fun na p -> PLambda (na, PMeta None, p)) nas pat in
+ let (avoid', env', nas, _) = Array.fold_left fold (avoid, env, [], epat) nas in
+ let pat = glob_of_pat avoid' env' sigma pat in
+ (Array.rev_of_list nas, pat)
+
let extern_constr_pattern env sigma pat =
extern true (InConstrEntrySomeLevel,(None,[]))
(* XXX no vars? *)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 298b52f0be..bb49c8697d 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -60,6 +60,7 @@ val print_parentheses : bool ref
val print_universes : bool ref
val print_no_symbol : bool ref
val print_projections : bool ref
+val print_raw_literal : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 70a4ea35e9..7c63ebda3a 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -244,6 +244,8 @@ let contract_curly_brackets_pat ntn (l,ll) =
type local_univs = { bound : Univ.Level.t Id.Map.t; unb_univs : bool }
+let empty_local_univs = { bound = Id.Map.empty; unb_univs = false }
+
type intern_env = {
ids: Id.Set.t;
unb: bool;
@@ -1202,6 +1204,11 @@ let intern_sort ~local_univs s =
let intern_instance ~local_univs us =
Option.map (List.map (map_glob_sort_gen (intern_sort_name ~local_univs))) us
+let try_interp_name_alias = function
+ | [], { CAst.v = CRef (ref,u) } ->
+ NRef (intern_reference ref,intern_instance ~local_univs:empty_local_univs u)
+ | _ -> raise Not_found
+
(* 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
@@ -1251,16 +1258,16 @@ let intern_qualid_for_pattern test_global intern_not qid pats =
| SynDef kn ->
let filter (vars,a) =
match a with
- | NRef g ->
+ | NRef (g,_) ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_global g;
let () = assert (List.is_empty vars) in
Some (g, Some [], pats)
- | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
+ | NApp (NRef (g,_),[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
test_global g;
let () = assert (List.is_empty vars) in
Some (g, None, pats)
- | NApp (NRef g,args) ->
+ | NApp (NRef (g,_),args) ->
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_global g;
let nvars = List.length vars in
@@ -1330,7 +1337,7 @@ 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;
- local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *)
+ local_univs = empty_local_univs;(* <- doesn't matter here *)
tmp_scope = None; scopes = []; impls = empty_internalization_env;
binder_block_names = None}
Environ.empty_named_context_val
@@ -1784,10 +1791,10 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
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 ->
+ | NRef (g,_) ->
ensure_kind test_kind ?loc g;
DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true false [] args)
- | NApp (NRef g,ntnpl) ->
+ | NApp (NRef (g,_),ntnpl) ->
ensure_kind test_kind ?loc g;
let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in
let no_impl =
@@ -2554,7 +2561,7 @@ let interp_notation_constr env ?(impls=empty_internalization_env) nenv a =
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;
- local_univs = { bound = Id.Map.empty; unb_univs = false };
+ local_univs = empty_local_univs;
tmp_scope = None; scopes = []; impls; binder_block_names = None}
false (empty_ltac_sign, vl) a
in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index f92a54e23f..65b63962d0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -150,6 +150,10 @@ val interp_constr_pattern :
(** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
val intern_reference : qualid -> GlobRef.t
+(** For syntactic definitions: check if abbreviation to a name
+ and avoid early insertion of maximal implicit arguments *)
+val try_interp_name_alias : 'a list * constr_expr -> notation_constr
+
(** Expands abbreviations (syndef); raise an error if not existing *)
val interp_reference : ltac_sign -> qualid -> glob_constr
diff --git a/interp/dune b/interp/dune
index 6d73d5724c..793ce48ea3 100644
--- a/interp/dune
+++ b/interp/dune
@@ -1,6 +1,6 @@
(library
(name interp)
(synopsis "Coq's Syntactic Interpretation for AST [notations, implicits]")
- (public_name coq.interp)
+ (public_name coq-core.interp)
(wrapped false)
(libraries zarith pretyping))
diff --git a/interp/notation.ml b/interp/notation.ml
index f2d113954b..4010c3487e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -400,12 +400,12 @@ let cases_pattern_key c = match DAst.get c with
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
- | NApp (NRef ref,args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
- | NList (_,_,NApp (NRef ref,args),_,_)
- | NBinderList (_,_,NApp (NRef ref,args),_,_) ->
+ | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), AppBoundedNotation (List.length args)
+ | NList (_,_,NApp (NRef (ref,_),args),_,_)
+ | 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') ->
+ | 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')
@@ -548,15 +548,15 @@ type number_ty =
hexadecimal : Names.inductive;
number : Names.inductive }
+type pos_neg_int63_ty =
+ { pos_neg_int63_ty : Names.inductive }
+
type target_kind =
| 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 *)
+ | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
| 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 number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
@@ -869,30 +869,16 @@ let mkDecHex ind c n = match c with
| CDec -> mkApp (mkConstruct (ind, 1), [|n|]) (* (UInt|Int|)Decimal *)
| CHex -> mkApp (mkConstruct (ind, 2), [|n|]) (* (UInt|Int|)Hexadecimal *)
-exception NonDecimal
-
-let decimal_coqnumber_of_rawnum inds n =
- if NumTok.Signed.classify n <> CDec then raise NonDecimal;
- coqnumber_of_rawnum inds CDec n
-
let coqnumber_of_rawnum inds n =
let c = NumTok.Signed.classify n in
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;
- coquint_of_rawnum inds CDec (Some n)
-
let coquint_of_rawnum inds n =
let c = NumTok.UnsignedNat.classify n in
let n = coquint_of_rawnum inds c (Some n) in
mkDecHex inds.uint c n
-let decimal_coqint_of_rawnum inds n =
- if NumTok.SignedNat.classify n <> CDec then raise NonDecimal;
- coqint_of_rawnum inds CDec n
-
let coqint_of_rawnum inds n =
let c = NumTok.SignedNat.classify n in
let n = coqint_of_rawnum inds c n in
@@ -947,23 +933,14 @@ let destDecHex c = match Constr.kind c with
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
-let decimal_rawnum_of_coqnumber c =
- rawnum_of_coqnumber CDec c
-
let rawnum_of_coqnumber c =
let cl, c = destDecHex c in
rawnum_of_coqnumber cl c
-let decimal_rawnum_of_coquint c =
- rawnum_of_coquint CDec c
-
let rawnum_of_coquint c =
let cl, c = destDecHex c in
rawnum_of_coquint cl c
-let decimal_rawnum_of_coqint c =
- rawnum_of_coqint CDec c
-
let rawnum_of_coqint c =
let cl, c = destDecHex c in
rawnum_of_coqint cl c
@@ -1038,12 +1015,22 @@ let error_negative ?loc =
let error_overflow ?loc n =
CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "overflow in int63 literal: " ++ str (Z.to_string n))
-let interp_int63 ?loc n =
+let error_underflow ?loc n =
+ CErrors.user_err ?loc ~hdr:"interp_int63" Pp.(str "underflow in int63 literal: " ++ str (Z.to_string n))
+
+let coqpos_neg_int63_of_bigint ?loc ind (sign,n) =
+ let uint = int63_of_pos_bigint ?loc n in
+ let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
+ mkApp (mkConstruct (ind, pos_neg), [|uint|])
+
+let interp_int63 ?loc ind n =
+ let sign = if Z.(compare n zero >= 0) then SPlus else SMinus in
+ let n = Z.abs n in
if Z.(leq zero n)
then
if Z.(lt n (pow z_two 63))
- then int63_of_pos_bigint ?loc n
- else error_overflow ?loc n
+ then coqpos_neg_int63_of_bigint ?loc ind (sign,n)
+ else match sign with SPlus -> error_overflow ?loc n | SMinus -> error_underflow ?loc n
else error_negative ?loc
let bigint_of_int63 c =
@@ -1051,6 +1038,15 @@ let bigint_of_int63 c =
| Int i -> Z.of_int64 (Uint63.to_int64 i)
| _ -> raise NotAValidPrimToken
+let bigint_of_coqpos_neg_int63 c =
+ match Constr.kind c with
+ | App (c,[|c'|]) ->
+ (match Constr.kind c with
+ | Construct ((_,1), _) (* Pos *) -> bigint_of_int63 c'
+ | Construct ((_,2), _) (* Neg *) -> Z.neg (bigint_of_int63 c')
+ | _ -> raise NotAValidPrimToken)
+ | _ -> raise NotAValidPrimToken
+
let interp o ?loc n =
begin match o.warning, n with
| Warning threshold, n when NumTok.Signed.is_bigger_int_than n threshold ->
@@ -1062,22 +1058,13 @@ let interp o ?loc n =
coqint_of_rawnum int_ty n
| UInt int_ty, Some (SPlus, n) ->
coquint_of_rawnum int_ty n
- | DecimalInt int_ty, Some n ->
- (try decimal_coqint_of_rawnum int_ty n
- with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
- | DecimalUInt int_ty, Some (SPlus, n) ->
- (try decimal_coquint_of_rawnum int_ty n
- with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
| Z z_pos_ty, Some n ->
z_of_bigint z_pos_ty (NumTok.SignedNat.to_bigint n)
- | Int63, Some n ->
- interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
- | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
+ | Int63 pos_neg_int63_ty, Some n ->
+ interp_int63 ?loc pos_neg_int63_ty.pos_neg_int63_ty (NumTok.SignedNat.to_bigint n)
+ | (Int _ | UInt _ | Z _ | Int63 _), _ ->
no_such_prim_token "number" ?loc o.ty_name
| 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
let sigma = Evd.from_env env in
@@ -1100,11 +1087,8 @@ let uninterp o n =
| (Int _, c) -> NumTok.Signed.of_int (rawnum_of_coqint c)
| (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)
+ | (Int63 _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_coqpos_neg_int63 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_coqnumber c
end o n
end
@@ -1357,6 +1341,7 @@ let find_with_delimiters = function
match (String.Map.find scope !scope_map).delimiters with
| Some key -> Some (Some scope, Some key)
| None -> None
+ | exception Not_found -> None
let rec find_without_delimiters find (ntn_scope,ntn) = function
| OpenScopeItem scope :: scopes ->
@@ -2353,8 +2338,8 @@ let browse_notation strict ntn map =
let global_reference_of_notation ~head test (ntn,sc,(on_parsing,on_printing,{not_interp = (_,c)})) =
match c with
- | NRef ref when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
- | NApp (NRef ref, l) when head || List.for_all isNVar_or_NHole l && test ref ->
+ | NRef (ref,_) when test ref -> Some (on_parsing,on_printing,ntn,sc,ref)
+ | NApp (NRef (ref,_), l) when head || List.for_all isNVar_or_NHole l && test ref ->
Some (on_parsing,on_printing,ntn,sc,ref)
| _ -> None
diff --git a/interp/notation.mli b/interp/notation.mli
index 97955bf92e..195f2a4416 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -137,15 +137,15 @@ type number_ty =
hexadecimal : Names.inductive;
number : Names.inductive }
+type pos_neg_int63_ty =
+ { pos_neg_int63_ty : Names.inductive }
+
type target_kind =
| 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 *)
+ | Int63 of pos_neg_int63_ty (* Coq.Numbers.Cyclic.Int63.PrimInt63.pos_neg_int63 *)
| 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 number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
type string_target_kind =
| ListByte
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 0e7f085bde..ea5e2a1ad4 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -43,6 +43,28 @@ let cast_type_iter2 f t1 t2 = match t1, t2 with
in NList and NBinderList, since the iterator has its own variable *)
let replace_var i j var = j :: List.remove Id.equal i var
+(* compare_glob_universe_instances true strictly_lt us1 us2 computes us1 <= us2,
+ compare_glob_universe_instances false strictly_lt us1 us2 computes us1 = us2.
+ strictly_lt will be set to true if any part is strictly less. *)
+let compare_glob_universe_instances lt strictly_lt us1 us2 =
+ match us1, us2 with
+ | None, None -> true
+ | Some _, None -> strictly_lt := true; lt
+ | None, Some _ -> false
+ | Some l1, Some l2 ->
+ CList.for_all2eq (fun u1 u2 ->
+ match u1, u2 with
+ | UAnonymous {rigid=true}, UAnonymous {rigid=true} -> true
+ | UAnonymous {rigid=false}, UAnonymous {rigid=false} -> true
+ | UAnonymous _, UAnonymous _ -> false
+ | UNamed _, UAnonymous _ -> strictly_lt := true; lt
+ | UAnonymous _, UNamed _ -> false
+ | UNamed _, UNamed _ -> glob_level_eq u1 u2) l1 l2
+
+(* Compute us1 <= us2, as a boolean *)
+let compare_glob_universe_instances_le us1 us2 =
+ compare_glob_universe_instances true (ref false) us1 us2
+
(* 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
@@ -93,7 +115,7 @@ let compare_notation_constr lt (vars1,vars2) t1 t2 =
| 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 -> ()
+ | NRef (gr1,u1), NRef (gr2,u2) when GlobRef.equal gr1 gr2 && compare_glob_universe_instances lt strictly_lt u1 u2 -> ()
| NHole (_, _, _), NHole (_, _, _) -> () (* FIXME? *)
| _, NHole (_, _, _) when lt -> strictly_lt := true
| NList (i1, j1, iter1, tail1, b1), NList (i2, j2, iter2, tail2, b2)
@@ -377,7 +399,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f ?(h=default_binder_stat
| NCast (c,k) -> GCast (f e c,map_cast_type (f (h.slide e)) k)
| NSort x -> GSort x
| NHole (x, naming, arg) -> GHole (x, naming, arg)
- | NRef x -> GRef (x,None)
+ | NRef (x,u) -> GRef (x,u)
| NInt i -> GInt i
| NFloat f -> GFloat f
| NArray (t,def,ty) -> GArray(None, Array.map (f e) t, f e def, f e ty)
@@ -612,7 +634,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
NHole (w, naming, arg)
- | GRef (r,_) -> NRef r
+ | GRef (r,u) -> NRef (r,u)
| GArray (_u,t,def,ty) -> NArray (Array.map aux t, aux def, aux ty)
| GEvar _ | GPatVar _ ->
user_err Pp.(str "Existential variables not allowed in notations.")
@@ -706,10 +728,10 @@ let rec subst_pat subst pat =
let rec subst_notation_constr subst bound raw =
match raw with
- | NRef ref ->
+ | NRef (ref,u) ->
let ref',t = subst_global subst ref in
if ref' == ref then raw else (match t with
- | None -> NRef ref'
+ | None -> NRef (ref',u)
| Some t ->
fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
@@ -1344,7 +1366,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* Matching compositionally *)
| GVar id1, NVar id2 when alpha_var id1 id2 (fst (snd alp)) -> sigma
- | GRef (r1,_), NRef r2 when (GlobRef.equal r1 r2) -> sigma
+ | GRef (r1,u1), NRef (r2,u2) when (GlobRef.equal r1 r2) && compare_glob_universe_instances_le u1 u2 -> sigma
| GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
@@ -1570,10 +1592,10 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
match DAst.get a1, a2 with
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
| PatVar Anonymous, NHole _ -> sigma,(false,0,[])
- | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when Construct.CanOrd.equal r1 r2 ->
+ | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2,None) 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)
+ | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2,None),l2)
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
@@ -1597,9 +1619,9 @@ 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 Ind.CanOrd.equal ind r2 ->
+ | NRef (GlobRef.IndRef r2,None) when Ind.CanOrd.equal ind r2 ->
sigma,(false,0,pats)
- | NApp (NRef (GlobRef.IndRef r2),l2)
+ | NApp (NRef (GlobRef.IndRef r2,None),l2)
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
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index c541a19bfd..2979447cf8 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -21,7 +21,7 @@ open Glob_term
type notation_constr =
(* Part common to [glob_constr] and [cases_pattern] *)
- | NRef of GlobRef.t
+ | NRef of GlobRef.t * glob_level list option
| NVar of Id.t
| NApp of notation_constr * notation_constr list
| NHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
diff --git a/interp/numTok.ml b/interp/numTok.ml
index 124a6cd249..12ef33717a 100644
--- a/interp/numTok.ml
+++ b/interp/numTok.ml
@@ -85,7 +85,7 @@ struct
let string_of_nonneg_bigint c n =
match c with
| CDec -> Z.format "%d" n
- | CHex -> Z.format "0x%x" n
+ | CHex -> Z.format "%#x" n
let of_bigint c n =
let sign, n = if Int.equal (-1) (Z.sign n) then (SMinus, Z.neg n) else (SPlus, n) in
(sign, string_of_nonneg_bigint c n)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 274d3655d3..07160dcf6f 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -71,10 +71,10 @@ let reserve_table = Summary.ref Id.Map.empty ~name:"reserved-type"
let reserve_revtable = Summary.ref KeyMap.empty ~name:"reserved-type-rev"
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
- | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
- | NList (_,_,NApp (NRef ref,args),_,_)
- | NBinderList (_,_,NApp (NRef ref,args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
- | NRef ref -> RefKey(canonical_gr ref), None
+ | NApp (NRef (ref,_),args) -> RefKey(canonical_gr ref), Some (List.length args)
+ | NList (_,_,NApp (NRef (ref,_),args),_,_)
+ | NBinderList (_,_,NApp (NRef (ref,_),args),_,_) -> RefKey (canonical_gr ref), Some (List.length args)
+ | NRef (ref,_) -> RefKey(canonical_gr ref), None
| _ -> Oth, None
let cache_reserved_type (_,(id,t)) =
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 46baa00c74..91d05f7317 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -26,7 +26,7 @@ let global_of_extended_global_head = function
| SynDef kn ->
let _, syn_def = search_syntactic_definition kn in
let rec head_of = function
- | NRef ref -> ref
+ | NRef (ref,None) -> ref
| NApp (rc, _) -> head_of rc
| NCast (rc, _) -> head_of rc
| NLetIn (_, _, _, rc) -> head_of rc
@@ -37,8 +37,8 @@ let global_of_extended_global = function
| TrueGlobal ref -> ref
| SynDef kn ->
match search_syntactic_definition kn with
- | [],NRef ref -> ref
- | [],NApp (NRef ref,[]) -> ref
+ | [],NRef (ref,None) -> ref
+ | [],NApp (NRef (ref,None),[]) -> ref
| _ -> raise Not_found
let locate_global_with_alias ?(head=false) qid =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f3ad3546ff..39e628883a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -40,7 +40,7 @@ let load_syntax_constant i ((sp,kn),(_local,syndef)) =
Nametab.push_syndef (Nametab.Until i) sp kn
let is_alias_of_already_visible_name sp = function
- | _,NRef ref ->
+ | _,NRef (ref,_) ->
let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in
DirPath.is_empty dir && Id.equal id (basename sp)
| _ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 10:26:23 +0000