summaryrefslogtreecommitdiff
path: root/proofs/lfsc_checker/libwriter.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/lfsc_checker/libwriter.cpp')
-rw-r--r--proofs/lfsc_checker/libwriter.cpp238
1 files changed, 238 insertions, 0 deletions
diff --git a/proofs/lfsc_checker/libwriter.cpp b/proofs/lfsc_checker/libwriter.cpp
new file mode 100644
index 000000000..49e9bbaad
--- /dev/null
+++ b/proofs/lfsc_checker/libwriter.cpp
@@ -0,0 +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;
+ }
+}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback