aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml7
-rw-r--r--interp/constrexpr_ops.ml15
-rw-r--r--interp/constrexpr_ops.mli3
-rw-r--r--interp/constrextern.ml28
-rw-r--r--interp/constrintern.ml1
-rw-r--r--interp/dumpglob.ml32
-rw-r--r--interp/dumpglob.mli14
-rw-r--r--interp/impargs.ml23
-rw-r--r--interp/impargs.mli2
-rw-r--r--interp/implicit_quantifiers.ml1
-rw-r--r--interp/modintern.ml6
-rw-r--r--interp/modintern.mli4
-rw-r--r--interp/notation.ml13
-rw-r--r--interp/notation_ops.ml11
-rw-r--r--interp/notation_term.ml1
-rw-r--r--interp/syntax_def.ml4
16 files changed, 96 insertions, 69 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index e4af0fcee0..49b9149675 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -10,7 +10,6 @@
open Names
open Libnames
-open Decl_kinds
(** {6 Concrete syntax for terms } *)
@@ -39,8 +38,8 @@ type explicitation =
| ExplByName of Id.t
type binder_kind =
- | Default of binding_kind
- | Generalized of binding_kind * bool
+ | Default of Glob_term.binding_kind
+ | Generalized of Glob_term.binding_kind * bool
(** (Inner binding always Implicit) Outer bindings, typeclass-specific flag
for implicit generalization of superclasses *)
@@ -121,7 +120,7 @@ and constr_expr_r =
| CSort of Glob_term.glob_sort
| CCast of constr_expr * constr_expr Glob_term.cast_type
| CNotation of notation * constr_notation_substitution
- | CGeneralization of binding_kind * abstraction_kind option * constr_expr
+ | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr
| CPrim of prim_token
| CDelimiters of string * constr_expr
and constr_expr = constr_expr_r CAst.t
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 8fce24249c..b4798127f9 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -17,25 +17,19 @@ open Namegen
open Glob_term
open Constrexpr
open Notation
-open Decl_kinds
(***********************)
(* For binders parsing *)
-let binding_kind_eq bk1 bk2 = match bk1, bk2 with
-| Explicit, Explicit -> true
-| Implicit, Implicit -> true
-| _ -> false
-
let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with
| AbsLambda, AbsLambda -> true
| AbsPi, AbsPi -> true
| _ -> false
let binder_kind_eq b1 b2 = match b1, b2 with
-| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2
+| Default bk1, Default bk2 -> Glob_ops.binding_kind_eq bk1 bk2
| Generalized (ck1, b1), Generalized (ck2, b2) ->
- binding_kind_eq ck1 ck2 &&
+ Glob_ops.binding_kind_eq ck1 ck2 &&
(if b1 then b2 else not b2)
| _ -> false
@@ -172,7 +166,7 @@ let rec constr_expr_eq e1 e2 =
| CPrim i1, CPrim i2 ->
prim_token_eq i1 i2
| CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) ->
- binding_kind_eq bk1 bk2 &&
+ Glob_ops.binding_kind_eq bk1 bk2 &&
Option.equal abstraction_kind_eq ak1 ak2 &&
constr_expr_eq e1 e2
| CDelimiters(s1,e1), CDelimiters(s2,e2) ->
@@ -631,7 +625,8 @@ let interp_univ_constraints env evd 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 (Environ.universes env) pl) 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;
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 3ed240d356..a05a9cb999 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -26,9 +26,6 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool
val local_binder_eq : local_binder_expr -> local_binder_expr -> bool
(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *)
-val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool
-(** Equality on [binding_kind] *)
-
val binder_kind_eq : binder_kind -> binder_kind -> bool
(** Equality on [binder_kind] *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 96392edb11..0a1371413a 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -27,7 +27,6 @@ open Glob_ops
open Pattern
open Notation
open Detyping
-open Decl_kinds
module NamedDecl = Context.Named.Declaration
(*i*)
@@ -753,6 +752,30 @@ let extended_glob_local_binder_of_decl loc = function
let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u)
(**********************************************************************)
+(* mapping special floats *)
+
+(* this helper function is copied from notation.ml as it's not exported *)
+let qualid_of_ref n =
+ n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_infinity () = qualid_of_ref "num.float.infinity"
+let q_neg_infinity () = qualid_of_ref "num.float.neg_infinity"
+let q_nan () = qualid_of_ref "num.float.nan"
+
+let extern_float f scopes =
+ if Float64.is_nan f then CRef(q_nan (), None)
+ else if Float64.is_infinity f then CRef(q_infinity (), None)
+ else if Float64.is_neg_infinity f then CRef(q_neg_infinity (), None)
+ else
+ let sign = if Float64.sign f then SMinus else SPlus in
+ let s = Float64.(to_string (abs f)) in
+ match NumTok.of_string s with
+ | None -> assert false
+ | Some n ->
+ extern_prim_token_delimiter_if_required (Numeral (sign, n))
+ "float" "float_scope" scopes
+
+(**********************************************************************)
(* mapping glob_constr to constr_expr *)
let extern_glob_sort = function
@@ -973,6 +996,8 @@ let rec extern inctx scopes vars r =
(Numeral (SPlus, NumTok.int (Uint63.to_string i)))
"int63" "int63_scope" (snd scopes)
+ | GFloat f -> extern_float f (snd scopes)
+
in insert_coercion coercion (CAst.make ?loc c)
and extern_typ (subentry,(_,scopes)) =
@@ -1315,6 +1340,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PSort Sorts.InSet -> GSort (UNamed [GSet,0])
| PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
| PInt i -> GInt i
+ | PFloat f -> GFloat f
let extern_constr_pattern env sigma pat =
extern true (InConstrEntrySomeLevel,(None,[])) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f341071728..f2cb4ae5c7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -31,7 +31,6 @@ open Notation_term
open Notation_ops
open Notation
open Inductiveops
-open Decl_kinds
open Context.Rel.Declaration
(** constr_expr -> glob_constr translation:
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 8d6a266c30..41d1da9694 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -20,31 +20,21 @@ let open_glob_file f =
let close_glob_file () =
close_out !glob_file
-type glob_output_t =
- | NoGlob
- | StdOut
- | MultFiles
- | Feedback
- | File of string
+type glob_output =
+ | NoGlob
+ | Feedback
+ | MultFiles
+ | File of string
let glob_output = ref NoGlob
-let dump () = !glob_output != NoGlob
+let dump () = !glob_output <> NoGlob
-let noglob () = glob_output := NoGlob
-
-let dump_to_dotglob () = glob_output := MultFiles
-
-let dump_into_file f =
- if String.equal f "stdout" then
- (glob_output := StdOut; glob_file := stdout)
- else
- (glob_output := File f; open_glob_file f)
-
-let feedback_glob () = glob_output := Feedback
+let set_glob_output mode =
+ glob_output := mode
let dump_string s =
- if dump () && !glob_output != Feedback then
+ if dump () && !glob_output != Feedback then
output_string !glob_file s
let start_dump_glob ~vfile ~vofile =
@@ -57,13 +47,13 @@ let start_dump_glob ~vfile ~vofile =
| File f ->
open_glob_file f;
output_string !glob_file "DIGEST NO\n"
- | NoGlob | Feedback | StdOut ->
+ | NoGlob | Feedback ->
()
let end_dump_glob () =
match !glob_output with
| MultFiles | File _ -> close_glob_file ()
- | NoGlob | Feedback | StdOut -> ()
+ | NoGlob | Feedback -> ()
let previous_state = ref MultFiles
let pause () = previous_state := !glob_output; glob_output := NoGlob
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 60d62a1cb2..2b6a116a01 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -8,19 +8,19 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val open_glob_file : string -> unit
-val close_glob_file : unit -> unit
-
val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
-val noglob : unit -> unit
-val dump_into_file : string -> unit (** special handling of "stdout" *)
+type glob_output =
+ | NoGlob
+ | Feedback
+ | MultFiles (* one glob file per .v file *)
+ | File of string (* Single file for all coqc arguments *)
-val dump_to_dotglob : unit -> unit
-val feedback_glob : unit -> unit
+(* Default "NoGlob" *)
+val set_glob_output : glob_output -> unit
val pause : unit -> unit
val continue : unit -> unit
diff --git a/interp/impargs.ml b/interp/impargs.ml
index 0466efa991..0de4eb5fa1 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -15,7 +15,6 @@ open Names
open Constr
open Globnames
open Declarations
-open Decl_kinds
open Lib
open Libobject
open EConstr
@@ -217,7 +216,7 @@ let rec is_rigid_head sigma t = match kind sigma t with
| Fix ((fi,i),_) -> is_rigid_head sigma (args.(fi.(i)))
| _ -> is_rigid_head sigma f)
| Lambda _ | LetIn _ | Construct _ | CoFix _ | Fix _
- | Prod _ | Meta _ | Cast _ | Int _ -> assert false
+ | Prod _ | Meta _ | Cast _ | Int _ | Float _ -> assert false
let is_rigid env sigma t =
let open Context.Rel.Declaration in
@@ -486,12 +485,19 @@ let subst_implicits_decl subst (r,imps as o) =
let subst_implicits (subst,(req,l)) =
(ImplLocal,List.Smart.map (subst_implicits_decl subst) l)
+(* This was moved out of lib.ml, however it is not stored with regular
+ implicit data *)
+let sec_implicits =
+ Summary.ref Id.Map.empty ~name:"section-implicits"
+
let impls_of_context ctx =
- let map (decl, impl) = match impl with
- | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
- | _ -> None
+ let map decl =
+ let id = NamedDecl.get_id decl in
+ match Id.Map.get id !sec_implicits with
+ | Glob_term.Implicit -> Some (id, Manual, (true, true))
+ | Glob_term.Explicit -> None
in
- List.rev_map map (List.filter (fst %> NamedDecl.is_local_assum) ctx)
+ List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
let adjust_side_condition p = function
| LessArgsThan n -> LessArgsThan (n+p)
@@ -577,9 +583,10 @@ let declare_implicits local ref =
if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in
declare_implicits_gen req flags ref
-let declare_var_implicits id =
+let declare_var_implicits id ~impl =
let flags = !implicit_args in
- declare_implicits_gen ImplLocal flags (GlobRef.VarRef id)
+ sec_implicits := Id.Map.add id impl !sec_implicits;
+ declare_implicits_gen ImplLocal flags (GlobRef.VarRef id)
let declare_constant_implicits con =
let flags = !implicit_args in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 90a7944642..2751b9d40b 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -93,7 +93,7 @@ val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list
(** {6 Computation of implicits (done using the global environment). } *)
-val declare_var_implicits : variable -> unit
+val declare_var_implicits : variable -> impl:Glob_term.binding_kind -> unit
val declare_constant_implicits : Constant.t -> unit
val declare_mib_implicits : MutInd.t -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 9f6281ae15..455471a472 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -11,7 +11,6 @@
(*i*)
open Names
open Context
-open Decl_kinds
open CErrors
open Util
open Glob_term
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 955288244e..ddf5b2d7b1 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,6 @@ open Declarations
open Libnames
open Constrexpr
open Constrintern
-open Declaremods
type module_internalization_error =
| NotAModuleNorModtype of string
@@ -21,9 +20,11 @@ type module_internalization_error =
exception ModuleInternalizationError of module_internalization_error
+type module_kind = Module | ModType | ModAny
+
let error_not_a_module_loc kind loc qid =
let s = string_of_qualid qid in
- let e = let open Declaremods in match kind with
+ let e = match kind with
| Module -> Modops.ModuleTypingError (Modops.NotAModule s)
| ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
| ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
@@ -46,7 +47,6 @@ let error_application_to_module_type loc =
it is equal to the input kind when this one isn't ModAny. *)
let lookup_module_or_modtype kind qid =
- let open Declaremods in
let loc = qid.CAst.loc in
try
if kind == ModType then raise Not_found;
diff --git a/interp/modintern.mli b/interp/modintern.mli
index 75ab38c64a..72695a680e 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -28,5 +28,7 @@ exception ModuleInternalizationError of module_internalization_error
kind is never ModAny, and it is equal to the input kind when this one
isn't ModAny. *)
+type module_kind = Module | ModType | ModAny
+
val interp_module_ast :
- env -> Declaremods.module_kind -> module_ast -> module_struct_entry * Declaremods.module_kind * Univ.ContextSet.t
+ env -> module_kind -> module_ast -> module_struct_entry * module_kind * Univ.ContextSet.t
diff --git a/interp/notation.ml b/interp/notation.ml
index d88182241b..c157cf43fb 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -503,6 +503,9 @@ let rec constr_of_glob env sigma g = match DAst.get g with
let sigma,cl = List.fold_left_map (constr_of_glob env) sigma gcl in
sigma,mkApp (c, Array.of_list cl)
| 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
+ sigma,mkSort c
| _ ->
raise NotAValidPrimToken
@@ -516,6 +519,10 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with
| Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None))
| Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None))
| Int i -> DAst.make ?loc (Glob_term.GInt i)
+ | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0]))
+ | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0]))
+ | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0]))
+ | Sort (Sorts.Type _) -> DAst.make ?loc (Glob_term.GSort (Glob_term.UAnonymous {rigid=true}))
| _ -> Loc.raise ?loc (PrimTokenNotationError(token_kind,env,sigma,UnexpectedTerm c))
let no_such_prim_token uninterpreted_token_kind ?loc ty =
@@ -1205,7 +1212,7 @@ let interp_notation ?loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
try
let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
- Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+ Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
n.not_interp, (n.not_location, sc)
with Not_found ->
user_err ?loc
@@ -1533,7 +1540,7 @@ let discharge_arguments_scope (_,(req,r,n,l,_)) =
let n =
try
let vars = Lib.variable_section_segment_of_reference r in
- vars |> List.map fst |> List.filter is_local_assum |> List.length
+ vars |> List.filter is_local_assum |> List.length
with
Not_found (* Not a ref defined in this section *) -> 0 in
Some (req,r,n,l,[])
@@ -1836,7 +1843,7 @@ let locate_notation prglob ntn scope =
str "Notation" ++ fnl () ++
prlist_with_sep fnl (fun (ntn,l) ->
let scope = find_default ntn scopes in
- prlist
+ prlist_with_sep fnl
(fun (sc,r,(_,df)) ->
hov 0 (
pr_notation_info prglob df r ++
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 2fa78bb9f3..7e146754b2 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -15,7 +15,6 @@ open Names
open Nameops
open Constr
open Globnames
-open Decl_kinds
open Namegen
open Glob_term
open Glob_ops
@@ -91,9 +90,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
(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
| (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _
| NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _
- | NRec _ | NSort _ | NCast _ | NInt _), _ -> false
+ | NRec _ | NSort _ | NCast _ | NInt _ | NFloat _), _ -> false
(**********************************************************************)
(* Re-interpret a notation as a glob_constr, taking care of binders *)
@@ -223,6 +224,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
| NHole (x, naming, arg) -> GHole (x, naming, arg)
| NRef x -> GRef (x,None)
| NInt i -> GInt i
+ | NFloat f -> GFloat f
let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
@@ -439,6 +441,7 @@ let notation_constr_and_vars_of_glob_constr recvars a =
| GCast (c,k) -> NCast (aux c,map_cast_type aux k)
| GSort s -> NSort s
| GInt i -> NInt i
+ | GFloat f -> NFloat f
| GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
NHole (w, naming, arg)
@@ -628,6 +631,7 @@ let rec subst_notation_constr subst bound raw =
| NSort _ -> raw
| NInt _ -> raw
+ | NFloat _ -> raw
| NHole (knd, naming, solve) ->
let nknd = match knd with
@@ -1197,6 +1201,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
| GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
+ | GFloat f1, NFloat f2 when Float64.equal f1 f2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -1224,7 +1229,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
| (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
| GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _
- | GCast _ | GInt _ ), _ -> raise No_match
+ | GCast _ | GInt _ | GFloat _), _ -> raise No_match
and match_in u = match_ true u
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 908455bd05..c6ddd9ac95 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -44,6 +44,7 @@ type notation_constr =
| NSort of glob_sort
| NCast of notation_constr * notation_constr cast_type
| NInt of Uint63.t
+ | NFloat of Float64.t
(** Note concerning NList: first constr is iterator, second is terminator;
first id is where each argument of the list has to be substituted
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 302bb6ece2..9dded8656c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -100,7 +100,7 @@ let warn_deprecated_syntactic_definition =
let search_syntactic_definition ?loc kn =
let syndef = KNmap.find kn !syntax_table in
let def = out_pat syndef.syndef_pattern in
- Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+ Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
def
let search_filtered_syntactic_definition ?loc filter kn =
@@ -108,5 +108,5 @@ let search_filtered_syntactic_definition ?loc filter kn =
let def = out_pat syndef.syndef_pattern in
let res = filter def in
if Option.has_some res then
- Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+ Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
res
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:06:11 +0000