# HG changeset patch # User haftmann # Date 1160464637 -7200 # Node ID 19d9b78218fd5c42575c74d24450a0676fcba127 # Parent 7ab9fa7d658fd676cd3da92ed8fa69afd3f020b0 added code_abstype and code_constsubst diff -r 7ab9fa7d658f -r 19d9b78218fd etc/isar-keywords-HOL-Nominal.el --- 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" diff -r 7ab9fa7d658f -r 19d9b78218fd etc/isar-keywords-ZF.el --- 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" diff -r 7ab9fa7d658f -r 19d9b78218fd etc/isar-keywords.el --- 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" diff -r 7ab9fa7d658f -r 19d9b78218fd src/Pure/Tools/codegen_package.ML --- 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; +val merge_appgens : appgens * appgens -> appgens = + Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => + bounds1 = bounds2 andalso stamp1 = stamp2); -fun merge_appgens (x : appgens * appgens) = - Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => - bounds1 = bounds2 andalso stamp1 = stamp2) x; - -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.$$$ "\\" || 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 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.$$$ "\\" || P.$$$ "==") -- P.term)) []) + >> (Toplevel.theory o uncurry abstyp_e) ); -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_constsubstP = + OuterSyntax.command code_constsubstK "axiomatic constant substitutions for code generation" K.thy_decl ( + Scan.repeat1 (P.term --| (P.$$$ "\\" || P.$$$ "==") -- P.term) + >> (Toplevel.theory o constsubst_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 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 *) diff -r 7ab9fa7d658f -r 19d9b78218fd src/Pure/Tools/codegen_serializer.ML --- 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 "" - | 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 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)); +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))); -in +structure P = OuterParse +and K = OuterKeyword + +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.$$$ "\\" || 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];