--- a/Nominal/Parser.thy Mon Mar 01 21:50:24 2010 +0100
+++ b/Nominal/Parser.thy Mon Mar 01 21:50:40 2010 +0100
@@ -4,7 +4,6 @@
atom_decl name
-
section{* Interface for nominal_datatype *}
text {*
@@ -88,10 +87,9 @@
fun raw_dts ty_ss dts =
let
- val ty_ss' = ty_ss ~~ (add_raws ty_ss)
fun raw_dts_aux1 (bind, tys, mx) =
- (raw_bind bind, map (replace_typ ty_ss') 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)
@@ -108,26 +106,24 @@
*}
ML {*
-fun get_constrs dts =
- flat (map (fn (_, _, _, constrs) => constrs) dts)
+fun get_cnstrs dts =
+ map (fn (_, _, _, constrs) => constrs) dts
-fun get_typed_constrs dts =
+fun get_typed_cnstrs 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_cnstr_strs dts =
+ map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs 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 =
+fun rawify_dts dt_names dts dts_env =
let
- val thy = ProofContext.theory_of lthy
- val dt_full_names = map (Sign.full_bname thy) dt_names
- val raw_dts = raw_dts dt_full_names dts
+ val raw_dts = raw_dts dts_env dts
val raw_dt_names = add_raws dt_names
in
(raw_dt_names, raw_dts)
@@ -135,52 +131,65 @@
*}
ML {*
-fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
+fun rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs =
+let
+ val bn_funs' = map (fn (bn, ty, mx) =>
+ (raw_bind bn, replace_typ dts_env ty, mx)) bn_funs
+
+ val bn_eqs' = map (fn (attr, trm) =>
+ (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs
+in
+ (bn_funs', bn_eqs')
+end
+*}
+
+ML {*
+fun add_primrec_wrapper funs eqs lthy =
+ if null funs then (([], []), lthy)
+ else
+ let
+ val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs
+ val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs
+ in
+ Primrec.add_primrec funs' eqs' lthy
+ end
+*}
+
+
+ML {*
+fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
let
val thy = ProofContext.theory_of lthy
+ val thy_name = Context.theory_name thy
+
+ val conf = Datatype.default_config
- 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 dt_env = dt_full_names ~~ dt_full_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 ctrs_env = ctrs_names ~~ ctrs_names'
+ val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts
+ val dt_full_names = map (Long_Name.qualify thy_name) dt_names
+ val dt_full_names' = add_raws dt_full_names
+ val dts_env = dt_full_names ~~ dt_full_names'
+
+ val cnstrs = get_cnstr_strs dts
+ val cnstrs_ty = get_typed_cnstrs dts
+ val cnstrs_full_names = map (Long_Name.qualify thy_name) cnstrs
+ val cnstrs_full_names' = map (fn (x, y) => Long_Name.qualify thy_name
+ (Long_Name.qualify (add_raw x) (add_raw y))) cnstrs_ty
+ val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names'
val bn_fun_strs = get_bn_fun_strs bn_funs
val bn_fun_strs' = add_raws bn_fun_strs
val bn_fun_env = bn_fun_strs ~~ bn_fun_strs'
-
- val bn_funs' = map (fn (bn, ty, mx) =>
- (raw_bind bn, SOME (replace_typ dt_env ty), mx)) bn_funs
-
- val bn_eqs' = map (fn (_, trm) =>
- (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs
-in
- if null bn_eqs
- then (([], []), lthy)
- else Primrec.add_primrec bn_funs' bn_eqs' lthy
-end
-*}
+
+ val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env
-ML {*
-fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
-let
- val conf = Datatype.default_config
- val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
-
- val (raw_dt_names, raw_dts) = raw_dts_decl dts_names dts lthy
-
+ val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs
in
- lthy
- |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
- ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
+ lthy
+ |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts)
+ ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs
end
*}
-
ML {*
(* parsing the datatypes and declaring *)
(* constructors in the local theory *)
@@ -236,14 +245,12 @@
*}
ML {*
-fun forth (_, _, _, x) = x
-
-fun find_all eq xs k' =
- maps (fn (k, v) => if eq (k, k') then [v] else []) xs
+fun find_all eq xs (k',i) =
+ maps (fn (k, (v1, v2)) => if eq (k, k') then [(v1, v2, i)] else []) xs
*}
ML {*
-(* associates every SOME with the index in the list *)
+(* associates every SOME with the index in the list; drops NONEs *)
fun mk_env xs =
let
fun mapp (_: int) [] = []
@@ -261,37 +268,35 @@
| NONE => error ("cannot find " ^ x ^ " in the binding specification.");
*}
-
-
ML {*
fun prepare_binds dt_strs lthy =
let
fun extract_annos_binds dt_strs =
- map ((map (fn (_, antys, _, bns) => (map fst antys, bns))) o forth) dt_strs
+ map (map (fn (_, antys, _, bns) => (map fst antys, bns))) dt_strs
fun prep_bn env bn_str =
case (Syntax.read_term lthy bn_str) of
- Free (x, _) => (env_lookup env x, NONE)
- | Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
+ Free (x, _) => (NONE, env_lookup env x)
+ | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), env_lookup env x)
| _ => error (bn_str ^ " not allowed as binding specification.");
- fun prep_typ env opt_name =
+ fun prep_typ env (i, opt_name) =
case opt_name of
NONE => []
- | SOME x => find_all (op=) env x;
+ | SOME x => find_all (op=) env (x,i);
(* annos - list of annotation for each type (either NONE or SOME fo a type *)
fun prep_binds (annos, bind_strs) =
let
- val env = mk_env annos (* for ever label the index *)
+ val env = mk_env annos (* for every label the index *)
val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs
in
- map (prep_typ binds) annos
+ map_index (prep_typ binds) annos
end
in
- map (map prep_binds) (extract_annos_binds dt_strs)
+ map (map prep_binds) (extract_annos_binds (get_cnstrs dt_strs))
end
*}
--- a/Nominal/Test.thy Mon Mar 01 21:50:24 2010 +0100
+++ b/Nominal/Test.thy Mon Mar 01 21:50:40 2010 +0100
@@ -40,7 +40,7 @@
where
"f PN = {}"
| "f (PS x) = {x}"
-| "f (PD x y) = {x,y}"
+| "f (PD x y) = {x, y}"
thm f_raw.simps
@@ -78,7 +78,7 @@
nominal_datatype trm1 =
Vr1 "name"
| Ap1 "trm1" "trm1"
-| Lm1 x::"name" t::"trm1" bind x in t
+| Lm1 x::"name" t::"trm1" bind x in t
| Lt1 p::"bp1" "trm1" t::"trm1" bind "bv1 p" in t
and bp1 =
BUnit1
@@ -203,13 +203,13 @@
atom_decl coname
nominal_datatype phd =
- Ax name coname
-| Cut n::name t1::phd c::coname t2::phd bind n in t1, bind c in t2
-| AndR c1::coname t1::phd c2::coname t2::phd coname bind c1 in t1, bind c2 in t2
-| AndL1 n::name t::phd name bind n in t
-| AndL2 n::name t::phd name bind n in t
-| ImpL c::coname t1::phd n::name t2::phd name bind c in t1, bind n in t2
-| ImpR c::coname n::name t::phd coname bind n in 1, bind c in t
+ Ax "name" "coname"
+| Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2
+| AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2
+| AndL1 n::"name" t::"phd" "name" bind n in t
+| AndL2 n::"name" t::"phd" "name" bind n in t
+| ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2
+| ImpR c::"coname" n::"name" t::"phd" "coname" bind n in 1, bind c in t
(* example form Leroy 96 about modules; OTT *)