adding disk impl to crashpong1

ivy/ivy_compiler.py

@@ -585,6 +585,8 @@ def compile_native_symbol(arg):
         return ivy_logic.Variable('X',ivy_logic.sig.sorts[name])
     if ivy_logic.is_numeral_name(name):
         return ivy_logic.Symbol(name,ivy_logic.TopS)
+    if name in im.module.hierarchy:
+        return compile_native_name(arg)
     raise iu.IvyError(arg,'{} is not a declared symbol or type'.format(name))
 
 def compile_native_action(self):
@@ -599,6 +601,7 @@ def compile_native_name(atom):
     return ivy_ast.Atom(atom.rep,[ivy_ast.Variable(a.rep,resolve_alias(a.sort)) for a in atom.args])
 
 def compile_native_def(self):
+    iu.dbg('self.args')
     fields = self.args[1].code.split('`')
     args = [compile_native_name(self.args[0]),self.args[1]] + [compile_native_arg(a) if not fields[i*2].endswith('"') else compile_native_symbol(a) for i,a in enumerate(self.args[2:])]
     return self.clone(args)

ivy/ivy_parser.py

@@ -1344,7 +1344,7 @@ def p_top_interpret_symbol_arrow_lcb_symbol_dots_symbol_rcb(p):
 def parse_nativequote(p,n):
     string = p[n][3:-3] # drop the quotation marks
     fields = string.split('`')
-    bqs = [Atom(s) for idx,s in enumerate(fields) if idx % 2 == 1]
+    bqs = [(Atom(This()) if s == 'this' else Atom(s))  for idx,s in enumerate(fields) if idx % 2 == 1]
     text = "`".join([(s if idx % 2 == 0 else str(idx/2)) for idx,s in enumerate(fields)])
     eols = [sum(1 for c in s if c == '\n') for idx,s in enumerate(fields) if idx % 2 == 0]
     seols = 0

ivy/ivy_to_cpp.py

@@ -1776,7 +1776,8 @@ struct ivy_socket_deser : public ivy_binary_deser {
             get = (get < 1024) ? 1024 : get;
             inp.resize(pos + get);
             int bytes;
-	    if ((bytes = recvfrom(sock,&inp[pos],get,0,0,0)) < 0)
+//	    if ((bytes = recvfrom(sock,&inp[pos],get,0,0,0)) < 0)
+	    if ((bytes = read(sock,&inp[pos],get)) < 0)
 		 { std::cerr << "recvfrom failed\\n"; exit(1); }
             inp.resize(pos + bytes);
             if (bytes == 0)
@@ -3262,6 +3263,11 @@ def emit_call(self,header):
 
 ia.CallAction.emit = emit_call
 
+def emit_crash(self,header):
+    pass
+
+ia.CrashAction.emit = emit_crash
+
 def local_start(header,params,nondet_id=None):
     global indent_level
     indent(header)

test/crashpong1.ivy

@@ -13,6 +13,55 @@ module file(data) = {
             ensure d = contents
         }
     }
+    implementation {
+        object fildes = {}
+        <<< member
+            int fildes;
+        >>>
+        <<< init
+            std::string pathname = "`this`.log";
+            int f = ::open(pathname.cstr(),O_RDWR|O_CREAT|O_TRUNC,0666);
+            if (f < 0) {
+                perror("cannot open file to write");
+            }
+            `fildes` = f;
+        >>>
+        implement write {
+        <<<
+            if (::lseek(`fildes`,0,SEEK_SET) < 0) {
+                perror("cannot seek to beginning of file");
+            }
+            ivy_binary_ser sr;
+            __ser(sr,d);
+            if (::write(`fildes`,&sr.res[0],sr.res.size()) < 0) {
+                perror("cannot seek to beginning of file");
+            }
+            if (::ftruncate(`fildes`,&sr.res[0],sr.res.size()) < 0) {
+                perror("cannot truncate file");
+            }
+        >>>
+        }
+        implement read {
+        <<<
+            if (::lseek(`fildes`,0,SEEK_SET) < 0) {
+                perror("cannot seek to beginning of file");
+            }
+            std::vector<char> buf;
+            ivy_socket_deser ds(sock,buf);  // initializer deserializer with zero bytes
+            try {
+                __deser(ds,d);            // read the message
+            } 
+
+            // If file has bad syntax, something really terrible happened so we give up
+
+            catch (deser_err &){
+                std::cerr << "syntax error in log file";
+                exit(1);
+            }
+        >>>
+        }
+    }
+    trusted isolate iso = this 
 }
 
 object intf = {
@@ -115,3 +164,5 @@ export right_player.crash
 
 isolate iso_l = left_player with spec
 isolate iso_r = right_player with spec
+
+extract iso_impl = this