aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml40
-rw-r--r--interp/constrextern.mli3
-rw-r--r--interp/declare.ml15
-rw-r--r--interp/declare.mli5
-rw-r--r--interp/notation.ml10
-rw-r--r--interp/notation.mli14
-rw-r--r--interp/ppextend.ml9
-rw-r--r--interp/ppextend.mli14
8 files changed, 22 insertions, 88 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fcaee5c939..e85415bed3 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -320,38 +320,6 @@ let drop_implicits_in_patt cst nb_expl args =
let imps = List.skipn_at_least nb_expl (select_stronger_impargs impl_st) in
impls_fit [] (imps,args)
-let has_curly_brackets ntn =
- String.length ntn >= 6 && (String.is_sub "{ _ } " ntn 0 ||
- String.is_sub " { _ }" ntn (String.length ntn - 6) ||
- String.string_contains ~where:ntn ~what:" { _ } ")
-
-let rec wildcards ntn n =
- if Int.equal n (String.length ntn) then []
- else let l = spaces ntn (n+1) in if ntn.[n] == '_' then n::l else l
-and spaces ntn n =
- if Int.equal n (String.length ntn) then []
- else if ntn.[n] == ' ' then wildcards ntn (n+1) else spaces ntn (n+1)
-
-let expand_curly_brackets loc mknot ntn l =
- let ntn' = ref ntn in
- let rec expand_ntn i =
- function
- | [] -> []
- | a::l ->
- let a' =
- let p = List.nth (wildcards !ntn' 0) i - 2 in
- if p>=0 && p+5 <= String.length !ntn' && String.is_sub "{ _ }" !ntn' p
- then begin
- ntn' :=
- String.sub !ntn' 0 p ^ "_" ^
- String.sub !ntn' (p+5) (String.length !ntn' -p-5);
- mknot (loc,"{ _ }",[a]) end
- else a in
- a' :: expand_ntn (i+1) l in
- let l = expand_ntn 0 l in
- (* side effect *)
- mknot (loc,!ntn',l)
-
let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
@@ -367,9 +335,7 @@ let is_zero s =
in aux 0
let make_notation_gen loc ntn mknot mkprim destprim l =
- if has_curly_brackets ntn
- then expand_curly_brackets loc mknot ntn l
- else match ntn,List.map destprim l with
+ match 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) ->
mknot (loc,ntn,([mknot (loc,"( _ )",l)]))
@@ -1098,7 +1064,6 @@ let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* Not "goal_concl_style" means do alpha-conversion avoiding only *)
(* those goal/section/rel variables that occurs in the subterm under *)
(* consideration; see namegen.ml for further details *)
- let t = EConstr.of_constr t in
let avoid = if goal_concl_style then ids_of_context env else [] in
let r = Detyping.detype ~lax:lax goal_concl_style avoid env sigma t in
let vars = vars_of_env env in
@@ -1111,7 +1076,6 @@ let extern_constr ?(lax=false) goal_concl_style env sigma t =
extern_constr_gen lax goal_concl_style None env sigma t
let extern_type goal_concl_style env sigma t =
- let t = EConstr.of_constr t in
let avoid = if goal_concl_style then ids_of_context env else [] in
let r = Detyping.detype goal_concl_style avoid env sigma t in
extern_glob_type (vars_of_env env) r
@@ -1198,8 +1162,6 @@ let extern_constr_pattern env sigma pat =
extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
let extern_rel_context where env sigma sign =
- let sign = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) sign in
- let where = Option.map EConstr.of_constr where in
let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
let a = List.map (extended_glob_local_binder_of_decl) a in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b5242b3477..ffa891c502 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -9,6 +9,7 @@
open Names
open Term
open Termops
+open EConstr
open Environ
open Libnames
open Globnames
@@ -41,7 +42,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
- Context.Rel.t -> local_binder_expr list
+ rel_context -> local_binder_expr list
(** Printing options *)
val print_implicits : bool ref
diff --git a/interp/declare.ml b/interp/declare.ml
index 70f422b514..7fcb38296f 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -32,14 +32,6 @@ type internal_flag =
| InternalTacticRequest (* kernel action, no message is displayed *)
| UserIndividualRequest (* user action, a message is displayed *)
-(** XML output hooks *)
-
-let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
-let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
-let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
-
-let if_xml f x = if !Flags.xml_export then f x else ()
-
(** Declaration of section variables and local definitions *)
type section_variable_entry =
@@ -95,7 +87,6 @@ let declare_variable id obj =
declare_var_implicits id;
Notation.declare_ref_arguments_scope (VarRef id);
Heads.declare_head (EvalVarRef id);
- if_xml (Hook.get f_xml_declare_variable) oname;
oname
@@ -256,7 +247,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
let id = Label.to_id (pi3 (Constant.repr3 c)) in
ignore(add_leaf id o);
update_tables c;
- let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in
match role with
| Safe_typing.Subproof -> ()
| Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]
@@ -268,9 +258,7 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
cst_kind = kind;
cst_locl = local;
} in
- let kn = declare_constant_common id cst in
- let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
- kn
+ declare_constant_common id cst
let declare_definition ?(internal=UserIndividualRequest)
?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
@@ -410,7 +398,6 @@ let declare_mind mie =
let isrecord,isprim = declare_projections mind in
declare_mib_implicits mind;
declare_inductive_argument_scopes mind mie;
- if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
oname, isprim
(* Declaration messages *)
diff --git a/interp/declare.mli b/interp/declare.mli
index 6a09434645..ccd7d28bb5 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -69,11 +69,6 @@ val set_declare_scheme :
the whole block and a boolean indicating if it is a primitive record. *)
val declare_mind : mutual_inductive_entry -> object_name * bool
-(** Hooks for XML output *)
-val xml_declare_variable : (object_name -> unit) Hook.t
-val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
-val xml_declare_inductive : (bool * object_name -> unit) Hook.t
-
(** Declaration messages *)
val definition_message : Id.t -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index c07a009438..c373faf680 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -41,7 +41,6 @@ open Context.Named.Declaration
(**********************************************************************)
(* Scope of symbols *)
-type level = precedence * tolerability list
type delimiters = string
type notation_location = (DirPath.t * DirPath.t) * string
@@ -83,11 +82,18 @@ let parenRelation_eq t1 t2 = match t1, t2 with
| Prec l1, Prec l2 -> Int.equal l1 l2
| _ -> false
-let level_eq (l1, t1) (l2, t2) =
+let notation_var_internalization_type_eq v1 v2 = match v1, v2 with
+| NtnInternTypeConstr, NtnInternTypeConstr -> true
+| NtnInternTypeBinder, NtnInternTypeBinder -> true
+| NtnInternTypeIdent, NtnInternTypeIdent -> true
+| (NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent), _ -> false
+
+let level_eq (l1, t1, u1) (l2, t2, u2) =
let tolerability_eq (i1, r1) (i2, r2) =
Int.equal i1 i2 && parenRelation_eq r1 r2
in
Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+ && List.equal notation_var_internalization_type_eq u1 u2
let declare_scope scope =
try let _ = String.Map.find scope !scope_map in ()
diff --git a/interp/notation.mli b/interp/notation.mli
index dd0144e8d0..f9f247fe10 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open Bigint
open Names
open Libnames
@@ -22,7 +21,6 @@ open Ppextend
(** A scope is a set of interpreters for symbols + optional
interpreter and printers for integers + optional delimiters *)
-type level = precedence * tolerability list
type delimiters = string
type scope
type scopes (** = [scope_name list] *)
@@ -189,13 +187,13 @@ val make_notation_key : symbol list -> notation
val decompose_notation_key : notation -> symbol list
(** Prints scopes (expects a pure aconstr printer) *)
-val pr_scope_class : scope_class -> std_ppcmds
-val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds
-val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds
-val locate_notation : (glob_constr -> std_ppcmds) -> notation ->
- scope_name option -> std_ppcmds
+val pr_scope_class : scope_class -> Pp.t
+val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t
+val pr_scopes : (glob_constr -> Pp.t) -> Pp.t
+val locate_notation : (glob_constr -> Pp.t) -> notation ->
+ scope_name option -> Pp.t
-val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds
+val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
(** {6 Printing rules for notations} *)
diff --git a/interp/ppextend.ml b/interp/ppextend.ml
index 2bbe87bbca..3ebc9b71d2 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.ml
@@ -7,17 +7,10 @@
(************************************************************************)
open Pp
+open Notation_term
(*s Pretty-print. *)
-(* Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
type ppbox =
| PpHB of int
| PpHOVB of int
diff --git a/interp/ppextend.mli b/interp/ppextend.mli
index 4874989cd9..6ff5a42728 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.mli
@@ -6,18 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
+open Notation_term
(** {6 Pretty-print. } *)
-(** Dealing with precedences *)
-
-type precedence = int
-
-type parenRelation = L | E | Any | Prec of precedence
-
-type tolerability = precedence * parenRelation
-
type ppbox =
| PpHB of int
| PpHOVB of int
@@ -28,9 +20,9 @@ type ppcut =
| PpBrk of int * int
| PpFnl
-val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds
+val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
-val ppcmd_of_cut : ppcut -> std_ppcmds
+val ppcmd_of_cut : ppcut -> Pp.t
type unparsing =
| UnpMetaVar of int * parenRelation
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 23:24:26 +0000