diff options
Diffstat (limited to 'proofs/lfsc_checker/libwriter.cpp')
-rw-r--r-- | proofs/lfsc_checker/libwriter.cpp | 476 |
1 files changed, 238 insertions, 238 deletions
diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp index 49e9bbaad..016016c9d 100644 --- a/proofs/lfsc_checker/libwriter.cpp +++ b/proofs/lfsc_checker/libwriter.cpp @@ -1,238 +1,238 @@ -#include "libwriter.h"
-#include <sstream>
-#include <algorithm>
-#include <fstream>
-
-void libwriter::get_var_name( const std::string& n, std::string& nn ) {
- nn = std::string( n.c_str() );
- for( int i = 0; i <(int)n.length(); i++ ){
- char c = n[i];
- if (c <= 47)
- c += 65;
- else if (c >= 58 && c <= 64)
- c += 97-58;
- if ((c >= 91 && c <= 94) || c == 96)
- c += 104-91;
- else if (c >= 123)
- c -= 4;
- nn[i] = c;
- }
-}
-
-void libwriter::write_file()
-{
- //std::cout << "write lib" << std::endl;
- std::ostringstream os_enum;
- std::ostringstream os_print;
- std::ostringstream os_constructor_h;
- std::ostringstream os_constructor_c;
-
- for ( int a=0; a<(int)syms.size(); a++ ) {
- //std::cout << "sym #" << (a+1) << ": ";
- //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl;
- //defs[a]->print( std::cout );
- //std::cout << std::endl;
-
- if( defs[a]->getclass()==CEXPR ){
- //calculate which arguments are required for input
- std::vector< Expr* > args;
- std::vector< bool > argsNeed;
- std::vector< Expr* > argTypes;
- CExpr* c = ((CExpr*)defs[a]);
- while( c->getop()==PI ){
- //std::cout << c->kids[0] << std::endl;
- if( ((CExpr*)c->kids[1])->getop()!=RUN ){
- args.push_back( c->kids[0] );
- argsNeed.push_back( true );
- argTypes.push_back( c->kids[1] );
- }
- for( int b=0; b<(int)args.size(); b++ ){
- if( argsNeed[b] ){
- if( ((CExpr*)c->kids[1])->getop()==RUN ){
- if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){
- argsNeed[b] = false;
- }
- }else{
- if( c->kids[1]->free_in( args[b] ) ){
- argsNeed[b] = false;
- }
- }
- }
- }
- c = (CExpr*)(c->kids[2]);
- }
-
- //record if this declares a judgement
- if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){
- //std::cout << "This is a judgement" << std::endl;
- judgements.push_back( syms[a] );
- //record if this declares a proof rule
- }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){
- std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl;
- //std::cout << "These are required to input:" << std::endl;
- //for( int b=0; b<(int)args.size(); b++ ){
- // if( argsNeed[b] ){
- // std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl;
- // }
- //}
- os_enum << " rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl;
-
- os_print << " case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \"";
- os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl;
-
- std::ostringstream os_args;
- os_args << "(";
- bool firstTime = true;
- for( int b=0; b<(int)args.size(); b++ ){
- if( argsNeed[b] ){
- if( !firstTime )
- os_args << ",";
- std::string str;
- get_var_name( ((SymSExpr*)args[b])->s, str );
- os_args << " LFSCProof* " << str.c_str();
- firstTime = false;
- }
- }
- if( !firstTime ){
- os_args << " ";
- }
- os_args << ")";
-
- os_constructor_h << " static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str();
- os_constructor_h << os_args.str().c_str() << ";" << std::endl;
-
- os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str();
- os_constructor_c << os_args.str().c_str() << "{" << std::endl;
- os_constructor_c << " LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl;
- for( int b=0; b<(int)args.size(); b++ ){
- os_constructor_c << " kids[" << b << "] = ";
- if( argsNeed[b] ){
- std::string str;
- get_var_name( ((SymSExpr*)args[b])->s, str );
- os_constructor_c << str.c_str();
- }else{
- os_constructor_c << "hole";
- }
- os_constructor_c << ";" << std::endl;
- }
- os_constructor_c << " kids[" << (int)args.size() << "] = 0;" << std::endl;
- os_constructor_c << " return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl;
- os_constructor_c << "}" << std::endl << std::endl;
- }
- }
-
- //write the header
- static std::string filename( "lfsc_proof" );
- std::fstream fsh;
- std::string fnameh( filename );
- fnameh.append(".h");
- fsh.open( fnameh.c_str(), std::ios::out );
-
- fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl;
- fsh << "#define LFSC_PROOF_LIB_H" << std::endl;
- fsh << std::endl;
- fsh << "#include <string>" << std::endl;
- fsh << std::endl;
- fsh << "class LFSCProof{" << std::endl;
- fsh << "protected:" << std::endl;
- fsh << " enum{" << std::endl;
- fsh << os_enum.str().c_str();
- fsh << " };" << std::endl;
- fsh << " static LFSCProof* hole;" << std::endl;
- fsh << " LFSCProof(){}" << std::endl;
- fsh << "public:" << std::endl;
- fsh << " virtual ~LFSCProof(){}" << std::endl;
- fsh << " static void init();" << std::endl;
- fsh << std::endl;
- fsh << " //functions to build LFSC proofs" << std::endl;
- fsh << os_constructor_h.str().c_str();
- fsh << std::endl;
- fsh << " virtual void set_child( int i, LFSCProof* e ) {}" << std::endl;
- fsh << " virtual void print( std::ostream& os ){}" << std::endl;
- fsh << "};" << std::endl;
- fsh << std::endl;
- fsh << "class LFSCProofC : public LFSCProof{" << std::endl;
- fsh << " short id;" << std::endl;
- fsh << " LFSCProof **kids;" << std::endl;
- fsh << "public:" << std::endl;
- fsh << " LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl;
- fsh << " void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl;
- fsh << " void print( std::ostream& os );" << std::endl;
- fsh << "};" << std::endl;
- fsh << std::endl;
- fsh << "class LFSCProofSym : public LFSCProof{" << std::endl;
- fsh << "private:" << std::endl;
- fsh << " std::string s;" << std::endl;
- fsh << " LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl;
- fsh << "public:" << std::endl;
- fsh << " static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl;
- fsh << " static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl;
- fsh << " ~LFSCProofSym(){}" << std::endl;
- fsh << " void print( std::ostream& os ) { os << s.c_str(); }" << std::endl;
- fsh << "};" << std::endl;
- fsh << std::endl;
- fsh << "class LFSCProofLam : public LFSCProof{" << std::endl;
- fsh << " LFSCProofSym* var;" << std::endl;
- fsh << " LFSCProof* body;" << std::endl;
- fsh << " LFSCProof* typ;" << std::endl;
- fsh << " LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl;
- fsh << "public:" << std::endl;
- fsh << " static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl;
- fsh << " return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl;
- fsh << " }" << std::endl;
- fsh << " ~LFSCProofLam(){}" << std::endl;
- fsh << std::endl;
- fsh << " void print( std::ostream& os );" << std::endl;
- fsh << "};" << std::endl;
- fsh << std::endl;
- fsh << "#endif" << std::endl;
-
- //write the cpp
- std::fstream fsc;
- std::string fnamec( filename );
- fnamec.append(".cpp");
- fsc.open( fnamec.c_str(), std::ios::out );
-
- fsc << "#include \"lfsc_proof.h\"" << std::endl;
- fsc << std::endl;
- fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl;
- fsc << std::endl;
- fsc << "void LFSCProof::init(){" << std::endl;
- fsc << " hole = LFSCProofSym::make( \"_\" );" << std::endl;
- fsc << "}" << std::endl;
- fsc << std::endl;
- fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl;
- fsc << " os << \"(\";" << std::endl;
- fsc << " switch( id ){" << std::endl;
- fsc << os_print.str().c_str();
- fsc << " }" << std::endl;
- fsc << " int counter = 0;" << std::endl;
- fsc << " while( kids[counter] ){" << std::endl;
- fsc << " os << \" \";" << std::endl;
- fsc << " kids[counter]->print( os );" << std::endl;
- fsc << " counter++;" << std::endl;
- fsc << " }" << std::endl;
- fsc << " os << \")\";" << std::endl;
- fsc << "}" << std::endl;
- fsc << std::endl;
- fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl;
- fsc << " os << \"(\";" << std::endl;
- fsc << " if( typ ){" << std::endl;
- fsc << " os << \"% \";" << std::endl;
- fsc << " }else{" << std::endl;
- fsc << " os << \"\\\\ \";" << std::endl;
- fsc << " }" << std::endl;
- fsc << " var->print( os );" << std::endl;
- fsc << " if( typ ){" << std::endl;
- fsc << " os << \" \";" << std::endl;
- fsc << " typ->print( os );" << std::endl;
- fsc << " }" << std::endl;
- fsc << " os << std::endl;" << std::endl;
- fsc << " body->print( os );" << std::endl;
- fsc << " os << \")\";" << std::endl;
- fsc << "}" << std::endl;
- fsc << std::endl;
- fsc << os_constructor_c.str().c_str();
- fsc << std::endl;
- }
-}
+#include "libwriter.h" +#include <sstream> +#include <algorithm> +#include <fstream> + +void libwriter::get_var_name( const std::string& n, std::string& nn ) { + nn = std::string( n.c_str() ); + for( int i = 0; i <(int)n.length(); i++ ){ + char c = n[i]; + if (c <= 47) + c += 65; + else if (c >= 58 && c <= 64) + c += 97-58; + if ((c >= 91 && c <= 94) || c == 96) + c += 104-91; + else if (c >= 123) + c -= 4; + nn[i] = c; + } +} + +void libwriter::write_file() +{ + //std::cout << "write lib" << std::endl; + std::ostringstream os_enum; + std::ostringstream os_print; + std::ostringstream os_constructor_h; + std::ostringstream os_constructor_c; + + for ( int a=0; a<(int)syms.size(); a++ ) { + //std::cout << "sym #" << (a+1) << ": "; + //std::cout << ((SymSExpr*)syms[a])->s.c_str() << std::endl; + //defs[a]->print( std::cout ); + //std::cout << std::endl; + + if( defs[a]->getclass()==CEXPR ){ + //calculate which arguments are required for input + std::vector< Expr* > args; + std::vector< bool > argsNeed; + std::vector< Expr* > argTypes; + CExpr* c = ((CExpr*)defs[a]); + while( c->getop()==PI ){ + //std::cout << c->kids[0] << std::endl; + if( ((CExpr*)c->kids[1])->getop()!=RUN ){ + args.push_back( c->kids[0] ); + argsNeed.push_back( true ); + argTypes.push_back( c->kids[1] ); + } + for( int b=0; b<(int)args.size(); b++ ){ + if( argsNeed[b] ){ + if( ((CExpr*)c->kids[1])->getop()==RUN ){ + if( ((CExpr*)c->kids[1])->kids[1]->free_in( args[b] ) ){ + argsNeed[b] = false; + } + }else{ + if( c->kids[1]->free_in( args[b] ) ){ + argsNeed[b] = false; + } + } + } + } + c = (CExpr*)(c->kids[2]); + } + + //record if this declares a judgement + if( ((CExpr*)defs[a])->getop()==PI && c->getop()==TYPE ){ + //std::cout << "This is a judgement" << std::endl; + judgements.push_back( syms[a] ); + //record if this declares a proof rule + }else if( c->getclass()==CEXPR && std::find( judgements.begin(), judgements.end(), c->kids[0] )!=judgements.end() ){ + std::cout << "Handle rule: " << ((SymSExpr*)syms[a])->s.c_str() << std::endl; + //std::cout << "These are required to input:" << std::endl; + //for( int b=0; b<(int)args.size(); b++ ){ + // if( argsNeed[b] ){ + // std::cout << ((SymSExpr*)args[b])->s.c_str() << std::endl; + // } + //} + os_enum << " rule_" << ((SymSExpr*)syms[a])->s.c_str() << "," << std::endl; + + os_print << " case rule_" << ((SymSExpr*)syms[a])->s.c_str() << ": os << \""; + os_print << ((SymSExpr*)syms[a])->s.c_str() << "\";break;" << std::endl; + + std::ostringstream os_args; + os_args << "("; + bool firstTime = true; + for( int b=0; b<(int)args.size(); b++ ){ + if( argsNeed[b] ){ + if( !firstTime ) + os_args << ","; + std::string str; + get_var_name( ((SymSExpr*)args[b])->s, str ); + os_args << " LFSCProof* " << str.c_str(); + firstTime = false; + } + } + if( !firstTime ){ + os_args << " "; + } + os_args << ")"; + + os_constructor_h << " static LFSCProof* make_" << ((SymSExpr*)syms[a])->s.c_str(); + os_constructor_h << os_args.str().c_str() << ";" << std::endl; + + os_constructor_c << "LFSCProof* LFSCProof::make_" << ((SymSExpr*)syms[a])->s.c_str(); + os_constructor_c << os_args.str().c_str() << "{" << std::endl; + os_constructor_c << " LFSCProof **kids = new LFSCProof *[" << (int)args.size()+1 << "];" << std::endl; + for( int b=0; b<(int)args.size(); b++ ){ + os_constructor_c << " kids[" << b << "] = "; + if( argsNeed[b] ){ + std::string str; + get_var_name( ((SymSExpr*)args[b])->s, str ); + os_constructor_c << str.c_str(); + }else{ + os_constructor_c << "hole"; + } + os_constructor_c << ";" << std::endl; + } + os_constructor_c << " kids[" << (int)args.size() << "] = 0;" << std::endl; + os_constructor_c << " return new LFSCProofC( rule_" << ((SymSExpr*)syms[a])->s.c_str() << ", kids );" << std::endl; + os_constructor_c << "}" << std::endl << std::endl; + } + } + + //write the header + static std::string filename( "lfsc_proof" ); + std::fstream fsh; + std::string fnameh( filename ); + fnameh.append(".h"); + fsh.open( fnameh.c_str(), std::ios::out ); + + fsh << "#ifndef LFSC_PROOF_LIB_H" << std::endl; + fsh << "#define LFSC_PROOF_LIB_H" << std::endl; + fsh << std::endl; + fsh << "#include <string>" << std::endl; + fsh << std::endl; + fsh << "class LFSCProof{" << std::endl; + fsh << "protected:" << std::endl; + fsh << " enum{" << std::endl; + fsh << os_enum.str().c_str(); + fsh << " };" << std::endl; + fsh << " static LFSCProof* hole;" << std::endl; + fsh << " LFSCProof(){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " virtual ~LFSCProof(){}" << std::endl; + fsh << " static void init();" << std::endl; + fsh << std::endl; + fsh << " //functions to build LFSC proofs" << std::endl; + fsh << os_constructor_h.str().c_str(); + fsh << std::endl; + fsh << " virtual void set_child( int i, LFSCProof* e ) {}" << std::endl; + fsh << " virtual void print( std::ostream& os ){}" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofC : public LFSCProof{" << std::endl; + fsh << " short id;" << std::endl; + fsh << " LFSCProof **kids;" << std::endl; + fsh << "public:" << std::endl; + fsh << " LFSCProofC( short d_id, LFSCProof **d_kids ) : id( d_id ), kids( d_kids ){}" << std::endl; + fsh << " void set_child( int i, LFSCProof* e ) { kids[i] = e; }" << std::endl; + fsh << " void print( std::ostream& os );" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofSym : public LFSCProof{" << std::endl; + fsh << "private:" << std::endl; + fsh << " std::string s;" << std::endl; + fsh << " LFSCProofSym( std::string ss ) : s( ss ){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " static LFSCProofSym* make( std::string ss ) { return new LFSCProofSym( ss ); }" << std::endl; + fsh << " static LFSCProofSym* make( const char* ss ) { return new LFSCProofSym( std::string( ss ) ); }" << std::endl; + fsh << " ~LFSCProofSym(){}" << std::endl; + fsh << " void print( std::ostream& os ) { os << s.c_str(); }" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "class LFSCProofLam : public LFSCProof{" << std::endl; + fsh << " LFSCProofSym* var;" << std::endl; + fsh << " LFSCProof* body;" << std::endl; + fsh << " LFSCProof* typ;" << std::endl; + fsh << " LFSCProofLam( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ ) : var( d_var ), body( d_body ), typ( d_typ ){}" << std::endl; + fsh << "public:" << std::endl; + fsh << " static LFSCProof* make( LFSCProofSym* d_var, LFSCProof* d_body, LFSCProof* d_typ = NULL ) {" << std::endl; + fsh << " return new LFSCProofLam( d_var, d_body, d_typ );" << std::endl; + fsh << " }" << std::endl; + fsh << " ~LFSCProofLam(){}" << std::endl; + fsh << std::endl; + fsh << " void print( std::ostream& os );" << std::endl; + fsh << "};" << std::endl; + fsh << std::endl; + fsh << "#endif" << std::endl; + + //write the cpp + std::fstream fsc; + std::string fnamec( filename ); + fnamec.append(".cpp"); + fsc.open( fnamec.c_str(), std::ios::out ); + + fsc << "#include \"lfsc_proof.h\"" << std::endl; + fsc << std::endl; + fsc << "LFSCProof* LFSCProof::hole = NULL;" << std::endl; + fsc << std::endl; + fsc << "void LFSCProof::init(){" << std::endl; + fsc << " hole = LFSCProofSym::make( \"_\" );" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << "void LFSCProofC::print( std::ostream& os ){" << std::endl; + fsc << " os << \"(\";" << std::endl; + fsc << " switch( id ){" << std::endl; + fsc << os_print.str().c_str(); + fsc << " }" << std::endl; + fsc << " int counter = 0;" << std::endl; + fsc << " while( kids[counter] ){" << std::endl; + fsc << " os << \" \";" << std::endl; + fsc << " kids[counter]->print( os );" << std::endl; + fsc << " counter++;" << std::endl; + fsc << " }" << std::endl; + fsc << " os << \")\";" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << "void LFSCProofLam::print( std::ostream& os ){" << std::endl; + fsc << " os << \"(\";" << std::endl; + fsc << " if( typ ){" << std::endl; + fsc << " os << \"% \";" << std::endl; + fsc << " }else{" << std::endl; + fsc << " os << \"\\\\ \";" << std::endl; + fsc << " }" << std::endl; + fsc << " var->print( os );" << std::endl; + fsc << " if( typ ){" << std::endl; + fsc << " os << \" \";" << std::endl; + fsc << " typ->print( os );" << std::endl; + fsc << " }" << std::endl; + fsc << " os << std::endl;" << std::endl; + fsc << " body->print( os );" << std::endl; + fsc << " os << \")\";" << std::endl; + fsc << "}" << std::endl; + fsc << std::endl; + fsc << os_constructor_c.str().c_str(); + fsc << std::endl; + } +} |