--- a/Quot/Nominal/Test.thy Fri Feb 19 10:17:35 2010 +0100
+++ b/Quot/Nominal/Test.thy Fri Feb 19 10:26:38 2010 +0100
@@ -5,145 +5,171 @@
atom_decl name
-(* test for how to add datatypes *)
+(* tests *)
+ML {*
+Datatype.datatype_cmd;
+Datatype.add_datatype Datatype.default_config;
+
+Primrec.add_primrec_cmd;
+Primrec.add_primrec;
+Primrec.add_primrec_simple;
+*}
+
+section {* test for setting up a primrec on the ML-level *}
+
+datatype simple = Foo
+
+local_setup {*
+Primrec.add_primrec [(@{binding "Bar"}, SOME @{typ "simple \<Rightarrow> nat"}, NoSyn)]
+ [(Attrib.empty_binding, HOLogic.mk_Trueprop @{term "Bar Foo = Suc 0"})] #> snd
+*}
+thm Bar.simps
+
+lemma "Bar Foo = XXX"
+apply(simp)
+oops
+
+section {* test for setting up a datatype on the ML-level *}
setup {*
-Datatype.datatype_cmd
+Datatype.add_datatype Datatype.default_config
["foo"]
[([], @{binding "foo"}, NoSyn,
- [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)])
- ]
+ [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, [Type ("Test.foo", [])], NoSyn)])
+ ] #> snd
+*}
+
+ML {*
+ PolyML.makestring (#descr (Datatype.the_info @{theory} "Test.foo"))
*}
thm foo.recs
thm foo.induct
+(* adds "_raw" to the end of constants and types *)
+ML {*
+fun raw_str [] s = s
+ | raw_str (s'::ss) s = (if s = s' then s ^ "_str" else raw_str ss s)
-ML{*
-fun filtered_input str =
- filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
+val raw_strs = map raw_str
+
+fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts)
+ | raw_typ ty_strs T = T
-fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
+fun raw_term trm_strs ty_strs (Const (a, T)) = Const (raw_str trm_strs a, raw_typ ty_strs T)
+ | raw_term trm_strs ty_strs (Abs (a, T, t)) = Abs (a, T, raw_term trm_strs ty_strs t)
+ | raw_term trm_strs ty_strs (t $ u) = (raw_term trm_strs ty_strs t) $ (raw_term trm_strs ty_strs u)
+
+fun raw_binding bn = Binding.suffix_name "_raw" bn
*}
-(* type plus possible annotation *)
-ML {*
-val anno_typ =
- (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ
+section{* Interface for nominal_datatype *}
+
+text {*
+
+Nominal-Datatype-part:
+
+1st Arg: string list
+ ^^^^^^^^^^^
+ strings of the types to be defined
+
+2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ type(s) to be defined constructors list
+ (ty args, name, syn) (name, typs, syn)
+
+Binder-Function-part:
+
+3rd Arg: (binding * typ option * mixfix) list
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ binding function(s)
+ to be defined
+ (name, type, syn)
+
+4th Arg: (attrib * term) list
+ ^^^^^^^^^^^^^^^^^^^
+ the equations of the binding functions
+ (Trueprop equations)
+
*}
+ML {* Datatype.add_datatype *}
+
ML {*
-parse (Scan.repeat anno_typ) (filtered_input "x::string bool")
+fun raw_definitions dt_names dts bn_funs bn_eqs lthy =
+let
+ val conf = Datatype.default_config
+ val bn_funs' = map (fn (bn, ty) => (raw_binding bn, ty, NoSyn)) bn_funs
+ val bn_eqs' = map (pair Attrib.empty_binding) bn_eqs
+in
+ lthy
+ |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts))
+ ||>> Primrec.add_primrec bn_funs' bn_eqs'
+end
*}
-ML {* OuterParse.enum "," ; OuterParse.and_list1 *}
+ML {* @{binding "zero"} *}
+
+local_setup {*
+raw_definitions
+ ["foo'"]
+ [([], @{binding "foo'"}, NoSyn,
+ [(@{binding "zero'"}, [], NoSyn),(@{binding "suc'"}, [Type ("Test.foo'", [])], NoSyn)])]
+ [(@{binding "Bar'"}, SOME @{typ "simple \<Rightarrow> nat"})]
+ [HOLogic.mk_Trueprop @{term "Bar'_raw Foo = Suc 0"}]
+ #> snd
+*}
+
+typ foo'
+thm Bar'.simps
+
+text {*****************************************************}
+ML {*
+(* nominal datatype parser *)
+local
+ structure P = OuterParse
+in
+
+val _ = OuterKeyword.keyword "bind"
+val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ
(* binding specification *)
-ML {*
-datatype bind = B of string * string | BS of string * string
-
-val _ = OuterKeyword.keyword "bind"
-val _ = OuterKeyword.keyword "bindset"
-
-val bind_parse_aux =
- (OuterParse.$$$ "bind" >> (K B))
- || (OuterParse.$$$ "bindset" >> (K BS))
-
(* should use and_list *)
val bind_parser =
- OuterParse.enum ","
- ((bind_parse_aux -- OuterParse.term) --
- (OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2)))
-*}
+ P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
(* datatype parser *)
-ML {*
val dt_parser =
- OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix --
- (OuterParse.$$$ "=" |-- OuterParse.enum1 "|"
- (OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix))
-*}
+ P.type_args -- P.binding -- P.opt_infix --
+ (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix))
(* function equation parser *)
-ML {*
val fun_parser =
- Scan.optional
- ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[])
+ Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
+
+(* main parser *)
+val parser =
+ P.and_list1 dt_parser -- fun_parser
+
+end
*}
-(* main parser *)
-ML {*
-val parser =
- OuterParse.and_list1 dt_parser -- fun_parser
-*}
(* printing stuff *)
ML {*
fun print_str_option NONE = "NONE"
| print_str_option (SOME s) = (s:bstring)
-*}
-ML {*
fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
| print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
-*}
-ML {*
-fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2
- | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2
-*}
+fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
-ML {*
fun print_constr lthy (((name, anno_tys), bds), syn) =
(Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " "
^ (commas (map print_bind bds)) ^ " "
^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
-*}
-(* TODO: replace with the proper thing *)
-ML {*
-fun is_atom ty = ty = "Test.name"
-*}
-
-ML {*
-fun fv_bds s bds set =
- case bds of
- [] => set
- | B (s1, s2) :: tl =>
- if s2 = s then
- fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
- else fv_bds s tl set
- | BS (s1, s2) :: tl =>
- (* TODO: This is just a copy *)
- if s2 = s then
- fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
- else fv_bds s tl set
-*}
-
-(* TODO: After variant_frees, check that the new names correspond to the ones given by user
- so that 'bind' is matched with variables correctly *)
-ML {*
-fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) =
-let
- fun prepare_name (NONE, ty) = ("", ty)
- | prepare_name (SOME n, ty) = (n, ty);
- val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys));
- val var_strs = map (Syntax.string_of_term lthy) vars;
- fun fv_var (t as Free (s, (ty as Type (tyS, _)))) =
- if is_atom tyS then HOLogic.mk_set ty [t] else
- if (Long_Name.base_name tyS) mem dt_names then
- fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
- HOLogic.mk_set @{typ name} []
- val fv_eq =
- if null vars then HOLogic.mk_set @{typ name} []
- else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
- val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq)
-in
- prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str
-end
-*}
-
-ML {*
-fun single_dt lthy (((s2, s3), syn), constrs) =
+fun print_single_dt lthy (((s2, s3), syn), constrs) =
["constructor declaration"]
@ ["type arguments: "] @ s2
@ ["datatype name: ", Binding.name_of s3]
@@ -151,57 +177,30 @@
@ ["constructors: "] @ (map (print_constr lthy) constrs)
|> separate "\n"
|> implode
-*}
-ML {*
-fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
- map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs
- |> separate "\n"
- |> implode
-*}
-
-ML {* fun single_fun_eq lthy (at, s) =
+fun print_single_fun_eq lthy (at, s) =
["function equations: ", (Syntax.string_of_term lthy s)]
|> separate "\n"
|> implode
-*}
-ML {* fun single_fun_fix (b, _, _) =
+fun print_single_fun_fix lthy (b, _, _) =
["functions: ", Binding.name_of b]
|> separate "\n"
|> implode
-*}
-ML {*
fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
-*}
-ML {*
fun print_dts (dts, (funs, feqs)) lthy =
let
- val _ = warning (implode (separate "\n" (map (single_dt lthy) dts)));
- val _ = warning (implode (separate "\n" (map single_fun_fix funs)));
- val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs)));
+ val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
+ val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
+ val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
in
()
end
*}
ML {*
-fun fv_dts (dts, (funs, feqs)) lthy =
-let
- val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts)));
-in
- lthy
-end
-*}
-
-ML {*
-parser;
-Datatype.datatype_cmd;
-*}
-
-ML {*
fun transp_ty_arg (anno, ty) = ty
fun transp_constr (((constr_name, ty_args), bind), mx) =
@@ -225,35 +224,39 @@
fun fn_defn [] [] lthy = lthy
| fn_defn funs feqs lthy =
Function_Fun.add_fun Function_Common.default_config funs feqs false lthy
-*}
-ML {*
fun fn_defn_cmd [] [] lthy = lthy
| fn_defn_cmd funs feqs lthy =
Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
*}
ML {*
-fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =
+fun parse_fun lthy (b, NONE, m) = (b, NONE, m)
+ | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m)
+
+fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t);
+
+fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty);
+
+fun parse_constr lthy (((constr_name, ty_args), bind), mx) =
+ (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx);
+
+fun parse_dt lthy (((ty_args, ty_name), mx), constrs) =
+ (((ty_args, ty_name), mx), map (parse_constr lthy) constrs);
+*}
+
+ML {*
+fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy =
let
- val thy' = dt_defn (map transp_dt dts) thy
+ val thy' = dt_defn (map transp_dt dt_strs) thy
val lthy = Theory_Target.init NONE thy'
- val lthy' = fn_defn_cmd funs feqs lthy
- fun parse_fun (b, NONE, m) = (b, NONE, m)
- | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m);
- val funs = map parse_fun funs
- fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t);
- val feqs = map parse_feq feqs
- fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty);
- fun parse_constr (((constr_name, ty_args), bind), mx) =
- (((constr_name, map parse_anno_ty ty_args), bind), mx);
- fun parse_dt (((ty_args, ty_name), mx), constrs) =
- (((ty_args, ty_name), mx), map parse_constr constrs);
- val dts = map parse_dt dts
- val _ = print_dts (dts, (funs, feqs)) lthy
+ val lthy' = fn_defn_cmd fun_strs feq_strs lthy
+ val funs = map (parse_fun lthy') fun_strs
+ val feqs = map (parse_feq lthy') feq_strs
+ val dts = map (parse_dt lthy') dt_strs
+ val _ = print_dts (dts, (funs, feqs)) lthy'
in
- fv_dts (dts, (funs, feqs)) lthy
-|> Local_Theory.exit_global
+ Local_Theory.exit_global lthy'
end
*}
@@ -284,7 +287,7 @@
nominal_datatype trm =
Var "name"
| App "trm" "trm"
-| Lam x::"name" t::"trm" bindset x in t
+| Lam x::"name" t::"trm" bind x in t
| Let p::"pat" "trm" t::"trm" bind "f p" in t
and pat =
PN
@@ -300,7 +303,7 @@
nominal_datatype trm2 =
Var2 "name"
| App2 "trm2" "trm2"
-| Lam2 x::"name" t::"trm2" bindset x in t
+| Lam2 x::"name" t::"trm2" bind x in t
| Let2 p::"pat2" "trm2" t::"trm2" bind "f2 p" in t
and pat2 =
PN2
@@ -319,7 +322,7 @@
| Fun "ty" "ty"
nominal_datatype tyS =
- All xs::"name list" ty::"ty" bindset xs in ty
+ All xs::"name list" ty::"ty" bind xs in ty