# HG changeset patch # User haftmann # Date 1168931220 -3600 # Node ID a10ad9d71eaf90add8ec65ca83dcf4933c11fd8f # Parent 8668c056c507568c3abba2983265fa6251871f1e introduced binding concept diff -r 8668c056c507 -r a10ad9d71eaf src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 16 08:06:59 2007 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 16 08:07:00 2007 +0100 @@ -62,10 +62,10 @@ val APP = INFX (~1, L); -type typ_syntax = int * ((fixity -> itype -> Pretty.T) -> fixity - -> itype list -> Pretty.T); -type term_syntax = int * ((vname list -> fixity -> iterm -> Pretty.T) -> fixity - -> iterm list -> Pretty.T); +type typ_syntax = int * ((fixity -> itype -> Pretty.T) + -> fixity -> itype list -> Pretty.T); +type term_syntax = int * ((CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) + -> CodegenNames.var_ctxt -> fixity -> iterm list -> Pretty.T); fun eval_lrx L L = false | eval_lrx R R = false @@ -153,19 +153,19 @@ (* generic serializer combinators *) -fun gen_pr_app pr_app' pr_term const_syntax fxy (app as ((c, (_, ty)), ts)) = +fun gen_pr_app pr_app' pr_term const_syntax vars fxy (app as ((c, (_, ty)), ts)) = case const_syntax c - of NONE => brackify fxy (pr_app' app) + of NONE => brackify fxy (pr_app' vars app) | SOME (i, pr) => let val k = if i < 0 then (length o fst o CodegenThingol.unfold_fun) ty else i in if k = length ts then - pr pr_term fxy ts + pr pr_term vars fxy ts else if k < length ts then case chop k ts of (ts1, ts2) => - brackify fxy (pr pr_term APP ts1 :: map (pr_term [] BR) ts2) - else pr_term [] fxy (CodegenThingol.eta_expand app k) + brackify fxy (pr pr_term vars APP ts1 :: map (pr_term vars BR) ts2) + else pr_term vars fxy (CodegenThingol.eta_expand app k) end; fun gen_pr_bind pr_bind' pr_term fxy ((v, pat), ty) vars = @@ -217,12 +217,12 @@ fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode = let - fun pretty pr fxy [t] = + fun pretty pr vars fxy [t] = case implode_list c_nil c_cons t of SOME ts => (case implode_string mk_char mk_string ts of SOME p => p - | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr [] BR t]) - | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr [] BR t] + | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t]) + | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr vars BR t] in (1, pretty) end; fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) = @@ -233,43 +233,25 @@ str target_cons, pr (INFX (target_fxy, R)) t2 ]; - fun pretty pr fxy [t1, t2] = + fun pretty pr vars fxy [t1, t2] = case Option.map (cons t1) (implode_list c_nil c_cons t2) of SOME ts => (case mk_char_string of SOME (mk_char, mk_string) => (case implode_string mk_char mk_string ts of SOME p => p - | NONE => mk_list (map (pr [] NOBR) ts)) - | NONE => mk_list (map (pr [] NOBR) ts)) - | NONE => default (pr []) fxy t1 t2; + | NONE => mk_list (map (pr vars NOBR) ts)) + | NONE => mk_list (map (pr vars NOBR) ts)) + | NONE => default (pr vars) fxy t1 t2; in (2, pretty) end; val pretty_imperative_monad_bind = let - fun pretty (pr : vname list -> fixity -> iterm -> Pretty.T) fxy [t1, (v, ty) `|-> t2] = - pr [] fxy (ICase ((t1, ty), ([(IVar v, t2)]))) - | pretty _ _ _ = error "bad arguments for imperative monad bind"; + fun pretty (pr : CodegenNames.var_ctxt -> fixity -> iterm -> Pretty.T) vars fxy [t1, (v, ty) `|-> t2] = + pr vars fxy (ICase ((t1, ty), ([(IVar v, t2)]))) + | pretty _ _ _ _ = error "bad arguments for imperative monad bind"; in (2, pretty) end; -fun pretty_haskell_monad c_mbind c_kbind = - let - fun pr_bnd pr ((SOME v, NONE), _) = str "" - | pr_bnd pr ((NONE, SOME t), _) = str "" - | pr_bnd pr ((SOME v, SOME t), _) = str ""; - fun pr_bind pr (NONE, t) = semicolon [pr [] NOBR t] - | pr_bind pr (SOME (bind, true), t) = semicolon [pr_bnd pr bind, str "<-", pr [] NOBR t] - | pr_bind pr (SOME (bind, false), t) = semicolon [str "let", pr_bnd pr bind, str "=", pr [] NOBR t]; - fun brack fxy p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p; - fun pretty pr fxy [t] = - let - val (binds, t) = implode_monad c_mbind c_kbind t; - in (brack fxy o Pretty.block_enclose (str "do {", str "}")) ( - map (pr_bind pr) binds - @| pr [] NOBR t - ) end; - in (1, pretty) end; - (** name auxiliary **) @@ -443,9 +425,7 @@ else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else (str o deresolv) c :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts) - and pr_app vars fxy (app as ((c, (iss, ty)), ts)) = - gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars)) - const_syntax fxy app + and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -723,9 +703,7 @@ else [pr_term vars BR (CodegenThingol.eta_expand app ((length o fst o CodegenThingol.unfold_fun) ty))] else (str o deresolv) c :: ((map (pr_insts BR) o filter_out null) iss @ map (pr_term vars BR) ts) - and pr_app vars fxy (app as ((c, (iss, ty)), ts)) = - gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars)) - const_syntax fxy app + and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars and pr_bind' ((NONE, NONE), _) = str "_" | pr_bind' ((SOME v, NONE), _) = str v | pr_bind' ((NONE, SOME p), _) = p @@ -1107,6 +1085,17 @@ (** Haskell serializer **) +local + +fun pr_bind' ((NONE, NONE), _) = str "_" + | pr_bind' ((SOME v, NONE), _) = str v + | pr_bind' ((NONE, SOME p), _) = p + | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p] + +val pr_bind_haskell = gen_pr_bind pr_bind'; + +in + fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv deriving_show def = let fun class_name class = case class_syntax class @@ -1203,14 +1192,8 @@ end and pr_app' vars ((c, _), ts) = (str o deresolv) c :: map (pr_term vars BR) ts - and pr_app vars fxy = - gen_pr_app (pr_app' vars) (fn vars' => pr_term (CodegenNames.intro_vars vars' vars)) - const_syntax fxy - and pr_bind' ((NONE, NONE), _) = str "_" - | pr_bind' ((SOME v, NONE), _) = str v - | pr_bind' ((NONE, SOME p), _) = p - | pr_bind' ((SOME v, SOME p), _) = brackets [str v, str "@", p] - and pr_bind fxy = gen_pr_bind pr_bind' pr_term fxy; + and pr_app vars = gen_pr_app pr_app' pr_term const_syntax vars + and pr_bind fxy = pr_bind_haskell pr_term fxy; fun pr_def (name, CodegenThingol.Fun (eqs, (vs, ty))) = let val tyvars = CodegenNames.intro_vars (map fst vs) keyword_vars; @@ -1326,6 +1309,27 @@ end; in pr_def def end; +fun pretty_haskell_monad c_mbind c_kbind = + let + fun pretty pr vars fxy [t] = + let + val pr_bind = pr_bind_haskell pr; + fun pr_mbind (NONE, t) vars = + (semicolon [pr vars NOBR t], vars) + | pr_mbind (SOME (bind, true), t) vars = vars + |> pr_bind NOBR bind + |>> (fn p => semicolon [p, str "<-", pr vars NOBR t]) + | pr_mbind (SOME (bind, false), t) vars = vars + |> pr_bind NOBR bind + |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]); + val (binds, t) = implode_monad c_mbind c_kbind t; + val (ps, vars') = fold_map pr_mbind binds vars; + fun brack p = if eval_fxy BR fxy then Pretty.block [str "(", p, str ")"] else p; + in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end; + in (1, pretty) end; + +end; (*local*) + val reserved_haskell = [ "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", "import", "default", "forall", "let", "in", "class", "qualified", "data", @@ -1581,13 +1585,16 @@ |> (CodegenSerializerData.map o Symtab.map_entry target o map_target) f end; +val target_SML = "SML"; +val target_OCaml = "OCaml"; +val target_Haskell = "Haskell"; val target_diag = "diag"; val _ = Context.add_setup ( CodegenSerializerData.init - #> add_serializer ("SML", isar_seri_sml) - #> add_serializer ("OCaml", isar_seri_ocaml) - #> add_serializer ("Haskell", isar_seri_haskell) + #> add_serializer (target_SML, isar_seri_sml) + #> add_serializer (target_OCaml, isar_seri_ocaml) + #> add_serializer (target_Haskell, isar_seri_haskell) #> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis)) ); @@ -1753,12 +1760,26 @@ else error ("No such type constructor: " ^ quote raw_tyco); in tyco end; -fun idfs_of_const_names thy c = +fun idfs_of_const thy c = let val c' = (c, Sign.the_const_type thy c); val c'' = CodegenConsts.norm_of_typ thy c'; in (c'', CodegenNames.const thy c'') end; +fun gen_add_haskell_monad prep_const c_run c_mbind c_kbind thy = + let + val c_run' = + (CodegenConsts.norm thy o prep_const thy) c_run; + val c_mbind'' = + (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_mbind; + val c_kbind'' = + (CodegenNames.const thy o CodegenConsts.norm thy o prep_const thy) c_kbind; + val pr = pretty_haskell_monad c_mbind'' c_kbind'' + in + thy + |> gen_add_syntax_const (K I) target_Haskell c_run' (SOME pr) + end; + val add_syntax_class = gen_add_syntax_class read_class CodegenConsts.read_const; val add_syntax_inst = gen_add_syntax_inst read_class read_type; val add_syntax_tyco = gen_add_syntax_tyco read_type; @@ -1790,7 +1811,7 @@ (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")")); fun no_bindings x = (Option.map o apsnd) - (fn pretty => fn pr => pretty (pr [])) x; + (fn pretty => fn pr => fn vars => pretty (pr vars)) x; val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr"); @@ -1813,8 +1834,8 @@ fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = let - val (_, nil'') = idfs_of_const_names thy nill; - val (cons', cons'') = idfs_of_const_names thy cons; + val (_, nil'') = idfs_of_const thy nill; + val (cons', cons'') = idfs_of_const thy cons; val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons; in thy @@ -1823,9 +1844,9 @@ fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy = let - val (_, nil'') = idfs_of_const_names thy nill; - val (_, cons'') = idfs_of_const_names thy cons; - val (str', _) = idfs_of_const_names thy str; + val (_, nil'') = idfs_of_const thy nill; + val (_, cons'') = idfs_of_const thy cons; + val (str', _) = idfs_of_const thy str; val pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode; in thy @@ -1834,8 +1855,8 @@ fun add_undefined target undef target_undefined thy = let - val (undef', _) = idfs_of_const_names thy undef; - fun pr _ _ _ = str target_undefined; + val (undef', _) = idfs_of_const thy undef; + fun pr _ _ _ _ = str target_undefined; in thy |> gen_add_syntax_const (K I) target undef' (SOME (~1, pr)) @@ -1843,13 +1864,15 @@ fun add_pretty_imperative_monad_bind target bind thy = let - val (bind', _) = idfs_of_const_names thy bind; + val (bind', _) = idfs_of_const thy bind; val pr = pretty_imperative_monad_bind in thy |> gen_add_syntax_const (K I) target bind' (SOME pr) end; +val add_haskell_monad = gen_add_haskell_monad CodegenConsts.read_const; + val code_classP = OuterSyntax.command code_classK "define code syntax for class" K.thy_decl ( parse_multi_syntax P.xname @@ -1881,12 +1904,12 @@ fold (fn (raw_const, syn) => add_syntax_const target raw_const (no_bindings syn)) syns) ); -(*val code_monadP = - OuterSyntax.command code_typeK "define code syntax for Haskell monads" K.thy_decl ( - parse_multi_syntax P.xname parse_syntax - >> (Toplevel.theory oo fold) (fn (target, syns) => - fold (fn (raw_tyco, syn) => add_syntax_monad target raw_tyco syn) syns) - );*) +val code_monadP = + OuterSyntax.command code_monadK "define code syntax for Haskell monads" K.thy_decl ( + P.term -- P.term -- P.term + >> (fn ((raw_run, raw_mbind), raw_kbind) => Toplevel.theory + (add_haskell_monad raw_run raw_mbind raw_kbind)) + ); val code_reservedP = OuterSyntax.command code_reservedK "declare words as reserved for target language" K.thy_decl ( @@ -1909,7 +1932,7 @@ val _ = OuterSyntax.add_keywords [infixK, infixlK, infixrK]; val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP, - code_reservedP, code_modulenameP, code_moduleprologP]; + code_reservedP, code_modulenameP, code_moduleprologP, code_monadP]; (*including serializer defaults*) val _ = Context.add_setup (