# HG changeset patch
# User Chengsong
# Date 1555093573 -3600
# Node ID 4868c26268aad49cb871e72a9c062df7473630ff
# Parent  768b833d6230436174b3fdf6ceb90f247ce696ff
test of
retrieve r v = retrieve (bsimp r) (decode bsimp r code v)

diff -r 768b833d6230 -r 4868c26268aa Spiral.scala
--- a/Spiral.scala	Wed Apr 10 17:06:24 2019 +0100
+++ b/Spiral.scala	Fri Apr 12 19:26:13 2019 +0100
@@ -464,6 +464,12 @@
         }
     }
   }
+  /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
+      println(bts)
+      println(cdbts)
+      println("code v = retrieve internalise(r) v if |- v : r")
+    }
+    */
   def retrieve_experience(){
     val rg = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) 
     val st = "abaab"
@@ -471,10 +477,12 @@
     //println(vl)
     val bts = retrieve(rg, vl)
     val cdbts = code(vl)
-    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
+    val simprg = bsimp(rg)
+    val simpbts = retrieve(simprg, decode(erase(simprg), cdbts))
+    if(bts == simpbts){
+      println("retrieve r v = retrieve (bsimp r) (decode bsimp(r) code(v))")
       println(bts)
-      println(cdbts)
-      println("code v = retrieve internalise(r) v if |- v : r")
+      println(simpbts)
     }
   }
   def radical_correctness(){