--- a/src/HOL/ex/Cartouche_Examples.thy Sun Oct 20 22:40:18 2024 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Oct 21 11:55:51 2024 +0200
@@ -70,8 +70,8 @@
let fun err () = raise TERM ("string_tr", args) in
(case args of
[(c as Const (\<^syntax_const>\<open>_constrain\<close>, _)) $ Free (s, _) $ p] =>
- (case Term_Position.decode_position p of
- SOME (pos, _) => c $ mk_string (content (s, pos)) $ p
+ (case Term_Position.decode_position1 p of
+ SOME pos => c $ mk_string (content (s, pos)) $ p
| NONE => err ())
| _ => err ())
end;
--- a/src/Pure/Isar/specification.ML Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Isar/specification.ML Mon Oct 21 11:55:51 2024 +0200
@@ -94,7 +94,7 @@
fun get Cs (Const ("_type_constraint_", C) $ t) = get (C :: Cs) t
| get Cs (Free (y, T)) =
if x = y then
- map_filter Term_Position.decode_positionT
+ maps Term_Position.decode_positionT
(T :: map (Type.constraint_type ctxt) Cs)
else []
| get _ (t $ u) = get [] t @ get [] u
--- a/src/Pure/Syntax/ast.ML Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/ast.ML Mon Oct 21 11:55:51 2024 +0200
@@ -88,8 +88,8 @@
fun pretty_var x =
(case Term_Position.decode x of
- SOME pos => Term_Position.pretty pos
- | NONE => Pretty.str x);
+ [] => Pretty.str x
+ | ps => Term_Position.pretty ps);
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
| pretty_ast (Variable x) = pretty_var x
@@ -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 is_some (Term_Position.decode x)
+ if member (op =) Term_Position.markers c andalso not (null (Term_Position.decode 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)
--- a/src/Pure/Syntax/syntax_phases.ML Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Oct 21 11:55:51 2024 +0200
@@ -118,7 +118,7 @@
(* decode_typ *)
fun decode_pos (Free (s, _)) =
- if is_some (Term_Position.decode s) then SOME s else NONE
+ if not (null (Term_Position.decode s)) then SOME s else NONE
| decode_pos _ = NONE;
fun decode_typ tm =
@@ -174,7 +174,7 @@
if Lexicon.is_literal tok then report (report_pos tok) markup_cache a else ());
val ast_of_pos = Ast.Variable o Term_Position.encode;
- val ast_of_position = ast_of_pos o report_pos;
+ 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 =
@@ -290,11 +290,11 @@
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
(case Term_Position.decode_position typ of
- SOME (p, T) => Type.constraint T (decode (p :: ps) qs bs t)
+ SOME (ps', T) => Type.constraint T (decode (ps' @ ps) qs bs t)
| NONE => Type.constraint (decode_typ typ) (decode ps qs bs t))
| decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
(case Term_Position.decode_position typ of
- SOME (q, T) => Type.constraint (T --> dummyT) (decode ps (q :: qs) bs t)
+ SOME (qs', T) => Type.constraint (T --> dummyT) (decode ps (qs' @ qs) bs t)
| NONE => Type.constraint (decode_typ typ --> dummyT) (decode ps qs bs t))
| decode _ qs bs (Abs (x, T, t)) =
let
@@ -494,8 +494,8 @@
| decode ps (Ast.Appl (asts as (Ast.Constant c :: ast :: Ast.Variable x :: args))) =
if member (op =) Term_Position.markers c then
(case Term_Position.decode x of
- SOME p => Ast.mk_appl (decode (p :: ps) ast) (map (decode ps) args)
- | NONE => decode_appl ps asts)
+ [] => decode_appl ps asts
+ | ps' => Ast.mk_appl (decode (ps' @ ps) ast) (map (decode ps) args))
else decode_appl ps asts
| decode ps (Ast.Appl asts) = decode_appl ps asts;
@@ -546,7 +546,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 is_some (Term_Position.decode x) then Syntax.free x
+ if not (null (Term_Position.decode 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;
@@ -877,8 +877,7 @@
(case asts of
[Ast.Appl [Ast.Constant "_constrain", Ast.Variable c, T as Ast.Variable p]] =>
let
- val pos = the_default Position.none (Term_Position.decode p);
- val (c', _) = decode_const ctxt (c, [pos]);
+ val (c', _) = decode_const ctxt (c, Term_Position.decode p);
val d = if intern then Lexicon.mark_const c' else c;
in Ast.constrain (Ast.Constant d) T end
| _ => raise Ast.AST ("const_ast_tr", asts));
--- a/src/Pure/Syntax/term_position.ML Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/Syntax/term_position.ML Mon Oct 21 11:55:51 2024 +0200
@@ -1,16 +1,17 @@
(* Title: Pure/Syntax/term_position.ML
Author: Makarius
-Encoded position within term syntax trees.
+Positions within term syntax trees (non-empty list).
*)
signature TERM_POSITION =
sig
- val pretty: Position.T -> Pretty.T
- val encode: Position.T -> string
- val decode: string -> Position.T option
- val decode_position: term -> (Position.T * typ) option
- val decode_positionT: typ -> Position.T option
+ val pretty: Position.T list -> Pretty.T
+ val encode: Position.T list -> string
+ val decode: string -> Position.T list
+ val decode_position: term -> (Position.T list * typ) option
+ val decode_position1: term -> Position.T option
+ 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
@@ -26,37 +27,53 @@
val position_dummy = "<position>";
val position_text = XML.Text position_dummy;
-fun pretty pos = Pretty.mark_str_position (pos, position_dummy);
+fun pretty ps = Pretty.marks_str (map Position.markup ps, position_dummy);
-fun encode pos =
- YXML.string_of (XML.Elem (Position.markup pos, [position_text]));
+fun encode_pos pos = XML.Elem (Position.markup pos, [position_text]);
-fun decode str =
- (case YXML.parse_body str handle Fail msg => error msg of
- [XML.Elem ((name, props), [arg])] =>
+fun decode_pos (XML.Elem ((name, props), [arg])) =
if name = Markup.positionN andalso arg = position_text
then SOME (Position.of_properties props)
else NONE
- | _ => NONE);
+ | decode_pos _ = NONE;
+
+fun encode ps =
+ YXML.string_of_body (map encode_pos (if null ps then [Position.none] else ps));
+
+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;
(* positions within parse trees *)
fun decode_position (Free (x, _)) =
(case decode x of
- SOME pos => SOME (pos, TFree (x, dummyS))
- | NONE => NONE)
+ [] => NONE
+ | ps => SOME (ps, TFree (x, dummyS)))
| decode_position _ = NONE;
+fun decode_position1 (Free (x, _)) =
+ (case decode x of
+ [] => NONE
+ | pos :: _ => SOME pos)
+ | decode_position1 _ = NONE;
+
fun decode_positionT (TFree (x, _)) = decode x
- | decode_positionT _ = NONE;
+ | decode_positionT _ = [];
fun decode_positionS cs =
- let val (ps, sort) = List.partition (is_some o decode) cs
- in (map (the o decode) ps, sort) end;
+ let val (ps, sort) = List.partition (not o null o decode) cs
+ in (maps decode ps, sort) end;
val is_position = is_some o decode_position;
-val is_positionT = is_some o decode_positionT;
+val is_positionT = not o null o decode_positionT;
val markers = ["_constrain", "_constrainAbs", "_ofsort"];
--- a/src/Pure/type_infer_context.ML Sun Oct 20 22:40:18 2024 +0200
+++ b/src/Pure/type_infer_context.ML Mon Oct 21 11:55:51 2024 +0200
@@ -125,10 +125,12 @@
in (Type (a, Ts'), ps_idx') end
| prepareT T (ps, idx) =
(case Term_Position.decode_positionT T of
- SOME pos =>
- let val U = Type_Infer.mk_param idx []
- in (U, ((pos, U) :: ps, idx + 1)) end
- | NONE => (T, (ps, idx)));
+ [] => (T, (ps, idx))
+ | pos =>
+ let
+ val U = Type_Infer.mk_param idx [];
+ val ps' = map (rpair U) pos;
+ in (U, (ps' @ ps, idx + 1)) end);
fun prepare (Const ("_type_constraint_", T)) ps_idx =
let