introduce Row type

makam-spec/src/row.makam

@@ -0,0 +1,95 @@
+row : type -> type.
+
+(* A row is like a set, but extendable on the back,
+ * and lazy, in some sense of lazyness *)
+
+extend : A -> row A -> row A.
+closed : row A.
+
+%extend row.
+(* This map doesn't eagerly instantiate the back of the row *)
+map : (A -> prop) -> row A -> prop.
+map F R :-
+    guard R (ifte (eq (extend X R') R) (and (F X) (map F R')) (eq closed R)).
+
+
+(* An empty, extendable, row *)
+empty : row A -> prop.
+empty A :- refl.isunif A.
+
+(* To close a row, can't use map, must be eager *)
+close : row A -> prop.
+close closed.
+close R :-
+    not (empty R),
+    eq (extend _ R') R,
+    close R'.
+
+lacks : A -> row A -> prop.
+lacks A R :-
+    map (pfun X => not (eqv X A)) R.
+
+(* Notice that member and add are not the same *)
+member : row A -> A -> prop.
+member R A :-
+  not (empty R),
+  eq (extend A' R') R,
+  unless (eqv A A') (member R' A).
+
+add : A -> row A -> prop.
+add A R :-
+    member R A.
+add A R :-
+    empty R,
+    eq (extend A R') R,
+    lacks A R'.
+add A R :-
+    not (empty R),
+    eq (extend A' R') R,
+    not (eqv A A'),
+    add A R'.
+
+remove : A -> row A -> row A -> prop.
+remove A R R' :-
+    member R A,
+    not (empty R),
+    eq (extend A' R'') R,
+    ifte (eqv A A')
+        (eq R' R'')
+        (and (remove A R'' R''') (eq R' (extend A' R'''))).
+
+(* fromList gives you the non-closed version, use close to close it *)
+fromList : list A -> row A -> prop.
+fromList [] R :-
+    empty R.
+fromList (HD :: TL) RTL :-
+    fromList TL RTL,
+    once (add HD RTL). (* TODO, I dont remember why this has once *)
+
+toList : row A -> list A -> prop.
+toList R [] :-
+    empty R.
+toList closed [].
+toList (extend A R) (A :: TL) :-
+    toList R TL.
+
+%end.
+
+(* This disables the builtin eqv relation for rows *)
+without_eqv_refl (_: row A).
+
+(* This unifies their definitions by expanding them *)
+eqv (R: row A) S :-
+    row.empty R, row.empty S, eq R S.
+eqv (R: row A) S :-
+    row.empty R, not (row.empty S), eqv S R.
+eqv (R: row A) S :-
+    not (row.empty R),
+    eq R closed,
+    eq S closed.
+eqv (R: row B) S :-
+    not (row.empty R),
+    eq (extend A R') R,
+    row.add A S, (* If S doesnt have A and it's closed, this line fails *)
+    row.remove A S S',
+    eqv R' S'.

makam-spec/src/testnickel.makam

@@ -1,4 +1,5 @@
 %use "init".
+%use "row".
 
 (* This file defines a bunch of tests across many features
  * of the Makam implementation of the Nickel language.
@@ -365,3 +366,32 @@ testcase nickel :-
     not (raw_interpreter
     "{blop: 3; blop: false}"
     _ _).
+
+(* Rows *)
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.add 3 A,
+    row.member A 2, row.member A 3, not(row.member A 1).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.add 3 A, row.add 2 A,
+    row.toList A [2, 3].
+
+testcase nickel :-
+    row.fromList [1, 2, 3, 1] R,
+    row.member R 1, row.member R 2, row.member R 3,
+    row.remove 1 R A, not(row.member A 1).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.remove 2 A R,
+    not (row.add 2 R).
+
+testcase nickel :-
+    row.empty A, row.add 2 A, row.close A,
+    row.member A 2, not(row.add 3 A), row.add 2 A.
+
+testcase nickel :-
+    row.fromList [1,2 ,3] R, row.close R, row.fromList [1,2] RR, eqv RR R.
+
+testcase nickel :-
+    row.fromList [1,2 ,3] R, row.fromList [1,2] RR, row.close RR, not(eqv RR R).