src/Tools/Code/code_printer.ML
changeset 32908 9aa8dfef16ff
parent 32091 30e2ffbba718
child 32913 3e9809678574
     1.1 --- a/src/Tools/Code/code_printer.ML	Mon Oct 12 09:25:27 2009 +0200
     1.2 +++ b/src/Tools/Code/code_printer.ML	Mon Oct 12 12:19:19 2009 +0200
     1.3 @@ -6,6 +6,11 @@
     1.4  
     1.5  signature CODE_PRINTER =
     1.6  sig
     1.7 +  type itype = Code_Thingol.itype
     1.8 +  type iterm = Code_Thingol.iterm
     1.9 +  type const = Code_Thingol.const
    1.10 +  type dict = Code_Thingol.dict
    1.11 +
    1.12    val nerror: thm -> string -> 'a
    1.13  
    1.14    val @@ : 'a * 'a -> 'a list
    1.15 @@ -22,6 +27,7 @@
    1.16    val make_vars: string list -> var_ctxt
    1.17    val intro_vars: string list -> var_ctxt -> var_ctxt
    1.18    val lookup_var: var_ctxt -> string -> string
    1.19 +  val aux_params: var_ctxt -> iterm list list -> string list
    1.20  
    1.21    type literals
    1.22    val Literals: { literal_char: string -> string, literal_string: string -> string,
    1.23 @@ -47,10 +53,6 @@
    1.24    val brackify_infix: int * lrx -> fixity -> Pretty.T list -> Pretty.T
    1.25    val brackify_block: fixity -> Pretty.T -> Pretty.T list -> Pretty.T -> Pretty.T
    1.26  
    1.27 -  type itype = Code_Thingol.itype
    1.28 -  type iterm = Code_Thingol.iterm
    1.29 -  type const = Code_Thingol.const
    1.30 -  type dict = Code_Thingol.dict
    1.31    type tyco_syntax
    1.32    type const_syntax
    1.33    type proto_const_syntax
    1.34 @@ -118,6 +120,20 @@
    1.35  val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
    1.36  val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    1.37  
    1.38 +fun aux_params vars lhss =
    1.39 +  let
    1.40 +    fun fish_param _ (w as SOME _) = w
    1.41 +      | fish_param (IVar (SOME v)) NONE = SOME v
    1.42 +      | fish_param _ NONE = NONE;
    1.43 +    fun fillup_param _ (_, SOME v) = v
    1.44 +      | fillup_param x (i, NONE) = x ^ string_of_int i;
    1.45 +    val fished1 = fold (map2 fish_param) lhss (replicate (length (hd lhss)) NONE);
    1.46 +    val x = Name.variant (map_filter I fished1) "x";
    1.47 +    val fished2 = map_index (fillup_param x) fished1;
    1.48 +    val (fished3, _) = Name.variants fished2 Name.context;
    1.49 +    val vars' = intro_vars fished3 vars;
    1.50 +  in map (lookup_var vars') fished3 end;
    1.51 +
    1.52  
    1.53  (** pretty literals **)
    1.54