--- 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(){