Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/Nominal/Test.thy
changeset 1228 c179ad9d2446
parent 1223 160343d86a6f
child 1232 35bc8f7b66f8
equal deleted inserted replaced
1224:20f76fde8ef1 1228:c179ad9d2446 
    73 val fun_parser = 
    73 val fun_parser = 
    74   Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
 
    74   Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[])
 
    75 
    75 
    76 (* main parser *)
 
    76 (* main parser *)
 
    77 val main_parser =
 
    77 val main_parser =
 
    78   P.and_list1 dt_parser -- fun_parser
 
    78   (P.and_list1 dt_parser) -- fun_parser
 
    79 
    79 
    80 end
 
    80 end
 
    81 *}
 
    81 *}
 
    82 
    82 
    83 (* adds "_raw" to the end of constants and types *)
 
    83 (* adds "_raw" to the end of constants and types *)
 
   118 fun get_bn_fun_strs bn_funs =
 
   118 fun get_bn_fun_strs bn_funs =
 
   119   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 
   119   map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 
   120 *}
 
   120 *}
 
   121 
   121 
   122 ML {*
 
   122 ML {*
 
   123 fun nominal_dt_decl dt_names dts bn_funs bn_eqs lthy =
 
   123 fun raw_dts_decl dt_names dts lthy =
 
   124 let
 
   124 let
 
   125   val conf = Datatype.default_config
 
   125   val conf = Datatype.default_config
 
   126   
   126 
   127   val dt_names' = map add_raw dt_names
 
   127   val dt_names' = map add_raw dt_names
 
   128   val dts' = raw_dts dt_names dts
 
   128   val dts' = raw_dts dt_names dts
 
   129   val constr_strs = get_constr_strs dts
 
   129 in
 
       
   130   Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') lthy
 
       
   131 end 
       
   132 *}
 
       
   133 
       
   134 ML {*
 
       
   135 fun raw_bn_fun_decl dt_names cnstr_names bn_funs bn_eqs lthy =
 
       
   136 let
 
   130   val bn_fun_strs = get_bn_fun_strs bn_funs
 
   137   val bn_fun_strs = get_bn_fun_strs bn_funs
 
   131   
   138   
   132   val bn_funs' = map (fn (bn, opt_ty, mx) => 
   139   val bn_funs' = map (fn (bn, opt_ty, mx) => 
   133     (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs
 
   140     (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs
 
   134   val bn_eqs' = map (fn trm => 
   141   val bn_eqs' = map (fn trm => 
   135     (Attrib.empty_binding, raw_term (constr_strs @ bn_fun_strs) dt_names trm)) bn_eqs
 
   142     (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs
 
       
   143 in
 
       
   144   (*Primrec.add_primrec bn_funs' bn_eqs' lthy*)
 
       
   145   ((), lthy)
 
       
   146 end 
       
   147 *}
 
       
   148 
       
   149 ML {* 
       
   150 fun nominal_datatype2 dts bn_funs bn_eqs lthy =
 
       
   151 let
 
       
   152   val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
 
       
   153   val ctrs_names = get_constr_strs dts
 
   136 in
 
   154 in
 
   137   lthy
 
   155   lthy
 
   138   |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts'))
 
   156   |> raw_dts_decl dts_names dts 
   139   ||>> Primrec.add_primrec bn_funs' bn_eqs'
 
   157   ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs
 
   140 end 
   158 end
 
   141 *}
 
   159 *}
 
   142 
   160 
   143 local_setup {*
 
   161 ML {*
 
   144 let
 
   162 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
 
   145   val T0 = Type ("Test.foo", [])
 
   163 let
 
   146   val T1 = T0 --> @{typ "nat"}
 
   164   val lthy_tmp = lthy
 
   147 in
 
   165     |> (Local_Theory.theory
 
   148 nominal_dt_decl
 
   166         (Sign.add_types (map (fn ((tvs, tname, mx), _) =>
 
   149   ["foo"]
 
   167           (tname, length tvs, mx)) dt_strs)))
 
   150   [([], @{binding "foo"}, NoSyn, 
   168 
   151     [(@{binding "myzero"}, [], NoSyn),(@{binding "mysuc"}, [Type ("Test.foo", [])], NoSyn)])]
 
   169   fun prep_cnstr lthy (((cname, atys), mx), binders) =
 
   152   [(@{binding "Bar"}, SOME T1, NoSyn)]
 
   170     (cname, map (Syntax.read_typ lthy o snd) atys, mx)
 
   153   [HOLogic.mk_Trueprop (HOLogic.mk_eq 
       
   154         (Free ("Bar", T1) $ Const ("Test.foo_raw.myzero", T0), @{term "0::nat"})),
 
       
   155    HOLogic.mk_Trueprop (HOLogic.mk_eq 
       
   156         (Free ("Bar", T1) $ (Const ("Test.foo_raw.mysuc", T0 --> T0) $ Free ("n", T0)), @{term "0::nat"}))]
 
       
   157   #> snd
 
       
   158 end
 
       
   159 *}
 
       
   160 
       
   161 typ foo_raw
 
       
   162 thm foo_raw.induct
 
       
   163 term myzero_raw
 
       
   164 term mysuc_raw
 
       
   165 thm Bar_raw.simps
 
       
   166 
       
   167 (* printing stuff *)
 
       
   168 
       
   169 ML {*
 
       
   170 fun print_str_option NONE = "NONE"
 
       
   171   | print_str_option (SOME s) = (s:bstring)
 
       
   172 
       
   173 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
 
       
   174   | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
 
       
   175 
       
   176 fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
 
       
   177 
       
   178 fun print_constr lthy (((name, anno_tys), bds), syn) =
 
       
   179   (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
 
       
   180    ^ (commas (map print_bind bds)) ^ "  "
 
       
   181    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 
       
   182 
       
   183 fun print_single_dt lthy (((s2, s3), syn), constrs) =
 
       
   184    ["constructor declaration"]
 
       
   185  @ ["type arguments: "] @ s2 
       
   186  @ ["datatype name: ", Binding.name_of s3] 
       
   187  @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
 
       
   188  @ ["constructors: "] @ (map (print_constr lthy) constrs)
 
       
   189  |> separate "\n"
 
       
   190  |> implode
 
       
   191 
       
   192 fun print_single_fun_eq lthy (at, s) = 
       
   193   ["function equations: ", (Syntax.string_of_term lthy s)] 
       
   194   |> separate "\n"
 
       
   195   |> implode
 
       
   196 
       
   197 fun print_single_fun_fix lthy (b, _, _) = 
       
   198   ["functions: ", Binding.name_of b] 
       
   199   |> separate "\n"
 
       
   200   |> implode
 
       
   201 
       
   202 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
 
       
   203 
       
   204 fun print_dts (dts, (funs, feqs)) lthy =
 
       
   205 let
 
       
   206   val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
 
       
   207   val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
 
       
   208   val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
 
       
   209 in
 
       
   210   ()
 
       
   211 end
 
       
   212 *}
 
       
   213 
       
   214 ML {*
 
       
   215 fun transp_ty_arg (anno, ty) = ty
 
       
   216 
       
   217 fun transp_constr (((constr_name, ty_args), bind), mx) = 
       
   218   (constr_name, map transp_ty_arg ty_args, mx)
 
       
   219 
       
   220 fun transp_dt (((ty_args, ty_name), mx), constrs) = 
       
   221  (ty_args, ty_name, mx, map transp_constr constrs)
 
       
   222 *}
 
       
   223 
       
   224 ML {*
 
       
   225 fun dt_defn dts thy =
 
       
   226 let
 
       
   227   val names = map (fn (_, s, _, _) => Binding.name_of s) dts
 
       
   228   val thy' = Datatype.datatype_cmd names dts thy
 
       
   229 in
 
       
   230   thy'
 
       
   231 end
 
       
   232 *}
 
       
   233 
       
   234 ML {*
 
       
   235 fun fn_defn [] [] lthy = lthy
 
       
   236   | fn_defn funs feqs lthy =
 
       
   237       Function_Fun.add_fun Function_Common.default_config funs feqs false lthy
 
       
   238 
       
   239 fun fn_defn_cmd [] [] lthy = lthy
 
       
   240   | fn_defn_cmd funs feqs lthy =
 
       
   241       Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy
 
       
   242 *}
 
       
   243 
       
   244 ML {*
 
       
   245 fun parse_fun lthy (b, NONE, m) = (b, NONE, m)
 
       
   246   | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m)
 
       
   247 
       
   248 fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t);
 
       
   249 
       
   250 fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty);
 
       
   251 
       
   252 fun parse_constr lthy (((constr_name, ty_args), bind), mx) =
 
       
   253   (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx);
 
       
   254   
   171   
   255 fun parse_dt lthy (((ty_args, ty_name), mx), constrs) =
 
   172   fun prep_dt lthy ((tvs, tname, mx), cnstrs) = 
   256    (((ty_args, ty_name), mx), map (parse_constr lthy) constrs);
 
   173     (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
 
   257 *}
 
   174 
   258 
   175   fun prep_bn_fun lthy (bn, ty_str, mx) =
 
   259 ML {*
 
   176     (bn, Option.map (Syntax.read_typ lthy) ty_str, mx) 
   260 fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy =
 
   177 
   261 let
 
   178   fun prep_bn_eq lthy (attr, trm_str) = Syntax.read_term lthy trm_str
 
   262   val thy' = dt_defn (map transp_dt dt_strs) thy
 
   179 
   263   val lthy = Theory_Target.init NONE thy'
 
   180   val dts_prep = map (prep_dt lthy_tmp) dt_strs
 
   264   val lthy' = fn_defn_cmd fun_strs feq_strs lthy
 
   181   val bn_fun_prep = map (prep_bn_fun lthy_tmp) bn_fun_strs
 
   265   val funs = map (parse_fun lthy') fun_strs
 
   182   val bn_eq_prep = map (prep_bn_eq lthy_tmp) bn_eq_strs
 
   266   val feqs = map (parse_feq lthy') feq_strs
 
   183 in
 
   267   val dts = map (parse_dt lthy') dt_strs
 
   184   nominal_datatype2 dts_prep bn_fun_prep [] lthy |> snd
 
   268   val _ = print_dts (dts, (funs, feqs)) lthy'
 
       
   269 in
 
       
   270   Local_Theory.exit_global lthy'
 
       
   271 end
 
   185 end
 
   272 *}
 
   186 *}
 
   273 
   187 
   274 (* Command Keyword *)
 
   188 (* Command Keyword *)
 
   275 ML {*
 
   189 ML {*
 
   276 let
 
   190 let
 
   277    val kind = OuterKeyword.thy_decl
 
   191    val kind = OuterKeyword.thy_decl
 
   278 in
 
   192 in
 
   279    OuterSyntax.command "nominal_datatype" "test" kind 
   193    OuterSyntax.local_theory "nominal_datatype" "test" kind 
   280      (parser >> (Toplevel.theory o nominal_datatype2_cmd))
 
   194      (main_parser >> nominal_datatype2_cmd)
 
   281 end
 
   195 end
 
   282 *}
 
   196 *}
 
   283 
   197 
   284 text {* example 1 *}
 
   198 text {* example 1 *}
 
   285 nominal_datatype lam =
 
   199 nominal_datatype lam =
 
   290   BP "name" "lam"  ("_ ::= _" [100,100] 100)
 
   204   BP "name" "lam"  ("_ ::= _" [100,100] 100)
 
   291 binder
 
   205 binder
 
   292   bi::"bp \<Rightarrow> name set"
 
   206   bi::"bp \<Rightarrow> name set"
 
   293 where
 
   207 where
 
   294   "bi (BP x t) = {x}"
 
   208   "bi (BP x t) = {x}"
 
       
   209 
       
   210 typ lam_raw
 
       
   211 term VAR_raw
 
       
   212 term BP_raw
 
       
   213 
   295 print_theorems
 
   214 print_theorems
 
   296 
   215 
   297 text {* examples 2 *}
 
   216 text {* examples 2 *}
 
   298 nominal_datatype trm =
 
   217 nominal_datatype trm =
 
   299   Var "name"
 
   218   Var "name"
 
   339 
   258 
   340 
   259 
   341 end
 
   260 end
 
   342 
   261 
   343 
   262 
   344 (* probably can be done with a clever morphism trick *)
 
   263 (* printing stuff *)
 
   345 
   264 
       
   265 ML {*
 
       
   266 fun print_str_option NONE = "NONE"
 
       
   267   | print_str_option (SOME s) = (s:bstring)
 
       
   268 
       
   269 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
 
       
   270   | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
 
       
   271 
       
   272 fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
 
       
   273 
       
   274 fun print_constr lthy (((name, anno_tys), bds), syn) =
 
       
   275   (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
 
       
   276    ^ (commas (map print_bind bds)) ^ "  "
 
       
   277    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 
       
   278 
       
   279 fun print_single_dt lthy (((s2, s3), syn), constrs) =
 
       
   280    ["constructor declaration"]
 
       
   281  @ ["type arguments: "] @ s2 
       
   282  @ ["datatype name: ", Binding.name_of s3] 
       
   283  @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
 
       
   284  @ ["constructors: "] @ (map (print_constr lthy) constrs)
 
       
   285  |> separate "\n"
 
       
   286  |> implode
 
       
   287 
       
   288 fun print_single_fun_eq lthy (at, s) = 
       
   289   ["function equations: ", (Syntax.string_of_term lthy s)] 
       
   290   |> separate "\n"
 
       
   291   |> implode
 
       
   292 
       
   293 fun print_single_fun_fix lthy (b, _, _) = 
       
   294   ["functions: ", Binding.name_of b] 
       
   295   |> separate "\n"
 
       
   296   |> implode
 
       
   297 
       
   298 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
 
       
   299 
       
   300 fun print_dts (dts, (funs, feqs)) lthy =
 
       
   301 let
 
       
   302   val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
 
       
   303   val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
 
       
   304   val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
 
       
   305 in
 
       
   306   ()
 
       
   307 end
 
       
   308 *}
 
       
   309
nominal2