Commit 4468ff82 authored by Mário Pereira's avatar Mário Pereira

Code extraction (wip)

parent d3ea5de2
......@@ -116,22 +116,20 @@ module ML = struct
| Efun of var list * expr
| Elet of let_def * expr
| Eif of expr * expr * expr
| Ecast of expr * ty
(* | Ecast of expr * ty *)
| Eassign of (pvsymbol * rsymbol * pvsymbol) list
| Etuple of expr list (* at least 2 expressions *)
| Ematch of expr * (pat * expr) list
| Ebinop of expr * binop * expr
| Enot of expr
| Eblock of expr list
| Ewhile of expr * expr
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr (* Why3's type int *)
(* For loop for Why3's type int *)
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
| Eraise of xsymbol * expr option
| Etry of expr * (xsymbol * pvsymbol list * expr) list
| Eabsurd
and let_def =
| Lvar of pvsymbol * expr
| Lsym of rsymbol * var list * expr
| Lsym of rsymbol * ty * var list * expr
| Lrec of rdef list
and rdef = {
......@@ -139,6 +137,7 @@ module ML = struct
rec_rsym : rsymbol; (* internal *)
rec_args : var list;
rec_exp : expr;
rec_res : ty;
}
type is_mutable = bool
......@@ -208,21 +207,13 @@ type info = {
info_fname : string option;
}
let has_syntax cxt id =
(* Mid.iter *)
(* (fun id' _ -> Format.printf "id': %s@\n" id'.id_string) *)
(* cxt.info_syn; *)
query_syntax cxt.info_syn id <> None ||
query_syntax cxt.info_convert id <> None
(** Translation from Mlw to ML *)
module Translate = struct
open Expr (* Mlw expressions *)
open Pmodule (* for the type of modules *)
open Pdecl (* for the type of program declarations *)
open Expr
open Pmodule
open Pdecl
(* useful predicates and transformations *)
let pv_not_ghost e = not e.pv_ghost
......@@ -361,19 +352,15 @@ module Translate = struct
| args -> let args = filter_params args in
if args = [] then [ML.mk_var_unit ()] else args
let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body eff =
let mk_for op_b_rs op_a_rs i_pv from_pv to_pv body_expr eff =
let i_expr, from_expr, to_expr =
let int_ity = ML.ity_int in let eff_e = eff_empty in
ML.mk_expr (ML.Evar i_pv) int_ity eff_e,
ML.mk_expr (ML.Evar from_pv) int_ity eff_e,
ML.mk_expr (ML.Evar to_pv) int_ity eff_e in
let body_ity = ity_func ity_int ity_unit in
let body_pv =
let body_id = id_fresh "body" in create_pvsymbol body_id body_ity in
let body_expr = ML.mk_expr (ML.Evar body_pv) (ML.I body_ity) eff in
let for_rs =
let for_id = id_fresh "for_loop_to" in
let for_cty = create_cty [i_pv; to_pv; body_pv] [] [] Mxs.empty
let for_cty = create_cty [i_pv; to_pv] [] [] Mxs.empty
Mpv.empty eff ity_unit in
create_rsymbol for_id for_cty in
let for_expr =
......@@ -386,35 +373,26 @@ module Translate = struct
let i_op_one = ML.Eapp (op_a_rs, [i_expr; one_expr]) in
ML.mk_expr i_op_one ML.ity_int eff_empty in
let rec_call =
ML.mk_expr (ML.Eapp (for_rs, [next_expr; to_expr; body_expr]))
ML.ity_unit eff in
let body_app =
ML.mk_expr (ML.Eapp (rs_func_app, [body_expr; i_expr]))
ML.mk_expr (ML.Eapp (for_rs, [next_expr; to_expr]))
ML.ity_unit eff in
let seq_expr =
ML.mk_expr (ML.eseq body_app rec_call) ML.ity_unit eff in
ML.mk_expr (ML.eseq body_expr rec_call) ML.ity_unit eff in
ML.mk_expr (ML.Eif (test, seq_expr, ML.mk_unit)) ML.ity_unit eff in
let ty_int = ity ity_int in
let for_call_expr =
let body_fun = ML.Efun ([pv_name i_pv, ty_int, false], body) in
let body_fun_expr = ML.mk_expr body_fun ML.ity_unit eff in
let for_call = ML.Eapp (for_rs, [i_expr; to_expr; body_fun_expr]) in
let for_call = ML.Eapp (for_rs, [from_expr; to_expr]) in
ML.mk_expr for_call ML.ity_unit eff in
let let_i_for_call_expr =
let let_i = ML.mk_let_var i_pv from_expr for_call_expr in
ML.mk_expr let_i ML.ity_unit eff in
let pv_name pv = pv.pv_vs.vs_name in
let ty_int_to_unit = ity body_ity in
let args = [
(pv_name i_pv, ty_int, false);
(pv_name to_pv, ty_int, false);
(pv_name body_pv, ty_int_to_unit, false);
(pv_name i_pv, ty_int, false);
(pv_name to_pv, ty_int, false);
] in
let for_rec_def = {
ML.rec_sym = for_rs; ML.rec_args = args;
ML.rec_rsym = for_rs; ML.rec_exp = for_expr;
ML.rec_res = ML.tunit;
} in
let for_let = ML.Elet (ML.Lrec [for_rec_def], let_i_for_call_expr) in
let for_let = ML.Elet (ML.Lrec [for_rec_def], for_call_expr) in
ML.mk_expr for_let ML.ity_unit eff
let mk_for_downto info i_pv from_pv to_pv body eff =
......@@ -453,23 +431,26 @@ module Translate = struct
let args = params cty.cty_args in
let ef = expr info ef in
let ein = expr info ein in
let ml_letrec = ML.Elet (ML.Lsym (rs, args, ef), ein) in
let res = ity cty.cty_result in
let ml_letrec = ML.Elet (ML.Lsym (rs, res, args, ef), ein) in
ML.mk_expr ml_letrec (ML.I e.e_ity) eff
| Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein)
when isconstructor info rs_app ->
let eta_app = make_eta_expansion rs_app pvl cty in
let ein = expr info ein in
let ml_letrec = ML.Elet (ML.Lsym (rsf, [], eta_app), ein) in
let res = ity cty.cty_result in
let ml_letrec = ML.Elet (ML.Lsym (rsf, res, [], eta_app), ein) in
ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
| Elet (LDsym (rsf, {c_node = Capp (rs_app, pvl); c_cty = cty}), ein) ->
(* partial application *)
let pvl = app pvl in
let eapp =
ML.mk_expr (ML.Eapp (rs_app, pvl)) (ML.C cty) cty.cty_effect in
let ein = expr info ein in
let ein = expr info ein in
let res = ity cty.cty_result in
let args =
if filter_params cty.cty_args = [] then [ML.mk_var_unit ()] else [] in
let ml_letrec = ML.Elet (ML.Lsym (rsf, args, eapp), ein) in
let ml_letrec = ML.Elet (ML.Lsym (rsf, res, args, eapp), ein) in
ML.mk_expr ml_letrec (ML.I e.e_ity) e.e_effect
| Elet (LDrec rdefl, ein) ->
let ein = expr info ein in
......@@ -477,9 +458,10 @@ module Translate = struct
List.map (fun rdef -> match rdef with
| {rec_sym = rs1; rec_rsym = rs2;
rec_fun = {c_node = Cfun ef; c_cty = cty}} ->
let res = ity rs1.rs_cty.cty_result in
let args = params cty.cty_args in let ef = expr info ef in
{ ML.rec_sym = rs1; ML.rec_rsym = rs2;
ML.rec_args = args; ML.rec_exp = ef }
ML.rec_args = args; ML.rec_exp = ef ; ML.rec_res = res }
| _ -> assert false) rdefl
in
let ml_letrec = ML.Elet (ML.Lrec rdefl, ein) in
......@@ -589,17 +571,19 @@ module Translate = struct
| PDlet (LDsym (rs, _)) when rs_ghost rs ->
[]
| PDlet (LDsym (rs, {c_node = Cany})) ->
[]
(* raise (ExtractionVal rs) *)
raise (ExtractionVal rs)
| PDlet (LDsym ({rs_cty = cty} as rs, {c_node = Cfun e})) ->
let args = params cty.cty_args in
[ML.Dlet (ML.Lsym (rs, args, expr info e))]
let res = ity cty.cty_result in
[ML.Dlet (ML.Lsym (rs, res, args, expr info e))]
| PDlet (LDrec rl) ->
let def {rec_fun = e; rec_sym = rs1; rec_rsym = rs2} =
let e = match e.c_node with Cfun e -> e | _ -> assert false in
let e = match e.c_node with Cfun e -> e | _ -> assert false in
let args = params rs1.rs_cty.cty_args in
let res = ity rs1.rs_cty.cty_result in
{ ML.rec_sym = rs1; ML.rec_rsym = rs2;
ML.rec_args = args; ML.rec_exp = expr info e } in
ML.rec_args = args; ML.rec_exp = expr info e;
ML.rec_res = res } in
let rec_def = filter_ghost_rdef def rl in
[ML.Dlet (ML.Lrec rec_def)]
| PDlet (LDsym _) | PDpure | PDlet (LDvar (_, _)) ->
......@@ -660,16 +644,10 @@ module Transform = struct
mk (Efun (vl, expr info subst e))
| Eif (e1, e2, e3) ->
mk (Eif (expr info subst e1, expr info subst e2, expr info subst e3))
| Ecast (e, ty) ->
mk (Ecast (expr info subst e, ty))
| Etuple el ->
mk (Etuple (List.map (expr info subst) el))
(* | Ecast (e, ty) -> *)
(* mk (Ecast (expr info subst e, ty)) *)
| Ematch (e, bl) ->
mk (Ematch (expr info subst e, List.map (branch info subst) bl))
| Ebinop (e1, op, e2) ->
mk (Ebinop (expr info subst e1, op, expr info subst e2))
| Enot e ->
mk (Enot (expr info subst e))
| Eblock el ->
mk (Eblock (List.map (expr info subst) el))
| Ewhile (e1, e2) ->
......@@ -700,8 +678,8 @@ module Transform = struct
| Lvar (pv, e) ->
assert (not (Mpv.mem pv subst)); (* no capture *)
Lvar (pv, expr info subst e)
| Lsym (rs, args, e) ->
Lsym (rs, args, expr info subst e)
| Lsym (rs, res, args, e) ->
Lsym (rs, res, args, expr info subst e)
| Lrec rl -> Lrec (List.map (rdef info subst) rl)
and rdef info subst r =
......
......@@ -61,7 +61,7 @@ module Print = struct
let forget_let_defn = function
| Lvar (v,_) -> forget_pv v
| Lsym (s,_,_) -> forget_rs s
| Lsym (s,_,_,_) -> forget_rs s
| Lrec rdl -> List.iter (fun fd -> forget_rs fd.rec_sym) rdl
let rec forget_pat = function
......@@ -107,6 +107,16 @@ module Print = struct
let star fmt () = fprintf fmt " *@ "
let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
match l1, l2 with
| x1 :: r1, x2 :: r2 ->
print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
print_list2 sep sep_m print1 print2 fmt (r1, r2)
| _ -> ()
let print_rs info fmt rs =
fprintf fmt "%a" (print_lident info) rs.rs_name
(** Types *)
let rec print_ty ?(paren=false) info fmt = function
......@@ -121,21 +131,20 @@ module Print = struct
fprintf fmt (protect_on paren "@[%a ->@ %a@]")
(print_ty ~paren:true info) t1 (print_ty info) t2
| Tapp (ts, tl) ->
begin match query_syntax info.info_syn ts with
| Some s -> syntax_arguments s (print_ty ~paren:true info) fmt tl
| None ->
begin match tl with
| [] ->
print_ident fmt ts
| [ty] ->
fprintf fmt (protect_on paren "%a@ %a")
(print_ty ~paren:true info) ty print_ident ts
| tl ->
fprintf fmt (protect_on paren "(%a)@ %a")
(print_list comma (print_ty ~paren:false info)) tl
print_ident ts
end
end
match query_syntax info.info_syn ts with
| Some s ->
syntax_arguments s (print_ty ~paren:true info) fmt tl
| None ->
match tl with
| [] ->
(print_lident info) fmt ts
| [ty] ->
fprintf fmt (protect_on paren "%a@ %a")
(print_ty ~paren:true info) ty (print_lident info) ts
| tl ->
fprintf fmt (protect_on paren "(%a)@ %a")
(print_list comma (print_ty ~paren:false info)) tl
(print_lident info) ts
let print_vsty info fmt (v, ty, _) =
fprintf fmt "%a:@ %a" print_ident v (print_ty ~paren:false info) ty
......@@ -186,30 +195,19 @@ module Print = struct
| Some s, _ ->
syntax_arguments s (print_pat info) fmt pl
| None, pl ->
let rs = restore_rs ls in
let pjl = get_record info rs in
match pjl, pl with
| [], [] ->
fprintf fmt "%a" (print_uident info) ls.ls_name
| [], [p] ->
fprintf fmt "%a %a"
(print_uident info) ls.ls_name (print_pat info) p
| [], _ ->
fprintf fmt "%a (%a)"
(print_uident info) ls.ls_name
(print_list comma (print_pat info)) pl
| _, _ ->
let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
match l1, l2 with
| x1 :: r1, x2 :: r2 ->
print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
print_list2 sep sep_m print1 print2 fmt (r1, r2)
| _ -> ()
in
let print_rs info fmt rs =
fprintf fmt "%a" (print_lident info) rs.rs_name in
fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
let pjl = let rs = restore_rs ls in get_record info rs in
match pjl with
| [] -> print_papp info ls fmt pl
| pjl ->
fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_pat info)) (pjl, pl)
and print_papp info ls fmt = function
| [] -> fprintf fmt "%a" (print_uident info) ls.ls_name
| [p] -> fprintf fmt "%a %a" (print_uident info) ls.ls_name
(print_pat info) p
| pl -> fprintf fmt "%a (%a)" (print_uident info) ls.ls_name
(print_list comma (print_pat info)) pl
(** Expressions *)
......@@ -261,14 +259,6 @@ module Print = struct
fprintf fmt "@[<hov 2>%a (%a)@]"
print_ident rs.rs_name (print_list comma (print_expr info)) tl
else
let rec print_list2 sep sep_m print1 print2 fmt (l1, l2) =
match l1, l2 with
| x1 :: r1, x2 :: r2 ->
print1 fmt x1; sep_m fmt (); print2 fmt x2; sep fmt ();
print_list2 sep sep_m print1 print2 fmt (r1, r2)
| _ -> () in
let print_rs info fmt rs =
fprintf fmt "%a" (print_lident info) rs.rs_name in
fprintf fmt "@[<hov 2>{ %a}@]"
(print_list2 semi equal (print_rs info) (print_expr info)) (pjl, tl)
| _, _, tl ->
......@@ -279,20 +269,20 @@ module Print = struct
| Lvar (pv, e) ->
fprintf fmt "@[<hov 2>let %a =@ %a@]"
(print_lident info) (pv_name pv) (print_expr info) e;
| Lsym (rs, args, ef) ->
fprintf fmt "@[<hov 2>let %a@ @[%a@]@ =@ @[%a@]@]"
| Lsym (rs, res, args, ef) ->
fprintf fmt "@[<hov 2>let %a@[%a@] : %a@ =@ @[%a@]@]"
(print_lident info) rs.rs_name
(print_list space (print_vs_arg info)) args
(print_expr info) ef;
(print_list_pre space (print_vs_arg info)) args
(print_ty info) res (print_expr info) ef;
forget_vars args
| Lrec (rdef) ->
let print_one fst fmt = function
| { rec_sym = rs1; rec_args = args; rec_exp = e } ->
fprintf fmt "@[<hov 2>%s %a@ %a@ =@ %a@]"
| { rec_sym = rs1; rec_args = args; rec_exp = e; rec_res = res } ->
fprintf fmt "@[<hov 2>%s %a@ %a :@ %a@ =@ %a@]"
(if fst then "let rec" else "and")
(print_lident info) rs1.rs_name
(print_list space (print_vs_arg info)) args
(print_expr info) e;
(print_ty info) res (print_expr info) e;
forget_vars args;
(* forget_tvs () *)
in
......@@ -307,11 +297,11 @@ module Print = struct
| Evar pvs ->
(print_lident info) fmt (pv_name pvs)
| Elet (let_def, e) ->
fprintf fmt "@[%a@] in@ %a"
fprintf fmt (protect_on paren "@[%a@] in@ %a")
(print_let_def info) let_def (print_expr info) e;
forget_let_defn let_def
| Eabsurd ->
fprintf fmt "assert false (* absurd *)"
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Eapp (s, []) when rs_equal s rs_true ->
fprintf fmt "true"
| Eapp (s, []) when rs_equal s rs_false ->
......@@ -323,7 +313,8 @@ module Print = struct
fprintf fmt (protect_on paren "%a")
(print_apply info (Hrs.find_def ht_rs s s)) pvl
| Ematch (e, pl) ->
fprintf fmt "begin match @[%a@] with@\n@[<hov>%a@]@\nend"
fprintf fmt (protect_on paren
"begin match @[%a@] with@\n@[<hov>%a@]@\nend")
(print_expr info) e (print_list newline (print_branch info)) pl
| Eassign al ->
let assign fmt (rho, rs, pv) =
......@@ -334,8 +325,11 @@ module Print = struct
| [] -> assert false | [a] -> assign fmt a
| al -> fprintf fmt "@[begin %a end@]" (print_list semi assign) al end
| Eif (e1, e2, {e_node = Eblock []}) ->
fprintf fmt "@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]"
fprintf fmt (protect_on paren
"@[<hv>@[<hov 2>if@ %a@]@ then begin@;<1 2>@[%a@] end@]")
(print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) when is_false e2 && is_true e3 ->
fprintf fmt (protect_on paren "not %a") (print_expr info ~paren:true) e1
| Eif (e1, e2, e3) when is_true e2 ->
fprintf fmt (protect_on paren "@[<hv>%a || %a@]")
(print_expr info) e1 (print_expr info) e3
......@@ -343,8 +337,8 @@ module Print = struct
fprintf fmt (protect_on paren "@[<hv>%a && %a@]")
(print_expr info) e1 (print_expr info) e2
| Eif (e1, e2, e3) ->
fprintf fmt
"@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]"
fprintf fmt (protect_on paren
"@[<hv>@[<hov 2>if@ %a@]@ then@;<1 2>@[%a@]@;<1 0>else@;<1 2>@[%a@]@]")
(print_expr info) e1 (print_expr info) e2 (print_expr info) e3
| Eblock [] ->
fprintf fmt "()"
......@@ -354,17 +348,14 @@ module Print = struct
fprintf fmt "@[<hv>begin@;<1 2>@[%a@]@ end@]"
(print_list semi (print_expr info)) el
| Efun (varl, e) ->
fprintf fmt "@[<hov 2>(fun %a ->@ %a)@]"
fprintf fmt (protect_on paren "@[<hov 2>(fun %a ->@ %a)@]")
(print_list space (print_vs_arg info)) varl (print_expr info) e
| Ewhile (e1, e2) ->
fprintf fmt "@[<hov 2>while %a do@ %a@ done@]"
(print_expr info) e1 (print_expr info) e2
| Eraise (xs, None) -> (* FIXME : check exceptions in driver *)
fprintf fmt (protect_on paren "raise %a") (print_uident info) xs.xs_name
| Eraise (xs, Some e) ->
fprintf fmt (protect_on paren "raise (%a %a)")
(print_uident info) xs.xs_name (print_expr ~paren:true info) e
| Etuple _ -> (* TODO *) assert false
| Eraise (xs, e_opt) ->
print_raise ~paren info xs fmt e_opt
(* | Etuple _ -> (\* TODO *\) assert false *)
| Efor (pv1, pv2, direction, pv3, e) ->
let print_for_direction fmt = function
| To -> fprintf fmt "to"
......@@ -372,45 +363,57 @@ module Print = struct
in
fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
(print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
print_for_direction direction
(print_lident info) (pv_name pv3) (print_expr info) e
print_for_direction direction (print_lident info) (pv_name pv3)
(print_expr info) e
| Etry (e, bl) ->
fprintf fmt
"@[<hv>@[<hov 2>begin@ try@ %a@] with@]@\n@[<hov>%a@]@\nend"
(print_expr info) e (print_list newline (print_xbranch info)) bl
| Enot _ -> (* TODO *) assert false
| Ebinop _ -> (* TODO *) assert false
| Ecast _ -> (* TODO *) assert false
(* | Enot _ -> (\* TODO *\) assert false *)
(* | Ebinop _ -> (\* TODO *\) assert false *)
(* | Ecast _ -> (\* TODO *\) assert false *)
and print_branch info fmt (p, e) =
fprintf fmt "@[<hov 4>| %a ->@ @[%a@]@]"
(print_pat info) p (print_expr info) e
and print_raise ~paren info xs fmt e_opt =
match query_syntax info.info_syn xs.xs_name, e_opt with
| Some s, None ->
fprintf fmt "raise %s" s
| Some s, Some e ->
fprintf fmt (protect_on paren "raise (%a)")
(syntax_arguments s (print_expr info)) [e]
| None, None ->
fprintf fmt (protect_on paren "raise %a")
(print_uident info) xs.xs_name
| None, Some e ->
fprintf fmt (protect_on paren "raise (%a %a)")
(print_uident info) xs.xs_name (print_expr ~paren:true info) e
and print_xbranch info fmt (xs, pvl, e) =
let print_var fmt pv =
print_lident info fmt (pv_name pv) in
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) (xs.xs_name)
(print_list nothing print_var) pvl (print_expr info) e
match query_syntax info.info_syn xs.xs_name with
| Some s ->
fprintf fmt "@[<hov 4>| %a ->@ %a@]"
(syntax_arguments s print_var) pvl (print_expr info ~paren:true) e
| None ->
fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) (xs.xs_name)
(print_list nothing print_var) pvl (print_expr info) e
and print_expr ?(paren=false) info fmt e =
print_enode ~paren info fmt e.e_node
let print_type_decl info fmt its =
let print_type_decl info fst fmt its =
let print_constr fmt (id, cs_args) =
match cs_args with
| [] ->
fprintf fmt "@[<hov 4>| %a@]"
print_ident id (* FIXME: first letter must be uppercase
-> print_uident *)
| l ->
fprintf fmt "@[<hov 4>| %a of %a@]"
print_ident id (* FIXME: print_uident *)
(print_list star (print_ty ~paren:false info)) l in
| [] -> fprintf fmt "@[<hov 4>| %a@]" (print_uident info) id
| l -> fprintf fmt "@[<hov 4>| %a of %a@]" (print_uident info) id
(print_list star (print_ty ~paren:false info)) l in
let print_field fmt (is_mutable, id, ty) =
fprintf fmt "%s%a: %a;"
(if is_mutable then "mutable " else "")
print_ident id
(print_ty ~paren:false info) ty in
fprintf fmt "%s%a: %a;" (if is_mutable then "mutable " else "")
print_ident id (print_ty ~paren:false info) ty in
let print_def fmt = function
| None ->
()
......@@ -424,19 +427,16 @@ module Print = struct
fprintf fmt " =@ %a" (print_ty ~paren:false info) ty
in
fprintf fmt "@[<hov 2>%s %a%a%a@]"
(if true then "type" else "and") (* FIXME: mutual recursive types *)
print_tv_args its.its_args
print_ident its.its_name (* FIXME: first letter must be lowercase
-> print_lident *)
print_def its.its_def
(if fst then "type" else "and") print_tv_args its.its_args
(print_lident info) its.its_name print_def its.its_def
let print_decl info fmt = function
| Dlet (ldef) ->
| Dlet ldef ->
print_let_def info fmt ldef;
forget_tvs ();
fprintf fmt "@\n@\n"
| Dtype dl ->
print_list newline (print_type_decl info) fmt dl;
print_list_next newline (print_type_decl info) fmt dl;
fprintf fmt "@\n@\n"
| Dexn (xs, None) ->
fprintf fmt "exception %a@\n@\n" print_ident xs.xs_name
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment