--- a/etc/isar-keywords-HOL-Nominal.el Mon Oct 09 20:12:45 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Tue Oct 10 09:17:17 2006 +0200
@@ -43,15 +43,16 @@
"classes"
"classrel"
"clear_undos"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_gen"
"code_instance"
"code_instname"
"code_library"
"code_module"
- "code_simtype"
"code_type"
"code_typename"
"coinductive"
@@ -206,6 +207,7 @@
"types_code"
"ultimately"
"undo"
+ "undo_end"
"undos_proof"
"unfolding"
"update_thy"
@@ -283,6 +285,7 @@
"quit"
"redo"
"undo"
+ "undo_end"
"undos_proof"))
(defconst isar-keywords-diag
@@ -373,9 +376,11 @@
"class"
"classes"
"classrel"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_instance"
"code_instname"
"code_library"
@@ -439,7 +444,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
- "code_simtype"
"corollary"
"function"
"instance"
--- a/etc/isar-keywords-ZF.el Mon Oct 09 20:12:45 2006 +0200
+++ b/etc/isar-keywords-ZF.el Tue Oct 10 09:17:17 2006 +0200
@@ -41,15 +41,16 @@
"classrel"
"clear_undos"
"codatatype"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_gen"
"code_instance"
"code_instname"
"code_library"
"code_module"
- "code_simtype"
"code_type"
"code_typename"
"coinductive"
@@ -193,6 +194,7 @@
"types_code"
"ultimately"
"undo"
+ "undo_end"
"undos_proof"
"unfolding"
"update_thy"
@@ -269,6 +271,7 @@
"quit"
"redo"
"undo"
+ "undo_end"
"undos_proof"))
(defconst isar-keywords-diag
@@ -358,9 +361,11 @@
"classes"
"classrel"
"codatatype"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_instance"
"code_instname"
"code_library"
@@ -417,8 +422,7 @@
"inductive_cases"))
(defconst isar-keywords-theory-goal
- '("code_simtype"
- "corollary"
+ '("corollary"
"instance"
"interpretation"
"lemma"
--- a/etc/isar-keywords.el Mon Oct 09 20:12:45 2006 +0200
+++ b/etc/isar-keywords.el Tue Oct 10 09:17:17 2006 +0200
@@ -43,15 +43,16 @@
"classes"
"classrel"
"clear_undos"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_gen"
"code_instance"
"code_instname"
"code_library"
"code_module"
- "code_simtype"
"code_type"
"code_typename"
"coinductive"
@@ -210,6 +211,7 @@
"types_code"
"ultimately"
"undo"
+ "undo_end"
"undos_proof"
"unfolding"
"update_thy"
@@ -304,6 +306,7 @@
"quit"
"redo"
"undo"
+ "undo_end"
"undos_proof"))
(defconst isar-keywords-diag
@@ -394,9 +397,11 @@
"class"
"classes"
"classrel"
+ "code_abstype"
"code_class"
"code_const"
"code_constname"
+ "code_constsubst"
"code_instance"
"code_instname"
"code_library"
@@ -462,7 +467,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
- "code_simtype"
"corollary"
"cpodef"
"function"
--- a/src/Pure/Tools/codegen_package.ML Mon Oct 09 20:12:45 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Oct 10 09:17:17 2006 +0200
@@ -35,34 +35,53 @@
(* theory data *)
+structure Code = CodeDataFun
+(struct
+ val name = "Pure/code";
+ type T = CodegenThingol.code;
+ val empty = CodegenThingol.empty_code;
+ fun merge _ = CodegenThingol.merge_code;
+ fun purge _ NONE _ = CodegenThingol.empty_code
+ | purge NONE _ _ = CodegenThingol.empty_code
+ | purge (SOME thy) (SOME cs) code =
+ let
+ val cs_exisiting =
+ map_filter (CodegenNames.const_rev thy) (Graph.keys code);
+ in
+ Graph.del_nodes
+ ((Graph.all_succs code
+ o map (CodegenNames.const thy)
+ o filter (member CodegenConsts.eq_const cs_exisiting)
+ ) cs)
+ code
+ end;
+end);
+
type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T
-> CodegenFuncgr.T
-> bool * string list option
-> (string * typ) * term list -> CodegenThingol.transact -> iterm * CodegenThingol.transact;
type appgens = (int * (appgen * stamp)) Symtab.table;
-
-fun merge_appgens (x : appgens * appgens) =
+val merge_appgens : appgens * appgens -> appgens =
Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
- bounds1 = bounds2 andalso stamp1 = stamp2) x;
+ bounds1 = bounds2 andalso stamp1 = stamp2);
-structure Code = CodeDataFun
-(struct
- val name = "Pure/code";
- type T = CodegenThingol.code;
- val empty = CodegenThingol.empty_code;
- fun merge _ = CodegenThingol.merge_code;
- fun purge _ _ = CodegenThingol.empty_code;
-end);
+structure Consttab = CodegenConsts.Consttab;
+type abstypes = typ Symtab.table * CodegenConsts.const Consttab.table;
+fun merge_abstypes ((typs1, consts1) : abstypes, (typs2, consts2) : abstypes) =
+ (Symtab.merge (Type.eq_type Vartab.empty) (typs1, typs2),
+ Consttab.merge CodegenConsts.eq_const (consts1, consts2));
structure CodegenPackageData = TheoryDataFun
(struct
val name = "Pure/codegen_package";
- type T = appgens;
- val empty = Symtab.empty;
+ type T = appgens * abstypes;
+ val empty = (Symtab.empty, (Symtab.empty, Consttab.empty));
val copy = I;
val extend = I;
- fun merge _ = merge_appgens;
+ fun merge _ ((appgens1, abstypes1), (appgens2, abstypes2)) =
+ (merge_appgens (appgens1, appgens2), merge_abstypes (abstypes1, abstypes2));
fun print _ _ = ();
end);
@@ -71,13 +90,17 @@
(* extraction kernel *)
-fun check_strict has_seri x (false, _) =
+fun check_strict (false, _) has_seri x =
false
- | check_strict has_seri x (_, SOME targets) =
+ | check_strict (_, SOME targets) has_seri x =
not (has_seri targets x)
- | check_strict has_seri x (true, _) =
+ | check_strict (true, _) has_seri x =
true;
+fun get_abstype thy (tyco, tys) = case Symtab.lookup ((fst o snd o CodegenPackageData.get) thy) tyco
+ of SOME ty => SOME ((map_atyps (fn TFree (n, _) => nth tys (the (Int.fromString n)))) ty)
+ | NONE => NONE;
+
fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
let
val (v, cs) = (ClassPackage.the_consts_sign thy) class;
@@ -115,7 +138,7 @@
trns
|> fail ("No such datatype: " ^ quote tyco)
val tyco' = CodegenNames.tyco thy tyco;
- val strict = check_strict (CodegenSerializer.tyco_has_serialization thy) tyco' strct;
+ val strict = check_strict strct (CodegenSerializer.tyco_has_serialization thy) tyco';
in
trns
|> tracing (fn _ => "generating type constructor " ^ quote tyco)
@@ -139,10 +162,15 @@
||>> exprgen_type thy algbr funcgr strct t2
|-> (fn (t1', t2') => pair (t1' `-> t2'))
| exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns =
- trns
- |> ensure_def_tyco thy algbr funcgr strct tyco
- ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
- |-> (fn (tyco, tys) => pair (tyco `%% tys));
+ case get_abstype thy (tyco, tys)
+ of SOME ty =>
+ trns
+ |> exprgen_type thy algbr funcgr strct ty
+ | NONE =>
+ trns
+ |> ensure_def_tyco thy algbr funcgr strct tyco
+ ||>> fold_map (exprgen_type thy algbr funcgr strct) tys
+ |-> (fn (tyco, tys) => pair (tyco `%% tys));
exception CONSTRAIN of (string * typ) * typ;
@@ -239,7 +267,8 @@
|> ensure_def_class thy algbr funcgr strct ((the o AxClass.class_of_param thy) c)
|-> (fn _ => succeed CodegenThingol.Bot);
fun defgen_fun trns =
- case CodegenFuncgr.get_funcs funcgr (c, tys)
+ case CodegenFuncgr.get_funcs funcgr
+ (perhaps (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (c, tys))
of eq_thms as eq_thm :: _ =>
let
val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms);
@@ -271,7 +300,7 @@
else if CodegenNames.has_nsp CodegenNames.nsp_dtco c'
then defgen_datatypecons
else error ("Illegal shallow name space for constant: " ^ quote c');
- val strict = check_strict (CodegenSerializer.const_has_serialization thy) c' strct;
+ val strict = check_strict strct (CodegenSerializer.const_has_serialization thy) c';
in
trns
|> tracing (fn _ => "generating constant "
@@ -318,7 +347,7 @@
|-> (fn (((c, ty), iss), ts) =>
pair (IConst (c, (iss, ty)) `$$ ts))
and select_appgen thy algbr funcgr strct ((c, ty), ts) trns =
- case Symtab.lookup (CodegenPackageData.get thy) c
+ case Symtab.lookup (fst (CodegenPackageData.get thy)) c
of SOME (i, (appgen, _)) =>
if length ts < i then
let
@@ -415,8 +444,96 @@
fun add_appconst (c, appgen) thy =
let
- val i = (length o fst o strip_type o Sign.the_const_type thy) c
- in CodegenPackageData.map (Symtab.update (c, (i, (appgen, stamp ())))) thy end;
+ val i = (length o fst o strip_type o Sign.the_const_type thy) c;
+ val _ = Code.change thy (K CodegenThingol.empty_code);
+ in
+ (CodegenPackageData.map o apfst)
+ (Symtab.update (c, (i, (appgen, stamp ())))) thy
+ end;
+
+
+
+(** abstype and constsubst interface **)
+
+fun gen_abstyp prep_const prep_typ (raw_abstyp, raw_substtyp) raw_absconsts thy =
+ let
+ val abstyp = Type.no_tvars (prep_typ thy raw_abstyp);
+ val substtyp = Type.no_tvars (prep_typ thy raw_substtyp);
+ val absconsts = (map o pairself) (prep_const thy) raw_absconsts;
+ val Type (abstyco, tys) = abstyp handle BIND => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
+ val typarms = map (fst o dest_TFree) tys handle MATCH => error ("bad type: " ^ Sign.string_of_typ thy abstyp);
+ fun mk_index v =
+ let
+ val k = find_index (fn w => v = w) typarms;
+ in if k = ~1
+ then error ("free type variable: " ^ quote v)
+ else TFree (string_of_int k, [])
+ end;
+ val typpat = map_atyps (fn TFree (v, _) => mk_index v) substtyp;
+ fun apply_typpat (Type (tyco, tys)) =
+ let
+ val tys' = map apply_typpat tys;
+ in if tyco = abstyco then
+ (map_atyps (fn TFree (n, _) => nth tys' (the (Int.fromString n)))) typpat
+ else
+ Type (tyco, tys')
+ end
+ | apply_typpat ty = ty;
+ val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
+ fun add_consts (c1, c2) =
+ let
+ val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
+ then ()
+ else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
+ val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
+ val ty_map = CodegenFuncgr.get_func_typs funcgr;
+ val ty1 = (apply_typpat o the o AList.lookup CodegenConsts.eq_const ty_map) c1;
+ val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
+ val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
+ error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
+ ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
+ ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
+ in Consttab.update (c1, c2) end;
+ val _ = Code.change thy (K CodegenThingol.empty_code);
+ in
+ thy
+ |> (CodegenPackageData.map o apsnd) (fn (abstypes, abscs) =>
+ (abstypes
+ |> Symtab.update (abstyco, typpat),
+ abscs
+ |> fold add_consts absconsts)
+ )
+ end;
+
+fun gen_constsubst prep_const raw_constsubsts thy =
+ let
+ val constsubsts = (map o pairself) (prep_const thy) raw_constsubsts;
+ val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
+ fun add_consts (c1, c2) =
+ let
+ val _ = if CodegenNames.has_nsp CodegenNames.nsp_fun (CodegenNames.const thy c2)
+ then ()
+ else error ("not a function: " ^ CodegenConsts.string_of_const thy c2);
+ val funcgr = CodegenFuncgr.mk_funcgr thy [c1, c2] [];
+ val ty_map = CodegenFuncgr.get_func_typs funcgr;
+ val ty1 = (the o AList.lookup CodegenConsts.eq_const ty_map) c1;
+ val ty2 = (the o AList.lookup CodegenConsts.eq_const ty_map) c2;
+ val _ = if Sign.typ_equiv thy (ty1, ty2) then () else
+ error ("Incompatiable type signatures of " ^ CodegenConsts.string_of_const thy c1
+ ^ " and " ^ CodegenConsts.string_of_const thy c2 ^ ":\n"
+ ^ string_of_typ ty1 ^ "\n" ^ string_of_typ ty2);
+ in Consttab.update (c1, c2) end;
+ val _ = Code.change thy (K CodegenThingol.empty_code);
+ in
+ thy
+ |> (CodegenPackageData.map o apsnd o apsnd) (fold add_consts constsubsts)
+ end;
+
+val abstyp = gen_abstyp CodegenConsts.norm Sign.certify_typ;
+val abstyp_e = gen_abstyp CodegenConsts.read_const (fn thy => Sign.read_typ (thy, K NONE));
+
+val constsubst = gen_constsubst CodegenConsts.norm;
+val constsubst_e = gen_constsubst CodegenConsts.read_const;
@@ -424,13 +541,16 @@
fun generate thy (cs, rhss) targets init gen it =
let
- val funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
- val qnaming = NameSpace.qualified_names NameSpace.default_naming
+ val raw_funcgr = CodegenFuncgr.mk_funcgr thy cs rhss;
+ val cs' = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy))
+ (CodegenFuncgr.Constgraph.keys raw_funcgr);
+ val funcgr = CodegenFuncgr.mk_funcgr thy cs' [];
+ val qnaming = NameSpace.qualified_names NameSpace.default_naming;
val algebr = ClassPackage.operational_algebra thy;
val consttab = Consts.empty
|> fold (fn (c, ty) => Consts.declare qnaming
((CodegenNames.const thy c, ty), true))
- (CodegenFuncgr.get_func_typs funcgr)
+ (CodegenFuncgr.get_func_typs funcgr);
val algbr = (algebr, consttab);
in
Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr
@@ -504,30 +624,11 @@
(map (serialize' cs code) seris'; ())
end;
-fun reader_tyco thy rhss target dep =
- generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_type);
-
-fun reader_const thy rhss target dep =
- generate thy rhss (SOME [target]) (SOME dep) (fold_map oooo exprgen_term');
-
-fun zip_list (x::xs) f g =
- f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
- #-> (fn xys => pair ((x, y) :: xys)));
-
-fun parse_multi_syntax parse_thing parse_syntax =
- P.and_list1 parse_thing
- #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
- (fn target => zip_list things (parse_syntax target)
- (P.$$$ "and")) --| P.$$$ ")"))
-
+val (codeK, code_abstypeK, code_constsubstK) =
+ ("code_gen", "code_abstype", "code_constsubst");
in
-val (codeK,
- syntax_classK, syntax_instK, syntax_tycoK, syntax_constK) =
- ("code_gen",
- "code_class", "code_instance", "code_type", "code_const");
-
val codeP =
OuterSyntax.improper_command codeK "generate and serialize executable code for constants" K.diag (
Scan.repeat P.term
@@ -537,42 +638,20 @@
>> (fn (raw_cs, seris) => Toplevel.keep (code raw_cs seris o Toplevel.theory_of))
);
-val syntax_classP =
- OuterSyntax.command syntax_classK "define code syntax for class" K.thy_decl (
- parse_multi_syntax P.xname
- (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
- (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_class, syn) => CodegenSerializer.add_syntax_class target raw_class syn) syns)
- );
-
-val syntax_instP =
- OuterSyntax.command syntax_instK "define code syntax for instance" K.thy_decl (
- parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
- (fn _ => fn _ => P.name #->
- (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
- >> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_inst, ()) => CodegenSerializer.add_syntax_inst target raw_inst) syns)
+val code_abstypeP =
+ OuterSyntax.command code_abstypeK "axiomatic abstypes for code generation" K.thy_decl (
+ (P.typ -- P.typ -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
+ (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)) [])
+ >> (Toplevel.theory o uncurry abstyp_e)
);
-val syntax_tycoP =
- OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
- Scan.repeat1 (
- parse_multi_syntax P.xname (CodegenSerializer.parse_syntax_tyco reader_tyco)
- )
- >> (Toplevel.theory o (fold o fold) (fold snd o snd))
+val code_constsubstP =
+ OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl (
+ Scan.repeat1 (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.term)
+ >> (Toplevel.theory o constsubst_e)
);
-val syntax_constP =
- OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
- Scan.repeat1 (
- parse_multi_syntax P.term (CodegenSerializer.parse_syntax_const reader_const)
- )
- >> (Toplevel.theory o (fold o fold) (fold snd o snd))
- );
-
-val _ = OuterSyntax.add_parsers [codeP,
- syntax_classP, syntax_instP, syntax_tycoP, syntax_constP];
+val _ = OuterSyntax.add_parsers [codeP, code_abstypeP, code_constsubstP];
end; (* local *)
--- a/src/Pure/Tools/codegen_serializer.ML Mon Oct 09 20:12:45 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Oct 10 09:17:17 2006 +0200
@@ -9,35 +9,7 @@
signature CODEGEN_SERIALIZER =
sig
include BASIC_CODEGEN_THINGOL;
- val get_serializer: theory -> string * Args.T list
- -> string list option -> CodegenThingol.code -> unit;
- val eval_verbose: bool ref;
- val eval_term: theory ->
- (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
- -> 'a;
- val const_has_serialization: theory -> string list -> string -> bool;
- val tyco_has_serialization: theory -> string list -> string -> bool;
- val add_syntax_class:
- string -> string -> string * (string * string) list -> theory -> theory;
- val add_syntax_inst: string -> (string * string) -> theory -> theory;
- val parse_syntax_tyco: (theory
- -> CodegenConsts.const list * (string * typ) list
- -> string
- -> CodegenNames.tyco
- -> typ list -> CodegenThingol.itype list)
- -> Symtab.key
- -> xstring
- -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list;
- val parse_syntax_const: (theory
- -> CodegenConsts.const list * (string * typ) list
- -> string
- -> CodegenNames.const
- -> term list -> CodegenThingol.iterm list)
- -> Symtab.key
- -> string
- -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list;
+
val add_pretty_list: string -> string -> string -> (Pretty.T list -> Pretty.T)
-> ((string -> string) * (string -> string)) option -> int * string
-> theory -> theory;
@@ -45,11 +17,20 @@
-> (string -> string) -> (string -> string) -> string -> theory -> theory;
val add_undefined: string -> string -> string -> theory -> theory;
- type fixity;
type serializer;
val add_serializer : string * serializer -> theory -> theory;
val ml_from_thingol: serializer;
val hs_from_thingol: serializer;
+ val get_serializer: theory -> string * Args.T list
+ -> string list option -> CodegenThingol.code -> unit;
+
+ val const_has_serialization: theory -> string list -> string -> bool;
+ val tyco_has_serialization: theory -> string list -> string -> bool;
+
+ val eval_verbose: bool ref;
+ val eval_term: theory ->
+ (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.code
+ -> 'a;
end;
structure CodegenSerializer: CODEGEN_SERIALIZER =
@@ -120,8 +101,7 @@
datatype 'a mixfix =
Arg of fixity
- | Pretty of Pretty.T
- | Quote of 'a;
+ | Pretty of Pretty.T;
fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
let
@@ -131,8 +111,6 @@
pr fxy a :: fillin ms args
| fillin (Pretty p :: ms) args =
p :: fillin ms args
- | fillin (Quote q :: ms) args =
- pr BR q :: fillin ms args
| fillin [] _ =
error ("Inconsistent mixfix: too many arguments")
| fillin _ [] =
@@ -146,44 +124,40 @@
val r = case x of R => fixity
| _ => INFX (i, X);
in
- pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
+ [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
end;
-fun parse_mixfix reader s ctxt =
+fun parse_mixfix s =
let
- fun sym s = Scan.lift ($$ s);
- fun lift_reader ctxt s =
- ctxt
- |> reader s
- |-> (fn x => pair (Quote x));
- val sym_any = Scan.lift (Scan.one Symbol.not_eof);
+ val sym_any = Scan.one Symbol.not_eof;
val parse = Scan.repeat (
- (sym "_" -- sym "_" >> K (Arg NOBR))
- || (sym "_" >> K (Arg BR))
- || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
- || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
- ( $$ "'" |-- Scan.one Symbol.not_eof
- || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
- $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
+ ($$ "_" -- $$ "_" >> K (Arg NOBR))
+ || ($$ "_" >> K (Arg BR))
+ || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
|| (Scan.repeat1
- ( sym "'" |-- sym_any
- || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
+ ( $$ "'" |-- sym_any
+ || Scan.unless ($$ "_" || $$ "/")
sym_any) >> (Pretty o str o implode)));
- in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
- of (p, (ctxt, [])) => (p, ctxt)
+ in case Scan.finite Symbol.stopper parse (Symbol.explode s)
+ of (p, []) => p
| _ => error ("Malformed mixfix annotation: " ^ quote s)
end;
-fun parse_syntax num_args reader =
+fun parse_syntax num_args =
let
fun is_arg (Arg _) = true
| is_arg _ = false;
- fun parse_nonatomic s ctxt =
- case parse_mixfix reader s ctxt
- of ([Pretty _], _) =>
+ fun parse_nonatomic s =
+ case parse_mixfix s
+ of [Pretty _] =>
error ("Mixfix contains just one pretty element; either declare as "
^ quote atomK ^ " or consider adding a break")
| x => x;
+ fun mk fixity mfx ctxt =
+ let
+ val i = (length o List.filter is_arg) mfx;
+ val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
+ in (i, fillin_mixfix fixity mfx) end;
val parse = (
OuterParse.$$$ infixK |-- OuterParse.nat
>> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
@@ -191,19 +165,11 @@
>> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
|| OuterParse.$$$ infixrK |-- OuterParse.nat
>> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
- || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
+ || OuterParse.$$$ atomK |-- pair (parse_mixfix, NOBR)
|| pair (parse_nonatomic, BR)
) -- OuterParse.string >> (fn ((p, fxy), s) => (p s, fxy));
- fun mk fixity mfx ctxt =
- let
- val i = (length o List.filter is_arg) mfx;
- val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else ();
- in ((i, fillin_mixfix fixity mfx), ctxt) end;
in
- parse
- #-> (fn (mfx_reader, fixity) =>
- pair (mfx_reader #-> (fn mfx => (mk fixity mfx)))
- )
+ parse #-> (fn (mfx, fixity) => pair (mk fixity mfx))
end;
@@ -858,7 +824,7 @@
) classop_defs)
]
end |> SOME
- in pr_def def end;
+ in Pretty.setmp_margin 999999 pr_def def end;
(** generic abstract serializer **)
@@ -1320,138 +1286,6 @@
end;
-(** LEGACY DIAGNOSIS **)
-
-local
-
-open CodegenThingol;
-
-in
-
-val pretty_typparms =
- Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
- [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
-
-fun pretty_itype (tyco `%% tys) =
- Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
- | pretty_itype (ty1 `-> ty2) =
- Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
- | pretty_itype (ITyVar v) =
- Pretty.str v;
-
-fun pretty_iterm (IConst (c, _)) =
- Pretty.str c
- | pretty_iterm (IVar v) =
- Pretty.str ("?" ^ v)
- | pretty_iterm (t1 `$ t2) =
- (Pretty.enclose "(" ")" o Pretty.breaks)
- [pretty_iterm t1, pretty_iterm t2]
- | pretty_iterm ((v, ty) `|-> t) =
- (Pretty.enclose "(" ")" o Pretty.breaks)
- [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
- | pretty_iterm (INum (n, _)) =
- (Pretty.str o IntInf.toString) n
- | pretty_iterm (IChar (h, _)) =
- (Pretty.str o quote) h
- | pretty_iterm (ICase (((t, _), bs), _)) =
- (Pretty.enclose "(" ")" o Pretty.breaks) [
- Pretty.str "case",
- pretty_iterm t,
- Pretty.enclose "(" ")" (map (fn (p, t) =>
- (Pretty.block o Pretty.breaks) [
- pretty_iterm p,
- Pretty.str "=>",
- pretty_iterm t
- ]
- ) bs)
- ];
-
-fun pretty_def Bot =
- Pretty.str "<Bot>"
- | pretty_def (Fun (eqs, (vs, ty))) =
- Pretty.enum " |" "" "" (
- map (fn (ps, body) =>
- Pretty.block [
- Pretty.enum "," "[" "]" (map pretty_iterm ps),
- Pretty.str " |->",
- Pretty.brk 1,
- pretty_iterm body,
- Pretty.str "::",
- pretty_typparms vs,
- Pretty.str "/",
- pretty_itype ty
- ]) eqs
- )
- | pretty_def (Datatype (vs, cs)) =
- Pretty.block [
- pretty_typparms vs,
- Pretty.str " |=> ",
- Pretty.enum " |" "" ""
- (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
- (Pretty.str c :: map pretty_itype tys)) cs)
- ]
- | pretty_def (Datatypecons dtname) =
- Pretty.str ("cons " ^ dtname)
- | pretty_def (Class (supcls, (v, mems))) =
- Pretty.block [
- Pretty.str ("class var " ^ v ^ " extending "),
- Pretty.enum "," "[" "]" (map Pretty.str supcls),
- Pretty.str " with ",
- Pretty.enum "," "[" "]"
- (map (fn (m, ty) => Pretty.block
- [Pretty.str (m ^ "::"), pretty_itype ty]) mems)
- ]
- | pretty_def (Classmember clsname) =
- Pretty.block [
- Pretty.str "class member belonging to ",
- Pretty.str clsname
- ]
- | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
- Pretty.block [
- Pretty.str "class instance (",
- Pretty.str clsname,
- Pretty.str ", (",
- Pretty.str tyco,
- Pretty.str ", ",
- Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
- map Pretty.str o snd) arity),
- Pretty.str "))"
- ];
-
-fun pretty_module code =
- Pretty.chunks (map (fn (name, def) => Pretty.block
- [Pretty.str name, Pretty.str " :=", Pretty.brk 1, pretty_def def])
- (AList.make (Graph.get_node code) (Graph.strong_conn code |> flat |> rev)));
-
-fun pretty_deps code =
- let
- fun one_node key =
- let
- val preds_ = Graph.imm_preds code key;
- val succs_ = Graph.imm_succs code key;
- val mutbs = gen_inter (op =) (preds_, succs_);
- val preds = subtract (op =) mutbs preds_;
- val succs = subtract (op =) mutbs succs_;
- in
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str key
- :: map (fn s => Pretty.str ("<-> " ^ s)) mutbs
- @ map (fn s => Pretty.str ("<-- " ^ s)) preds
- @ map (fn s => Pretty.str ("--> " ^ s)) succs
- )
- end
- in
- code
- |> Graph.strong_conn
- |> flat
- |> rev
- |> map one_node
- |> Pretty.chunks
- end;
-
-end; (*local*)
-
-
(** theory data **)
@@ -1603,7 +1437,7 @@
-(** target syntax interfaces **)
+(** ML and toplevel interface **)
local
@@ -1675,26 +1509,26 @@
val cs'' = map (CodegenConsts.norm_of_typ thy) cs';
in AList.make (CodegenNames.const thy) cs'' end;
-fun read_quote reader consts_of target get_init gen raw_it thy =
- let
- val it = reader thy raw_it;
- val cs = consts_of thy it;
- in
- gen thy cs target (get_init thy) [it]
- |> (fn [it'] => (it', thy))
- end;
+fun parse_quote num_of consts_of target get_init adder =
+ parse_syntax num_of #-> (fn mfx => pair (fn thy => adder target (mfx thy) thy));
+
+fun zip_list (x::xs) f g =
+ f x #-> (fn y => fold_map (fn x => g |-- f x >> pair x) xs
+ #-> (fn xys => pair ((x, y) :: xys)));
-fun parse_quote num_of reader consts_of target get_init gen adder =
- parse_syntax num_of
- (read_quote reader consts_of target get_init gen)
- #-> (fn modifier => pair (modifier #-> adder target));
+structure P = OuterParse
+and K = OuterKeyword
-in
+fun parse_multi_syntax parse_thing parse_syntax =
+ P.and_list1 parse_thing
+ #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name :--
+ (fn target => zip_list things (parse_syntax target)
+ (P.$$$ "and")) --| P.$$$ ")"))
val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const;
val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type;
-fun parse_syntax_tyco generate target raw_tyco =
+fun parse_syntax_tyco target raw_tyco =
let
fun intern thy = read_type thy raw_tyco;
fun num_of thy = Sign.arity_number thy (intern thy);
@@ -1702,20 +1536,61 @@
fun read_typ thy =
Sign.read_typ (thy, K NONE);
in
- parse_quote num_of read_typ ((K o K) ([], [])) target idf_of generate
+ parse_quote num_of ((K o K) ([], [])) target idf_of
(gen_add_syntax_tyco read_type raw_tyco)
end;
-fun parse_syntax_const generate target raw_const =
+fun parse_syntax_const target raw_const =
let
fun intern thy = CodegenConsts.read_const thy raw_const;
fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;
fun idf_of thy = (CodegenNames.const thy o intern) thy;
in
- parse_quote num_of Sign.read_term CodegenConsts.consts_of target idf_of generate
+ parse_quote num_of CodegenConsts.consts_of target idf_of
(gen_add_syntax_const CodegenConsts.read_const raw_const)
end;
+val (code_classK, code_instanceK, code_typeK, code_constK) =
+ ("code_class", "code_instance", "code_type", "code_const");
+
+in
+
+val code_classP =
+ OuterSyntax.command code_classK "define code syntax for class" K.thy_decl (
+ parse_multi_syntax P.xname
+ (fn _ => fn _ => P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
+ (P.term --| (P.$$$ "\\<equiv>" || P.$$$ "==") -- P.string)) [])
+ >> (Toplevel.theory oo fold) (fn (target, syns) =>
+ fold (fn (raw_class, syn) => add_syntax_class target raw_class syn) syns)
+ );
+
+val code_instanceP =
+ OuterSyntax.command code_instanceK "define code syntax for instance" K.thy_decl (
+ parse_multi_syntax (P.xname --| P.$$$ "::" -- P.xname)
+ (fn _ => fn _ => P.name #->
+ (fn "-" => Scan.succeed () | _ => Scan.fail_with (fn _ => "\"-\" expected") ()))
+ >> (Toplevel.theory oo fold) (fn (target, syns) =>
+ fold (fn (raw_inst, ()) => add_syntax_inst target raw_inst) syns)
+ );
+
+val code_typeP =
+ OuterSyntax.command code_typeK "define code syntax for type constructor" K.thy_decl (
+ Scan.repeat1 (
+ parse_multi_syntax P.xname parse_syntax_tyco
+ )
+ >> (Toplevel.theory o (fold o fold) (fold snd o snd))
+ );
+
+val code_constP =
+ OuterSyntax.command code_constK "define code syntax for constant" K.thy_decl (
+ Scan.repeat1 (
+ parse_multi_syntax P.term parse_syntax_const
+ )
+ >> (Toplevel.theory o (fold o fold) (fold snd o snd))
+ );
+
+val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP];
+
fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
let
val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];