let rec print_expression e = 
  (match e with
     | EPrimApp (_, PCharConstant c, _) -> 
        pp_print_string !ppf ("'"^ String.make 1 c ^"'")
     | EPrimApp (_, PIntegerConstant i, _) -> 
        pp_print_string !ppf (string_of_int i)
     | EPrimApp (_, PUnit, _) -> 
        pp_print_string !ppf "()"
     | EAssertFalse _ -> pp_print_string !ppf "assert false"
     | EVar (_, SName name) -> pp_print_string !ppf name
     | EDCon (_, DName "_Unit", es) ->
         pp_print_string !ppf "()"
     | EDCon (_, DName "_Tuple", es) ->
         pp_print_string !ppf "(";
         print_separated_list "," print_expression es;
         pp_print_string !ppf ")"
     | EDCon (_, DName dname, []) ->
         pp_print_string !ppf "(";
         pp_print_string !ppf dname; 
         pp_print_string !ppf ")"
     | EDCon (_, DName dname, es) -> 
         pp_print_string !ppf "(";
         pp_print_string !ppf dname; 
         pp_print_string !ppf " ";
         print_separated_list " " print_expression es;
         pp_print_string !ppf ")"
     | ELambda (_, pat, exp) ->
         pp_print_string !ppf "\\";
         print_pattern pat;
         pp_print_string !ppf ".";
         pp_print_cut !ppf (); 
         print_expression exp;
     | EApp (_, t1, t2) ->
         pp_print_string !ppf "(";
         print_expression t1;
         pp_print_string !ppf " ";
         print_expression t2;
         pp_print_string !ppf ")"
     | EMatch (_, e, cs) ->
         pp_open_hvbox !ppf 0; 
         pp_print_string !ppf "match ";
         print_expression e;
         pp_print_string !ppf " with ";
         pp_print_cut !ppf ();
         print_separated_list "| " print_clause cs;
         pp_print_string !ppf "end ";
         pp_close_box !ppf ();
     | EBinding (_, bd, exp) -> 
         pp_open_box !ppf 0;
         print_binding bd;
         pp_print_string !ppf " in ";
         print_expression exp;
         pp_close_box !ppf ();
     | ETypeConstraint (_, exp, ty) -> 
         pp_print_string !ppf "(";
         print_expression exp;
         pp_print_string !ppf " : ";
         print_type ty;
         pp_print_string !ppf ")"
     | EForall (_, vs, e) ->
         fprintf !ppf "forall ";
         pp_print_string !ppf ".";
         print_expression e
     | EExists (_, vs, e) ->
         fprintf !ppf "exists ";
         print_separated_list " " 
           (fun (TName x) -> pp_print_string !ppf x) vs;
         pp_print_string !ppf ".";
         print_expression e
     | ERecordEmpty _ ->
         pp_print_string !ppf "{}"
     | ERecordAccess (_, exp, LName name) -> 
         print_expression exp;
         pp_print_string !ppf ".";
         pp_print_string !ppf name;
     | ERecordExtend (_, bds, ERecordEmpty _) -> 
         pp_print_string !ppf "{ ";
         print_record_binding bds;
         pp_print_string !ppf "} ";
     | ERecordExtend _ -> assert false
     | ERecordUpdate (_, exp, LName label, v) -> 
         print_expression exp;
         pp_print_string !ppf ".";
         pp_print_string !ppf label;
         pp_print_string !ppf " <- ";
         print_expression v);

and print_record_binding bds = 
  print_separated_list ";" 
    (fun (LName name, exp) ->
       pp_print_string !ppf (name^" = ");
       print_expression exp) bds

and print_binding b =
  (match b with
     | BindValue (pos, vs) ->
         pp_print_string !ppf "let ";
         print_separated_list " and " print_value_definition vs;
     | BindRecValue (pos, vs) ->
         pp_print_string !ppf "let rec ";
         print_separated_list " and " print_value_definition vs;
     | TypeDec (_, tds) ->
         pp_print_string !ppf "type ";
         print_separated_list " and " print_type_declaration tds)

and print_value_definition (_, tnames, pat, expression) =
  let rec chop_args pat expression = 
    match (pat, expression) with
      | ((PTypeConstraint (_, PVar (m, name), _)) as p), 
         ELambda(_, pat, expression) ->
          let q, exp = chop_args pat expression in
            p :: q, exp
          
      | (PVar (m, name) as p, ELambda(_, pat, expression)) ->
          let q, exp = chop_args pat expression in
            p :: q, exp
      | (pat, expression) -> [pat], expression
  in
  let print (pats, expression) = (
    pp_open_box !ppf 0;
    if tnames <> [] then (
      pp_print_string !ppf "forall ";
      print_separated_list " " (fun (TName s) -> pp_print_string !ppf s) tnames;
      pp_print_string !ppf ".";
      pp_print_cut !ppf ()
    );
    print_separated_list " " print_pattern pats;
    pp_print_string !ppf " = ";
    pp_close_box !ppf ();
    pp_print_cut !ppf (); 
    print_expression expression;
  )
  in
    print (chop_args pat expression)

and print_pattern p = 
  (match p with
     | PPrimitive _ -> assert false
     | PVar (_, SName name) -> pp_print_string !ppf name
     | PWildcard _ -> pp_print_string !ppf "_"
     | PAlias (_, name, pattern) -> 
         pp_print_string !ppf "("; 
         print_pattern pattern; 
         pp_print_string !ppf " as ";
         pp_print_string !ppf ")"
     | PTypeConstraint (_, pat, ty) -> 
         pp_print_string !ppf "(";
         print_pattern pat;
         pp_print_string !ppf " : ";
         print_type ty;
         pp_print_string !ppf ")"
     | PData (_, DName "_Unit", ps) -> 
         pp_print_string !ppf "()"
     | PData (_, DName "_Tuple", ps) -> 
         if ps <> [] then (
           pp_print_string !ppf "(";
           print_separated_list "," print_pattern ps;
           pp_print_string !ppf ")")
     | PData (_, DName k, ps) -> 
         pp_print_string !ppf "(";
         pp_print_string !ppf k;
         pp_print_string !ppf " ";
         if ps <> [] then print_separated_list " " print_pattern ps;
         pp_print_string !ppf ")"
     | POr (_, [ x ]) | PAnd (_, [ x ]) ->
         print_pattern x
     | PAnd (_, ps) ->
         pp_print_string !ppf "(";
         print_separated_list "&" print_pattern ps;
         pp_print_string !ppf ")";
     | POr (_, ps) ->
         pp_print_string !ppf "(";
         print_separated_list "|" print_pattern ps;
         pp_print_string !ppf ")");

and print_type ?paren = function
  | TypVar (_, TName name) ->
      pp_print_string !ppf name
  | TypApp (_, TypVar(_, TName "->"), [t; t']) ->
      if paren <> None then 
        pp_print_string !ppf "(";
      print_type ~paren:true t;
      pp_print_string !ppf " -> ";
      print_type t';
      if paren <> None then 
        pp_print_string !ppf ")"
  | TypApp (_, TypVar(_, TName "*"), [a; b]) ->
      print_type ~paren:true a;
      pp_print_string !ppf " * ";
      print_type ~paren:true b
  | TypApp (_, t, []) ->
      print_type t
  | TypApp (_, t, ts) -> 
      pp_print_string !ppf "(";
      print_type t; 
      pp_print_string !ppf " ";
      print_separated_list " " print_type ts;
      pp_print_string !ppf ")";
  | TypRowCons (_, ls, ty) -> 
      pp_print_string !ppf "{";
      let print_label (LName l, ty) =
        pp_print_string !ppf l;
        pp_print_string !ppf " : ";
        print_type ty
      in
        print_separated_list "; " print_label ls;
        pp_print_string !ppf "; ";
        print_type ty;
        pp_print_string !ppf "}"
  | TypRowUniform (_, ty) -> 
      pp_print_string !ppf "\\";
      print_type ty

and print_kind = function
    KStar -> pp_print_string !ppf "*"
  | KArrow (KStar, k2) -> pp_print_string !ppf "* ->";
      print_kind k2
  | KArrow (k1, k2) -> 
      pp_print_string !ppf "(";
      print_kind k1;
      pp_print_string !ppf ") -> ";
      print_kind k2
  | _ -> assert false

and print_type_declaration (_, kind, TName n, typ) = 
  pp_open_box !ppf 0;
  pp_print_string !ppf n;
  pp_print_string !ppf ":";
  print_kind kind;
  pp_print_string !ppf " = ";      
  pp_close_box !ppf ();
  pp_print_cut !ppf ();
  pp_open_box !ppf 0;
  print_type_definition typ;
  pp_print_string !ppf " ";
  pp_close_box !ppf ()

and print_type_definition = function
  | DAlgebraic ds -> 
      let first = ref true in
      let print_datatype_def (_, DName k, betas, ty) = 
        if !first then (
          first := false) 
        else (pp_print_cut !ppf (); pp_print_string !ppf "| ");
        pp_print_string !ppf k;
        pp_print_string !ppf " : ";
        if betas <> [] then begin 
          pp_print_string !ppf "forall ";
          print_separated_list " " (fun (TName s) -> pp_print_string !ppf s) 
            betas;
          pp_print_string !ppf "."
        end;
        print_type ty
      in
        print_separated_list "" print_datatype_def ds;

and print_clause (_, pat, expression) =
  print_pattern pat;
  pp_print_string !ppf " => ";
  print_expression expression;
  pp_print_cut !ppf ()