src/Tools/Code/code_haskell.ML
changeset 55147 bce3dbc11f95
parent 55145 2bb3cd36bcf7
child 55148 7e1b7cb54114
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -37,8 +37,11 @@
     1.4  fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     1.5      reserved deresolve deriving_show =
     1.6    let
     1.7 +    val deresolve_const = deresolve o Code_Symbol.Constant;
     1.8 +    val deresolve_tyco = deresolve o Code_Symbol.Type_Constructor;
     1.9 +    val deresolve_class = deresolve o Code_Symbol.Type_Class;
    1.10      fun class_name class = case class_syntax class
    1.11 -     of NONE => deresolve class
    1.12 +     of NONE => deresolve_class class
    1.13        | SOME class => class;
    1.14      fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
    1.15       of [] => []
    1.16 @@ -53,7 +56,7 @@
    1.17      fun print_tyco_expr tyvars fxy (tyco, tys) =
    1.18        brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
    1.19      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.20 -         of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
    1.21 +         of NONE => print_tyco_expr tyvars fxy (deresolve_tyco tyco, tys)
    1.22            | SOME (_, print) => print (print_typ tyvars) fxy tys)
    1.23        | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    1.24      fun print_typdecl tyvars (tyco, vs) =
    1.25 @@ -81,18 +84,19 @@
    1.26            in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    1.27        | print_term tyvars some_thm vars fxy (ICase case_expr) =
    1.28            (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.29 -           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.30 +           of SOME (app as ({ sym = Code_Symbol.Constant const, ... }, _)) =>
    1.31 +                if is_none (const_syntax const)
    1.32                  then print_case tyvars some_thm vars fxy case_expr
    1.33                  else print_app tyvars some_thm vars fxy app
    1.34              | NONE => print_case tyvars some_thm vars fxy case_expr)
    1.35 -    and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
    1.36 +    and print_app_expr tyvars some_thm vars ({ sym, dom, range, annotate, ... }, ts) =
    1.37        let
    1.38 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
    1.39 +        val ty = Library.foldr (op `->) (dom, range)
    1.40          val printed_const =
    1.41            if annotate then
    1.42 -            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    1.43 +            brackets [(str o deresolve) sym, str "::", print_typ tyvars NOBR ty]
    1.44            else
    1.45 -            (str o deresolve) c
    1.46 +            (str o deresolve) sym
    1.47        in 
    1.48          printed_const :: map (print_term tyvars some_thm vars BR) ts
    1.49        end
    1.50 @@ -122,17 +126,16 @@
    1.51              (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
    1.52              (map print_select clauses)
    1.53            end;
    1.54 -    fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    1.55 +    fun print_stmt (Code_Symbol.Constant const, Code_Thingol.Fun (((vs, ty), raw_eqs), _)) =
    1.56            let
    1.57              val tyvars = intro_vars (map fst vs) reserved;
    1.58              fun print_err n =
    1.59 -              semicolon (
    1.60 -                (str o deresolve) name
    1.61 -                :: map str (replicate n "_")
    1.62 -                @ str "="
    1.63 -                :: str "error"
    1.64 -                @@ (str o ML_Syntax.print_string
    1.65 -                    o Long_Name.base_name o Long_Name.qualifier) name
    1.66 +              (semicolon o map str) (
    1.67 +                deresolve_const const
    1.68 +                :: replicate n "_"
    1.69 +                @ "="
    1.70 +                :: "error"
    1.71 +                @@ ML_Syntax.print_string const
    1.72                );
    1.73              fun print_eqn ((ts, t), (some_thm, _)) =
    1.74                let
    1.75 @@ -143,7 +146,7 @@
    1.76                        (insert (op =)) ts []);
    1.77                in
    1.78                  semicolon (
    1.79 -                  (str o deresolve) name
    1.80 +                  (str o deresolve_const) const
    1.81                    :: map (print_term tyvars some_thm vars BR) ts
    1.82                    @ str "="
    1.83                    @@ print_term tyvars some_thm vars NOBR t
    1.84 @@ -152,7 +155,7 @@
    1.85            in
    1.86              Pretty.chunks (
    1.87                semicolon [
    1.88 -                (str o suffix " ::" o deresolve) name,
    1.89 +                (str o suffix " ::" o deresolve_const) const,
    1.90                  print_typscheme tyvars (vs, ty)
    1.91                ]
    1.92                :: (case filter (snd o snd) raw_eqs
    1.93 @@ -160,52 +163,52 @@
    1.94                  | eqs => map print_eqn eqs)
    1.95              )
    1.96            end
    1.97 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) =
    1.98 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [])) =
    1.99            let
   1.100              val tyvars = intro_vars vs reserved;
   1.101            in
   1.102              semicolon [
   1.103                str "data",
   1.104 -              print_typdecl tyvars (deresolve name, vs)
   1.105 +              print_typdecl tyvars (deresolve_tyco tyco, vs)
   1.106              ]
   1.107            end
   1.108 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, [((co, _), [ty])]))) =
   1.109 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, [((co, _), [ty])])) =
   1.110            let
   1.111              val tyvars = intro_vars vs reserved;
   1.112            in
   1.113              semicolon (
   1.114                str "newtype"
   1.115 -              :: print_typdecl tyvars (deresolve name, vs)
   1.116 +              :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   1.117                :: str "="
   1.118 -              :: (str o deresolve) co
   1.119 +              :: (str o deresolve_const) co
   1.120                :: print_typ tyvars BR ty
   1.121 -              :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
   1.122 +              :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
   1.123              )
   1.124            end
   1.125 -      | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) =
   1.126 +      | print_stmt (Code_Symbol.Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
   1.127            let
   1.128              val tyvars = intro_vars vs reserved;
   1.129              fun print_co ((co, _), tys) =
   1.130                concat (
   1.131 -                (str o deresolve) co
   1.132 +                (str o deresolve_const) co
   1.133                  :: map (print_typ tyvars BR) tys
   1.134                )
   1.135            in
   1.136              semicolon (
   1.137                str "data"
   1.138 -              :: print_typdecl tyvars (deresolve name, vs)
   1.139 +              :: print_typdecl tyvars (deresolve_tyco tyco, vs)
   1.140                :: str "="
   1.141                :: print_co co
   1.142                :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
   1.143 -              @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
   1.144 +              @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
   1.145              )
   1.146            end
   1.147 -      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
   1.148 +      | print_stmt (Code_Symbol.Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
   1.149            let
   1.150              val tyvars = intro_vars [v] reserved;
   1.151              fun print_classparam (classparam, ty) =
   1.152                semicolon [
   1.153 -                (str o deresolve) classparam,
   1.154 +                (str o deresolve_const) classparam,
   1.155                  str "::",
   1.156                  print_typ tyvars NOBR ty
   1.157                ]
   1.158 @@ -213,8 +216,8 @@
   1.159              Pretty.block_enclose (
   1.160                Pretty.block [
   1.161                  str "class ",
   1.162 -                Pretty.block (print_typcontext tyvars [(v, map fst super_classes)]),
   1.163 -                str (deresolve name ^ " " ^ lookup_var tyvars v),
   1.164 +                Pretty.block (print_typcontext tyvars [(v, map snd classrels)]),
   1.165 +                str (deresolve_class class ^ " " ^ lookup_var tyvars v),
   1.166                  str " where {"
   1.167                ],
   1.168                str "};"
   1.169 @@ -230,20 +233,20 @@
   1.170              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
   1.171                case requires_args classparam
   1.172                 of NONE => semicolon [
   1.173 -                      (str o Long_Name.base_name o deresolve) classparam,
   1.174 +                      (str o Long_Name.base_name o deresolve_const) classparam,
   1.175                        str "=",
   1.176                        print_app tyvars (SOME thm) reserved NOBR (const, [])
   1.177                      ]
   1.178                  | SOME k =>
   1.179                      let
   1.180 -                      val { name = c, dom, range, ... } = const;
   1.181 +                      val { sym = Code_Symbol.Constant c, dom, range, ... } = const;
   1.182                        val (vs, rhs) = (apfst o map) fst
   1.183                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
   1.184                        val s = if (is_some o const_syntax) c
   1.185 -                        then NONE else (SOME o Long_Name.base_name o deresolve) c;
   1.186 +                        then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
   1.187                        val vars = reserved
   1.188                          |> intro_vars (map_filter I (s :: vs));
   1.189 -                      val lhs = IConst { name = classparam, typargs = [],
   1.190 +                      val lhs = IConst { sym = Code_Symbol.Constant classparam, typargs = [],
   1.191                          dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
   1.192                          (*dictionaries are not relevant at this late stage,
   1.193                            and these consts never need type annotations for disambiguation *)
   1.194 @@ -268,7 +271,7 @@
   1.195            end;
   1.196    in print_stmt end;
   1.197  
   1.198 -fun haskell_program_of_program ctxt symbol_of module_prefix module_name reserved identifiers =
   1.199 +fun haskell_program_of_program ctxt module_prefix module_name reserved identifiers =
   1.200    let
   1.201      fun namify_fun upper base (nsp_fun, nsp_typ) =
   1.202        let
   1.203 @@ -279,7 +282,7 @@
   1.204        let
   1.205          val (base', nsp_typ') = Name.variant (first_upper base) nsp_typ;
   1.206        in (base', (nsp_fun, nsp_typ')) end;
   1.207 -    fun namify_stmt (Code_Thingol.Fun (_, (_, SOME _))) = pair
   1.208 +    fun namify_stmt (Code_Thingol.Fun (_, SOME _)) = pair
   1.209        | namify_stmt (Code_Thingol.Fun _) = namify_fun false
   1.210        | namify_stmt (Code_Thingol.Datatype _) = namify_typ
   1.211        | namify_stmt (Code_Thingol.Datatypecons _) = namify_fun true
   1.212 @@ -287,7 +290,7 @@
   1.213        | namify_stmt (Code_Thingol.Classrel _) = pair
   1.214        | namify_stmt (Code_Thingol.Classparam _) = namify_fun false
   1.215        | namify_stmt (Code_Thingol.Classinst _) = pair;
   1.216 -    fun select_stmt (Code_Thingol.Fun (_, (_, SOME _))) = false
   1.217 +    fun select_stmt (Code_Thingol.Fun (_, SOME _)) = false
   1.218        | select_stmt (Code_Thingol.Fun _) = true
   1.219        | select_stmt (Code_Thingol.Datatype _) = true
   1.220        | select_stmt (Code_Thingol.Datatypecons _) = false
   1.221 @@ -296,7 +299,7 @@
   1.222        | select_stmt (Code_Thingol.Classparam _) = false
   1.223        | select_stmt (Code_Thingol.Classinst _) = true;
   1.224    in
   1.225 -    Code_Namespace.flat_program ctxt symbol_of
   1.226 +    Code_Namespace.flat_program ctxt
   1.227        { module_prefix = module_prefix, module_name = module_name, reserved = reserved,
   1.228          identifiers = identifiers, empty_nsp = (reserved, reserved), namify_stmt = namify_stmt,
   1.229          modify_stmt = fn stmt => if select_stmt stmt then SOME stmt else NONE }
   1.230 @@ -323,25 +326,24 @@
   1.231    ("Maybe", ["Nothing", "Just"])
   1.232  ];
   1.233  
   1.234 -fun serialize_haskell module_prefix string_classes ctxt { symbol_of, module_name,
   1.235 +fun serialize_haskell module_prefix string_classes ctxt { module_name,
   1.236      reserved_syms, identifiers, includes, class_syntax, tyco_syntax, const_syntax } program =
   1.237    let
   1.238  
   1.239      (* build program *)
   1.240      val reserved = fold (insert (op =) o fst) includes reserved_syms;
   1.241      val { deresolver, flat_program = haskell_program } = haskell_program_of_program
   1.242 -      ctxt symbol_of module_prefix module_name (Name.make_context reserved) identifiers program;
   1.243 +      ctxt module_prefix module_name (Name.make_context reserved) identifiers program;
   1.244  
   1.245      (* print statements *)
   1.246      fun deriving_show tyco =
   1.247        let
   1.248          fun deriv _ "fun" = false
   1.249 -          | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
   1.250 -              andalso (member (op =) tycos tyco
   1.251 -              orelse case try (Graph.get_node program) tyco
   1.252 -                of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
   1.253 +          | deriv tycos tyco = member (op =) tycos tyco
   1.254 +              orelse case try (Code_Symbol.Graph.get_node program) (Code_Symbol.Type_Constructor tyco)
   1.255 +                of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
   1.256                      (maps snd cs)
   1.257 -                 | NONE => true)
   1.258 +                 | NONE => true
   1.259          and deriv' tycos (tyco `%% tys) = deriv tycos tyco
   1.260                andalso forall (deriv' tycos) tys
   1.261            | deriv' _ (ITyVar _) = true
   1.262 @@ -369,10 +371,10 @@
   1.263          val deresolve = deresolver module_name;
   1.264          fun print_import module_name = (semicolon o map str) ["import qualified", module_name];
   1.265          val import_ps = import_common_ps @ map (print_qualified_import o fst) imports;
   1.266 -        fun print_stmt' name = case Graph.get_node gr name
   1.267 +        fun print_stmt' sym = case Code_Symbol.Graph.get_node gr sym
   1.268           of (_, NONE) => NONE
   1.269 -          | (_, SOME stmt) => SOME (markup_stmt name (print_stmt deresolve (name, stmt)));
   1.270 -        val body_ps = map_filter print_stmt' ((flat o rev o Graph.strong_conn) gr);
   1.271 +          | (_, SOME stmt) => SOME (markup_stmt sym (print_stmt deresolve (sym, stmt)));
   1.272 +        val body_ps = map_filter print_stmt' ((flat o rev o Code_Symbol.Graph.strong_conn) gr);
   1.273        in
   1.274          print_module_frame module_name
   1.275            ((if null import_ps then [] else [Pretty.chunks import_ps]) @ body_ps)
   1.276 @@ -430,7 +432,7 @@
   1.277       of SOME ((pat, ty), t') =>
   1.278            SOME ((SOME ((pat, ty), true), t1), t')
   1.279        | NONE => NONE;
   1.280 -    fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
   1.281 +    fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
   1.282            if c = c_bind_name then dest_bind t1 t2
   1.283            else NONE
   1.284        | dest_monad _ t = case Code_Thingol.split_let t