954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory Test
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
atom_decl name
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
(* test for how to add datatypes *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
setup {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
Datatype.datatype_cmd
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
["foo"]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
[([], @{binding "foo"}, NoSyn,
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
[(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)])
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
thm foo.recs
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
thm foo.induct
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
ML{*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
fun filtered_input str =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
(* type plus possible annotation *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
val anno_typ =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
(Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
32 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
34 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
35 |
parse (Scan.repeat anno_typ) (filtered_input "x::string bool")
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
ML {* OuterParse.enum "," ; OuterParse.and_list1 *}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
(* binding specification *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
datatype bind = B of string * string | BS of string * string
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
val _ = OuterKeyword.keyword "bind"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
val _ = OuterKeyword.keyword "bindset"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
val bind_parse_aux =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
(OuterParse.$$$ "bind" >> (K B))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
|| (OuterParse.$$$ "bindset" >> (K BS))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
(* should use and_list *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
val bind_parser =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
OuterParse.enum ","
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
((bind_parse_aux -- OuterParse.term) --
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
(OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2)))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
(* datatype parser *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
val dt_parser =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix --
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
(OuterParse.$$$ "=" |-- OuterParse.enum1 "|"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
(OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
(* function equation parser *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
67 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
68 |
val fun_parser =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
Scan.optional
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[])
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
71 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
72 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
73 |
(* main parser *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
74 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
75 |
val parser =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
OuterParse.and_list1 dt_parser -- fun_parser
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
(* printing stuff *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
fun print_str_option NONE = "NONE"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
| print_str_option (SOME s) = (s:bstring)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
fun print_anno_typ (NONE, ty) = ty
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
87 |
| print_anno_typ (SOME x, ty) = x ^ ":" ^ ty
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
88 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
89 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
90 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
91 |
fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
92 |
| print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
93 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
94 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
fun print_constr (((name, anno_tys), bds), syn) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
(Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ " "
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
98 |
^ (commas (map print_bind bds)) ^ " "
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
99 |
^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
fun single_dt (((s2, s3), syn), constrs) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
["constructor declaration"]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
105 |
@ ["type arguments: "] @ s2
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
106 |
@ ["datatype name: ", Binding.name_of s3]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
107 |
@ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
108 |
@ ["constructors: "] @ (map print_constr constrs)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
109 |
|> separate "\n"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
|> implode
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
111 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
ML {* fun single_fun_eq (at, s) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
["function equations: ", s]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
115 |
|> separate "\n"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
116 |
|> implode
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
ML {* fun single_fun_fix (b, _, _) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
120 |
["functions: ", Binding.name_of b]
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
|> separate "\n"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
122 |
|> implode
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
123 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
124 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
125 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
126 |
fun print_dts (dts, (funs, feqs)) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
127 |
let
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
128 |
val _ = warning (implode (separate "\n" (map single_dt dts)))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
val _ = warning (implode (separate "\n" (map single_fun_fix funs)))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
val _ = warning (implode (separate "\n" (map single_fun_eq feqs)))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
in
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
()
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
133 |
end
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
136 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
parser;
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
Datatype.datatype_cmd;
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
fun transp_ty_arg (anno, ty) = ty
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
fun transp_constr (((constr_name, ty_args), bind), mx) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
(constr_name, map transp_ty_arg ty_args, mx)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
146 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
fun transp_dt (((ty_args, ty_name), mx), constrs) =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
(ty_args, ty_name, mx, map transp_constr constrs)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
149 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
151 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
152 |
fun dt_defn dts thy =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
let
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
154 |
val names = map (fn (_, s, _, _) => Binding.name_of s) dts
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
155 |
val thy' = Datatype.datatype_cmd names dts thy
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
156 |
in
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
157 |
thy'
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
end
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
161 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
162 |
fun fn_defn [] [] thy = thy
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
163 |
| fn_defn funs feqs thy =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
164 |
let
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
165 |
val lthy = Theory_Target.init NONE thy
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
166 |
val ctxt = Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
167 |
val thy' = ProofContext.theory_of ctxt
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
168 |
in
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
thy'
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
end
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
174 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
175 |
fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
176 |
let
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
177 |
val thy1 = dt_defn (map transp_dt dts) thy
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
178 |
val thy2 = fn_defn funs feqs thy1
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
val _ = print_dts (dts, (funs, feqs))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
in
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
181 |
thy2
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
182 |
end *}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
183 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
184 |
(* Command Keyword *)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
185 |
ML {*
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
186 |
let
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
187 |
val kind = OuterKeyword.thy_decl
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
188 |
in
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
189 |
OuterSyntax.command "nominal_datatype" "test" kind
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
190 |
(parser >> (Toplevel.theory o nominal_datatype2_cmd))
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
191 |
end
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
192 |
*}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
193 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
194 |
text {* example 1 *}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
195 |
nominal_datatype lam =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
196 |
VAR "name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
197 |
| APP "lam" "lam"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
198 |
| LET bp::"bp" t::"lam" bind "bi bp" in t ("Let _ in _" [100,100] 100)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
199 |
and bp =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
200 |
BP "name" "lam" ("_ ::= _" [100,100] 100)
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
201 |
binder
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
202 |
bi::"bp \<Rightarrow> name set"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
203 |
where
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
204 |
"bi (BP x t) = {x}"
|
961
|
205 |
print_theorems
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
206 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
207 |
text {* examples 2 *}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
208 |
nominal_datatype trm =
|
961
|
209 |
Var "name"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
210 |
| App "trm" "trm"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
211 |
| Lam x::"name" t::"trm" bindset x in t
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
212 |
| Let p::"pat" "trm" t::"trm" bind "f p" in t
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
213 |
and pat =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
214 |
PN
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
215 |
| PS "name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
216 |
| PD "name \<times> name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
217 |
binder
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
218 |
f::"pat \<Rightarrow> name set"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
219 |
where
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
220 |
"f PN = {}"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
221 |
| "f (PS x) = {x}"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
222 |
| "f (PD (x,y)) = {x,y}"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
223 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
224 |
nominal_datatype trm2 =
|
962
|
225 |
Var2 "name"
|
954
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
226 |
| App2 "trm2" "trm2"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
227 |
| Lam2 x::"name" t::"trm2" bindset x in t
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
228 |
| Let2 p::"pat2" "trm2" t::"trm2" bind "f2 p" in t
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
229 |
and pat2 =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
230 |
PN2
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
231 |
| PS2 "name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
232 |
| PD2 "pat2 \<times> pat2"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
233 |
binder
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
234 |
f2::"pat2 \<Rightarrow> name set"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
235 |
where
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
236 |
"f2 PN2 = {}"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
237 |
| "f2 (PS2 x) = {x}"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
238 |
| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
239 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
240 |
text {* example type schemes *}
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
241 |
datatype ty =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
242 |
Var "name"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
243 |
| Fun "ty" "ty"
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
244 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
245 |
nominal_datatype tyS =
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
246 |
All xs::"name list" ty::"ty" bindset xs in ty
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
247 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
248 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
249 |
|
c009d2535896
very rough example file for how nominal2 specification can be parsed
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
250 |
|
961
|
251 |
end
|