let encodeExpr ev e = bracket (match e with
  | Ident x -> (escape x) 
  | EqOp (ex1,ex2) -> encodeExpr ev ex1^" = "^encodeExpr ev ex2
  | And (ex1,ex2) -> encodeExpr ev ex1^" "^wedge^" "^encodeExpr ev ex2
  | Or (ex1,ex2) -> encodeExpr ev ex1^" "^vee^" "^encodeExpr ev ex2
  | Not ex -> neg^" "^encodeExpr ev ex
  | Iff (ex1,ex2) -> encodeExpr ev ex1^" "^harr^" "^encodeExpr ev ex2
  | Implies (ex1,ex2) -> encodeExpr ev ex1^" "^rarr^" "^encodeExpr ev ex2
  | BFalse -> "False"
  | BTrue -> "True"
  | Appl app ->
    let (exf,ex) = getGenApp app in
    encodeExpr ev exf^" "^encodeExpr ev ex
  | Binder (q,VarSpec (vl,ty),ex) ->
    let qs = match q with
      | Forall -> " "^forall^" "
      | Exists -> " "^exists^" "
      | ExistsUniq -> " "^exists^"! "
      | Abs -> " "^lambda^" " in
    let (tys, ev') = match ty with
      | Some ty -> (" : "^encodeType ev ty, fold_left (fun e i -> addDecl e i ty) ev vl)
      | None -> ("",ev) in
    qs^(String.concat " , " (map escape vl))^tys^" . "^encodeExpr ev' ex
  | Desc (q,i,ty,ex) ->
    let qs = match q with
      | Iota -> " "^iota^" "
      | Epsilon -> " "^epsilon^" "
    in qs^i^" : "^encodeType ev ty^" . "^encodeExpr ev ex
  | Tuple exl ->
    fold_right
      (fun ex rest -> lang^" "^encodeExpr ev ex^" , "^ rest^" "^rang)
      exl
      (lang^rang)
  | If (ex1,ex2,ex3) -> "if "^encodeExpr ev ex1^" then "^encodeExpr ev ex2^ " else "^encodeExpr ev ex3
  | ConstrSel (ty, lbl) -> begin match normalize ev ty with
      | TInduct (id, fsl) ->
        let ctr = inductiveContainer id fsl in
        let (lam, bod) = findConstructor lbl ctr
        in lam^"roll "^bracket (inductiveContainerType ctr)^" "^bracket (bod)
      | _ -> raise (MatitaEncodeException "encodeExpr: No inductive type in constructor selector")
    end
  | Case (Ident id,cases) -> begin match cases with
      | [Branch (PatTuple pl, bdy)] ->
        let getIdent = function
          | PatIdent id -> id
          | PatNone | PatApp _ | PatTuple _ | PatRecord _ -> 
            raise (MatitaEncodeException ("encodeExpr: complex patterns not supported"))
        in
        bracket
          (fold_right
             (fun i rest -> "'uncurry "^bracket(lambda^" "^escape i^" ."^rest))
             (List.map getIdent pl)
             ("'point "^encodeExpr ev bdy))
        ^ bracket (encodeExpr ev (Ident id))
      | _ ->
        match normalize ev
          (try
             (Util.StringMap.find id ev.tydecl) 
           with Not_found ->
             raise (MatitaEncodeException ("encodeExpr: cannot find type for case analysis on "^id)))
        with
          | TInduct (ind, fsl) ->
            let ctr = inductiveContainer ind fsl in
            let pred = "P_"^ind in
            let return f = " return "^lambda^"w. ("^pred^" "^f "w"^" "^rarr^" "^pred^" s) "^rarr^" ? " in
            let header bdy = "let "^pred^" "^defeq^" pos "^bracket (inductiveContainerType ctr)^" in "
              ^ "match "^encodeExpr ev (Ident id)^" with "
              ^ "[roll r "^rArr^" match r with [contain s f "^rArr^" "^bdy
              ^ " ("^lambda^"x.x)]]" in
            let mkCase (lbl,cont) rest (bv,f) =
              let rec findLabel = function 
                | PatIdent x -> x = lbl
                | PatApp (l,_) -> findLabel l
                | PatNone | PatTuple _ | PatRecord _ -> false
              in
              let Branch (p,bdy) = match List.filter (fun (Branch (p,_)) -> findLabel p) cases with
                | [] -> failwith ("encodeExpr: case "^lbl^" not found")
                | [p0] -> p0
                | _ ->  failwith ("encodeExpr: multiple case "^lbl^" found") in                                                          
              let mkBranch _ rest (n,f) =
                let v = "z"^string_of_int n in
                let f' x = f (lang^v^", "^x^rang) in
                "match y"^return f^"with [pair "^v^" y "^rArr^" "^rest (n+1,f')^"]" in
              let rec content n = if 0 = n then sigma^"1 z" else sigma^"2"^bracket (content (n-1)) in
              let rec binds n p cont = match p, cont with
                | PatIdent _, [] -> ""
                | PatApp (p, PatIdent bv), c::cs ->
                  "let "^escape bv^" "^defeq^" "^c.psi^" "^bracket ("contain ? ? z"^string_of_int n^" "^bracket (lambda^"z. f "^bracket ("cast "^bracket (content n))))^" in "^binds (n+1) p cs
                | _ -> raise (MatitaEncodeException ("encodeExpr: complex patterns not supported for inductive types"))
              in
              let endBranch (_,f) = "match y"^return f^"with [neo "^rArr^" "^lambda^"cast. "^binds 0 p cont^" "^encodeExpr ev bdy^"]" in
              "match "^bv^return f^"with "
              ^ "[ sigma1 y "^rArr^" "^fold_right mkBranch cont endBranch (0,fun x -> f (bracket (sigma^"1 "^x)))^" "
              ^ "| sigma2 x "^rArr^" "^rest ("x",fun x -> f (bracket (sigma^"2 "^x)))
              ^ "]" in
            let bdy = fold_right mkCase ctr (fun (bv,_) -> "[]"^bv) in
            header (bdy ("s",fun x -> x))
          | _ -> failwith ("encodeExpr: not an inductive type for "^id)
  end
  | _ ->
    let module M = Printers.Make(Printers.Configuration.ASCII)(Printers.Options.StdOpt)
          (struct let f = Format.str_formatter end) in
    let _ = M.expr e in
    raise (MatitaEncodeException ("encodeExpr: not implemented:"^Format.flush_str_formatter ()))
)