nominal2: comparison Nominal/Parser.thy

equal deleted inserted replaced

-:6a133abb7633
+:212f3ab40cc2
 lthy
 |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')
 end
 *}
-ML {* Primrec.add_primrec *}
 ML {*
 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy =
 let
 val thy = ProofContext.theory_of lthy
 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 =>
+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
 *}
 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
 lthy
 |> raw_dts_decl dts_names dts
 ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs
 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
-(* makes a full named type out of a binding with tvars applied to it *)
+fun mk_type full_tname tvrs =
-fun mk_type thy bind tvrs =
+Type (full_tname, map (fn a => TVar ((a, 0), [])) 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, _) =
-val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts
+let
-in
+val tys = map (Syntax.read_typ lthy o snd) anno_tys
-flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) =>  (bn, tys ---> ty, mx)) constrs) dts')
+val ty = mk_type full_tname tvs
-end
+in
-*}
+((cname, tys ---> ty, mx), (cname, tys, mx))
+end
-ML {*
-fun find_all _ [] _ = []
+fun prep_dt lthy (tvs, tname, mx, cnstrs) =
-| find_all eq ((y, z)::xs) x =
+let
-if eq (x, y)
+val full_tname = Sign.full_name thy tname
-then z::find_all eq xs x
+val (cnstrs', cnstrs'') =
-else find_all eq xs x
+split_list (map (prep_cnstr lthy full_tname tvs) cnstrs)
-*}
+in
+(cnstrs', (tvs, tname, mx, cnstrs''))
-ML {*
+end
+val (cnstrs, dts) =
+split_list (map (prep_dt lthy) dt_strs)
+in
+lthy
+|> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))
+|> pair dts
+end
+*}
+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) [] = []
 | mapp i ((a, _) :: xs) =
 case a 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 =
+fun prepare_binds dt_strs lthy =
 let
-fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx);
+fun prep_bn env str =
+(case Syntax.read_term lthy str of
-(* 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
 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, _) =
 (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
+map ((map prep_binds) o forth) dt_strs
 end
+*}
-val _ = tracing (PolyML.makestring binds)
-in
+ML {*
-nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd
+fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy =
-end
+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
 in

changeset 1284	212f3ab40cc2
parent 1283	6a133abb7633
child 1285	e3ac56d3b7af