--- a/src/Pure/Tools/codegen_serializer.ML Wed Dec 13 20:38:20 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Wed Dec 13 20:38:23 2006 +0100
@@ -16,6 +16,7 @@
val add_pretty_ml_string: string -> string -> string -> string
-> (string -> string) -> (string -> string) -> string -> theory -> theory;
val add_undefined: string -> string -> string -> theory -> theory;
+ val add_pretty_imperative_monad_bind: string -> string -> theory -> theory;
type serializer;
val add_serializer : string * serializer -> theory -> theory;
@@ -144,6 +145,7 @@
| _ => Scan.!! (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
end;
+(*FIXME: use Args.syntax ???*)
fun parse_args f args =
case f args
of (x, []) => x
@@ -172,32 +174,39 @@
fun pretty_ml_string c_nil c_cons mk_char mk_string target_implode =
let
- fun pretty fxy pr [e] =
- case implode_list c_nil c_cons e
- of SOME es => (case implode_string mk_char mk_string es
+ fun pretty fxy pr [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 e])
- | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR e]
+ | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR t])
+ | NONE => Pretty.block [str target_implode, Pretty.brk 1, pr BR t]
in (1, pretty) end;
fun pretty_list c_nil c_cons mk_list mk_char_string (target_fxy, target_cons) =
let
- fun default fxy pr e1 e2 =
+ fun default fxy pr t1 t2 =
brackify_infix (target_fxy, R) fxy [
- pr (INFX (target_fxy, X)) e1,
+ pr (INFX (target_fxy, X)) t1,
str target_cons,
- pr (INFX (target_fxy, R)) e2
+ pr (INFX (target_fxy, R)) t2
];
- fun pretty fxy pr [e1, e2] =
- case Option.map (cons e1) (implode_list c_nil c_cons e2)
- of SOME es =>
+ fun pretty fxy pr [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 es
+ (case implode_string mk_char mk_string ts
of SOME p => p
- | NONE => mk_list (map (pr NOBR) es))
- | NONE => mk_list (map (pr NOBR) es))
- | NONE => default fxy pr e1 e2;
+ | NONE => mk_list (map (pr NOBR) ts))
+ | NONE => mk_list (map (pr NOBR) ts))
+ | NONE => default fxy pr t1 t2;
+ in (2, pretty) end;
+
+fun pretty_imperative_monad_bind c_bind =
+ let
+ fun pretty fxy pr [t1, (v, ty) `|-> t2] =
+ pr fxy (ICase ((t1, ty), ([(IVar v, t2)])))
+ | pretty _ _ _ = error "bad arguments for imperative monad bind";
in (2, pretty) end;
@@ -242,7 +251,7 @@
* ((class * (string * inst list list)) list
* (string * iterm) list));
-fun pr_sml_def tyco_syntax const_syntax keyword_vars deresolv ml_def =
+fun pr_sml tyco_syntax const_syntax keyword_vars deresolv ml_def =
let
val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
fun dictvar v =
@@ -559,9 +568,334 @@
end;
in pr_def ml_def end;
+fun pr_sml_modl name content =
+ Pretty.chunks ([
+ str ("structure " ^ name ^ " = "),
+ str "struct",
+ str ""
+ ] @ content @ [
+ str "",
+ str ("end; (*struct " ^ name ^ "*)")
+ ]);
+
+fun pr_ocaml tyco_syntax const_syntax keyword_vars deresolv ml_def =
+ let
+ val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
+ fun dictvar v =
+ first_upper v ^ "_";
+ val label = translate_string (fn "." => "__" | c => c)
+ o NameSpace.pack o op @ o apsnd single o apfst (fst o split_last) o split_last o NameSpace.unpack;
+ fun pr_tyvar (v, []) =
+ str "()"
+ | pr_tyvar (v, sort) =
+ let
+ fun pr_class class =
+ str ("'" ^ v ^ " " ^ deresolv class);
+ in
+ Pretty.block [
+ str "(",
+ (str o dictvar) v,
+ str ":",
+ case sort
+ of [class] => pr_class class
+ | _ => Pretty.enum " *" "" "" (map pr_class sort),
+ str ")"
+ ]
+ end;
+ fun pr_insts fxy iys =
+ let
+ fun pr_proj s = str ("#" ^ s);
+ fun pr_lookup [] p =
+ p
+ | pr_lookup [p'] p =
+ brackify BR [p', p]
+ | pr_lookup (ps as _ :: _) p =
+ brackify BR [Pretty.enum " o" "(" ")" ps, p];
+ fun pr_inst fxy (Instance (inst, iss)) =
+ brackify fxy (
+ (str o deresolv) inst
+ :: map (pr_insts BR) iss
+ )
+ | pr_inst fxy (Context (classes, (v, i))) =
+ pr_lookup (map (pr_proj o label) classes
+ @ (if i = ~1 then [] else [(pr_proj o string_of_int) (i+1)])
+ ) ((str o dictvar) v);
+ in case iys
+ of [] => str "()"
+ | [iy] => pr_inst fxy iy
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_inst NOBR)) iys
+ end;
+ fun pr_tycoexpr fxy (tyco, tys) =
+ let
+ val tyco' = (str o deresolv) 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 tyco_syntax tyco
+ of NONE => pr_tycoexpr fxy (tyco, tys)
+ | SOME (i, pr) =>
+ if not (i = length tys)
+ then error ("Number of argument mismatch in customary serialization: "
+ ^ (string_of_int o length) tys ^ " given, "
+ ^ string_of_int i ^ " expected")
+ else pr fxy pr_typ tys)
+ | pr_typ fxy (ITyVar v) =
+ str ("'" ^ v);
+ fun pr_term vars fxy (IConst c) =
+ pr_app vars fxy (c, [])
+ | pr_term vars fxy (IVar v) =
+ str (CodegenThingol.lookup_var vars v)
+ | pr_term vars fxy (t as t1 `$ t2) =
+ (case CodegenThingol.unfold_const_app t
+ of SOME c_ts => pr_app vars fxy c_ts
+ | NONE =>
+ brackify fxy [pr_term vars NOBR t1, pr_term vars BR t2])
+ | pr_term vars fxy (t as _ `|-> _) =
+ let
+ val (ps, t') = CodegenThingol.unfold_abs t;
+ fun pr ((v, NONE), _) vars =
+ let
+ val vars' = CodegenThingol.intro_vars [v] vars;
+ in
+ ((Pretty.block o Pretty.breaks) [str "fun", str (CodegenThingol.lookup_var vars' v), str "=>"], vars')
+ end
+ | pr ((v, SOME p), _) vars =
+ let
+ val vars' = CodegenThingol.intro_vars [v] vars;
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars'' = CodegenThingol.intro_vars vs vars';
+ in
+ ((Pretty.block o Pretty.breaks) [str "fun", str (CodegenThingol.lookup_var vars' v), str "as",
+ pr_term vars'' NOBR p, str "=>"], vars'')
+ end;
+ val (ps', vars') = fold_map pr ps vars;
+ in brackify BR (ps' @ [pr_term vars' NOBR t']) end
+ | pr_term vars fxy (INum n) =
+ brackify BR [(str o IntInf.toString) n, str ":", str "Big_int.big_int"]
+ | pr_term vars _ (IChar c) =
+ (str o prefix "#" o quote)
+ (let val i = ord c
+ in if i < 32
+ then prefix "\\" (string_of_int i)
+ else c
+ end)
+ | pr_term vars fxy (t as ICase (_, [_])) =
+ let
+ val (ts, t') = CodegenThingol.unfold_let t;
+ fun mk ((p, _), t'') vars =
+ let
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = CodegenThingol.intro_vars vs vars;
+ in
+ (Pretty.block [
+ (Pretty.block o Pretty.breaks) [
+ str "val",
+ pr_term vars' NOBR p,
+ str "=",
+ pr_term vars NOBR t''
+ ],
+ str ";"
+ ], vars')
+ end
+ val (binds, vars') = fold_map mk ts vars;
+ in
+ Pretty.chunks [
+ [str ("let"), Pretty.fbrk, binds |> Pretty.chunks] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term vars' NOBR t'] |> Pretty.block
+ ] end
+ | pr_term vars fxy (ICase ((td, ty), b::bs)) =
+ let
+ fun pr definer (p, t) =
+ let
+ val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
+ val vars' = CodegenThingol.intro_vars vs vars;
+ in
+ (Pretty.block o Pretty.breaks) [
+ str definer,
+ pr_term vars' NOBR p,
+ str "=>",
+ pr_term vars' NOBR t
+ ]
+ end;
+ in
+ (Pretty.enclose "(" ")" o single o brackify fxy) (
+ str "match"
+ :: pr_term vars NOBR td
+ :: pr "with" b
+ :: map (pr "|") bs
+ )
+ end
+ and pr_app' vars (app as ((c, (iss, ty)), ts)) =
+ if is_cons c then let
+ val k = (length o fst o CodegenThingol.unfold_fun) ty
+ in if k = 0 then
+ [(str o deresolv) c]
+ else if k = length ts then
+ [(str o deresolv) c, Pretty.enum "," "(" ")" (map (pr_term vars NOBR) ts)]
+ else [pr_term vars BR (CodegenThingol.eta_expand app k)] end else
+ (str o deresolv) c :: map (pr_term vars BR) ts
+ and pr_app vars fxy (app as ((c, (iss, ty)), ts)) =
+ case if is_cons c then [] else (map (pr_insts BR) o filter_out null) iss
+ of [] =>
+ mk_app (pr_app' vars) (pr_term vars) const_syntax fxy app
+ | ps =>
+ if (is_none o const_syntax) c then
+ brackify fxy ((str o deresolv) c :: (ps @ map (pr_term vars BR) ts))
+ else
+ error ("Cannot apply user defined serialization for function expecting dictionaries: " ^ quote c)
+ fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([_], ([], _)))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([(_::_, _)], _))) =
+ funn
+ | eta_expand_poly_fun (funn as (_, ([(_, _ `|-> _)], _))) =
+ funn
+ | eta_expand_poly_fun (funn as (name, ([([], t)], tysm as (vs, ty)))) =
+ if (null o fst o CodegenThingol.unfold_fun) ty
+ orelse (not o null o filter_out (null o snd)) vs
+ then funn
+ else (name, ([([IVar "x"], t `$ IVar "x")], tysm));
+ fun pr_def (MLFuns raw_funns) =
+ let
+ val funns as (funn :: funns') = map (eta_expand_poly_fun o constructive_fun) raw_funns;
+ fun pr_funn definer (name, (eqs as eq::eqs', (raw_vs, ty))) =
+ let
+ val vs = filter_out (null o snd) raw_vs;
+ val dummy_args = map_index (fn (i, _) => str ("x" ^ string_of_int i)) (fst eq);
+ fun pr_eq definer (ts, t) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o const_syntax) c
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ ((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = keyword_vars
+ |> CodegenThingol.intro_vars consts
+ |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
+ in
+ (Pretty.block o Pretty.breaks) [
+ str definer,
+ Pretty.list "(" ")" (map (pr_term vars BR) ts),
+ str "->",
+ pr_term vars NOBR t
+ ]
+ end
+ in
+ (Pretty.block o Pretty.breaks) (
+ str "let rec"
+ :: (str o deresolv) name
+ :: (map pr_tyvar vs
+ @ dummy_args
+ @ [str "=", str "match", Pretty.list "(" ")" dummy_args, pr_eq "with" eq]
+ @ map (pr_eq "|") eqs')
+ )
+ end;
+ val (ps, p) = split_last (pr_funn "let rec" funn :: map (pr_funn "and") funns');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
+ | pr_def (MLDatas (datas as (data :: datas'))) =
+ let
+ fun pr_co (co, []) =
+ str (deresolv co)
+ | pr_co (co, tys) =
+ (Pretty.block o Pretty.breaks) [
+ str (deresolv co),
+ str "of",
+ Pretty.enum " *" "" "" (map (pr_typ (INFX (2, L))) tys)
+ ];
+ fun pr_data definer (tyco, (vs, cos)) =
+ (Pretty.block o Pretty.breaks) (
+ 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_def (MLClass (class, (superclasses, (v, classops)))) =
+ let
+ val w = dictvar v;
+ fun pr_superclass class =
+ (Pretty.block o Pretty.breaks o map str) [
+ label class, ":", "'" ^ v, deresolv class
+ ];
+ fun pr_classop (classop, ty) =
+ (Pretty.block o Pretty.breaks) [
+ (str o suffix "_" o NameSpace.base) classop, str ":", pr_typ NOBR ty
+ ];
+ fun pr_classop_fun (classop, _) =
+ (Pretty.block o Pretty.breaks) [
+ str "fun",
+ (str o deresolv) classop,
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolv class)],
+ str "=",
+ str ("#" ^ (suffix "_" o NameSpace.base) classop),
+ str (w ^ ";")
+ ];
+ in
+ Pretty.chunks (
+ (Pretty.block o Pretty.breaks) [
+ str ("type '" ^ v),
+ (str o deresolv) class,
+ str "=",
+ Pretty.enum "," "{" "};" (
+ map pr_superclass superclasses @ map pr_classop classops
+ )
+ ]
+ :: map pr_classop_fun classops
+ )
+ end
+ | pr_def (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classop_defs)))) =
+ let
+ fun pr_superclass (superclass, superinst_iss) =
+ (Pretty.block o Pretty.breaks) [
+ (str o label) superclass,
+ str "=",
+ pr_insts NOBR [Instance superinst_iss]
+ ];
+ fun pr_classop_def (classop, t) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o const_syntax) c
+ then NONE else (SOME o NameSpace.base o deresolv) c)
+ (CodegenThingol.fold_constnames (insert (op =)) t []);
+ val vars = keyword_vars
+ |> CodegenThingol.intro_vars consts;
+ in
+ (Pretty.block o Pretty.breaks) [
+ (str o suffix "_" o NameSpace.base) classop,
+ str "=",
+ pr_term vars NOBR t
+ ]
+ end;
+ in
+ (Pretty.block o Pretty.breaks) ([
+ str (if null arity then "val" else "fun"),
+ (str o deresolv) inst ] @
+ map pr_tyvar arity @ [
+ str "=",
+ Pretty.enum "," "{" "}" (map pr_superclass superarities @ map pr_classop_def classop_defs),
+ str ":",
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ])
+ end;
+ in pr_def ml_def end;
+
+fun pr_ocaml_modl name content =
+ Pretty.chunks ([
+ str ("module " ^ name ^ " = "),
+ str "struct",
+ str ""
+ ] @ content @ [
+ str "",
+ str ("end;; (*struct " ^ name ^ "*)")
+ ]);
+
val sml_code_width = ref 80;
-fun seri_sml output reserved_user module_alias module_prolog
+fun seri_ml pr_def pr_modl output reserved_user module_alias module_prolog
(_ : string -> (string * (string -> string option)) option) tyco_syntax const_syntax code =
let
datatype node =
@@ -644,7 +978,6 @@
fun add_group mk defs nsp_nodes =
let
val names as (name :: names') = map fst defs;
-(* val _ = writeln ("adding " ^ commas names); *)
val deps =
[]
|> fold (fold (insert (op =)) o Graph.imm_succs code) names
@@ -657,9 +990,6 @@
fun add_dep defname name'' =
let
val (modl'', defname'') = (apfst name_modl o dest_name) name'';
-(* val _ = writeln (uncurry NameSpace.append defname ^ " -> " ^ name''); *)
-(* val _ = (writeln o NameSpace.pack) modl'; *)
-(* val _ = (writeln o NameSpace.pack) modl''; *)
in if modl' = modl'' then
map_node modl'
(Graph.add_edge (NameSpace.pack (modl @ [fst defname, snd defname]), name''))
@@ -701,7 +1031,6 @@
(rev (Graph.strong_conn code)))
fun deresolver prefix name =
let
-(* val _ = writeln ("resolving " ^ name) *)
val (modl, _) = apsnd (uncurry NameSpace.append) (dest_name name);
val modl' = name_modl modl;
val (_, (_, remainder)) = chop_prefix (op =) (prefix, modl');
@@ -718,28 +1047,13 @@
fun pr_node prefix (Def (_, NONE)) =
NONE
| pr_node prefix (Def (_, SOME def)) =
- SOME (pr_sml_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
+ SOME (pr_def tyco_syntax const_syntax init_vars (deresolver prefix) def)
| pr_node prefix (Module (dmodlname, (_, nodes))) =
- (SOME o Pretty.chunks) ([
- str ("structure " ^ dmodlname ^ " = "),
- str "struct",
- str ""
- ] @ the_prolog (NameSpace.pack (prefix @ [dmodlname]))
+ SOME (pr_modl dmodlname (the_prolog (NameSpace.pack (prefix @ [dmodlname]))
@ separate (str "") ((map_filter (pr_node (prefix @ [dmodlname]) o Graph.get_node nodes)
- o rev o flat o Graph.strong_conn) nodes) @ [
- str "",
- str ("end; (*struct " ^ dmodlname ^ "*)")
- ]);
- val p = Pretty.chunks ([
- str ("structure ROOT = "),
- str "struct",
- str ""
- ] @ the_prolog ""
- @ separate (str "") ((map_filter (pr_node [] o Graph.get_node nodes)
- o rev o flat o Graph.strong_conn) nodes) @ [
- str "",
- str ("end; (*struct ROOT*)")
- ]);
+ o rev o flat o Graph.strong_conn) nodes)));
+ val p = pr_modl "ROOT" (the_prolog "" @ separate (str "") ((map_filter
+ (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes))
in output p end;
val isar_seri_sml =
@@ -751,9 +1065,18 @@
parse_args ((Args.$$$ "-" >> K output_diag
|| Args.$$$ "#" >> K output_internal
|| Args.name >> output_file)
- >> (fn output => seri_sml output))
+ >> (fn output => seri_ml pr_sml pr_sml_modl output))
end;
+val isar_seri_ocaml =
+ let
+ fun output_file file p = File.write (Path.unpack file) (Pretty.output p ^ "\n");
+ fun output_diag p = Pretty.writeln p;
+ in
+ parse_args ((Args.$$$ "-" >> K output_diag
+ || Args.name >> output_file)
+ >> (fn output => seri_ml pr_ocaml pr_ocaml_modl output))
+ end;
(** Haskell serializer **)
@@ -1068,6 +1391,7 @@
o Symtab.lookup code') ((NameSpace.qualifier o NameSpace.qualifier) name))) name
handle Option => "(error \"undefined name " ^ name ^ "\")";
val deresolv_module = fst o the o Symtab.lookup code';
+ (*FIXME: chain this into every module name access *)
fun deriving_show tyco =
let
fun deriv _ "fun" = false
@@ -1246,6 +1570,7 @@
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_diag, (fn _ => fn _ => seri_diagnosis))
);
@@ -1297,7 +1622,7 @@
|> CodegenThingol.project_code
(Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const)
(SOME [val_name])
- |> seri_sml I reserved (Symtab.lookup alias) (Symtab.lookup prolog)
+ |> seri_ml pr_sml pr_sml_modl I reserved (Symtab.lookup alias) (Symtab.lookup prolog)
(fun_of class) (fun_of tyco) (fun_of const)
|> eval
end;
@@ -1419,11 +1744,11 @@
else error ("No such type constructor: " ^ quote raw_tyco);
in tyco end;
-fun idfs_of_const_names thy cs =
+fun idfs_of_const_names thy c =
let
- val cs' = AList.make (fn c => Sign.the_const_type thy c) cs;
- val cs'' = map (CodegenConsts.norm_of_typ thy) cs';
- in AList.make (CodegenNames.const thy) cs'' end;
+ val c' = (c, Sign.the_const_type thy c);
+ val c'' = CodegenConsts.norm_of_typ thy c';
+ in (c'', CodegenNames.const thy c'') 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;
@@ -1476,7 +1801,8 @@
fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
let
- val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];
+ val (_, nil'') = idfs_of_const_names thy nill;
+ val (cons', cons'') = idfs_of_const_names thy cons;
val pr = pretty_list nil'' cons'' mk_list mk_char_string target_cons;
in
thy
@@ -1485,7 +1811,9 @@
fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
let
- val [(_, nil''), (_, cons''), (str', _)] = idfs_of_const_names thy [nill, cons, str];
+ 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 pr = pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
in
thy
@@ -1494,11 +1822,20 @@
fun add_undefined target undef target_undefined thy =
let
- val [(undef', _)] = idfs_of_const_names thy [undef];
- fun pretty _ _ _ = str target_undefined;
+ val (undef', _) = idfs_of_const_names thy undef;
+ fun pr _ _ _ = str target_undefined;
in
thy
- |> gen_add_syntax_const (K I) target undef' (SOME (~1, pretty))
+ |> gen_add_syntax_const (K I) target undef' (SOME (~1, pr))
+ end;
+
+fun add_pretty_imperative_monad_bind target bind thy =
+ let
+ val (bind', bind'') = idfs_of_const_names thy bind;
+ val pr = pretty_imperative_monad_bind bind''
+ in
+ thy
+ |> gen_add_syntax_const (K I) target bind' (SOME pr)
end;
val code_classP =
@@ -1569,6 +1906,12 @@
str "->",
pr_typ (INFX (1, R)) ty2
]))
+ #> gen_add_syntax_tyco (K I) "OCaml" "fun" (SOME (2, fn fxy => fn pr_typ => fn [ty1, ty2] =>
+ (gen_brackify (case fxy of NOBR => false | _ => eval_fxy (INFX (1, R)) fxy) o Pretty.breaks) [
+ pr_typ (INFX (1, X)) ty1,
+ str "->",
+ pr_typ (INFX (1, R)) ty2
+ ]))
#> gen_add_syntax_tyco (K I) "Haskell" "fun" (SOME (2, fn fxy => fn pr_typ => fn [ty1, ty2] =>
brackify_infix (1, R) fxy [
pr_typ (INFX (1, X)) ty1,