1 theory Test

     2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp"

     3 begin

     4 

     5 atom_decl name

     6 

     7 

     8 (* test for how to add datatypes *)

     9 setup {*

    10 Datatype.datatype_cmd

    11   ["foo"]

    12   [([], @{binding "foo"}, NoSyn, 

    13     [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)])

    14   ]

    15 *}

    16 

    17 thm foo.recs

    18 thm foo.induct

    19 

    20 

    21 ML{*

    22 fun filtered_input str = 

    23   filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 

    24 

    25 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input

    26 *}

    27 

    28 (* type plus possible annotation *)

    29 ML {* 

    30 val anno_typ =

    31   (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ

    32 *}

    33 

    34 ML {*

    35 parse (Scan.repeat anno_typ) (filtered_input "x::string bool")

    36 *}

    37 

    38 ML {* OuterParse.enum "," ; OuterParse.and_list1 *}

    39 

    40 (* binding specification *)

    41 ML {* 

    42 datatype bind = B of string * string | BS of string * string

    43  

    44 val _ = OuterKeyword.keyword "bind" 

    45 val _ = OuterKeyword.keyword "bindset" 

    46 

    47 val bind_parse_aux =

    48     (OuterParse.$$$ "bind" >> (K B)) 

    49  || (OuterParse.$$$ "bindset" >> (K BS))

    50 

    51 (* should use and_list *)

    52 val bind_parser = 

    53   OuterParse.enum ","

    54    ((bind_parse_aux -- OuterParse.term) --

    55     (OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2)))

    56 *}

    57 

    58 (* datatype parser *)

    59 ML {*

    60 val dt_parser =

    61   OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix -- 

    62     (OuterParse.$$$ "=" |-- OuterParse.enum1 "|" 

    63        (OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix))

    64 *}

    65 

    66 (* function equation parser *)

    67 ML {*

    68 val fun_parser = 

    69   Scan.optional 

    70     ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[])

    71 *}

    72 

    73 (* main parser *)

    74 ML {*

    75 val parser =

    76   OuterParse.and_list1 dt_parser -- fun_parser

    77 *}

    78 

    79 (* printing stuff *)

    80 ML {*

    81 fun print_str_option NONE = "NONE"

    82   | print_str_option (SOME s) = (s:bstring)

    83 *}

    84 

    85 ML {* 

    86 fun print_anno_typ (NONE, ty) = ty

    87   | print_anno_typ (SOME x, ty) = x ^ ":" ^ ty     

    88 *}

    89 

    90 ML {*

    91 fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2

    92   | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2

    93 *}

    94 

    95 ML {*

    96 fun print_constr (((name, anno_tys), bds), syn) =

    97   (Binding.name_of name ^ " of " ^ (commas (map print_anno_typ anno_tys)) ^ "   " 

    98    ^ (commas (map print_bind bds)) ^ "  "  

    99    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))

   100 *}

   101 

   102 ML {*

   103 fun single_dt (((s2, s3), syn), constrs) =

   104    ["constructor declaration"]

   105  @ ["type arguments: "] @ s2 

   106  @ ["datatype name: ", Binding.name_of s3] 

   107  @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]

   108  @ ["constructors: "] @ (map print_constr constrs)

   109  |> separate "\n"

   110  |> implode

   111 *}

   112 

   113 ML {* fun single_fun_eq (at, s) = 

   114   ["function equations: ", s] 

   115   |> separate "\n"

   116   |> implode

   117 *}

   118 

   119 ML {* fun single_fun_fix (b, _, _) = 

   120   ["functions: ", Binding.name_of b] 

   121   |> separate "\n"

   122   |> implode

   123 *}

   124 

   125 ML {*

   126 fun print_dts (dts, (funs, feqs)) = 

   127 let

   128    val _ = warning (implode (separate "\n" (map single_dt dts)))

   129    val _ = warning (implode (separate "\n" (map single_fun_fix funs)))

   130    val _ = warning (implode (separate "\n" (map single_fun_eq feqs)))

   131 in

   132   ()

   133 end   

   134 *}

   135 

   136 ML {*

   137 parser;

   138 Datatype.datatype_cmd; 

   139 *}

   140 

   141 ML {*

   142 fun transp_ty_arg (anno, ty) = ty

   143 

   144 fun transp_constr (((constr_name, ty_args), bind), mx) = 

   145   (constr_name, map transp_ty_arg ty_args, mx)

   146 

   147 fun transp_dt (((ty_args, ty_name), mx), constrs) = 

   148  (ty_args, ty_name, mx, map transp_constr constrs)

   149 *}

   150 

   151 ML {*

   152 fun dt_defn dts thy =

   153 let

   154   val names = map (fn (_, s, _, _) => Binding.name_of s) dts

   155   val thy' = Datatype.datatype_cmd names dts thy

   156 in

   157   thy'

   158 end

   159 *}

   160 

   161 ML {*

   162 fun fn_defn [] [] thy = thy

   163   | fn_defn funs feqs thy =

   164 let

   165   val lthy = Theory_Target.init NONE thy

   166   val ctxt = Function_Fun.add_fun_cmd  Function_Common.default_config funs feqs false lthy

   167   val thy' = ProofContext.theory_of ctxt

   168 in

   169   thy'

   170 end

   171 *}

   172 

   173 

   174 ML {*

   175 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy =

   176 let

   177   val thy1 = dt_defn (map transp_dt dts) thy

   178   val thy2 = fn_defn funs feqs thy1

   179   val _ = print_dts (dts, (funs, feqs)) 

   180 in

   181   thy2

   182 end *}

   183 

   184 (* Command Keyword *)

   185 ML {*

   186 let

   187    val kind = OuterKeyword.thy_decl

   188 in

   189    OuterSyntax.command "nominal_datatype" "test" kind 

   190      (parser >> (Toplevel.theory o nominal_datatype2_cmd))

   191 end

   192 *}

   193 

   194 text {* example 1 *}

   195 nominal_datatype lam =

   196   VAR "name"

   197 | APP "lam" "lam"

   198 | LET bp::"bp" t::"lam"   bind "bi bp" in t ("Let _ in _" [100,100] 100)

   199 and bp = 

   200   BP "name" "lam"  ("_ ::= _" [100,100] 100)

   201 binder

   202   bi::"bp \<Rightarrow> name set"

   203 where

   204   "bi (BP x t) = {x}"

   205 

   206 

   207 text {* examples 2 *}

   208 nominal_datatype trm =

   209   Var "string"

   210 | App "trm" "trm"

   211 | Lam x::"name" t::"trm"        bindset x in t 

   212 | Let p::"pat" "trm" t::"trm"   bind "f p" in t

   213 and pat =

   214   PN

   215 | PS "name"

   216 | PD "name \<times> name"

   217 binder

   218   f::"pat \<Rightarrow> name set"

   219 where 

   220   "f PN = {}"

   221 | "f (PS x) = {x}"

   222 | "f (PD (x,y)) = {x,y}"

   223 

   224 nominal_datatype trm2 =

   225   Var2 "string"

   226 | App2 "trm2" "trm2"

   227 | Lam2 x::"name" t::"trm2"          bindset x in t 

   228 | Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t

   229 and pat2 =

   230   PN2

   231 | PS2 "name"

   232 | PD2 "pat2 \<times> pat2"

   233 binder

   234   f2::"pat2 \<Rightarrow> name set"

   235 where 

   236   "f2 PN2 = {}"

   237 | "f2 (PS2 x) = {x}"

   238 | "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"

   239 

   240 text {* example type schemes *}

   241 datatype ty = 

   242   Var "name" 

   243 | Fun "ty" "ty"

   244 

   245 nominal_datatype tyS = 

   246   All xs::"name list" ty::"ty" bindset xs in ty

   247 

   248 

   249 

   250 

   251 end