--- a/src/HOL/Eisbach/match_method.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/HOL/Eisbach/match_method.ML Tue Oct 22 23:56:48 2024 +0200
@@ -121,18 +121,27 @@
then Syntax.parse_prop ctxt3 term
else Syntax.parse_term ctxt3 term;
- fun drop_judgment_dummy t =
+ val judgment_name = Object_Logic.judgment_name ctxt;
+
+ fun dest_judgment_dummy t =
(case t of
- Const (judgment, _) $
- (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
- Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, _)) =>
- if judgment = Object_Logic.judgment_name ctxt then
- Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $
- Const (\<^const_name>\<open>Pure.dummy_pattern\<close>, propT)
- else t
- | t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
- | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
- | _ => t);
+ Const (c, _) $
+ (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const_>\<open>Pure.dummy_pattern _\<close>) =>
+ if c = judgment_name then SOME T else NONE
+ | Const (\<^syntax_const>\<open>_type_constraint_\<close>, _) $ Const (c, _) $
+ (Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const_>\<open>Pure.dummy_pattern _\<close>) =>
+ if c = judgment_name then SOME T else NONE
+ | _ => NONE);
+
+ fun drop_judgment_dummy t =
+ (case dest_judgment_dummy t of
+ SOME T =>
+ Const (\<^syntax_const>\<open>_type_constraint_\<close>, T) $ \<^Const>\<open>Pure.dummy_pattern \<^Type>\<open>prop\<close>\<close>
+ | NONE =>
+ (case t of
+ t1 $ t2 => drop_judgment_dummy t1 $ drop_judgment_dummy t2
+ | Abs (a, T, b) => Abs (a, T, drop_judgment_dummy b)
+ | _ => t));
val pats =
map (fn (_, (term, _)) => parse_term (Parse_Tools.the_parse_val term)) ts
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Tue Oct 22 23:56:48 2024 +0200
@@ -1,7 +1,9 @@
(* Title: HOL/HOLCF/Tools/cont_consts.ML
- Author: Tobias Mayr, David von Oheimb, and Markus Wenzel
+ Author: Tobias Mayr
+ Author: David von Oheimb
+ Author: Makarius
-HOLCF version of consts: handle continuous function types in mixfix
+HOLCF version of 'consts' command: handle continuous function types in mixfix
syntax.
*)
@@ -14,83 +16,51 @@
structure Cont_Consts: CONT_CONSTS =
struct
-
-(* misc utils *)
-
-fun change_arrow 0 T = T
- | change_arrow n (Type (_, [S, T])) = \<^Type>\<open>fun S \<open>change_arrow (n - 1) T\<close>\<close>
- | change_arrow _ T = raise TYPE ("cont_consts: change_arrow", [T], [])
-
-fun trans_rules name2 name1 n mx =
- let
- val vnames = Name.invent Name.context "a" n
- val extra_parse_rule = Syntax.Parse_Rule (Ast.Constant name2, Ast.Constant name1)
- in
- [Syntax.Parse_Print_Rule
- (Ast.mk_appl (Ast.Constant name2) (map Ast.Variable vnames),
- fold (fn a => fn t =>
- Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable a])
- vnames (Ast.Constant name1))] @
- (case mx of
- Infix _ => [extra_parse_rule]
- | Infixl _ => [extra_parse_rule]
- | Infixr _ => [extra_parse_rule]
- | _ => [])
- end
-
+fun count_cfun \<^Type>\<open>cfun _ B\<close> = count_cfun B + 1
+ | count_cfun _ = 0
-(* transforming infix/mixfix declarations of constants with type ...->...
- a declaration of such a constant is transformed to a normal declaration with
- an internal name, the same type, and nofix. Additionally, a purely syntactic
- declaration with the original name, type ...=>..., and the original mixfix
- is generated and connected to the other declaration via some translation.
-*)
-fun transform thy (c, T, mx) =
- let
- val thy_ctxt = Proof_Context.init_global thy
- fun syntax b = Lexicon.mark_const (Sign.full_bname thy b)
- val c1 = Binding.name_of c
- val c2 = c1 ^ "_cont_syntax"
- val n = Mixfix.mixfix_args thy_ctxt mx
- in
- ((c, T, NoSyn),
- (Binding.name c2, change_arrow n T, mx),
- trans_rules (syntax c2) (syntax c1) n mx)
- end
-
-fun cfun_arity (Type (n, [_, T])) = if n = \<^type_name>\<open>cfun\<close> then 1 + cfun_arity T else 0
- | cfun_arity _ = 0
-
-fun is_contconst _ (_, _, NoSyn) = false
- | is_contconst _ (_, _, Binder _) = false (* FIXME ? *)
- | is_contconst thy (c, T, mx) =
- let
- val thy_ctxt = Proof_Context.init_global thy
- val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
- cat_error msg ("in mixfix annotation for " ^ Binding.print c)
- in cfun_arity T >= n end
-
-
-(* add_consts *)
-
-local
+fun change_cfun 0 T = T
+ | change_cfun n \<^Type>\<open>cfun A B\<close> = \<^Type>\<open>fun A \<open>change_cfun (n - 1) B\<close>\<close>
+ | change_cfun _ T = raise TYPE ("cont_consts: change_cfun", [T], [])
fun gen_add_consts prep_typ raw_decls thy =
let
- val decls = map (fn (c, T, mx) => (c, prep_typ thy T, mx)) raw_decls
- val (contconst_decls, normal_decls) = List.partition (is_contconst thy) decls
- val transformed_decls = map (transform thy) contconst_decls
+ val thy_ctxt = Proof_Context.init_global thy
+
+ fun is_cont_const (_, _, NoSyn) = false
+ | is_cont_const (_, _, Binder _) = false
+ | is_cont_const (b, T, mx) =
+ let
+ val n = Mixfix.mixfix_args thy_ctxt mx handle ERROR msg =>
+ cat_error msg ("in mixfix annotation for " ^ Binding.print b)
+ in count_cfun T >= n end
+
+ fun transform (b, T, mx) =
+ let
+ val c = Sign.full_name thy b
+ val c1 = Lexicon.mark_syntax c
+ val c2 = Lexicon.mark_const c
+ val xs = Name.invent Name.context "xa" (Mixfix.mixfix_args thy_ctxt mx)
+ val trans_rules =
+ Syntax.Parse_Print_Rule
+ (Ast.mk_appl (Ast.Constant c1) (map Ast.Variable xs),
+ fold (fn x => fn t =>
+ Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Rep_cfun\<close>) [t, Ast.Variable x])
+ xs (Ast.Constant c2)) ::
+ (if Mixfix.is_infix mx then [Syntax.Parse_Rule (Ast.Constant c1, Ast.Constant c2)] else [])
+ in ((b, T, NoSyn), (c1, change_cfun (length xs) T, mx), trans_rules) end
+
+ val decls = map (fn (b, T, mx) => (b, prep_typ thy T, mx)) raw_decls
+ val (cont_decls, normal_decls) = List.partition is_cont_const decls
+ val transformed_decls = map transform cont_decls
in
thy
- |> Sign.add_consts (normal_decls @ map #1 transformed_decls @ map #2 transformed_decls)
+ |> Sign.add_consts (normal_decls @ map #1 transformed_decls)
+ |> Sign.syntax_global true Syntax.mode_default (map #2 transformed_decls)
|> Sign.add_trrules (maps #3 transformed_decls)
end
-in
-
val add_consts = gen_add_consts Sign.certify_typ
val add_consts_cmd = gen_add_consts Syntax.read_typ_global
end
-
-end
--- a/src/Pure/Isar/attrib.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Isar/attrib.ML Tue Oct 22 23:56:48 2024 +0200
@@ -612,6 +612,7 @@
register_config_bool Syntax.ambiguity_warning #>
register_config_int Syntax.ambiguity_limit #>
register_config_bool Syntax_Trans.eta_contract #>
+ register_config_bool Syntax_Phases.const_syntax_legacy #>
register_config_bool Name_Space.names_long #>
register_config_bool Name_Space.names_short #>
register_config_bool Name_Space.names_unique #>
--- a/src/Pure/Isar/proof_context.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Oct 22 23:56:48 2024 +0200
@@ -95,6 +95,7 @@
val read_term_schematic: Proof.context -> string -> term
val read_term_abbrev: Proof.context -> string -> term
val show_abbrevs: bool Config.T
+ val contract_abbrevs: Proof.context -> term -> term
val expand_abbrevs: Proof.context -> term -> term
val cert_term: Proof.context -> term -> term
val cert_prop: Proof.context -> term -> term
@@ -779,7 +780,7 @@
val reports =
(fold o fold_atyps)
(fn T =>
- if Term_Position.is_positionT T then I
+ if Term_Position.detect_positionT T then I
else
(case T of
TFree (x, raw_S) => get_sort_reports (x, ~1) raw_S
@@ -791,7 +792,7 @@
fun replace_sortsT_same get_sort =
Term.map_atyps_same
(fn T =>
- if Term_Position.is_positionT T then raise Same.SAME
+ if Term_Position.detect_positionT T then raise Same.SAME
else
(case T of
TFree (x, raw_S) => TFree (x, Same.function_eq (op =) (get_sort (x, ~1)) raw_S)
--- a/src/Pure/Syntax/ast.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/ast.ML Tue Oct 22 23:56:48 2024 +0200
@@ -104,7 +104,7 @@
(* strip_positions *)
fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
- if member (op =) Term_Position.markers c andalso not (null (Term_Position.decode x))
+ if member (op =) Term_Position.markers c andalso Term_Position.detect x
then mk_appl (strip_positions u) (map strip_positions asts)
else Appl (map strip_positions (t :: u :: v :: asts))
| strip_positions (Appl asts) = Appl (map strip_positions asts)
@@ -163,15 +163,19 @@
exception NO_MATCH;
-fun const_match _ (Constant a) b = a = b
- | const_match _ (Variable a) b = a = b
- | const_match true (Appl [Constant "_constrain", ast, _]) b = const_match false ast b
- | const_match _ _ _ = false;
+fun const_match0 (Constant a) b = a = b
+ | const_match0 (Variable a) b = a = b
+ | const_match0 _ _ = false;
+
+fun const_match true (Appl [Constant "_constrain", ast, _]) b = const_match0 ast b
+ | const_match false (Appl [Constant "_constrain", ast, Variable x]) b =
+ Term_Position.detect x andalso const_match0 ast b
+ | const_match _ a b = const_match0 a b;
fun match1 p ast (Constant b) env = if const_match p ast b then env else raise NO_MATCH
- | match1 p ast (Variable x) env = Symtab.update (x, ast) env
+ | match1 _ ast (Variable x) env = Symtab.update (x, ast) env
| match1 p (Appl asts) (Appl pats) env = match2 p asts pats env
- | match1 p _ _ _ = raise NO_MATCH
+ | match1 _ _ _ _ = raise NO_MATCH
and match2 p (ast :: asts) (pat :: pats) env = match1 p ast pat env |> match2 p asts pats
| match2 _ [] [] env = env
| match2 _ _ _ _ = raise NO_MATCH;
--- a/src/Pure/Syntax/lexicon.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/lexicon.ML Tue Oct 22 23:56:48 2024 +0200
@@ -60,6 +60,9 @@
val read_int: string -> int option
val read_num: string -> {radix: int, leading_zeros: int, value: int}
val read_float: string -> {mant: int, exp: int}
+ val mark_syntax: string -> string
+ val mark_binder: string -> string
+ val mark_indexed: string -> string
val mark_class: string -> string val unmark_class: string -> string val is_class: string -> bool
val mark_type: string -> string val unmark_type: string -> string val is_type: string -> bool
val mark_const: string -> string val unmark_const: string -> string val is_const: string -> bool
@@ -474,10 +477,21 @@
end;
-(* marked logical entities *)
+
+(** marked names **)
fun marker s = (prefix s, unprefix s, String.isPrefix s);
+
+(* syntax consts *)
+
+val (mark_syntax, _, _) = marker "\<^syntax>";
+val (mark_binder, _, _) = marker "\<^binder>";
+val (mark_indexed, _, _) = marker "\<^indexed>";
+
+
+(* logical entities *)
+
val (mark_class, unmark_class, is_class) = marker "\<^class>";
val (mark_type, unmark_type, is_type) = marker "\<^type>";
val (mark_const, unmark_const, is_const) = marker "\<^const>";
--- a/src/Pure/Syntax/mixfix.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML Tue Oct 22 23:56:48 2024 +0200
@@ -1,26 +1,25 @@
(* Title: Pure/Syntax/mixfix.ML
- Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
+ Author: Tobias Nipkow, TU Muenchen
+ Author: Makarius
Mixfix declarations, infixes, binders.
*)
-signature BASIC_MIXFIX =
-sig
- datatype mixfix =
- NoSyn |
- Mixfix of Input.source * int list * int * Position.range |
- Infix of Input.source * int * Position.range |
- Infixl of Input.source * int * Position.range |
- Infixr of Input.source * int * Position.range |
- Binder of Input.source * int * int * Position.range |
- Structure of Position.range
-end;
+datatype mixfix =
+ NoSyn |
+ Mixfix of Input.source * int list * int * Position.range |
+ Infix of Input.source * int * Position.range |
+ Infixl of Input.source * int * Position.range |
+ Infixr of Input.source * int * Position.range |
+ Binder of Input.source * int * int * Position.range |
+ Structure of Position.range;
signature MIXFIX =
sig
- include BASIC_MIXFIX
+ datatype mixfix = datatype mixfix
val mixfix: string -> mixfix
val is_empty: mixfix -> bool
+ val is_infix: mixfix -> bool
val equal: mixfix * mixfix -> bool
val range_of: mixfix -> Position.range
val pos_of: mixfix -> Position.T
@@ -30,7 +29,6 @@
val default_constraint: Proof.context -> mixfix -> typ
val make_type: int -> typ
val binder_name: string -> string
- val is_binder_name: string -> bool
val syn_ext_types: Proof.context -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
val syn_ext_consts: Proof.context -> string list -> (string * typ * mixfix) list ->
Syntax_Ext.syn_ext
@@ -41,20 +39,18 @@
(** mixfix declarations **)
-datatype mixfix =
- NoSyn |
- Mixfix of Input.source * int list * int * Position.range |
- Infix of Input.source * int * Position.range |
- Infixl of Input.source * int * Position.range |
- Infixr of Input.source * int * Position.range |
- Binder of Input.source * int * int * Position.range |
- Structure of Position.range;
+datatype mixfix = datatype mixfix;
fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range);
fun is_empty NoSyn = true
| is_empty _ = false;
+fun is_infix (Infix _) = true
+ | is_infix (Infixl _) = true
+ | is_infix (Infixr _) = true
+ | is_infix _ = false;
+
fun equal (NoSyn, NoSyn) = true
| equal (Mixfix (sy, ps, p, _), Mixfix (sy', ps', p', _)) =
Input.equal_content (sy, sy') andalso ps = ps' andalso p = p'
@@ -171,9 +167,11 @@
(* binder notation *)
val binder_stamp = stamp ();
-val binder_suffix = "_binder"
-val binder_name = suffix binder_suffix;
-val is_binder_name = String.isSuffix binder_suffix;
+
+fun binder_name c =
+ (if Lexicon.is_const c then Lexicon.unmark_const c
+ else if Lexicon.is_fixed c then Lexicon.unmark_fixed c
+ else c) |> Lexicon.mark_binder;
val binder_bg = Symbol_Pos.explode0 "(";
val binder_en = Symbol_Pos.explode0 "_./ _)";
@@ -276,6 +274,3 @@
end;
end;
-
-structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
-open Basic_Mixfix;
--- a/src/Pure/Syntax/syntax_ext.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Tue Oct 22 23:56:48 2024 +0200
@@ -383,7 +383,7 @@
else
let
val indexed_const =
- if const <> "" then const ^ "_indexed"
+ if const <> "" then Lexicon.mark_indexed const
else err_in_mixfix "Missing constant name for indexed syntax";
val rangeT = Term.range_type typ handle Match =>
err_in_mixfix "Missing structure argument for indexed syntax";
--- a/src/Pure/Syntax/syntax_phases.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Tue Oct 22 23:56:48 2024 +0200
@@ -15,6 +15,7 @@
Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result
val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
val term_of_typ: Proof.context -> typ -> term
+ val const_syntax_legacy: bool Config.T
val print_checks: Proof.context -> unit
val typ_check: int -> string -> (Proof.context -> typ list -> typ list) ->
Context.generic -> Context.generic
@@ -117,8 +118,7 @@
(* decode_typ *)
-fun decode_pos (Free (s, _)) =
- if not (null (Term_Position.decode s)) then SOME s else NONE
+fun decode_pos (Free (x, _)) = if Term_Position.detect x then SOME x else NONE
| decode_pos _ = NONE;
fun decode_typ tm =
@@ -153,6 +153,15 @@
(* parsetree_to_ast *)
+val const_syntax_legacy = Config.declare_bool ("const_syntax_legacy", \<^here>) (K false);
+
+fun parsetree_literals (Parser.Markup (_, ts)) = maps parsetree_literals ts
+ | parsetree_literals (Parser.Node _) = []
+ | parsetree_literals (Parser.Tip tok) =
+ if Lexicon.is_literal tok andalso
+ not (null (Lexicon.literal_markup (Lexicon.str_of_token tok)))
+ then [Lexicon.pos_of_token tok] else [];
+
fun parsetree_to_ast ctxt trf parsetree =
let
val reports = Unsynchronized.ref ([]: Position.report_text list);
@@ -177,11 +186,6 @@
val ast_of_position = ast_of_pos o single o report_pos;
fun ast_of_position' a = Ast.constrain (Ast.Constant a) o ast_of_position;
- fun trans a args =
- (case trf a of
- NONE => Ast.mk_appl (Ast.Constant a) args
- | SOME f => f ctxt args);
-
fun asts_of_token tok =
if Lexicon.valued_token tok
then [Ast.Variable (Lexicon.str_of_token tok)]
@@ -223,7 +227,20 @@
let val args = maps asts_of pts
in [Ast.Appl (Ast.Constant "_constrain" :: ast_of_position' "_idtdummy" tok :: args)] end
| asts_of (Parser.Node ({const = a, ...}, pts)) =
- (report_literals a pts; [trans a (maps asts_of pts)])
+ let
+ val ps = maps parsetree_literals pts;
+ val args = maps asts_of pts;
+ fun head () =
+ if (Lexicon.is_fixed a orelse Lexicon.is_const a)
+ andalso not (Config.get ctxt const_syntax_legacy)
+ then Ast.constrain (Ast.Constant a) (ast_of_pos ps)
+ else Ast.Constant a;
+ val _ = List.app (fn pos => report pos markup_cache a) ps;
+ in
+ [case trf a of
+ SOME f => f ctxt args
+ | NONE => Ast.mk_appl (head ()) args]
+ end
| asts_of (Parser.Tip tok) = asts_of_token tok
and ast_of pt =
@@ -304,15 +321,13 @@
| decode _ _ bs (t $ u) = decode [] [] bs t $ decode [] [] bs u
| decode ps _ _ (Const (a, T)) =
(case try Lexicon.unmark_fixed a of
- SOME x => (report ps markup_free_cache x; Free (x, T))
+ SOME x => Free (x, T)
| NONE =>
- let
- val c =
- (case try Lexicon.unmark_const a of
- SOME c => c
- | NONE => #1 (decode_const ctxt (a, [])));
- val _ = report ps markup_const_cache c;
- in Const (c, T) end)
+ (case try Lexicon.unmark_const a of
+ SOME c => Const (c, T)
+ | NONE =>
+ let val c = #1 (decode_const ctxt (a, []))
+ in report ps markup_const_cache c; Const (c, T) end))
| decode ps _ _ (Free (a, T)) =
((Name.reject_internal (a, ps) handle ERROR msg =>
error (msg ^ Proof_Context.consts_completion_message ctxt (a, ps)));
@@ -546,7 +561,7 @@
fun term_of (Type (a, Ts)) =
Term.list_comb (Syntax.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) =
- if not (null (Term_Position.decode x)) then Syntax.free x
+ if Term_Position.detect x then Syntax.free x
else ofsort (Syntax.const "_tfree" $ Syntax.free x) S
| term_of (TVar (xi, S)) = ofsort (Syntax.const "_tvar" $ Syntax.var xi) S;
in term_of ty end;
--- a/src/Pure/Syntax/syntax_trans.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML Tue Oct 22 23:56:48 2024 +0200
@@ -205,7 +205,7 @@
fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
| update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
| update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
- if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+ if Term_Position.detect_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
else
list_comb (c $ update_name_tr [t] $
(Lexicon.fun_type $
--- a/src/Pure/Syntax/term_position.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML Tue Oct 22 23:56:48 2024 +0200
@@ -8,13 +8,14 @@
sig
val pretty: Position.T list -> Pretty.T
val encode: Position.T list -> string
+ val detect: string -> bool
val decode: string -> Position.T list
+ val detect_position: term -> bool
val decode_position: term -> (Position.T list * typ) option
val decode_position1: term -> Position.T option
+ val detect_positionT: typ -> bool
val decode_positionT: typ -> Position.T list
val decode_positionS: sort -> Position.T list * sort
- val is_position: term -> bool
- val is_positionT: typ -> bool
val markers: string list
val strip_positions: term -> term
end;
@@ -37,22 +38,42 @@
else NONE
| decode_pos _ = NONE;
+
+(* encode *)
+
+val encode_none = YXML.string_of (encode_pos Position.none);
+
fun encode ps =
- YXML.string_of_body (map encode_pos (if null ps then [Position.none] else ps));
+ (case remove (op =) Position.none ps of
+ [] => encode_none
+ | ps' => YXML.string_of_body (map encode_pos (distinct (op =) ps')));
+
+val encode_prefix = YXML.XY ^ Markup.positionN;
+
+
+(* decode *)
+
+val detect = String.isPrefix encode_prefix;
fun decode str =
- let
- val xml = YXML.parse_body str handle Fail msg => error msg;
- val ps = map decode_pos xml;
- in
- if not (null ps) andalso forall is_some ps then map the ps
- else if forall is_none ps then []
- else error ("Bad encoded positions: " ^ quote str)
- end;
+ if str = encode_none then [Position.none]
+ else if detect str then
+ let
+ val xml = YXML.parse_body str handle Fail msg => error msg;
+ val ps = map decode_pos xml;
+ in
+ if not (null ps) andalso forall is_some ps then map the ps
+ else if forall is_none ps then []
+ else error ("Bad encoded positions: " ^ quote str)
+ end
+ else [];
(* positions within parse trees *)
+fun detect_position (Free (x, _)) = detect x
+ | detect_position _ = false;
+
fun decode_position (Free (x, _)) =
(case decode x of
[] => NONE
@@ -65,20 +86,23 @@
| pos :: _ => SOME pos)
| decode_position1 _ = NONE;
+fun detect_positionT (TFree (x, _)) = detect x
+ | detect_positionT _ = false;
+
fun decode_positionT (TFree (x, _)) = decode x
| decode_positionT _ = [];
fun decode_positionS cs =
- let val (ps, sort) = List.partition (not o null o decode) cs
+ let val (ps, sort) = List.partition detect cs
in (maps decode ps, sort) end;
-val is_position = is_some o decode_position;
-val is_positionT = not o null o decode_positionT;
+
+(* strip_positions *)
val markers = ["_constrain", "_constrainAbs", "_ofsort"];
fun strip_positions ((t as Const (c, _)) $ u $ v) =
- if member (op =) markers c andalso is_position v
+ if member (op =) markers c andalso detect_position v
then strip_positions u
else t $ strip_positions u $ strip_positions v
| strip_positions (t $ u) = strip_positions t $ strip_positions u
--- a/src/Pure/pure_thy.ML Tue Oct 22 17:32:34 2024 +0200
+++ b/src/Pure/pure_thy.ML Tue Oct 22 23:56:48 2024 +0200
@@ -219,7 +219,7 @@
("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",
mixfix ("(\<open>indent=3 notation=abstraction\<close>%_./ _)", [0, 3], 3)),
(const "Pure.eq", typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("==", 2)),
- (const "Pure.all_binder", typ "idts \<Rightarrow> prop \<Rightarrow> prop",
+ (Mixfix.binder_name "Pure.all", typ "idts \<Rightarrow> prop \<Rightarrow> prop",
mixfix ("(\<open>indent=3 notation=\<open>binder !!\<close>\<close>!!_./ _)", [0, 0], 0)),
(const "Pure.imp", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("==>", 1)),
("_DDDOT", typ "aprop", Mixfix.mixfix "..."),