--- a/Nominal/Parser.thy Fri Feb 26 18:21:39 2010 +0100
+++ b/Nominal/Parser.thy Fri Feb 26 18:38:25 2010 +0100
@@ -31,6 +31,10 @@
(Trueprop equations)
*}
+ML {*
+
+*}
+
text {*****************************************************}
ML {*
(* nominal datatype parser *)
@@ -38,6 +42,7 @@
structure P = OuterParse
fun tuple ((x, y, z), u) = (x, y, z, u)
+ fun tswap (((x, y), z), u) = (x, y, u, z)
in
val _ = OuterKeyword.keyword "bind"
@@ -46,15 +51,15 @@
(* binding specification *)
(* maybe use and_list *)
val bind_parser =
- P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name))
+ P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name) >> swap)
val constr_parser =
P.binding -- Scan.repeat anno_typ
(* datatype parser *)
val dt_parser =
- (P.type_args -- P.binding -- P.opt_infix >> P.triple1) --
- (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple
+ (P.type_args -- P.binding -- P.opt_mixfix >> P.triple1) --
+ (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> tswap)) >> tuple
(* function equation parser *)
val fun_parser =
@@ -132,6 +137,8 @@
end
*}
+ML {* Primrec.add_primrec *}
+
ML {*
fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
let
@@ -151,8 +158,8 @@
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, opt_ty, mx) =>
- (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs
+ 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
@@ -175,8 +182,10 @@
*}
ML {*
-fun get_constrs2 thy dts =
+fun get_constrs2 lthy dts =
let
+ val thy = ProofContext.theory_of lthy
+
(* 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)
@@ -187,44 +196,104 @@
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 {*
+fun mk_env xs =
+ let
+ fun mapp (_: int) [] = []
+ | mapp i ((a, _) :: xs) =
+ case a of
+ NONE => mapp (i + 1) xs
+ | SOME x => (x, i) :: mapp (i + 1) xs
+ in mapp 0 xs end
+
+fun env_lookup xs x =
+ case AList.lookup (op =) xs x of
+ SOME x => x
+ | NONE => error ("cannot find " ^ x ^ " in the binding specification.")
+*}
+
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
+ val lthy_tmp1 = lthy
|> Local_Theory.theory (Sign.add_types (map prep_typ 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
-
+ 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_tmp
- |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep))
+ val lthy_tmp2 = lthy_tmp1
+ |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 lthy dts_prep))
- val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2)
+ (* 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
- fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx)
-
- fun prep_bn_eq (attr, t) = t
+ (* adding functions for parsing binders *)
+ val lthy_tmp3 = lthy_tmp2
+ |> Local_Theory.theory (Sign.add_consts_i bn_fun_prep)
- val bn_fun_prep = map prep_bn_fun bn_fun_aux
- val bn_eq_prep = map prep_bn_eq bn_eq_aux
+ (* parsing the binding structure *)
+ val binds =
+ let
+ fun prep_bn env str =
+ (case Syntax.read_term lthy_tmp3 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."))
+
+ 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)
in
- nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
+ nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
end
*}
(* Command Keyword *)
+
+
ML {*
let
val kind = OuterKeyword.thy_decl