nominal2: comparison Quot/Nominal/Test.thy

equal deleted inserted replaced

-:8338292adbb6
+:11b8798dea5d
 *}
 (* adds "_raw" to the end of constants and types *)
 ML {*
 fun add_raw s = s ^ "_raw"
+fun add_raws ss = map add_raw ss
 fun raw_bind bn = Binding.suffix_name "_raw" bn
-fun raw_str [] s = s
+fun replace_str ss s =
-| raw_str (s'::ss) s =
+case (AList.lookup (op=) ss s) of
-if (Long_Name.base_name s) = s'
+SOME s' => s'
-then add_raw s
+| NONE => s
-else raw_str ss s
+fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts)
-fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts)
+| replace_typ ty_ss T = T
-| raw_typ ty_strs T = T
+fun raw_dts ty_ss dts =
-fun raw_aterm trm_strs (Const (a, T)) = Const (raw_str trm_strs a, T)
+let
-| raw_aterm trm_strs (Free (a, T)) = Free (raw_str trm_strs a, T)
+val ty_ss' = ty_ss ~~ (add_raws ty_ss)
-| raw_aterm trm_strs trm = trm
-fun raw_term trm_strs ty_strs trm =
-trm |> Term.map_aterms (raw_aterm trm_strs) |> map_types (raw_typ ty_strs)
-fun raw_dts ty_strs dts =
-let
 fun raw_dts_aux1 (bind, tys, mx) =
-(raw_bind bind, map (raw_typ ty_strs) tys, mx)
+(raw_bind bind, map (replace_typ ty_ss') tys, mx)
 fun raw_dts_aux2 (ty_args, bind, mx, constrs) =
 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs)
 in
 map raw_dts_aux2 dts
 end
+fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T)
+| replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T)
+| replace_aterm trm_ss trm = trm
+fun replace_term trm_ss ty_ss trm =
+trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss)
+*}
+ML {*
 fun get_constrs dts =
-flat (map (fn (_, _, _, constrs) => map (fn (bn, tys, mx) => (bn, tys, mx)) constrs) dts)
+flat (map (fn (_, _, _, constrs) => constrs) dts)
+fun get_typed_constrs dts =
+flat (map (fn (_, bn, _, constrs) =>
+(map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts)
 fun get_constr_strs dts =
 map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts)
-fun get_constrs2 dts =
-flat (map (fn (tvrs, tname, _, constrs) =>
-map (fn (bn, tys, mx) => (bn, tys ---> Type ("Test." ^ Binding.name_of tname, map (fn s => TVar ((s,0),[])) tvrs), mx)) constrs) dts)
 fun get_bn_fun_strs bn_funs =
 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs
 *}
 ML {*
 fun raw_dts_decl dt_names dts lthy =
 let
+val thy = ProofContext.theory_of lthy
 val conf = Datatype.default_config
-val dt_names' = map add_raw dt_names
+val dt_names' = add_raws dt_names
-val dts' = raw_dts dt_names dts
+val dt_full_names = map (Sign.full_bname thy) dt_names
-in
+val dts' = raw_dts dt_full_names dts
-Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') lthy
+in
+lthy
+|> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
 end
 *}
 ML {*
-fun raw_bn_fun_decl dt_names cnstr_names bn_funs bn_eqs lthy =
+fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
+val thy = ProofContext.theory_of lthy
+val dt_names' = add_raws dt_names
+val dt_full_names = map (Sign.full_bname thy) dt_names
+val dt_full_names' = map (Sign.full_bname thy) dt_names'
+val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts)
+val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y)))
+(get_typed_constrs dts)
 val bn_fun_strs = get_bn_fun_strs bn_funs
+val bn_fun_strs' = add_raws bn_fun_strs
 val bn_funs' = map (fn (bn, opt_ty, mx) =>
-(raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs
+(raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs
 val bn_eqs' = map (fn trm =>
-(Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs
+(Attrib.empty_binding,
-in
+(replace_term ((ctrs_names ~~ ctrs_names') @ (bn_fun_strs ~~ bn_fun_strs')) (dt_full_names ~~ dt_full_names') trm))) bn_eqs
-Primrec.add_primrec bn_funs' bn_eqs' lthy
+in
+if null bn_eqs
+then (([], []), lthy)
+else Primrec.add_primrec bn_funs' bn_eqs' lthy
 end
 *}
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs lthy =
 let
 val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
-val ctrs_names = get_constr_strs dts
 in
 lthy
 |> raw_dts_decl dts_names dts
-||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs
+||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 end
 *}
+ML {*
+(* makes a full named type out of a binding with tvars applied to it *)
+fun mk_type thy bind tvrs =
+Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs)
+fun get_constrs2 thy dts =
+let
+val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
+in
+flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
+end
+*}
 ML {*
 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy =
 let
+val thy = ProofContext.theory_of lthy
+fun prep_typ ((tvs, tname, mx), _) = (tname, length tvs, mx);
+(* adding the types for parsing datatypes *)
 val lthy_tmp = lthy
-|> Local_Theory.theory
+|> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
-(Sign.add_types (map (fn ((tvs, tname, mx), _) =>
-(tname, length tvs, mx)) dt_strs))
 fun prep_cnstr lthy (((cname, atys), mx), binders) =
 (cname, map (Syntax.read_typ lthy o snd) atys, mx)
 fun prep_dt lthy ((tvs, tname, mx), cnstrs) =
 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
+(* parsing the datatypes *)
 val dts_prep = map (prep_dt lthy_tmp) dt_strs
+(* adding constructors for parsing functions *)
 val lthy_tmp2 = lthy_tmp
-|> Local_Theory.theory (Sign.add_consts_i (get_constrs2 dts_prep))
+|> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep))
+val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
 fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx)
 fun prep_bn_eq (attr, t) = t
-val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
 val bn_fun_prep = map prep_bn_fun bn_fun_aux
 val bn_eq_prep = map prep_bn_eq bn_eq_aux
-val _ = tracing (cat_lines (map (Syntax.string_of_term lthy_tmp2) bn_eq_prep))
 in
 nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
 end
 *}
 (main_parser >> nominal_datatype2_cmd)
 end
 *}
 text {* example 1 *}
 nominal_datatype lam =
 VAR "name"
 | APP "lam" "lam"
 | LET bp::"bp" t::"lam"   bind "bi bp" in t ("Let _ in _" [100,100] 100)
 and bp =
 where
 "bi (BP x t) = {x}"
 typ lam_raw
 term VAR_raw
-term BP_raw
+term Test.BP_raw
+thm bi_raw.simps
 print_theorems
 text {* examples 2 *}
 nominal_datatype trm =
 | Lam x::"name" t::"trm"        bind x in t
 | Let p::"pat" "trm" t::"trm"   bind "f p" in t
 and pat =
 PN
 | PS "name"
-| PD "name \<times> name"
+| PD "name" "name"
 binder
 f::"pat \<Rightarrow> name set"
 where
 "f PN = {}"
 | "f (PS x) = {x}"
-| "f (PD (x,y)) = {x,y}"
+| "f (PD x y) = {x,y}"
-nominal_datatype trm2 =
+thm f_raw.simps
-Var2 "name"
-| App2 "trm2" "trm2"
+nominal_datatype trm0 =
-| Lam2 x::"name" t::"trm2"          bind x in t
+Var0 "name"
-| Let2 p::"pat2" "trm2" t::"trm2"   bind "f2 p" in t
+| App0 "trm0" "trm0"
-and pat2 =
+| Lam0 x::"name" t::"trm0"          bind x in t
-PN2
+| Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
-| PS2 "name"
+and pat0 =
-| PD2 "pat2 \<times> pat2"
+PN0
-binder
+| PS0 "name"
-f2::"pat2 \<Rightarrow> name set"
+| PD0 "pat0" "pat0"
+binder
+f0::"pat0 \<Rightarrow> name set"
 where
-"f2 PN2 = {}"
+"f0 PN0 = {}"
-| "f2 (PS2 x) = {x}"
+| "f0 (PS0 x) = {x}"
-| "f2 (PD2 (p1, p2)) = (f2 p1) \<union> (f2 p2)"
+| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+thm f0_raw.simps
 text {* example type schemes *}
 datatype ty =
 Var "name"
 | Fun "ty" "ty"
 nominal_datatype tyS =
 All xs::"name list" ty::"ty" bind xs in ty
+(* example 1 from Terms.thy *)
-end
+nominal_datatype trm1 =
+Vr1 "name"
-(* printing stuff *)
+| Ap1 "trm1" "trm1"
+| Lm1 x::"name" t::"trm1"      bind x in t
-ML {*
+| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
-fun print_str_option NONE = "NONE"
+and bp1 =
-| print_str_option (SOME s) = (s:bstring)
+BUnit1
+| BV1 "name"
-fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty
+| BP1 "bp1" "bp1"
-| print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty
+binder
+bv1
-fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2
+where
+"bv1 (BUnit1) = {}"
-fun print_constr lthy (((name, anno_tys), bds), syn) =
+| "bv1 (BV1 x) = {atom x}"
-(Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ "   "
+| "bv1 (BP1 bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
-^ (commas (map print_bind bds)) ^ "  "
-^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
+thm bv1_raw.simps
-fun print_single_dt lthy (((s2, s3), syn), constrs) =
+(* example 2 from Terms.thy *)
-["constructor declaration"]
-@ ["type arguments: "] @ s2
+nominal_datatype trm2 =
-@ ["datatype name: ", Binding.name_of s3]
+Vr2 "name"
-@ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)]
+| Ap2 "trm2" "trm2"
-@ ["constructors: "] @ (map (print_constr lthy) constrs)
+| Lm2 x::"name" t::"trm2"       bind x in t
-|> separate "\n"
+| Lt2 r::"rassign" t::"trm2"    bind "bv2 r" in t
-|> implode
+and rassign =
+As "name" "trm2"
-fun print_single_fun_eq lthy (at, s) =
+binder
-["function equations: ", (Syntax.string_of_term lthy s)]
+bv2
-|> separate "\n"
+where
-|> implode
+"bv2 (As x t) = {atom x}"
-fun print_single_fun_fix lthy (b, _, _) =
+(* example 3 from Terms.thy *)
-["functions: ", Binding.name_of b]
-|> separate "\n"
+nominal_datatype trm3 =
-|> implode
+Vr3 "name"
+| Ap3 "trm3" "trm3"
-fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3
+| Lm3 x::"name" t::"trm3"        bind x in t
+| Lt3 r::"rassigns3" t::"trm3"   bind "bv3 r" in t
-fun print_dts (dts, (funs, feqs)) lthy =
+and rassigns3 =
-let
+ANil
-val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts)));
+| ACons "name" "trm3" "rassigns3"
-val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs)));
+binder
-val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs)));
+bv3
-in
+where
-()
+"bv3 ANil = {}"
-end
+| "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)"
-*}
+(* example 4 from Terms.thy *)
+nominal_datatype trm4 =
+Vr4 "name"
+| Ap4 "trm4" "trm4 list"
+| Lm4 x::"name" t::"trm4"  bind x in t
+(* example 5 from Terms.thy *)
+nominal_datatype trm5 =
+Vr5 "name"
+| Ap5 "trm5" "trm5"
+| Lt5 l::"lts" t::"trm5"  bind "bv5 l" in t
+and lts =
+Lnil
+| Lcons "name" "trm5" "lts"
+binder
+bv5
+where
+"bv5 Lnil = {}"
+| "bv5 (Lcons n t ltl) = {atom n} \<union> (bv5 ltl)"
+(* example 6 from Terms.thy *)
+nominal_datatype trm6 =
+Vr6 "name"
+| Lm6 x::"name" t::"trm6"         bind x in t
+| Lt6 left::"trm6" right::"trm6"  bind "bv6 left" in right
+binder
+bv6
+where
+"bv6 (Vr6 n) = {}"
+| "bv6 (Lm6 n t) = {atom n} \<union> bv6 t"
+| "bv6 (Lt6 l r) = bv6 l \<union> bv6 r"
+(* example 7 from Terms.thy *)
+nominal_datatype trm7 =
+Vr7 "name"
+| Lm7 l::"name" r::"trm7"   bind l in r
+| Lt7 l::"trm7" r::"trm7"   bind "bv7 l" in r
+binder
+bv7
+where
+"bv7 (Vr7 n) = {atom n}"
+| "bv7 (Lm7 n t) = bv7 t - {atom n}"
+| "bv7 (Lt7 l r) = bv7 l \<union> bv7 r"
+(* example 8 from Terms.thy *)
+nominal_datatype foo8 =
+Foo0 "name"
+| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in foo
+and bar8 =
+Bar0 "name"
+| Bar1 "name" s::"name" b::"bar8" bind s in b
+binder
+bv8
+where
+"bv8 (Bar0 x) = {}"
+| "bv8 (Bar1 v x b) = {atom v}"
+(* example 9 from Terms.thy *)
+nominal_datatype lam9 =
+Var9 "name"
+| Lam9 n::"name" l::"lam9" bind n in l
+and bla9 =
+Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s
+binder
+bv9
+where
+"bv9 (Var9 x) = {}"
+| "bv9 (Lam9 x b) = {atom x}"
+end

changeset 1251	11b8798dea5d
parent 1232	35bc8f7b66f8