Cook.ml

open Error

(* The source calculus. *)
module S = RawLambda
(* The target calculus. *)
module T = Lambda
(* Alias some modules defined in [Lambda] for quicker access. *)
module TyC = T.TyC
module TyS = T.TyS
module TyE = T.TyE
module TyCSet = T.TyCSet
module TySSet = T.TySSet
module TyESet = T.TyESet
module TySPSet = T.TySPSet

let disable_type_checking = ref false

let builtin_int_id = Atom.fresh "int"
let builtin_io_id = Atom.fresh "io"

type scheme = {
  (* First place where the variable was used, for error reporting. *)
  hypotheses : (TyS.t * place) Atom.Map.t ;
  typ : TyS.t ;
  eff : TyE.t ;
}

type binding =
  | BScheme of scheme
  | BInfer

type inst = (TyS.t Atom.Map.t * TyE.t Atom.Map.t) -> TyS.t

type typedef =
  | TBaseType of Atom.atom
  | TTypeSynonym of inst * inst (* positive, negative *)

type tavar =
  | ANone
  | APos of Atom.atom
  | ANeg of Atom.atom
  | APosNeg of Atom.atom * Atom.atom

module Smap = Map.Make(String)
type env = {
  bindings : (binding * Atom.atom) Smap.t ;
  type_bindings : Atom.atom Smap.t ;
  type_variables : (Atom.atom * Atom.atom) Smap.t ;
  type_variance : (tavar * bool) list Atom.Map.t ;
  type_defs : typedef Atom.Map.t ;
  constructor_bindings : Atom.atom Smap.t ;
  constructor_defs :
    (Atom.atom * (inst * inst) list * int * bool) Atom.Map.t ;
  effect_bindings : Atom.atom Smap.t;
  effect_defs : ((inst * inst) option * (inst * inst) * int) Atom.Map.t ;
  free_effect_tag : int ;
}

let base_env = {
  bindings = Smap.empty ;
  type_bindings = Smap.singleton "int" builtin_int_id ;
  type_variables = Smap.empty ;
  type_variance = Atom.Map.singleton builtin_int_id [] ;
  type_defs = Atom.Map.singleton builtin_int_id (TBaseType builtin_int_id) ;
  constructor_bindings = Smap.empty ;
  constructor_defs = Atom.Map.empty ;
  effect_bindings = Smap.singleton "io" builtin_io_id ;
  effect_defs = Atom.Map.empty ;
  free_effect_tag = 0 ;
}

let rec do_instanciate env polarity t vs vas =
  assert (List.length vas = List.length vs);
  let add_to_map create build am v va =
    match va with
    | ANone -> assert (v = TyC.VNone); am
    | APos xp ->
      let qp = match v with
        | TyC.VNone -> create polarity
        | TyC.VPos qps -> build polarity qps
        | _ -> assert false
      in
      Atom.Map.add xp qp am
    | ANeg xn ->
      let qn = match v with
        | TyC.VNone -> create (not polarity)
        | TyC.VNeg qns -> build (not polarity) qns
        | _ -> assert false
      in
      Atom.Map.add xn qn am
    | APosNeg (xp, xn) ->
      assert (not (Atom.equal xp xn));
      let qp, qn = match v with
        | TyC.VNone -> create polarity, create (not polarity)
        | TyC.VPos qps -> build polarity qps, create (not polarity)
        | TyC.VNeg qns -> create polarity, build (not polarity) qns
        | TyC.VPosNeg (qps, qns) ->
          build polarity qps, build (not polarity) qns
      in
      Atom.Map.add xn qn (Atom.Map.add xp qp am)
  in
  let ve, vt = List.partition (fun (v, (_, b)) ->
      match v with
      | TyC.AEff _ -> assert b; b
      | TyC.AType _ -> assert (not b); b
  ) (List.combine vs vas) in
  let vts, vtas = List.split
      (List.map (fun (v, (va, _)) ->
           match v with TyC.AType v -> (v, va) | _ -> assert false) vt) in
  let ves, veas = List.split
      (List.map (fun (v, (va, _)) ->
           match v with TyC.AEff v -> (v, va) | _ -> assert false) ve) in
  let amt = List.fold_left2 (add_to_map TyS.create (merge_all env)) Atom.Map.empty vts vtas in
  let ame = List.fold_left2 (add_to_map TyE.create (fun _ x -> x)) Atom.Map.empty ves veas in
  t (amt, ame)

and resolve env polarity t =
  match t with
  | TyC.Tident (vs, n) ->
    (match Atom.Map.find n env.type_defs with
     | TTypeSynonym (typ, tyn) ->
       let vas = Atom.Map.find n env.type_variance in
       let q = do_instanciate env polarity
           (if polarity then typ else tyn) vs vas in
       resolve_all env polarity q.TyS.constructors
     | TBaseType _ -> TyCSet.singleton polarity t)
  | t -> TyCSet.singleton polarity t

and resolve_all env polarity ts =
  TyCSet.map_flatten (resolve env) polarity ts

and maybe_resolve env polarity1 polarity2 tc1 tc2 =
  if TyCSet.need_resolve polarity1 polarity2 tc1 tc2 then
    resolve_all env polarity1 tc1, resolve_all env polarity2 tc2
  else
    tc1, tc2

and cmerge env polarity tc1 tc2 =
  let tc1, tc2 = maybe_resolve env polarity polarity tc1 tc2 in
  TyCSet.merge polarity tc1 tc2

and scheme_merge env q1 q2 =
  let open TyS in
  assert (q1.polarity = q2.polarity);
  let qs = TySSet.diff q2.flow q1.flow in
  TySSet.iter (add_flow_edge q1) qs;
  q1.constructors <- cmerge env q1.polarity q1.constructors q2.constructors

and merge_all env polarity qs =
  let q = TyS.create polarity in
  TySSet.iter (scheme_merge env q) qs;
  q

module PTySSetMap = Map.Make(struct
    type t = bool * TySSet.t
    let compare (p1, qs1) (p2, qs2) =
      let u = compare p1 p2 in
      if u = 0 then
        TySSet.compare qs1 qs2
      else
        u
  end)

let rec simpl_tyss env st polarity qs =
  try PTySSetMap.find (polarity, qs) !st
  with Not_found ->
    let q = merge_all env polarity qs in
    let r = TyS.create polarity in
    st := PTySSetMap.add (polarity, qs) r !st;
    simpl_tys_in env st polarity q r;
    r

and simpl_tys env st polarity q =
  let q2 = TyS.create polarity in
  simpl_tys_in env st polarity q q2;
  q2

and simpl_tys_in env st polarity q q2 =
  TySSet.iter (TyS.add_flow_edge q2) q.TyS.flow;
  q2.TyS.constructors <- List.map (simpl_tyc env st polarity) q.TyS.constructors

and simpl_tyc env st polarity c =
  let open TyC in
  match c with
  | Tarrow (qs1, e, qs2) ->
    Tarrow (TySSet.singleton (simpl_tyss env st (not polarity) qs1),
            e,
            TySSet.singleton (simpl_tyss env st polarity qs2))
  | Tproduct qsl ->
    Tproduct (List.map (fun qs ->
        TySSet.singleton (simpl_tyss env st polarity qs)) qsl)
  | Tident (vs, n) -> Tident (List.map (simpl_arg env st polarity) vs, n)

and simpl_var env st polarity v =
  let open TyC in
  match v with
  | VNone -> VNone
  | VPos qs -> VPos (TySSet.singleton (simpl_tyss env st polarity qs))
  | VNeg qs -> VNeg (TySSet.singleton (simpl_tyss env st (not polarity) qs))
  | VPosNeg (qps, qns) ->
    VPosNeg (TySSet.singleton (simpl_tyss env st polarity qps),
             TySSet.singleton (simpl_tyss env st (not polarity) qns))

and simpl_arg env st polarity a =
  let open TyC in
  match a with
  | AEff v -> AEff v
  | AType v -> AType (simpl_var env st polarity v)

let print_scheme env ff { hypotheses ; typ ; eff } =
  let st = ref PTySSetMap.empty in
  let typ = simpl_tys env st true typ in
  let hypotheses = Atom.Map.map
      (fun (q, _) -> simpl_tys env st false q) hypotheses in
  let l = typ :: (List.map snd (Atom.Map.bindings hypotheses)) in
  let st = T.prepare_printing l [eff] in
  if not (Atom.Map.is_empty hypotheses) then begin
    Format.fprintf ff "[@[<hov 2>";
    List.iteri (fun i (a, ty) ->
        if i > 0 then Format.fprintf ff ",@ ";
        Format.fprintf ff "%s : %a" (Atom.hint a) (T.print_tys st 0) ty
    ) (Atom.Map.bindings hypotheses);
    Format.fprintf ff "@]] "
  end;
  Format.fprintf ff "%a" (T.print_tys st 0) typ;
  Format.fprintf ff " !{%a}" (T.print_eff st 0 true) eff

let unify_hyp env hp1 hp2 =
  Atom.Map.merge (fun _ ty1 ty2 ->
      match ty1, ty2 with
      | None, None -> None
      | None, Some ty | Some ty, None -> Some ty
      | Some (ty1, place1), Some (ty2, _) ->
        let open TyS in
        let w = create false in
        TySSet.iter (add_flow_edge w) (TySSet.union ty1.flow ty2.flow);
        w.constructors <- cmerge env false ty1.constructors ty2.constructors;
        Some (w, place1)
  ) hp1 hp2

exception BiUnificationFailure of TyC.t * TyC.t
exception EffBiUnificationFailure of TyE.t * TyE.t

let biunification_error t1 t2 =
  raise (BiUnificationFailure (t1, t2))

let eff_biunification_error e1 e2 =
  raise (EffBiUnificationFailure (e1, e2))

let biunify_vs bu env t vp vm =
  let open TyC in
  match vp, vm with
  | VNone, _ | _, VNone | VPos _, VNeg _ | VNeg _, VPos _ -> ()
  | VPos qp, VPos qm | VPos qp, VPosNeg (qm, _) | VPosNeg (qp, _), VPos qm ->
    bu env t qp qm
  | VNeg qp, VNeg qm | VNeg qp, VPosNeg (_, qm) | VPosNeg (_, qp), VNeg qm ->
    bu env t qm qp
  | VPosNeg (qp1, qp2), VPosNeg (qm1, qm2) ->
    bu env t qp1 qm1;
    bu env t qm2 qp2

let rec biunify_tys env t qp qm =
  if not (TySPSet.mem (qp, qm) !t) then begin
    t := TySPSet.add (qp, qm) !t;
    assert (qp.TyS.polarity && not qm.TyS.polarity);
    TySSet.iter (fun q -> scheme_merge env q qp) qm.TyS.flow;
    TySSet.iter (fun q -> scheme_merge env q qm) qp.TyS.flow;
    let qmc, qpc = maybe_resolve env false true
        qm.TyS.constructors qp.TyS.constructors in
    List.iter (fun tp ->
      List.iter (fun tm ->
        biunify_tyc env t tp tm
      ) qmc;
    ) qpc;
  end

and biunify_tyss env t qps qms =
  TySSet.iter (fun qp ->
    TySSet.iter (fun qm ->
      biunify_tys env t qp qm
    ) qms
  ) qps

and merge_eff _ name e1 e2 =
  let open TyE in
  assert (e1.polarity = e2.polarity);
  (match name with
   | None -> () | Some name -> extend name e1; extend name e2);
  let get e =
    match name with
    | None -> snd e.flows
    | Some name -> Atom.Map.find name (fst e.flows)
  in
  let es1, b1 = get e1 in
  let es2, b2 = get e2 in
  let es = TyESet.diff es2 es1 in
  TyESet.iter (add_flow_edge name e1) es;
  match name with
  | None ->
    if e1.polarity then
      assert (not b1 && not b2)
    else
      e1.flows <- (fst e1.flows, (fst (snd e1.flows), b1 || b2))
  | Some name -> e1.flows <- (Atom.Map.add name (fst (get e1), b1 || b2) (fst e1.flows), snd e1.flows)

and biunify_eff_excl ex env _ ep em =
  TyE.common_domain ep em;
  assert (ep.TyE.polarity && not em.TyE.polarity);
  let (epf, epd) = ep.TyE.flows in
  let (emf, emd) = em.TyE.flows in
  Atom.Map.iter (fun name (es, _) -> if not (Atom.Set.mem name ex) then TyESet.iter (fun e -> merge_eff env (Some name) e ep) es) emf;
  Atom.Map.iter (fun name (es, _) -> if not (Atom.Set.mem name ex) then TyESet.iter (fun e -> merge_eff env (Some name) e em) es) epf;
  TyESet.iter (fun e -> merge_eff env None e ep) (fst emd);
  TyESet.iter (fun e -> merge_eff env None e em) (fst epd);
  assert (not (snd epd));
  Atom.Map.iter (fun name (_, bp) ->
      let (_, bm) = Atom.Map.find name emf in
      if bm && bp then
        eff_biunification_error ep em
    ) epf

and biunify_eff env = biunify_eff_excl Atom.Set.empty env

and biunify_tyc env t tp tm =
  let open TyC in
  match tp, tm with
  | Tident (vs1, n1), Tident (vs2, n2) ->
    if not (Atom.equal n1 n2) then
      biunification_error tp tm;
    assert (List.length vs1 = List.length vs2);
    List.iter2 (biunify_args env t) vs1 vs2
  | Tarrow (tpa, effp, tpb), Tarrow (tma, effm, tmb) ->
    biunify_tyss env t tma tpa;
    biunify_tyss env t tpb tmb;
    biunify_eff env t effp effm
  | Tproduct l1, Tproduct l2 ->
    if List.length l1 = List.length l2 then
      List.iter2 (biunify_tyss env t) l1 l2
    else
      biunification_error tp tm
  | _, _ -> biunification_error tp tm

and biunify_args env t ap am =
  let open TyC in
  match ap, am with
  | AType vp, AType vm -> biunify_vs biunify_tyss env t vp vm
  | AEff vp, AEff vm -> biunify_vs biunify_eff env t vp vm
  | _ -> assert false

let biunify_eff_excl excl env = biunify_eff_excl excl env (ref TySPSet.empty)
let biunify env = biunify_tys env (ref TySPSet.empty)

let not_subtype_msg : _ format6 =
  "The type %a is not a subtype of the type %a@."
let not_subeffect_msg : _ format6 =
  "The effect %a is not a compatible with the effect %a@."

let check_biunify_msg msg place env t1 t2 =
  if not !disable_type_checking then
    try biunify env t1 t2 with
    | BiUnificationFailure (ty1, ty2) ->
      let st = T.prepare_printing
          ([t1; t2] @
           TySSet.(elements (union (T.tyc_succ ty1) (T.tyc_succ ty2)))) []
      in
      error place (msg ^^ "@.%t")
        (T.print_tys st 0) t1 (T.print_tys st 0) t2
        (fun ff -> Format.fprintf ff not_subtype_msg (T.print_tyc st 0 true) ty1 (T.print_tyc st 0 false) ty2)
    | EffBiUnificationFailure (e1, e2) ->
      let st = T.prepare_printing [t1; t2] [e1; e2] in
      error place (msg ^^ "@.%t")
        (T.print_tys st 0) t1 (T.print_tys st 0) t2
        (fun ff -> Format.fprintf ff not_subeffect_msg (T.print_eff st 0 true) e1 (T.print_eff st 0 false) e2)

let check_biunify =
  check_biunify_msg "This expression has type %a but was expected of type %a@."

let check_biunify_eff_excl_msg msg excl place env t1 t2 =
  if not !disable_type_checking then
    try biunify_eff_excl excl env t1 t2 with
    | EffBiUnificationFailure (e1, e2) ->
      let st = T.prepare_printing [] [t1; t2; e1; e2] in
      error place (msg ^^ "@.%t")
        (T.print_eff st 0 true) t1 (T.print_eff st 0 false) t2
        (fun ff -> Format.fprintf ff not_subeffect_msg (T.print_eff st 0 true) e1 (T.print_eff st 0 false) e2)

let check_biunify_eff_excl =
  check_biunify_eff_excl_msg "This expression has effect %a but was expected to have effect %a"

let check_biunify_eff = check_biunify_eff_excl Atom.Set.empty

let add_bound id a env =
  { env with bindings = Smap.add id (BInfer, a) env.bindings }

let add id env =
  let a = Atom.fresh id in
  add_bound id a env, a

let empty_eff polarity =
  let w = TyE.create polarity in
  w.TyE.flows <- (Atom.Map.empty, (TyESet.empty, not polarity));
  w

let add_gen id scheme env =
  let a = Atom.fresh id in
  let scheme = { scheme with eff = empty_eff true } in
  let nenv = { env with bindings = Smap.add id (BScheme scheme, a) env.bindings } in
  (nenv, a)

let copy_scheme { hypotheses ; typ ; eff } =
  let l = typ :: (List.map (fun (_, (st, _)) -> st)
                           (Atom.Map.bindings hypotheses)) in
  let st = T.prepare_copy l [eff] in
  {
    hypotheses = Atom.Map.map
        (fun (ty, place) -> (T.copy st ty, place)) hypotheses ;
    typ = T.copy st typ ;
    eff = T.eff_copy st eff ;
  }

let find place id env =
  let (sc, a) = Smap.find id env.bindings in
  match sc with
  | BScheme sc -> copy_scheme sc, a
  | BInfer ->
    let typ, tyn = TyS.create_flow_pair () in
    let sc = {
      hypotheses = Atom.Map.singleton a (tyn, place) ;
      typ = typ ;
      eff = empty_eff true ;
    } in
    sc, a

let unify_hyp_many env l =
  List.fold_left (unify_hyp env) Atom.Map.empty l

let create_var_pair mk build = function
  | ANone -> TyC.VNone, TyC.VNone
  | APos _ ->
    let qp, qn = mk () in
    TyC.VPos (build qp), TyC.VPos (build qn)
  | ANeg _ ->
    let qp, qn = mk () in
    TyC.VNeg (build qn), TyC.VNeg (build qp)
  | APosNeg _ ->
    let qp1, qn1 = mk () in
    let qp2, qn2 = mk () in
    TyC.VPosNeg (build qp1, build qn2),
    TyC.VPosNeg (build qn1, build qp2)

let create_arg_pair (v, is_effect) =
  if is_effect then
    let a, b = create_var_pair TyE.create_flow_pair (fun x -> x) v in
    TyC.AEff a, TyC.AEff b
  else
    let a, b = create_var_pair TyS.create_flow_pair TySSet.singleton v in
    TyC.AType a, TyC.AType b

let create_var_pairs l =
  List.split (List.map create_arg_pair l)

let rec is_irrefutable { S.value ; _ } =
  match value with
  | S.PVar _ -> true
  | S.PTuple l -> List.for_all is_irrefutable l
  | S.POr (p1, p2) -> is_irrefutable p1 || is_irrefutable p2
  | S.PConstructor _ -> false

let rec cook_term env { S.place ; S.value } =
  match value with
  | S.Var x -> begin
    match find place x env with
    | sc, a -> sc, T.Var a
    | exception Not_found -> error place "Unbound variable: %s" x
    end
  | S.Lam (x, t) ->
    let nenv, x = add x env in
    let sc, t = cook_term nenv t in
    let nh, src =
      try
        let ty, _ = Atom.Map.find x sc.hypotheses in
        Atom.Map.remove x sc.hypotheses, Some ty
      with Not_found ->
        sc.hypotheses, None
    in
    let w = T.arrow_option true src sc.eff sc.typ in
    let nsc = {
      hypotheses = nh ;
      typ = w ;
      eff = empty_eff true ;
    } in
    nsc, T.Lam (T.NoSelf, x, t)
  | S.App (t1, t2) ->
    let sc1, nt1 = cook_term env t1 in
    let sc2, nt2 = cook_term env t2 in
    let (wp, wn) = TyS.create_flow_pair () in
    let (ep, en) = TyE.create_flow_pair () in
    let w = T.arrow false sc2.typ en wn in
    let nh = unify_hyp env sc1.hypotheses sc2.hypotheses in
    check_biunify t1.S.place env sc1.typ w;
    check_biunify_eff t1.S.place env sc1.eff en;
    check_biunify_eff t2.S.place env sc2.eff en;
    let nsc = {
      hypotheses = nh ;
      typ = wp ;
      eff = ep ;
    } in
    nsc, T.App (nt1, nt2)
  | S.Lit i ->
    let w = T.ident true builtin_int_id [] in
    let sc = {
      hypotheses = Atom.Map.empty ;
      typ = w ;
      eff = empty_eff true ;
    } in
    sc, T.Lit i
  | S.BinOp (t1, op, t2) ->
    let sc1, nt1 = cook_term env t1 in
    let sc2, nt2 = cook_term env t2 in
    let nh = unify_hyp env sc1.hypotheses sc2.hypotheses in
    let w1 = T.ident true builtin_int_id [] in
    let w2 = T.ident false builtin_int_id [] in
    let (ep, en) = TyE.create_flow_pair () in
    check_biunify t1.S.place env sc1.typ w2;
    check_biunify t2.S.place env sc2.typ w2;
    check_biunify_eff t1.S.place env sc1.eff en;
    check_biunify_eff t2.S.place env sc2.eff en;
    let sc = {
      hypotheses = nh ;
      typ = w1 ;
      eff = ep ;
    } in
    sc, T.BinOp (nt1, op, nt2)
  | S.Print t ->
    let sc, nt = cook_term env t in
    let w1 = T.ident true builtin_int_id [] in
    let w2 = T.ident false builtin_int_id [] in
    let (ep, en) = TyE.create_flow_pair () in
    let e = TyE.create true in
    e.TyE.flows <- (Atom.Map.singleton builtin_io_id (TyESet.empty, true), (TyESet.empty, false));
    check_biunify t.S.place env sc.typ w2;
    check_biunify_eff t.S.place env sc.eff en;
    check_biunify_eff t.S.place env e en;
    { sc with eff = ep ; typ = w1 }, T.Print nt
  | S.Let (recursive, x, t1, t2) ->
    let nenv, x, sc1, nt1 = cook_let env recursive x t1 in
    let sc2, nt2 = cook_term nenv t2 in
    let (ep, en) = TyE.create_flow_pair () in
    check_biunify_eff t1.S.place env sc1.eff en;
    check_biunify_eff t2.S.place env sc2.eff en;
    let nh = unify_hyp env sc1.hypotheses sc2.hypotheses in
    let nsc = {
      hypotheses = nh ;
      typ = sc2.typ ;
      eff = ep ;
    } in
    nsc, T.Let (x, nt1, nt2)
  | S.IfZero (t1, t2, t3) ->
    let sc1, nt1 = cook_term env t1 in
    let sc2, nt2 = cook_term env t2 in
    let sc3, nt3 = cook_term env t3 in
    let nh = unify_hyp env sc1.hypotheses
        (unify_hyp env sc2.hypotheses sc3.hypotheses) in
    let (wp, wn) = TyS.create_flow_pair () in
    let (ep, en) = TyE.create_flow_pair () in
    let w = T.ident false builtin_int_id [] in
    check_biunify t1.S.place env sc1.typ w;
    check_biunify t2.S.place env sc2.typ wn;
    check_biunify t3.S.place env sc3.typ wn;
    check_biunify_eff t1.S.place env sc1.eff en;
    check_biunify_eff t2.S.place env sc2.eff en;
    check_biunify_eff t3.S.place env sc3.eff en;
    let nsc = {
      hypotheses = nh ;
      typ = wp ;
      eff = ep ;
    } in
    nsc, T.IfZero (nt1, nt2, nt3)
  | S.Tuple l ->
    let l = List.map (cook_term env) l in
    let nh = unify_hyp_many env (List.map (fun (sc, _) -> sc.hypotheses) l) in
    let w = T.product true (List.map (fun (sc, _) -> sc.typ) l) in
    let (ep, en) = TyE.create_flow_pair () in
    List.iter (fun (sc, _) -> check_biunify_eff place env sc.eff en) l;
    let nsc = {
      hypotheses = nh ;
      typ = w ;
      eff = ep ;
    } in
    nsc, (T.Tuple (List.map snd l))
  | S.Constructor (x, t) ->
    let catom =
      try Smap.find x env.constructor_bindings
      with Not_found -> error place "Unbound constructor: %s" x
    in
    let tname, cargs, ctag, is_effect = Atom.Map.find catom env.constructor_defs in
    let targs =
      if is_effect then
        []
      else
        Atom.Map.find tname env.type_variance
    in
    let tap, tan = create_var_pairs targs in
    let n = List.length cargs in
    let args =
      match n, t with
      | 0, None -> []
      | 1, Some t -> [t]
      | 2, Some { S.value = (S.Tuple l) ; _ } -> l
      | _ ->
        let m = match t with
          | None -> 0
          | Some { S.value = (S.Tuple l) ; _} -> List.length l
          | Some _ -> 1
        in
        error place "The constructor %s expects %d argument(s), but is applied here to %d argument(s)" x n m
    in
    let args = List.map (fun t -> t.S.place, cook_term env t) args in
    let (ep, en) = TyE.create_flow_pair () in
    let nh = unify_hyp_many env
        (List.map (fun (_, (sc, _)) -> sc.hypotheses) args) in
    List.iter2 (fun (place, (sc, _)) (_, enty) ->
        check_biunify place env sc.typ (do_instanciate env false enty tan targs);
        check_biunify_eff place env sc.eff en;
    ) args cargs;
    let nt =
      if is_effect then begin
        let (_, (npt, _), _) = Atom.Map.find tname env.effect_defs in
        let e = TyE.create true in
        e.TyE.flows <- (Atom.Map.singleton tname (TyESet.empty, true), (TyESet.empty, false));
        check_biunify_eff place env e en;
        do_instanciate env true npt tap targs
      end else
        T.ident true tname tap
    in
    let nsc = {
      hypotheses = nh ;
      typ = nt ;
      eff = ep ;
    } in
    nsc, T.Constructor ((catom, ctag, is_effect),
                        List.map (fun (_, (_, t)) -> t) args)
  | S.Match (t, l) ->
    let sc, nt = cook_term env t in
    let rtyp, rtyn = TyS.create_flow_pair () in
    let ep, en = TyE.create_flow_pair () in
    let erp, ern = TyE.create_flow_pair () in
    check_biunify_eff t.S.place env sc.eff en;
    let matched_effects = ref Atom.Set.empty in
    let nl = List.map (fun (p, t1) ->
      let np, dv, ef = cook_pattern_or_effect env sc.typ rtyp erp p in
      matched_effects := Atom.Set.union !matched_effects ef;
      let nenv = Smap.fold (fun x (a, _) env -> add_bound x a env) dv env in
      let sc1, nt1 = cook_term nenv t1 in
      check_biunify t1.S.place env sc1.typ rtyn;
      check_biunify_eff t1.S.place env sc1.eff ern;
      let nh = Smap.fold (fun _ (a, t) h ->
          try
            let ty, place = Atom.Map.find a h in
            check_biunify place env t ty;
            Atom.Map.remove a h
          with Not_found -> h
      ) dv sc1.hypotheses in
      (nh, (np, nt1))
    ) l in
    Atom.Set.iter (fun name -> TyE.extend name ep) !matched_effects;
    Atom.Set.iter (fun name -> TyE.extend name ern) !matched_effects;
    check_biunify_eff_excl !matched_effects place env ep ern;
    let nsc = {
      hypotheses = List.fold_left
          (fun h1 (h2, _) -> unify_hyp env h1 h2) sc.hypotheses nl ;
      typ = rtyp ;
      eff = erp ;
    } in
    nsc, T.Match (nt, List.map snd nl)

and cook_pattern_or_effect env ty rty ep = function
  | S.Pattern p ->
    let p, dv = cook_pattern env Smap.empty ty p in
    T.Pattern p, dv, Atom.Set.empty
  | S.Effect ({ S.value = c ; S.place }, p, k) ->
    let catom =
      try Smap.find c env.constructor_bindings
      with Not_found -> error place "Unbound constructor: %s" c
    in
    let ename, _, ctag, is_effect = Atom.Map.find catom env.constructor_defs in
    let ty1, (_, ty2n), _ = Atom.Map.find ename env.effect_defs in
    if not is_effect then
      error place "This constructor is a value constructor, not an effect constructor";
    let np, dv =
      match p, ty1 with
      | None, None -> T.PConstructor ((catom, ctag, true), []), Smap.empty
      | Some p, Some (ty1p, _) ->
        let np, dv = cook_pattern env Smap.empty (do_instanciate env true ty1p [] []) p in
        if Smap.mem k dv then
          error p.S.place "The variable %s is already bound in this matching" k;
        T.PConstructor ((catom, ctag, true), [np]), dv
      | None, Some _ ->
        error place "The effect constructor %s expects 1 argument, but is applied here to 0 arguments" c
      | Some _, None ->
        error place "The effect constructor %s expects 0 arguments, but is applied here to 1 argument" c
    in
    let kty = T.arrow true (do_instanciate env false ty2n [] []) ep rty in
    (* Conservative exhaustivity checking: assume the effect is matched only if the pattern is irrefutable *)
    let matched_effects =
      if match p with None -> true | Some p -> is_irrefutable p then
        Atom.Set.singleton ename
      else
        Atom.Set.empty
    in
    let kv = Atom.fresh k in
      T.Effect (np, kv), (Smap.add k (kv, kty) dv), matched_effects

and cook_pattern env mapped_vars ty { S.value ; S.place } =
  match value with
  | S.PVar x ->
    let a = try Smap.find x mapped_vars with Not_found -> Atom.fresh x in
    T.PVar a, Smap.singleton x (a, ty)
  | S.POr (p1, p2) ->
    let np1, dv1 = cook_pattern env mapped_vars ty p1 in
    let mv = Smap.fold (fun x (a, _) mv -> Smap.add x a mv) dv1 mapped_vars in
    let np2, dv2 = cook_pattern env mv ty p2 in
    let np = T.POr (np1, np2) in
    let dv = Smap.merge (fun x def1 def2 ->
      match def1, def2 with
      | None, None -> None
      | Some (a1, ty1), Some (a2, ty2) ->
        assert (Atom.equal a1 a2);
        let wp, wn = TyS.create_flow_pair () in
        check_biunify place env ty1 wn;
        check_biunify place env ty2 wn;
        Some (a1, wp)
      | _ -> error place "Variable %s must appear on both sides of this | pattern" x
    ) dv1 dv2 in
    np, dv
  | S.PTuple l ->
    let ws = List.map (fun _ -> TyS.create_flow_pair ()) l in
    check_biunify_msg "A pattern was expected which matches values of type %a but this pattern matches values of type %a" place env ty (T.product false (List.map snd ws));
    let nl = List.map2 (cook_pattern env mapped_vars) (List.map fst ws) l in
    let np = T.PTuple (List.map fst nl) in
    let dv = List.fold_left (fun dv (_, dvi) ->
      Smap.merge (fun x def1 def2 ->
        match def1, def2 with
        | None, None -> None
        | Some (a, ty), None | None, Some (a, ty) -> Some (a, ty)
        | Some _, Some _ ->
          error place "The variable %s is bound several times in this matching" x
      ) dv dvi
    ) Smap.empty nl in
    np, dv
  | S.PConstructor (x, p) ->
    let catom =
      try Smap.find x env.constructor_bindings
      with Not_found -> error place "Unbound constructor: %s" x
    in
    let tname, cargs, ctag, is_effect = Atom.Map.find catom env.constructor_defs in
    if is_effect then
      error place "This constructor is an effect constructor, not a value constructor";
    let targs = Atom.Map.find tname env.type_variance in
    let tap, tan = create_var_pairs targs in
    check_biunify_msg "A pattern was expected which matches values of type %a but this pattern matches values of type %a" place env ty (T.ident false tname tan);
    let n = List.length cargs in
    let args =
      match n, p with
      | 0, None -> []
      | 1, Some p -> [p]
      | 2, Some { S.value = (S.PTuple l) ; _ } -> l
      | _ ->
        let m = match p with
          | None -> 0
          | Some { S.value = (S.PTuple l) ; _} -> List.length l
          | Some _ -> 1
        in
        error place "The constructor %s expects %d argument(s), but is applied here to %d argument(s)" x n m
    in
    let nl = List.map2 (cook_pattern env mapped_vars)
        (List.map (fun (ap, _) -> do_instanciate env true ap tap targs) cargs)
        args
    in
    let np = T.PConstructor ((catom, ctag, false), List.map fst nl) in
    let dv = List.fold_left (fun dv (_, dvi) ->
      Smap.merge (fun x def1 def2 ->
        match def1, def2 with
        | None, None -> None
        | Some (a, ty), None | None, Some (a, ty) -> Some (a, ty)
        | Some _, Some _ ->
          error place "The variable %s is bound several times in this matching" x
      ) dv dvi
    ) Smap.empty nl in
    np, dv

and cook_let env recursive x t =
  match recursive, t with
  | S.NonRecursive, t ->
    let sc, t = cook_term env t in
    let nenv, nx = add_gen x sc env in
    (nenv, nx, copy_scheme sc, t)
  | S.Recursive, { S.value = S.Lam (y, t) ; _ } ->
    let sc, nx, ny, nt =
      let nenv, nx = add x env in
      let nenv, ny = add y nenv in
      let sc, nt = cook_term nenv t in
      let nh, src =
        try
          let ty, _ = Atom.Map.find ny sc.hypotheses in
          Atom.Map.remove ny sc.hypotheses, Some ty
        with Not_found ->
          sc.hypotheses, None
      in
      let w = T.arrow_option true src sc.eff sc.typ in
      let nh =
        try
          let ty, _ = Atom.Map.find nx nh in
          check_biunify t.S.place nenv w ty;
          Atom.Map.remove nx nh
        with Not_found -> nh
      in
      let nsc = {
        hypotheses = nh ;
        typ = w ;
        eff = empty_eff true ;
      } in
      nsc, nx, ny, nt
    in
    let nenv, nx2 = add_gen x sc env in
    (nenv, nx2, sc, T.Lam (T.Self nx, ny, nt))
  | _, { S.place ; _} ->
    error place
      "the right-hand side of 'let rec' must be a lambda-abstraction"

let cook_var cook build polarity va t =
  match va with
  | ANone -> fun _ -> TyC.VNone
  | APos _ ->
    let t = cook polarity t in
    fun inst -> TyC.VPos (build (t inst))
  | ANeg _ ->
    let t = cook (not polarity) t in
    fun inst -> TyC.VNeg (build (t inst))
  | APosNeg _ ->
    let tp = cook polarity t in
    let tn = cook (not polarity) t in
    fun inst -> TyC.VPosNeg (build (tp inst), build (tn inst))

let rec cook_type env polarity { S.place ; S.value } =
  match value with
  | S.TVariable x ->
    let np, nn =
      try
        Smap.find ("'" ^ x) env.type_variables
      with Not_found -> error place "Unbound type variable: '%s" x
    in
    let n = if polarity then np else nn in
    fun (tinst, _) ->
      let q = Atom.Map.find n tinst in
      assert (q.TyS.polarity = polarity);
      q
  | S.TConstructor (l, x) -> begin
    match Smap.find x env.type_bindings with
    | n ->
      let vas = Atom.Map.find n env.type_variance in
      if List.length vas <> List.length l then
        error place "The type constructor %s expects %d arguments but was given %d arguments" x (List.length vas) (List.length l);
      let nl = List.map2 (cook_arg env polarity) vas l in
      fun inst ->
        T.ident polarity n (List.map (fun t -> t inst) nl)
    | exception Not_found -> error place "Unbound type: %s" x
    end
  | S.TArrow (t1, eff, t2) ->
    let t1 = cook_type env (not polarity) t1 in
    let t2 = cook_type env polarity t2 in
    let te = cook_eff env polarity eff in
    fun inst ->
      T.arrow polarity (t1 inst) (te inst) (t2 inst)
  | S.TTuple l ->
    let l = List.map (cook_type env polarity) l in
    fun inst ->
      T.product polarity (List.map (fun t -> t inst) l)

and cook_arg env polarity (va, b) t =
  match t with
  | S.TEff e ->
    if not b then
      error e.S.place "A type is expected here, but this is an effect.";
    let c = cook_var (cook_eff env) (fun x -> x) polarity va e in
    fun inst -> TyC.AEff (c inst)
  | S.TType t ->
    if b then
      error t.S.place "An effect is expected here, but this is a type.";
    let c = cook_var (cook_type env) TySSet.singleton polarity va t in
    fun inst -> TyC.AType (c inst)

and cook_eff env polarity { S.place ; S.value } =
  let rec to_list = function
    | S.EEmpty -> [], None
    | S.EVariable v -> [], Some v
    | S.EEff (i, e) -> let l, v = to_list e in i :: l, v
  in
  let l, v = to_list value in
  let n = match v with
    | None -> None
    | Some x ->
      let np, nn =
        try
          Smap.find ("!" ^ x) env.type_variables
        with Not_found -> error place "Unbound type variable: !%s" x
      in
      Some (if polarity then np else nn)
  in
  let l = List.map (fun x -> Smap.find x env.effect_bindings) l in
  (* TODO: check effect names *)
  fun (_, einst) ->
    let w = TyE.create polarity in
    let em = List.fold_left (fun em e -> Atom.Map.add e (TyESet.empty, polarity) em) Atom.Map.empty l in
    match n with
    | None -> w.TyE.flows <- (em, (TyESet.empty, not polarity)); w
    | Some n ->
      let v = Atom.Map.find n einst in
      let em = Atom.Map.merge (fun _ u1 u2 ->
          match u1, u2 with
          | None, None -> None
          | Some u, _ -> Some u
          | None, Some u -> Some u
      ) em (fst v.TyE.flows) in
      w.TyE.flows <- (em, snd v.TyE.flows);
      Atom.Map.iter (fun name (qs, _) ->
        TyESet.iter (TyE.add_flow_edge (Some name) w) qs;
      ) (fst w.TyE.flows);
      TyESet.iter (TyE.add_flow_edge None w) (fst (snd w.TyE.flows));
      w

let cook_arg_name = function
  | S.TTypeVar x -> "'" ^ x
  | S.TEffectVar x -> "!" ^ x

let rec cook_program env = function
  | { S.value = S.DTerm t ; S.place } :: p ->
    let a = Atom.fresh "_" in
    let sc, nt = cook_term env t in
    assert (Atom.Map.is_empty sc.hypotheses);
    let e = TyE.create false in
    e.TyE.flows <- (Atom.Map.singleton builtin_io_id (TyESet.empty, false),
                (TyESet.empty, true));
    check_biunify_eff place env sc.eff e;
    T.Let (a, nt, cook_program env p)
  | { S.value = S.DLet (recursive, x, t) ; S.place } :: p ->
    let env, nx, sc, nt = cook_let env recursive x t in
    assert (Atom.Map.is_empty sc.hypotheses);
    Format.eprintf "val %s : @[<hv>%a@]@." x (print_scheme env) sc;
    let e = TyE.create false in
    e.TyE.flows <- (Atom.Map.singleton builtin_io_id (TyESet.empty, false),
                (TyESet.empty, true));
    check_biunify_eff place env sc.eff e;
    T.Let (nx, nt, cook_program env p)
  | { S.value = S.DTypeSynonym ((args, x), t) ; _ } :: p ->
    let n = Atom.fresh x in
    let args = List.map cook_arg_name args in
    let vars = List.map (fun x -> (x.[0] = '!', Atom.fresh x, Atom.fresh x)) args in
    let vas = List.map (fun (b, x, y) -> APosNeg (x, y), b) vars in
    let vamp = List.fold_left2 (fun vam x (_, u, v) -> Smap.add x (u, v) vam) env.type_variables args vars in
    let vamn = List.fold_left2 (fun vam x (_, u, v) -> Smap.add x (v, u) vam) env.type_variables args vars in
    let env1p = { env with type_variables = vamp } in
    let env1n = { env with type_variables = vamn } in
    let nenv = { env with
      type_bindings = Smap.add x n env.type_bindings ;
      type_defs = Atom.Map.add n
          (TTypeSynonym (cook_type env1p true t, cook_type env1n false t))
          env.type_defs ;
      type_variance = Atom.Map.add n vas env.type_variance ;
    } in
    cook_program nenv p
  | { S.value = S.DNewType ((args, x), l) ; _ } :: p ->
    let n = Atom.fresh x in
    let args = List.map cook_arg_name args in
    let vars = List.map (fun x -> (x.[0] = '!', Atom.fresh x, Atom.fresh x)) args in
    let vas = List.map (fun (b, x, y) -> APosNeg (x, y), b) vars in
    let vamp = List.fold_left2 (fun vam x (_, u, v) -> Smap.add x (u, v) vam) env.type_variables args vars in
    let vamn = List.fold_left2 (fun vam x (_, u, v) -> Smap.add x (v, u) vam) env.type_variables args vars in
    let env1 = { env with
      type_bindings = Smap.add x n env.type_bindings ;
      type_variance = Atom.Map.add n vas env.type_variance ;
    } in
    let env1p = { env1 with type_variables = vamp } in
    let env1n = { env1 with type_variables = vamn } in
    let constructors = List.map
        (fun { S.value = (name, r) ; _ } ->
           (name, Atom.fresh name,
            List.map (fun t ->
                cook_type env1p true t, cook_type env1n false t) r)
        ) l in
    let env2 = { env1 with
      type_defs = Atom.Map.add n (TBaseType n) env.type_defs ;
      constructor_bindings = List.fold_left
          (fun cbinds (name, atom, _) -> Smap.add name atom cbinds)
          env.constructor_bindings constructors ;
      constructor_defs = snd (List.fold_left
          (fun (i, cdefs) (_, name, types) ->
            (i + 1, Atom.Map.add name (n, types, i, false) cdefs))
          (0, env.constructor_defs) constructors) ;
    } in
    cook_program env2 p
  | { S.value = S.DEffect (x, { S.value = (c, t1, t2) ; _ }) ; _ } :: p ->
    let n = Atom.fresh x in
    let cn = Atom.fresh c in
    let ty1 = match t1 with
      | None -> None
      | Some t1 -> Some (cook_type env true t1, cook_type env false t1)
    in
    let ty2 = (cook_type env true t2, cook_type env false t2) in
    let nenv = { env with
      effect_bindings = Smap.add x n env.effect_bindings ;
      effect_defs = Atom.Map.add n (ty1, ty2, env.free_effect_tag) env.effect_defs ;
      free_effect_tag = env.free_effect_tag + 1 ;
      constructor_bindings = Smap.add c cn env.constructor_bindings ;
      constructor_defs = Atom.Map.add cn (n, (match ty1 with None -> [] | Some ty1 -> [ty1]), env.free_effect_tag, true) env.constructor_defs ;
    } in
    cook_program nenv p
  | [] -> T.Lit 0

let cook_program = cook_program base_env