aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml37
-rw-r--r--interp/constrexpr_ops.ml28
-rw-r--r--interp/constrextern.ml57
-rw-r--r--interp/constrintern.ml199
-rw-r--r--interp/constrintern.mli13
-rw-r--r--interp/declare.ml23
-rw-r--r--interp/implicit_quantifiers.ml36
-rw-r--r--interp/interp.mllib1
-rw-r--r--interp/notation.ml144
-rw-r--r--interp/notation.mli17
-rw-r--r--interp/notation_ops.ml13
-rw-r--r--interp/notation_term.ml2
-rw-r--r--interp/numTok.ml52
-rw-r--r--interp/numTok.mli18
14 files changed, 397 insertions, 243 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 757d186c8b..9f778d99e9 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -48,16 +48,26 @@ type abstraction_kind = AbsLambda | AbsPi
type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-(** Representation of integer literals that appear in Coq scripts.
- We now use raw strings of digits in base 10 (big-endian), and a separate
- sign flag. Note that this representation is not unique, due to possible
- multiple leading zeros, and -0 = +0 *)
-
-type sign = bool
-type raw_natural_number = string
+(** Representation of decimal literals that appear in Coq scripts.
+ We now use raw strings following the format defined by
+ [NumTok.t] 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
+ (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
+ [Notation "2e1" := ...]). Those notations, which override the
+ generic interpretation as numeral, use the same representation of
+ numeral using the Numeral constructor. So the latter should be able
+ to record the form of the numeral which exactly matches the
+ notation. *)
+
+type sign = SPlus | SMinus
+type raw_numeral = NumTok.t
type prim_token =
- | Numeral of raw_natural_number * sign
+ | Numeral of sign * raw_numeral
| String of string
type instance_expr = Glob_term.glob_level list
@@ -124,16 +134,17 @@ and branch_expr =
(cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr =
- lident * (lident option * recursion_order_expr) *
+ lident * recursion_order_expr option *
local_binder_expr list * constr_expr * constr_expr
and cofix_expr =
lident * local_binder_expr list * constr_expr * constr_expr
-and recursion_order_expr =
- | CStructRec
- | CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+and recursion_order_expr_r =
+ | CStructRec of lident
+ | CWfRec of lident * constr_expr
+ | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
+and recursion_order_expr = recursion_order_expr_r CAst.t
(* Anonymous defs allowed ?? *)
and local_binder_expr =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 95a0039b0a..443473d5b6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -50,13 +50,14 @@ let names_of_local_binders bl =
(**********************************************************************)
(* Functions on constr_expr *)
-(* Note: redundant Numeral representations such as -0 and +0 (or different
- numbers of leading zeros) are considered different here. *)
+(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+ are considered different here. *)
let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2
+| Numeral (SPlus,n1), Numeral (SPlus,n2)
+| Numeral (SMinus,n1), Numeral (SMinus,n2) -> NumTok.equal n1 n2
| String s1, String s2 -> String.equal s1 s2
-| _ -> false
+| (Numeral ((SPlus|SMinus),_) | String _), _ -> false
let explicitation_eq ex1 ex2 = match ex1, ex2 with
| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
@@ -195,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
constr_expr_eq e1 e2
-and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
+and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
(eq_ast Id.equal id1 id2) &&
- Option.equal (eq_ast Id.equal) j1 j2 &&
- recursion_order_expr_eq r1 r2 &&
+ 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
@@ -209,13 +209,17 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
-and recursion_order_expr_eq r1 r2 = match r1, r2 with
- | CStructRec, CStructRec -> true
- | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2
- | CMeasureRec (e1, o1), CMeasureRec (e2, o2) ->
+and recursion_order_expr_eq_r r1 r2 = match r1, r2 with
+ | CStructRec i1, CStructRec i2 -> eq_ast Id.equal 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 &&
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 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
@@ -348,7 +352,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
| CFix (_,l) ->
let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
- List.fold_right (fun (_,(_,o),lb,t,c) acc ->
+ List.fold_right (fun (_,ro,lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c2afa097bb..3b169edaab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -212,7 +212,7 @@ let encode_record r =
module PrintingRecordRecord =
PrintingInductiveMake (struct
- let encode = encode_record
+ let encode _env = encode_record
let field = "Record"
let title = "Types leading to pretty-printing using record notation: "
let member_message s b =
@@ -224,7 +224,7 @@ module PrintingRecordRecord =
module PrintingRecordConstructor =
PrintingInductiveMake (struct
- let encode = encode_record
+ let encode _env = encode_record
let field = "Constructor"
let title = "Types leading to pretty-printing using constructor form: "
let member_message s b =
@@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l
let add_patt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l
let add_cpatt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -318,29 +318,28 @@ let drop_implicits_in_patt cst nb_expl args =
let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
-let is_number s =
- let rec aux i =
- Int.equal (String.length s) i ||
- match s.[i] with '0'..'9' -> aux (i+1) | _ -> false
- in aux 0
-
let is_zero s =
let rec aux i =
Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
in aux 0
+let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
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,true))] when not (is_zero p) ->
+ | "- _", [Some (Numeral (SPlus,p))] when not (is_zero p) ->
assert (bl=[]);
mknot (loc,ntn,([mknot (loc,(InConstrEntrySomeLevel,"( _ )"),l,[])]),[])
| _ ->
match decompose_notation_key ntn, l with
- | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] when is_number x ->
- mkprim (loc, Numeral (x,false))
- | (InConstrEntrySomeLevel,[Terminal x]), [] when is_number x ->
- mkprim (loc, Numeral (x,true))
+ | (InConstrEntrySomeLevel,[Terminal "-"; Terminal x]), [] ->
+ begin match NumTok.of_string x with
+ | Some n -> mkprim (loc, Numeral (SMinus,n))
+ | None -> mknot (loc,ntn,l,bl) end
+ | (InConstrEntrySomeLevel,[Terminal x]), [] ->
+ begin match NumTok.of_string x with
+ | Some n -> mkprim (loc, Numeral (SPlus,n))
+ | None -> mknot (loc,ntn,l,bl) end
| _ -> mknot (loc,ntn,l,bl)
let make_notation loc ntn (terms,termlists,binders,binderlists as subst) =
@@ -365,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
- let nb_params = Inductiveops.inductive_nparams ind in
+ let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
List.exists (fun (_,impls) ->
(List.length impls >= nb_params) &&
let params,args = Util.List.chop nb_params impls in
@@ -527,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi
let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
- if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
+ if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
let c = extern_reference vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
@@ -939,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
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 n =
- match fst nv.(i) with
- | None -> None
- | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
- in
- let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ let n =
+ match nv.(i) with
+ | None -> None
+ | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
+ in
+ ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -969,7 +967,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
CCast (sub_extern true scopes vars c,
map_cast_type (extern_typ scopes vars) c')
| GInt i ->
- CPrim(Numeral (Uint63.to_string i,true))
+ CPrim(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
in insert_coercion coercion (CAst.make ?loc c)
@@ -1160,13 +1158,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
let lonely_seen = add_lonely keyrule lonely_seen in
extern_notation allscopes lonely_seen vars t rules
-and extern_recursion_order scopes vars = function
- GStructRec -> CStructRec
- | GWfRec c -> CWfRec (extern true scopes vars c)
- | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
- Option.map (extern true scopes vars) r)
-
-
let extern_glob_constr vars c =
extern false (InConstrEntrySomeLevel,(None,[])) vars c
@@ -1295,7 +1286,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
let v = Array.map3
(fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
bl tl ln in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi),
Array.map (fun (bl,_,_) -> bl) v,
Array.map (fun (_,_,ty) -> ty) v,
Array.map (fun (_,bd,_) -> bd) v)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 349402035c..c0801067ce 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -96,21 +96,6 @@ let is_global id =
with Not_found ->
false
-let global_reference_of_reference qid =
- locate_reference qid
-
-let global_reference id =
- locate_reference (qualid_of_ident id)
-
-let construct_reference ctx id =
- try
- VarRef (let _ = Context.Named.lookup id ctx in id)
- with Not_found ->
- global_reference id
-
-let global_reference_in_absolute_module dir id =
- Nametab.global_of_path (Libnames.make_path dir id)
-
(**********************************************************************)
(* Internalization errors *)
@@ -658,7 +643,7 @@ let terms_of_binders bl =
| PatCstr (c,l,_) ->
let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
- let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+ let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables l = match l with
| bnd :: l ->
@@ -753,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
else
let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
match disjpat with
- | [pat] -> (glob_constr_of_cases_pattern pat, None)
+ | [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
@@ -815,7 +800,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
else
let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
match disjpat with
- | [pat] -> glob_constr_of_cases_pattern pat
+ | [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
@@ -1033,7 +1018,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
| TrueGlobal (VarRef _) when no_secvar ->
(* Rule out section vars since these should have been found by intern_var *)
raise Not_found
- | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args
+ | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), Some ref, args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in
let nids = List.length ids in
@@ -1043,7 +1028,6 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
let terms = make_subst ids (List.map fst args1) in
let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
let infos = (Id.Map.empty, env) in
- let projapp = match c with NRef _ -> true | _ -> false in
let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
let loc = c.loc in
let err () =
@@ -1067,33 +1051,60 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid)
| Some _, _ -> err ()
in
- c, projapp, args2
+ c, None, args2
+
+let warn_nonprimitive_projection =
+ CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled
+ Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
+
+let error_nonprojection_syntax ?loc qid =
+ CErrors.user_err ?loc ~hdr:"nonprojection-syntax" Pp.(pr_qualid qid ++ str" is not a projection.")
+
+let check_applied_projection isproj realref qid =
+ match isproj with
+ | None -> ()
+ | Some projargs ->
+ let is_prim = match realref with
+ | None | Some (IndRef _ | ConstructRef _ | VarRef _) -> false
+ | Some (ConstRef c) ->
+ if Recordops.is_primitive_projection c then true
+ else if Recordops.is_projection c then false
+ else error_nonprojection_syntax ?loc:qid.loc qid
+ (* TODO check projargs, note we will need implicit argument info *)
+ in
+ if not is_prim then warn_nonprimitive_projection ?loc:qid.loc qid
-let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid =
+let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us args qid =
let loc = qid.CAst.loc in
if qualid_is_ident qid then
- try intern_var env lvar namedctx loc (qualid_basename qid) us, args
+ try
+ let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
+ check_applied_projection isproj None qid;
+ res, args
with Not_found ->
try
- let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
+ let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
+ check_applied_projection isproj realref qid;
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
with Not_found ->
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
+ (* check_applied_projection ?? *)
(gvar (loc,qualid_basename qid) us, [], [], []), args
else Nametab.error_global_not_found qid
else
- let r,projapp,args2 =
+ let r,realref,args2 =
try intern_qualid qid intern env ntnvars us args
with Not_found -> Nametab.error_global_not_found qid
in
+ check_applied_projection isproj realref qid;
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
let interp_reference vars r =
let (r,_,_,_),_ =
- intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None)
+ intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env}
Environ.empty_named_context_val
@@ -1186,10 +1197,10 @@ let check_or_pat_variables loc ids idsl =
@return if letin are included *)
let check_constructor_length env loc cstr len_pl pl0 =
let n = len_pl + List.length pl0 in
- if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
- (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
+ if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else
+ (Int.equal n (Inductiveops.constructor_nalldecls env cstr) ||
(error_wrong_numarg_constructor ?loc env cstr
- (Inductiveops.constructor_nrealargs cstr)))
+ (Inductiveops.constructor_nrealargs env cstr)))
open Declarations
@@ -1215,9 +1226,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with
have been given in the "explicit" arguments, which come from a
"@C args" notation or from a custom user notation *)
let pl' = insert_local_defs_in_pattern cstr pl in
- let maxargs = Inductiveops.constructor_nalldecls cstr in
+ let maxargs = Inductiveops.constructor_nalldecls env cstr in
if List.length pl' + List.length args > maxargs then
- error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr);
+ error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
(* Two possibilities: either the args are given with explict
variables for local definitions, then we give the explicit args
extended with local defs, so that there is nothing more to be
@@ -1247,15 +1258,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
in aux 0 (impl_list,pl2)
let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
- let nargs = Inductiveops.constructor_nallargs c in
- let nargs' = Inductiveops.constructor_nalldecls c in
+ let nargs = Inductiveops.constructor_nallargs env c in
+ let nargs' = Inductiveops.constructor_nalldecls env c in
let impls_st = implicits_of_global (ConstructRef c) in
add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
nargs nargs' impls_st len_pl1 pl2
let add_implicits_check_ind_length env loc c len_pl1 pl2 =
- let nallargs = inductive_nallargs_env env c in
- let nalldecls = inductive_nalldecls_env env c in
+ let nallargs = inductive_nallargs env c in
+ let nalldecls = inductive_nalldecls env c in
let impls_st = implicits_of_global (IndRef c) in
add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
nallargs nalldecls impls_st len_pl1 pl2
@@ -1263,8 +1274,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 =
(** Do not raise NotEnoughArguments thanks to preconditions*)
let chop_params_pattern loc ind args with_letin =
let nparams = if with_letin
- then Inductiveops.inductive_nparamdecls ind
- else Inductiveops.inductive_nparams ind in
+ then Inductiveops.inductive_nparamdecls (Global.env()) ind
+ else Inductiveops.inductive_nparams (Global.env()) ind in
assert (nparams <= List.length args);
let params,args = List.chop nparams args in
List.iter (fun c -> match DAst.get c with
@@ -1284,10 +1295,11 @@ let find_constructor loc add_params ref =
in
cstr, match add_params with
| Some nb_args ->
+ let env = Global.env () in
let nb =
- if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
- then Inductiveops.inductive_nparamdecls ind
- else Inductiveops.inductive_nparams ind
+ if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr)
+ then Inductiveops.inductive_nparamdecls env ind
+ else Inductiveops.inductive_nparams env ind
in
List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
| None -> []
@@ -1328,7 +1340,7 @@ let sort_fields ~complete loc fields completer =
| (first_field_ref, first_field_value):: other_fields ->
let (first_field_glob_ref, record) =
try
- let gr = global_reference_of_reference first_field_ref in
+ let gr = locate_reference first_field_ref in
(gr, Recordops.find_projection gr)
with Not_found ->
raise (InternalizationError(loc, NotAProjection first_field_ref))
@@ -1386,7 +1398,7 @@ let sort_fields ~complete loc fields completer =
let rec index_fields fields remaining_projs acc =
match fields with
| (field_ref, field_value) :: fields ->
- let field_glob_ref = try global_reference_of_reference field_ref
+ let field_glob_ref = try locate_reference field_ref
with Not_found ->
user_err ?loc ~hdr:"intern"
(str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
@@ -1461,8 +1473,9 @@ let alias_of als = match als.alias_ids with
let is_zero s =
let rec aux i =
- Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+ Int.equal (String.length s) i || ((s.[i] == '0' || s.[i] == '_') && aux (i+1))
in aux 0
+let is_zero n = is_zero n.NumTok.int && is_zero n.NumTok.frac
let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
@@ -1487,11 +1500,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, true)) } -> not (is_zero p)
+| { CAst.v = CPrim (Numeral (SPlus, p)) } -> not (is_zero p)
| _ -> false
let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral (p, true)) } -> not (is_zero p)
+| { CAst.v = CPatPrim (Numeral (SPlus, p)) } -> not (is_zero p)
| _ -> false
let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
@@ -1602,8 +1615,8 @@ let drop_notations_pattern looked_for genv =
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, [])
| CPatNotation ((InConstrEntrySomeLevel,"- _"),([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 (p,false)) scopes in
+ 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
rcp_of_glob scopes pat
| CPatNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[]),[]) ->
in_pat top scopes a
@@ -1827,56 +1840,49 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let rec intern env = CAst.with_loc_val (fun ?loc -> function
| CRef (ref,us) ->
let (c,imp,subscopes,l),_ =
- intern_applied_reference intern env (Environ.named_context_val globalenv)
- lvar us [] ref
+ intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
+ lvar us [] ref
in
apply_impargs c env imp subscopes l loc
- | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+ | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
- let n =
- try List.index0 Id.equal iddef lf
+ let n =
+ try List.index0 Id.equal iddef lf
with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (false,iddef)))
- in
- let idl_temp = Array.map
- (fun (id,(n,order),bl,ty,_) ->
- let intern_ro_arg f =
- let before, after = split_at_annot bl n in
- let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
- let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
- | GLocalAssum _ -> true
- | _ -> false (* remove let-ins *))
- rbefore) n in
- n', ro, List.fold_left intern_local_binder (env',rbefore) after
- in
- let n, ro, (env',rbl) =
- match order with
- | CStructRec ->
- intern_ro_arg (fun _ -> GStructRec)
- | CWfRec c ->
- intern_ro_arg (fun f -> GWfRec (f c))
- | CMeasureRec (m,r) ->
- intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
- in
- let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
- ((n, ro), bl, intern_type env' ty, env')) dl in
+ raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+ in
+ let idl_temp = Array.map
+ (fun (id,recarg,bl,ty,_) ->
+ let recarg = Option.map (function { CAst.v = v } -> match v with
+ | CStructRec i -> i
+ | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+ in
+ let before, after = split_at_annot bl recarg in
+ let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+ let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
+ | GLocalAssum _ -> true
+ | _ -> false (* remove let-ins *))
+ rbefore) recarg in
+ let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in
+ let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
+ (n, bl, intern_type env' ty, env')) dl in
let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
- let env'' = List.fold_left_i (fun i en name ->
- let (_,bli,tyi,_) = idl_temp.(i) in
- let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
- push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
- en (CAst.make @@ Name name)) 0 env' lf in
- (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
- DAst.make ?loc @@
- GRec (GFix
- (Array.map (fun (ro,_,_,_) -> ro) idl,n),
+ let env'' = List.fold_left_i (fun i en name ->
+ let (_,bli,tyi,_) = idl_temp.(i) in
+ let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+ push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
+ en (CAst.make @@ Name name)) 0 env' lf in
+ (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+ DAst.make ?loc @@
+ GRec (GFix
+ (Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
+
| CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
let dl = Array.of_list dl in
@@ -1918,8 +1924,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
GLetIn (na.CAst.v, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation ((InConstrEntrySomeLevel,"- _"), ([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 (p,false)))
+ let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
+ intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
| CNotation ((InConstrEntrySomeLevel,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (ntn,args) ->
intern_notation intern env ntnvars loc ntn args
@@ -1933,30 +1939,31 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CAppExpl ((isproj,ref,us), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
- intern_applied_reference intern env (Environ.named_context_val globalenv)
- lvar us args ref
+ intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
+ lvar us args ref
in
(* Rem: GApp(_,f,[]) stands for @f *)
if args = [] then DAst.make ?loc @@ GApp (f,[]) else
smart_gapp f loc (intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
- let f,args = match f.CAst.v with
+ let isproj,f,args = match f.CAst.v with
(* Compact notations like "t.(f args') args" *)
- | CApp ((Some _,f), args') when not (Option.has_some isproj) ->
- f,args'@args
+ | CApp ((Some _ as isproj',f), args') when not (Option.has_some isproj) ->
+ isproj',f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
- | _ -> f,args in
+ | _ -> isproj,f,args in
let (c,impargs,args_scopes,l),args =
match f.CAst.v with
| CRef (ref,us) ->
- intern_applied_reference intern env
+ intern_applied_reference ~isproj intern env
(Environ.named_context_val globalenv) lvar us args ref
| CNotation (ntn,([],[],[],[])) ->
+ assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
(x,impl,scopes,l), args
- | _ -> (intern env f,[],[],[]), args in
+ | _ -> assert (Option.is_empty isproj); (intern env f,[],[],[]), args in
apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2d14a0d0a7..0d4bc91f57 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -162,24 +162,11 @@ val interp_context_evars :
env -> evar_map -> local_binder_expr list ->
evar_map * (internalization_env * ((env * rel_context) * Impargs.manual_implicits))
-(* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *)
-(* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *)
-(* ?global_level:bool -> ?impl_env:internalization_env -> *)
-(* env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
-
-(* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *)
-(* env -> evar_map -> local_binder_expr list -> *)
-(* internalization_env * *)
-(* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *)
-
(** Locating references of constructions, possibly via a syntactic definition
(these functions do not modify the glob file) *)
val locate_reference : Libnames.qualid -> GlobRef.t
val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
-val global_reference : Id.t -> GlobRef.t
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
(** Interprets a term as the left-hand side of a notation. The returned map is
guaranteed to have the same domain as the input one. *)
diff --git a/interp/declare.ml b/interp/declare.ml
index 08a6ac5f7b..76b4bab2ce 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -119,7 +119,6 @@ let set_declare_scheme f = declare_scheme := f
let update_tables c =
declare_constant_implicits c;
- Heads.declare_head (EvalConstRef c);
Notation.declare_ref_arguments_scope Evd.empty (ConstRef c)
let register_side_effect (c, role) =
@@ -257,7 +256,6 @@ let declare_variable id obj =
let oname = add_leaf id (inVariable (Inr (id,obj))) in
declare_var_implicits id;
Notation.declare_ref_arguments_scope Evd.empty (VarRef id);
- Heads.declare_head (EvalVarRef id);
oname
(** Declaration of inductive blocks *)
@@ -348,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj =
discharge_function = discharge_inductive;
rebuild_function = rebuild_inductive }
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.subst_constant subst c
+
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
+
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
+ declare_object {
+ (default_object "PRIMPROJS") with
+ cache_function = cache_prim ;
+ load_function = load_prim;
+ subst_function = subst_prim;
+ classify_function = (fun x -> Substitute x);
+ discharge_function = discharge_prim }
+
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
+
let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
let id = Label.to_id label in
let univs, u = match univs with
@@ -362,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
let entry = definition_entry ~types ~univs term in
let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
- Recordops.declare_primitive_projection p cst
+ declare_primitive_projection p cst
let declare_projections univs mind =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 854651e7b7..dffccf02fc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty =
| Some ({CAst.loc;v=(id, par, inst)}, gr) ->
let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
let c, avoid =
- let c = class_info gr in
- let (ci, rd) = c.cl_context in
- if not allow_partial then
- begin
- let opt_succ x n = match x with
- | None -> succ n
- | Some _ -> n
- in
- let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
- let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
- if not (Int.equal needlen applen) then
- mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
- end;
- let pars = List.rev (List.combine ci rd) in
- let args, avoid = combine_params avoid f par pars in
- CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
- in c, avoid
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let c = class_info env sigma gr in
+ let (ci, rd) = c.cl_context in
+ if not allow_partial then
+ begin
+ let opt_succ x n = match x with
+ | None -> succ n
+ | Some _ -> n
+ in
+ let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+ let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+ if not (Int.equal needlen applen) then
+ mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+ end;
+ let pars = List.rev (List.combine ci rd) in
+ let args, avoid = combine_params avoid f par pars in
+ CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
+ in c, avoid
let warn_ignoring_implicit_status =
CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 147eaf20dc..1262dbb181 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,4 @@
+NumTok
Constrexpr
Tactypes
Stdarg
diff --git a/interp/notation.ml b/interp/notation.ml
index bc68d97bb8..56504db04e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -476,7 +476,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
(* Interpreting numbers (not in summary because functional objects) *)
type required_module = full_path * string list
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
type prim_token_uid = string
@@ -499,15 +499,20 @@ module InnerPrimToken = struct
| StringInterp f, StringInterp f' -> f == f'
| _ -> false
- let ofNumeral n s =
- if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+ let ofNumeral s n =
+ let n = String.(concat "" (split_on_char '_' n)) in
+ match s with
+ | SPlus -> Bigint.of_string n
+ | SMinus -> Bigint.neg (Bigint.of_string n)
let do_interp ?loc interp primtok =
match primtok, interp with
- | Numeral (n,s), RawNumInterp interp -> interp ?loc (n,s)
- | Numeral (n,s), BigNumInterp interp -> interp ?loc (ofNumeral n s)
+ | Numeral (s,n), RawNumInterp interp -> interp ?loc (s,n)
+ | Numeral (s,{ NumTok.int = n; frac = ""; exp = "" }),
+ BigNumInterp interp -> interp ?loc (ofNumeral s n)
| String s, StringInterp interp -> interp ?loc s
- | _ -> raise Not_found
+ | (Numeral _ | String _),
+ (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
type uninterpreter =
| RawNumUninterp of (any_glob_constr -> rawnum option)
@@ -521,15 +526,17 @@ module InnerPrimToken = struct
| _ -> false
let mkNumeral n =
- if Bigint.is_pos_or_zero n then Numeral (Bigint.to_string n, true)
- else Numeral (Bigint.to_string (Bigint.neg n), false)
+ if Bigint.is_pos_or_zero n then
+ Numeral (SPlus,NumTok.int (Bigint.to_string n))
+ else
+ Numeral (SMinus,NumTok.int (Bigint.to_string (Bigint.neg 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 (n,s) -> Numeral (n,s)) (u g)
+ | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
| BigNumUninterp u -> Option.map mkNumeral (u g)
| StringUninterp u -> mkString (u g)
@@ -559,8 +566,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
type numnot_option =
| Nop
- | Warning of raw_natural_number
- | Abstract of raw_natural_number
+ | Warning of string
+ | Abstract of string
type int_ty =
{ uint : Names.inductive;
@@ -570,11 +577,16 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
+type decimal_ty =
+ { int : int_ty;
+ decimal : Names.inductive }
+
type target_kind =
| Int of int_ty (* Coq.Init.Decimal.int + uint *)
| UInt of Names.inductive (* Coq.Init.Decimal.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+ | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
type string_target_kind =
| ListByte
@@ -606,20 +618,18 @@ module PrimTokenNotation = struct
At least [c] is known to be evar-free, since it comes from
our own ad-hoc [constr_of_glob] or from conversions such
as [coqint_of_rawnum].
-*)
-let eval_constr env sigma (c : Constr.t) =
- let c = EConstr.of_constr c in
- let sigma,t = Typing.type_of env sigma c in
- let c' = Vnorm.cbv_vm env sigma c t in
- EConstr.Unsafe.to_constr c'
+ It is important to fully normalize the term, *including inductive
+ parameters of constructors*; see
+ https://github.com/coq/coq/issues/9840 for details on what goes
+ wrong if this does not happen, e.g., from using the vm rather than
+ cbv.
+*)
-(* For testing with "compute" instead of "vm_compute" :
let eval_constr env sigma (c : Constr.t) =
let c = EConstr.of_constr c in
let c' = Tacred.compute env sigma c in
EConstr.Unsafe.to_constr c'
-*)
let eval_constr_app env sigma c1 c2 =
eval_constr env sigma (mkApp (c1,[| c2 |]))
@@ -628,12 +638,21 @@ exception NotAValidPrimToken
(** The uninterp function below work at the level of [glob_constr]
which is too low for us here. So here's a crude conversion back
- to [constr] for the subset that concerns us. *)
+ 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
+ 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 (ConstructRef c, _) ->
let sigma,c = Evd.fresh_constructor_instance env sigma c in
sigma,mkConstructU c
+ | Glob_term.GRef (IndRef c, _) ->
+ let sigma,c = Evd.fresh_inductive_instance env sigma c in
+ sigma,mkIndU c
| 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
@@ -753,15 +772,29 @@ let coquint_of_rawnum uint str =
let nil = mkConstruct (uint,1) in
let rec do_chars s i acc =
if i < 0 then acc
- else
+ else if s.[i] == '_' then do_chars s (i-1) acc else
let dg = mkConstruct (uint, digit_of_char s.[i]) in
do_chars s (i-1) (mkApp(dg,[|acc|]))
in
do_chars str (String.length str - 1) nil
-let coqint_of_rawnum inds (str,sign) =
+let coqint_of_rawnum inds sign str =
let uint = coquint_of_rawnum inds.uint str in
- mkApp (mkConstruct (inds.int, if sign then 1 else 2), [|uint|])
+ let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
+ mkApp (mkConstruct (inds.int, pos_neg), [|uint|])
+
+let coqdecimal_of_rawnum inds sign n =
+ let i, f, e = NumTok.(n.int, n.frac, n.exp) in
+ let i = coqint_of_rawnum inds.int sign i in
+ let f = coquint_of_rawnum inds.int.uint f in
+ if e = "" then mkApp (mkConstruct (inds.decimal, 1), [|i; f|]) (* Decimal *)
+ else
+ let sign, e = match e.[1] with
+ | '-' -> SMinus, String.sub e 2 (String.length e - 2)
+ | '+' -> SPlus, String.sub e 2 (String.length e - 2)
+ | _ -> SPlus, String.sub e 1 (String.length e - 1) in
+ let e = coqint_of_rawnum inds.int sign e in
+ mkApp (mkConstruct (inds.decimal, 2), [|i; f; e|]) (* DecimalExp *)
let rawnum_of_coquint c =
let rec of_uint_loop c buf =
@@ -781,17 +814,30 @@ let rawnum_of_coquint c =
(* To avoid ambiguities between Nil and (D0 Nil), we choose
to not display Nil alone as "0" *)
raise NotAValidPrimToken
- else Buffer.contents buf
+ else NumTok.int (Buffer.contents buf)
let rawnum_of_coqint c =
match Constr.kind c with
| App (c,[|c'|]) ->
(match Constr.kind c with
- | Construct ((_,1), _) (* Pos *) -> (rawnum_of_coquint c', true)
- | Construct ((_,2), _) (* Neg *) -> (rawnum_of_coquint c', false)
+ | Construct ((_,1), _) (* Pos *) -> (SPlus, rawnum_of_coquint c')
+ | Construct ((_,2), _) (* Neg *) -> (SMinus, rawnum_of_coquint c')
| _ -> raise NotAValidPrimToken)
| _ -> raise NotAValidPrimToken
+let rawnum_of_decimal c =
+ let of_ife i f e =
+ let sign, n = rawnum_of_coqint i in
+ let f =
+ try (rawnum_of_coquint f).NumTok.int with NotAValidPrimToken -> "" in
+ let e = match e with None -> "" | Some e -> match rawnum_of_coqint e with
+ | SPlus, e -> "e+" ^ e.NumTok.int
+ | SMinus, e -> "e-" ^ e.NumTok.int in
+ sign,{ n with NumTok.frac = f; exp = e } in
+ match Constr.kind c with
+ | App (_,[|i; f|]) -> of_ife i f None
+ | App (_,[|i; f; e|]) -> of_ife i f (Some e)
+ | _ -> raise NotAValidPrimToken
(***********************************************************************)
@@ -878,31 +924,42 @@ let bigint_of_int63 c =
| _ -> raise NotAValidPrimToken
let big2raw n =
- if Bigint.is_pos_or_zero n then (Bigint.to_string n, true)
- else (Bigint.to_string (Bigint.neg n), false)
+ if Bigint.is_pos_or_zero n then
+ (SPlus, NumTok.int (Bigint.to_string n))
+ else
+ (SMinus, NumTok.int (Bigint.to_string (Bigint.neg n)))
-let raw2big (n,s) =
- if s then Bigint.of_string n else Bigint.neg (Bigint.of_string n)
+let raw2big s n = match s with
+ | SPlus -> Bigint.of_string n
+ | SMinus -> Bigint.neg (Bigint.of_string n)
let interp o ?loc n =
- begin match o.warning with
- | Warning threshold when snd n && rawnum_compare (fst n) threshold >= 0 ->
+ begin match o.warning, n with
+ | Warning threshold, (SPlus, { NumTok.int = n; frac = ""; exp = "" })
+ when rawnum_compare n threshold >= 0 ->
warn_large_num o.ty_name
| _ -> ()
end;
- let c = match fst o.to_kind with
- | Int int_ty -> coqint_of_rawnum int_ty n
- | UInt uint_ty when snd n -> coquint_of_rawnum uint_ty (fst n)
- | UInt _ (* n <= 0 *) -> no_such_prim_token "number" ?loc o.ty_name
- | Z z_pos_ty -> z_of_bigint z_pos_ty (raw2big n)
- | Int63 -> interp_int63 ?loc (raw2big n)
+ let c = match fst o.to_kind, n with
+ | Int int_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
+ coqint_of_rawnum int_ty s n
+ | UInt uint_ty, (SPlus, { NumTok.int = n; frac = ""; exp = "" }) ->
+ coquint_of_rawnum uint_ty n
+ | Z z_pos_ty, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
+ z_of_bigint z_pos_ty (raw2big s n)
+ | Int63, (s, { NumTok.int = n; frac = ""; exp = "" }) ->
+ interp_int63 ?loc (raw2big s n)
+ | (Int _ | UInt _ | Z _ | Int63), _ ->
+ no_such_prim_token "number" ?loc o.ty_name
+ | Decimal decimal_ty, (s,n) -> coqdecimal_of_rawnum decimal_ty s n
in
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,to_ty = Evd.fresh_global env sigma o.to_ty in
let to_ty = EConstr.Unsafe.to_constr to_ty in
match o.warning, snd o.to_kind with
- | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
+ | Abstract threshold, Direct
+ when rawnum_compare (snd n).NumTok.int threshold >= 0 ->
warn_abstract_large_num (o.ty_name,o.to_ty);
glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
| _ ->
@@ -915,9 +972,10 @@ let uninterp o n =
PrimTokenNotation.uninterp
begin function
| (Int _, c) -> rawnum_of_coqint c
- | (UInt _, c) -> (rawnum_of_coquint c, true)
+ | (UInt _, c) -> (SPlus, rawnum_of_coquint c)
| (Z _, c) -> big2raw (bigint_of_z c)
| (Int63, c) -> big2raw (bigint_of_int63 c)
+ | (Decimal _, c) -> rawnum_of_decimal c
end o n
end
@@ -1242,8 +1300,8 @@ let find_notation ntn sc =
(n.not_interp, n.not_location)
let notation_of_prim_token = function
- | Numeral (n,true) -> InConstrEntrySomeLevel, n
- | Numeral (n,false) -> InConstrEntrySomeLevel, "- "^n
+ | Numeral (SPlus,n) -> InConstrEntrySomeLevel, NumTok.to_string n
+ | Numeral (SMinus,n) -> InConstrEntrySomeLevel, "- "^NumTok.to_string n
| String _ -> raise Not_found
let find_prim_token check_allowed ?loc p sc =
@@ -1458,7 +1516,7 @@ let uninterp_prim_token c =
with Not_found -> raise Notation_ops.No_match
let uninterp_prim_token_cases_pattern c =
- match glob_constr_of_closed_cases_pattern c with
+ match glob_constr_of_closed_cases_pattern (Global.env()) c with
| exception Not_found -> raise Notation_ops.No_match
| na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
diff --git a/interp/notation.mli b/interp/notation.mli
index 5dcc96dc29..57e2be16b9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -70,14 +70,14 @@ 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 **integer**
+(** A numeral interpreter is the pair of an interpreter for **decimal**
numbers in terms and an optional interpreter in pattern, if
- negative numbers are not supported, the interpreter must fail with
- an appropriate error message *)
+ non integer or negative numbers are not supported, the interpreter
+ must fail with an appropriate error message *)
type notation_location = (DirPath.t * DirPath.t) * string
type required_module = full_path * string list
-type rawnum = Constrexpr.raw_natural_number * Constrexpr.sign
+type rawnum = Constrexpr.sign * Constrexpr.raw_numeral
(** The unique id string below will be used to refer to a particular
registered interpreter/uninterpreter of numeral or string notation.
@@ -112,8 +112,8 @@ exception PrimTokenNotationError of string * Environ.env * Evd.evar_map * prim_t
type numnot_option =
| Nop
- | Warning of raw_natural_number
- | Abstract of raw_natural_number
+ | Warning of string
+ | Abstract of string
type int_ty =
{ uint : Names.inductive;
@@ -123,11 +123,16 @@ type z_pos_ty =
{ z_ty : Names.inductive;
pos_ty : Names.inductive }
+type decimal_ty =
+ { int : int_ty;
+ decimal : Names.inductive }
+
type target_kind =
| Int of int_ty (* Coq.Init.Decimal.int + uint *)
| UInt of Names.inductive (* Coq.Init.Decimal.uint *)
| Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
| Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
+ | Decimal of decimal_ty (* Coq.Init.Decimal.decimal + uint + int *)
type string_target_kind =
| ListByte
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7d7e10a05b..7f084fffdd 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function
| GApp (t, l) ->
begin match DAst.get t with
| GRef (ConstructRef cstr,_) ->
- let nparams = Inductiveops.inductive_nparams (fst cstr) in
+ let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in
let _,l = List.chop nparams l in
PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
| _ -> raise No_match
@@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
alp, add_env alp sigma var (DAst.make @@ GVar id)
let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
- let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
+ let env = Global.env () in
+ 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
@@ -956,7 +957,7 @@ let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| GCoFix n1, GCoFix n2 -> Int.equal n1 n2
| GFix (nl1,n1), GFix (nl2,n2) ->
- let test (n1, _) (n2, _) = match n1, n2 with
+ let test n1 n2 = match n1, n2 with
| _, None -> true
| Some id1, Some id2 -> Int.equal id1 id2
| _ -> false
@@ -1292,7 +1293,7 @@ let match_notation_constr u c (metas,pat) =
| NtnTypeBinder (NtnBinderParsedAsConstr _) ->
(match Id.List.assoc x binders with
| [pat] ->
- let v = glob_constr_of_cases_pattern pat in
+ let v = glob_constr_of_cases_pattern (Global.env()) pat in
((v,scl)::terms',termlists',binders',binderlists')
| _ -> raise No_match)
| NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
@@ -1333,11 +1334,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
| r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
| PatVar Anonymous, NHole _ -> sigma,(0,[])
| PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
- let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+ let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
sigma,(0,l)
| PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
when eq_constructor r1 r2 ->
- let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
+ let 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 Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
then
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6fe20486dc..5024f5c26f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -38,7 +38,7 @@ type notation_constr =
notation_constr * notation_constr
| NIf of notation_constr * (Name.t * notation_constr option) *
notation_constr * notation_constr
- | NRec of fix_kind * Id.t array *
+ | NRec of glob_fix_kind * Id.t array *
(Name.t * notation_constr option * notation_constr) list array *
notation_constr array * notation_constr array
| NSort of glob_sort
diff --git a/interp/numTok.ml b/interp/numTok.ml
new file mode 100644
index 0000000000..8f2004b889
--- /dev/null
+++ b/interp/numTok.ml
@@ -0,0 +1,52 @@
+type t = {
+ int : string;
+ frac : string;
+ exp : string
+}
+
+let equal n1 n2 =
+ String.(equal n1.int n2.int && equal n1.frac n2.frac && equal n1.exp n2.exp)
+
+let int s = { int = s; frac = ""; exp = "" }
+
+let to_string n = n.int ^ (if n.frac = "" then "" else "." ^ n.frac) ^ n.exp
+
+let parse =
+ let buff = ref (Bytes.create 80) in
+ let store len x =
+ let open Bytes in
+ if len >= length !buff then
+ buff := cat !buff (create (length !buff));
+ set !buff len x;
+ succ len in
+ let get_buff len = Bytes.sub_string !buff 0 len in
+ (* reads [0-9_]* *)
+ let rec number len s = match Stream.peek s with
+ | Some (('0'..'9' | '_') as c) -> Stream.junk s; number (store len c) s
+ | _ -> len in
+ fun s ->
+ let i = get_buff (number 0 s) in
+ let f =
+ match Stream.npeek 2 s with
+ | '.' :: (('0'..'9' | '_') as c) :: _ ->
+ Stream.junk s; Stream.junk s; get_buff (number (store 0 c) s)
+ | _ -> "" in
+ let e =
+ match (Stream.npeek 2 s) with
+ | (('e'|'E') as e) :: ('0'..'9' as c) :: _ ->
+ Stream.junk s; Stream.junk s; get_buff (number (store (store 0 e) c) s)
+ | (('e'|'E') as e) :: (('+'|'-') as sign) :: _ ->
+ begin match Stream.npeek 3 s with
+ | _ :: _ :: ('0'..'9' as c) :: _ ->
+ Stream.junk s; Stream.junk s; Stream.junk s;
+ get_buff (number (store (store (store 0 e) sign) c) s)
+ | _ -> ""
+ end
+ | _ -> "" in
+ { int = i; frac = f; exp = e }
+
+let of_string s =
+ if s = "" || s.[0] < '0' || s.[0] > '9' then None else
+ let strm = Stream.of_string (s ^ " ") in
+ let n = parse strm in
+ if Stream.count strm >= String.length s then Some n else None
diff --git a/interp/numTok.mli b/interp/numTok.mli
new file mode 100644
index 0000000000..0b6a877cbd
--- /dev/null
+++ b/interp/numTok.mli
@@ -0,0 +1,18 @@
+type t = {
+ int : string; (** \[0-9\]\[0-9_\]* *)
+ frac : string; (** empty or \[0-9_\]+ *)
+ exp : string (** empty or \[eE\]\[+-\]?\[0-9\]\[0-9_\]* *)
+}
+
+val equal : t -> t -> bool
+
+(** [int s] amounts to [\{ int = s; frac = ""; exp = "" \}] *)
+val int : string -> t
+
+val to_string : t -> string
+
+val of_string : string -> t option
+
+(** Precondition: the first char on the stream is a digit (\[0-9\]).
+ Precondition: at least two extra chars after the numeral to parse. *)
+val parse : char Stream.t -> t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 14:57:23 +0000