--- a/src/HOL/HOLCF/Cfun.thy Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/HOLCF/Cfun.thy Wed Apr 06 23:04:00 2011 +0200
@@ -57,7 +57,7 @@
let
fun Lambda_ast_tr [pats, body] =
Ast.fold_ast_p @{syntax_const "_cabs"}
- (Ast.unfold_ast @{syntax_const "_cargs"} (Syntax.strip_positions_ast pats), body)
+ (Ast.unfold_ast @{syntax_const "_cargs"} (Ast.strip_positions pats), body)
| Lambda_ast_tr asts = raise Ast.AST ("Lambda_ast_tr", asts);
in [(@{syntax_const "_Lambda"}, Lambda_ast_tr)] end;
*}
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Wed Apr 06 23:04:00 2011 +0200
@@ -456,7 +456,7 @@
fun con1 authentic n (con,args) =
Library.foldl capp (c_ast authentic con, argvars n args)
fun case1 authentic (n, c) =
- app "_case1" (Syntax.strip_positions_ast (con1 authentic n c), expvar n)
+ app "_case1" (Ast.strip_positions (con1 authentic n c), expvar n)
fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
fun when1 n (m, c) = if n = m then arg1 (n, c) else Ast.Constant @{const_syntax bottom}
val case_constant = Ast.Constant (syntax (case_const dummyT))
--- a/src/HOL/List.thy Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/List.thy Wed Apr 06 23:04:00 2011 +0200
@@ -385,7 +385,7 @@
let
val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
val e = if opti then singl e else e;
- val case1 = Syntax.const @{syntax_const "_case1"} $ Syntax.strip_positions p $ e;
+ val case1 = Syntax.const @{syntax_const "_case1"} $ Term_Position.strip_positions p $ e;
val case2 =
Syntax.const @{syntax_const "_case1"} $
Syntax.const @{const_syntax dummy_pattern} $ NilC;
--- a/src/HOL/Statespace/state_space.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML Wed Apr 06 23:04:00 2011 +0200
@@ -624,7 +624,7 @@
else raise TERM ("StateSpace.gen_lookup_tr: component " ^ n ^ " not defined",[]));
fun lookup_tr ctxt [s, x] =
- (case Syntax.strip_positions x of
+ (case Term_Position.strip_positions x of
Free (n,_) => gen_lookup_tr ctxt s n
| _ => raise Match);
@@ -656,7 +656,7 @@
end;
fun update_tr ctxt [s, x, v] =
- (case Syntax.strip_positions x of
+ (case Term_Position.strip_positions x of
Free (n, _) => gen_update_tr false ctxt n v s
| _ => raise Match);
--- a/src/Pure/IsaMakefile Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/IsaMakefile Wed Apr 06 23:04:00 2011 +0200
@@ -188,7 +188,7 @@
Syntax/syn_trans.ML \
Syntax/syntax.ML \
Syntax/syntax_phases.ML \
- Syntax/type_ext.ML \
+ Syntax/term_position.ML \
System/isabelle_process.ML \
System/isabelle_system.ML \
System/isar.ML \
--- a/src/Pure/ROOT.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/ROOT.ML Wed Apr 06 23:04:00 2011 +0200
@@ -114,16 +114,16 @@
use "sorts.ML";
use "type.ML";
use "logic.ML";
-use "Syntax/lexicon.ML";
-use "Syntax/simple_syntax.ML";
(* inner syntax *)
+use "Syntax/term_position.ML";
+use "Syntax/lexicon.ML";
+use "Syntax/simple_syntax.ML";
use "Syntax/ast.ML";
use "Syntax/syn_ext.ML";
use "Syntax/parser.ML";
-use "Syntax/type_ext.ML";
use "Syntax/syn_trans.ML";
use "Syntax/mixfix.ML";
use "Syntax/printer.ML";
--- a/src/Pure/Syntax/ast.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/ast.ML Wed Apr 06 23:04:00 2011 +0200
@@ -14,6 +14,7 @@
exception AST of string * ast list
val pretty_ast: ast -> Pretty.T
val pretty_rule: ast * ast -> Pretty.T
+ val strip_positions: ast -> ast
val head_of_rule: ast * ast -> string
val rule_error: ast * ast -> string option
val fold_ast: string -> ast list -> ast
@@ -57,8 +58,8 @@
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
| pretty_ast (Variable x) =
- (case Lexicon.decode_position x of
- SOME pos => Lexicon.pretty_position pos
+ (case Term_Position.decode x of
+ SOME pos => Term_Position.pretty pos
| NONE => Pretty.str x)
| pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
@@ -66,7 +67,17 @@
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
-(* head_of_ast, head_of_rule *)
+(* strip_positions *)
+
+fun strip_positions (Appl ((t as Constant c) :: u :: (v as Variable x) :: asts)) =
+ if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (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)
+ | strip_positions ast = ast;
+
+
+(* head_of_ast and head_of_rule *)
fun head_of_ast (Constant a) = a
| head_of_ast (Appl (Constant a :: _)) = a
--- a/src/Pure/Syntax/lexicon.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML Wed Apr 06 23:04:00 2011 +0200
@@ -44,9 +44,6 @@
val is_marked: string -> bool
val dummy_type: term
val fun_type: term
- val pretty_position: Position.T -> Pretty.T
- val encode_position: Position.T -> string
- val decode_position: string -> Position.T option
end;
signature LEXICON =
@@ -459,24 +456,4 @@
exp = length fracpart}
end;
-
-(* positions *)
-
-val position_dummy = "<position>";
-val position_text = XML.Text position_dummy;
-
-fun pretty_position pos =
- Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
-
-fun encode_position pos =
- YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
-
-fun decode_position str =
- (case YXML.parse_body str handle Fail msg => error msg of
- [XML.Elem ((name, props), [arg])] =>
- if name = Markup.positionN andalso arg = position_text
- then SOME (Position.of_properties props)
- else NONE
- | _ => NONE);
-
end;
--- a/src/Pure/Syntax/syn_trans.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Wed Apr 06 23:04:00 2011 +0200
@@ -86,7 +86,7 @@
(* strip_positions *)
-fun strip_positions_ast_tr [ast] = Type_Ext.strip_positions_ast ast
+fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
| strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
@@ -223,7 +223,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 Type_Ext.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
+ if Term_Position.is_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/syntax.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Wed Apr 06 23:04:00 2011 +0200
@@ -16,7 +16,6 @@
sig
include LEXICON0
include SYN_EXT0
- include TYPE_EXT0
include SYN_TRANS1
include MIXFIX1
include PRINTER0
@@ -795,7 +794,7 @@
(*export parts of internal Syntax structures*)
val syntax_tokenize = tokenize;
-open Lexicon Syn_Ext Type_Ext Syn_Trans Mixfix Printer;
+open Lexicon Syn_Ext Syn_Trans Mixfix Printer;
val tokenize = syntax_tokenize;
end;
@@ -804,6 +803,5 @@
open Basic_Syntax;
forget_structure "Syn_Ext";
-forget_structure "Type_Ext";
forget_structure "Mixfix";
--- a/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 22:25:44 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Apr 06 23:04:00 2011 +0200
@@ -119,7 +119,7 @@
| ast_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
if constrain_pos then
Ast.Appl [Ast.Constant "_constrain", ast_of pt,
- Ast.Variable (Lexicon.encode_position (Lexicon.pos_of_token tok))]
+ Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]
else ast_of pt
| ast_of (Parser.Node (a, pts)) = trans a (map ast_of pts)
| ast_of (Parser.Tip tok) = Ast.Variable (Lexicon.str_of_token tok);
@@ -172,11 +172,11 @@
fun report ps = Position.reports reports ps;
fun decode ps qs bs (Const ("_constrain", _) $ t $ typ) =
- (case Syntax.decode_position_term typ of
+ (case Term_Position.decode_position typ of
SOME p => decode (p :: ps) qs bs t
| NONE => Type.constraint (decodeT typ) (decode ps qs bs t))
| decode ps qs bs (Const ("_constrainAbs", _) $ t $ typ) =
- (case Syntax.decode_position_term typ of
+ (case Term_Position.decode_position typ of
SOME q => decode ps (q :: qs) bs t
| NONE => Type.constraint (decodeT typ --> dummyT) (decode ps qs bs t))
| decode _ qs bs (Abs (x, T, t)) =
@@ -418,7 +418,7 @@
fun term_of (Type (a, Ts)) =
Term.list_comb (Lexicon.const (Lexicon.mark_type a), map term_of Ts)
| term_of (TFree (x, S)) =
- if is_some (Lexicon.decode_position x) then Lexicon.free x
+ if is_some (Term_Position.decode x) then Lexicon.free x
else of_sort (Lexicon.const "_tfree" $ Lexicon.free x) S
| term_of (TVar (xi, S)) = of_sort (Lexicon.const "_tvar" $ Lexicon.var xi) S;
in term_of ty end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Syntax/term_position.ML Wed Apr 06 23:04:00 2011 +0200
@@ -0,0 +1,55 @@
+(* Title: Pure/Syntax/term_position.ML
+ Author: Makarius
+
+Encoded position within term syntax trees.
+*)
+
+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 option
+ val is_position: term -> bool
+ val strip_positions: term -> term
+end;
+
+structure Term_Position: TERM_POSITION =
+struct
+
+(* markup *)
+
+val position_dummy = "<position>";
+val position_text = XML.Text position_dummy;
+
+fun pretty pos =
+ Pretty.markup (Position.markup pos Markup.position) [Pretty.str position_dummy];
+
+fun encode pos =
+ YXML.string_of (XML.Elem (Position.markup pos Markup.position, [position_text]));
+
+fun decode str =
+ (case YXML.parse_body str handle Fail msg => error msg of
+ [XML.Elem ((name, props), [arg])] =>
+ if name = Markup.positionN andalso arg = position_text
+ then SOME (Position.of_properties props)
+ else NONE
+ | _ => NONE);
+
+
+(* positions within parse trees *)
+
+fun decode_position (Free (x, _)) = decode x
+ | decode_position _ = NONE;
+
+val is_position = is_some o decode_position;
+
+fun strip_positions ((t as Const (c, _)) $ u $ v) =
+ if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
+ then strip_positions u
+ else t $ strip_positions u $ strip_positions v
+ | strip_positions (t $ u) = strip_positions t $ strip_positions u
+ | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
+ | strip_positions t = t;
+
+end;
--- a/src/Pure/Syntax/type_ext.ML Wed Apr 06 22:25:44 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-(* Title: Pure/Syntax/type_ext.ML
- Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
-
-Utilities for input and output of types. The concrete syntax of types.
-*)
-
-signature TYPE_EXT0 =
-sig
- val decode_position_term: term -> Position.T option
- val is_position: term -> bool
- val strip_positions: term -> term
- val strip_positions_ast: Ast.ast -> Ast.ast
-end;
-
-signature TYPE_EXT =
-sig
- include TYPE_EXT0
-end;
-
-structure Type_Ext: TYPE_EXT =
-struct
-
-(** input utils **)
-
-(* positions *)
-
-fun decode_position_term (Free (x, _)) = Lexicon.decode_position x
- | decode_position_term _ = NONE;
-
-val is_position = is_some o decode_position_term;
-
-fun strip_positions ((t as Const (c, _)) $ u $ v) =
- if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v
- then strip_positions u
- else t $ strip_positions u $ strip_positions v
- | strip_positions (t $ u) = strip_positions t $ strip_positions u
- | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t)
- | strip_positions t = t;
-
-fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) =
- if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x)
- then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts)
- else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts))
- | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts)
- | strip_positions_ast ast = ast;
-
-end;