--- a/Nominal/Parser.thy Fri Feb 26 18:38:25 2010 +0100
+++ b/Nominal/Parser.thy Sat Feb 27 11:54:59 2010 +0100
@@ -137,8 +137,6 @@
end
*}
-ML {* Primrec.add_primrec *}
-
ML {*
fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
let
@@ -161,7 +159,7 @@
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 =>
+ 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
@@ -171,7 +169,7 @@
*}
ML {*
-fun nominal_datatype2 dts bn_funs bn_eqs lthy =
+fun nominal_datatype2 dts bn_funs bn_eqs binds lthy =
let
val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts
in
@@ -181,30 +179,70 @@
end
*}
-ML {*
-fun get_constrs2 lthy dts =
+
+ML {*
+(* parsing the datatypes and declaring *)
+(* constructors in the local theory *)
+fun prepare_dts dt_strs lthy =
let
val thy = ProofContext.theory_of lthy
+
+ fun mk_type full_tname tvrs =
+ Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)
- (* 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 prep_cnstr lthy full_tname tvs (cname, anno_tys, mx, _) =
+ let
+ val tys = map (Syntax.read_typ lthy o snd) anno_tys
+ val ty = mk_type full_tname tvs
+ in
+ ((cname, tys ---> ty, mx), (cname, tys, mx))
+ end
+
+ fun prep_dt lthy (tvs, tname, mx, cnstrs) =
+ let
+ val full_tname = Sign.full_name thy tname
+ val (cnstrs', cnstrs'') =
+ split_list (map (prep_cnstr lthy full_tname tvs) cnstrs)
+ in
+ (cnstrs', (tvs, tname, mx, cnstrs''))
+ end
- val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
+ val (cnstrs, dts) =
+ split_list (map (prep_dt lthy) dt_strs)
in
- flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) => (bn, tys ---> ty, mx)) constrs) dts')
+ lthy
+ |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+ |> pair dts
end
*}
-ML {*
-fun find_all _ [] _ = []
- | find_all eq ((y, z)::xs) x =
- if eq (x, y)
- then z::find_all eq xs x
- else find_all eq xs x
+ML {*
+(* parsing the function specification and *)
+(* declaring the functions in the local theory *)
+fun prepare_bn_funs bn_fun_strs bn_eq_strs lthy =
+let
+ fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
+
+ val ((bn_funs, bn_eqs), _) =
+ Specification.read_spec bn_fun_strs bn_eq_strs lthy
+
+ val bn_funs' = map prep_bn_fun bn_funs
+in
+ lthy
+ |> Local_Theory.theory (Sign.add_consts_i bn_funs')
+ |> pair (bn_funs', bn_eqs)
+end
*}
ML {*
+fun forth (_, _, _, x) = x
+
+fun find_all eq [] _ = []
+ | find_all eq ((key, value)::xs) key' =
+ let
+ val values = find_all eq xs key'
+ in if eq (key', key) then value :: values else values end;
+
fun mk_env xs =
let
fun mapp (_: int) [] = []
@@ -221,79 +259,55 @@
*}
ML {*
-fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+fun prepare_binds dt_strs lthy =
let
- fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
-
- (* adding the types for parsing datatypes *)
- val lthy_tmp1 = lthy
- |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
-
- (* parsing the datatypes *)
- val dts_prep =
- let
- fun prep_cnstr lthy (cname, anno_tys, mx, _) =
- (cname, map (Syntax.read_typ lthy o snd) anno_tys, mx)
-
- fun prep_dt lthy (tvs, tname, mx, cnstrs) =
- (tvs, tname, mx, map (prep_cnstr lthy) cnstrs)
- in
- map (prep_dt lthy_tmp1) dt_strs
- end
-
- (* adding constructors for parsing functions *)
- val lthy_tmp2 = lthy_tmp1
- |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep))
-
- (* parsing the function specification *)
- val (bn_fun_prep, bn_eq_prep) =
- let
- val ((bn_fun_aux, bn_eq_aux), _) = Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2
-
- fun prep_bn_fun ((bn, T), mx) = (bn, T, mx)
- fun prep_bn_eq (attr, t) = t
- in
- (map prep_bn_fun bn_fun_aux, map prep_bn_eq bn_eq_aux)
- end
-
- (* adding functions for parsing binders *)
- val lthy_tmp3 = lthy_tmp2
- |> Local_Theory.theory (Sign.add_consts_i bn_fun_prep)
-
- (* parsing the binding structure *)
- val binds =
- let
- fun prep_bn env str =
- (case Syntax.read_term lthy_tmp3 str of
+ fun prep_bn env str =
+ (case Syntax.read_term lthy str of
Free (x, _) => (env_lookup env x, NONE)
| Const (a, T) $ Free (x, _) => (env_lookup env x, SOME (Const (a, T)))
- | _ => error (str ^ " not allowed as binding specification."))
+ | x => error (str ^ " not allowed as binding specification."))
- fun prep_typ env (opt_name, _) =
+ fun prep_typ env (opt_name, _) =
(case opt_name of
NONE => []
| SOME x => find_all (op=) env x)
- fun prep_binds (_, anno_tys, _, bind_strs) =
- let
- val env = mk_env anno_tys
- val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs
- in
- map (prep_typ binds) anno_tys
- end
- in
- map ((map prep_binds) o #4) dt_strs
- end
-
- val _ = tracing (PolyML.makestring binds)
+ fun prep_binds (_, anno_tys, _, bind_strs) =
+ let
+ val env = mk_env anno_tys
+ val binds = map (fn (x, y) => (x, prep_bn env y)) bind_strs
+ in
+ map (prep_typ binds) anno_tys
+ end
in
- nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
+ map ((map prep_binds) o forth) dt_strs
end
*}
+ML {*
+fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
+let
+ val t = start_timing ()
+
+ fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx)
+
+ val ((dts, (bn_fun, bn_eq)), binds) =
+ lthy
+ |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs))
+ |> prepare_dts dt_strs
+ ||>> prepare_bn_funs bn_fun_strs bn_eq_strs
+ ||> prepare_binds dt_strs
+
+ val _ = tracing (PolyML.makestring binds)
+ val _ = tracing (#message (end_timing t))
+in
+ nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd
+end
+*}
+
+
(* Command Keyword *)
-
ML {*
let
val kind = OuterKeyword.thy_decl