Commit 0f57a419 authored by Raphaël Rieu-Helft's avatar Raphaël Rieu-Helft

Merge branch 'rich_ml_ast' into 'master'

Extraction fixes

Closes #481 and #325

See merge request !364
parents c1e14686 24d7685d
......@@ -3,9 +3,8 @@
printer "cakeml"
theory BuiltIn
module BuiltIn
syntax type int "int"
syntax predicate (=) "%1 = %2"
end
module HighOrd
......@@ -13,44 +12,44 @@ module HighOrd
syntax val ( @ ) "%1 %2"
end
theory option.Option
module option.Option
syntax type option "%1 option"
syntax function None "NONE"
syntax function Some "SOME %1"
syntax val None "NONE"
syntax val Some "SOME %1"
end
theory Bool
module Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax val True "true"
syntax val False "false"
end
theory bool.Ite
syntax function ite "(if %1 then %2 else %3)"
module bool.Ite
syntax val ite "(if %1 then %2 else %3)"
end
theory bool.Bool
syntax function andb "%1 andalso %2"
syntax function orb "%1 orelse %2"
syntax function xorb "%1 <> %2"
syntax function notb "not %1"
syntax function implb "not %1 orelse %2"
module bool.Bool
syntax val andb "%1 andalso %2"
syntax val orb "%1 orelse %2"
syntax val xorb "%1 <> %2"
syntax val notb "not %1"
syntax val implb "not %1 orelse %2"
end
theory list.List
module list.List
syntax type list "%1 list"
syntax function Nil "[]"
syntax function Cons "%1 :: %2"
syntax predicate is_nil "%1 = []"
syntax val Nil "[]"
syntax val Cons "%1 :: %2"
syntax val is_nil "%1 = []"
end
theory list.Length
syntax function length "List.length %1"
module list.Length
syntax val length "List.length %1"
end
module Ref
syntax type ref "%1 ref"
syntax function contents "!%1"
syntax val contents "!%1"
syntax val ref "ref %1"
end
......@@ -68,19 +67,19 @@ module ref.Refint
end
module int.Int
syntax constant zero "0"
syntax constant one "1"
syntax val zero "0"
syntax val one "1"
syntax predicate (<) "%1 < %2"
syntax predicate (<=) "%1 <= %2"
syntax predicate (>) "%1 > %2"
syntax predicate (>=) "%1 >= %2"
syntax val (<) "%1 < %2"
syntax val (<=) "%1 <= %2"
syntax val (>) "%1 > %2"
syntax val (>=) "%1 >= %2"
syntax val (=) "%1 = %2"
syntax function (+) "%1 + %2"
syntax function (-) "%1 - %2"
syntax function ( * ) "%1 * %2"
syntax function (-_) "~%1"
syntax val (+) "%1 + %2"
syntax val (-) "%1 - %2"
syntax val ( * ) "%1 * %2"
syntax val (-_) "~%1"
end
module int.EuclideanDivision
......
This diff is collapsed.
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Compile
open Format
open Ident
open Pp
......@@ -97,15 +96,6 @@ module Print = struct
let pv_name pv = pv.pv_vs.vs_name
let print_pv info fmt pv = print_lident info fmt (pv_name pv)
(* FIXME put these in Compile*)
let is_true e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_true
| _ -> false
let is_false e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_false
| _ -> false
let is_mapped_to_int info ity =
match ity.ity_node with
| Ityapp ({ its_ts = ts }, _, _) ->
......@@ -238,8 +228,8 @@ module Print = struct
| Econst (Constant.ConstInt c) ->
let n = c.Number.il_int in
let n = BigInt.to_string n in
let id = match e.e_ity with
| I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
let id = match e.e_mlty with
| Tapp (tname, _) -> tname
| _ -> assert false in
(match query_syntax info.info_literal id with
| Some s -> syntax_arguments s print_constant fmt [e]
......@@ -255,13 +245,11 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on paren "assert false (* absurd *)")
| Eapp (rs, []) when rs_equal rs rs_true ->
| Eapp (rs, [], false) when rs_equal rs rs_true ->
fprintf fmt "true"
| Eapp (rs, []) when rs_equal rs rs_false ->
| Eapp (rs, [], false) when rs_equal rs rs_false ->
fprintf fmt "false"
| Eapp (rs, []) -> (* avoids parenthesis around values *)
fprintf fmt "%a" (print_apply info rs) []
| Eapp (rs, pvl) ->
| Eapp (rs, pvl, _) ->
fprintf fmt (protect_on paren "%a")
(print_apply info rs) pvl
| Ematch (e1, [p, e2], []) ->
......@@ -281,10 +269,10 @@ module Print = struct
(print_expr info) e (print_list_next newline (print_branch info)) bl
(print_list_next newline (print_xbranch true info)) xl
| Eassign al ->
let assign fmt (rho, rs, e) =
let assign fmt (e1, _, rs, e2) =
fprintf fmt "@[<hov 2>%a.%a <-@ %a@]"
(print_lident info) (pv_name rho) (print_lident info) rs.rs_name
(print_expr info) e in
(print_expr info) e1 (print_lident info) rs.rs_name
(print_expr info) e2 in
begin match al with
| [] -> assert false | [a] -> assign fmt a
| al -> fprintf fmt "@[(%a)]" (print_list semi assign) al end
......@@ -320,7 +308,7 @@ module Print = struct
(print_expr info) e1 (print_expr info) e2
| Eraise (xs, e_opt) ->
print_raise ~paren info xs fmt e_opt
| Efor (pv1, pv2, dir, pv3, e) ->
| Efor (pv1, _ty, pv2, dir, pv3, e) ->
if is_mapped_to_int info pv1.pv_ity then
fprintf fmt "@[<hov 2>for %a = %a %a %a do@ @[%a@]@ done@]"
(print_lident info) (pv_name pv1) (print_lident info) (pv_name pv2)
......
This diff is collapsed.
......@@ -9,9 +9,6 @@
(* *)
(********************************************************************)
val clean_name : string -> string
val module_name : ?fname:string -> string list -> string -> string
module Translate : sig
val module_ : Pmodule.pmodule -> Mltree.pmodule
......@@ -46,9 +43,12 @@ module InlineProxyVars : sig
end
module InlineTrivialLets : sig
module ExprSimplifications : sig
(* Optimizes trivial let-ins of the form `let x = e in x`. *)
(* Expression optimizations:
- Optimizes trivial let-ins of the form `let x = e in x`.
- Optimizes trivial matches of the form `match e1 with x -> e2 end`.
*)
val module_ : Mltree.pmodule -> Mltree.pmodule
end
......
......@@ -22,7 +22,6 @@ open Printer
open Pp
open Theory
open Pmodule
open Compile
open Mltree
......@@ -50,6 +49,20 @@ let create_info pargs fname ~flat ({mod_theory = th} as m) = {
info_current_ph = [];
}
let clean_name fname =
(* TODO: replace with Filename.remove_extension
* after migration to OCaml 4.04+ *)
let remove_extension s =
try Filename.chop_extension s with Invalid_argument _ -> s in
let f = Filename.basename fname in (remove_extension f)
let module_name ?fname path t =
let fname = match fname, path with
| None, "why3"::_ -> "why3"
| None, _ -> String.concat "__" path
| Some f, _ -> clean_name f in
fname ^ "__" ^ t
let add_current_path info s =
{ info with info_current_ph = s :: info.info_current_ph }
......@@ -198,6 +211,9 @@ module MLPrinter (K: sig val keywords: string list end) = struct
| Ttuple tl ->
fprintf fmt (protect_on paren "@[%a@]")
(print_list star (print_ty ~paren:true info)) tl
| Tarrow (t1, t2) ->
fprintf fmt (protect_on paren "%a -> %a")
(print_ty ~paren info) t1 (print_ty ~paren info) t2
| Tapp (ts, tl) ->
match query_syntax info.info_syn ts with
| Some s ->
......
......@@ -13,6 +13,10 @@ open Pp
open Printer
open Mltree
val clean_name : string -> string
val module_name : ?fname:string -> string list -> string -> string
val protect_on :
bool -> ('a, 'b, 'c, 'd, 'e, 'f) format6 -> ('a, 'b, 'c, 'd, 'e, 'f) format6
......
......@@ -615,7 +615,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
with Not_found ->
Debug.dprintf debug_interp "var %a not found@." print_pv pv;
raise CannotReduce)
| Eapp (rs, le) -> begin
| Eapp (rs, le, _) -> begin
Debug.dprintf debug_interp "Eapp %a@." Expr.print_rs rs;
let eval_call info vl e rs =
Debug.dprintf debug_interp "eval params@.";
......@@ -702,9 +702,12 @@ let rec interp_expr info (e:Mltree.expr) : value =
end
| Eassign l ->
List.iter
(fun (pvs, rs, e) ->
(fun (epv, _, rs, e) ->
let fld = fd_of_rs rs in
let value = interp_expr info e in
let pvs = match epv.e_node with
| Evar pv -> pv
| _ -> assert false in
match get pvs info with
| Vconstr(c, args) ->
let rec aux cargs args =
......@@ -735,7 +738,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
interp_expr info e
| Vbool false -> Vvoid
| _ -> assert false end
| Efor (x, pv1, dir, pv2, e) ->
| Efor (x, _, pv1, dir, pv2, e) ->
Debug.dprintf debug_interp "for@.";
begin match (get pv1 info, get pv2 info) with
| (Vbigint i1, Vbigint i2) ->
......
......@@ -18,6 +18,7 @@ open Term
type ty =
| Tvar of tvsymbol
| Tapp of ident * ty list
| Tarrow of ty * ty
| Ttuple of ty list
type is_ghost = bool
......@@ -35,6 +36,7 @@ type pat =
| Pas of pat * vsymbol
type is_rec = bool
type is_partial = bool
type binop = Band | Bor | Beq
......@@ -43,6 +45,7 @@ type ity = I of Ity.ity | C of Ity.cty (* TODO: keep it like this? *)
type expr = {
e_node : expr_node;
e_ity : ity;
e_mlty : ty;
e_effect : effect;
e_attrs : Sattr.t;
}
......@@ -50,16 +53,17 @@ type expr = {
and expr_node =
| Econst of Constant.constant
| Evar of pvsymbol
| Eapp of rsymbol * expr list
| Eapp of rsymbol * expr list * is_partial
| Efun of var list * expr
| Elet of let_def * expr
| Eif of expr * expr * expr
| Eassign of (pvsymbol * rsymbol * expr) list
| Eassign of (expr * ty * rsymbol * expr) list
| Ematch of expr * reg_branch list * exn_branch list
| Eblock of expr list
| Ewhile of expr * expr
(* For loop for Why3's type int *)
| Efor of pvsymbol * pvsymbol * for_direction * pvsymbol * expr
(* For loop on a range type *)
(* index var, index ty, start, direction, end, expr *)
| Efor of pvsymbol * ty * pvsymbol * for_direction * pvsymbol * expr
| Eraise of xsymbol * expr option
| Eexn of xsymbol * ty option * expr
| Eignore of expr
......@@ -148,7 +152,8 @@ let rec add_known_decl decl k_map id =
let rec iter_deps_ty f = function
| Tvar _ -> ()
| Tapp (id, ty_l) -> f id; List.iter (iter_deps_ty f) ty_l
| Tarrow (ty1, ty2) -> iter_deps_ty f ty1; iter_deps_ty f ty2
| Tapp (s, ty_l) -> f s; List.iter (iter_deps_ty f) ty_l
| Ttuple ty_l -> List.iter (iter_deps_ty f) ty_l
let iter_deps_typedef f = function
......@@ -185,7 +190,7 @@ and iter_deps_pat f = function
and iter_deps_expr f e = match e.e_node with
| Econst _ | Eabsurd -> ()
| Evar pv -> f pv.pv_vs.vs_name
| Eapp (rs, exprl) ->
| Eapp (rs, exprl, _) ->
f rs.rs_name; List.iter (iter_deps_expr f) exprl
| Efun (args, e) ->
List.iter (fun (_, ty_arg, _) -> iter_deps_ty f ty_arg) args;
......@@ -221,7 +226,8 @@ and iter_deps_expr f e = match e.e_node with
| Ewhile (e1, e2) ->
iter_deps_expr f e1;
iter_deps_expr f e2
| Efor (_, _, _, _, e) ->
| Efor (_, ty, _, _, _, e) ->
iter_deps_ty f ty;
iter_deps_expr f e
| Eraise (xs, None) ->
f xs.xs_name
......@@ -233,8 +239,8 @@ and iter_deps_expr f e = match e.e_node with
| Eexn (_xs, Some ty, e) -> (* FIXME? How come we never do binding here? *)
iter_deps_ty f ty;
iter_deps_expr f e
| Eassign assingl ->
List.iter (fun (_, rs, _) -> f rs.rs_name) assingl
| Eassign assignl ->
List.iter (fun (_, ty, rs, _) -> iter_deps_ty f ty; f rs.rs_name) assignl
| Eignore e -> iter_deps_expr f e
let rec iter_deps f = function
......@@ -270,8 +276,8 @@ let ity_of_mask ity mask =
I (ity_tuple tl)
| _ -> ity (* FIXME ? *)
let mk_expr e_node e_ity mask e_effect e_attrs =
{ e_node; e_ity = ity_of_mask e_ity mask; e_effect; e_attrs; }
let mk_expr e_node e_ity mask e_mlty e_effect e_attrs =
{ e_node; e_ity = ity_of_mask e_ity mask; e_mlty; e_effect; e_attrs; }
let tunit = Ttuple []
......@@ -279,6 +285,19 @@ let is_unit = function
| I i -> ity_equal i Ity.ity_unit
| _ -> false
let is_true e = match e.e_node with
| Eapp (s, [], false) -> rs_equal s rs_true
| _ -> false
let is_false e = match e.e_node with
| Eapp (s, [], false) -> rs_equal s rs_false
| _ -> false
let t_arrow t1 t2 = Tarrow (t1, t2)
let t_fun params res =
List.fold_right (fun (_, targ, _) ty -> t_arrow targ ty) params res
let enope = Eblock []
let mk_var id ty ghost = (id, ty, ghost)
......@@ -292,7 +311,7 @@ let mk_its_defn its_name its_args its_private its_def =
(* smart constructors *)
let e_unit attrs =
mk_expr enope (I Ity.ity_unit) MaskVisible Ity.eff_empty attrs
mk_expr enope (I Ity.ity_unit) MaskVisible tunit Ity.eff_empty attrs
let dummy_expr_attr = Ident.create_attribute "__dummy_expr__"
......@@ -313,15 +332,14 @@ let sym_defn f svars ty_res args e =
let e_let ld e = mk_expr (Elet (ld, e))
let e_app rs pvl =
mk_expr (Eapp (rs, pvl))
let e_app rs pvl partial =
mk_expr (Eapp (rs, pvl, partial))
let e_fun args e = mk_expr (Efun (args, e))
let e_ignore e_ity e =
(* TODO : avoid ignore around a unit type expresson *)
if ity_equal e_ity Ity.ity_unit then e
else mk_expr (Eignore e) ity_unit MaskVisible e.e_effect e.e_attrs
let e_ignore e =
if is_unit e.e_ity then e
else mk_expr (Eignore e) ity_unit MaskVisible tunit e.e_effect e.e_attrs
let e_if e1 e2 e3 =
mk_expr (Eif (e1, e2, e3)) e2.e_ity
......@@ -329,8 +347,8 @@ let e_if e1 e2 e3 =
let e_while e1 e2 =
mk_expr (Ewhile (e1, e2)) ity_unit
let e_for pv1 pv2 dir pv3 e1 =
mk_expr (Efor (pv1, pv2, dir, pv3, e1)) ity_unit
let e_for pv1 ty pv2 dir pv3 e1 =
mk_expr (Efor (pv1, ty, pv2, dir, pv3, e1)) ity_unit
let e_match e bl xl =
mk_expr (Ematch (e, bl, xl))
......@@ -343,7 +361,7 @@ let e_match e bl xl =
*)
let e_assign al ity mask eff attrs =
if al = [] then e_unit else mk_expr (Eassign al) ity mask eff attrs
if al = [] then e_unit else mk_expr (Eassign al) ity mask tunit eff attrs
let e_absurd =
mk_expr Eabsurd
......@@ -357,10 +375,10 @@ let e_seq e1 e2 =
| _ -> Eblock [e1; e2] in
mk_expr e
let var_list_of_pv_list pvl =
let mk_var pv = mk_expr (Evar pv) (I pv.pv_ity)
MaskVisible eff_empty Sattr.empty in
List.map mk_var pvl
let var_list_of_pv_list pvl mltyl =
let mk_var pv mlty = mk_expr (Evar pv) (I pv.pv_ity)
MaskVisible mlty eff_empty Sattr.empty in
List.map2 mk_var pvl mltyl
let ld_map fn ld = match ld with
| Lsym (rs, tv, ty, vl, e) -> Lsym (rs, tv, ty, vl, fn e)
......@@ -373,11 +391,11 @@ let e_map fn e =
let mk en = { e with e_node = en } in
match e.e_node with
| Econst _ | Evar _ | Efun (_,_) | Eabsurd -> e
| Eapp (rs,el) -> mk (Eapp(rs,(List.map fn el)))
| Eapp (rs,el, p) -> mk (Eapp(rs,(List.map fn el), p))
| Elet (ld,e) -> mk (Elet (ld_map fn ld, fn e))
| Eif (c,t,e) -> mk (Eif (fn c, fn t, fn e))
| Eassign al ->
let al' = List.map (fun (pv, rs, e) -> pv, rs, fn e) al in
let al' = List.map (fun (e1, ty, rs, e2) -> fn e1, ty, rs, fn e2) al in
mk (Eassign al')
| Ematch (e,bl,xl) ->
let bl' = List.map (fun (p,e) -> (p, fn e)) bl in
......@@ -385,7 +403,7 @@ let e_map fn e =
mk (Ematch (fn e, bl', xl'))
| Eblock el -> mk (Eblock (List.map fn el))
| Ewhile (c,b) -> mk (Ewhile (fn c, fn b))
| Efor (i,vb,d,ve,e) -> mk (Efor (i, vb, d, ve, fn e))
| Efor (i,ty,vb,d,ve,e) -> mk (Efor (i, ty, vb, d, ve, fn e))
| Eraise (_, None) -> e
| Eraise (x, Some e) -> mk (Eraise (x, Some (fn e)))
| Eexn (x,t,e) -> mk (Eexn (x, t, fn e))
......@@ -401,20 +419,21 @@ let e_fold fn acc e =
match e.e_node with
| Econst _ | Evar _
| Efun (_,_) | Eabsurd -> acc
| Eapp (_,el) -> List.fold_left fn acc el
| Eapp (_,el,_) -> List.fold_left fn acc el
| Elet (ld,e) -> fn (ld_fold fn acc ld) e
| Eif (c,t,e) ->
let acc = fn acc c in
let acc = fn acc t in
fn acc e
| Eassign al -> List.fold_left (fun acc (_,_,e) -> fn acc e) acc al
| Eassign al ->
List.fold_left (fun acc (e1,_,_,e2) -> fn (fn acc e2) e1) acc al
| Ematch (e,bl,xl) ->
let acc = List.fold_left (fun acc (_p,e) -> fn acc e) acc bl in
let acc = List.fold_left (fun acc (_x, _vl, e) -> fn acc e) acc xl in
fn acc e
| Eblock el -> List.fold_left fn acc el
| Ewhile (c,b) -> fn (fn acc c) b
| Efor (_,_,_,_,e) -> fn acc e
| Efor (_,_,_,_,_,e) -> fn acc e
| Eraise (_, None) -> acc
| Eraise (_, Some e) -> fn acc e
| Eexn (_x,_t,e) -> fn acc e
......@@ -442,9 +461,9 @@ let e_map_fold fn acc e =
match e.e_node with
| Econst _ | Evar _
| Efun (_,_) | Eabsurd -> acc, e
| Eapp (rs,el) ->
| Eapp (rs,el,p) ->
let acc,el = Lists.map_fold_left fn acc el in
acc,mk (Eapp(rs,el))
acc,mk (Eapp(rs,el,p))
| Elet (ld,e) ->
let acc, ld = ld_map_fold fn acc ld in
let acc, e = fn acc e in
......@@ -457,9 +476,10 @@ let e_map_fold fn acc e =
| Eassign al ->
let acc,al' =
Lists.map_fold_left
(fun acc (pv, rs, e) ->
let acc, e = fn acc e in
acc, (pv, rs, e))
(fun acc (e1, ty, rs, e2) ->
let acc, e2' = fn acc e2 in
let acc, e1' = fn acc e1 in
acc, (e1', ty, rs, e2'))
acc al in
acc, mk (Eassign al')
| Ematch (e,bl,xl) ->
......@@ -482,9 +502,9 @@ let e_map_fold fn acc e =
let acc, c' = fn acc c in
let acc, b' = fn acc b in
acc, mk (Ewhile (c', b'))
| Efor (i,vb,d,ve,e) ->
| Efor (i,ty,vb,d,ve,e) ->
let acc, e' = fn acc e in
acc, mk (Efor (i, vb, d, ve, e'))
acc, mk (Efor (i, ty, vb, d, ve, e'))
| Eraise (_, None) -> acc, e
| Eraise (x, Some e) ->
let acc, e' = fn acc e in
......
......@@ -11,7 +11,6 @@
(** Printer for extracted OCaml code *)
open Compile
open Format
open Ident
open Pp
......@@ -165,7 +164,7 @@ module Print = struct
let p, t, q =
try Pmodule.restore_path id with Not_found -> Theory.restore_path id in
let fname = if p = [] then info.info_fname else None in
let m = Strings.capitalize (module_name ?fname p t) in
let m = Strings.capitalize (Ml_printer.module_name ?fname p t) in
fprintf fmt "%s.%a" m (print_path ~sanitizer) (q, id)
with
| Not_found ->
......@@ -227,6 +226,10 @@ module Print = struct
| Ttuple tl ->
fprintf fmt (protect_on paren "@[%a@]")
(print_list star (print_ty ~use_quote ~paren:true info)) tl
| Tarrow (t1, t2) ->
fprintf fmt (protect_on paren "%a -> %a")
(print_ty ~use_quote ~paren info) t1
(print_ty ~use_quote ~paren info) t2
| Tapp (ts, tl) ->
match query_syntax info.info_syn ts with
| Some s when complex_syntax s ->
......@@ -270,12 +273,14 @@ module Print = struct
else fprintf fmt "(%a:@ %a)" (print_lident info) id
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty_opt_fun info fmt id = function
let print_vsty_opt_fun info fmt id ty = match ty with
| Tapp (id_ty, [arg]) ->
assert (query_syntax info.info_syn id_ty = Some "%1 option");
fprintf fmt "?%s:%a" id.id_string
(print_ty ~use_quote:false ~paren:false info) arg
| _ -> invalid_arg "print_vsty_opt_fun" (*FIXME : better error message *)
| _ ->
Loc.errorm "invalid optional argument of type %a"
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty_named_fun info fmt id ty =
fprintf fmt "%s:%a" id.id_string
......@@ -355,15 +360,6 @@ module Print = struct
let pv_name pv = pv.pv_vs.vs_name
let print_pv info fmt pv = print_lident info fmt (pv_name pv)
(* FIXME put these in Compile*)
let is_true e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_true
| _ -> false
let is_false e = match e.e_node with
| Eapp (s, []) -> rs_equal s rs_false
| _ -> false
let is_field rs =
match rs.rs_field with
| None -> false
......@@ -400,7 +396,7 @@ module Print = struct
| expr :: exprl, pv :: pvl ->
if is_optional ~attrs:(pv_name pv).id_attrs then
begin match expr.e_node with
| Eapp (rs, _)
| Eapp (rs, _, false)
when query_syntax info.info_syn rs.rs_name = Some "None" -> ()
| _ -> fprintf fmt "?%s:%a" (pv_name pv).id_string
(print_expr info 1) expr end
......@@ -543,8 +539,8 @@ module Print = struct
| Econst (Constant.ConstInt c) ->
let n = c.Number.il_int in
let n = BigInt.to_string n in
let id = match e.e_ity with
| I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
let id = match e.e_mlty with
| Tapp (tname, _) -> tname
| _ -> assert false in
(match query_syntax info.info_literal id with
| Some s -> syntax_arguments s print_constant fmt [e]
......@@ -562,15 +558,14 @@ module Print = struct
forget_let_defn let_def
| Eabsurd ->
fprintf fmt (protect_on (opr && prec < 4) "assert false (* absurd *)")
| Eapp (rs, []) when rs_equal rs rs_true ->
| Eapp (rs, [], _) when rs_equal rs rs_true ->