# HG changeset patch
# User berghofe
# Date 1007995174 -3600
# Node ID 68493b92e7a67f5500725c1aa7dac4b2b8177816
# Parent  0224f472be7134057d6732d78c9d0b2ffe5c0cac
- Added code generator interface for types
- Changed type of invoke_codegen

diff -r 0224f472be71 -r 68493b92e7a6 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Mon Dec 10 15:37:03 2001 +0100
+++ b/src/Pure/codegen.ML	Mon Dec 10 15:39:34 2001 +0100
@@ -11,25 +11,28 @@
   val quiet_mode : bool ref
   val message : string -> unit
 
-  datatype mixfix =
+  datatype 'a mixfix =
       Arg
     | Ignore
     | Pretty of Pretty.T
-    | Term of term;
+    | Quote of 'a;
 
-  val add_codegen: string ->
-    (theory -> (exn option * string) Graph.T -> string -> bool -> term ->
-    ((exn option * string) Graph.T * Pretty.T) option) -> theory -> theory
+  type 'a codegen
+
+  val add_codegen: string -> term codegen -> theory -> theory
+  val add_tycodegen: string -> typ codegen -> theory -> theory
   val print_codegens: theory -> unit
   val generate_code: theory -> (string * string) list -> string
   val generate_code_i: theory -> (string * term) list -> string
-  val assoc_consts: (xstring * string option * mixfix list) list -> theory -> theory
-  val assoc_consts_i: (xstring * typ option * mixfix list) list -> theory -> theory
-  val assoc_types: (xstring * string) list -> theory -> theory
-  val get_assoc_code: theory -> string -> typ -> mixfix list option
-  val get_assoc_types: theory -> (string * string) list
-  val invoke_codegen: theory -> (exn option * string) Graph.T ->
-    string -> bool -> term -> (exn option * string) Graph.T * Pretty.T
+  val assoc_consts: (xstring * string option * term mixfix list) list -> theory -> theory
+  val assoc_consts_i: (xstring * typ option * term mixfix list) list -> theory -> theory
+  val assoc_types: (xstring * typ mixfix list) list -> theory -> theory
+  val get_assoc_code: theory -> string -> typ -> term mixfix list option
+  val get_assoc_type: theory -> string -> typ mixfix list option
+  val invoke_codegen: theory -> string -> bool ->
+    (exn option * string) Graph.T * term -> (exn option * string) Graph.T * Pretty.T
+  val invoke_tycodegen: theory -> string -> bool ->
+    (exn option * string) Graph.T * typ -> (exn option * string) Graph.T * Pretty.T
   val mk_const_id: Sign.sg -> string -> string
   val mk_type_id: Sign.sg -> string -> string
   val rename_term: term -> term
@@ -38,6 +41,7 @@
   val parens: Pretty.T -> Pretty.T
   val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T
   val eta_expand: term -> term list -> int -> term
+  val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
   val parsers: OuterSyntax.parser list
   val setup: (theory -> theory) list
 end;
@@ -50,19 +54,24 @@
 
 (**** Mixfix syntax ****)
 
-datatype mixfix =
+datatype 'a mixfix =
     Arg
   | Ignore
   | Pretty of Pretty.T
-  | Term of term;
+  | Quote of 'a;
 
 fun is_arg Arg = true
   | is_arg Ignore = true
   | is_arg _ = false;
 
-fun terms_of [] = []
-  | terms_of (Term t :: ms) = t :: terms_of ms
-  | terms_of (_ :: ms) = terms_of ms;
+fun quotes_of [] = []
+  | quotes_of (Quote q :: ms) = q :: quotes_of ms
+  | quotes_of (_ :: ms) = quotes_of ms;
+
+fun args_of [] xs = ([], xs)
+  | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs)
+  | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs
+  | args_of (_ :: ms) xs = args_of ms xs;
 
 val num_args = length o filter is_arg;
 
@@ -71,40 +80,54 @@
 
 (* data kind 'Pure/codegen' *)
 
+type 'a codegen = theory -> (exn option * string) Graph.T ->
+  string -> bool -> 'a -> ((exn option * string) Graph.T * Pretty.T) option;
+
 structure CodegenArgs =
 struct
   val name = "Pure/codegen";
   type T =
-    {codegens : (string * (theory -> (exn option * string) Graph.T -> string ->
-       bool -> term -> ((exn option * string) Graph.T * Pretty.T) option)) list,
-     consts : ((string * typ) * mixfix list) list,
-     types : (string * string) list};
+    {codegens : (string * term codegen) list,
+     tycodegens : (string * typ codegen) list,
+     consts : ((string * typ) * term mixfix list) list,
+     types : (string * typ mixfix list) list};
 
-  val empty = {codegens = [], consts = [], types = []};
+  val empty = {codegens = [], tycodegens = [], consts = [], types = []};
   val copy = I;
   val prep_ext = I;
 
-  fun merge ({codegens = codegens1, consts = consts1, types = types1},
-             {codegens = codegens2, consts = consts2, types = types2}) =
+  fun merge ({codegens = codegens1, tycodegens = tycodegens1, consts = consts1, types = types1},
+             {codegens = codegens2, tycodegens = tycodegens2, consts = consts2, types = types2}) =
     {codegens = rev (merge_alists (rev codegens1) (rev codegens2)),
+     tycodegens = rev (merge_alists (rev tycodegens1) (rev tycodegens2)),
      consts   = merge_alists consts1 consts2,
      types    = merge_alists types1 types2};
 
-  fun print sg (cs:T) = Pretty.writeln
-    (Pretty.strs ("code generators:" :: map fst (#codegens cs)));
+  fun print sg ({codegens, tycodegens, ...} : T) =
+    Pretty.writeln (Pretty.chunks
+      [Pretty.strs ("term code generators:" :: map fst codegens),
+       Pretty.strs ("type code generators:" :: map fst tycodegens)]);
 end;
 
 structure CodegenData = TheoryDataFun(CodegenArgs);
 val print_codegens = CodegenData.print;
 
 
-(**** add new code generator to theory ****)
+(**** add new code generators to theory ****)
 
 fun add_codegen name f thy =
-  let val {codegens, consts, types} = CodegenData.get thy
+  let val {codegens, tycodegens, consts, types} = CodegenData.get thy
   in (case assoc (codegens, name) of
-      None => CodegenData.put {codegens = (name, f)::codegens,
-        consts = consts, types = types} thy
+      None => CodegenData.put {codegens = (name, f) :: codegens,
+        tycodegens = tycodegens, consts = consts, types = types} thy
+    | Some _ => error ("Code generator " ^ name ^ " already declared"))
+  end;
+
+fun add_tycodegen name f thy =
+  let val {codegens, tycodegens, consts, types} = CodegenData.get thy
+  in (case assoc (tycodegens, name) of
+      None => CodegenData.put {tycodegens = (name, f) :: tycodegens,
+        codegens = codegens, consts = consts, types = types} thy
     | Some _ => error ("Code generator " ^ name ^ " already declared"))
   end;
 
@@ -114,7 +137,7 @@
 fun gen_assoc_consts prep_type xs thy = foldl (fn (thy, (s, tyopt, syn)) =>
   let
     val sg = sign_of thy;
-    val {codegens, consts, types} = CodegenData.get thy;
+    val {codegens, tycodegens, consts, types} = CodegenData.get thy;
     val cname = Sign.intern_const sg s;
   in
     (case Sign.const_type sg cname of
@@ -128,6 +151,7 @@
                   end)
          in (case assoc (consts, (cname, T')) of
              None => CodegenData.put {codegens = codegens,
+               tycodegens = tycodegens,
                consts = ((cname, T'), syn) :: consts, types = types} thy
            | Some _ => error ("Constant " ^ cname ^ " already associated with code"))
          end
@@ -141,16 +165,17 @@
 
 fun assoc_types xs thy = foldl (fn (thy, (s, syn)) =>
   let
-    val {codegens, consts, types} = CodegenData.get thy;
+    val {codegens, tycodegens, consts, types} = CodegenData.get thy;
     val tc = Sign.intern_tycon (sign_of thy) s
   in
     (case assoc (types, tc) of
-       None => CodegenData.put {codegens = codegens, consts = consts,
+       None => CodegenData.put {codegens = codegens,
+         tycodegens = tycodegens, consts = consts,
          types = (tc, syn) :: types} thy
      | Some _ => error ("Type " ^ tc ^ " already associated with code"))
   end) (thy, xs);
 
-fun get_assoc_types thy = #types (CodegenData.get thy);
+fun get_assoc_type thy s = assoc (#types (CodegenData.get thy), s);
 
 
 (**** retrieve definition of constant ****)
@@ -214,14 +239,21 @@
   end;
 
 
-(**** invoke suitable code generator for term t ****)
+(**** invoke suitable code generator for term / type ****)
 
-fun invoke_codegen thy gr dep brack t = (case get_first
+fun invoke_codegen thy dep brack (gr, t) = (case get_first
    (fn (_, f) => f thy gr dep brack t) (#codegens (CodegenData.get thy)) of
       None => error ("Unable to generate code for term:\n" ^
         Sign.string_of_term (sign_of thy) t ^ "\nrequired by:\n" ^
         commas (Graph.all_succs gr [dep]))
-    | Some x => x)
+    | Some x => x);
+
+fun invoke_tycodegen thy dep brack (gr, T) = (case get_first
+   (fn (_, f) => f thy gr dep brack T) (#tycodegens (CodegenData.get thy)) of
+      None => error ("Unable to generate code for type:\n" ^
+        Sign.string_of_typ (sign_of thy) T ^ "\nrequired by:\n" ^
+        commas (Graph.all_succs gr [dep]))
+    | Some x => x);
 
 
 (**** code generator for mixfix expressions ****)
@@ -234,12 +266,12 @@
 
 fun pretty_mixfix [] [] _ = []
   | pretty_mixfix (Arg :: ms) (p :: ps) qs = p :: pretty_mixfix ms ps qs
-  | pretty_mixfix (Ignore :: ms) (p :: ps) qs = pretty_mixfix ms ps qs
+  | pretty_mixfix (Ignore :: ms) ps qs = pretty_mixfix ms ps qs
   | pretty_mixfix (Pretty p :: ms) ps qs = p :: pretty_mixfix ms ps qs
-  | pretty_mixfix (Term _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs;
+  | pretty_mixfix (Quote _ :: ms) ps (q :: qs) = q :: pretty_mixfix ms ps qs;
 
 
-(**** default code generator ****)
+(**** default code generators ****)
 
 fun eta_expand t ts i =
   let
@@ -265,18 +297,16 @@
 fun default_codegen thy gr dep brack t =
   let
     val (u, ts) = strip_comb t;
-    fun mapcode brack' gr ts = foldl_map
-      (fn (gr, t) => invoke_codegen thy gr dep brack' t) (gr, ts)
-
+    fun codegens brack = foldl_map (invoke_codegen thy dep brack)
   in (case u of
       Var ((s, i), _) =>
-        let val (gr', ps) = mapcode true gr ts
+        let val (gr', ps) = codegens true (gr, ts)
         in Some (gr', mk_app brack (Pretty.str (s ^
            (if i=0 then "" else string_of_int i))) ps)
         end
 
     | Free (s, _) =>
-        let val (gr', ps) = mapcode true gr ts
+        let val (gr', ps) = codegens true (gr, ts)
         in Some (gr', mk_app brack (Pretty.str s) ps) end
 
     | Const (s, T) =>
@@ -287,11 +317,10 @@
                default_codegen thy gr dep brack (eta_expand u ts i)
              else
                let
-                 val ts1 = take (i, ts);
-                 val ts2 = drop (i, ts);
-                 val (gr1, ps1) = mapcode false gr ts1;
-                 val (gr2, ps2) = mapcode true gr1 ts2;
-                 val (gr3, ps3) = mapcode false gr2 (terms_of ms);
+                 val (ts1, ts2) = args_of ms ts;
+                 val (gr1, ps1) = codegens false (gr, ts1);
+                 val (gr2, ps2) = codegens true (gr1, ts2);
+                 val (gr3, ps3) = codegens false (gr2, quotes_of ms);
                in
                  Some (gr3, mk_app brack (Pretty.block (pretty_mixfix ms ps1 ps3)) ps2)
                end
@@ -302,7 +331,7 @@
              let
                val id = mk_const_id (sign_of thy) s ^ (case k of
                  None => "" | Some i => "_def" ^ string_of_int i);
-               val (gr', ps) = mapcode true gr ts;
+               val (gr', ps) = codegens true (gr, ts);
              in
                Some (Graph.add_edge (id, dep) gr' handle Graph.UNDEF _ =>
                  let
@@ -312,9 +341,10 @@
                      if not (null args) orelse null Ts then (args, rhs) else
                        let val v = Free (new_name rhs "x", hd Ts)
                        in ([v], betapply (rhs, v)) end;
-                   val (gr1, p) = invoke_codegen thy (Graph.add_edge (id, dep)
-                     (Graph.new_node (id, (None, "")) gr')) id false rhs';
-                   val (gr2, xs) = mapcode false gr1 args';
+                   val (gr1, p) = invoke_codegen thy id false
+                     (Graph.add_edge (id, dep)
+                        (Graph.new_node (id, (None, "")) gr'), rhs');
+                   val (gr2, xs) = codegens false (gr1, args');
                  in Graph.map_node id (K (None, Pretty.string_of (Pretty.block
                    (Pretty.str (if null args' then "val " else "fun ") ::
                     separate (Pretty.brk 1) (Pretty.str id :: xs) @
@@ -327,9 +357,9 @@
         val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
         val t = strip_abs_body u
         val bs' = new_names t bs;
-        val (gr1, ps) = mapcode true gr ts;
-        val (gr2, p) = invoke_codegen thy gr1 dep false
-          (subst_bounds (map Free (rev (bs' ~~ Ts)), t));
+        val (gr1, ps) = codegens true (gr, ts);
+        val (gr2, p) = invoke_codegen thy dep false
+          (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
       in
         Some (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @
           [Pretty.str ")"])) ps)
@@ -338,6 +368,20 @@
     | _ => None)
   end;
 
+fun default_tycodegen thy gr dep brack (TVar ((s, i), _)) =
+      Some (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i)))
+  | default_tycodegen thy gr dep brack (TFree (s, _)) = Some (gr, Pretty.str s)
+  | default_tycodegen thy gr dep brack (Type (s, Ts)) =
+      (case assoc (#types (CodegenData.get thy), s) of
+         None => None
+       | Some ms =>
+           let
+             val (gr', ps) = foldl_map
+               (invoke_tycodegen thy dep false) (gr, fst (args_of ms Ts));
+             val (gr'', qs) = foldl_map
+               (invoke_tycodegen thy dep false) (gr', quotes_of ms)
+           in Some (gr'', Pretty.block (pretty_mixfix ms ps qs)) end);
+
 
 fun output_code gr xs = implode (map (snd o Graph.get_node gr)
   (rev (Graph.all_preds gr xs)));
@@ -347,7 +391,8 @@
     val sg = sign_of thy;
     val gr = Graph.new_node ("<Top>", (None, "")) Graph.empty;
     val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
-      (invoke_codegen thy gr "<Top>" false t)) (gr, map (apsnd (prep_term sg)) xs)
+      (invoke_codegen thy "<Top>" false (gr, t)))
+        (gr, map (apsnd (prep_term sg)) xs)
   in
     "structure Generated =\nstruct\n\n" ^
     output_code gr' ["<Top>"] ^
@@ -360,6 +405,9 @@
 val generate_code = gen_generate_code
   (fn sg => term_of o read_cterm sg o rpair TypeInfer.logicT);
 
+
+(**** Interface ****)
+
 fun parse_mixfix rd s =
   (case Scan.finite Symbol.stopper (Scan.repeat
      (   $$ "_" >> K Arg
@@ -368,7 +416,7 @@
       || $$ "{" |-- $$ "*" |-- Scan.repeat1
            (   $$ "'" |-- Scan.one Symbol.not_eof
             || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
-         $$ "*" --| $$ "}" >> (Term o rd o implode)
+         $$ "*" --| $$ "}" >> (Quote o rd o implode)
       || Scan.repeat1
            (   $$ "'" |-- Scan.one Symbol.not_eof
             || Scan.unless ($$ "_" || $$ "?" || $$ "/" || $$ "{" |-- $$ "*")
@@ -383,7 +431,9 @@
   OuterSyntax.command "types_code"
   "associate types with target language types" K.thy_decl
     (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")") >>
-     (Toplevel.theory o assoc_types));
+     (fn xs => Toplevel.theory (fn thy => assoc_types
+       (map (fn (name, mfx) => (name, parse_mixfix
+         (typ_of o read_ctyp (sign_of thy)) mfx)) xs) thy)));
 
 val assoc_constP =
   OuterSyntax.command "consts_code"
@@ -408,7 +458,11 @@
 
 val parsers = [assoc_typeP, assoc_constP, generate_codeP];
 
-val setup = [CodegenData.init, add_codegen "default" default_codegen];
+val setup =
+  [CodegenData.init,
+   add_codegen "default" default_codegen,
+   add_tycodegen "default" default_tycodegen,
+   assoc_types [("fun", parse_mixfix (K dummyT) "(_ ->/ _)")]];
 
 end;