File ‹code_go.ML›
signature CODE_GO =
sig
val target: string
end;
structure Code_Go : CODE_GO =
struct
open Basic_Code_Symbol;
open Basic_Code_Thingol;
open Code_Printer;
infixr 5 @@;
infixr 5 @|;
val target = "Go";
fun map_terms_bottom_up f (t as IConst _) = f t
| map_terms_bottom_up f (t as IVar _) = f t
| map_terms_bottom_up f (t1 `$ t2) = f
(map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
| map_terms_bottom_up f ((v, ty) `|=> (t, rty)) = f
((v, ty) `|=> (map_terms_bottom_up f t, rty))
| map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
(ICase { term = map_terms_bottom_up f t, typ = ty,
clauses = (map o apply2) (map_terms_bottom_up f) clauses,
primitive = map_terms_bottom_up f t0 });
fun range_of_head t =
case fst (Code_Thingol.unfold_app t) of
IConst {range, ...} => range
val print_go_string =
let
fun unicode i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i)
fun char "\"" = "\\\""
| char "\\" = "\\\\"
| char c =
let val i = ord c
in if i < 32 orelse i > 126
then unicode i
else if i >= 128
then error "non-ASCII byte in Go string literal"
else c
end;
in quote o translate_string char end;
val block_enclose = Pretty.block_enclose o apply2 Pretty.unbreakable;
fun print_go_numeral num = "Bigint.MkInt(\"" ^ signed_string_of_int num ^ "\")";
val literals = Literals {
literal_string = print_go_string,
literal_numeral = print_go_numeral,
literal_list = Pretty.enum "," "[" "]",
infix_cons = (6, "<no infix cons operator in go>")
};
datatype go_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list
| Datatype of vname list * ((string * vname list) * itype list) list
| Class of (vname * ((class * class) list * (string * itype) list))
| Datatypecons of string
| Instance of { class: string, tyco: string, vs: (vname * sort) list,
superinsts: (class * (itype * dict list) list) list,
inst_params: ((string * (const * int)) * (thm * bool)) list,
superinst_params: ((string * (const * int)) * (thm * bool)) list };
fun print_go_stmt gen_stringer undefineds infinite_types tyco_syntax const_syntax reserved
args_num is_sum_type is_class_param is_constr (deresolve, deresolve_full) =
let
fun lookup_tyvar tyvars = lookup_var tyvars;
fun intro_tyvars vs = intro_vars (map fst vs);
val deresolve_const = deresolve o Constant;
val deresolve_class = deresolve o Type_Class;
val deresolve_classrel = deresolve o Class_Relation;
val deresolve_inst = deresolve o Class_Instance;
val deresolve_tyco = deresolve o Type_Constructor;
val oneline = Pretty.unbreakable o semicolon;
val block = Pretty.unbreakable o Pretty.block;
val spaced = Pretty.unbreakable o concat;
fun mk_dest_name name = Long_Name.map_base_name (fn s => s^"_dest") name
fun applify_constraints _ head [] = head
| applify_constraints tyvars head vs = let
val anys = (Pretty.block o Pretty.commas o map (Pretty.str o lookup_tyvar tyvars)) vs
in block [head, Pretty.str "[", anys, Pretty.brk 1, Pretty.str "any", Pretty.str "]"] end
fun print_go_typ tyvars (tyco `%% tys) = (case tyco_syntax tyco of
NONE => apply_constraints tyvars ((Pretty.str o deresolve_tyco) tyco) tys
| SOME (_, print) => print (K (print_go_typ tyvars)) NOBR tys)
| print_go_typ tyvars (ITyVar v) = (Pretty.str o lookup_tyvar tyvars) v
and apply_constraints tyvars head vs =
gen_applify false "[" "]" (print_go_typ tyvars) NOBR head vs
fun print_go_typ_uncurried_toplevel tyvars (typ as "fun" `%% _) = let
val (args, rtyp) = Code_Thingol.unfold_fun typ
val head = applify "(" ")" (print_go_typ tyvars) NOBR (Pretty.str "func") args;
in concat [head, print_go_typ tyvars rtyp] end
| print_go_typ_uncurried_toplevel tyvars typ =
block [Pretty.str "func () ", print_go_typ tyvars typ]
fun wrap_into_lambda tyvars typ body =
block_enclose
(concat [Pretty.str "func ()", print_go_typ tyvars typ, Pretty.str "{"], Pretty.str "}()") body
fun wrap_in_return t = oneline [Pretty.str "return", t]
fun wrap_if true = wrap_in_return
| wrap_if false = I
fun print_func head body = block_enclose
(Pretty.block [Pretty.str "func ", head, Pretty.str " {"], Pretty.str "}")
[body];
fun print_func_head tyvars vars const tvs extras params tys rty = let
val args = params ~~ tys
|> map (fn (param, ty) => let
val name = case param of
NONE => "_" | SOME n => lookup_var vars n;
in Pretty.block [Pretty.str name, Pretty.brk 1, print_go_typ tyvars ty] end)
|> (curry op @ extras)
|> Pretty.enum "," "(" ")"
val sym = case const of
SOME name => (Pretty.str o deresolve) name
| NONE => Pretty.str ""
val func_head = concat (applify_constraints tyvars sym tvs :: [args, rty]);
in func_head
end;
fun print_go_typedef tyco vs cos reserved = let
val [p,m] = Name.invent (snd reserved) "p" 2
val ctxt = Name.declare p (Name.declare m (snd reserved))
val tyargs = map ITyVar vs
val self = tyco `%% tyargs
val tyvars = intro_tyvars (map (rpair []) vs) reserved;
val allowed_infinite = List.exists (fn n => n = tyco) infinite_types
fun print_constructor m type_name ((name,_), tys) = let
val named_fields = Name.invent_names ctxt "A" tys
val fields = named_fields
|> map (fn (name, arg) => oneline [Pretty.str name, print_go_typ tyvars arg])
val head = applify_constraints tyvars (Pretty.str name) vs
val typ = apply_constraints tyvars (Pretty.str name) tyargs
val elim_body = if type_name = NONE
then let
val case_branch = block
[Pretty.str "return ", (Pretty.block o Pretty.commas) (map (fn (field,_) => Pretty.str (p^"."^field)) named_fields)]
in case_branch end
else Pretty.block [oneline [Pretty.str "return ", (Pretty.block o Pretty.commas) (map (fn (field,_) => Pretty.str (p^"."^field)) named_fields)]]
val elim_name = mk_dest_name (case type_name of
NONE => name
| SOME name' => name')
val eliminator = if null tys then Pretty.str "" else print_func
(applify "(" ")" I NOBR (Pretty.block [applify_constraints tyvars (Pretty.str elim_name) vs, Pretty.str ("("^p^" "), typ, Pretty.str ")"]) (map (print_go_typ tyvars o snd) named_fields))
elim_body
val pretty = name ^ "(" ^ (fold (curry (op ^)) (map (K "%v") fields) "") ^ ")"
val constr = oneline [block_enclose (concat [Pretty.str "type", head, Pretty.str "struct {"], Pretty.str "}")
fields]
in (constr, eliminator) end
in if not allowed_infinite andalso length cos = 1 then case cos of
[((name,_),tys)] => let
val name = deresolve_const name
val tname = deresolve_tyco tyco
val (constr, dest) = print_constructor m (SOME name) ((tname, []), tys)
in Pretty.chunks [constr, dest] end
else let
val (constrs, destrs) = cos
|> map (fn ((name,_),tys) => ((deresolve_const name, []),tys))
|> map (print_constructor m NONE)
|> split_list
val names = map (fn ((name,_),_) => (Pretty.str o deresolve_const) name) cos
val comment = Pretty.block (Pretty.str "// sum type which can be " :: Pretty.commas names)
val any = oneline [Pretty.str "type", applify_constraints tyvars ((Pretty.str o deresolve_tyco) tyco) vs, Pretty.str "any"]
in Pretty.chunks (comment :: any :: constrs @ destrs) end
end;
fun print_classrels [] ps = Pretty.block ps
| print_classrels rels ps = let
val postfix = rels
|> map (fn (self, super) => (Long_Name.base_name o deresolve_classrel) (self, super))
|> rev
|> String.concatWith "."
in block (ps @ [Pretty.str ".", Pretty.str postfix]) end
fun print_dict tyvars (Dict (classrels, x)) =
print_classrels classrels (print_plain_dict tyvars x)
and print_plain_dict tyvars (Dict_Const (inst, args)) = let
val needs_mono = true
val (typargs, dictss) = split_list args
val wrap = if needs_mono
then fn head => apply_constraints tyvars head typargs
else I
in wrap ((Pretty.str o deresolve_inst) inst)
:: (if needs_mono then [((Pretty.enum "," "(" ")") o map (print_dict tyvars) o flat) dictss] else []) end
| print_plain_dict tyvars (Dict_Var { var, index, length, ... }) =
[Pretty.str (if length = 1 then var ^ "_"
else var ^ string_of_int (index + 1) ^ "_")]
fun wrap_new_scope term =
block_enclose (Pretty.str "{", Pretty.str "};") [term]
fun type_of_primitive_pattern t =
let
val destructor = case fst (Code_Thingol.unfold_app t) of
IConst const => const
val extras = drop (args_num (#sym destructor)) (#dom destructor)
in extras `--> (#range destructor)
end
fun print_app_expr const_syntax tyvars some_thm vars
(app as ({ sym, dictss, dom, range, typargs, ... }, ts)) = let
val k = length dom
val l = args_num sym
in if length ts = k then
let
val is_constr = is_constr sym
val is_sum_type = is_sum_type sym
val is_class_param = is_class_param sym
val dict_args = map (print_dict tyvars) (flat dictss)
val typ = case snd (Code_Thingol.unfold_fun range) of
name `%% _ => name | ITyVar name => name
val allowed_infinite = List.exists (fn n => n = typ) infinite_types
andalso is_constr
val _ = if is_class_param andalso not (length dict_args = 1)
then warning "bug in print_app" else ()
val applify' = if is_constr
then gen_applify true "{" "}"
else gen_applify true "(" ")"
val (immediate, curried) = chop l ts
val symbol = if is_constr
then (if is_sum_type orelse allowed_infinite then sym else Type_Constructor typ)
else sym
val func_name = if is_class_param
then Pretty.block [hd dict_args, Pretty.str ".", (Pretty.str o deresolve) symbol]
else (Pretty.str o deresolve) symbol
fun wrap_type_args s = if is_sum_type orelse allowed_infinite
then applify "(" ")" I APP (apply_constraints tyvars ((Pretty.str o deresolve_tyco) typ) typargs) [s]
else s
fun wrap_type_conversion name =
let
val typargs = if is_constr
then case range of _ `%% typargs => typargs | _ => []
else typargs
in if is_class_param then name
else apply_constraints tyvars name typargs
end
val immediate_args = immediate
|> map (print_go_expr const_syntax tyvars some_thm vars BR)
val invocation = (if is_class_param orelse is_constr then immediate_args else dict_args @ immediate_args)
|> applify' I APP (wrap_type_conversion func_name)
|> wrap_type_args
val curried_args = curried
|> map (Pretty.enclose "(" ")" o single o print_go_expr const_syntax tyvars some_thm vars NOBR)
in invocation :: curried_args
end
else
[print_go_expr const_syntax tyvars some_thm vars BR (Code_Thingol.saturated_application k app)]
end
and print_clause _ _ _ _ [] _ =
raise Fail "there's a bug in the pattern-match translator"
| print_clause tyvars some_thm vars p ((target, pattern) :: subps) term =
let
fun print_condition vars conds (constr, typargs, range, args) p q target body = let
val destructor = (mk_dest_name o deresolve) constr
val (tyco, typargs) = case snd (Code_Thingol.unfold_fun range) of
a `%% typargs => (a, typargs)
val is_boxed = is_sum_type constr orelse List.exists (fn n => n = tyco) infinite_types
val names = map (fn (SOME n) => (Pretty.str o lookup_var vars) n | NONE => Pretty.str "_") args
val any_names = exists is_some args
val checks = conds
|> map (fn (var,const) => concat [
Pretty.str var,
Pretty.str "==",
Pretty.enclose "(" ")" [print_app false const_syntax tyvars some_thm vars NOBR (const, [])]
])
|> separate (Pretty.str "&&")
|> concat
in Pretty.chunks
((if is_boxed then [oneline [(Pretty.block o Pretty.commas) [Pretty.str (if any_names then q else "_"), Pretty.str p], Pretty.str ":=",
applify ".(" ")" I NOBR (Pretty.str target) [apply_constraints tyvars ((Pretty.str o deresolve) constr) typargs]]]
else [oneline [Pretty.str "_ =", Pretty.str target]])
@ [(if is_boxed then block_enclose (spaced [Pretty.str "if", Pretty.str p, Pretty.str "{"], Pretty.str "}") else Pretty.chunks)
((if any_names then [oneline ((Pretty.block o Pretty.commas) names :: [Pretty.str ":=", applify "(" ")" Pretty.str NOBR (Pretty.str destructor) [if is_boxed then q else target]])]
else [])
@ [(if null conds then Pretty.chunks else (block_enclose ((spaced [Pretty.str "if", checks, Pretty.str "{"]), Pretty.str "}")))
[body]])])
end
in case pattern
of IConst c =>
let
val checks = concat
[Pretty.str target, Pretty.str "==", Pretty.enclose "(" ")" [print_app false const_syntax tyvars some_thm vars NOBR (c, [])]]
val body = (if subps = []
then print_go_term const_syntax tyvars some_thm vars NOBR term
else print_clause tyvars some_thm vars p subps term)
in block_enclose ((spaced [Pretty.str "if", checks, Pretty.str "{"]), Pretty.str "}")
[body]
end
| _ `$ _ => (case Code_Thingol.unfold_const_app pattern of
NONE => raise Fail "bad application in pattern match"
| SOME (constr, args) => let
val ((arg_names, subpatterns, conds), vars') =
fold_rev (fn term => fn ((ts, rs, cs), vars) => case term of
IConst c => let
val [name] = Name.invent (snd vars) "c" 1
in ((SOME name :: ts, rs,(name,c) :: cs), intro_vars [name] vars) end
| IVar NONE => ((NONE :: ts, rs, cs), vars)
| IVar (SOME v) => ((SOME v :: ts, rs, cs), intro_vars [v] vars)
| _ `$ _ => let
val [name] = Name.invent (snd vars) "p" 1
in ((SOME name :: ts, (name, term) :: rs, cs), intro_vars [name] vars) end)
args (([],[],[]), vars)
val [q] = Name.invent (snd vars) "q" 1
val vars = intro_vars [q] vars
val wrapper = print_condition vars' conds (#sym constr, #typargs constr, #range constr, arg_names) p q target
val subpatterns' = subpatterns @ subps
in wrapper (if subpatterns' = []
then print_go_term const_syntax tyvars some_thm vars' NOBR term
else print_clause tyvars some_thm vars' p subpatterns' term)
end)
| IVar v => let
val vars' = intro_vars (the_list v) vars
val name_printed = case v of
NONE => Pretty.str "_" | SOME name => (Pretty.str o lookup_var vars') name
val binding = oneline [name_printed, Pretty.str ":=", Pretty.str target]
val usage = case v of
SOME _ => oneline [Pretty.str "_ =", name_printed]
| NONE => Pretty.str ""
val body = if subps = []
then print_go_term const_syntax tyvars some_thm vars' NOBR term
else print_clause tyvars some_thm vars' p subps term
in
Pretty.chunks [binding, body]
end
| _ => raise Fail "bad term in pattern"
end
and print_pattern_match is_stmt tyvars some_thm vars rtyp target clauses =
let
val [target_var] = Name.invent (snd vars) "target" 1
val vars = intro_vars [target_var] vars
val [p] = Name.invent (snd vars) "m" 1
val vars = intro_vars [p] vars
val target = print_go_expr const_syntax tyvars some_thm vars NOBR target
val assignment = oneline [Pretty.str target_var, Pretty.str ":=", target]
val body = assignment
:: map (fn (pattern,term) =>
wrap_new_scope (print_clause tyvars some_thm vars p [(target_var, pattern)] term))
clauses @ [oneline [Pretty.str "panic(\"match failed\")"]]
in if is_stmt
then Pretty.chunks body
else wrap_into_lambda tyvars rtyp body
end
and print_app is_stmt const_syntax tyvars some_thm vars fxy (app as (const, args)) =
if List.exists (fn name => #sym const = Constant name) undefineds then
args
|> map (print_go_expr const_syntax tyvars some_thm vars fxy)
|> map (fn p => oneline [ Pretty.str "_ = ", p])
|> curry (op @) [ Pretty.str ("panic(\"encountered undefined function: \" + "^print_go_string (Code_Symbol.default_base (#sym const))^")") ]
|> Pretty.chunks
else wrap_if is_stmt (gen_print_app (print_app_expr const_syntax tyvars)
(print_go_expr const_syntax tyvars) const_syntax some_thm vars fxy app)
and print_go_term const_syntax tyvars some_thm vars fxy iterm =
print_go_term_gen true const_syntax tyvars some_thm vars fxy iterm
and print_go_expr const_syntax tyvars some_thm vars fxy t =
print_go_term_gen false const_syntax tyvars some_thm vars fxy t
and print_go_term_gen is_stmt const_syntax tyvars some_thm vars fxy t = case t of
IConst (const as {sym,...}) => let
in (print_app is_stmt const_syntax tyvars some_thm vars fxy (const, [])) end
| t1 `$ t2 => (case Code_Thingol.unfold_const_app t of
SOME app =>
(print_app is_stmt const_syntax tyvars some_thm vars fxy app)
| _ => wrap_if is_stmt
(applify "(" ")" (print_go_expr const_syntax tyvars some_thm vars NOBR) fxy
(print_go_expr const_syntax tyvars some_thm vars BR t1) [t2]))
| IVar NONE => raise Fail "can't return a variable with no name!"
| IVar (SOME v) => wrap_if is_stmt (Pretty.str (lookup_var vars v))
| (params, tys) `|=> (t, rty) => let
val vars' = intro_vars (map_filter I [params]) vars;
val func_head = print_func_head tyvars vars' NONE [] [] [params] [tys] (print_go_typ tyvars rty)
val body = print_go_term const_syntax tyvars some_thm vars' fxy t
in wrap_if is_stmt (print_func func_head body) end
| ICase { clauses = [], ... } => let
val _ = warning "empty case statement; generating call to panic() ...";
in Pretty.str "panic(\"empty case\");" end
| ICase (cases as { clauses = [_], ...}) =>
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
val does_not_pattern_match = List.all (Code_Thingol.is_IVar o fst o fst) binds
in if does_not_pattern_match then
let
fun print_call t vars =
(print_go_expr const_syntax tyvars some_thm vars fxy t, vars);
fun print_bind tyvars some_thm fxy p =
gen_print_bind (print_go_expr const_syntax tyvars) some_thm fxy p
fun print_assignment ((pat, _), t) vars = vars
|> print_bind tyvars some_thm BR pat
|>> (fn p => (oneline [p, Pretty.str ":=",
fst (print_call t vars)]))
fun print_left ((IVar NONE, _), t) =
print_call t
| print_left ((pat as IVar (SOME _), ty), t) =
print_assignment ((pat, ty), t)
val (seps_ps, vars') =
fold_map print_left binds vars;
val term = print_go_term const_syntax tyvars some_thm vars' fxy body
in if is_stmt then Pretty.chunks (seps_ps @ [term])
else wrap_into_lambda tyvars (type_of_primitive_pattern (#primitive cases)) (seps_ps @ [term])
end
else
print_pattern_match is_stmt tyvars some_thm vars
(type_of_primitive_pattern (#primitive cases)) (#term cases) (#clauses cases)
end
| ICase cases => print_pattern_match is_stmt tyvars some_thm vars
(type_of_primitive_pattern (#primitive cases)) (#term cases) (#clauses cases);
fun print_dict_args tyvars vs =
let
fun print_single_arg length v (index, class) =
let
val name = if length = 1 then v^"_" else v ^ string_of_int (index + 1) ^ "_"
val ty = apply_constraints tyvars ((Pretty.str o deresolve_class) class) [ITyVar v]
in concat [Pretty.str name, ty] end
fun print_single_dict (v, sort) = let
val args = map_index (print_single_arg (length sort) v) sort
in args end
in (flat (map print_single_dict vs))
end;
fun print_go_func const_syntax reserved const vs ty [] =
let
val (tys, ty') = Code_Thingol.unfold_fun ty;
val params = Name.invent (snd reserved) "a" (length tys);
val tyvars = intro_tyvars vs reserved;
val vars = intro_vars params tyvars;
val dict_args = print_dict_args tyvars vs
val head = print_func_head tyvars vars ((SOME o Constant) const) (map fst vs) dict_args (map SOME params) tys (print_go_typ tyvars ty');
val _ = warning ("you appear to have defined a function "^const^" with no body; generating a call to panic() ...")
in
print_func head (oneline [Pretty.str ("panic("^print_go_string const^")")])
end
| print_go_func const_syntax reserved const vs ty eqs =
let
val tycos = build (fold (fn ((ts, t), _) =>
fold Code_Thingol.add_tyconames (t :: ts)) eqs);
val tyvars = reserved
|> intro_base_names
(is_none o tyco_syntax) deresolve_tyco tycos
|> intro_tyvars vs;
val simple = case eqs
of [((ts, _), _)] => forall Code_Thingol.is_IVar ts
| _ => false;
val vars1 = reserved
|> intro_tyvars vs
|> intro_base_names_for (is_none o const_syntax)
deresolve (map (snd o fst) eqs);
val params = if simple
then (map (fn IVar x => x) o fst o fst o hd) eqs
else map SOME (aux_params vars1 (map (fst o fst) eqs));
val vars2 = intro_vars (map_filter I params) vars1;
val (tys', ty') = Code_Thingol.unfold_fun_n (length params) ty;
fun print_rhs is_stmt vars' ((_, t), (some_thm, _)) =
print_go_term_gen is_stmt const_syntax tyvars some_thm vars' NOBR t;
val [p] = Name.invent (snd vars2) "m" 1
val vars3 = intro_vars [p] vars2
fun print_fun_clause ((targets, t), (some_thm, _)) =
let
val used = Code_Thingol.add_varnames t []
val vars' =
intro_vars (build (fold Code_Thingol.add_varnames targets)) vars2;
fun remove_unused (IVar (SOME name)) = IVar
(if member (op =) used name then SOME name else NONE)
| remove_unused t = t
val clauses = params ~~ targets
|> map (apsnd (map_terms_bottom_up remove_unused))
|> filter (fn (_, IVar NONE) => false | _ => true)
|> map_filter (fn (NONE, _) => NONE | (SOME v, t) => SOME (v,t))
val clause = print_clause tyvars some_thm vars' p clauses t
in
wrap_new_scope clause
end;
val dict_args = print_dict_args tyvars vs
val head = print_func_head tyvars vars3 ((SOME o Constant) const) (map fst vs) dict_args params tys' (print_go_typ tyvars ty');
in
if simple then
print_func head (print_rhs true vars2 (hd eqs))
else
print_func head (Pretty.chunks
(map print_fun_clause eqs @ [oneline [Pretty.str "panic(\"match failed\")"]]))
end;
fun print_typeclass tyvars sym ((target, (super, params))) =
let
val tyvars = intro_vars [target] tyvars
val super_fields = super
|> map (fn (self, super) => block [
(Pretty.str o Long_Name.base_name o deresolve_classrel) (self, super),
Pretty.brk 1,
apply_constraints tyvars ((Pretty.str o deresolve_class) super) [ITyVar target]
])
val fields = params
|> map (fn (name,typ) => block [
(Pretty.str o deresolve_const) name, Pretty.brk 1,
print_go_typ_uncurried_toplevel tyvars typ
])
|> (curry op @) super_fields
val head = applify_constraints tyvars ((Pretty.str o deresolve_class) sym) [target]
in block_enclose (concat [Pretty.str "type", head, Pretty.str "struct {"], Pretty.str "}") fields
end;
fun print_instance tyvars (target, class) {vs, inst_params, superinsts, tyco, ...} =
let
val class_name = deresolve_class class
val tyvars = intro_tyvars vs tyvars
val tyargs = map fst vs
val class_head = apply_constraints tyvars (Pretty.str class_name) [tyco `%% (map ITyVar tyargs)]
val sym = Class_Instance (target, class)
val instance_name = deresolve_inst (target, class)
val superinsts_fields = superinsts
|> map (fn (super, dictss) => block [
(Pretty.str o Long_Name.base_name o deresolve_classrel) (class, super),
Pretty.str ":", Pretty.brk 1,
print_dict tyvars (Dict ([], Dict_Const ((tyco, super), dictss))), Pretty.str ","
])
fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =
let
val aux_dom = Name.invent_names (snd reserved) "A" dom;
val auxs = map fst aux_dom;
val vars = intro_vars auxs tyvars;
val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
fun abstract_using [] _ _ body = body
| abstract_using aux_dom should_wrap rty body = let
val params = aux_dom
|> map (fn (aux, ty) =>
block [(Pretty.str o lookup_var vars) aux, Pretty.brk 1, print_go_typ tyvars ty])
val head = print_func_head tyvars vars NONE [] params [] []
((if should_wrap then print_go_typ_uncurried_toplevel else print_go_typ) tyvars rty)
in print_func head (wrap_if should_wrap body) end;
val aux_abstract = if not (null aux_dom1) andalso not (null aux_dom2)
then abstract_using aux_dom1 true (map snd aux_dom2 `--> #range const) o abstract_using aux_dom2 false (#range const)
else abstract_using aux_dom1 false (#range const) o abstract_using aux_dom2 false (#range const)
val wrap_in_func = if null aux_dom1 andalso null aux_dom2
then print_func (print_func_head tyvars vars NONE [] [] [] [] (print_go_typ tyvars (#range const))) else I
val wrap_aux = case (null aux_dom1, null aux_dom2) of
(true, true) => print_func (print_func_head tyvars vars NONE [] [] [] [] (print_go_typ tyvars (#range const)))
| (false, false) => abstract_using aux_dom1 true (map snd aux_dom2 `--> #range const) o abstract_using aux_dom2 false (#range const)
| _ => abstract_using aux_dom1 false (#range const) o abstract_using aux_dom2 false (#range const)
in block [
(Pretty.str o Long_Name.base_name o deresolve_const) classparam,
Pretty.str ":", Pretty.brk 1,
(wrap_aux o wrap_in_return o print_app false const_syntax tyvars (SOME thm) vars NOBR)
(const, map (IVar o SOME) auxs),
Pretty.str ","
] end;
in let
val body = block_enclose (concat [Pretty.str "return", class_head, Pretty.str "{"],Pretty.str "}")
(superinsts_fields
@ map print_classparam_instance inst_params)
val head = print_func_head tyvars reserved (SOME sym) tyargs (print_dict_args tyvars vs)
[] [] class_head
in print_func head body end
end;
fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
print_go_func const_syntax reserved const vs ty (filter (snd o snd) raw_eqs)
| print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) =
print_go_typedef tyco vs cos reserved
| print_stmt (Type_Class sym, (_, Class class)) =
print_typeclass reserved sym class
| print_stmt (Class_Instance sym, (_, Instance instance)) =
print_instance reserved sym instance
| print_stmt (_, _) = Pretty.str "<unknown>"
in print_stmt
end;
fun variant_capitalize s ctxt =
let
val cs = Symbol.explode s;
val s_lower = case cs of
c :: cs => Symbol.to_ascii_upper c :: cs
in ctxt
|> Name.variant (implode s_lower)
end;
fun go_program_of_program ctxt module_name reserved identifiers exports program =
let
val variant = variant_capitalize
fun namify_module name_fragment ((nsp_class, nsp_object), nsp_common) =
let
val declare = Name.declare name_fragment;
in (name_fragment, ((declare nsp_class, declare nsp_object), declare nsp_common)) end;
fun namify_common base ((nsp_class, nsp_object), nsp_common) =
let
val (base', nsp_common') = variant base nsp_common
in
(base', ((Name.declare base' nsp_class, Name.declare base' nsp_object), nsp_common'))
end;
fun namify_stmt (Code_Thingol.Fun _) = namify_common
| namify_stmt (Code_Thingol.Datatype _) = namify_common
| namify_stmt (Code_Thingol.Datatypecons _) = namify_common
| namify_stmt (Code_Thingol.Class _) = namify_common
| namify_stmt (Code_Thingol.Classrel _) = namify_common
| namify_stmt (Code_Thingol.Classparam _) = namify_common
| namify_stmt (Code_Thingol.Classinst _) = namify_common;
fun modify_stmt (_, (_, Code_Thingol.Fun (_, SOME _))) = NONE
| modify_stmt (_, (export, Code_Thingol.Fun (x, _))) = SOME (export, Fun x)
| modify_stmt (_, (export, Code_Thingol.Datatype x)) = SOME (export, Datatype x)
| modify_stmt (_, (_, Code_Thingol.Datatypecons _)) = NONE
| modify_stmt (Type_Class class, (export, Code_Thingol.Class x)) =
SOME (export, Class x)
| modify_stmt (_, (_, Code_Thingol.Classrel x)) = NONE
| modify_stmt (_, (_, Code_Thingol.Classparam x)) = NONE
| modify_stmt (_, (export, Code_Thingol.Classinst inst)) =
SOME (export, Instance inst);
in
Code_Namespace.hierarchical_program ctxt
{ module_name = module_name, reserved = reserved, identifiers = identifiers,
empty_nsp = ((reserved, reserved), reserved), namify_module = namify_module,
namify_stmt = namify_stmt, cyclic_modules = false,
class_transitive = true, class_relation_public = true, empty_data = (),
memorize_data = K I, modify_stmts = map modify_stmt }
exports program
end;
fun serialize_go gen_stringer go_module undefineds infinite_types ctxt { module_name, reserved_syms,
identifiers, includes, class_syntax, tyco_syntax, const_syntax } program exports =
let
val { deresolver, hierarchical_program = go_program } =
go_program_of_program ctxt module_name (Name.make_context reserved_syms)
identifiers exports program;
val go_module = if go_module = "" then "isabelle/exported" else go_module;
fun lookup_constr tyco constr = case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
of Code_Thingol.Datatype (_, constrs) =>
(AList.lookup (op = o apsnd fst) constrs constr)
| _ => NONE;
fun is_sum_type sym = case Code_Symbol.Graph.get_node program sym of
Code_Thingol.Datatypecons tyco => (case Code_Symbol.Graph.get_node program (Type_Constructor tyco)
of Code_Thingol.Datatype (_, []) => false
| Code_Thingol.Datatype (_, [_]) => false
| Code_Thingol.Datatype _ => true
| _ => false)
| _ => false;
fun is_class_param (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
of Code_Thingol.Classparam _ => true
| _ => false
fun classparams_of_class class = case Code_Symbol.Graph.get_node program (Type_Class class)
of Code_Thingol.Class (_, (_, classparams)) => classparams;
fun args_num (sym as Constant const) = case Code_Symbol.Graph.get_node program sym
of Code_Thingol.Fun (((_, ty), []), _) =>
(length o fst o Code_Thingol.unfold_fun) ty
| Code_Thingol.Fun ((_, ((ts, _), _) :: _), _) => length ts
| Code_Thingol.Datatypecons tyco => length (the (lookup_constr tyco const))
| Code_Thingol.Classparam class =>
(length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =)
(classparams_of_class class)) const;
fun print_stmt prefix_fragments b = ("", print_go_stmt gen_stringer undefineds infinite_types
tyco_syntax const_syntax (make_vars reserved_syms) args_num is_sum_type is_class_param
(Code_Thingol.is_constr program) (deresolver prefix_fragments, deresolver) b);
fun get_imports module_name = Module module_name
|> Code_Symbol.Graph.immediate_succs go_program
|> map (fn (Module a) => a)
|> (curry op @) (map fst includes)
|> map (fn (a) => go_module ^ "/" ^ a)
fun print_module _ base _ ps = (base, Pretty.chunks2
(Pretty.str ("package " ^ base)
:: block_enclose (Pretty.str "import (", Pretty.str ")")
(map (Pretty.str o print_go_string) (get_imports base))
:: (map snd ps) ))
val p = Code_Namespace.print_hierarchical {
print_module = print_module, print_stmt = print_stmt,
lift_markup = K I } go_program
|> curry (op @) includes
|> map (apfst (fn a => [a, "exported.go"]))
val is_single_module = length p = 1
in (
if is_single_module
then Code_Target.Singleton ("go", snd (hd p))
else Code_Target.Hierarchy ((["go.mod"], Pretty.chunks2 [
concat [Pretty.str "module",(Pretty.str o print_go_string) go_module],
Pretty.str "go 1.18"
]) :: p),
try (deresolver [])
) end;
val serializer : Code_Target.serializer =
Code_Target.parse_args ((Scan.optional (Args.$$$ "go_module" |-- Args.name) ""
-- Scan.optional (Args.$$$ "gen_stringer" >> K true) false
-- Scan.optional (Args.$$$ "panic_on" |-- (Scan.repeat Parse.term)) []
-- Scan.optional (Args.$$$ "infinite_type" |-- (Scan.repeat Parse.term)) [])
>> (fn (((go_module, gen_stringer), undef_terms), infinite_types) => fn lthy => let
val undefineds = map (fst o dest_Const o Syntax.read_term lthy) undef_terms
val infinite_types = map (fst o dest_Type o Syntax.parse_typ lthy) infinite_types
in serialize_go gen_stringer go_module undefineds infinite_types lthy end))
val _ = Theory.setup
(Code_Target.add_language
(target, { serializer = serializer, literals = literals,
check = { env_var = "ISABELLE_GOEXE",
make_destination = fn p => p + Path.explode "export.go",
run_command = Code_Target.run_command_bash (fn module_name =>
"test -d export.go && cd export.go && isabelle go build ./" ^ Bash.string module_name ^
" || isabelle go build ./export.go")},
evaluation_args = []})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_go_typ => fn fxy => fn [arg, rtyp] => let
val head = applify "(" ")" (print_go_typ fxy) NOBR (Pretty.str "func") [arg];
in concat [head, print_go_typ fxy rtyp] end)
)]))
#> fold (Code_Target.add_reserved target) [
"any", "break", "default", "func", "interface", "select", "case", "defer",
"go", "map", "struct", "chan", "else", "goto", "package", "switch",
"const", "fallthrough", "if", "range", "type", "continue", "for",
"import", "return", "var"
]);
end;