--- a/Nominal/Parser.thy Mon Mar 01 16:55:41 2010 +0100
+++ b/Nominal/Parser.thy Mon Mar 01 19:23:08 2010 +0100
@@ -4,7 +4,6 @@
atom_decl name
-
section{* Interface for nominal_datatype *}
text {*
@@ -108,14 +107,14 @@
ML {*
fun get_cnstrs dts =
- flat (map (fn (_, _, _, constrs) => constrs) dts)
+ map (fn (_, _, _, constrs) => 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_cnstr_strs dts =
- map (fn (bn, _, _) => Binding.name_of bn) (get_cnstrs 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
@@ -246,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) [] = []
@@ -271,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
*}
@@ -317,7 +312,7 @@
||>> prepare_bn_funs bn_fun_strs bn_eq_strs
||> prepare_binds dt_strs
- (*val _ = tracing (PolyML.makestring binds)*)
+ val _ = tracing (PolyML.makestring binds)
in
nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
end