expr-visitor.sml

signature EXPR_VISITOR_PARAMS = sig
structure S : EXPR
structure T : EXPR
end

functor ExprVisitorFn (Params : EXPR_VISITOR_PARAMS) = struct

structure SrcExprUtil = ExprUtilFn (Params.S)
open SrcExprUtil
open Params
open Unbound
open Namespaces
open Binders
open Operators
open Region
open Pattern
open S

infixr 0 $
       
type ('this, 'env) expr_visitor_vtable =
     {
       visit_expr : 'this -> 'env -> expr -> T.expr,
       visit_EVar : 'this -> 'env -> var * (bool * bool) -> T.expr,
       visit_EConst : 'this -> 'env -> expr_const * region -> T.expr,
       visit_EUnOp : 'this -> 'env -> expr_un_op * expr * region -> T.expr,
       visit_EBinOp : 'this -> 'env -> expr_bin_op * expr * expr -> T.expr,
       visit_ETriOp : 'this -> 'env -> expr_tri_op * expr * expr * expr -> T.expr,
       visit_EEI : 'this -> 'env -> expr_EI * expr * idx -> T.expr,
       visit_EET : 'this -> 'env -> expr_ET * expr * mtype -> T.expr,
       visit_ET : 'this -> 'env -> expr_T * mtype * region -> T.expr,
       visit_EAbs : 'this -> 'env -> idx StMap.map * (ptrn, expr) bind * (idx * idx) option -> T.expr,
       visit_EAbsI : 'this -> 'env -> (sort, expr) ibind_anno * region -> T.expr,
       visit_EAppConstr : 'this -> 'env -> (cvar * (bool * bool)) * mtype list * idx list * expr * (int * mtype) option -> T.expr,
       visit_ECase : 'this -> 'env -> expr * return * (ptrn, expr) bind list * region -> T.expr,
       visit_ELet : 'this -> 'env -> return * (decl tele, expr) bind * region -> T.expr,
       (* visit_ECaseSumbool : 'this -> 'env -> expr * expr ibind * expr ibind * region -> T.expr, *)
       
       (* visit_decl : 'this -> 'env ctx -> decl -> T.decl, *)
       (* visit_DVal : 'this -> 'env ctx -> ebinder * (tbinder list, expr) bind outer * region -> T.decl, *)
       (* visit_DValPtrn : 'this -> 'env ctx -> ptrn * expr outer * region -> T.decl, *)
       (* visit_DRec : 'this -> 'env ctx -> ebinder * (tbinder list * stbind tele rebind, (mtype * idx) * expr) bind inner * region -> T.decl, *)
       (* visit_DIdxDef : 'this -> 'env ctx -> ibinder * sort outer * idx outer -> T.decl, *)
       (* visit_DAbsIdx2 : 'this -> 'env ctx -> ibinder * sort outer * idx outer -> T.decl, *)
       (* visit_DAbsIdx : 'this -> 'env ctx -> (ibinder * sort outer * idx outer) * decl tele rebind * region -> T.decl, *)
       (* visit_DTypeDef : 'this -> 'env ctx -> tbinder * mtype outer -> T.decl, *)
       (* visit_DOpen : 'this -> 'env ctx -> mod_id outer * scoping_ctx option -> T.decl, *)
       
       visit_decl : 'this -> 'env ctx -> decl -> T.decl list,
       visit_DVal : 'this -> 'env ctx -> ebinder * ((tbinder * (idx * idx) outer) list, expr) bind outer * region -> T.decl list,
       visit_DValPtrn : 'this -> 'env ctx -> ptrn * expr outer * region -> T.decl list,
       visit_DRec : 'this -> 'env ctx -> ebinder * ((tbinder * (idx * idx) outer) list * stbind tele rebind, (idx StMap.map * idx StMap.map) * (mtype * (idx * idx)) * expr) bind inner * region -> T.decl list,
       visit_DIdxDef : 'this -> 'env ctx -> ibinder * sort option outer * idx outer -> T.decl list,
       visit_DAbsIdx2 : 'this -> 'env ctx -> ibinder * sort outer * idx outer -> T.decl list,
       visit_DAbsIdx : 'this -> 'env ctx -> (ibinder * sort outer * idx outer) * decl tele rebind * region -> T.decl list,
       visit_DTypeDef : 'this -> 'env ctx -> tbinder * mtype outer -> T.decl list,
       visit_DConstrDef : 'this -> 'env ctx -> cbinder * cvar outer -> T.decl list,
       visit_DOpen : 'this -> 'env ctx -> mod_id inner * scoping_ctx option -> T.decl list,
       
       visit_sgn : 'this -> 'env ctx -> sgn -> T.sgn,
       visit_spec : 'this -> 'env ctx -> spec -> T.spec,
       visit_mod : 'this -> 'env ctx -> mod -> T.mod,
       visit_ty : 'this -> 'env -> ty -> T.ty,
       visit_kind : 'this -> 'env -> kind -> T.kind,
       visit_SpecVal : 'this -> 'env ctx -> name * ty -> T.spec,
       visit_SpecIdx : 'this -> 'env ctx -> name * sort -> T.spec,
       visit_SpecType : 'this -> 'env ctx -> name * kind -> T.spec,
       visit_SpecTypeDef : 'this -> 'env ctx -> name * mtype -> T.spec,
       visit_ModComponents : 'this -> 'env ctx -> decl list * region -> T.mod,
       visit_ModSeal : 'this -> 'env ctx -> mod * sgn -> T.mod,
       visit_ModTransparentAsc : 'this -> 'env ctx -> mod * sgn -> T.mod,
       visit_ptrn : 'this -> 'env ctx -> ptrn -> T.ptrn,
       visit_PnVar : 'this -> 'env ctx -> ebinder -> T.ptrn,
       visit_PnTT : 'this -> 'env ctx -> region -> T.ptrn,
       (* visit_PnPair : 'this -> 'env ctx -> ptrn * ptrn -> T.ptrn, *)
       visit_PnAlias : 'this -> 'env ctx -> ebinder * ptrn * region -> T.ptrn,
       visit_PnConstr : 'this -> 'env ctx -> ((cvar * ptrn_constr_tag) * bool) outer * ibinder list * ptrn * region -> T.ptrn,
       visit_PnAnno : 'this -> 'env ctx -> ptrn * mtype outer -> T.ptrn,
       visit_EApp : 'this -> 'env -> expr * expr -> T.expr,
       (* visit_EPair : 'this -> 'env -> expr * expr -> T.expr, *)
       visit_EAdd : 'this -> 'env -> expr * expr -> T.expr,
       visit_ENatAdd : 'this -> 'env -> expr * expr -> T.expr,
       visit_ENew : 'this -> 'env -> int * (expr * expr) -> T.expr,
       visit_ERead : 'this -> 'env -> int * (expr * expr) -> T.expr,
       visit_EAppI : 'this -> 'env -> expr * idx -> T.expr,
       visit_EAscTime : 'this -> 'env -> expr * idx -> T.expr,
       visit_EAppT : 'this -> 'env -> expr * mtype -> T.expr,
       visit_EAsc : 'this -> 'env -> expr * mtype -> T.expr,
       visit_var : 'this -> 'env -> var -> T.var,
       visit_cvar : 'this -> 'env -> cvar -> T.cvar,
       visit_mod_id : 'this -> 'env -> mod_id -> T.mod_id,
       visit_idx : 'this -> 'env -> idx -> T.idx,
       visit_sort : 'this -> 'env -> sort -> T.sort,
       visit_mtype : 'this -> 'env -> mtype -> T.mtype,
       visit_ptrn_constr_tag : 'this -> 'env -> ptrn_constr_tag -> T.ptrn_constr_tag,
       extend_i : 'this -> 'env -> iname -> 'env * iname,
       extend_t : 'this -> 'env -> tname -> 'env * tname,
       extend_c : 'this -> 'env -> cname -> 'env * cname,
       extend_e : 'this -> 'env -> ename -> 'env * ename
     }
       
type ('this, 'env) expr_visitor_interface =
     ('this, 'env) expr_visitor_vtable
                                       
(***************** the default visitor  **********************)    

open VisitorUtil
       
(* val visit_ibind = Unbound.visit_bind_simp *)
(* val visit_tbind = Unbound.visit_bind_simp *)
(* val visit_ebind = Unbound.visit_bind_simp *)

structure PV = PatternVisitor
       
fun visit_decls visit_decl ctx decls =
  let
  in
    Teles $ List.concat $ unTeles $ visit_tele visit_decl ctx decls
  end
    
fun default_expr_visitor_vtable
      (cast : 'this -> ('this, 'env) expr_visitor_interface)
      extend_i
      extend_t
      extend_c
      extend_e
      visit_var
      visit_cvar
      visit_mod_id
      visit_idx
      visit_sort
      visit_mtype
      visit_ty
      visit_kind
      visit_ptrn_constr_tag
    : ('this, 'env) expr_visitor_vtable =
  let
    fun visit_ibind this = visit_bind_simp (#extend_i (cast this) this)
    fun visit_ibind_anno this = visit_bind_anno (#extend_i (cast this) this)
    fun visit_expr this env data =
      let
        val vtable = cast this
      in
        case data of
	    EVar data => #visit_EVar vtable this env data
          | EConst data => #visit_EConst vtable this env data
          | EState data => T.EState data
          | EUnOp data => #visit_EUnOp vtable this env data
          | EBinOp data => #visit_EBinOp vtable this env data
	  | ETriOp data => #visit_ETriOp vtable this env data
          | EEI data => #visit_EEI vtable this env data
          | EET data => #visit_EET vtable this env data
          | ET data => #visit_ET vtable this env data
          | EAscState (e, st) =>
            let
              val e = #visit_expr vtable this env e
              val st = StMap.map (#visit_idx vtable this env) st
            in
              T.EAscState (e, st)
            end
          | ENewArrayValues (w, t, es, r) => T.ENewArrayValues (w, #visit_mtype vtable this env t, visit_list (#visit_expr vtable this) env es, r)
	  | EAbs data => #visit_EAbs vtable this env data
	  | EAbsI data => #visit_EAbsI vtable this env data
	  | EAppConstr data => #visit_EAppConstr vtable this env data
	  | ECase data => #visit_ECase vtable this env data
	  | ELet data => #visit_ELet vtable this env data
	  (* | ECaseSumbool data => #visit_ECaseSumbool vtable this env data *)
	  | EIfi (e, bind1, bind2, r) =>
            T.EIfi
              (#visit_expr vtable this env e,
               visit_ibind this (#visit_expr vtable this) env bind1,
               visit_ibind this (#visit_expr vtable this) env bind2, r)
          | ESet (x, es, e, r) => T.ESet (x, visit_list (visit_pair (#visit_expr vtable this) return2) env es, #visit_expr vtable this env e, r)
          | EGet (x, es, r) => T.EGet (x, visit_list (visit_pair (#visit_expr vtable this) return2) env es, r)
          | EEnv (name, r) => T.EEnv (name, r)
          | ERecord (fields, r) => T.ERecord (SMap.map (#visit_expr vtable this env) fields, r)
          | ETuple data => T.ETuple $ visit_list (#visit_expr vtable this) env data
          | EDispatch (ls, r) =>
            T.EDispatch (map (fn (name, e, t1, t2) => (name, #visit_expr vtable this env e, Option.map (#visit_mtype vtable this env) t1, Option.map (#visit_mtype vtable this env) t2)) ls, r)
          (* | EDebugLog e => *)
          (*   T.EDebugLog $ #visit_expr vtable this env e *)
      end
    fun visit_EVar this env data =
      let
        val vtable = cast this
        val (var, eia) = data
        val var = #visit_var vtable this env var
      in
        T.EVar (var, eia)
      end
    fun visit_EConst this env data =
      let
        val vtable = cast this
      in
        T.EConst data
      end
    fun visit_EUnOp this env data =
      let
        val vtable = cast this
        val (opr, e, r) = data
        val e = #visit_expr vtable this env e
      in
        T.EUnOp (opr, e, r)
      end
    fun visit_EBinOp this env data =
      let
        val vtable = cast this
        val (opr, e1, e2) = data
        val data = (e1, e2)
      in
        case opr of
            EBApp () => #visit_EApp vtable this env data
          (* | EBPair () => #visit_EPair vtable this env data *)
          | EBNew w => #visit_ENew vtable this env (w, data)
          | EBRead w => #visit_ERead vtable this env (w, data)
          | EBPrim (EBPIntAdd ()) => #visit_EAdd vtable this env data
          | EBNat (EBNAdd ()) => #visit_ENatAdd vtable this env data
          | _ => T.EBinOp (opr, #visit_expr vtable this env e1, #visit_expr vtable this env e2)
      end
    fun visit_EApp this env data =
      let
        val vtable = cast this
        val (e1, e2) = data
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
      in
        T.EBinOp (EBApp (), e1, e2)
      end
    (* fun visit_EPair this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (e1, e2) = data *)
    (*     val e1 = #visit_expr vtable this env e1 *)
    (*     val e2 = #visit_expr vtable this env e2 *)
    (*   in *)
    (*     T.EBinOp (EBPair (), e1, e2) *)
    (*   end *)
    fun visit_EAdd this env data =
      let
        val vtable = cast this
        val (e1, e2) = data
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
      in
        T.EBinOp (EBAdd, e1, e2)
      end
    fun visit_ENatAdd this env data =
      let
        val vtable = cast this
        val (e1, e2) = data
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
      in
        T.EBinOp (EBNatAdd, e1, e2)
      end
    fun visit_ENew this env (w, (e1, e2)) =
      let
        val vtable = cast this
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
      in
        T.EBinOp (EBNew w, e1, e2)
      end
    fun visit_ERead this env (w, (e1, e2)) =
      let
        val vtable = cast this
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
      in
        T.EBinOp (EBRead w, e1, e2)
      end
    fun visit_ETriOp this env data =
      let
        val vtable = cast this
        val (opr, e1, e2, e3) = data
        val e1 = #visit_expr vtable this env e1
        val e2 = #visit_expr vtable this env e2
        val e3 = #visit_expr vtable this env e3
      in
        T.ETriOp (opr, e1, e2, e3)
      end
    fun visit_EEI this env data = 
      let
        val vtable = cast this
        val (opr, e, i) = data
        val data = (e, i)
      in
        case opr of
	    EEIAppI () => #visit_EAppI vtable this env data
	  | EEIAscTime () => #visit_EAscTime vtable this env data
	  | EEIAscSpace () =>
            T.EEI (EEIAscSpace (), #visit_expr vtable this env e, #visit_idx vtable this env i)
      end
    fun visit_EAppI this env data = 
      let
        val vtable = cast this
        val (e, i) = data
        val e = #visit_expr vtable this env e
        val i = #visit_idx vtable this env i
      in
        T.EEI (EEIAppI (), e, i)
      end
    fun visit_EAscTime this env data = 
      let
        val vtable = cast this
        val (e, i) = data
        val e = #visit_expr vtable this env e
        val i = #visit_idx vtable this env i
      in
        T.EEI (EEIAscTime (), e, i)
      end
    fun visit_EET this env data = 
      let
        val vtable = cast this
        val (opr, e, t) = data
        val data = (e, t)
      in
        case opr of
	    EETAppT () => #visit_EAppT vtable this env data
	  | EETAsc () => #visit_EAsc vtable this env data
          | EETHalt _ => T.EET (opr, #visit_expr vtable this env e, #visit_mtype vtable this env t)
      end
    fun visit_EAppT this env data = 
      let
        val vtable = cast this
        val (e, t) = data
        val e = #visit_expr vtable this env e
        val t = #visit_mtype vtable this env t
      in
        T.EET (EETAppT (), e, t)
      end
    fun visit_EAsc this env data = 
      let
        val vtable = cast this
        val (e, t) = data
        val e = #visit_expr vtable this env e
        val t = #visit_mtype vtable this env t
      in
        T.EET (EETAsc (), e, t)
      end
    fun visit_ET this env data = 
      let
        val vtable = cast this
        val (opr, t, r) = data
        val t = #visit_mtype vtable this env t
      in
        T.ET (opr, t, r)
      end
    fun visit_EAbs this env (st, bind, spec) =
      let
        val vtable = cast this
        val st = StMap.map (#visit_idx vtable this env) st
        val bind = visit_bind (#visit_ptrn vtable this) (#visit_expr vtable this) env bind
        val spec = visit_option (visit_pair (#visit_idx vtable this) (#visit_idx vtable this)) env spec
      in
        T.EAbs (st, bind, spec)
      end
    fun visit_EAbsI this env data =
      let
        val vtable = cast this
        val (bind, r) = data
        val bind = visit_ibind_anno this (#visit_sort vtable this) (#visit_expr vtable this) env bind
      in
        T.EAbsI (bind, r)
      end
    fun visit_EAppConstr this env data = 
      let
        val vtable = cast this
        val ((var, eia), ts, is, e, ot) = data
        val var = #visit_cvar vtable this env var
        val ts = map (#visit_mtype vtable this env) ts
        val is = map (#visit_idx vtable this env) is
        val e = #visit_expr vtable this env e
        val ot = Option.map (mapSnd (#visit_mtype vtable this env)) ot
      in
        T.EAppConstr ((var, eia), ts, is, e, ot)
      end
    fun visit_return this env (t, i, j) =
      let
        val vtable = cast this
        val t = Option.map (#visit_mtype vtable this env) t                                      
        val i = Option.map (#visit_idx vtable this env) i                                     
        val j = Option.map (#visit_idx vtable this env) j
      in
        (t, i, j)
      end
    fun visit_ECase this env data =
      let
        val vtable = cast this
        val (e, return, binds, r) = data
        val e = #visit_expr vtable this env e
        val return = visit_return this env return
        val binds = map (visit_bind (#visit_ptrn vtable this) (#visit_expr vtable this) env) binds
      in
        T.ECase (e, return, binds, r)
      end
    fun visit_ELet this env data =
      let
        val vtable = cast this
        val (return, bind, r) = data
        val return = visit_return this env return
        val bind = visit_bind (visit_decls (#visit_decl vtable this)) (#visit_expr vtable this) env bind
      in
        T.ELet (return, bind, r)
      end
    (* fun visit_ECaseSumbool this env (e, bind1, bind2, r) = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val e = #visit_expr vtable this env e *)
    (*     val bind1 = visit_ibind this (#visit_expr vtable this) env bind1 *)
    (*     val bind2 = visit_ibind this (#visit_expr vtable this) env bind2 *)
    (*   in *)
    (*     T.ECaseSumbool (e, bind1, bind2, r) *)
    (*   end *)
    fun visit_decl this env data =
      let
        val vtable = cast this
      in
        case data of
            DVal data => #visit_DVal vtable this env data
          | DValPtrn data => #visit_DValPtrn vtable this env data
          | DRec data => #visit_DRec vtable this env data
          | DIdxDef data => #visit_DIdxDef vtable this env data
          | DAbsIdx2 data => #visit_DAbsIdx2 vtable this env data
          | DAbsIdx data => #visit_DAbsIdx vtable this env data
          | DTypeDef data => #visit_DTypeDef vtable this env data
          | DConstrDef data => #visit_DConstrDef vtable this env data
          | DOpen data => #visit_DOpen vtable this env data
      end
    fun visit_ibinder this env name =
      let
        val vtable = cast this
        val name = visit_binder (#extend_i vtable this) env name
      in
        name
      end
    fun visit_tbinder this env name =
      let
        val vtable = cast this
        val name = visit_binder (#extend_t vtable this) env name
      in
        name
      end
    fun visit_cbinder this env name =
      let
        val vtable = cast this
        val name = visit_binder (#extend_c vtable this) env name
      in
        name
      end
    fun visit_ebinder this env name =
      let
        val vtable = cast this
        val name = visit_binder (#extend_e vtable this) env name
      in
        name
      end
        
    (* fun visit_DVal this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (name, bind, r) = data *)
    (*     val name = visit_ebinder this env name *)
    (*     val bind = visit_outer (visit_bind (visit_list (visit_tbinder this)) (#visit_expr vtable this)) env bind *)
    (*   in *)
    (*     T.DVal (name, bind, r) *)
    (*   end *)
    (* fun visit_DValPtrn this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (pn, e, r) = data *)
    (*     val pn = #visit_ptrn vtable this env pn *)
    (*     val e = visit_outer (#visit_expr vtable this) env e *)
    (*   in *)
    (*     T.DValPtrn (pn, e, r) *)
    (*   end *)
    (* fun visit_stbind this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*   in *)
    (*     case data of *)
    (*         SortingST data => T.SortingST $ visit_pair (visit_ibinder this) (visit_outer (#visit_sort vtable this)) env data *)
    (*       | TypingST pn => T.TypingST $ #visit_ptrn vtable this env pn *)
    (*   end *)
    (* fun visit_DRec this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (name, bind, r) = data *)
    (*     val name = visit_ebinder this env name *)
    (*     val bind = *)
    (*         visit_inner ( *)
    (*           visit_bind (visit_pair (visit_list (visit_tbinder this)) *)
    (*                                  (visit_rebind (visit_tele (visit_stbind this)))) *)
    (*                      (visit_pair (visit_pair (#visit_mtype vtable this) *)
    (*                                              (#visit_idx vtable this)) *)
    (*                                  (#visit_expr vtable this))) env bind *)
    (*   in *)
    (*     T.DRec (name, bind, r) *)
    (*   end *)
    (* fun visit_DIdxDef this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (name, s, i) = data *)
    (*     val name = visit_ibinder this env name *)
    (*     val s = visit_outer (#visit_sort vtable this) env s *)
    (*     val i = visit_outer (#visit_idx vtable this) env i *)
    (*   in *)
    (*     T.DIdxDef (name, s, i) *)
    (*   end *)
    (* fun visit_DAbsIdx2 this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (name, s, i) = data *)
    (*     val name = visit_ibinder this env name *)
    (*     val s = visit_outer (#visit_sort vtable this) env s *)
    (*     val i = visit_outer (#visit_idx vtable this) env i *)
    (*   in *)
    (*     T.DAbsIdx2 (name, s, i) *)
    (*   end *)
    (* fun visit_DAbsIdx this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val ((name, s, i), decls, r) = data *)
    (*     val name = visit_ibinder this env name *)
    (*     val s = visit_outer (#visit_sort vtable this) env s *)
    (*     val i = visit_outer (#visit_idx vtable this) env i *)
    (*     val decls = visit_rebind (visit_decls (#visit_decl vtable this)) env decls *)
    (*   in *)
    (*     T.DAbsIdx ((name, s, i), decls, r) *)
    (*   end *)
    (* fun visit_DTypeDef this env data = *)
    (*   let *)
    (*     (* val () = println "default visit_DTypeDef" *) *)
    (*     val vtable = cast this *)
    (*     val (name, t) = data *)
    (*     val name = visit_tbinder this env name *)
    (*     val cnames = map (Binder o CName) $ get_constr_names $ unOuter t *)
    (*     val t = visit_outer (#visit_mtype vtable this) env t *)
    (*     val cnames = visit_list (visit_cbinder this) env cnames *)
    (*   in *)
    (*     T.DTypeDef (name, t) *)
    (*   end *)
    (* fun visit_scoping_ctx this env (sctx, kctx, cctx, tctx) = *)
    (*   let *)
    (*     val _ = visit_list (visit_ibinder this) env $ rev sctx *)
    (*     val _ = visit_list (visit_tbinder this) env $ rev kctx *)
    (*     val _ = visit_list (visit_cbinder this) env $ rev cctx *)
    (*     val _ = visit_list (visit_ebinder this) env $ rev tctx *)
    (*   in *)
    (*     (sctx, kctx, cctx, tctx) *)
    (*   end *)
    (* fun visit_DOpen this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (m, scp) = data *)
    (*     val m = visit_outer (#visit_mod_id vtable this) env m *)
    (*     val scp = Option.map (visit_scoping_ctx this env) scp *)
    (*   in *)
    (*     T.DOpen (m, scp) *)
    (*   end *)
        
    fun visit_DVal this env data =
      let
        val vtable = cast this
        val (name, bind, r) = data
        val name = visit_ebinder this env name
        val bind = visit_outer (visit_bind
                                  (visit_list (visit_pair
                                                 (visit_tbinder this)
                                                 (visit_outer
                                                    (visit_pair (#visit_idx vtable this)
                                                                (#visit_idx vtable this)))))
                                  (#visit_expr vtable this)) env bind
      in
        [T.DVal (name, bind, r)]
      end
    fun visit_DValPtrn this env data =
      let
        val vtable = cast this
        val (pn, e, r) = data
        val pn = #visit_ptrn vtable this env pn
        val e = visit_outer (#visit_expr vtable this) env e
      in
        [T.DValPtrn (pn, e, r)]
      end
    fun visit_map f env st = StMap.map (f env) st
    fun visit_stbind this env data =
      let
        val vtable = cast this
      in
        case data of
            SortingST data => T.SortingST $ visit_pair (visit_ibinder this) (visit_outer (#visit_sort vtable this)) env data
          | TypingST pn => T.TypingST (#visit_ptrn vtable this env pn)
      end
    fun visit_DRec this env data =
      let
        val vtable = cast this
        val (name, bind, r) = data
        val name = visit_ebinder this env name
        val bind =
            visit_inner (
              visit_bind (visit_pair (visit_list (visit_pair
                                                    (visit_tbinder this)
                                                    (visit_outer
                                                       (visit_pair (#visit_idx vtable this)
                                                                   (#visit_idx vtable this)))))
                                     (visit_rebind (visit_tele (visit_stbind this))))
                         (visit_triple (visit_pair (visit_map $ #visit_idx vtable this)
                                                   (visit_map $ #visit_idx vtable this))
                                       (visit_pair (#visit_mtype vtable this)
                                                   (visit_pair (#visit_idx vtable this)
                                                               (#visit_idx vtable this)))
                                       (#visit_expr vtable this))) env bind
      in
        [T.DRec (name, bind, r)]
      end
    fun visit_DIdxDef this env data =
      let
        val vtable = cast this
        val (name, s, i) = data
        val name = visit_ibinder this env name
        val s = visit_outer (visit_option (#visit_sort vtable this)) env s
        val i = visit_outer (#visit_idx vtable this) env i
      in
        [T.DIdxDef (name, s, i)]
      end
    fun visit_DAbsIdx2 this env data =
      let
        val vtable = cast this
        val (name, s, i) = data
        val name = visit_ibinder this env name
        val s = visit_outer (#visit_sort vtable this) env s
        val i = visit_outer (#visit_idx vtable this) env i
      in
        [T.DAbsIdx2 (name, s, i)]
      end
    fun visit_DAbsIdx this env data =
      let
        val vtable = cast this
        val ((name, s, i), decls, r) = data
        val name = visit_ibinder this env name
        val s = visit_outer (#visit_sort vtable this) env s
        val i = visit_outer (#visit_idx vtable this) env i
        val decls = visit_rebind (visit_decls (#visit_decl vtable this)) env decls
      in
        [T.DAbsIdx ((name, s, i), decls, r)]
      end
    fun visit_DTypeDef this env data =
      let
        (* val () = println "default visit_DTypeDef" *)
        val vtable = cast this
        val (name, t) = data
        val name = visit_tbinder this env name
        val t = visit_outer (#visit_mtype vtable this) env t
        val cnames = map (Binder o CName) $ T.get_constr_names $ unOuter t
        val cnames = visit_list (visit_cbinder this) env cnames
      in
        [T.DTypeDef (name, t)]
      end
    fun visit_DConstrDef this env data =
      let
        val vtable = cast this
        val (name, x) = data
        val name = visit_cbinder this env name
        val x = visit_outer (#visit_cvar vtable this) env x
      in
        [T.DConstrDef (name, x)]
      end
    fun visit_scoping_ctx this env (sctx, kctx, cctx, tctx) =
      let
        val _ = visit_list (visit_ibinder this) env $ rev sctx
        val _ = visit_list (visit_tbinder this) env $ rev kctx
        val _ = visit_list (visit_cbinder this) env $ rev cctx
        val _ = visit_list (visit_ebinder this) env $ rev tctx
      in
        (sctx, kctx, cctx, tctx)
      end
    fun visit_DOpen this env data =
      let
        val vtable = cast this
        val (m, scp) = data
        val m = visit_inner (#visit_mod_id vtable this) env m
        val scp = Option.map (visit_scoping_ctx this env) scp
      in
        [T.DOpen (m, scp)]
      end
        
    fun visit_cvar_tag this env data =
      let
        val vtable = cast this
      in
        visit_pair (#visit_cvar vtable this) (#visit_ptrn_constr_tag vtable this) env data
      end
    fun this_impls_ptrn_visitor_interface this :
        ('this, 'env, cvar * ptrn_constr_tag, mtype, T.cvar * T.ptrn_constr_tag, T.mtype) PV.ptrn_visitor_interface =
      let
        val vtable = cast this
      in
        {
          visit_ptrn = #visit_ptrn vtable,
          visit_PnVar = #visit_PnVar vtable,
          visit_PnTT = #visit_PnTT vtable,
          (* visit_PnPair = #visit_PnPair vtable, *)
          visit_PnAlias = #visit_PnAlias vtable,
          visit_PnAnno = #visit_PnAnno vtable,
          visit_PnConstr = #visit_PnConstr vtable,
          visit_cvar = visit_cvar_tag,
          visit_mtype = #visit_mtype vtable,
          extend_i = #extend_i vtable,
          extend_e = #extend_e vtable
        }
      end
    val pv_vtable =
        PV.default_ptrn_visitor_vtable
          this_impls_ptrn_visitor_interface
          extend_i
          extend_e
          visit_cvar_tag
          visit_mtype
          
    (* fun visit_ptrn this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*   in *)
    (*     case data of *)
    (*         PnVar data => #visit_PnVar vtable this env data *)
    (*       | PnTT data => #visit_PnTT vtable this env data *)
    (*       | PnPair data => #visit_PnPair vtable this env data *)
    (*       | PnAlias data => #visit_PnAlias vtable this env data *)
    (*       | PnConstr data => #visit_PnConstr vtable this env data *)
    (*       | PnAnno data => #visit_PnAnno vtable this env data *)
    (*   end *)
    (* fun visit_PnVar this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*   in *)
    (*     PnVar $ visit_ebinder this env data *)
    (*   end *)
    (* fun visit_PnTT this env data = *)
    (*   PnTT data *)
    (* fun visit_PnPair this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (p1, p2) = data *)
    (*     val p1 = #visit_ptrn vtable this env p1 *)
    (*     val p2 = #visit_ptrn vtable this env p2 *)
    (*   in *)
    (*     PnPair (p1, p2) *)
    (*   end *)
    (* fun visit_PnAlias this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (name, p, r) = data *)
    (*     val name = visit_ebinder this env name *)
    (*     val p = #visit_ptrn vtable this env p *)
    (*   in *)
    (*     PnAlias (name, p, r) *)
    (*   end *)
    (* fun visit_PnAnno this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (p, t) = data *)
    (*     val p = #visit_ptrn vtable this env p *)
    (*     val t = visit_outer (#visit_mtype vtable this) env t *)
    (*   in *)
    (*     PnAnno (p, t) *)
    (*   end *)
    (* fun visit_PnConstr this env data = *)
    (*   let *)
    (*     val vtable = cast this *)
    (*     val (x, inames, p, r) = data *)
    (*     val x = visit_outer (visit_pair (visit_pair (#visit_cvar vtable this) (#visit_ptrn_constr_tag vtable this)) return2) env x *)
    (*     val inames = map (visit_ibinder this env) inames *)
    (*     val p = #visit_ptrn vtable this env p *)
    (*   in *)
    (*     PnConstr (x, inames, p, r) *)
    (*   end *)

          
    fun visit_sgn this env data =
      let
        val vtable = cast this
        val (specs, r) = data
        val specs = unTeles $ visit_tele (#visit_spec vtable this) env $ Teles specs
      in
        (specs, r)
      end
    fun visit_spec this env data =
      let
        val vtable = cast this
      in
        case data of
            SpecVal data => #visit_SpecVal vtable this env data
          | SpecIdx data => #visit_SpecIdx vtable this env data
          | SpecType data => #visit_SpecType vtable this env data
          | SpecTypeDef data => #visit_SpecTypeDef vtable this env data
      end
    fun visit_SpecVal this env data =
      let
        val vtable = cast this
        val (ename, t) = data
        val ename = unBinderName $ visit_ebinder this env $ EBinder ename
        val t = unOuter $ visit_outer (#visit_ty vtable this) env $ Outer t
      in
        T.SpecVal (ename, t)
      end
    fun visit_SpecIdx this env data =
      let
        val vtable = cast this
        val (iname, s) = data
        val iname = unBinderName $ visit_ibinder this env $ IBinder iname
        val s = unOuter $ visit_outer (#visit_sort vtable this) env $ Outer s
      in
        T.SpecIdx (iname, s)
      end
    fun visit_SpecType this env data =
      let
        val vtable = cast this
        val (tname, k) = data
        val tname = unBinderName $ visit_tbinder this env $ TBinder tname
        val k = unOuter $ visit_outer (#visit_kind vtable this) env $ Outer k
      in
        T.SpecType (tname, k)
      end
    fun visit_SpecTypeDef this env data =
      let
        val vtable = cast this
        val (tname, t) = data
        val tname = unBinderName $ visit_tbinder this env $ TBinder tname
        val t = unOuter $ visit_outer (#visit_mtype vtable this) env $ Outer t
        val cnames = map (Binder o CName) $ T.get_constr_names t
        val cnames = visit_list (visit_cbinder this) env cnames
      in
        T.SpecTypeDef (tname, t)
      end
    fun visit_mod this env data =
      let
        val vtable = cast this
      in
        case data of
            ModComponents data => #visit_ModComponents vtable this env data
          | ModSeal data => #visit_ModSeal vtable this env data
          | ModTransparentAsc data => #visit_ModTransparentAsc vtable this env data
      end
    fun visit_ModComponents this env data =
      let
        val vtable = cast this
        val (decls, r) = data
        val decls = unTeles $ visit_decls (#visit_decl vtable this) env $ Teles decls
      in
        T.ModComponents (decls, r)
      end
    fun copy_ctx (ctx : 'env ctx) =
      {outer = #outer ctx, current = copy_ref $ #current ctx}
    fun visit_ModSeal this ctx data =
      let
        val vtable = cast this
        val (m, sg) = data
        val ctx' = copy_ctx ctx
        val m = #visit_mod vtable this ctx' m
        val sg = #visit_sgn vtable this ctx sg
      in
        T.ModSeal (m, sg)
      end
    fun visit_ModTransparentAsc this ctx data =
      let
        val vtable = cast this
        val (m, sg) = data
        val ctx' = copy_ctx ctx
        val m = #visit_mod vtable this ctx m
        val sg = #visit_sgn vtable this ctx' sg
      in
        T.ModTransparentAsc (m, sg)
      end
  in
    {
      visit_expr = visit_expr,
      visit_EVar = visit_EVar,
      visit_EConst = visit_EConst,
      visit_EUnOp = visit_EUnOp,
      visit_EBinOp = visit_EBinOp,
      visit_ETriOp = visit_ETriOp,
      visit_EEI = visit_EEI,
      visit_EET = visit_EET,
      visit_ET = visit_ET,
      visit_EAbs = visit_EAbs,
      visit_EAbsI = visit_EAbsI,
      visit_EAppConstr = visit_EAppConstr,
      visit_ECase = visit_ECase,
      visit_ELet = visit_ELet,
      (* visit_ECaseSumbool = visit_ECaseSumbool, *)
      visit_decl = visit_decl,
      visit_DVal = visit_DVal,
      visit_DValPtrn = visit_DValPtrn,
      visit_DRec = visit_DRec,
      visit_DIdxDef = visit_DIdxDef,
      visit_DAbsIdx2 = visit_DAbsIdx2,
      visit_DAbsIdx = visit_DAbsIdx,
      visit_DTypeDef = visit_DTypeDef,
      visit_DConstrDef = visit_DConstrDef,
      visit_DOpen = visit_DOpen,
      
      (* visit_ptrn = visit_ptrn, *)
      (* visit_PnVar = visit_PnVar, *)
      (* visit_PnTT = visit_PnTT, *)
      (* visit_PnPair = visit_PnPair, *)
      (* visit_PnAlias = visit_PnAlias, *)
      (* visit_PnAnno = visit_PnAnno, *)
      (* visit_PnConstr = visit_PnConstr, *)
      
      visit_ptrn = #visit_ptrn pv_vtable,
      visit_PnVar = #visit_PnVar pv_vtable,
      visit_PnTT = #visit_PnTT pv_vtable,
      (* visit_PnPair = #visit_PnPair pv_vtable, *)
      visit_PnAlias = #visit_PnAlias pv_vtable,
      visit_PnAnno = #visit_PnAnno pv_vtable,
      visit_PnConstr = #visit_PnConstr pv_vtable,
      
      visit_sgn = visit_sgn,
      visit_spec = visit_spec,
      visit_mod = visit_mod,
      visit_ty = visit_ty,
      visit_kind = visit_kind,
      visit_SpecVal = visit_SpecVal,
      visit_SpecIdx = visit_SpecIdx,
      visit_SpecType = visit_SpecType,
      visit_SpecTypeDef = visit_SpecTypeDef,
      visit_ModComponents = visit_ModComponents,
      visit_ModSeal = visit_ModSeal,
      visit_ModTransparentAsc = visit_ModTransparentAsc,
      visit_EApp = visit_EApp,
      (* visit_EPair = visit_EPair, *)
      visit_EAdd = visit_EAdd,
      visit_ENatAdd = visit_ENatAdd,
      visit_ENew = visit_ENew,
      visit_ERead = visit_ERead,
      visit_EAppT = visit_EAppT,
      visit_EAsc = visit_EAsc,
      visit_EAppI = visit_EAppI,
      visit_EAscTime = visit_EAscTime,
      visit_var = visit_var,
      visit_cvar = visit_cvar,
      visit_mod_id = visit_mod_id,
      visit_idx = visit_idx,
      visit_sort = visit_sort,
      visit_mtype = visit_mtype,
      visit_ptrn_constr_tag = visit_ptrn_constr_tag,
      extend_i = extend_i,
      extend_t = extend_t,
      extend_c = extend_c,
      extend_e = extend_e
    }
  end

datatype 'env expr_visitor =
         ExprVisitor of ('env expr_visitor, 'env) expr_visitor_interface

fun expr_visitor_impls_interface (this : 'env expr_visitor) :
    ('env expr_visitor, 'env) expr_visitor_interface =
  let
    val ExprVisitor vtable = this
  in
    vtable
  end

fun new_expr_visitor vtable params =
  let
    val vtable = vtable expr_visitor_impls_interface params
  in
    ExprVisitor vtable
  end
    
fun visit_decls' visitor ctx decls =
  let
    val ExprVisitor vtable = visitor
    val decls = visit_decls (#visit_decl vtable visitor) ctx decls
  in
    decls
  end
    
fun visit_decls_list visitor ctx decls =
  let
    val ExprVisitor vtable = visitor
    val decls = unTeles $ visit_decls (#visit_decl vtable visitor) ctx $ Teles decls
  in
    decls
  end
    
fun visit_with_acc f visitor (b, env) =
  let
    val ctx = env2ctx env
    val b = f visitor ctx b
    val env = !(#current ctx)
  in
    (b, env)
  end

fun visit_decl_acc visitor (b, env) =
  let
    val ExprVisitor vtable = visitor
    val (b, env) = visit_with_acc (#visit_decl vtable) visitor (b, env)
  in
    (hd b, env)
  end

fun visit_decls_acc a = visit_with_acc visit_decls' a
fun visit_decls_list_acc a = visit_with_acc visit_decls_list a

fun unExprVisitor (ExprVisitor vtable) = vtable
val get_vtable = unExprVisitor
                   
fun visit_sgn_acc visitor = visit_with_acc (#visit_sgn $ get_vtable visitor) visitor
fun visit_mod_acc visitor = visit_with_acc (#visit_mod $ get_vtable visitor) visitor

(*********** from here to the end: boring record overrides *****************)
    
fun override_visit_PnConstr (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = new,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }
    
fun override_visit_PnVar (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = new,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EVar (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = new,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EBinOp (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = new,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EApp (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = new,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EEI (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = new,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EAppI (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = new,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EAscTime (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = new,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_EAsc (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = new,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_ECase (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = new,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_DRec (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = new,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_DTypeDef (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = new,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_DOpen (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = new,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = #visit_SpecTypeDef record,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

fun override_visit_SpecTypeDef (record : ('this, 'env) expr_visitor_vtable) new : ('this, 'env) expr_visitor_vtable =
  {
    visit_expr = #visit_expr record,
    visit_EVar = #visit_EVar record,
    visit_EConst = #visit_EConst record,
    visit_EUnOp = #visit_EUnOp record,
    visit_EBinOp = #visit_EBinOp record,
    visit_ETriOp = #visit_ETriOp record,
    visit_EEI = #visit_EEI record,
    visit_EET = #visit_EET record,
    visit_ET = #visit_ET record,
    visit_EAbs = #visit_EAbs record,
    visit_EAbsI = #visit_EAbsI record,
    visit_EAppConstr = #visit_EAppConstr record,
    visit_ECase = #visit_ECase record,
    visit_ELet = #visit_ELet record,
    (* visit_ECaseSumbool = #visit_ECaseSumbool record, *)
    visit_EAppT = #visit_EAppT record,
    visit_EAsc = #visit_EAsc record,
    visit_decl = #visit_decl record,
    visit_DVal = #visit_DVal record,
    visit_DValPtrn = #visit_DValPtrn record,
    visit_DRec = #visit_DRec record,
    visit_DIdxDef = #visit_DIdxDef record,
    visit_DAbsIdx2 = #visit_DAbsIdx2 record,
    visit_DAbsIdx = #visit_DAbsIdx record,
    visit_DTypeDef = #visit_DTypeDef record,
    visit_DOpen = #visit_DOpen record,
    visit_DConstrDef = #visit_DConstrDef record,
    visit_ptrn = #visit_ptrn record,
    visit_PnVar = #visit_PnVar record,
    visit_PnTT = #visit_PnTT record,
    (* visit_PnPair = #visit_PnPair record, *)
    visit_PnAlias = #visit_PnAlias record,
    visit_PnConstr = #visit_PnConstr record,
    visit_PnAnno = #visit_PnAnno record,
    visit_sgn = #visit_sgn record,
    visit_spec = #visit_spec record,
    visit_SpecVal = #visit_SpecVal record,
    visit_SpecIdx = #visit_SpecIdx record,
    visit_SpecType = #visit_SpecType record,
    visit_SpecTypeDef = new,
    visit_mod = #visit_mod record,
    visit_ModComponents = #visit_ModComponents record,
    visit_ModSeal = #visit_ModSeal record,
    visit_ModTransparentAsc = #visit_ModTransparentAsc record,
    visit_ty = #visit_ty record,
    visit_kind = #visit_kind record,
    visit_EApp = #visit_EApp record,
    (* visit_EPair = #visit_EPair record, *)
    visit_EAdd = #visit_EAdd record,
    visit_ENatAdd = #visit_ENatAdd record,
    visit_ENew = #visit_ENew record,
    visit_ERead = #visit_ERead record,
    visit_EAppI = #visit_EAppI record,
    visit_EAscTime = #visit_EAscTime record,
    visit_var = #visit_var record,
    visit_cvar = #visit_cvar record,
    visit_mod_id = #visit_mod_id record,
    visit_idx = #visit_idx record,
    visit_sort = #visit_sort record,
    visit_mtype = #visit_mtype record,
    visit_ptrn_constr_tag = #visit_ptrn_constr_tag record,
    extend_i = #extend_i record,
    extend_t = #extend_t record,
    extend_c = #extend_c record,
    extend_e = #extend_e record
  }

end