src/Tools/code/code_haskell.ML
changeset 28708 a1a436f09ec6
parent 28687 150a8a1eae1a
child 29135 20b42397e293
     1.1 --- a/src/Tools/code/code_haskell.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Tools/code/code_haskell.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -59,45 +59,45 @@
     1.4        Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
     1.5      fun pr_typscheme tyvars (vs, ty) =
     1.6        Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
     1.7 -    fun pr_term tyvars thm pat vars fxy (IConst c) =
     1.8 -          pr_app tyvars thm pat vars fxy (c, [])
     1.9 -      | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
    1.10 +    fun pr_term tyvars thm vars fxy (IConst c) =
    1.11 +          pr_app tyvars thm vars fxy (c, [])
    1.12 +      | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) =
    1.13            (case Code_Thingol.unfold_const_app t
    1.14 -           of SOME app => pr_app tyvars thm pat vars fxy app
    1.15 +           of SOME app => pr_app tyvars thm vars fxy app
    1.16              | _ =>
    1.17                  brackify fxy [
    1.18 -                  pr_term tyvars thm pat vars NOBR t1,
    1.19 -                  pr_term tyvars thm pat vars BR t2
    1.20 +                  pr_term tyvars thm vars NOBR t1,
    1.21 +                  pr_term tyvars thm vars BR t2
    1.22                  ])
    1.23 -      | pr_term tyvars thm pat vars fxy (IVar v) =
    1.24 +      | pr_term tyvars thm vars fxy (IVar v) =
    1.25            (str o Code_Name.lookup_var vars) v
    1.26 -      | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
    1.27 +      | pr_term tyvars thm vars fxy (t as _ `|-> _) =
    1.28            let
    1.29              val (binds, t') = Code_Thingol.unfold_abs t;
    1.30              fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
    1.31              val (ps, vars') = fold_map pr binds vars;
    1.32 -          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
    1.33 -      | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
    1.34 +          in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
    1.35 +      | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
    1.36            (case Code_Thingol.unfold_const_app t0
    1.37             of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
    1.38                  then pr_case tyvars thm vars fxy cases
    1.39 -                else pr_app tyvars thm pat vars fxy c_ts
    1.40 +                else pr_app tyvars thm vars fxy c_ts
    1.41              | NONE => pr_case tyvars thm vars fxy cases)
    1.42 -    and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    1.43 -     of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
    1.44 +    and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
    1.45 +     of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    1.46        | fingerprint => let
    1.47            val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
    1.48            val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
    1.49              (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
    1.50 -          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
    1.51 +          fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t
    1.52              | pr_term_anno (t, SOME _) ty =
    1.53 -                brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
    1.54 +                brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty];
    1.55          in
    1.56            if needs_annotation then
    1.57              (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
    1.58 -          else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
    1.59 +          else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
    1.60          end
    1.61 -    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons naming
    1.62 +    and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
    1.63      and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
    1.64      and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
    1.65            let
    1.66 @@ -105,12 +105,12 @@
    1.67              fun pr ((pat, ty), t) vars =
    1.68                vars
    1.69                |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
    1.70 -              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
    1.71 +              |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
    1.72              val (ps, vars') = fold_map pr binds vars;
    1.73            in
    1.74              Pretty.block_enclose (
    1.75                str "let {",
    1.76 -              concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
    1.77 +              concat [str "}", str "in", pr_term tyvars thm vars' NOBR t]
    1.78              ) ps
    1.79            end
    1.80        | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
    1.81 @@ -118,10 +118,10 @@
    1.82              fun pr (pat, t) =
    1.83                let
    1.84                  val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
    1.85 -              in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
    1.86 +              in semicolon [p, str "->", pr_term tyvars thm vars' NOBR t] end;
    1.87            in
    1.88              Pretty.block_enclose (
    1.89 -              concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
    1.90 +              concat [str "(case", pr_term tyvars thm vars NOBR td, str "of", str "{"],
    1.91                str "})"
    1.92              ) (map pr bs)
    1.93            end
    1.94 @@ -165,9 +165,9 @@
    1.95                in
    1.96                  semicolon (
    1.97                    (str o deresolve_base) name
    1.98 -                  :: map (pr_term tyvars thm true vars BR) ts
    1.99 +                  :: map (pr_term tyvars thm vars BR) ts
   1.100                    @ str "="
   1.101 -                  @@ pr_term tyvars thm false vars NOBR t
   1.102 +                  @@ pr_term tyvars thm vars NOBR t
   1.103                  )
   1.104                end;
   1.105            in
   1.106 @@ -250,7 +250,7 @@
   1.107               of NONE => semicolon [
   1.108                      (str o deresolve_base) classparam,
   1.109                      str "=",
   1.110 -                    pr_app tyvars thm false init_syms NOBR (c_inst, [])
   1.111 +                    pr_app tyvars thm init_syms NOBR (c_inst, [])
   1.112                    ]
   1.113                | SOME (k, pr) =>
   1.114                    let
   1.115 @@ -266,9 +266,9 @@
   1.116                        (*dictionaries are not relevant at this late stage*)
   1.117                    in
   1.118                      semicolon [
   1.119 -                      pr_term tyvars thm false vars NOBR lhs,
   1.120 +                      pr_term tyvars thm vars NOBR lhs,
   1.121                        str "=",
   1.122 -                      pr_term tyvars thm false vars NOBR rhs
   1.123 +                      pr_term tyvars thm vars NOBR rhs
   1.124                      ]
   1.125                    end;
   1.126            in
   1.127 @@ -463,10 +463,10 @@
   1.128        | pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
   1.129            |> pr_bind NOBR bind
   1.130            |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
   1.131 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   1.132 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
   1.133       of SOME (bind, t') => let
   1.134            val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
   1.135 -          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K (K pr)) thm) pr) (bind :: binds) vars;
   1.136 +          val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
   1.137          in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
   1.138        | NONE => brackify_infix (1, L) fxy
   1.139            [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]