more abstract declaration of unqualified constant names in code printing context
authorhaftmann
Sat Jan 25 23:50:49 2014 +0100 (2014-01-25)
changeset 551452bb3cd36bcf7
parent 55144 de95c97efab3
child 55146 525309c2e4ee
more abstract declaration of unqualified constant names in code printing context
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 22:18:20 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -136,10 +136,9 @@
     1.4                );
     1.5              fun print_eqn ((ts, t), (some_thm, _)) =
     1.6                let
     1.7 -                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
     1.8                  val vars = reserved
     1.9 -                  |> intro_base_names
    1.10 -                      (is_none o const_syntax) deresolve consts
    1.11 +                  |> intro_base_names_for (is_none o const_syntax)
    1.12 +                      deresolve (t :: ts)
    1.13                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
    1.14                        (insert (op =)) ts []);
    1.15                in
     2.1 --- a/src/Tools/Code/code_ml.ML	Sat Jan 25 22:18:20 2014 +0100
     2.2 +++ b/src/Tools/Code/code_ml.ML	Sat Jan 25 23:50:49 2014 +0100
     2.3 @@ -178,10 +178,9 @@
     2.4            let
     2.5              fun print_eqn definer ((ts, t), (some_thm, _)) =
     2.6                let
     2.7 -                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
     2.8                  val vars = reserved
     2.9 -                  |> intro_base_names
    2.10 -                       (is_none o const_syntax) deresolve consts
    2.11 +                  |> intro_base_names_for (is_none o const_syntax)
    2.12 +                       deresolve (t :: ts)
    2.13                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
    2.14                         (insert (op =)) ts []);
    2.15                  val prolog = if needs_typ then
    2.16 @@ -470,10 +469,9 @@
    2.17            let
    2.18              fun print_eqn ((ts, t), (some_thm, _)) =
    2.19                let
    2.20 -                val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    2.21                  val vars = reserved
    2.22 -                  |> intro_base_names
    2.23 -                      (is_none o const_syntax) deresolve consts
    2.24 +                  |> intro_base_names_for (is_none o const_syntax)
    2.25 +                      deresolve (t :: ts)
    2.26                    |> intro_vars ((fold o Code_Thingol.fold_varnames)
    2.27                        (insert (op =)) ts []);
    2.28                in concat [
    2.29 @@ -484,10 +482,9 @@
    2.30                ] end;
    2.31              fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
    2.32                    let
    2.33 -                    val consts = fold Code_Thingol.add_constnames (t :: ts) [];
    2.34                      val vars = reserved
    2.35 -                      |> intro_base_names
    2.36 -                          (is_none o const_syntax) deresolve consts
    2.37 +                      |> intro_base_names_for (is_none o const_syntax)
    2.38 +                          deresolve (t :: ts)
    2.39                        |> intro_vars ((fold o Code_Thingol.fold_varnames)
    2.40                            (insert (op =)) ts []);
    2.41                    in
    2.42 @@ -510,10 +507,9 @@
    2.43                    )
    2.44                | print_eqns _ (eqs as eq :: eqs') =
    2.45                    let
    2.46 -                    val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) [];
    2.47                      val vars = reserved
    2.48 -                      |> intro_base_names
    2.49 -                          (is_none o const_syntax) deresolve consts;
    2.50 +                      |> intro_base_names_for (is_none o const_syntax)
    2.51 +                           deresolve (map (snd o fst) eqs)
    2.52                      val dummy_parms = (map str o aux_params vars o map (fst o fst)) eqs;
    2.53                    in
    2.54                      Pretty.block (
     3.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 22:18:20 2014 +0100
     3.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     3.3 @@ -36,6 +36,8 @@
     3.4    val lookup_var: var_ctxt -> string -> string
     3.5    val intro_base_names: (string -> bool) -> (string -> string)
     3.6      -> string list -> var_ctxt -> var_ctxt
     3.7 +  val intro_base_names_for: (string -> bool) -> (string -> string)
     3.8 +    -> iterm list -> var_ctxt -> var_ctxt
     3.9    val aux_params: var_ctxt -> iterm list list -> string list
    3.10  
    3.11    type literals
    3.12 @@ -187,12 +189,17 @@
    3.13      val vars' = intro_vars fished3 vars;
    3.14    in map (lookup_var vars') fished3 end;
    3.15  
    3.16 -fun intro_base_names no_syntax deresolve names = names
    3.17 -  |> map_filter (fn name => if no_syntax name then
    3.18 +fun intro_base_names no_syntax deresolve =
    3.19 +  map_filter (fn name => if no_syntax name then
    3.20        let val name' = deresolve name in
    3.21          if Long_Name.is_qualified name' then NONE else SOME name'
    3.22        end else NONE)
    3.23 -  |> intro_vars;
    3.24 +  #> intro_vars;
    3.25 +
    3.26 +fun intro_base_names_for no_syntax deresolve ts =
    3.27 +  []
    3.28 +  |> fold Code_Thingol.add_constnames ts 
    3.29 +  |> intro_base_names no_syntax deresolve;
    3.30  
    3.31  
    3.32  (** pretty literals **)
     4.1 --- a/src/Tools/Code/code_scala.ML	Sat Jan 25 22:18:20 2014 +0100
     4.2 +++ b/src/Tools/Code/code_scala.ML	Sat Jan 25 23:50:49 2014 +0100
     4.3 @@ -167,11 +167,9 @@
     4.4              val simple = case eqs
     4.5               of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
     4.6                | _ => false;
     4.7 -            val consts = fold Code_Thingol.add_constnames
     4.8 -              (map (snd o fst) eqs) [];
     4.9              val vars1 = reserved
    4.10 -              |> intro_base_names
    4.11 -                   (is_none o const_syntax) deresolve consts
    4.12 +              |> intro_base_names_for (is_none o const_syntax)
    4.13 +                   deresolve (map (snd o fst) eqs);
    4.14              val params = if simple
    4.15                then (map (fn IVar (SOME x) => x) o fst o fst o hd) eqs
    4.16                else aux_params vars1 (map (fst o fst) eqs);