1 (* Title: Pure/Syntax/type_ext.ML |
|
2 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
3 |
|
4 Utilities for input and output of types. The concrete syntax of types. |
|
5 *) |
|
6 |
|
7 signature TYPE_EXT0 = |
|
8 sig |
|
9 val decode_position_term: term -> Position.T option |
|
10 val is_position: term -> bool |
|
11 val strip_positions: term -> term |
|
12 val strip_positions_ast: Ast.ast -> Ast.ast |
|
13 end; |
|
14 |
|
15 signature TYPE_EXT = |
|
16 sig |
|
17 include TYPE_EXT0 |
|
18 end; |
|
19 |
|
20 structure Type_Ext: TYPE_EXT = |
|
21 struct |
|
22 |
|
23 (** input utils **) |
|
24 |
|
25 (* positions *) |
|
26 |
|
27 fun decode_position_term (Free (x, _)) = Lexicon.decode_position x |
|
28 | decode_position_term _ = NONE; |
|
29 |
|
30 val is_position = is_some o decode_position_term; |
|
31 |
|
32 fun strip_positions ((t as Const (c, _)) $ u $ v) = |
|
33 if (c = "_constrain" orelse c = "_constrainAbs") andalso is_position v |
|
34 then strip_positions u |
|
35 else t $ strip_positions u $ strip_positions v |
|
36 | strip_positions (t $ u) = strip_positions t $ strip_positions u |
|
37 | strip_positions (Abs (x, T, t)) = Abs (x, T, strip_positions t) |
|
38 | strip_positions t = t; |
|
39 |
|
40 fun strip_positions_ast (Ast.Appl ((t as Ast.Constant c) :: u :: (v as Ast.Variable x) :: asts)) = |
|
41 if (c = "_constrain" orelse c = "_constrainAbs") andalso is_some (Lexicon.decode_position x) |
|
42 then Ast.mk_appl (strip_positions_ast u) (map strip_positions_ast asts) |
|
43 else Ast.Appl (map strip_positions_ast (t :: u :: v :: asts)) |
|
44 | strip_positions_ast (Ast.Appl asts) = Ast.Appl (map strip_positions_ast asts) |
|
45 | strip_positions_ast ast = ast; |
|
46 |
|
47 end; |
|