changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
--- a/Nominal/Ex/CoreHaskell.thy Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/CoreHaskell.thy Sat Aug 21 16:20:10 2010 +0800
@@ -20,7 +20,7 @@
| TC "string"
| TApp "ty" "ty"
| TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty" bind_set tv in T
+| TAll tv::"tvar" "tkind" T::"ty" bind (set) tv in T
| TEq "ckind" "ty"
and ty_lst =
TsNil
@@ -30,7 +30,7 @@
| CConst "string"
| CApp "co" "co"
| CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co" bind_set cv in C
+| CAll cv::"cvar" "ckind" C::"co" bind (set) cv in C
| CEq "ckind" "co"
| CRefl "ty"
| CSym "co"
@@ -48,13 +48,13 @@
and trm =
Var "var"
| K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
+| LAMT tv::"tvar" "tkind" t::"trm" bind (set) tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind (set) cv in t
| AppT "trm" "ty"
| AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm" bind_set v in t
+| Lam v::"var" "ty" t::"trm" bind (set) v in t
| App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind_set x in t
+| Let x::"var" "ty" "trm" t::"trm" bind (set) x in t
| Case "trm" "assoc_lst"
| Cast "trm" "ty" --"ty is supposed to be a coercion type only"
and assoc_lst =
--- a/Nominal/Ex/Lambda.thy Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/Lambda.thy Sat Aug 21 16:20:10 2010 +0800
@@ -1,15 +1,18 @@
theory Lambda
-imports "../NewParser" Quotient_Option
+imports "../NewParser"
begin
atom_decl name
-declare [[STEPS = 9]]
+declare [[STEPS = 20]]
-nominal_datatype lam =
+nominal_datatype lam =
Var "name"
| App "lam" "lam"
| Lam x::"name" l::"lam" bind x in l
+
+thm eq_iff
+
thm lam.fv
thm lam.supp
lemmas supp_fn' = lam.fv[simplified lam.supp]
--- a/Nominal/Ex/SingleLet.thy Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy Sat Aug 21 16:20:10 2010 +0800
@@ -10,9 +10,9 @@
nominal_datatype trm =
Var "name"
| App "trm" "trm"
-| Lam x::"name" t::"trm" bind_set x in t
-| Let a::"assg" t::"trm" bind_set "bn a" in t
-| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2
+| Lam x::"name" t::"trm" bind x in t
+| Let a::"assg" t::"trm" bind (set) "bn a" in t
+| Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
| Bar x::"name" y::"name" t::"trm" bind y x in t x y
| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2
and assg =
@@ -24,6 +24,7 @@
+
ML {* Function.prove_termination *}
text {* can lift *}
@@ -32,14 +33,14 @@
thm trm_raw_assg_raw.inducts
thm trm_raw.exhaust
thm assg_raw.exhaust
-thm FV_defs
+thm fv_defs
thm perm_simps
thm perm_laws
thm trm_raw_assg_raw.size(9 - 16)
thm eq_iff
thm eq_iff_simps
thm bn_defs
-thm FV_eqvt
+thm fv_eqvt
thm bn_eqvt
thm size_eqvt
@@ -106,7 +107,6 @@
-
lemma supp_fv:
"supp t = fv_trm t"
"supp b = fv_bn b"
--- a/Nominal/Ex/TypeSchemes.thy Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy Sat Aug 21 16:20:10 2010 +0800
@@ -6,7 +6,7 @@
atom_decl name
-declare [[STEPS = 15]]
+declare [[STEPS = 20]]
nominal_datatype ty =
Var "name"
--- a/Nominal/NewParser.thy Thu Aug 19 18:24:36 2010 +0800
+++ b/Nominal/NewParser.thy Sat Aug 21 16:20:10 2010 +0800
@@ -20,48 +20,7 @@
*}
-
-ML {*
-(* nominal datatype parser *)
-local
- structure P = Parse;
- structure S = Scan
-
- fun triple1 ((x, y), z) = (x, y, z)
- fun triple2 (x, (y, z)) = (x, y, z)
- fun tuple ((x, y, z), u) = (x, y, z, u)
- fun tswap (((x, y), z), u) = (x, y, u, z)
-in
-
-val _ = Keyword.keyword "bind"
-val _ = Keyword.keyword "bind_set"
-val _ = Keyword.keyword "bind_res"
-
-val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
-
-val bind_mode = P.$$$ "bind" || P.$$$ "bind_set" || P.$$$ "bind_res"
-
-val bind_clauses =
- P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
-
-val cnstr_parser =
- P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
-
-(* datatype parser *)
-val dt_parser =
- (P.type_args -- P.binding -- P.opt_mixfix >> triple1) --
- (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
-
-(* binding function parser *)
-val bnfun_parser =
- S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
-
-(* main parser *)
-val main_parser =
- P.and_list1 dt_parser -- bnfun_parser >> triple2
-
-end
-*}
+ML {* print_depth 50 *}
ML {*
fun get_cnstrs dts =
@@ -744,16 +703,12 @@
fun prep_body env bn_str = index_lookup env bn_str
- fun prep_mode "bind" = Lst
- | prep_mode "bind_set" = Set
- | prep_mode "bind_res" = Res
-
fun prep_bclause env (mode, binders, bodies) =
let
val binders' = map (prep_binder env) binders
val bodies' = map (prep_body env) bodies
in
- BC (prep_mode mode, binders', bodies')
+ BC (mode, binders', bodies')
end
fun prep_bclauses (annos, bclause_strs) =
@@ -812,7 +767,51 @@
in
timeit (fn () => nominal_datatype2 dts bn_funs bn_eqs bclauses' lthy |> snd)
end
+*}
+ML {*
+(* nominal datatype parser *)
+local
+ structure P = Parse;
+ structure S = Scan
+
+ fun triple1 ((x, y), z) = (x, y, z)
+ fun triple2 (x, (y, z)) = (x, y, z)
+ fun tuple ((x, y, z), u) = (x, y, z, u)
+ fun tswap (((x, y), z), u) = (x, y, u, z)
+in
+
+val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "set"
+val _ = Keyword.keyword "res"
+val _ = Keyword.keyword "list"
+
+val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
+
+val bind_mode = P.$$$ "bind" |--
+ S.optional (Args.parens
+ (P.$$$ "list" >> K Lst || P.$$$ "set" >> K Set || P.$$$ "res" >> K Res)) Lst
+
+val bind_clauses =
+ P.enum "," (bind_mode -- S.repeat1 P.term -- (P.$$$ "in" |-- S.repeat1 P.name) >> triple1)
+
+val cnstr_parser =
+ P.binding -- S.repeat anno_typ -- bind_clauses -- P.opt_mixfix >> tswap
+
+(* datatype parser *)
+val dt_parser =
+ (P.type_args -- P.binding -- P.opt_mixfix >> triple1) --
+ (P.$$$ "=" |-- P.enum1 "|" cnstr_parser) >> tuple
+
+(* binding function parser *)
+val bnfun_parser =
+ S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
+
+(* main parser *)
+val main_parser =
+ P.and_list1 dt_parser -- bnfun_parser >> triple2
+
+end
(* Command Keyword *)