# HG changeset patch # User haftmann # Date 1260004703 -3600 # Node ID e4fb0daadcffd58a46b8f1a1cd90cbabd4dbe1ed # Parent c54498f88a77a58eb6792e8a27eb5c974ce92ee7# Parent ebf231de0c5cecf0ef60cf9c47ae9038355c6ec9 merged diff -r c54498f88a77 -r e4fb0daadcff NEWS --- a/NEWS Fri Dec 04 22:51:59 2009 +0100 +++ b/NEWS Sat Dec 05 10:18:23 2009 +0100 @@ -4,6 +4,18 @@ New in this Isabelle version ---------------------------- +*** HOL *** + +* Reorganized theory Sum_Type.thy; Inl and Inr now have +authentic syntax. INCOMPATIBILITY. + +* Code generation: ML and OCaml code is decorated with signatures. + + +*** ML *** + +* Curried take and drop. INCOMPATIBILITY. + New in Isabelle2009-1 (December 2009) ------------------------------------- diff -r c54498f88a77 -r e4fb0daadcff src/HOL/Predicate.thy --- a/src/HOL/Predicate.thy Fri Dec 04 22:51:59 2009 +0100 +++ b/src/HOL/Predicate.thy Sat Dec 05 10:18:23 2009 +0100 @@ -831,6 +831,8 @@ lemma the_eq[code]: "the A = singleton (\x. not_unique A) A" by (auto simp add: the_def singleton_def not_unique_def) +code_abort not_unique + ML {* signature PREDICATE = sig @@ -876,8 +878,6 @@ code_const Seq and Empty and Insert and Join (Eval "Predicate.Seq" and "Predicate.Empty" and "Predicate.Insert/ (_,/ _)" and "Predicate.Join/ (_,/ _)") -code_abort not_unique - no_notation inf (infixl "\" 70) and sup (infixl "\" 65) and diff -r c54498f88a77 -r e4fb0daadcff src/HOL/Sum_Type.thy --- a/src/HOL/Sum_Type.thy Fri Dec 04 22:51:59 2009 +0100 +++ b/src/HOL/Sum_Type.thy Sat Dec 05 10:18:23 2009 +0100 @@ -49,10 +49,10 @@ by (auto simp add: Inl_Rep_def Inr_Rep_def expand_fun_eq) definition Inl :: "'a \ 'a + 'b" where - "Inl = Abs_Sum \ Inl_Rep" + "Inl = Abs_Sum \ Inl_Rep" definition Inr :: "'b \ 'a + 'b" where - "Inr = Abs_Sum \ Inr_Rep" + "Inr = Abs_Sum \ Inr_Rep" lemma inj_Inl [simp]: "inj_on Inl A" by (auto simp add: Inl_def intro!: comp_inj_on Inl_Rep_inject inj_on_Abs_Sum Inl_RepI) @@ -160,6 +160,7 @@ then show "f x = g x" by simp qed + subsection {* The Disjoint Sum of Sets *} definition Plus :: "'a set \ 'b set \ ('a + 'b) set" (infixr "<+>" 65) where diff -r c54498f88a77 -r e4fb0daadcff src/HOL/Tools/numeral.ML --- a/src/HOL/Tools/numeral.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/HOL/Tools/numeral.ML Sat Dec 05 10:18:23 2009 +0100 @@ -62,16 +62,16 @@ let fun dest_bit (IConst (c, _)) = if c = bit0' then 0 else if c = bit1' then 1 - else Code_Printer.nerror thm "Illegal numeral expression: illegal bit" - | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit"; + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit" + | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"; fun dest_num (IConst (c, _)) = if c = pls' then SOME 0 else if c = min' then if negative then SOME ~1 else NONE - else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit" + else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit" | dest_num (t1 `$ t2) = let val (n, b) = (dest_num t2, dest_bit t1) in case n of SOME n => SOME (2 * n + b) | NONE => NONE end - | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term"; + | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; in dest_num end; fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] = (Code_Printer.str o Code_Printer.literal_numeral literals unbounded diff -r c54498f88a77 -r e4fb0daadcff src/HOL/Tools/string_code.ML --- a/src/HOL/Tools/string_code.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/HOL/Tools/string_code.ML Sat Dec 05 10:18:23 2009 +0100 @@ -67,7 +67,7 @@ fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] = case decode_char nibbles' (t1, t2) of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c - | NONE => Code_Printer.nerror thm "Illegal character expression"; + | NONE => Code_Printer.eqn_error thm "Illegal character expression"; in Code_Target.add_syntax_const target @{const_name Char} (SOME (2, (cs_nibbles, pretty))) end; @@ -79,8 +79,8 @@ of SOME ts => (case implode_string char' nibbles' (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts of SOME p => p - | NONE => Code_Printer.nerror thm "Illegal message expression") - | NONE => Code_Printer.nerror thm "Illegal message expression"; + | NONE => Code_Printer.eqn_error thm "Illegal message expression") + | NONE => Code_Printer.eqn_error thm "Illegal message expression"; in Code_Target.add_syntax_const target @{const_name STR} (SOME (1, (cs_summa, pretty))) end; diff -r c54498f88a77 -r e4fb0daadcff src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/Tools/Code/code_haskell.ML Sat Dec 05 10:18:23 2009 +0100 @@ -23,126 +23,124 @@ (** Haskell serializer **) -fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const +fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const 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 of NONE => deresolve class | SOME class => class; - fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs + fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs of [] => [] - | classbinds => Pretty.enum "," "(" ")" ( + | classbinds => Pretty.list "(" ")" ( map (fn (v, class) => str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds) @@ str " => "; - fun pr_typforall tyvars vs = case map fst vs + fun print_typforall tyvars vs = case map fst vs of [] => [] | vnames => str "forall " :: Pretty.breaks (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 (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 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) = - Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty); - fun pr_term tyvars thm vars fxy (IConst c) = - pr_app tyvars thm vars fxy (c, []) - | pr_term tyvars thm vars fxy (t as (t1 `$ t2)) = + fun print_tyco_expr tyvars fxy (tyco, tys) = + brackify fxy (str tyco :: map (print_typ tyvars BR) tys) + and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco + of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) + | SOME (i, print) => print (print_typ tyvars) fxy tys) + | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; + fun print_typdecl tyvars (vs, tycoexpr) = + Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); + fun print_typscheme tyvars (vs, ty) = + Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); + fun print_term tyvars thm vars fxy (IConst c) = + print_app tyvars thm vars fxy (c, []) + | print_term tyvars thm vars fxy (t as (t1 `$ t2)) = (case Code_Thingol.unfold_const_app t - of SOME app => pr_app tyvars thm vars fxy app + of SOME app => print_app tyvars thm vars fxy app | _ => brackify fxy [ - pr_term tyvars thm vars NOBR t1, - pr_term tyvars thm vars BR t2 + print_term tyvars thm vars NOBR t1, + print_term tyvars thm vars BR t2 ]) - | pr_term tyvars thm vars fxy (IVar NONE) = + | print_term tyvars thm vars fxy (IVar NONE) = str "_" - | pr_term tyvars thm vars fxy (IVar (SOME v)) = + | print_term tyvars thm vars fxy (IVar (SOME v)) = (str o lookup_var vars) v - | pr_term tyvars thm vars fxy (t as _ `|=> _) = + | print_term tyvars thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; - val (ps, vars') = fold_map (pr_bind tyvars thm BR o fst) binds vars; - in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end - | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) = + val (ps, vars') = fold_map (print_bind tyvars thm BR o fst) binds vars; + in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars thm vars' NOBR t') end + | print_term tyvars thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) - then pr_case tyvars thm vars fxy cases - else pr_app tyvars thm vars fxy c_ts - | NONE => pr_case tyvars thm vars fxy cases) - and pr_app' tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c - of [] => (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts + then print_case tyvars thm vars fxy cases + else print_app tyvars thm vars fxy c_ts + | NONE => print_case tyvars thm vars fxy cases) + and print_app_expr tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c + of [] => (str o deresolve) c :: map (print_term tyvars thm vars BR) ts | fingerprint => let val ts_fingerprint = ts ~~ take (length ts) fingerprint; val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) => (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint; - fun pr_term_anno (t, NONE) _ = pr_term tyvars thm vars BR t - | pr_term_anno (t, SOME _) ty = - brackets [pr_term tyvars thm vars NOBR t, str "::", pr_typ tyvars NOBR ty]; + fun print_term_anno (t, NONE) _ = print_term tyvars thm vars BR t + | print_term_anno (t, SOME _) ty = + brackets [print_term tyvars thm vars NOBR t, str "::", print_typ tyvars NOBR ty]; in if needs_annotation then - (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (take (length ts) tys) - else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts + (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys) + else (str o deresolve) c :: map (print_term tyvars thm vars BR) ts end - and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const - and pr_bind tyvars thm fxy p = gen_pr_bind (pr_term tyvars) thm fxy p - and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) = + and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const + and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars) thm fxy p + and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun pr ((pat, ty), t) vars = + fun print_match ((pat, ty), t) vars = vars - |> pr_bind tyvars thm BR pat - |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t]) - val (ps, vars') = fold_map pr binds vars; + |> print_bind tyvars thm BR pat + |>> (fn p => semicolon [p, str "=", print_term tyvars thm vars NOBR t]) + val (ps, vars') = fold_map print_match binds vars; in brackify_block fxy (str "let {") ps - (concat [str "}", str "in", pr_term tyvars thm vars' NOBR body]) + (concat [str "}", str "in", print_term tyvars thm vars' NOBR body]) end - | pr_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) = + | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) = let - fun pr (pat, body) = + fun print_select (pat, body) = let - val (p, vars') = pr_bind tyvars thm NOBR pat vars; - in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end; + val (p, vars') = print_bind tyvars thm NOBR pat vars; + in semicolon [p, str "->", print_term tyvars thm vars' NOBR body] end; in brackify_block fxy - (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"]) - (map pr clauses) + (concat [str "case", print_term tyvars thm vars NOBR t, str "of", str "{"]) + (map print_select clauses) (str "}") end - | pr_case tyvars thm vars fxy ((_, []), _) = + | print_case tyvars thm vars fxy ((_, []), _) = (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]; - fun pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = + fun print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), []))) = let val tyvars = intro_vars (map fst vs) reserved; val n = (length o fst o Code_Thingol.unfold_fun) ty; in Pretty.chunks [ - Pretty.block [ + semicolon [ (str o suffix " ::" o deresolve_base) name, - Pretty.brk 1, - pr_typscheme tyvars (vs, ty), - str ";" + print_typscheme tyvars (vs, ty) ], - concat ( + semicolon ( (str o deresolve_base) name :: map str (replicate n "_") @ str "=" :: str "error" - @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string + @@ (str o ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ) ] end - | pr_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = + | print_stmt (name, Code_Thingol.Fun (_, ((vs, ty), raw_eqs))) = let val eqs = filter (snd o snd) raw_eqs; val tyvars = intro_vars (map fst vs) reserved; - fun pr_eq ((ts, t), (thm, _)) = + fun print_eqn ((ts, t), (thm, _)) = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; val vars = reserved @@ -153,90 +151,88 @@ in semicolon ( (str o deresolve_base) name - :: map (pr_term tyvars thm vars BR) ts + :: map (print_term tyvars thm vars BR) ts @ str "=" - @@ pr_term tyvars thm vars NOBR t + @@ print_term tyvars thm vars NOBR t ) end; in Pretty.chunks ( - Pretty.block [ + semicolon [ (str o suffix " ::" o deresolve_base) name, - Pretty.brk 1, - pr_typscheme tyvars (vs, ty), - str ";" + print_typscheme tyvars (vs, ty) ] - :: map pr_eq eqs + :: map print_eqn eqs ) end - | pr_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = + | print_stmt (name, Code_Thingol.Datatype (_, (vs, []))) = let val tyvars = intro_vars (map fst vs) reserved; in semicolon [ str "data", - pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) + print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) ] end - | pr_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) = + | print_stmt (name, Code_Thingol.Datatype (_, (vs, [(co, [ty])]))) = let val tyvars = intro_vars (map fst vs) reserved; in semicolon ( str "newtype" - :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) + :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) :: str "=" :: (str o deresolve_base) co - :: pr_typ tyvars BR ty + :: print_typ tyvars BR ty :: (if deriving_show name then [str "deriving (Read, Show)"] else []) ) end - | pr_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = + | print_stmt (name, Code_Thingol.Datatype (_, (vs, co :: cos))) = let val tyvars = intro_vars (map fst vs) reserved; - fun pr_co (co, tys) = + fun print_co (co, tys) = concat ( (str o deresolve_base) co - :: map (pr_typ tyvars BR) tys + :: map (print_typ tyvars BR) tys ) in semicolon ( str "data" - :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) + :: print_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs)) :: str "=" - :: pr_co co - :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos + :: print_co co + :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos @ (if deriving_show name then [str "deriving (Read, Show)"] else []) ) end - | pr_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) = + | print_stmt (name, Code_Thingol.Class (_, (v, (superclasses, classparams)))) = let val tyvars = intro_vars [v] reserved; - fun pr_classparam (classparam, ty) = + fun print_classparam (classparam, ty) = semicolon [ (str o deresolve_base) classparam, str "::", - pr_typ tyvars NOBR ty + print_typ tyvars NOBR ty ] in Pretty.block_enclose ( Pretty.block [ str "class ", - Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]), + Pretty.block (print_typcontext tyvars [(v, map fst superclasses)]), str (deresolve_base name ^ " " ^ lookup_var tyvars v), str " where {" ], str "};" - ) (map pr_classparam classparams) + ) (map print_classparam classparams) end - | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = + | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = let val tyvars = intro_vars (map fst vs) reserved; - fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam + fun print_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam of NONE => semicolon [ (str o deresolve_base) classparam, str "=", - pr_app tyvars thm reserved NOBR (c_inst, []) + print_app tyvars thm reserved NOBR (c_inst, []) ] | SOME (k, pr) => let @@ -252,24 +248,24 @@ (*dictionaries are not relevant at this late stage*) in semicolon [ - pr_term tyvars thm vars NOBR lhs, + print_term tyvars thm vars NOBR lhs, str "=", - pr_term tyvars thm vars NOBR rhs + print_term tyvars thm vars NOBR rhs ] end; in Pretty.block_enclose ( Pretty.block [ str "instance ", - Pretty.block (pr_typcontext tyvars vs), + Pretty.block (print_typcontext tyvars vs), str (class_name class ^ " "), - pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), + print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs), str " where {" ], str "};" - ) (map pr_instdef classparam_insts) + ) (map print_instdef classparam_insts) end; - in pr_stmt end; + in print_stmt end; fun haskell_program_of_program labelled_name module_name module_prefix reserved raw_module_alias program = let @@ -344,12 +340,12 @@ | deriv' _ (ITyVar _) = true in deriv [] tyco end; val reserved = make_vars reserved; - fun pr_stmt qualified = pr_haskell_stmt labelled_name + fun print_stmt qualified = print_haskell_stmt labelled_name 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); - fun pr_module name content = + fun print_module name content = (name, Pretty.chunks [ str ("module " ^ name ^ " where {"), str "", @@ -366,26 +362,23 @@ |> map_filter (try deresolver) |> map Long_Name.qualifier |> distinct (op =); - fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";"); - val pr_import_module = str o (if qualified + fun print_import_include (name, _) = str ("import qualified " ^ name ^ ";"); + val print_import_module = str o (if qualified then prefix "import qualified " else prefix "import ") o suffix ";"; - val content = Pretty.chunks ( - map pr_import_include includes - @ map pr_import_module imports - @ str "" - :: separate (str "") (map_filter - (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt)) - | (_, (_, NONE)) => NONE) stmts) - ) - in pr_module module_name' content end; - fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks ( - separate (str "") (map_filter + val import_ps = map print_import_include includes @ map print_import_module imports + val content = Pretty.chunks2 (if null import_ps then [] else [Pretty.block import_ps] + @ map_filter + (fn (name, (_, SOME stmt)) => SOME (print_stmt qualified (name, stmt)) + | (_, (_, NONE)) => NONE) stmts + ); + in print_module module_name' content end; + fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks2 (map_filter (fn (name, (_, SOME stmt)) => if null stmt_names orelse member (op =) stmt_names name - then SOME (pr_stmt false (name, stmt)) + then SOME (print_stmt false (name, stmt)) else NONE - | (_, (_, NONE)) => NONE) stmts)); + | (_, (_, NONE)) => NONE) stmts); val serialize_module = if null stmt_names then serialize_module1 else pair "" o serialize_module2; fun check_destination destination = @@ -407,7 +400,7 @@ (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module (check_destination file))) (rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd)) - (map (uncurry pr_module) includes + (map (uncurry print_module) includes @ map serialize_module (Symtab.dest hs_program)) destination end; @@ -443,21 +436,25 @@ SOME ((SOME ((pat, ty), false), tbind), t') | NONE => NONE; fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name); - fun pr_monad pr_bind pr (NONE, t) vars = - (semicolon [pr vars NOBR t], vars) - | pr_monad pr_bind pr (SOME ((bind, _), true), t) vars = vars - |> pr_bind NOBR bind - |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) - | pr_monad pr_bind pr (SOME ((bind, _), false), t) vars = vars - |> pr_bind NOBR bind - |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); - fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 + fun print_monad print_bind print_term (NONE, t) vars = + (semicolon [print_term vars NOBR t], vars) + | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars + |> print_bind NOBR bind + |>> (fn p => semicolon [p, str "<-", print_term vars NOBR t]) + | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars + |> print_bind NOBR bind + |>> (fn p => semicolon [str "let", p, str "=", print_term vars NOBR t]); + fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2 of SOME (bind, t') => let val (binds, t'') = implode_monad c_bind' t' - val (ps, vars') = fold_map (pr_monad (gen_pr_bind (K pr) thm) pr) (bind :: binds) vars; - in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end + val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term) + (bind :: binds) vars; + in + (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) + (ps @| print_term vars' NOBR t'') + end | NONE => brackify_infix (1, L) fxy - [pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2] + [print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2] in (2, ([c_bind], pretty)) end; fun add_monad target' raw_c_bind thy = @@ -472,11 +469,11 @@ (** Isar setup **) -fun isar_seri_haskell module = +fun isar_seri_haskell module_name = Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name) -- Scan.optional (Args.$$$ "string_classes" >> K true) false >> (fn (module_prefix, string_classes) => - serialize_haskell module_prefix module string_classes)); + serialize_haskell module_prefix module_name string_classes)); val _ = OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl ( @@ -486,11 +483,11 @@ val setup = Code_Target.add_target (target, (isar_seri_haskell, literals)) - #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => + #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy [ - pr_typ (INFX (1, X)) ty1, + print_typ (INFX (1, X)) ty1, str "->", - pr_typ (INFX (1, R)) ty2 + print_typ (INFX (1, R)) ty2 ])) #> fold (Code_Target.add_reserved target) [ "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", diff -r c54498f88a77 -r e4fb0daadcff src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/Tools/Code/code_ml.ML Sat Dec 05 10:18:23 2009 +0100 @@ -21,6 +21,9 @@ infixr 5 @@; infixr 5 @|; + +(** generic **) + val target_SML = "SML"; val target_OCaml = "OCaml"; val target_Eval = "Eval"; @@ -32,7 +35,7 @@ * ((string * const) * (thm * bool)) list)); datatype ml_stmt = - ML_Exc of string * int + ML_Exc of string * (typscheme * int) | ML_Val of ml_binding | ML_Funs of ml_binding list * string list | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list @@ -47,130 +50,144 @@ | stmt_names_of (ML_Datas ds) = map fst ds | stmt_names_of (ML_Class (name, _)) = [name]; +fun print_product _ [] = NONE + | print_product print [x] = SOME (print x) + | print_product print xs = (SOME o Pretty.enum " *" "" "") (map print xs); -(** SML serailizer **) +fun print_tuple _ _ [] = NONE + | print_tuple print fxy [x] = SOME (print fxy x) + | print_tuple print _ xs = SOME (Pretty.list "(" ")" (map (print NOBR) xs)); -fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons = + +(** SML serializer **) + +fun print_sml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = let - fun pr_dicts is_pseudo_fun fxy ds = - let - fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_" - | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_"; - fun pr_proj [] p = - p - | pr_proj [p'] p = - brackets [p', p] - | pr_proj (ps as _ :: _) p = - brackets [Pretty.enum " o" "(" ")" ps, p]; - fun pr_dict fxy (DictConst (inst, dss)) = - brackify fxy ((str o deresolve) inst :: - (if is_pseudo_fun inst then [str "()"] - else map (pr_dicts is_pseudo_fun BR) dss)) - | pr_dict fxy (DictVar (classrels, v)) = - pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v) - in case ds - of [] => str "()" - | [d] => pr_dict fxy d - | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds - end; - fun pr_tyvar_dicts is_pseudo_fun vs = - vs - |> map (fn (v, sort) => map_index (fn (i, _) => - DictVar ([], (v, (i, length sort)))) sort) - |> map (pr_dicts is_pseudo_fun BR); - fun pr_tycoexpr fxy (tyco, tys) = - let - val tyco' = (str o deresolve) tyco - in case map (pr_typ BR) tys - of [] => tyco' - | [p] => Pretty.block [p, Pretty.brk 1, tyco'] - | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] - end - and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco - of NONE => pr_tycoexpr fxy (tyco, tys) - | SOME (i, pr) => pr pr_typ fxy tys) - | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term is_pseudo_fun thm vars fxy (IConst c) = - pr_app is_pseudo_fun thm vars fxy (c, []) - | pr_term is_pseudo_fun thm vars fxy (IVar NONE) = + fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco + | print_tyco_expr fxy (tyco, [ty]) = + concat [print_typ BR ty, (str o deresolve) tyco] + | print_tyco_expr fxy (tyco, tys) = + concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco + of NONE => print_tyco_expr fxy (tyco, tys) + | SOME (i, print) => print print_typ fxy tys) + | print_typ fxy (ITyVar v) = str ("'" ^ v); + fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); + fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + (map_filter (fn (v, sort) => + (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); + fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); + fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); + fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) = + brackify fxy ((str o deresolve) inst :: + (if is_pseudo_fun inst then [str "()"] + else map_filter (print_dicts is_pseudo_fun BR) dss)) + | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) = + let + val v_p = str (if k = 1 then first_upper v ^ "_" + else first_upper v ^ string_of_int (i+1) ^ "_"); + in case classrels + of [] => v_p + | [classrel] => brackets [(str o deresolve) classrel, v_p] + | classrels => brackets + [Pretty.enum " o" "(" ")" (map (str o deresolve) classrels), v_p] + end + and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); + val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR + (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); + fun print_term is_pseudo_fun thm vars fxy (IConst c) = + print_app is_pseudo_fun thm vars fxy (c, []) + | print_term is_pseudo_fun thm vars fxy (IVar NONE) = str "_" - | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = + | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) - | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = + | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts - | NONE => brackify fxy - [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2]) - | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = + of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts + | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, + print_term is_pseudo_fun thm vars BR t2]) + | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; - fun pr (pat, ty) = - pr_bind is_pseudo_fun thm NOBR pat + fun print_abs (pat, ty) = + print_bind is_pseudo_fun thm NOBR pat #>> (fn p => concat [str "fn", p, str "=>"]); - val (ps, vars') = fold_map pr binds vars; - in brackets (ps @ [pr_term is_pseudo_fun thm vars' NOBR t']) end - | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = + val (ps, vars') = fold_map print_abs binds vars; + in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end + | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) - then pr_case is_pseudo_fun thm vars fxy cases - else pr_app is_pseudo_fun thm vars fxy c_ts - | NONE => pr_case is_pseudo_fun thm vars fxy cases) - and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = + then print_case is_pseudo_fun thm vars fxy cases + else print_app is_pseudo_fun thm vars fxy c_ts + | NONE => print_case is_pseudo_fun thm vars fxy cases) + and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then - let - val k = length tys - in if k < 2 then - (str o deresolve) c :: map (pr_term is_pseudo_fun thm vars BR) ts - else if k = length ts then - [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term is_pseudo_fun thm vars NOBR) ts)] - else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] end + let val k = length tys in + if k < 2 orelse length ts = k + then (str o deresolve) c + :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) + else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] + end else if is_pseudo_fun c then (str o deresolve) c @@ str "()" - else - (str o deresolve) c - :: (map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts - and pr_app is_pseudo_fun thm vars = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun) - syntax_const thm vars - and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun) - and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = + else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss + @ map (print_term is_pseudo_fun thm vars BR) ts + and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) + (print_term is_pseudo_fun) syntax_const thm vars + and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) + and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun pr ((pat, ty), t) vars = + fun print_match ((pat, ty), t) vars = vars - |> pr_bind is_pseudo_fun thm NOBR pat - |>> (fn p => semicolon [str "val", p, str "=", pr_term is_pseudo_fun thm vars NOBR t]) - val (ps, vars') = fold_map pr binds vars; + |> print_bind is_pseudo_fun thm NOBR pat + |>> (fn p => semicolon [str "val", p, str "=", + print_term is_pseudo_fun thm vars NOBR t]) + val (ps, vars') = fold_map print_match binds vars; in Pretty.chunks [ - [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block, - [str ("in"), Pretty.fbrk, pr_term is_pseudo_fun thm vars' NOBR body] |> Pretty.block, + Pretty.block [str ("let"), Pretty.fbrk, Pretty.chunks ps], + Pretty.block [str ("in"), Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], str ("end") ] end - | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = + | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = let - fun pr delim (pat, body) = + fun print_select delim (pat, body) = let - val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars; + val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; in - concat [str delim, p, str "=>", pr_term is_pseudo_fun thm vars' NOBR body] + concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body] end; in brackets ( str "case" - :: pr_term is_pseudo_fun thm vars NOBR t - :: pr "of" clause - :: map (pr "|") clauses + :: print_term is_pseudo_fun thm vars NOBR t + :: print_select "of" clause + :: map (print_select "|") clauses ) end - | pr_case is_pseudo_fun thm vars fxy ((_, []), _) = + | print_case is_pseudo_fun thm vars fxy ((_, []), _) = (concat o map str) ["raise", "Fail", "\"empty case\""]; - fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs as eq :: eqs'))) = + fun print_val_decl print_typscheme (name, typscheme) = concat + [str "val", str (deresolve name), str ":", print_typscheme typscheme]; + fun print_datatype_decl definer (tyco, (vs, cos)) = + let + fun print_co (co, []) = str (deresolve co) + | print_co (co, tys) = concat [str (deresolve co), str "of", + Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + in + concat ( + str definer + :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) + :: str "=" + :: separate (str "|") (map print_co cos) + ) + end; + fun print_def is_pseudo_fun needs_typ definer + (ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) = let - val vs_dict = filter_out (null o snd) vs; - val shift = if null eqs' then I else - map (Pretty.block o single o Pretty.block o single); - fun pr_eq definer ((ts, t), (thm, _)) = + fun print_eqn definer ((ts, t), (thm, _)) = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; val vars = reserved @@ -179,157 +196,158 @@ |> intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []); val prolog = if needs_typ then - concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty] + concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] else Pretty.strs [definer, deresolve name]; in concat ( prolog :: (if is_pseudo_fun name then [str "()"] - else pr_tyvar_dicts is_pseudo_fun vs_dict - @ map (pr_term is_pseudo_fun thm vars BR) ts) + else print_dict_args vs + @ map (print_term is_pseudo_fun thm vars BR) ts) @ str "=" - @@ pr_term is_pseudo_fun thm vars NOBR t + @@ print_term is_pseudo_fun thm vars NOBR t ) end - in - (Pretty.block o Pretty.fbreaks o shift) ( - pr_eq definer eq - :: map (pr_eq "|") eqs' - ) + val shift = if null eqs then I else + map (Pretty.block o single o Pretty.block o single); + in pair + (print_val_decl print_typscheme (name, vs_ty)) + ((Pretty.block o Pretty.fbreaks o shift) ( + print_eqn definer eq + :: map (print_eqn "|") eqs + )) end - | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = + | print_def is_pseudo_fun _ definer + (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) = let - fun pr_superclass (_, (classrel, dss)) = + fun print_superinst (_, (classrel, dss)) = concat [ (str o Long_Name.base_name o deresolve) classrel, str "=", - pr_dicts is_pseudo_fun NOBR [DictConst dss] + print_dict is_pseudo_fun NOBR (DictConst dss) ]; - fun pr_classparam ((classparam, c_inst), (thm, _)) = + fun print_classparam ((classparam, c_inst), (thm, _)) = concat [ (str o Long_Name.base_name o deresolve) classparam, str "=", - pr_app (K false) thm reserved NOBR (c_inst, []) + print_app (K false) thm reserved NOBR (c_inst, []) ]; - in - concat ( + in pair + (print_val_decl print_dicttypscheme + (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) + (concat ( str definer :: (str o deresolve) inst :: (if is_pseudo_fun inst then [str "()"] - else pr_tyvar_dicts is_pseudo_fun arity) + else print_dict_args vs) @ str "=" - :: Pretty.enum "," "{" "}" - (map pr_superclass superarities @ map pr_classparam classparam_insts) + :: Pretty.list "{" "}" + (map print_superinst superinsts @ map print_classparam classparams) :: str ":" - @@ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) - ) + @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) + )) end; - fun pr_stmt (ML_Exc (name, n)) = - (concat o map str) ( + fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair + [print_val_decl print_typscheme (name, vs_ty)] + ((semicolon o map str) ( (if n = 0 then "val" else "fun") :: deresolve name :: replicate n "_" @ "=" :: "raise" :: "Fail" - @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";" - ) - | pr_stmt (ML_Val binding) = - semicolon [pr_binding (K false) true "val" binding] - | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name + )) + | print_stmt (ML_Val binding) = let - val pr_binding' = pr_binding (member (op =) pseudo_funs) false; - fun pr_pseudo_fun name = concat [ + val (sig_p, p) = print_def (K false) true "val" binding + in pair + [sig_p] + (semicolon [p]) + end + | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + let + val print_def' = print_def (member (op =) pseudo_funs) false; + fun print_pseudo_fun name = concat [ str "val", (str o deresolve) name, str "=", (str o deresolve) name, str "();" ]; - val (ps, p) = split_last - (pr_binding' "fun" binding :: map (pr_binding' "and") bindings); - val pseudo_ps = map pr_pseudo_fun pseudo_funs; - in Pretty.chunks (ps @ Pretty.block ([p, str ";"]) :: pseudo_ps) end - | pr_stmt (ML_Datas (datas as (data :: datas'))) = + val (sig_ps, (ps, p)) = (apsnd split_last o split_list) + (print_def' "fun" binding :: map (print_def' "and") bindings); + val pseudo_ps = map print_pseudo_fun pseudo_funs; + in pair + sig_ps + (Pretty.chunks (ps @ semicolon [p] :: pseudo_ps)) + end + | print_stmt (ML_Datas [(tyco, (vs, []))]) = + let + val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); + in + pair + [concat [str "type", ty_p]] + (concat [str "datatype", ty_p, str "=", str "EMPTY__"]) + end + | print_stmt (ML_Datas (data :: datas)) = let - fun pr_co (co, []) = - str (deresolve co) - | pr_co (co, tys) = - concat [ - str (deresolve co), - str "of", - Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) - ]; - fun pr_data definer (tyco, (vs, [])) = - concat ( - str definer - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs) - :: str "=" - @@ str "EMPTY__" - ) - | pr_data definer (tyco, (vs, cos)) = - concat ( - str definer - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs) - :: str "=" - :: separate (str "|") (map pr_co cos) - ); - val (ps, p) = split_last - (pr_data "datatype" data :: map (pr_data "and") datas'); - in Pretty.chunks (ps @| Pretty.block ([p, str ";"])) end - | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) = + val sig_ps = print_datatype_decl "datatype" data + :: map (print_datatype_decl "and") datas; + val (ps, p) = split_last sig_ps; + in pair + sig_ps + (Pretty.chunks (ps @| semicolon [p])) + end + | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) = let - val w = first_upper v ^ "_"; - fun pr_superclass_field (class, classrel) = - (concat o map str) [ - deresolve classrel, ":", "'" ^ v, deresolve class - ]; - fun pr_classparam_field (classparam, ty) = - concat [ - (str o deresolve) classparam, str ":", pr_typ NOBR ty - ]; - fun pr_classparam_proj (classparam, _) = - semicolon [ - str "fun", - (str o deresolve) classparam, - Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], - str "=", - str ("#" ^ deresolve classparam), - str w - ]; - fun pr_superclass_proj (_, classrel) = - semicolon [ - str "fun", - (str o deresolve) classrel, - Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)], - str "=", - str ("#" ^ deresolve classrel), - str w - ]; - in - Pretty.chunks ( + fun print_field s p = concat [str s, str ":", p]; + fun print_proj s p = semicolon + (map str ["val", s, "=", "#" ^ s, ":"] @| p); + fun print_superclass_decl (superclass, classrel) = + print_val_decl print_dicttypscheme + (classrel, ([(v, [class])], (superclass, ITyVar v))); + fun print_superclass_field (superclass, classrel) = + print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v)); + fun print_superclass_proj (superclass, classrel) = + print_proj (deresolve classrel) + (print_dicttypscheme ([(v, [class])], (superclass, ITyVar v))); + fun print_classparam_decl (classparam, ty) = + print_val_decl print_typscheme + (classparam, ([(v, [class])], ty)); + fun print_classparam_field (classparam, ty) = + print_field (deresolve classparam) (print_typ NOBR ty); + fun print_classparam_proj (classparam, ty) = + print_proj (deresolve classparam) + (print_typscheme ([(v, [class])], ty)); + in pair + (concat [str "type", print_dicttyp (class, ITyVar v)] + :: map print_superclass_decl superclasses + @ map print_classparam_decl classparams) + (Pretty.chunks ( concat [ str ("type '" ^ v), (str o deresolve) class, str "=", - Pretty.enum "," "{" "};" ( - map pr_superclass_field superclasses @ map pr_classparam_field classparams + Pretty.list "{" "};" ( + map print_superclass_field superclasses + @ map print_classparam_field classparams ) ] - :: map pr_superclass_proj superclasses - @ map pr_classparam_proj classparams - ) + :: map print_superclass_proj superclasses + @ map print_classparam_proj classparams + )) end; - in pr_stmt end; + in print_stmt end; -fun pr_sml_module name content = - Pretty.chunks ( - str ("structure " ^ name ^ " = ") - :: str "struct" - :: str "" - :: content - @ str "" - @@ str ("end; (*struct " ^ name ^ "*)") +fun print_sml_module name some_decls body = Pretty.chunks2 ( + Pretty.chunks ( + str ("structure " ^ name ^ (if is_some some_decls then " : sig" else " =")) + :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + @| (if is_some some_decls then str "end = struct" else str "struct") + ) + :: body + @| str ("end; (*struct " ^ name ^ "*)") ); val literals_sml = Literals { @@ -338,118 +356,127 @@ literal_numeral = fn unbounded => fn k => if unbounded then "(" ^ string_of_int k ^ " : IntInf.int)" else string_of_int k, - literal_list = Pretty.enum "," "[" "]", + literal_list = Pretty.list "[" "]", infix_cons = (7, "::") }; (** OCaml serializer **) -fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved deresolve is_cons = +fun print_ocaml_stmt labelled_name syntax_tyco syntax_const reserved is_cons deresolve = let - fun pr_dicts is_pseudo_fun fxy ds = - let - fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v - | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1); - fun pr_proj ps p = - fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p - fun pr_dict fxy (DictConst (inst, dss)) = - brackify fxy ((str o deresolve) inst :: - (if is_pseudo_fun inst then [str "()"] - else map (pr_dicts is_pseudo_fun BR) dss)) - | pr_dict fxy (DictVar (classrels, v)) = - pr_proj (map deresolve classrels) ((str o pr_dictvar) v) - in case ds - of [] => str "()" - | [d] => pr_dict fxy d - | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds - end; - fun pr_tyvar_dicts is_pseudo_fun vs = - vs - |> map (fn (v, sort) => map_index (fn (i, _) => - DictVar ([], (v, (i, length sort)))) sort) - |> map (pr_dicts is_pseudo_fun BR); - fun pr_tycoexpr fxy (tyco, tys) = - let - val tyco' = (str o deresolve) tyco - in case map (pr_typ BR) tys - of [] => tyco' - | [p] => Pretty.block [p, Pretty.brk 1, tyco'] - | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco'] - end - and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco - of NONE => pr_tycoexpr fxy (tyco, tys) - | SOME (i, pr) => pr pr_typ fxy tys) - | pr_typ fxy (ITyVar v) = str ("'" ^ v); - fun pr_term is_pseudo_fun thm vars fxy (IConst c) = - pr_app is_pseudo_fun thm vars fxy (c, []) - | pr_term is_pseudo_fun thm vars fxy (IVar NONE) = + fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco + | print_tyco_expr fxy (tyco, [ty]) = + concat [print_typ BR ty, (str o deresolve) tyco] + | print_tyco_expr fxy (tyco, tys) = + concat [Pretty.list "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco] + and print_typ fxy (tyco `%% tys) = (case syntax_tyco tyco + of NONE => print_tyco_expr fxy (tyco, tys) + | SOME (i, print) => print print_typ fxy tys) + | print_typ fxy (ITyVar v) = str ("'" ^ v); + fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]); + fun print_typscheme_prefix (vs, p) = Pretty.enum " ->" "" "" + (map_filter (fn (v, sort) => + (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p); + fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty); + fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty); + fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) = + brackify fxy ((str o deresolve) inst :: + (if is_pseudo_fun inst then [str "()"] + else map_filter (print_dicts is_pseudo_fun BR) dss)) + | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) = + str (if k = 1 then "_" ^ first_upper v + else "_" ^ first_upper v ^ string_of_int (i+1)) + |> fold_rev (fn classrel => fn p => + Pretty.block [p, str ".", (str o deresolve) classrel]) classrels + and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); + val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR + (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); + fun print_term is_pseudo_fun thm vars fxy (IConst c) = + print_app is_pseudo_fun thm vars fxy (c, []) + | print_term is_pseudo_fun thm vars fxy (IVar NONE) = str "_" - | pr_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = + | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = str (lookup_var vars v) - | pr_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = + | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = (case Code_Thingol.unfold_const_app t - of SOME c_ts => pr_app is_pseudo_fun thm vars fxy c_ts - | NONE => - brackify fxy [pr_term is_pseudo_fun thm vars NOBR t1, pr_term is_pseudo_fun thm vars BR t2]) - | pr_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = + of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts + | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, + print_term is_pseudo_fun thm vars BR t2]) + | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = let val (binds, t') = Code_Thingol.unfold_pat_abs t; - val (ps, vars') = fold_map (pr_bind is_pseudo_fun thm BR o fst) binds vars; - in brackets (str "fun" :: ps @ str "->" @@ pr_term is_pseudo_fun thm vars' NOBR t') end - | pr_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0 + val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars; + in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end + | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = + (case Code_Thingol.unfold_const_app t0 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) - then pr_case is_pseudo_fun thm vars fxy cases - else pr_app is_pseudo_fun thm vars fxy c_ts - | NONE => pr_case is_pseudo_fun thm vars fxy cases) - and pr_app' is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = + then print_case is_pseudo_fun thm vars fxy cases + else print_app is_pseudo_fun thm vars fxy c_ts + | NONE => print_case is_pseudo_fun thm vars fxy cases) + and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then - if length tys = length ts - then case ts - of [] => [(str o deresolve) c] - | [t] => [(str o deresolve) c, pr_term is_pseudo_fun thm vars BR t] - | _ => [(str o deresolve) c, Pretty.enum "," "(" ")" - (map (pr_term is_pseudo_fun thm vars NOBR) ts)] - else [pr_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand (length tys) app)] + let val k = length tys in + if length ts = k + then (str o deresolve) c + :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) + else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] + end else if is_pseudo_fun c then (str o deresolve) c @@ str "()" - else (str o deresolve) c - :: ((map (pr_dicts is_pseudo_fun BR) o filter_out null) iss @ map (pr_term is_pseudo_fun thm vars BR) ts) - and pr_app is_pseudo_fun = gen_pr_app (pr_app' is_pseudo_fun) (pr_term is_pseudo_fun) - syntax_const - and pr_bind is_pseudo_fun = gen_pr_bind (pr_term is_pseudo_fun) - and pr_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = + else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss + @ map (print_term is_pseudo_fun thm vars BR) ts + and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) + (print_term is_pseudo_fun) syntax_const thm vars + and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) + and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = let val (binds, body) = Code_Thingol.unfold_let (ICase cases); - fun pr ((pat, ty), t) vars = + fun print_let ((pat, ty), t) vars = vars - |> pr_bind is_pseudo_fun thm NOBR pat + |> print_bind is_pseudo_fun thm NOBR pat |>> (fn p => concat - [str "let", p, str "=", pr_term is_pseudo_fun thm vars NOBR t, str "in"]) - val (ps, vars') = fold_map pr binds vars; + [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"]) + val (ps, vars') = fold_map print_let binds vars; in brackify_block fxy (Pretty.chunks ps) [] - (pr_term is_pseudo_fun thm vars' NOBR body) + (print_term is_pseudo_fun thm vars' NOBR body) end - | pr_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = + | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = let - fun pr delim (pat, body) = + fun print_select delim (pat, body) = let - val (p, vars') = pr_bind is_pseudo_fun thm NOBR pat vars; - in concat [str delim, p, str "->", pr_term is_pseudo_fun thm vars' NOBR body] end; + val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; + in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end; in brackets ( str "match" - :: pr_term is_pseudo_fun thm vars NOBR t - :: pr "with" clause - :: map (pr "|") clauses + :: print_term is_pseudo_fun thm vars NOBR t + :: print_select "with" clause + :: map (print_select "|") clauses ) end - | pr_case is_pseudo_fun thm vars fxy ((_, []), _) = + | print_case is_pseudo_fun thm vars fxy ((_, []), _) = (concat o map str) ["failwith", "\"empty case\""]; - fun pr_binding is_pseudo_fun needs_typ definer (ML_Function (name, ((vs, ty), eqs))) = + fun print_val_decl print_typscheme (name, typscheme) = concat + [str "val", str (deresolve name), str ":", print_typscheme typscheme]; + fun print_datatype_decl definer (tyco, (vs, cos)) = + let + fun print_co (co, []) = str (deresolve co) + | print_co (co, tys) = concat [str (deresolve co), str "of", + Pretty.enum " *" "" "" (map (print_typ (INFX (2, X))) tys)]; + in + concat ( + str definer + :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs) + :: str "=" + :: separate (str "|") (map print_co cos) + ) + end; + fun print_def is_pseudo_fun needs_typ definer + (ML_Function (name, (vs_ty as (vs, ty), eqs))) = let - fun pr_eq ((ts, t), (thm, _)) = + fun print_eqn ((ts, t), (thm, _)) = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; val vars = reserved @@ -459,11 +486,11 @@ (insert (op =)) ts []); in concat [ (Pretty.block o Pretty.commas) - (map (pr_term is_pseudo_fun thm vars NOBR) ts), + (map (print_term is_pseudo_fun thm vars NOBR) ts), str "->", - pr_term is_pseudo_fun thm vars NOBR t + print_term is_pseudo_fun thm vars NOBR t ] end; - fun pr_eqs is_pseudo [((ts, t), (thm, _))] = + fun print_eqns is_pseudo [((ts, t), (thm, _))] = let val consts = fold Code_Thingol.add_constnames (t :: ts) []; val vars = reserved @@ -474,22 +501,22 @@ in concat ( (if is_pseudo then [str "()"] - else map (pr_term is_pseudo_fun thm vars BR) ts) + else map (print_term is_pseudo_fun thm vars BR) ts) @ str "=" - @@ pr_term is_pseudo_fun thm vars NOBR t + @@ print_term is_pseudo_fun thm vars NOBR t ) end - | pr_eqs _ (eqs as (eq as (([_], _), _)) :: eqs') = + | print_eqns _ ((eq as (([_], _), _)) :: eqs) = Pretty.block ( str "=" :: Pretty.brk 1 :: str "function" :: Pretty.brk 1 - :: pr_eq eq + :: print_eqn eq :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] - o single o pr_eq) eqs' + o single o print_eqn) eqs ) - | pr_eqs _ (eqs as eq :: eqs') = + | print_eqns _ (eqs as eq :: eqs') = let val consts = fold Code_Thingol.add_constnames (map (snd o fst) eqs) []; val vars = reserved @@ -508,142 +535,143 @@ :: Pretty.brk 1 :: str "with" :: Pretty.brk 1 - :: pr_eq eq + :: print_eqn eq :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1] - o single o pr_eq) eqs' + o single o print_eqn) eqs' ) end; val prolog = if needs_typ then - concat [str definer, (str o deresolve) name, str ":", pr_typ NOBR ty] + concat [str definer, (str o deresolve) name, str ":", print_typ NOBR ty] else Pretty.strs [definer, deresolve name]; - in - concat ( + in pair + (print_val_decl print_typscheme (name, vs_ty)) + (concat ( prolog - :: pr_tyvar_dicts is_pseudo_fun (filter_out (null o snd) vs) - @| pr_eqs (is_pseudo_fun name) eqs - ) + :: print_dict_args vs + @| print_eqns (is_pseudo_fun name) eqs + )) end - | pr_binding is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) = + | print_def is_pseudo_fun _ definer (ML_Instance (inst, ((class, (tyco, vs)), (superinsts, classparams)))) = let - fun pr_superclass (_, (classrel, dss)) = + fun print_superinst (_, (classrel, dss)) = concat [ (str o deresolve) classrel, str "=", - pr_dicts is_pseudo_fun NOBR [DictConst dss] + print_dict is_pseudo_fun NOBR (DictConst dss) ]; - fun pr_classparam_inst ((classparam, c_inst), (thm, _)) = + fun print_classparam ((classparam, c_inst), (thm, _)) = concat [ (str o deresolve) classparam, str "=", - pr_app (K false) thm reserved NOBR (c_inst, []) + print_app (K false) thm reserved NOBR (c_inst, []) ]; - in - concat ( + in pair + (print_val_decl print_dicttypscheme + (inst, (vs, (class, tyco `%% map (ITyVar o fst) vs)))) + (concat ( str definer :: (str o deresolve) inst - :: pr_tyvar_dicts is_pseudo_fun arity + :: print_dict_args vs @ str "=" @@ brackets [ - enum_default "()" ";" "{" "}" (map pr_superclass superarities - @ map pr_classparam_inst classparam_insts), + enum_default "()" ";" "{" "}" (map print_superinst superinsts + @ map print_classparam classparams), str ":", - pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity]) + print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs]) ] - ) + )) end; - fun pr_stmt (ML_Exc (name, n)) = - (concat o map str) ( + fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair + [print_val_decl print_typscheme (name, vs_ty)] + ((doublesemicolon o map str) ( "let" :: deresolve name :: replicate n "_" @ "=" :: "failwith" - @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name ^ ";;" - ) - | pr_stmt (ML_Val binding) = - Pretty.block [pr_binding (K false) true "let" binding, str ";;"] - | pr_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + @@ (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name + )) + | print_stmt (ML_Val binding) = let - val pr_binding' = pr_binding (member (op =) pseudo_funs) false; - fun pr_pseudo_fun name = concat [ + val (sig_p, p) = print_def (K false) true "let" binding + in pair + [sig_p] + (doublesemicolon [p]) + end + | print_stmt (ML_Funs (binding :: bindings, pseudo_funs)) = + let + val print_def' = print_def (member (op =) pseudo_funs) false; + fun print_pseudo_fun name = concat [ str "let", (str o deresolve) name, str "=", (str o deresolve) name, str "();;" ]; - val (ps, p) = split_last - (pr_binding' "let rec" binding :: map (pr_binding' "and") bindings); - val pseudo_ps = map pr_pseudo_fun pseudo_funs; - in Pretty.chunks (ps @ Pretty.block ([p, str ";;"]) :: pseudo_ps) end - | pr_stmt (ML_Datas (datas as (data :: datas'))) = + val (sig_ps, (ps, p)) = (apsnd split_last o split_list) + (print_def' "let rec" binding :: map (print_def' "and") bindings); + val pseudo_ps = map print_pseudo_fun pseudo_funs; + in pair + sig_ps + (Pretty.chunks (ps @ doublesemicolon [p] :: pseudo_ps)) + end + | print_stmt (ML_Datas [(tyco, (vs, []))]) = + let + val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs); + in + pair + [concat [str "type", ty_p]] + (concat [str "type", ty_p, str "=", str "EMPTY__"]) + end + | print_stmt (ML_Datas (data :: datas)) = let - fun pr_co (co, []) = - str (deresolve co) - | pr_co (co, tys) = - concat [ - str (deresolve co), - str "of", - Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys) - ]; - fun pr_data definer (tyco, (vs, [])) = - concat ( - str definer - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs) - :: str "=" - @@ str "EMPTY_" - ) - | pr_data definer (tyco, (vs, cos)) = - concat ( - str definer - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs) - :: str "=" - :: separate (str "|") (map pr_co cos) - ); - val (ps, p) = split_last - (pr_data "type" data :: map (pr_data "and") datas'); - in Pretty.chunks (ps @| Pretty.block ([p, str ";;"])) end - | pr_stmt (ML_Class (class, (v, (superclasses, classparams)))) = + val sig_ps = print_datatype_decl "type" data + :: map (print_datatype_decl "and") datas; + val (ps, p) = split_last sig_ps; + in pair + sig_ps + (Pretty.chunks (ps @| doublesemicolon [p])) + end + | print_stmt (ML_Class (class, (v, (superclasses, classparams)))) = let + fun print_field s p = concat [str s, str ":", p]; + fun print_superclass_field (superclass, classrel) = + print_field (deresolve classrel) (print_dicttyp (superclass, ITyVar v)); + fun print_classparam_decl (classparam, ty) = + print_val_decl print_typscheme + (classparam, ([(v, [class])], ty)); + fun print_classparam_field (classparam, ty) = + print_field (deresolve classparam) (print_typ NOBR ty); val w = "_" ^ first_upper v; - fun pr_superclass_field (class, classrel) = - (concat o map str) [ - deresolve classrel, ":", "'" ^ v, deresolve class - ]; - fun pr_classparam_field (classparam, ty) = - concat [ - (str o deresolve) classparam, str ":", pr_typ NOBR ty - ]; - fun pr_classparam_proj (classparam, _) = - concat [ - str "let", - (str o deresolve) classparam, - str w, + fun print_classparam_proj (classparam, _) = + (concat o map str) ["let", deresolve classparam, w, "=", + w ^ "." ^ deresolve classparam ^ ";;"]; + val type_decl_p = concat [ + str ("type '" ^ v), + (str o deresolve) class, str "=", - str (w ^ "." ^ deresolve classparam ^ ";;") + enum_default "unit" ";" "{" "}" ( + map print_superclass_field superclasses + @ map print_classparam_field classparams + ) ]; - in Pretty.chunks ( - concat [ - str ("type '" ^ v), - (str o deresolve) class, - str "=", - enum_default "unit;;" ";" "{" "};;" ( - map pr_superclass_field superclasses - @ map pr_classparam_field classparams - ) - ] - :: map pr_classparam_proj classparams - ) end; - in pr_stmt end; + in pair + (type_decl_p :: map print_classparam_decl classparams) + (Pretty.chunks ( + doublesemicolon [type_decl_p] + :: map print_classparam_proj classparams + )) + end; + in print_stmt end; -fun pr_ocaml_module name content = - Pretty.chunks ( - str ("module " ^ name ^ " = ") - :: str "struct" - :: str "" - :: content - @ str "" - @@ str ("end;; (*struct " ^ name ^ "*)") +fun print_ocaml_module name some_decls body = Pretty.chunks2 ( + Pretty.chunks ( + str ("module " ^ name ^ (if is_some some_decls then " : sig" else " =")) + :: (the_list o Option.map (Pretty.indent 2 o Pretty.chunks)) some_decls + @| (if is_some some_decls then str "end = struct" else str "struct") + ) + :: body + @| str ("end;; (*struct " ^ name ^ "*)") ); val literals_ocaml = let @@ -736,8 +764,8 @@ | _ => (eqs, NONE) else (eqs, NONE) in (ML_Function (name, (tysm, eqs')), is_value) end - | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, arity)), _))) = - (ML_Instance (name, stmt), if null arity then SOME (name, false) else NONE) + | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = + (ML_Instance (name, stmt), if forall (null o snd) vs then SOME (name, false) else NONE) | ml_binding_of_stmt (name, _) = error ("Binding block containing illegal statement: " ^ labelled_name name) fun add_fun (name, stmt) = @@ -745,7 +773,8 @@ val (binding, some_value_name) = ml_binding_of_stmt (name, stmt); val ml_stmt = case binding of ML_Function (name, ((vs, ty), [])) => - ML_Exc (name, (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty) + ML_Exc (name, ((vs, ty), + (length o filter_out (null o snd)) vs + (length o fst o Code_Thingol.unfold_fun) ty)) | _ => case some_value_name of NONE => ML_Funs ([binding], []) | SOME (name, true) => ML_Funs ([binding], [name]) @@ -869,34 +898,35 @@ error ("Unknown statement name: " ^ labelled_name name); in (deresolver, nodes) end; -fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved includes raw_module_alias - _ syntax_tyco syntax_const program stmt_names destination = +fun serialize_ml target compile print_module print_stmt raw_module_name with_signatures labelled_name + reserved includes raw_module_alias _ syntax_tyco syntax_const program stmt_names destination = let val is_cons = Code_Thingol.is_cons program; - val present_stmt_names = Code_Target.stmt_names_of_destination destination; - val is_present = not (null present_stmt_names); - val module_name = if is_present then SOME "Code" else raw_module_name; + val presentation_stmt_names = Code_Target.stmt_names_of_destination destination; + val is_presentation = not (null presentation_stmt_names); + val module_name = if is_presentation then SOME "Code" else raw_module_name; val (deresolver, nodes) = ml_node_of_program labelled_name module_name reserved raw_module_alias program; val reserved = make_vars reserved; - fun pr_node prefix (Dummy _) = + fun print_node prefix (Dummy _) = NONE - | pr_node prefix (Stmt (_, stmt)) = if is_present andalso - (null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt + | print_node prefix (Stmt (_, stmt)) = if is_presentation andalso + (null o filter (member (op =) presentation_stmt_names) o stmt_names_of) stmt then NONE - else SOME - (pr_stmt labelled_name syntax_tyco syntax_const reserved - (deresolver prefix) is_cons stmt) - | pr_node prefix (Module (module_name, (_, nodes))) = - separate (str "") - ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes) - o rev o flat o Graph.strong_conn) nodes) - |> (if is_present then Pretty.chunks else pr_module module_name) - |> SOME; + else SOME (print_stmt labelled_name syntax_tyco syntax_const reserved is_cons (deresolver prefix) stmt) + | print_node prefix (Module (module_name, (_, nodes))) = + let + val (decls, body) = print_nodes (prefix @ [module_name]) nodes; + val p = if is_presentation then Pretty.chunks2 body + else print_module module_name (if with_signatures then SOME decls else NONE) body; + in SOME ([], p) end + and print_nodes prefix nodes = (map_filter (print_node prefix o Graph.get_node nodes) + o rev o flat o Graph.strong_conn) nodes + |> split_list + |> (fn (decls, body) => (flat decls, body)) val stmt_names' = (map o try) (deresolver (if is_some module_name then the_list module_name else [])) stmt_names; - val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter - (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes)); + val p = Pretty.chunks2 (map snd includes @ snd (print_nodes [] nodes)); in Code_Target.mk_serialization target (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE) @@ -909,9 +939,16 @@ (** ML (system language) code for evaluation and instrumentalization **) -fun eval_code_of some_target thy = Code_Target.serialize_custom thy (the_default target_Eval some_target, - (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME ""), - literals_sml)); +val eval_struct_name = "Code" + +fun eval_code_of some_target with_struct thy = + let + val target = the_default target_Eval some_target; + val serialize = if with_struct then fn _ => fn [] => + serialize_ml target_SML (SOME (K ())) print_sml_module print_sml_stmt (SOME eval_struct_name) true + else fn _ => fn [] => + serialize_ml target_SML (SOME (K ())) ((K o K) Pretty.chunks2) print_sml_stmt (SOME eval_struct_name) true; + in Code_Target.serialize_custom thy (target, (serialize, literals_sml)) end; (* evaluation *) @@ -928,7 +965,7 @@ |> Graph.new_node (value_name, Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))]))) |> fold (curry Graph.add_edge value_name) deps; - val (value_code, [SOME value_name']) = eval_code_of some_target thy naming program' [value_name]; + val (value_code, [SOME value_name']) = eval_code_of some_target false thy naming program' [value_name]; val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name' ^ space_implode " " (map (enclose "(" ")") args) ^ " end"; in ML_Context.evaluate ctxt false reff sml_code end; @@ -952,7 +989,7 @@ let val (consts', (naming, program)) = Code_Thingol.consts_program thy consts; val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; - val (ml_code, target_names) = eval_code_of NONE thy naming program (consts' @ tycos'); + val (ml_code, target_names) = eval_code_of NONE true thy naming program (consts' @ tycos'); val (consts'', tycos'') = chop (length consts') target_names; val consts_map = map2 (fn const => fn NONE => error ("Constant " ^ (quote o Code.string_of_const thy) const @@ -970,7 +1007,7 @@ val tycos' = fold (insert (op =)) new_tycos tycos; val consts' = fold (insert (op =)) new_consts consts; val (struct_name', ctxt') = if struct_name = "" - then ML_Antiquote.variant "Code" ctxt + then ML_Antiquote.variant eval_struct_name ctxt else (struct_name, ctxt); val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) tycos' consts'); in CodeAntiqData.put ((tycos', consts'), (false, (struct_name', acc_code))) ctxt' end; @@ -998,9 +1035,8 @@ fun print_code struct_name is_first print_it ctxt = let val (_, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt; - val (raw_ml_code, (tycos_map, consts_map)) = Lazy.force acc_code; - val ml_code = if is_first then "\nstructure " ^ struct_code_name - ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n" + val (ml_code, (tycos_map, consts_map)) = Lazy.force acc_code; + val ml_code = if is_first then ml_code else ""; val all_struct_name = Long_Name.append struct_name struct_code_name; in (ml_code, print_it all_struct_name tycos_map consts_map) end; @@ -1038,31 +1074,31 @@ >> ml_code_datatype_antiq); fun isar_seri_sml module_name = - Code_Target.parse_args (Scan.succeed ()) - #> (fn () => serialize_ml target_SML + Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true + >> (fn with_signatures => serialize_ml target_SML (SOME (use_text ML_Env.local_context (1, "generated code") false)) - pr_sml_module pr_sml_stmt module_name); + print_sml_module print_sml_stmt module_name with_signatures)); fun isar_seri_ocaml module_name = - Code_Target.parse_args (Scan.succeed ()) - #> (fn () => serialize_ml target_OCaml NONE - pr_ocaml_module pr_ocaml_stmt module_name); + Code_Target.parse_args (Scan.optional (Args.$$$ "no_signatures" >> K false) true + >> (fn with_signatures => serialize_ml target_OCaml NONE + print_ocaml_module print_ocaml_stmt module_name with_signatures)); val setup = Code_Target.add_target (target_SML, (isar_seri_sml, literals_sml)) #> Code_Target.add_target (target_OCaml, (isar_seri_ocaml, literals_ocaml)) #> Code_Target.extend_target (target_Eval, (target_SML, K I)) - #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => + #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy [ - pr_typ (INFX (1, X)) ty1, + print_typ (INFX (1, X)) ty1, str "->", - pr_typ (INFX (1, R)) ty2 + print_typ (INFX (1, R)) ty2 ])) - #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] => + #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => brackify_infix (1, R) fxy [ - pr_typ (INFX (1, X)) ty1, + print_typ (INFX (1, X)) ty1, str "->", - pr_typ (INFX (1, R)) ty2 + print_typ (INFX (1, R)) ty2 ])) #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names #> fold (Code_Target.add_reserved target_SML) diff -r c54498f88a77 -r e4fb0daadcff src/Tools/Code/code_printer.ML --- a/src/Tools/Code/code_printer.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/Tools/Code/code_printer.ML Sat Dec 05 10:18:23 2009 +0100 @@ -11,7 +11,7 @@ type const = Code_Thingol.const type dict = Code_Thingol.dict - val nerror: thm -> string -> 'a + val eqn_error: thm -> string -> 'a val @@ : 'a * 'a -> 'a list val @| : 'a list * 'a -> 'a list @@ -19,6 +19,7 @@ val concat: Pretty.T list -> Pretty.T val brackets: Pretty.T list -> Pretty.T val semicolon: Pretty.T list -> Pretty.T + val doublesemicolon: Pretty.T list -> Pretty.T val enum_default: string -> string -> string -> string -> Pretty.T list -> Pretty.T val first_upper: string -> string @@ -68,11 +69,11 @@ -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option val activate_const_syntax: theory -> literals -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming - val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list) + val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list) -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> (string -> const_syntax option) -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T - val gen_pr_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) + val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T) -> thm -> fixity -> iterm -> var_ctxt -> Pretty.T * var_ctxt @@ -86,7 +87,7 @@ open Code_Thingol; -fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm); +fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm); (** assembling text pieces **) @@ -98,6 +99,7 @@ val concat = Pretty.block o Pretty.breaks; val brackets = Pretty.enclose "(" ")" o Pretty.breaks; fun semicolon ps = Pretty.block [concat ps, str ";"]; +fun doublesemicolon ps = Pretty.block [concat ps, str ";;"]; fun enum_default default sep opn cls [] = str default | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs; @@ -182,11 +184,11 @@ fun fixity NOBR _ = false | fixity _ NOBR = false - | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) = - pr < pr_ctxt - orelse pr = pr_ctxt + | fixity (INFX (pr, lr)) (INFX (print_ctxt, lr_ctxt)) = + pr < print_ctxt + orelse pr = print_ctxt andalso fixity_lrx lr lr_ctxt - orelse pr_ctxt = ~1 + orelse print_ctxt = ~1 | fixity BR (INFX _) = false | fixity _ _ = true; @@ -219,32 +221,32 @@ -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)); fun simple_const_syntax (SOME (n, f)) = SOME (n, - ([], (fn _ => fn _ => fn pr => fn thm => fn vars => f (pr vars)))) + ([], (fn _ => fn _ => fn print => fn thm => fn vars => f (print vars)))) | simple_const_syntax NONE = NONE; fun activate_const_syntax thy literals (n, (cs, f)) naming = fold_map (Code_Thingol.ensure_declared_const thy) cs naming |-> (fn cs' => pair (n, f literals cs')); -fun gen_pr_app pr_app pr_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) = +fun gen_print_app print_app_expr print_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) = case syntax_const c - of NONE => brackify fxy (pr_app thm vars app) - | SOME (k, pr) => + of NONE => brackify fxy (print_app_expr thm vars app) + | SOME (k, print) => let - fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ take k tys); + fun print' fxy ts = print (print_term thm) thm vars fxy (ts ~~ take k tys); in if k = length ts - then pr' fxy ts + then print' fxy ts else if k < length ts then case chop k ts of (ts1, ts2) => - brackify fxy (pr' APP ts1 :: map (pr_term thm vars BR) ts2) - else pr_term thm vars fxy (Code_Thingol.eta_expand k app) + brackify fxy (print' APP ts1 :: map (print_term thm vars BR) ts2) + else print_term thm vars fxy (Code_Thingol.eta_expand k app) end; -fun gen_pr_bind pr_term thm (fxy : fixity) pat vars = +fun gen_print_bind print_term thm (fxy : fixity) pat vars = let val vs = Code_Thingol.fold_varnames (insert (op =)) pat []; val vars' = intro_vars vs vars; - in (pr_term thm vars' fxy pat, vars') end; + in (print_term thm vars' fxy pat, vars') end; (* mixfix syntax *) @@ -260,13 +262,13 @@ val i = (length o filter is_arg) mfx; fun fillin _ [] [] = [] - | fillin pr (Arg fxy :: mfx) (a :: args) = - (pr fxy o prep_arg) a :: fillin pr mfx args - | fillin pr (Pretty p :: mfx) args = - p :: fillin pr mfx args; + | fillin print (Arg fxy :: mfx) (a :: args) = + (print fxy o prep_arg) a :: fillin print mfx args + | fillin print (Pretty p :: mfx) args = + p :: fillin print mfx args; in - (i, fn pr => fn fixity_ctxt => fn args => - gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args)) + (i, fn print => fn fixity_ctxt => fn args => + gen_brackify (fixity fixity_this fixity_ctxt) (fillin print mfx args)) end; fun parse_infix prep_arg (x, i) s = diff -r c54498f88a77 -r e4fb0daadcff src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Fri Dec 04 22:51:59 2009 +0100 +++ b/src/Tools/Code/code_thingol.ML Sat Dec 05 10:18:23 2009 +0100 @@ -488,9 +488,9 @@ | map_terms_stmt f (stmt as Class _) = stmt | map_terms_stmt f (stmt as Classrel _) = stmt | map_terms_stmt f (stmt as Classparam _) = stmt - | map_terms_stmt f (Classinst (arity, (superarities, classparms))) = - Classinst (arity, (superarities, (map o apfst o apsnd) (fn const => - case f (IConst const) of IConst const' => const') classparms)); + | map_terms_stmt f (Classinst (arity, (superinsts, classparams))) = + Classinst (arity, (superinsts, (map o apfst o apsnd) (fn const => + case f (IConst const) of IConst const' => const') classparams)); fun is_cons program name = case Graph.get_node program name of Datatypecons _ => true @@ -677,8 +677,8 @@ ##>> fold_map (translate_tyvar_sort thy algbr eqngr) vs ##>> fold_map translate_superarity superclasses ##>> fold_map translate_classparam_inst classparams - #>> (fn ((((class, tyco), arity), superarities), classparams) => - Classinst ((class, (tyco, arity)), (superarities, classparams))); + #>> (fn ((((class, tyco), arity), superinsts), classparams) => + Classinst ((class, (tyco, arity)), (superinsts, classparams))); in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end and translate_typ thy algbr eqngr (TFree (v, _)) = pair (ITyVar (unprefix "'" v))