1.1 --- a/etc/isar-keywords-HOL-Nominal.el Mon Oct 09 20:12:45 2006 +0200
1.2 +++ b/etc/isar-keywords-HOL-Nominal.el Tue Oct 10 09:17:17 2006 +0200
1.3 @@ -43,15 +43,16 @@
1.4 "classes"
1.5 "classrel"
1.6 "clear_undos"
1.7 + "code_abstype"
1.8 "code_class"
1.9 "code_const"
1.10 "code_constname"
1.11 + "code_constsubst"
1.12 "code_gen"
1.13 "code_instance"
1.14 "code_instname"
1.15 "code_library"
1.16 "code_module"
1.17 - "code_simtype"
1.18 "code_type"
1.19 "code_typename"
1.20 "coinductive"
1.21 @@ -206,6 +207,7 @@
1.22 "types_code"
1.23 "ultimately"
1.24 "undo"
1.25 + "undo_end"
1.26 "undos_proof"
1.27 "unfolding"
1.28 "update_thy"
1.29 @@ -283,6 +285,7 @@
1.30 "quit"
1.31 "redo"
1.32 "undo"
1.33 + "undo_end"
1.34 "undos_proof"))
1.35
1.36 (defconst isar-keywords-diag
1.37 @@ -373,9 +376,11 @@
1.38 "class"
1.39 "classes"
1.40 "classrel"
1.41 + "code_abstype"
1.42 "code_class"
1.43 "code_const"
1.44 "code_constname"
1.45 + "code_constsubst"
1.46 "code_instance"
1.47 "code_instname"
1.48 "code_library"
1.49 @@ -439,7 +444,6 @@
1.50
1.51 (defconst isar-keywords-theory-goal
1.52 '("ax_specification"
1.53 - "code_simtype"
1.54 "corollary"
1.55 "function"
1.56 "instance"
2.1 --- a/etc/isar-keywords-ZF.el Mon Oct 09 20:12:45 2006 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Tue Oct 10 09:17:17 2006 +0200
2.3 @@ -41,15 +41,16 @@
2.4 "classrel"
2.5 "clear_undos"
2.6 "codatatype"
2.7 + "code_abstype"
2.8 "code_class"
2.9 "code_const"
2.10 "code_constname"
2.11 + "code_constsubst"
2.12 "code_gen"
2.13 "code_instance"
2.14 "code_instname"
2.15 "code_library"
2.16 "code_module"
2.17 - "code_simtype"
2.18 "code_type"
2.19 "code_typename"
2.20 "coinductive"
2.21 @@ -193,6 +194,7 @@
2.22 "types_code"
2.23 "ultimately"
2.24 "undo"
2.25 + "undo_end"
2.26 "undos_proof"
2.27 "unfolding"
2.28 "update_thy"
2.29 @@ -269,6 +271,7 @@
2.30 "quit"
2.31 "redo"
2.32 "undo"
2.33 + "undo_end"
2.34 "undos_proof"))
2.35
2.36 (defconst isar-keywords-diag
2.37 @@ -358,9 +361,11 @@
2.38 "classes"
2.39 "classrel"
2.40 "codatatype"
2.41 + "code_abstype"
2.42 "code_class"
2.43 "code_const"
2.44 "code_constname"
2.45 + "code_constsubst"
2.46 "code_instance"
2.47 "code_instname"
2.48 "code_library"
2.49 @@ -417,8 +422,7 @@
2.50 "inductive_cases"))
2.51
2.52 (defconst isar-keywords-theory-goal
2.53 - '("code_simtype"
2.54 - "corollary"
2.55 + '("corollary"
2.56 "instance"
2.57 "interpretation"
2.58 "lemma"
3.1 --- a/etc/isar-keywords.el Mon Oct 09 20:12:45 2006 +0200
3.2 +++ b/etc/isar-keywords.el Tue Oct 10 09:17:17 2006 +0200
3.3 @@ -43,15 +43,16 @@
3.4 "classes"
3.5 "classrel"
3.6 "clear_undos"
3.7 + "code_abstype"
3.8 "code_class"
3.9 "code_const"
3.10 "code_constname"
3.11 + "code_constsubst"
3.12 "code_gen"
3.13 "code_instance"
3.14 "code_instname"
3.15 "code_library"
3.16 "code_module"
3.17 - "code_simtype"
3.18 "code_type"
3.19 "code_typename"
3.20 "coinductive"
3.21 @@ -210,6 +211,7 @@
3.22 "types_code"
3.23 "ultimately"
3.24 "undo"
3.25 + "undo_end"
3.26 "undos_proof"
3.27 "unfolding"
3.28 "update_thy"
3.29 @@ -304,6 +306,7 @@
3.30 "quit"
3.31 "redo"
3.32 "undo"
3.33 + "undo_end"
3.34 "undos_proof"))
3.35
3.36 (defconst isar-keywords-diag
3.37 @@ -394,9 +397,11 @@
3.38 "class"
3.39 "classes"
3.40 "classrel"
3.41 + "code_abstype"
3.42 "code_class"
3.43 "code_const"
3.44 "code_constname"
3.45 + "code_constsubst"
3.46 "code_instance"
3.47 "code_instname"
3.48 "code_library"
3.49 @@ -462,7 +467,6 @@
3.50
3.51 (defconst isar-keywords-theory-goal
3.52 '("ax_specification"
3.53 - "code_simtype"
3.54 "corollary"
3.55 "cpodef"
3.56 "function"
4.1 --- a/src/Pure/Tools/codegen_package.ML Mon Oct 09 20:12:45 2006 +0200
4.2 +++ b/src/Pure/Tools/codegen_package.ML Tue Oct 10 09:17:17 2006 +0200
4.3 @@ -35,34 +35,53 @@
4.4
4.5 (* theory data *)
4.6
4.7 +structure Code = CodeDataFun
4.8 +(struct
4.9 + val name = "Pure/code";
4.10 + type T = CodegenThingol.code;
4.11 + val empty = CodegenThingol.empty_code;
4.12 + fun merge _ = CodegenThingol.merge_code;
4.13 + fun purge _ NONE _ = CodegenThingol.empty_code
4.14 + | purge NONE _ _ = CodegenThingol.empty_code
4.15 + | purge (SOME thy) (SOME cs) code =
4.16 + let
4.17 + val cs_exisiting =
4.18 + map_filter (CodegenNames.const_rev thy) (Graph.keys code);
4.19 + in
4.20 + Graph.del_nodes
4.21 + ((Graph.all_succs code
4.22 + o map (CodegenNames.const thy)
4.23 + o filter (member CodegenConsts.eq_const cs_exisiting)
4.24 + ) cs)
4.25 + code
4.26 + end;
4.27 +end);
4.28 +
4.29 type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
4.30 -> CodegenFuncgr.T
4.31 -> bool * string list option
4.32 -> (string * typ) * term list -> CodegenThingol.transact -> iterm * CodegenThingol.transact;
4.33
4.34 type appgens = (int * (appgen * stamp)) Symtab.table;
4.35 +val merge_appgens : appgens * appgens -> appgens =
4.36 + Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
4.37 + bounds1 = bounds2 andalso stamp1 = stamp2);
4.38
4.39 -fun merge_appgens (x : appgens * appgens) =
4.40 - Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
4.41 - bounds1 = bounds2 andalso stamp1 = stamp2) x;
4.42 -
4.43 -structure Code = CodeDataFun
4.44 -(struct
4.45 - val name = "Pure/code";
4.46 - type T = CodegenThingol.code;
4.47 - val empty = CodegenThingol.empty_code;
4.48 - fun merge _ = CodegenThingol.merge_code;
4.49 - fun purge _ _ = CodegenThingol.empty_code;
4.50 -end);
4.51 +structure Consttab = CodegenConsts.Consttab;
4.52 +type abstypes = typ Symtab.table * CodegenConsts.const Consttab.table;
4.53 +fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
4.54 + (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
4.55 + Consttab.merge CodegenConsts.eq_const (consts1, consts2));
4.56
4.57 structure CodegenPackageData = TheoryDataFun
4.58 (struct
4.59 val name = "Pure/codegen_package";
4.60 - type T = appgens;
4.61 - val empty = Symtab.empty;
4.62 + type T = appgens * abstypes;
4.63 + val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
4.64 val copy = I;
4.65 val extend = I;
4.66 - fun merge _ = merge_appgens;
4.67 + fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
4.68 + (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
4.69 fun print _ _ = ();
4.70 end);
4.71
4.72 @@ -71,13 +90,17 @@
4.73
4.74 (* extraction kernel *)
4.75
4.76 -fun check_strict has_seri x (false, _) =
4.77 +fun check_strict (false, _) has_seri x =
4.78 false
4.79 - | check_strict has_seri x (_, SOME targets) =
4.80 + | check_strict (_, SOME targets) has_seri x =
4.81 not (has_seri targets x)
4.82 - | check_strict has_seri x (true, _) =
4.83 + | check_strict (true, _) has_seri x =
4.84 true;
4.85
4.86 +fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o CodegenPackageData.get) thy) tyco
4.87 + of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
4.88 + | NONE => NONE;
4.89 +
4.90 fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
4.91 let
4.92 val (v, cs) = (ClassPackage.the_consts_sign thy) class;
4.93 @@ -115,7 +138,7 @@
4.94 trns
4.95 |> fail ("No such datatype: " ^ quote tyco)
4.96 val tyco' = CodegenNames.tyco thy tyco;
4.97 - val strict = check_strict (CodegenSerializer.tyco_has_serialization thy) tyco' strct;
4.98 + val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
4.99 in
4.100 trns
4.101 |> tracing (fn _ => "generating type constructor " ^ quote tyco)
4.102 @@ -139,10 +162,15 @@
4.103 ||>> exprgen_type thy algbr funcgr strct t2
4.104 |-> (fn (t1', t2') => pair (t1' `-> t2'))
4.105 | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
4.106 - trns
4.107 - |> ensure_def_tyco thy algbr funcgr strct tyco
4.108 - ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
4.109 - |-> (fn (tyco, tys) => pair (tyco `%% tys));
4.110 + case get_abstype thy (tyco, tys)
4.111 + of SOME ty =>
4.112 + trns
4.113 + |> exprgen_type thy algbr funcgr strct ty
4.114 + | NONE =>
4.115 + trns
4.116 + |> ensure_def_tyco thy algbr funcgr strct tyco
4.117 + ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
4.118 + |-> (fn (tyco, tys) => pair (tyco `%% tys));
4.119
4.120 exception CONSTRAIN of (string * typ) * typ;
4.121
4.122 @@ -239,7 +267,8 @@
4.123 |> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
4.124 |-> (fn _ => succeed CodegenThingol.Bot);
4.125 fun defgen_fun trns =
4.126 - case CodegenFuncgr.get_funcs funcgr (c, tys)
4.127 + case CodegenFuncgr.get_funcs funcgr
4.128 + (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))
4.129 of eq_thms as eq_thm :: _ =>
4.130 let
4.131 val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
4.132 @@ -271,7 +300,7 @@
4.133 else if CodegenNames.has_nsp CodegenNames.nsp_dtco c'
4.134 then defgen_datatypecons
4.135 else error ("Illegal shallow name space for constant: " ^ quote c');
4.136 - val strict = check_strict (CodegenSerializer.const_has_serialization thy) c' strct;
4.137 + val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
4.138 in
4.139 trns
4.140 |> tracing (fn _ => "generating constant "
4.141 @@ -318,7 +347,7 @@
4.142 |-> (fn (((c, ty), iss), ts) =>
4.143 pair (IConst (c, (iss, ty)) `$$ ts))
4.144 and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
4.145 - case Symtab.lookup (CodegenPackageData.get thy) c
4.146 + case Symtab.lookup (fst (CodegenPackageData.get thy)) c
4.147 of SOME (i, (appgen, _)) =>
4.148 if length ts < i then
4.149 let
4.150 @@ -415,8 +444,96 @@
4.151
4.152 fun add_appconst (c, appgen) thy =
4.153 let
4.154 - val i = (length o fst o strip_type o Sign.the_const_type thy) c
4.155 - in CodegenPackageData.map (Symtab.update (c, (i, (appgen, stamp ())))) thy end;
4.156 + val i = (length o fst o strip_type o Sign.the_const_type thy) c;
4.157 + val _ = Code.change thy (K CodegenThingol.empty_code);
4.158 + in
4.159 + (CodegenPackageData.map o apfst)
4.160 + (Symtab.update (c, (i, (appgen, stamp ())))) thy
4.161 + end;
4.162 +
4.163 +
4.164 +
4.165 +(** abstype and constsubst interface **)
4.166 +
4.167 +fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
4.168 + let
4.169 + val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
4.170 + val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
4.171 + val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
4.172 + val Type (abstyco, tys) = abstyp handle BIND => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
4.173 + val typarms = map (fst o dest_TFree) tys handle MATCH => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
4.174 + fun mk_index v =
4.175 + let
4.176 + val k = find_index (fn w => v = w) typarms;
4.177 + in if k = ~1
4.178 + then error ("free type variable: " ^ quote v)
4.179 + else TFree (string_of_int k, [])
4.180 + end;
4.181 + val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
4.182 + fun apply_typpat (Type (tyco, tys)) =
4.183 + let
4.184 + val tys' = map apply_typpat tys;
4.185 + in if tyco = abstyco then
4.186 + (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
4.187 + else
4.188 + Type (tyco, tys')
4.189 + end
4.190 + | apply_typpat ty = ty;
4.191 + val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
4.192 + fun add_consts (c1, c2) =
4.193 + let
4.194 + val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
4.195 + then ()
4.196 + else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
4.197 + val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
4.198 + val ty_map = CodegenFuncgr.get_func_typs funcgr;
4.199 + val ty1 = (apply_typpat o the o AList.lookup CodegenConsts.eq_const ty_map) c1;
4.200 + val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
4.201 + val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
4.202 + error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
4.203 + ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
4.204 + ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
4.205 + in Consttab.update (c1, c2) end;
4.206 + val _ = Code.change thy (K CodegenThingol.empty_code);
4.207 + in
4.208 + thy
4.209 + |> (CodegenPackageData.map o apsnd) (fn (abstypes, abscs) =>
4.210 + (abstypes
4.211 + |> Symtab.update (abstyco, typpat),
4.212 + abscs
4.213 + |> fold add_consts absconsts)
4.214 + )
4.215 + end;
4.216 +
4.217 +fun gen_constsubst prep_const raw_constsubsts thy =
4.218 + let
4.219 + val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
4.220 + val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
4.221 + fun add_consts (c1, c2) =
4.222 + let
4.223 + val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
4.224 + then ()
4.225 + else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
4.226 + val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
4.227 + val ty_map = CodegenFuncgr.get_func_typs funcgr;
4.228 + val ty1 = (the o AList.lookup CodegenConsts.eq_const ty_map) c1;
4.229 + val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
4.230 + val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
4.231 + error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
4.232 + ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
4.233 + ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
4.234 + in Consttab.update (c1, c2) end;
4.235 + val _ = Code.change thy (K CodegenThingol.empty_code);
4.236 + in
4.237 + thy
4.238 + |> (CodegenPackageData.map o apsnd o apsnd) (fold add_consts constsubsts)
4.239 + end;
4.240 +
4.241 +val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
4.242 +val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
4.243 +
4.244 +val constsubst = gen_constsubst CodegenConsts.norm;
4.245 +val constsubst_e = gen_constsubst CodegenConsts.read_const;
4.246
4.247
4.248
4.249 @@ -424,13 +541,16 @@
4.250
4.251 fun generate thy (cs, rhss) targets init gen it =
4.252 let
4.253 - val funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
4.254 - val qnaming = NameSpace.qualified_names NameSpace.default_naming
4.255 + val raw_funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
4.256 + val cs' = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))
4.257 + (CodegenFuncgr.Constgraph.keys raw_funcgr);
4.258 + val funcgr = CodegenFuncgr.mk_funcgr thy cs' [];
4.259 + val qnaming = NameSpace.qualified_names NameSpace.default_naming;
4.260 val algebr = ClassPackage.operational_algebra thy;
4.261 val consttab = Consts.empty
4.262 |> fold (fn (c, ty) => Consts.declare qnaming
4.263 ((CodegenNames.const thy c, ty), true))
4.264 - (CodegenFuncgr.get_func_typs funcgr)
4.265 + (CodegenFuncgr.get_func_typs funcgr);
4.266 val algbr = (algebr, consttab);
4.267 in
4.268 Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr
4.269 @@ -504,30 +624,11 @@
4.270 (map (serialize' cs code) seris'; ())
4.271 end;
4.272
4.273 -fun reader_tyco thy rhss target dep =
4.274 - generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_type);
4.275 -
4.276 -fun reader_const thy rhss target dep =
4.277 - generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_term');
4.278 -
4.279 -fun zip_list (x::xs) f g =
4.280 - f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
4.281 - #-> (fn xys => pair ((x, y) :: xys)));
4.282 -
4.283 -fun parse_multi_syntax parse_thing parse_syntax =
4.284 - P.and_list1 parse_thing
4.285 - #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
4.286 - (fn target => zip_list things (parse_syntax target)
4.287 - (P.$$$ "and")) --| P.$$$ ")"))
4.288 -
4.289 +val (codeK, code_abstypeK, code_constsubstK) =
4.290 + ("code_gen", "code_abstype", "code_constsubst");
4.291
4.292 in
4.293
4.294 -val (codeK,
4.295 - syntax_classK, syntax_instK, syntax_tycoK, syntax_constK) =
4.296 - ("code_gen",
4.297 - "code_class", "code_instance", "code_type", "code_const");
4.298 -
4.299 val codeP =
4.300 OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
4.301 Scan.repeat P.term
4.302 @@ -537,42 +638,20 @@
4.303 >> (fn (raw_cs, seris) => Toplevel.keep (code raw_cs seris o Toplevel.theory_of))
4.304 );
4.305
4.306 -val syntax_classP =
4.307 - OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl (
4.308 - parse_multi_syntax P.xname
4.309 - (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
4.310 - (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
4.311 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
4.312 - fold (fn (raw_class, syn) => CodegenSerializer.add_syntax_class target raw_class syn) syns)
4.313 +val code_abstypeP =
4.314 + OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
4.315 + (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
4.316 + (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
4.317 + >> (Toplevel.theory o uncurry abstyp_e)
4.318 );
4.319
4.320 -val syntax_instP =
4.321 - OuterSyntax.command syntax_instK "define code syntax for instance" K.thy_decl (
4.322 - parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
4.323 - (fn _ => fn _ => P.name #->
4.324 - (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
4.325 - >> (Toplevel.theory oo fold) (fn (target, syns) =>
4.326 - fold (fn (raw_inst, ()) => CodegenSerializer.add_syntax_inst target raw_inst) syns)
4.327 +val code_constsubstP =
4.328 + OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl (
4.329 + Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
4.330 + >> (Toplevel.theory o constsubst_e)
4.331 );
4.332
4.333 -val syntax_tycoP =
4.334 - OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
4.335 - Scan.repeat1 (
4.336 - parse_multi_syntax P.xname (CodegenSerializer.parse_syntax_tyco reader_tyco)
4.337 - )
4.338 - >> (Toplevel.theory o (fold o fold) (fold snd o snd))
4.339 - );
4.340 -
4.341 -val syntax_constP =
4.342 - OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
4.343 - Scan.repeat1 (
4.344 - parse_multi_syntax P.term (CodegenSerializer.parse_syntax_const reader_const)
4.345 - )
4.346 - >> (Toplevel.theory o (fold o fold) (fold snd o snd))
4.347 - );
4.348 -
4.349 -val _ = OuterSyntax.add_parsers [codeP,
4.350 - syntax_classP, syntax_instP, syntax_tycoP, syntax_constP];
4.351 +val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_constsubstP];
4.352
4.353 end; (* local *)
4.354
5.1 --- a/src/Pure/Tools/codegen_serializer.ML Mon Oct 09 20:12:45 2006 +0200
5.2 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Oct 10 09:17:17 2006 +0200
5.3 @@ -9,35 +9,7 @@
5.4 signature CODEGEN_SERIALIZER =
5.5 sig
5.6 include BASIC_CODEGEN_THINGOL;
5.7 - val get_serializer: theory -> string * Args.T list
5.8 - -> string list option -> CodegenThingol.code -> unit;
5.9 - val eval_verbose: bool ref;
5.10 - val eval_term: theory ->
5.11 - (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
5.12 - -> 'a;
5.13 - val const_has_serialization: theory -> string list -> string -> bool;
5.14 - val tyco_has_serialization: theory -> string list -> string -> bool;
5.15 - val add_syntax_class:
5.16 - string -> string -> string * (string * string) list -> theory -> theory;
5.17 - val add_syntax_inst: string -> (string * string) -> theory -> theory;
5.18 - val parse_syntax_tyco: (theory
5.19 - -> CodegenConsts.const list * (string * typ) list
5.20 - -> string
5.21 - -> CodegenNames.tyco
5.22 - -> typ list -> CodegenThingol.itype list)
5.23 - -> Symtab.key
5.24 - -> xstring
5.25 - -> OuterParse.token list
5.26 - -> (theory -> theory) * OuterParse.token list;
5.27 - val parse_syntax_const: (theory
5.28 - -> CodegenConsts.const list * (string * typ) list
5.29 - -> string
5.30 - -> CodegenNames.const
5.31 - -> term list -> CodegenThingol.iterm list)
5.32 - -> Symtab.key
5.33 - -> string
5.34 - -> OuterParse.token list
5.35 - -> (theory -> theory) * OuterParse.token list;
5.36 +
5.37 val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
5.38 -> ((string -> string) * (string -> string)) option -> int * string
5.39 -> theory -> theory;
5.40 @@ -45,11 +17,20 @@
5.41 -> (string -> string) -> (string -> string) -> string -> theory -> theory;
5.42 val add_undefined: string -> string -> string -> theory -> theory;
5.43
5.44 - type fixity;
5.45 type serializer;
5.46 val add_serializer : string * serializer -> theory -> theory;
5.47 val ml_from_thingol: serializer;
5.48 val hs_from_thingol: serializer;
5.49 + val get_serializer: theory -> string * Args.T list
5.50 + -> string list option -> CodegenThingol.code -> unit;
5.51 +
5.52 + val const_has_serialization: theory -> string list -> string -> bool;
5.53 + val tyco_has_serialization: theory -> string list -> string -> bool;
5.54 +
5.55 + val eval_verbose: bool ref;
5.56 + val eval_term: theory ->
5.57 + (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
5.58 + -> 'a;
5.59 end;
5.60
5.61 structure CodegenSerializer: CODEGEN_SERIALIZER =
5.62 @@ -120,8 +101,7 @@
5.63
5.64 datatype 'a mixfix =
5.65 Arg of fixity
5.66 - | Pretty of Pretty.T
5.67 - | Quote of 'a;
5.68 + | Pretty of Pretty.T;
5.69
5.70 fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
5.71 let
5.72 @@ -131,8 +111,6 @@
5.73 pr fxy a :: fillin ms args
5.74 | fillin (Pretty p :: ms) args =
5.75 p :: fillin ms args
5.76 - | fillin (Quote q :: ms) args =
5.77 - pr BR q :: fillin ms args
5.78 | fillin [] _ =
5.79 error ("Inconsistent mixfix: too many arguments")
5.80 | fillin _ [] =
5.81 @@ -146,44 +124,40 @@
5.82 val r = case x of R => fixity
5.83 | _ => INFX (i, X);
5.84 in
5.85 - pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
5.86 + [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
5.87 end;
5.88
5.89 -fun parse_mixfix reader s ctxt =
5.90 +fun parse_mixfix s =
5.91 let
5.92 - fun sym s = Scan.lift ($$ s);
5.93 - fun lift_reader ctxt s =
5.94 - ctxt
5.95 - |> reader s
5.96 - |-> (fn x => pair (Quote x));
5.97 - val sym_any = Scan.lift (Scan.one Symbol.not_eof);
5.98 + val sym_any = Scan.one Symbol.not_eof;
5.99 val parse = Scan.repeat (
5.100 - (sym "_" -- sym "_" >> K (Arg NOBR))
5.101 - || (sym "_" >> K (Arg BR))
5.102 - || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
5.103 - || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
5.104 - ( $$ "'" |-- Scan.one Symbol.not_eof
5.105 - || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
5.106 - $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
5.107 + ($$ "_" -- $$ "_" >> K (Arg NOBR))
5.108 + || ($$ "_" >> K (Arg BR))
5.109 + || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
5.110 || (Scan.repeat1
5.111 - ( sym "'" |-- sym_any
5.112 - || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
5.113 + ( $$ "'" |-- sym_any
5.114 + || Scan.unless ($$ "_" || $$ "/")
5.115 sym_any) >> (Pretty o str o implode)));
5.116 - in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
5.117 - of (p, (ctxt, [])) => (p, ctxt)
5.118 + in case Scan.finite Symbol.stopper parse (Symbol.explode s)
5.119 + of (p, []) => p
5.120 | _ => error ("Malformed mixfix annotation: " ^ quote s)
5.121 end;
5.122
5.123 -fun parse_syntax num_args reader =
5.124 +fun parse_syntax num_args =
5.125 let
5.126 fun is_arg (Arg _) = true
5.127 | is_arg _ = false;
5.128 - fun parse_nonatomic s ctxt =
5.129 - case parse_mixfix reader s ctxt
5.130 - of ([Pretty _], _) =>
5.131 + fun parse_nonatomic s =
5.132 + case parse_mixfix s
5.133 + of [Pretty _] =>
5.134 error ("Mixfix contains just one pretty element; either declare as "
5.135 ^ quote atomK ^ " or consider adding a break")
5.136 | x => x;
5.137 + fun mk fixity mfx ctxt =
5.138 + let
5.139 + val i = (length o List.filter is_arg) mfx;
5.140 + val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
5.141 + in (i, fillin_mixfix fixity mfx) end;
5.142 val parse = (
5.143 OuterParse.$$$ infixK |-- OuterParse.nat
5.144 >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
5.145 @@ -191,19 +165,11 @@
5.146 >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
5.147 || OuterParse.$$$ infixrK |-- OuterParse.nat
5.148 >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
5.149 - || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
5.150 + || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR)
5.151 || pair (parse_nonatomic, BR)
5.152 ) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
5.153 - fun mk fixity mfx ctxt =
5.154 - let
5.155 - val i = (length o List.filter is_arg) mfx;
5.156 - val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
5.157 - in ((i, fillin_mixfix fixity mfx), ctxt) end;
5.158 in
5.159 - parse
5.160 - #-> (fn (mfx_reader, fixity) =>
5.161 - pair (mfx_reader #-> (fn mfx => (mk fixity mfx)))
5.162 - )
5.163 + parse #-> (fn (mfx, fixity) => pair (mk fixity mfx))
5.164 end;
5.165
5.166
5.167 @@ -858,7 +824,7 @@
5.168 ) classop_defs)
5.169 ]
5.170 end |> SOME
5.171 - in pr_def def end;
5.172 + in Pretty.setmp_margin 999999 pr_def def end;
5.173
5.174
5.175 (** generic abstract serializer **)
5.176 @@ -1320,138 +1286,6 @@
5.177 end;
5.178
5.179
5.180 -(** LEGACY DIAGNOSIS **)
5.181 -
5.182 -local
5.183 -
5.184 -open CodegenThingol;
5.185 -
5.186 -in
5.187 -
5.188 -val pretty_typparms =
5.189 - Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
5.190 - [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
5.191 -
5.192 -fun pretty_itype (tyco `%% tys) =
5.193 - Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
5.194 - | pretty_itype (ty1 `-> ty2) =
5.195 - Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
5.196 - | pretty_itype (ITyVar v) =
5.197 - Pretty.str v;
5.198 -
5.199 -fun pretty_iterm (IConst (c, _)) =
5.200 - Pretty.str c
5.201 - | pretty_iterm (IVar v) =
5.202 - Pretty.str ("?" ^ v)
5.203 - | pretty_iterm (t1 `$ t2) =
5.204 - (Pretty.enclose "(" ")" o Pretty.breaks)
5.205 - [pretty_iterm t1, pretty_iterm t2]
5.206 - | pretty_iterm ((v, ty) `|-> t) =
5.207 - (Pretty.enclose "(" ")" o Pretty.breaks)
5.208 - [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
5.209 - | pretty_iterm (INum (n, _)) =
5.210 - (Pretty.str o IntInf.toString) n
5.211 - | pretty_iterm (IChar (h, _)) =
5.212 - (Pretty.str o quote) h
5.213 - | pretty_iterm (ICase (((t, _), bs), _)) =
5.214 - (Pretty.enclose "(" ")" o Pretty.breaks) [
5.215 - Pretty.str "case",
5.216 - pretty_iterm t,
5.217 - Pretty.enclose "(" ")" (map (fn (p, t) =>
5.218 - (Pretty.block o Pretty.breaks) [
5.219 - pretty_iterm p,
5.220 - Pretty.str "=>",
5.221 - pretty_iterm t
5.222 - ]
5.223 - ) bs)
5.224 - ];
5.225 -
5.226 -fun pretty_def Bot =
5.227 - Pretty.str "<Bot>"
5.228 - | pretty_def (Fun (eqs, (vs, ty))) =
5.229 - Pretty.enum " |" "" "" (
5.230 - map (fn (ps, body) =>
5.231 - Pretty.block [
5.232 - Pretty.enum "," "[" "]" (map pretty_iterm ps),
5.233 - Pretty.str " |->",
5.234 - Pretty.brk 1,
5.235 - pretty_iterm body,
5.236 - Pretty.str "::",
5.237 - pretty_typparms vs,
5.238 - Pretty.str "/",
5.239 - pretty_itype ty
5.240 - ]) eqs
5.241 - )
5.242 - | pretty_def (Datatype (vs, cs)) =
5.243 - Pretty.block [
5.244 - pretty_typparms vs,
5.245 - Pretty.str " |=> ",
5.246 - Pretty.enum " |" "" ""
5.247 - (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
5.248 - (Pretty.str c :: map pretty_itype tys)) cs)
5.249 - ]
5.250 - | pretty_def (Datatypecons dtname) =
5.251 - Pretty.str ("cons " ^ dtname)
5.252 - | pretty_def (Class (supcls, (v, mems))) =
5.253 - Pretty.block [
5.254 - Pretty.str ("class var " ^ v ^ " extending "),
5.255 - Pretty.enum "," "[" "]" (map Pretty.str supcls),
5.256 - Pretty.str " with ",
5.257 - Pretty.enum "," "[" "]"
5.258 - (map (fn (m, ty) => Pretty.block
5.259 - [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
5.260 - ]
5.261 - | pretty_def (Classmember clsname) =
5.262 - Pretty.block [
5.263 - Pretty.str "class member belonging to ",
5.264 - Pretty.str clsname
5.265 - ]
5.266 - | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
5.267 - Pretty.block [
5.268 - Pretty.str "class instance (",
5.269 - Pretty.str clsname,
5.270 - Pretty.str ", (",
5.271 - Pretty.str tyco,
5.272 - Pretty.str ", ",
5.273 - Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
5.274 - map Pretty.str o snd) arity),
5.275 - Pretty.str "))"
5.276 - ];
5.277 -
5.278 -fun pretty_module code =
5.279 - Pretty.chunks (map (fn (name, def) => Pretty.block
5.280 - [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def])
5.281 - (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev)));
5.282 -
5.283 -fun pretty_deps code =
5.284 - let
5.285 - fun one_node key =
5.286 - let
5.287 - val preds_ = Graph.imm_preds code key;
5.288 - val succs_ = Graph.imm_succs code key;
5.289 - val mutbs = gen_inter (op =) (preds_, succs_);
5.290 - val preds = subtract (op =) mutbs preds_;
5.291 - val succs = subtract (op =) mutbs succs_;
5.292 - in
5.293 - (Pretty.block o Pretty.fbreaks) (
5.294 - Pretty.str key
5.295 - :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
5.296 - @ map (fn s => Pretty.str ("<-- " ^ s)) preds
5.297 - @ map (fn s => Pretty.str ("--> " ^ s)) succs
5.298 - )
5.299 - end
5.300 - in
5.301 - code
5.302 - |> Graph.strong_conn
5.303 - |> flat
5.304 - |> rev
5.305 - |> map one_node
5.306 - |> Pretty.chunks
5.307 - end;
5.308 -
5.309 -end; (*local*)
5.310 -
5.311 -
5.312
5.313 (** theory data **)
5.314
5.315 @@ -1603,7 +1437,7 @@
5.316
5.317
5.318
5.319 -(** target syntax interfaces **)
5.320 +(** ML and toplevel interface **)
5.321
5.322 local
5.323
5.324 @@ -1675,26 +1509,26 @@
5.325 val cs'' = map (CodegenConsts.norm_of_typ thy) cs';
5.326 in AList.make (CodegenNames.const thy) cs'' end;
5.327
5.328 -fun read_quote reader consts_of target get_init gen raw_it thy =
5.329 - let
5.330 - val it = reader thy raw_it;
5.331 - val cs = consts_of thy it;
5.332 - in
5.333 - gen thy cs target (get_init thy) [it]
5.334 - |> (fn [it'] => (it', thy))
5.335 - end;
5.336 +fun parse_quote num_of consts_of target get_init adder =
5.337 + parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy));
5.338
5.339 -fun parse_quote num_of reader consts_of target get_init gen adder =
5.340 - parse_syntax num_of
5.341 - (read_quote reader consts_of target get_init gen)
5.342 - #-> (fn modifier => pair (modifier #-> adder target));
5.343 +fun zip_list (x::xs) f g =
5.344 + f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
5.345 + #-> (fn xys => pair ((x, y) :: xys)));
5.346
5.347 -in
5.348 +structure P = OuterParse
5.349 +and K = OuterKeyword
5.350 +
5.351 +fun parse_multi_syntax parse_thing parse_syntax =
5.352 + P.and_list1 parse_thing
5.353 + #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
5.354 + (fn target => zip_list things (parse_syntax target)
5.355 + (P.$$$ "and")) --| P.$$$ ")"))
5.356
5.357 val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const;
5.358 val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type;
5.359
5.360 -fun parse_syntax_tyco generate target raw_tyco =
5.361 +fun parse_syntax_tyco target raw_tyco =
5.362 let
5.363 fun intern thy = read_type thy raw_tyco;
5.364 fun num_of thy = Sign.arity_number thy (intern thy);
5.365 @@ -1702,20 +1536,61 @@
5.366 fun read_typ thy =
5.367 Sign.read_typ (thy, K NONE);
5.368 in
5.369 - parse_quote num_of read_typ ((K o K) ([], [])) target idf_of generate
5.370 + parse_quote num_of ((K o K) ([], [])) target idf_of
5.371 (gen_add_syntax_tyco read_type raw_tyco)
5.372 end;
5.373
5.374 -fun parse_syntax_const generate target raw_const =
5.375 +fun parse_syntax_const target raw_const =
5.376 let
5.377 fun intern thy = CodegenConsts.read_const thy raw_const;
5.378 fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;
5.379 fun idf_of thy = (CodegenNames.const thy o intern) thy;
5.380 in
5.381 - parse_quote num_of Sign.read_term CodegenConsts.consts_of target idf_of generate
5.382 + parse_quote num_of CodegenConsts.consts_of target idf_of
5.383 (gen_add_syntax_const CodegenConsts.read_const raw_const)
5.384 end;
5.385
5.386 +val (code_classK, code_instanceK, code_typeK, code_constK) =
5.387 + ("code_class", "code_instance", "code_type", "code_const");
5.388 +
5.389 +in
5.390 +
5.391 +val code_classP =
5.392 + OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
5.393 + parse_multi_syntax P.xname
5.394 + (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
5.395 + (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
5.396 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
5.397 + fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)
5.398 + );
5.399 +
5.400 +val code_instanceP =
5.401 + OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
5.402 + parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
5.403 + (fn _ => fn _ => P.name #->
5.404 + (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
5.405 + >> (Toplevel.theory oo fold) (fn (target, syns) =>
5.406 + fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns)
5.407 + );
5.408 +
5.409 +val code_typeP =
5.410 + OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
5.411 + Scan.repeat1 (
5.412 + parse_multi_syntax P.xname parse_syntax_tyco
5.413 + )
5.414 + >> (Toplevel.theory o (fold o fold) (fold snd o snd))
5.415 + );
5.416 +
5.417 +val code_constP =
5.418 + OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
5.419 + Scan.repeat1 (
5.420 + parse_multi_syntax P.term parse_syntax_const
5.421 + )
5.422 + >> (Toplevel.theory o (fold o fold) (fold snd o snd))
5.423 + );
5.424 +
5.425 +val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP];
5.426 +
5.427 fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
5.428 let
5.429 val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];