let trans_form_or_pattern env (ps, ue) pf tt =
  let state = PFS.create () in

  let rec transf_r opsc env f =
    let transf = transf_r opsc in

    match f.pl_desc with
    | PFhole -> begin
      match ps with
      | None    -> tyerror f.pl_loc env PatternNotAllowed
      | Some ps ->
        let x  = EcIdent.create (Printf.sprintf "?%d" (EcUid.unique ())) in
        let ty = UE.fresh ue in
          ps := Mid.add x ty !ps; f_local x ty
    end

    | PFmem _ -> tyerror f.pl_loc env MemNotAllowed

    | PFscope (popsc, f) ->
        let opsc = lookup_scope env popsc in
          transf_r (Some opsc) env f

    | PFglob gp ->
        let mp = fst (trans_msymbol env gp) in
        let me =
          match EcEnv.Memory.current env with
          | None -> tyerror f.pl_loc env NoActiveMemory
          | Some me -> EcMemory.memory me
        in PFS.set_memused state; f_glob mp me

    | PFint n ->
        f_int n

    | PFtuple args -> begin
        let args = List.map (transf env) args in
          match args with
          | []  -> f_tt
          | [f] -> f
          | fs  -> f_tuple fs
    end

    | PFident ({ pl_desc = name; pl_loc = loc }, tvi) ->
        let tvi = tvi |> omap (transtvi env ue) in
        let ops = select_form_op env opsc name ue tvi [] in
        begin match ops with
        | [] ->
            tyerror loc env (UnknownVarOrOp (name, []))

        | [sel] -> begin
            let op = form_of_opselect (env, ue) loc sel [] in
            let inmem =
              match op.f_node with
              | Fpvar _ | Fproj ({ f_node = Fpvar _ }, _) -> true
              | _ -> false in
            if inmem then PFS.set_memused state; op
        end

        | _ ->
            let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in
            tyerror loc env (MultipleOpMatch (name, [], matches))
        end

    | PFside (f, side) -> begin
        let (sloc, side) = (side.pl_loc, unloc side) in
        let me =
          match EcEnv.Memory.lookup side env with
          | None -> tyerror sloc env (UnknownMemName side)
          | Some me -> EcMemory.memory me
        in

        let used, aout =
          PFS.new_memused
            (transf (EcEnv.Memory.set_active me env))
            state f
        in
        if not used then begin
          let ppe = EcPrinting.PPEnv.ofenv env in
          EcEnv.notify ~immediate:false env `Warning
            "unused memory `%s', while typing %a"
            side (EcPrinting.pp_form ppe) aout
        end;
        aout
      end

    | PFeqveq (xs, om) ->
        let lookup me x =
          match EcEnv.Var.lookup_progvar_opt ~side:me (unloc x) env with
          | None -> tyerror x.pl_loc env (UnknownVarOrOp (unloc x, []))
          | Some (x, ty) ->
              match x with
              | `Var x -> f_pvar x ty me
              | `Proj (x, ty', (i, n)) ->
                  if   i = 0 && n = 1
                  then f_pvar x ty me
                  else f_proj (f_pvar x ty' me) i ty
        in

        let check_mem loc me =
          match EcEnv.Memory.byid me env with
          | None -> tyerror loc env (UnknownMemName (EcIdent.name me))
          | Some _ -> ()
        in

        let qual (mq : pmsymbol option) (x : pqsymbol) =
          match mq with
          | None    -> x
          | Some qs ->
              let (nm, name) = x.pl_desc in
              { x with pl_desc = ((List.map (unloc |- fst) qs)@nm, name) }
        in

         let do1 = function
          | GVvar x ->
              let x1 = lookup EcFol.mleft  (qual (om |> omap fst) x) in
              let x2 = lookup EcFol.mright (qual (om |> omap snd) x) in
                unify_or_fail env ue x.pl_loc ~expct:x1.f_ty x2.f_ty;
                f_eq x1 x2

          | GVglob gp ->
              let (mp, _) = trans_msymbol env gp in
                let x1 = f_glob mp EcFol.mleft in
                let x2 = f_glob mp EcFol.mright in
                  unify_or_fail env ue gp.pl_loc ~expct:x1.f_ty x2.f_ty;
                  f_eq x1 x2
        in
          check_mem f.pl_loc EcFol.mleft;
          check_mem f.pl_loc EcFol.mright;
          EcFol.f_ands (List.map do1 xs)

    | PFeqf fs ->
        let check_mem loc me =
          match EcEnv.Memory.byid me env with
          | None -> tyerror loc env (UnknownMemName (EcIdent.name me))
          | Some _ -> ()

        and do1 (me1, me2) f =
          let _, f1 =
            PFS.new_memused
              (transf (EcEnv.Memory.set_active me1 env))
              state f in
          let _, f2 =
            PFS.new_memused
              (transf (EcEnv.Memory.set_active me2 env))
              state f in
          unify_or_fail env ue f.pl_loc ~expct:f1.f_ty f2.f_ty;
          f_eq f1 f2

        in
          check_mem f.pl_loc EcFol.mleft;
          check_mem f.pl_loc EcFol.mright;
          EcFol.f_ands (List.map (do1 (EcFol.mleft, EcFol.mright)) fs)

    | PFapp ({pl_desc = PFident ({ pl_desc = name; pl_loc = loc }, tvi)}, pes) ->
        let tvi  = tvi |> omap (transtvi env ue) in
        let es   = List.map (transf env) pes in
        let esig = List.map EcFol.f_ty es in
        let ops  = select_form_op env opsc name ue tvi esig in
          begin match ops with
          | [] ->
              let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in
                tyerror loc env (UnknownVarOrOp (name, esig))

          | [sel] ->
              let es = List.map2 (fun e l -> mk_loc l.pl_loc e) es pes in
              form_of_opselect (env, ue) loc sel es

          | _ ->
              let esig = Tuni.offun_dom (EcUnify.UniEnv.assubst ue) esig in
              let matches = List.map (fun (_, _, subue, m) -> (m, subue)) ops in
              tyerror loc env (MultipleOpMatch (name, esig, matches))
          end

    | PFapp (e, pes) ->
        let es    = List.map (transf env) pes in
        let esig  = List.map2 (fun f l -> mk_loc l.pl_loc f.f_ty) es pes in
        let op    = transf env e in
        let codom = ty_fun_app e.pl_loc env ue op.f_ty esig in
        f_app op es codom

    | PFif (pf1, pf2, pf3) ->
        let f1 = transf env pf1 in
        let f2 = transf env pf2 in
        let f3 = transf env pf3 in
          unify_or_fail env ue pf1.pl_loc ~expct:tbool   f1.f_ty;
          unify_or_fail env ue pf3.pl_loc ~expct:f2.f_ty f3.f_ty;
          f_if f1 f2 f3

    | PFlet (lp, (pf1, paty), f2) ->
        let (penv, p, pty) = transpattern env ue lp in
        let aty = paty |> omap (transty tp_uni env ue) in
        let f1 = transf env pf1 in
        unify_or_fail env ue pf1.pl_loc ~expct:pty f1.f_ty;
        aty |> oiter (fun aty-> unify_or_fail env ue pf1.pl_loc ~expct:pty aty);
        let f2 = transf penv f2 in
        f_let p f1 f2

    | PFforall (xs, pf) ->
        let env, xs = trans_gbinding env ue xs in
        let f = transf env pf in
          unify_or_fail env ue pf.pl_loc ~expct:tbool f.f_ty;
          f_forall xs f

    | PFexists (xs, f1) ->
        let env, xs = trans_gbinding env ue xs in
        let f = transf env f1 in
          unify_or_fail env ue f1.pl_loc ~expct:tbool f.f_ty;
          f_exists xs f

    | PFlambda (xs, f1) ->
        let env, xs = trans_binding env ue xs in
        let f = transf env f1 in
          f_lambda (List.map (fun (x,ty) -> (x,GTty ty)) xs) f

    | PFrecord fields ->
        let (ctor, fields, (rtvi, reccty)) =
          trans_record env ue
            (fun f -> let f = transf env f in (f, f.f_ty))
            (f.pl_loc, fields) in
        let ctor = f_op ctor rtvi (toarrow (List.map snd fields) reccty) in
        let ctor = f_app ctor (List.map fst fields) reccty in
          ctor

    | PFproj (subf, x) -> begin
      let subf = transf env subf in

      match select_proj env opsc (unloc x) ue None subf.f_ty with
      | [] ->
        let ty = Tuni.offun (EcUnify.UniEnv.assubst ue) subf.f_ty in
        let lf =
          let mp =
            match ty.ty_node with
            | Tglob mp -> mp
            | _ -> tyerror x.pl_loc env (UnknownProj (unloc x)) in

          match NormMp.norm_glob env EcFol.mhr mp with
          | { f_node = Ftuple xs } -> xs
          | _ -> tyerror x.pl_loc env (UnknownProj (unloc x))
        in

        let (vx, ty) =
          match EcEnv.Var.lookup_progvar_opt ~side:EcFol.mhr (unloc x) env with
          | None ->
              tyerror x.pl_loc env (UnknownVarOrOp (unloc x, []))
          | Some (`Var x, ty) ->
              (NormMp.norm_pvar env x, ty)
          | Some (_, _) ->
              tyerror x.pl_loc env (UnknownVarOrOp (unloc x, [])) in

        let find = function
          | { f_node = Fpvar (x, _) } ->
              EcTypes.pv_equal vx (NormMp.norm_pvar env x)
          | _ -> false in

        let i =
          match List.oindex find lf with
          | None   -> tyerror x.pl_loc env (UnknownProj (unloc x))
          | Some i -> i

        in f_proj subf i ty

      | _ :: _ :: _ ->
          tyerror x.pl_loc env (AmbiguousProj (unloc x))

      | [(op, tvi), pty, subue] ->
        EcUnify.UniEnv.restore ~src:subue ~dst:ue;
        let rty = EcUnify.UniEnv.fresh ue in
        (try  EcUnify.unify env ue (tfun subf.f_ty rty) pty
         with EcUnify.UnificationFailure _ -> assert false);
        f_app (f_op op tvi pty) [subf] rty
    end

    | PFproji (psubf, i) -> begin
      let subf = transf env psubf in
      let ty   = Tuni.offun (EcUnify.UniEnv.assubst ue) subf.f_ty in
      match (EcEnv.ty_hnorm ty env).ty_node with
      | Ttuple l when i < List.length l ->
          f_proj subf i (List.nth l i)
      | _ ->
          tyerror psubf.pl_loc env (AmbiguousProji (i, ty))
    end

    | PFprob (gp, args, m, event) ->
        let fpath = trans_gamepath env gp in
        let fun_  = EcEnv.Fun.by_xpath fpath env in
        let args,_ =
          transcall (fun f -> let f = transf env f in f, f.f_ty)
            env ue f.pl_loc fun_.f_sig args in
        let memid = transmem env m in
        let env = EcEnv.Fun.prF fpath env in
        let event' = transf env event in
        unify_or_fail env ue event.pl_loc ~expct:tbool event'.f_ty;
        f_pr memid fpath (f_tuple args) event'

    | PFhoareF (pre, gp, post) ->
        let fpath = trans_gamepath env gp in
        let penv, qenv = EcEnv.Fun.hoareF fpath env in
        let pre'  = transf penv pre in
        let post' = transf qenv post in
          unify_or_fail penv ue pre.pl_loc  ~expct:tbool pre' .f_ty;
          unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
          f_hoareF pre' fpath post'

    | PFBDhoareF (pre, gp, post, hcmp, bd) ->
        let fpath = trans_gamepath env gp in
        let penv, qenv = EcEnv.Fun.hoareF fpath env in
        let pre'  = transf penv pre in
        let post' = transf qenv post in
        let bd'   = transf penv bd in
          (* FIXME: check that there are not pvars in bd *)
          unify_or_fail penv ue pre .pl_loc ~expct:tbool pre' .f_ty;
          unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
          unify_or_fail env  ue bd  .pl_loc ~expct:treal bd'  .f_ty;
          f_bdHoareF pre' fpath post' hcmp bd'

    | PFlsless gp ->
        let fpath = trans_gamepath env gp in
          f_losslessF fpath

    | PFequivF (pre, (gp1, gp2), post) ->
        let fpath1 = trans_gamepath env gp1 in
        let fpath2 = trans_gamepath env gp2 in
        let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in
        let pre'  = transf penv pre in
        let post' = transf qenv post in
          unify_or_fail penv ue pre .pl_loc ~expct:tbool pre' .f_ty;
          unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
          f_equivF pre' fpath1 fpath2 post'

    | PFeagerF (pre, (s1,gp1,gp2,s2), post) ->
        let fpath1 = trans_gamepath env gp1 in
        let fpath2 = trans_gamepath env gp2 in
        let penv, qenv = EcEnv.Fun.equivF fpath1 fpath2 env in
        let pre'  = transf penv pre in
        let post' = transf qenv post in
        let s1    = transstmt env ue s1 in
        let s2    = transstmt env ue s2 in
        unify_or_fail penv ue pre .pl_loc ~expct:tbool pre' .f_ty;
        unify_or_fail qenv ue post.pl_loc ~expct:tbool post'.f_ty;
        f_eagerF pre' s1 fpath1 fpath2 s2 post'

  in

  let f = transf_r None env pf in
  tt |> oiter (fun tt -> unify_or_fail env ue pf.pl_loc ~expct:tt f.f_ty);
  f