# HG changeset patch # User Christian Urban # Date 1282378810 -28800 # Node ID 621ebd8b13c410de42d147a6878a258fe4daeefc # Parent f2d4dae2a10b9d36ce3b8b788b662624a35a6811 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 diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/CoreHaskell.thy --- 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 = diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/Lambda.thy --- 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] diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/SingleLet.thy --- 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" diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/Ex/TypeSchemes.thy --- 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" diff -r f2d4dae2a10b -r 621ebd8b13c4 Nominal/NewParser.thy --- 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 *)