fix FFI and add an easy execution entry for debugging

Author: arthurpaulino

Ix/Ixon.lean

@@ -264,11 +264,6 @@ inductive MetadatumFFI where
 | all : Array NameFFI -> MetadatumFFI
 | mutCtx : Array (Array NameFFI) -> MetadatumFFI
 
-structure EnvFFI where
-  env : Array (Address × Address)
-
-def Env.toFFI (x: Env) : EnvFFI := .mk x.env.toArray
-
 def Metadatum.toFFI : Metadatum → MetadatumFFI
   | .name n => .name n.toFFI
   | .info i => .info i
@@ -285,10 +280,10 @@ inductive IxonFFI where
 | apps : IxonFFI -> IxonFFI -> Array IxonFFI -> IxonFFI
 | lams : Array IxonFFI -> IxonFFI -> IxonFFI
 | alls : Array IxonFFI -> IxonFFI -> IxonFFI
-| letE : Bool -> IxonFFI -> IxonFFI -> IxonFFI -> IxonFFI
 | proj : Address -> UInt64 -> IxonFFI -> IxonFFI
 | strl : String -> IxonFFI
 | natl : ByteArray -> IxonFFI
+| letE : Bool -> IxonFFI -> IxonFFI -> IxonFFI -> IxonFFI
 | list : Array IxonFFI -> IxonFFI
 | defn : DefinitionFFI -> IxonFFI
 | axio : AxiomFFI -> IxonFFI
@@ -304,7 +299,7 @@ inductive IxonFFI where
 | eval : EvalClaim -> IxonFFI
 | chck : CheckClaim -> IxonFFI
 | comm : Comm -> IxonFFI
-| envn : EnvFFI -> IxonFFI
+| envn : Array (Address × Address) -> IxonFFI
 
 def Ixon.toFFI : Ixon → IxonFFI
   | .vari i => .vari i
@@ -314,10 +309,10 @@ def Ixon.toFFI : Ixon → IxonFFI
   | .apps f a as => .apps f.toFFI a.toFFI (as.map Ixon.toFFI).toArray
   | .lams xs b => .lams (xs.map Ixon.toFFI).toArray b.toFFI
   | .alls xs x => .alls (xs.map Ixon.toFFI).toArray x.toFFI
-  | .letE x v t b => .letE x v.toFFI t.toFFI b.toFFI
   | .proj addr i x => .proj addr i x.toFFI
   | .strl s => .strl s
   | .natl n => .natl (nat2Bytes n)
+  | .letE x v t b => .letE x v.toFFI t.toFFI b.toFFI
   | .list xs => .list (xs.map Ixon.toFFI).toArray
   | .defn d => .defn d.toFFI
   | .axio a => .axio a.toFFI
@@ -335,7 +330,7 @@ def Ixon.toFFI : Ixon → IxonFFI
   | .eval x => .eval x
   | .chck x => .chck x
   | .comm x => .comm x
-  | .envn x => .envn x.toFFI
+  | .envn x => .envn x.env.toArray
 
 end FFI
 

src/lean/ffi/ixon.rs

@@ -57,7 +57,6 @@ fn lean_ctor_to_univ(ctor: &LeanCtorObject) -> Univ {
     }
 }
 
-// FIXME
 fn lean_ptr_to_address(ptr: *const c_void) -> Address {
     let sarray: &LeanSArrayObject = as_ref_unsafe(ptr.cast());
     let hash = Hash::from_slice(sarray.data()).unwrap();
@@ -229,11 +228,9 @@ fn lean_ptr_to_name_parts(ptr: *const c_void) -> Vec<NamePart> {
 }
 
 fn lean_ptr_to_name(ptr: *const c_void) -> Name {
-    let parts = lean_ptr_to_name_parts(ptr);
-    // Is `parts` reversed?
-    Name {
-        parts: parts.into_iter().rev().collect(),
-    }
+    let mut parts = lean_ptr_to_name_parts(ptr);
+    parts.reverse();
+    Name { parts }
 }
 
 fn lean_ptr_to_metadatum(ptr: *const c_void) -> Metadatum {
@@ -301,7 +298,6 @@ fn lean_ptr_to_metadata_entry(ptr: *const c_void) -> (Nat, Vec<Metadatum>) {
     (fst, snd)
 }
 
-// FIXME
 fn lean_ptr_to_env_entry(ptr: *const c_void) -> (Address, Address) {
     let ctor: &LeanCtorObject = as_ref_unsafe(ptr.cast());
     let [fst, snd] = ctor.objs().map(lean_ptr_to_address);
@@ -518,11 +514,8 @@ fn lean_ctor_to_ixon(ctor: &LeanCtorObject) -> Ixon {
             let [secret, payload] = comm.objs().map(lean_ptr_to_address);
             Ixon::Comm(Comm { secret, payload })
         }
-        // FIXME
         26 => {
-            let [env_ptr] = ctor.objs();
-            let env: &LeanCtorObject = as_ref_unsafe(env_ptr.cast());
-            let [map_ptr] = env.objs();
+            let [map_ptr] = ctor.objs();
             let map: &LeanArrayObject = as_ref_unsafe(map_ptr.cast());
             let env = map.to_vec(lean_ptr_to_env_entry);
             Ixon::Envn(Env { env })
@@ -537,7 +530,6 @@ extern "C" fn rs_eq_lean_rust_serialization(
     bytes: &LeanSArrayObject,
 ) -> bool {
     let mut buf = Vec::new();
-    println!("{:?}", lean_ctor_to_ixon(ixon));
     lean_ctor_to_ixon(ixon).put(&mut buf);
     buf == bytes.data()
 }

src/lean/string.rs

@@ -21,7 +21,7 @@ pub struct LeanStringObject {
 impl LeanStringObject {
     #[inline]
     pub fn as_string(&self) -> String {
-        let bytes = self.m_data.slice(self.m_size);
+        let bytes = self.m_data.slice(self.m_size - 1); // Ignore the last '\0'
         unsafe { String::from_utf8_unchecked(bytes.to_vec()) }
     }
 }