Parse support for sygus LetGTerm.

4 files changed, 198 insertions, 40 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 45630d2cd..54938a686 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -498,9 +498,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
   bool allow_const = false;
   bool read_syntax = false;
-  int sygus_dt_index;
+  int sygus_dt_index = 0;
   Type sygus_ret;
   std::map< CVC4::Type, CVC4::Type > sygus_to_builtin;
+  std::map< CVC4::Type, CVC4::Expr > sygus_to_builtin_expr;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -620,7 +621,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
-      LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, sygus_to_builtin, allow_const, sygus_ret, -1]+ RPAREN_TOK
+      LPAREN_TOK sygusGTerm[sygus_dt_index, datatypes, sorts, fun, ops, cnames, cargs, sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, allow_const, sygus_ret, -1]+ RPAREN_TOK
       RPAREN_TOK
       { Debug("parser-sygus") << "Making sygus datatypes..." << std::endl;
         for( unsigned i=sygus_dt_index; i<datatypes.size(); i++ ){
@@ -641,7 +642,10 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
         PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars );
       }
       PARSER_STATE->popScope();
-      Debug("parser-sygus") << "Make mutual datatypes..." << std::endl;
+      Debug("parser-sygus") << "Make " << datatypes.size() << " mutual datatypes..." << std::endl;
+      for( unsigned i=0; i<datatypes.size(); i++ ){
+        Debug("parser-sygus") << "  " << i << " : " << datatypes[i].getName() << std::endl;
+      }
       seq = new CommandSequence();
       std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
       seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
@@ -735,7 +739,9 @@ sygusGTerm[int index,
            std::vector< std::vector<CVC4::Expr> >& ops, 
            std::vector< std::vector<std::string> >& cnames, 
            std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, 
-           std::vector<CVC4::Expr>& sygus_vars, std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, bool& allow_const, CVC4::Type& ret, int gtermType]
+           std::vector<CVC4::Expr>& sygus_vars, 
+           std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
+           bool& allow_const, CVC4::Type& ret, int gtermType]
 @declarations {
   std::string name;
   Kind k;
@@ -745,12 +751,17 @@ sygusGTerm[int index,
   std::string sname;
   // 0 builtin operator, 1 defined operator, 2 any constant, 3 any variable, 4 ignore, 5 let, -1 none
   int sub_gtermType = -1;
-  bool sub_allow_const;
+  bool sub_allow_const = false;
   Type sub_ret;
-  int sub_dt_index;
+  int sub_dt_index = -1;
   std::string sub_dname;
   Type null_type;
+  Expr null_expr;
   std::vector< Expr > let_vars;
+  int let_start_index = -1;
+  int let_end_index = -1;
+  int let_end_arg_index = -1;
+  Expr let_func;
 }
   : LPAREN_TOK
     ( builtinOp[k]
@@ -759,31 +770,41 @@ sygusGTerm[int index,
         if( k==CVC4::kind::BITVECTOR_UDIV ){
           k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
         }
-        ops[index].push_back(EXPR_MANAGER->operatorOf(k));
         name = kind::kindToString(k);
         sub_gtermType = 0;
+        ops[index].push_back(EXPR_MANAGER->operatorOf(k));
+        cnames[index].push_back( name );
       }
-      /* TODO
-     | LET_TOK { sub_gtermType = 5; }
-       LPAREN_TOK { PARSER_STATE->pushScope(true); }
-      ( LPAREN_TOK 
+     | LET_TOK LPAREN_TOK { 
+         name = std::string("let");
+         sub_gtermType = 5; 
+         ops[index].push_back( null_expr );
+         cnames[index].push_back( name );
+         cargs[index].push_back( std::vector< CVC4::Type >() );
+         PARSER_STATE->pushScope(true);
+         let_start_index = datatypes.size();
+       }
+       ( LPAREN_TOK 
         symbol[sname,CHECK_NONE,SYM_VARIABLE] 
         sortSymbol[t,CHECK_DECLARED] { 
-          Expr v = PARSER_STATE->mkVar(sname,t); 
+          Expr v = PARSER_STATE->mkBoundVar(sname,t); 
           let_vars.push_back( v ); 
           std::stringstream ss;
-          ss << datatypes[index].getName() << "_let_arg_" << let_vars.size();
+          ss << datatypes[index].getName() << "_let_var_" << let_vars.size();
           sub_dname = ss.str();
           PARSER_STATE->pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs );
           sub_dt_index = datatypes.size()-1;
           sub_ret = null_type;
         } 
-        sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sub_allow_const,sub_ret,sub_gtermType] {
+        sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType] {
           Debug("parser-sygus") << "Process argument #" << let_vars.size() << "..." << std::endl;
-          Type t = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sub_ret );
+          Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
+          cargs[index].back().push_back(tt);
+        }
+        RPAREN_TOK )+ RPAREN_TOK { 
+          let_end_index = datatypes.size();
+          let_end_arg_index = cargs[index].back().size();
         }
-        RPAREN_TOK )+ RPAREN_TOK  
-        */
     | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] 
       { sub_gtermType = 2; allow_const = true;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; }
     | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED]
@@ -800,8 +821,9 @@ sygusGTerm[int index,
           if( k==CVC4::kind::BITVECTOR_UDIV ){
             k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
           }
-          ops[index].push_back(EXPR_MANAGER->operatorOf(k));
           name = kind::kindToString(k);
+          ops[index].push_back(EXPR_MANAGER->operatorOf(k));
+          cnames[index].push_back( name );
           sub_gtermType = 0;
         }else{
           // what is this sygus term trying to accomplish here, if the
@@ -813,17 +835,17 @@ sygusGTerm[int index,
             PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined."));
           }
           ops[index].push_back( PARSER_STATE->getVariable(name) );
+          cnames[index].push_back( name );
           sub_gtermType = 1;
         }
       }
     )
-    { if( sub_gtermType<=1 ){
-        cnames[index].push_back( name );
-      }
-      cargs[index].push_back( std::vector< CVC4::Type >() );
-      Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl;
-      if( !ops[index].empty() ){
-        Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl;
+    { Debug("parser-sygus") << "Read arguments under " << name << ", gtermType = " << sub_gtermType << std::endl;
+      if( sub_gtermType!=5 ){
+        cargs[index].push_back( std::vector< CVC4::Type >() );
+        if( !ops[index].empty()  ){
+          Debug("parser-sygus") << "Operator " << ops[index].back() << std::endl;
+        }
       }
       //add datatype definition for argument
       count++;
@@ -834,10 +856,9 @@ sygusGTerm[int index,
       sub_dt_index = datatypes.size()-1;
       sub_ret = null_type;
     }
-    ( //symbol[sname,CHECK_NONE,SYM_VARIABLE]
-      sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sub_allow_const,sub_ret,sub_gtermType]
+    ( sygusGTerm[sub_dt_index,datatypes,sorts,fun,ops,cnames,cargs,sygus_vars,sygus_to_builtin,sygus_to_builtin_expr,sub_allow_const,sub_ret,sub_gtermType]
       { Debug("parser-sygus") << "Process argument #" << count << "..." << std::endl;
-        Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sub_ret );
+        Type tt = PARSER_STATE->processSygusNestedGTerm( sub_dt_index, sub_dname, datatypes, sorts, ops, cnames, cargs, sygus_to_builtin, sygus_to_builtin_expr, sub_ret );
         cargs[index].back().push_back(tt);
         //add next datatype definition for argument
         count++;
@@ -883,6 +904,19 @@ sygusGTerm[int index,
           }else if( sub_gtermType==4 ){
             //local variable, TODO?
           }
+        }else if( sub_gtermType==5 ){
+          if( (cargs[index].back().size()-let_end_arg_index)!=1 ){
+            PARSER_STATE->parseError(std::string("Must provide single body for let Sygus constructor."));
+          }
+          PARSER_STATE->processSygusLetConstructor( let_vars, index, let_start_index, datatypes, sorts, ops, cnames, cargs, 
+                                                    sygus_vars, sygus_to_builtin, sygus_to_builtin_expr );
+          PARSER_STATE->popScope();
+          //remove datatypes defining body
+          //while( (int)datatypes.size()>let_end_index ){
+          //  Debug("parser-sygus") << "Removing let body datatype " << datatypes[datatypes.size()-1].getName() << std::endl;
+          //  PARSER_STATE->popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs );
+          //}
+          //Debug("parser-sygus") << "Done let body datatypes" << std::endl;
         }else{
           if( cargs[index].back().empty() ){
             PARSER_STATE->parseError(std::string("Must provide argument for Sygus constructor."));
@@ -925,11 +959,9 @@ sygusGTerm[int index,
         cargs[index].push_back( std::vector< CVC4::Type >() );
       }else{
         //prepend function name to base sorts when reading an operator
-        if( gtermType<=1 ){
-          std::stringstream ss;
-          ss << fun << "_" << name;
-          name = ss.str();
-        }
+        std::stringstream ss;
+        ss << fun << "_" << name;
+        name = ss.str();
         if( PARSER_STATE->isDeclared(name, SYM_SORT) ){
           Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl;
           ret = PARSER_STATE->getSort(name);
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 6e5e57355..101e26746 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -649,7 +649,8 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
                                     std::vector< std::vector<CVC4::Expr> >& ops,
                                     std::vector< std::vector<std::string> >& cnames,
                                     std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, Type sub_ret ) {
+                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, 
+                                    std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret ) {
   Type t = sub_ret;
   Debug("parser-sygus") << "Argument is ";
   if( t.isNull() ){
@@ -662,24 +663,36 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     }
     Expr sop = ops[sub_dt_index][0];
     Type curr_t;
-    if( sop.getKind() != kind::BUILTIN && sop.isConst() ){
+    if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || sop.getNumChildren()==0 ) ){
       curr_t = sop.getType();
-      Debug("parser-sygus") << ": it is constant with type " << sop.getType() << std::endl;
+      Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << std::endl;
+      sygus_to_builtin_expr[t] = sop;
+      d_sygus_bound_var_type[sop] = t;
     }else{
       std::vector< Expr > children;
       if( sop.getKind() != kind::BUILTIN ){
         children.push_back( sop );
       }
       for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
-        Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
-        Debug("parser-sygus") << ":  type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
-        children.push_back( mkVar("x", bt) );
+        std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[sub_dt_index][0][i] );
+        if( it==sygus_to_builtin_expr.end() ){
+          Type bt = sygus_to_builtin[cargs[sub_dt_index][0][i]];
+          Debug("parser-sygus") << ":  type elem " << i << " " << cargs[sub_dt_index][0][i] << " " << bt << std::endl;
+          std::stringstream ss;
+          ss << t << "_x_" << i;
+          Expr bv = mkBoundVar(ss.str(), bt);
+          children.push_back( bv );
+          d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i];
+        }else{
+          children.push_back( it->second );
+        }
       }
       Kind sk = sop.getKind() != kind::BUILTIN ? kind::APPLY : getExprManager()->operatorToKind(sop);
       Debug("parser-sygus") << ": operator " << sop << " with " << sop.getKind() << " " << sk << std::endl;
       Expr e = getExprManager()->mkExpr( sk, children );
       Debug("parser-sygus") << ": constructed " << e << ", which has type " << e.getType() << std::endl;
       curr_t = e.getType();
+      sygus_to_builtin_expr[t] = e;
     }
     sorts[sub_dt_index] = curr_t;
     sygus_to_builtin[t] = curr_t;
@@ -693,6 +706,99 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
   return t;
 }
 
+void Smt2::processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
+                                       int index, int start_index,
+                                       std::vector< CVC4::Datatype >& datatypes,
+                                       std::vector< CVC4::Type>& sorts,
+                                       std::vector< std::vector<CVC4::Expr> >& ops,
+                                       std::vector< std::vector<std::string> >& cnames,
+                                       std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                       std::vector<CVC4::Expr>& sygus_vars, 
+                                       std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+                                       std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr ) {
+  std::vector< CVC4::Expr > let_define_args;
+  Expr let_body;
+  int dindex = cargs[index].size()-1;
+  Debug("parser-sygus") << "Process let constructor for datatype " << datatypes[index].getName() << ", #subtypes = " << cargs[index][dindex].size() << std::endl;
+  for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
+    Debug("parser-sygus") << "  " << i << " : " << cargs[index][dindex][i] << std::endl;
+    if( i+1==cargs[index][dindex].size() ){
+      std::map< CVC4::Type, CVC4::Expr >::iterator it = sygus_to_builtin_expr.find( cargs[index][dindex][i] );
+      if( it!=sygus_to_builtin_expr.end() ){
+        let_body = it->second;
+      }else{
+        std::stringstream ss;
+        ss << datatypes[index].getName() << "_body";
+        let_body = mkBoundVar(ss.str(), sygus_to_builtin[cargs[index][dindex][i]]);
+        d_sygus_bound_var_type[let_body] = cargs[index][dindex][i];
+      }
+    }
+  }
+  Debug("parser-sygus") << std::endl;
+  Debug("parser-sygus") << "Body is " << let_body << std::endl;
+  Debug("parser-sygus") << "# let vars = " << let_vars.size() << std::endl;
+  for( unsigned i=0; i<let_vars.size(); i++ ){
+    Debug("parser-sygus") << "  let var " << i << " : " << let_vars[i] << " " << let_vars[i].getType() << std::endl;
+    let_define_args.push_back( let_vars[i] );
+  }
+  Debug("parser-sygus") << "index = " << index << ", start index = " << start_index << ", #Current datatypes = " << datatypes.size() << std::endl;
+  for( unsigned i=start_index; i<datatypes.size(); i++ ){
+    Debug("parser-sygus") << "  datatype " << i << " : " << datatypes[i].getName() << ", #cons = " << cargs[i].size() << std::endl;
+    if( !cargs[i].empty() ){
+      Debug("parser-sygus") << "  operator 0 is " << ops[i][0] << std::endl;
+      Debug("parser-sygus") << "  cons 0 has " << cargs[i][0].size() << " sub fields." << std::endl;
+      for( unsigned j=0; j<cargs[i][0].size(); j++ ){
+        Type bt = sygus_to_builtin[cargs[i][0][j]];
+        Debug("parser-sygus") << "    cons 0, selector " << j << " : " << cargs[i][0][j] << " " << bt << std::endl;
+      }
+    }
+  } 
+  //last argument is the return, pop
+  cargs[index][dindex].pop_back();
+  collectSygusLetArgs( let_body, cargs[index][dindex], let_define_args );  
+  
+  Debug("parser-sygus") << "Make define-fun with " << cargs[index][dindex].size() << " arguments..." << std::endl;
+  std::vector<CVC4::Type> fsorts;
+  for( unsigned i=0; i<cargs[index][dindex].size(); i++ ){
+    Debug("parser-sygus") << "  " << i << " : " << let_define_args[i] << " " << let_define_args[i].getType() << " " << cargs[index][dindex][i] << std::endl;
+    fsorts.push_back(let_define_args[i].getType());
+  }
+  
+  Type ft = getExprManager()->mkFunctionType(fsorts, let_body.getType());
+  std::stringstream ss;
+  ss << datatypes[index].getName() << "_let";
+  Expr let_func = mkFunction(ss.str(), ft, ExprManager::VAR_FLAG_DEFINED);
+  preemptCommand( new DefineFunctionCommand(ss.str(), let_func, let_define_args, let_body) );
+  
+  ops[index].pop_back();
+  ops[index].push_back( let_func );
+  cnames[index].pop_back();
+  cnames[index].push_back(ss.str());
+  
+  //TODO : mark function as let constructor
+  d_sygus_let_func_to_vars[let_func].insert( d_sygus_let_func_to_vars[let_func].end(), let_vars.begin(), let_vars.end() );
+  d_sygus_let_func_to_body[let_func] = let_body;
+}
+
+
+void Smt2::collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs ) {
+  if( e.getKind()==kind::BOUND_VARIABLE ){
+    if( std::find( builtinArgs.begin(), builtinArgs.end(), e )==builtinArgs.end() ){
+      builtinArgs.push_back( e );
+      sygusArgs.push_back( d_sygus_bound_var_type[e] );
+      if( d_sygus_bound_var_type[e].isNull() ){
+        std::stringstream ss;
+        ss << "While constructing body of let gterm, can't map " << e << " to sygus type." << std::endl;
+        parseError(ss.str());
+      }
+    }
+  }else{
+    for( unsigned i=0; i<e.getNumChildren(); i++ ){
+      collectSygusLetArgs( e[i], sygusArgs, builtinArgs );      
+    } 
+  }
+}
+
 
 void Smt2::defineSygusFuns() {
   // only define each one once
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 166f15640..6781fec95 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -201,8 +201,21 @@ public:
                                 std::vector< std::vector<CVC4::Expr> >& ops,
                                 std::vector< std::vector<std::string> >& cnames,
                                 std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                                std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, Type sub_ret );
+                                std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+                                std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, Type sub_ret );
 
+  void processSygusLetConstructor( std::vector< CVC4::Expr >& let_vars,
+                                   int index, int start_index,
+                                   std::vector< CVC4::Datatype >& datatypes,
+                                   std::vector< CVC4::Type>& sorts,
+                                   std::vector< std::vector<CVC4::Expr> >& ops,
+                                   std::vector< std::vector<std::string> >& cnames,
+                                   std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
+                                   std::vector<CVC4::Expr>& sygus_vars, 
+                                   std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
+                                   std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
+  
+  
   void addSygusFun(const std::string& fun, Expr eval) {
     d_sygusFuns.push_back(std::make_pair(fun, eval));
   }
@@ -285,6 +298,11 @@ public:
   }
 
 private:
+  std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
+  std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;
+  std::map< CVC4::Expr, CVC4::Expr > d_sygus_let_func_to_body;
+  
+  void collectSygusLetArgs( CVC4::Expr e, std::vector< CVC4::Type >& sygusArgs, std::vector< CVC4::Expr >& builtinArgs );
 
   void addArithmeticOperators();
 
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 1082bed23..d57f52b35 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1612,6 +1612,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn ) {
 
 Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs ) {
   return n;
+  /*  TODO?
   if( n.getKind()==SKOLEM ){
     std::map< Node, Node >::iterator its = subs.find( n );
     if( its!=subs.end() ){
@@ -1644,6 +1645,7 @@ Node TermDbSygus::getSygusNormalized( Node n, std::map< TypeNode, int >& var_cou
     }
     return n;
   }
+  */
 }
 
 Node TermDbSygus::getNormalized( TypeNode t, Node prog, bool do_pre_norm, bool do_post_norm ) {