HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-08-15 19:30:41 +03:00
Code Issues Packages Projects Releases Wiki Activity

Fix kdl var linearization test

Browse Source
This commit is contained in:
Nicolas Abril 2022-11-30 17:44:02 +01:00
parent ae88843df0
commit b06dd3f64e
2 changed files with 6 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
crates/kind-tests/suite/kdl/LinearizeVars.golden
View File

@ -5,6 +5,6 @@ fun (U120.new hi lo) {
}
fun (TestFunc xs) {
(TestFunc {List.cons ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {List.cons (& (+ x2.0 x3.0) #1152921504606846975) x1.0} #4) x3) (& (+ x2.1 x2.2) #1152921504606846975)) #2) x1)
(TestFunc {List.cons ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {List.cons {U120.add x2.0 x3.0} x1.0} #4) x3) {U120.add x2.1 x2.2}) #2) x1)
}

7
crates/kind-tests/suite/kdl/LinearizeVars.kind2
View File

@ -1,6 +1,9 @@
U120 : Type
U120.new (a: U60) (b: U60) : U120
#kdl_erase
U120.add (a: U120) (b: U120) : U120
List : Type
List.nil : List
List.cons (h: U120) (t: List) : Type
@ -9,6 +12,6 @@ List.cons (h: U120) (t: List) : Type
TestFunc (xs: List) : List
TestFunc (List.cons h t) =
let aa = 2u120
let bb = (+ aa aa)
let bb = (U120.add aa aa)
let cc = 4u120
List.cons (+ aa bb) t
List.cons (U120.add aa bb) t