src/Tools/code/code_ml.ML
changeset 28708 a1a436f09ec6
parent 28705 c77a9f5672f8
child 28724 4656aacba2bc
     1.1 --- a/src/Tools/code/code_ml.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Tools/code/code_ml.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -83,40 +83,40 @@
     1.4           of NONE => pr_tycoexpr fxy (tyco, tys)
     1.5            | SOME (i, pr) => pr pr_typ fxy tys)
     1.6        | pr_typ fxy (ITyVar v) = str ("'" ^ v);
     1.7 -    fun pr_term thm pat vars fxy (IConst c) =
     1.8 -          pr_app thm pat vars fxy (c, [])
     1.9 -      | pr_term thm pat vars fxy (IVar v) =
    1.10 +    fun pr_term thm vars fxy (IConst c) =
    1.11 +          pr_app thm vars fxy (c, [])
    1.12 +      | pr_term thm vars fxy (IVar v) =
    1.13            str (Code_Name.lookup_var vars v)
    1.14 -      | pr_term thm pat vars fxy (t as t1 `$ t2) =
    1.15 +      | pr_term thm vars fxy (t as t1 `$ t2) =
    1.16            (case Code_Thingol.unfold_const_app t
    1.17 -           of SOME c_ts => pr_app thm pat vars fxy c_ts
    1.18 +           of SOME c_ts => pr_app thm vars fxy c_ts
    1.19              | NONE =>
    1.20 -                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
    1.21 -      | pr_term thm pat vars fxy (t as _ `|-> _) =
    1.22 +                brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
    1.23 +      | pr_term thm vars fxy (t as _ `|-> _) =
    1.24            let
    1.25              val (binds, t') = Code_Thingol.unfold_abs t;
    1.26              fun pr ((v, pat), ty) =
    1.27                pr_bind thm NOBR ((SOME v, pat), ty)
    1.28                #>> (fn p => concat [str "fn", p, str "=>"]);
    1.29              val (ps, vars') = fold_map pr binds vars;
    1.30 -          in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
    1.31 -      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
    1.32 +          in brackets (ps @ [pr_term thm vars' NOBR t']) end
    1.33 +      | pr_term thm vars fxy (ICase (cases as (_, t0))) =
    1.34            (case Code_Thingol.unfold_const_app t0
    1.35             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    1.36                  then pr_case thm vars fxy cases
    1.37 -                else pr_app thm pat vars fxy c_ts
    1.38 +                else pr_app thm vars fxy c_ts
    1.39              | NONE => pr_case thm vars fxy cases)
    1.40 -    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
    1.41 +    and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
    1.42        if is_cons c then let
    1.43          val k = length tys
    1.44        in if k < 2 then 
    1.45 -        (str o deresolve) c :: map (pr_term thm pat vars BR) ts
    1.46 +        (str o deresolve) c :: map (pr_term thm vars BR) ts
    1.47        else if k = length ts then
    1.48 -        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
    1.49 -      else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
    1.50 +        [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm vars NOBR) ts)]
    1.51 +      else [pr_term thm vars BR (Code_Thingol.eta_expand k app)] end else
    1.52          (str o deresolve) c
    1.53 -          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
    1.54 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
    1.55 +          :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts
    1.56 +    and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
    1.57      and pr_bind' ((NONE, NONE), _) = str "_"
    1.58        | pr_bind' ((SOME v, NONE), _) = str v
    1.59        | pr_bind' ((NONE, SOME p), _) = p
    1.60 @@ -128,12 +128,12 @@
    1.61              fun pr ((pat, ty), t) vars =
    1.62                vars
    1.63                |> pr_bind thm NOBR ((NONE, SOME pat), ty)
    1.64 -              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
    1.65 +              |>> (fn p => semicolon [str "val", p, str "=", pr_term thm vars NOBR t])
    1.66              val (ps, vars') = fold_map pr binds vars;
    1.67            in
    1.68              Pretty.chunks [
    1.69                [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
    1.70 -              [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
    1.71 +              [str ("in"), Pretty.fbrk, pr_term thm vars' NOBR t'] |> Pretty.block,
    1.72                str ("end")
    1.73              ]
    1.74            end
    1.75 @@ -143,12 +143,12 @@
    1.76                let
    1.77                  val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
    1.78                in
    1.79 -                concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
    1.80 +                concat [str delim, p, str "=>", pr_term thm vars' NOBR t]
    1.81                end;
    1.82            in
    1.83              (Pretty.enclose "(" ")" o single o brackify fxy) (
    1.84                str "case"
    1.85 -              :: pr_term thm false vars NOBR td
    1.86 +              :: pr_term thm vars NOBR td
    1.87                :: pr "of" b
    1.88                :: map (pr "|") bs
    1.89              )
    1.90 @@ -209,8 +209,8 @@
    1.91                               then [str ":", pr_typ NOBR ty]
    1.92                               else
    1.93                                 pr_tyvar_dicts vs_dict
    1.94 -                               @ map (pr_term thm true vars BR) ts)
    1.95 -                       @ [str "=", pr_term thm false vars NOBR t]
    1.96 +                               @ map (pr_term thm vars BR) ts)
    1.97 +                       @ [str "=", pr_term thm vars NOBR t]
    1.98                          )
    1.99                        end
   1.100                    in
   1.101 @@ -303,7 +303,7 @@
   1.102                concat [
   1.103                  (str o pr_label_classparam) classparam,
   1.104                  str "=",
   1.105 -                pr_app thm false reserved_names NOBR (c_inst, [])
   1.106 +                pr_app thm reserved_names NOBR (c_inst, [])
   1.107                ];
   1.108            in
   1.109              semicolon ([
   1.110 @@ -376,38 +376,38 @@
   1.111           of NONE => pr_tycoexpr fxy (tyco, tys)
   1.112            | SOME (i, pr) => pr pr_typ fxy tys)
   1.113        | pr_typ fxy (ITyVar v) = str ("'" ^ v);
   1.114 -    fun pr_term thm pat vars fxy (IConst c) =
   1.115 -          pr_app thm pat vars fxy (c, [])
   1.116 -      | pr_term thm pat vars fxy (IVar v) =
   1.117 +    fun pr_term thm vars fxy (IConst c) =
   1.118 +          pr_app thm vars fxy (c, [])
   1.119 +      | pr_term thm vars fxy (IVar v) =
   1.120            str (Code_Name.lookup_var vars v)
   1.121 -      | pr_term thm pat vars fxy (t as t1 `$ t2) =
   1.122 +      | pr_term thm vars fxy (t as t1 `$ t2) =
   1.123            (case Code_Thingol.unfold_const_app t
   1.124 -           of SOME c_ts => pr_app thm pat vars fxy c_ts
   1.125 +           of SOME c_ts => pr_app thm vars fxy c_ts
   1.126              | NONE =>
   1.127 -                brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
   1.128 -      | pr_term thm pat vars fxy (t as _ `|-> _) =
   1.129 +                brackify fxy [pr_term thm vars NOBR t1, pr_term thm vars BR t2])
   1.130 +      | pr_term thm vars fxy (t as _ `|-> _) =
   1.131            let
   1.132              val (binds, t') = Code_Thingol.unfold_abs t;
   1.133              fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
   1.134              val (ps, vars') = fold_map pr binds vars;
   1.135 -          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
   1.136 -      | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   1.137 +          in brackets (str "fun" :: ps @ str "->" @@ pr_term thm vars' NOBR t') end
   1.138 +      | pr_term thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
   1.139             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
   1.140                  then pr_case thm vars fxy cases
   1.141 -                else pr_app thm pat vars fxy c_ts
   1.142 +                else pr_app thm vars fxy c_ts
   1.143              | NONE => pr_case thm vars fxy cases)
   1.144 -    and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
   1.145 +    and pr_app' thm vars (app as ((c, (iss, tys)), ts)) =
   1.146        if is_cons c then
   1.147          if length tys = length ts
   1.148          then case ts
   1.149           of [] => [(str o deresolve) c]
   1.150 -          | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
   1.151 +          | [t] => [(str o deresolve) c, pr_term thm vars BR t]
   1.152            | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
   1.153 -                    (map (pr_term thm pat vars NOBR) ts)]
   1.154 -        else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
   1.155 +                    (map (pr_term thm vars NOBR) ts)]
   1.156 +        else [pr_term thm vars BR (Code_Thingol.eta_expand (length tys) app)]
   1.157        else (str o deresolve) c
   1.158 -        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
   1.159 -    and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons naming thm pat vars
   1.160 +        :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm vars BR) ts)
   1.161 +    and pr_app thm vars = gen_pr_app pr_app' pr_term syntax_const naming thm vars
   1.162      and pr_bind' ((NONE, NONE), _) = str "_"
   1.163        | pr_bind' ((SOME v, NONE), _) = str v
   1.164        | pr_bind' ((NONE, SOME p), _) = p
   1.165 @@ -420,19 +420,19 @@
   1.166                vars
   1.167                |> pr_bind thm NOBR ((NONE, SOME pat), ty)
   1.168                |>> (fn p => concat
   1.169 -                  [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
   1.170 +                  [str "let", p, str "=", pr_term thm vars NOBR t, str "in"])
   1.171              val (ps, vars') = fold_map pr binds vars;
   1.172 -          in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
   1.173 +          in Pretty.chunks (ps @| pr_term thm vars' NOBR t') end
   1.174        | pr_case thm vars fxy (((td, ty), b::bs), _) =
   1.175            let
   1.176              fun pr delim (pat, t) =
   1.177                let
   1.178                  val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
   1.179 -              in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
   1.180 +              in concat [str delim, p, str "->", pr_term thm vars' NOBR t] end;
   1.181            in
   1.182              (Pretty.enclose "(" ")" o single o brackify fxy) (
   1.183                str "match"
   1.184 -              :: pr_term thm false vars NOBR td
   1.185 +              :: pr_term thm vars NOBR td
   1.186                :: pr "with" b
   1.187                :: map (pr "|") bs
   1.188              )
   1.189 @@ -464,9 +464,9 @@
   1.190                    |> Code_Name.intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
   1.191                        (insert (op =)) ts []);
   1.192                in concat [
   1.193 -                (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
   1.194 +                (Pretty.block o Pretty.commas) (map (pr_term thm vars NOBR) ts),
   1.195                  str "->",
   1.196 -                pr_term thm false vars NOBR t
   1.197 +                pr_term thm vars NOBR t
   1.198                ] end;
   1.199              fun pr_eqs name ty [] =
   1.200                    let
   1.201 @@ -493,9 +493,9 @@
   1.202                            (insert (op =)) ts []);
   1.203                    in
   1.204                      concat (
   1.205 -                      map (pr_term thm true vars BR) ts
   1.206 +                      map (pr_term thm vars BR) ts
   1.207                        @ str "="
   1.208 -                      @@ pr_term thm false vars NOBR t
   1.209 +                      @@ pr_term thm vars NOBR t
   1.210                      )
   1.211                    end
   1.212                | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
   1.213 @@ -615,7 +615,7 @@
   1.214                concat [
   1.215                  (str o deresolve) classparam,
   1.216                  str "=",
   1.217 -                pr_app thm false reserved_names NOBR (c_inst, [])
   1.218 +                pr_app thm reserved_names NOBR (c_inst, [])
   1.219                ];
   1.220            in
   1.221              concat (