diff -r 6a133abb7633 -r 212f3ab40cc2 Nominal/Parser.thy --- 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