src/Tools/Code/code_printer.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69659 07025152dd80
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      Tools/Code/code_printer.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Generic operations for pretty printing of target language code.
     5 *)
     6 
     7 signature CODE_PRINTER =
     8 sig
     9   type itype = Code_Thingol.itype
    10   type iterm = Code_Thingol.iterm
    11   type const = Code_Thingol.const
    12   type dict = Code_Thingol.dict
    13 
    14   val eqn_error: theory -> thm option -> string -> 'a
    15 
    16   val @@ : 'a * 'a -> 'a list
    17   val @| : 'a list * 'a -> 'a list
    18   val str: string -> Pretty.T
    19   val concat: Pretty.T list -> Pretty.T
    20   val brackets: Pretty.T list -> Pretty.T
    21   val enclose: string -> string -> Pretty.T list -> Pretty.T
    22   val commas: Pretty.T list -> Pretty.T list
    23   val enum: string -> string -> string -> Pretty.T list -> Pretty.T
    24   val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T
    25   val semicolon: Pretty.T list -> Pretty.T
    26   val doublesemicolon: Pretty.T list -> Pretty.T
    27   val indent: int -> Pretty.T -> Pretty.T
    28   val markup_stmt: Code_Symbol.T -> Pretty.T -> Pretty.T
    29   val format: Code_Symbol.T list -> int -> Pretty.T -> string
    30 
    31   type var_ctxt
    32   val make_vars: string list -> var_ctxt
    33   val intro_vars: string list -> var_ctxt -> var_ctxt
    34   val lookup_var: var_ctxt -> string -> string
    35   val intro_base_names: (string -> bool) -> (string -> string)
    36     -> string list -> var_ctxt -> var_ctxt
    37   val intro_base_names_for: (string -> bool) -> (Code_Symbol.T -> string)
    38     -> iterm list -> var_ctxt -> var_ctxt
    39   val aux_params: var_ctxt -> iterm list list -> string list
    40 
    41   type literals
    42   val Literals: { literal_string: string -> string,
    43         literal_numeral: int -> string,
    44         literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    45     -> literals
    46   val literal_string: literals -> string -> string
    47   val literal_numeral: literals -> int -> string
    48   val literal_list: literals -> Pretty.T list -> Pretty.T
    49   val infix_cons: literals -> int * string
    50 
    51   type lrx
    52   val L: lrx
    53   val R: lrx
    54   val X: lrx
    55   type fixity
    56   val BR: fixity
    57   val NOBR: fixity
    58   val INFX: int * lrx -> fixity
    59   val APP: fixity
    60   val brackify: fixity -> Pretty.T list -> Pretty.T
    61   val brackify_infix: int * lrx -> fixity -> Pretty.T * Pretty.T * Pretty.T -> Pretty.T
    62   val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
    63   val gen_applify: bool -> string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
    64   val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
    65   val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
    66 
    67   type raw_const_syntax
    68   val plain_const_syntax: string -> raw_const_syntax
    69   type simple_const_syntax
    70   val simple_const_syntax: simple_const_syntax -> raw_const_syntax
    71   type complex_const_syntax
    72   val complex_const_syntax: complex_const_syntax -> raw_const_syntax
    73   val parse_const_syntax: raw_const_syntax parser
    74   val requires_args: raw_const_syntax -> int
    75   datatype const_printer = Plain_printer of string
    76     | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
    77         -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
    78   type const_syntax = int * const_printer
    79   val prep_const_syntax: theory -> literals
    80     -> string -> raw_const_syntax -> const_syntax
    81   type tyco_syntax
    82   val parse_tyco_syntax: tyco_syntax parser
    83   val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    84     -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    85     -> (string -> const_syntax option)
    86     -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    87   val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    88     -> thm option -> fixity
    89     -> iterm -> var_ctxt -> Pretty.T * var_ctxt
    90 
    91   type identifiers
    92   type printings
    93   type data
    94   val empty_data: data
    95   val map_data: (string list * identifiers * printings
    96     -> string list * identifiers * printings)
    97     -> data -> data
    98   val merge_data: data * data -> data
    99   val the_reserved: data -> string list;
   100   val the_identifiers: data -> identifiers;
   101   val the_printings: data -> printings;
   102 end;
   103 
   104 structure Code_Printer : CODE_PRINTER =
   105 struct
   106 
   107 open Basic_Code_Symbol;
   108 open Code_Thingol;
   109 
   110 (** generic nonsense *)
   111 
   112 fun eqn_error thy (SOME thm) s =
   113       error (s ^ ",\nin equation " ^ Thm.string_of_thm_global thy thm)
   114   | eqn_error _ NONE s = error s;
   115 
   116 val code_presentationN = "code_presentation";
   117 val stmt_nameN = "stmt_name";
   118 val _ = Markup.add_mode code_presentationN YXML.output_markup;
   119 
   120 
   121 (** assembling and printing text pieces **)
   122 
   123 infixr 5 @@;
   124 infixr 5 @|;
   125 fun x @@ y = [x, y];
   126 fun xs @| y = xs @ [y];
   127 fun with_no_print_mode f = Print_Mode.setmp [] f;
   128 val str = with_no_print_mode Pretty.str;
   129 val concat = Pretty.block o Pretty.breaks;
   130 val commas = with_no_print_mode Pretty.commas;
   131 fun enclose l r = with_no_print_mode (Pretty.enclose l r);
   132 val brackets = enclose "(" ")" o Pretty.breaks;
   133 fun enum sep l r = with_no_print_mode (Pretty.enum sep l r);
   134 fun enum_default default sep l r [] = str default
   135   | enum_default default sep l r xs = enum sep l r xs;
   136 fun semicolon ps = Pretty.block [concat ps, str ";"];
   137 fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   138 fun indent i = with_no_print_mode (Pretty.indent i);
   139 
   140 fun with_presentation_marker f = Print_Mode.setmp [code_presentationN] f;
   141 
   142 fun markup_stmt sym = with_presentation_marker
   143   (Pretty.mark (code_presentationN, [(stmt_nameN, Code_Symbol.marker sym)]));
   144 
   145 fun filter_presentation [] tree =
   146       Buffer.empty
   147       |> fold XML.add_content tree
   148   | filter_presentation presentation_syms tree =
   149       let
   150         val presentation_idents = map Code_Symbol.marker presentation_syms
   151         fun is_selected (name, attrs) =
   152           name = code_presentationN
   153           andalso member (op =) presentation_idents (the (Properties.get attrs stmt_nameN));
   154         fun add_content_with_space tree (is_first, buf) =
   155           buf
   156           |> not is_first ? Buffer.add "\n\n"
   157           |> XML.add_content tree
   158           |> pair false;
   159         fun filter (XML.Elem (name_attrs, xs)) =
   160               fold (if is_selected name_attrs then add_content_with_space else filter) xs
   161           | filter (XML.Text _) = I;
   162       in snd (fold filter tree (true, Buffer.empty)) end;
   163 
   164 fun format presentation_names width =
   165   with_presentation_marker (Pretty.string_of_margin width)
   166   #> YXML.parse_body
   167   #> filter_presentation presentation_names
   168   #> Buffer.add "\n"
   169   #> Buffer.content;
   170 
   171 
   172 (** names and variable name contexts **)
   173 
   174 type var_ctxt = string Symtab.table * Name.context;
   175 
   176 fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
   177   Name.make_context names);
   178 
   179 fun intro_vars names (namemap, namectxt) =
   180   let
   181     val (names', namectxt') = fold_map Name.variant names namectxt;
   182     val namemap' = fold2 (curry Symtab.update) names names' namemap;
   183   in (namemap', namectxt') end;
   184 
   185 fun lookup_var (namemap, _) name =
   186   case Symtab.lookup namemap name of
   187     SOME name' => name'
   188   | NONE => error ("Invalid name in context: " ^ quote name);
   189 
   190 fun aux_params vars lhss =
   191   let
   192     fun fish_param _ (w as SOME _) = w
   193       | fish_param (IVar (SOME v)) NONE = SOME v
   194       | fish_param _ NONE = NONE;
   195     fun fillup_param _ (_, SOME v) = v
   196       | fillup_param x (i, NONE) = x ^ string_of_int i;
   197     val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
   198     val x = singleton (Name.variant_list (map_filter I fished1)) "x";
   199     val fished2 = map_index (fillup_param x) fished1;
   200     val (fished3, _) = fold_map Name.variant fished2 Name.context;
   201     val vars' = intro_vars fished3 vars;
   202   in map (lookup_var vars') fished3 end;
   203 
   204 fun intro_base_names no_syntax deresolve =
   205   map_filter (fn name => if no_syntax name then
   206       let val name' = deresolve name in
   207         if Long_Name.is_qualified name' then NONE else SOME name'
   208       end else NONE)
   209   #> intro_vars;
   210 
   211 fun intro_base_names_for no_syntax deresolve ts =
   212   []
   213   |> fold Code_Thingol.add_constsyms ts 
   214   |> intro_base_names (fn Constant const => no_syntax const | _ => true) deresolve;
   215 
   216 
   217 (** pretty literals **)
   218 
   219 datatype literals = Literals of {
   220   literal_string: string -> string,
   221   literal_numeral: int -> string,
   222   literal_list: Pretty.T list -> Pretty.T,
   223   infix_cons: int * string
   224 };
   225 
   226 fun dest_Literals (Literals lits) = lits;
   227 
   228 val literal_string = #literal_string o dest_Literals;
   229 val literal_numeral = #literal_numeral o dest_Literals;
   230 val literal_list = #literal_list o dest_Literals;
   231 val infix_cons = #infix_cons o dest_Literals;
   232 
   233 
   234 (** syntax printer **)
   235 
   236 (* binding priorities *)
   237 
   238 datatype lrx = L | R | X;
   239 
   240 datatype fixity =
   241     BR
   242   | NOBR
   243   | INFX of (int * lrx);
   244 
   245 val APP = INFX (~1, L);
   246 
   247 fun fixity_lrx L L = false
   248   | fixity_lrx R R = false
   249   | fixity_lrx _ _ = true;
   250 
   251 fun fixity NOBR _ = false
   252   | fixity _ NOBR = false
   253   | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
   254       pr < pr_ctxt
   255       orelse pr = pr_ctxt
   256         andalso fixity_lrx lr lr_ctxt
   257       orelse pr_ctxt = ~1
   258   | fixity BR (INFX _) = false
   259   | fixity _ _ = true;
   260 
   261 fun gen_brackify _ [p] = p
   262   | gen_brackify true (ps as _::_) = enclose "(" ")" ps
   263   | gen_brackify false (ps as _::_) = Pretty.block ps;
   264 
   265 fun brackify fxy_ctxt =
   266   gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
   267 
   268 fun brackify_infix infx fxy_ctxt (l, m, r) =
   269   gen_brackify (fixity (INFX infx) fxy_ctxt) [l, str " ", m, Pretty.brk 1, r];
   270 
   271 fun brackify_block fxy_ctxt p1 ps p2 =
   272   let val p = Pretty.block_enclose (p1, p2) ps
   273   in if fixity BR fxy_ctxt
   274     then enclose "(" ")" [p]
   275     else p
   276   end;
   277 
   278 fun gen_applify strict opn cls f fxy_ctxt p [] =
   279       if strict
   280       then gen_brackify (fixity BR fxy_ctxt) [p, str (opn ^ cls)]
   281       else p
   282   | gen_applify strict opn cls f fxy_ctxt p ps =
   283       gen_brackify (fixity BR fxy_ctxt) (p @@ enum "," opn cls (map f ps));
   284 
   285 fun applify opn = gen_applify false opn;
   286 
   287 fun tuplify _ _ [] = NONE
   288   | tuplify print fxy [x] = SOME (print fxy x)
   289   | tuplify print _ xs = SOME (enum "," "(" ")" (map (print NOBR) xs));
   290 
   291 
   292 (* generic syntax *)
   293 
   294 type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
   295   -> fixity -> (iterm * itype) list -> Pretty.T);
   296 
   297 type complex_const_syntax = int * (literals
   298   -> (var_ctxt -> fixity -> iterm -> Pretty.T)
   299     -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
   300 
   301 datatype raw_const_syntax = plain_const_syntax of string
   302   | complex_const_syntax of complex_const_syntax;
   303 
   304 fun simple_const_syntax syn =
   305   complex_const_syntax
   306     (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
   307 
   308 fun requires_args (plain_const_syntax _) = 0
   309   | requires_args (complex_const_syntax (k, _)) = k;
   310 
   311 datatype const_printer = Plain_printer of string
   312   | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
   313       -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
   314 
   315 type const_syntax = int * const_printer;
   316 
   317 fun prep_const_syntax thy literals c (plain_const_syntax s) =
   318       (Code.args_number thy c, Plain_printer s)
   319   | prep_const_syntax thy literals c (complex_const_syntax (n, f))=
   320       (n, Complex_printer (f literals));
   321 
   322 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
   323     (app as ({ sym, dom, ... }, ts)) =
   324   case sym of
   325     Constant const => (case const_syntax const of
   326       NONE => brackify fxy (print_app_expr some_thm vars app)
   327     | SOME (_, Plain_printer s) =>
   328         brackify fxy (str s :: map (print_term some_thm vars BR) ts)
   329     | SOME (k, Complex_printer print) =>
   330         let
   331           fun print' fxy ts =
   332             print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
   333         in
   334           if k = length ts
   335           then print' fxy ts
   336           else if k < length ts
   337           then case chop k ts of (ts1, ts2) =>
   338             brackify fxy (print' APP ts1 :: map (print_term some_thm vars BR) ts2)
   339           else print_term some_thm vars fxy (Code_Thingol.eta_expand k app)
   340         end)
   341   | _ => brackify fxy (print_app_expr some_thm vars app);
   342 
   343 fun gen_print_bind print_term thm (fxy : fixity) pat vars =
   344   let
   345     val vs = Code_Thingol.fold_varnames (insert (op =)) pat [];
   346     val vars' = intro_vars vs vars;
   347   in (print_term thm vars' fxy pat, vars') end;
   348 
   349 type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
   350   -> fixity -> itype list -> Pretty.T);
   351 
   352 
   353 (* mixfix syntax *)
   354 
   355 datatype 'a mixfix =
   356     Arg of fixity
   357   | String of string
   358   | Break;
   359 
   360 fun printer_of_mixfix prep_arg (fixity_this, mfx) =
   361   let
   362     fun is_arg (Arg _) = true
   363       | is_arg _ = false;
   364     val i = (length o filter is_arg) mfx;
   365     fun fillin _ [] [] =
   366           []
   367       | fillin print (Arg fxy :: mfx) (a :: args) =
   368           (print fxy o prep_arg) a :: fillin print mfx args
   369       | fillin print (String s :: mfx) args =
   370           str s :: fillin print mfx args
   371       | fillin print (Break :: mfx) args =
   372           Pretty.brk 1 :: fillin print mfx args;
   373   in
   374     (i, fn print => fn fixity_ctxt => fn args =>
   375       gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args))
   376   end;
   377 
   378 fun read_infix (fixity_this, i) s =
   379   let
   380     val l = case fixity_this of L => INFX (i, L) | _ => INFX (i, X);
   381     val r = case fixity_this of R => INFX (i, R) | _ => INFX (i, X);
   382   in
   383     (INFX (i, fixity_this), [Arg l, String " ", String s, Break, Arg r])
   384   end;
   385 
   386 fun read_mixfix s =
   387   let
   388     val sym_any = Scan.one Symbol.not_eof;
   389     val parse = Scan.optional ($$ "!" >> K NOBR) BR -- Scan.repeat (
   390          ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
   391       || ($$ "_" >> K (Arg BR))
   392       || ($$ "/" |-- Scan.repeat ($$ " ") >> (K Break))
   393       || (Scan.repeat1
   394            (   $$ "'" |-- sym_any
   395             || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
   396                  sym_any) >> (String o implode)));
   397     fun err s (_, NONE) = (fn () => "malformed mixfix annotation: " ^ quote s)
   398       | err _ (_, SOME msg) = msg;
   399   in
   400     case Scan.finite Symbol.stopper parse (Symbol.explode s) of
   401         (fixity_mixfix, []) => fixity_mixfix
   402       | _ => Scan.!! (err s) Scan.fail ()
   403   end;
   404 
   405 val parse_fixity =
   406   (\<^keyword>\<open>infix\<close> >> K X) || (\<^keyword>\<open>infixl\<close> >> K L) || (\<^keyword>\<open>infixr\<close> >> K R)
   407 
   408 fun parse_mixfix x =
   409   (Parse.string >> read_mixfix
   410   || parse_fixity -- Parse.nat -- Parse.string
   411      >> (fn ((fixity, i), s) => read_infix (fixity, i) s)) x;
   412 
   413 fun syntax_of_mixfix of_plain of_printer prep_arg (BR, [String s]) = of_plain s
   414   | syntax_of_mixfix of_plain of_printer prep_arg (fixity, mfx) =
   415       of_printer (printer_of_mixfix prep_arg (fixity, mfx));
   416 
   417 fun parse_tyco_syntax x =
   418   (parse_mixfix >> syntax_of_mixfix (fn s => (0, (K o K o K o str) s)) I I) x;
   419 
   420 val parse_const_syntax =
   421   parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
   422 
   423 
   424 (** custom data structure **)
   425 
   426 type identifiers = (string list * string, string list * string, string list * string, string list * string,
   427   string list * string, string list * string) Code_Symbol.data;
   428 type printings = (const_syntax, tyco_syntax, string, unit, unit,
   429     (Pretty.T * Code_Symbol.T list)) Code_Symbol.data;
   430 
   431 datatype data = Data of { reserved: string list, identifiers: identifiers,
   432   printings: printings };
   433 
   434 fun make_data (reserved, identifiers, printings) =
   435   Data { reserved = reserved, identifiers = identifiers, printings = printings };
   436 val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
   437 fun map_data f (Data { reserved, identifiers, printings }) =
   438   make_data (f (reserved, identifiers, printings));
   439 fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
   440     Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
   441   make_data (merge (op =) (reserved1, reserved2),
   442     Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
   443 
   444 fun the_reserved (Data { reserved, ... }) = reserved;
   445 fun the_identifiers (Data { identifiers , ... }) = identifiers;
   446 fun the_printings (Data { printings, ... }) = printings;
   447 
   448 
   449 end; (*struct*)