diff -r 0b92e6359bc4 -r d2e9b2dab760 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Tue Oct 13 14:57:53 2009 +0200 +++ b/src/Tools/Code/code_haskell.ML Wed Oct 14 11:56:44 2009 +0200 @@ -24,7 +24,7 @@ (** Haskell serializer **) fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const - init_syms deresolve contr_classparam_typs deriving_show = + reserved deresolve contr_classparam_typs deriving_show = let val deresolve_base = Long_Name.base_name o deresolve; fun class_name class = case syntax_class class @@ -34,18 +34,18 @@ of [] => [] | classbinds => Pretty.enum "," "(" ")" ( map (fn (v, class) => - str (class_name class ^ " " ^ Code_Printer.lookup_var tyvars v)) classbinds) + str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds) @@ str " => "; fun pr_typforall tyvars vs = case map fst vs of [] => [] | vnames => str "forall " :: Pretty.breaks - (map (str o Code_Printer.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; + (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; fun pr_tycoexpr tyvars fxy (tyco, tys) = brackify fxy (str tyco :: map (pr_typ tyvars BR) tys) and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys) | SOME (i, pr) => pr (pr_typ tyvars) fxy tys) - | pr_typ tyvars fxy (ITyVar v) = (str o Code_Printer.lookup_var tyvars) v; + | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun pr_typdecl tyvars (vs, tycoexpr) = Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr); fun pr_typscheme tyvars (vs, ty) = @@ -63,7 +63,7 @@ | pr_term tyvars thm vars fxy (IVar NONE) = str "_" | pr_term tyvars thm vars fxy (IVar (SOME v)) = - (str o Code_Printer.lookup_var vars) v + (str o lookup_var vars) v | pr_term tyvars thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; @@ -118,7 +118,7 @@ (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = let - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; val n = (length o fst o Code_Thingol.unfold_fun) ty; in Pretty.chunks [ @@ -141,14 +141,14 @@ | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = let val eqs = filter (snd o snd) raw_eqs; - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; fun pr_eq ((ts, t), (thm, _)) = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; - val vars = init_syms - |> Code_Printer.intro_base_names + val vars = reserved + |> intro_base_names (is_none o syntax_const) deresolve consts - |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames) + |> intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []); in semicolon ( @@ -171,7 +171,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = let - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; in semicolon [ str "data", @@ -180,7 +180,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) = let - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; in semicolon ( str "newtype" @@ -193,7 +193,7 @@ end | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = let - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; fun pr_co (co, tys) = concat ( (str o deresolve_base) co @@ -211,7 +211,7 @@ end | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) = let - val tyvars = Code_Printer.intro_vars [v] init_syms; + val tyvars = intro_vars [v] reserved; fun pr_classparam (classparam, ty) = semicolon [ (str o deresolve_base) classparam, @@ -223,7 +223,7 @@ Pretty.block [ str "class ", Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), - str (deresolve_base name ^ " " ^ Code_Printer.lookup_var tyvars v), + str (deresolve_base name ^ " " ^ lookup_var tyvars v), str " where {" ], str "};" @@ -231,12 +231,12 @@ end | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = let - val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; + val tyvars = intro_vars (map fst vs) reserved; fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam of NONE => semicolon [ (str o deresolve_base) classparam, str "=", - pr_app tyvars thm init_syms NOBR (c_inst, []) + pr_app tyvars thm reserved NOBR (c_inst, []) ] | SOME (k, pr) => let @@ -245,9 +245,9 @@ then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name; val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs); - val vars = init_syms - |> Code_Printer.intro_vars (the_list const) - |> Code_Printer.intro_vars (map_filter I vs); + val vars = reserved + |> intro_vars (the_list const) + |> intro_vars (map_filter I vs); val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; (*dictionaries are not relevant at this late stage*) in @@ -271,24 +271,24 @@ end; in pr_stmt end; -fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program = +fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program = let val module_alias = if is_some module_name then K module_name else raw_module_alias; - val reserved_names = Name.make_context reserved_names; - val mk_name_module = Code_Printer.mk_name_module reserved_names module_prefix module_alias program; + val reserved = Name.make_context reserved; + val mk_name_module = mk_name_module reserved module_prefix module_alias program; fun add_stmt (name, (stmt, deps)) = let - val (module_name, base) = Code_Printer.dest_name name; + val (module_name, base) = dest_name name; val module_name' = mk_name_module module_name; val mk_name_stmt = yield_singleton Name.variants; fun add_fun upper (nsp_fun, nsp_typ) = let val (base', nsp_fun') = - mk_name_stmt (if upper then Code_Printer.first_upper base else base) nsp_fun + mk_name_stmt (if upper then first_upper base else base) nsp_fun in (base', (nsp_fun', nsp_typ)) end; fun add_typ (nsp_fun, nsp_typ) = let - val (base', nsp_typ') = mk_name_stmt (Code_Printer.first_upper base) nsp_typ + val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ in (base', (nsp_fun, nsp_typ')) end; val add_name = case stmt of Code_Thingol.Fun _ => add_fun false @@ -306,7 +306,7 @@ cons (name, (Long_Name.append module_name' base', NONE)) | _ => cons (name, (Long_Name.append module_name' base', SOME stmt)); in - Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names)))) + Symtab.map_default (module_name', ([], ([], (reserved, reserved)))) (apfst (fold (insert (op = : string * string -> bool)) deps)) #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name')) #-> (fn (base', names) => @@ -317,19 +317,19 @@ (Graph.get_node program name, Graph.imm_succs program name)) (Graph.strong_conn program |> flat)) Symtab.empty; fun deresolver name = (fst o the o AList.lookup (op =) ((fst o snd o the - o Symtab.lookup hs_program) ((mk_name_module o fst o Code_Printer.dest_name) name))) name + o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name handle Option => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, hs_program) end; fun serialize_haskell module_prefix raw_module_name string_classes labelled_name - raw_reserved_names includes raw_module_alias + raw_reserved includes raw_module_alias syntax_class syntax_tyco syntax_const program cs destination = let val stmt_names = Code_Target.stmt_names_of_destination destination; val module_name = if null stmt_names then raw_module_name else SOME "Code"; - val reserved_names = fold (insert (op =) o fst) includes raw_reserved_names; + val reserved = fold (insert (op =) o fst) includes raw_reserved; val (deresolver, hs_program) = haskell_program_of_program labelled_name - module_name module_prefix reserved_names raw_module_alias program; + module_name module_prefix reserved raw_module_alias program; val contr_classparam_typs = Code_Thingol.contr_classparam_typs program; fun deriving_show tyco = let @@ -343,9 +343,9 @@ andalso forall (deriv' tycos) tys | deriv' _ (ITyVar _) = true in deriv [] tyco end; - val reserved_names = Code_Printer.make_vars reserved_names; + val reserved = make_vars reserved; fun pr_stmt qualified = pr_haskell_stmt labelled_name - syntax_class syntax_tyco syntax_const reserved_names + syntax_class syntax_tyco syntax_const reserved (if qualified then deresolver else Long_Name.base_name o deresolver) contr_classparam_typs (if string_classes then deriving_show else K false);