Skip to content

Instantly share code, notes, and snippets.

@AHartNtkn

AHartNtkn/qs_hylo.pir Secret

Created March 15, 2023 01:06
Show Gist options
  • Save AHartNtkn/1b69a3000c57de3e3ab21e08fbc4667e to your computer and use it in GitHub Desktop.
Save AHartNtkn/1b69a3000c57de3e3ab21e08fbc4667e to your computer and use it in GitHub Desktop.
Download ZIP
Fully compiled quicksort hylomorphism in Vamp-IR
Raw
qs_hylo.pir
def inl x l r = l x;
def inr x l r = r x;
def emptyEq a b = 0;
def unitEq a b = 1;
def prodEq eqX eqY (x1, y1) (x2, y2) = eqX x1 x2 * eqY y1 y2;
def sumEq eqX eqY a b = a (fun x1 { b (fun x2 { eqX x1 x2 }) (fun y2 { 0 }) })
(fun y1 { b (fun x2 { 0 }) (fun y2 { eqY y1 y2 }) });
def isZero x = {
def xi = fresh (1 | x);
x * (1 - xi * x) = 0;
1 - xi * x
};
def intEq a b = isZero (a - b);
def isBool x = (x * (1 - x) = 0);
def decomp4 x = {
def x0 = fresh ((x\2^0) % 2); isBool x0;
def x1 = fresh ((x\2^1) % 2); isBool x1;
def x2 = fresh ((x\2^2) % 2); isBool x2;
def x3 = fresh ((x\2^3) % 2); isBool x3;
x = x0 + 2*x1 + 2^2*x2 + 2^3*x3 ;
(x0, x1, x2, x3)
};
def intDecomp4 x = {
decomp4 (x + 2^3)
};
def isNegative4 a = {
def (a0, a1, a2, a3) = intDecomp4 a;
1 - a3
};
def less4 a b = isNegative4 (a - b);
def listEq = (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq (sumEq unitEq (prodEq intEq emptyEq))))))))))))))))))))));
def or b1 b2 = 1 - (1 - b1) * (1 - b2);
def filterAlgCheck p a (b1, b2) =
a (fun x { listEq b1 (inl 0) * listEq b2 (inl 0) })
(fun (h, (a1, a2)) {
or (less4 h p * listEq (inr (h, a1)) b1 * listEq a2 b2)
((1 - less4 h p) * listEq a1 b1 * listEq (inr (h, a2)) b2)
});
def concatAlgCheck p a b =
a (fun x { listEq p b })
(fun (n, l) { listEq (inr (n, l)) b });
(listEq (inl 0) (inl 0)) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl termStr[tt]) (inl termStr[tt])) = 1;
(concatAlgCheck (inr (0, (inr (1, (inr (2, (inr (3, (inl 0))))))))) (inl termStr[tt]) (inr (0, (inr (1, (inr (2, (inr (3, (inl 0)))))))))) = 1;
(listEq (inr (0, (inr (1, (inr (2, (inr (3, (inl 0))))))))) (inr (0, (inr (1, (inr (2, (inr (3, (inl 0)))))))))) = 1;
(concatAlgCheck (inr (1, (inl 0))) (inl termStr[tt]) (inr (1, (inl 0)))) = 1;
(listEq (inr (1, (inl 0))) (inr (1, (inl 0)))) = 1;
(concatAlgCheck (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))) (inl termStr[tt]) (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))) = 1;
(listEq (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))) (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))) = 1;
(concatAlgCheck (inr (6, (inl 0))) (inl termStr[tt]) (inr (6, (inl 0)))) = 1;
(listEq (inr (6, (inl 0))) (inr (6, (inl 0)))) = 1;
(concatAlgCheck (inr (8, (inl 0))) (inl termStr[tt]) (inr (8, (inl 0)))) = 1;
(listEq (inr (8, (inl 0))) (inr (8, (inl 0)))) = 1;
(filterAlgCheck 1 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (1, (inl 0), (inl 0))) (inl (1, (inl 0), (inl 0)))) = 1;
(filterAlgCheck 6 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (6, (inl 0), (inl 0))) (inl (6, (inl 0), (inl 0)))) = 1;
(filterAlgCheck 8 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (8, (inl 0), (inl 0))) (inl (8, (inl 0), (inl 0)))) = 1;
(concatAlgCheck (inr (2, (inl 0))) (inl termStr[tt]) (inr (2, (inl 0)))) = 1;
(concatAlgCheck (inr (2, (inl 0))) (inl (1, (inr (2, (inl 0))))) (inr (1, (inr (2, (inl 0)))))) = 1;
(listEq (inr (1, (inr (2, (inl 0))))) (inr (1, (inr (2, (inl 0)))))) = 1;
(concatAlgCheck (inr (7, (inr (8, (inl 0))))) (inl termStr[tt]) (inr (7, (inr (8, (inl 0)))))) = 1;
(concatAlgCheck (inr (7, (inr (8, (inl 0))))) (inl (6, (inr (7, (inr (8, (inl 0))))))) (inr (6, (inr (7, (inr (8, (inl 0)))))))) = 1;
(listEq (inr (6, (inr (7, (inr (8, (inl 0))))))) (inr (6, (inr (7, (inr (8, (inl 0)))))))) = 1;
(filterAlgCheck 2 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 2 (inl (1, (inl 0), (inl 0))) ((inr (1, (inl 0))), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (2, (inr (1, (inl 0))), (inl 0))) (inl (2, (inr (1, (inl 0))), (inl 0)))) = 1;
(concatAlgCheck (inr (3, (inl 0))) (inl termStr[tt]) (inr (3, (inl 0)))) = 1;
(concatAlgCheck (inr (3, (inl 0))) (inl (1, (inr (2, (inr (3, (inl 0))))))) (inr (1, (inr (2, (inr (3, (inl 0)))))))) = 1;
(concatAlgCheck (inr (3, (inl 0))) (inl (2, (inr (3, (inl 0))))) (inr (2, (inr (3, (inl 0)))))) = 1;
(listEq (inr (1, (inr (2, (inr (3, (inl 0))))))) (inr (1, (inr (2, (inr (3, (inl 0)))))))) = 1;
(filterAlgCheck 3 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 3 (inl (1, (inl 0), (inl 0))) ((inr (1, (inl 0))), (inl 0))) = 1;
(filterAlgCheck 3 (inl (2, (inr (1, (inl 0))), (inl 0))) ((inr (2, (inr (1, (inl 0))))), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (3, (inr (2, (inr (1, (inl 0))))), (inl 0))) (inl (3, (inr (2, (inr (1, (inl 0))))), (inl 0)))) = 1;
(filterAlgCheck 7 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 7 (inl (6, (inl 0), (inl 0))) ((inr (6, (inl 0))), (inl 0))) = 1;
(filterAlgCheck 7 (inl (8, (inr (6, (inl 0))), (inl 0))) ((inr (6, (inl 0))), (inr (8, (inl 0))))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (7, (inr (6, (inl 0))), (inr (8, (inl 0))))) (inl (7, (inr (6, (inl 0))), (inr (8, (inl 0)))))) = 1;
(filterAlgCheck 0 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 0 (inl (1, (inl 0), (inl 0))) ((inl 0), (inr (1, (inl 0))))) = 1;
(filterAlgCheck 0 (inl (2, (inl 0), (inr (1, (inl 0))))) ((inl 0), (inr (2, (inr (1, (inl 0))))))) = 1;
(filterAlgCheck 0 (inl (3, (inl 0), (inr (2, (inr (1, (inl 0))))))) ((inl 0), (inr (3, (inr (2, (inr (1, (inl 0))))))))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (0, (inl 0), (inr (3, (inr (2, (inr (1, (inl 0))))))))) (inl (0, (inl 0), (inr (3, (inr (2, (inr (1, (inl 0)))))))))) = 1;
(filterAlgCheck 5 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 5 (inl (6, (inl 0), (inl 0))) ((inl 0), (inr (6, (inl 0))))) = 1;
(filterAlgCheck 5 (inl (7, (inl 0), (inr (8, (inr (6, (inl 0))))))) ((inl 0), (inr (7, (inr (8, (inr (6, (inl 0))))))))) = 1;
(filterAlgCheck 5 (inl (8, (inl 0), (inr (6, (inl 0))))) ((inl 0), (inr (8, (inr (6, (inl 0))))))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (5, (inl 0), (inr (7, (inr (8, (inr (6, (inl 0))))))))) (inl (5, (inl 0), (inr (7, (inr (8, (inr (6, (inl 0)))))))))) = 1;
(concatAlgCheck (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))) (inl termStr[tt]) (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))) = 1;
(concatAlgCheck (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))) (inl (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))))))))))) (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))))))))))) = 1;
(concatAlgCheck (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))) (inl (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))))))))) (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))))))))) = 1;
(concatAlgCheck (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))) (inl (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))))))) (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))))))) = 1;
(concatAlgCheck (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))) (inl (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))))) (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))))) = 1;
(listEq (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0))))))))))))))))))) (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inl 0)))))))))))))))))))) = 1;
(filterAlgCheck 4 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 4 (inl (0, (inr (3, (inr (2, (inr (1, (inl 0))))))), (inr (5, (inr (7, (inr (8, (inr (6, (inl 0))))))))))) ((inr (0, (inr (3, (inr (2, (inr (1, (inl 0))))))))), (inr (5, (inr (7, (inr (8, (inr (6, (inl 0))))))))))) = 1;
(filterAlgCheck 4 (inl (1, (inl 0), (inl 0))) ((inr (1, (inl 0))), (inl 0))) = 1;
(filterAlgCheck 4 (inl (2, (inr (1, (inl 0))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) ((inr (2, (inr (1, (inl 0))))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) = 1;
(filterAlgCheck 4 (inl (3, (inr (2, (inr (1, (inl 0))))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) ((inr (3, (inr (2, (inr (1, (inl 0))))))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) = 1;
(filterAlgCheck 4 (inl (5, (inr (3, (inr (2, (inr (1, (inl 0))))))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) ((inr (3, (inr (2, (inr (1, (inl 0))))))), (inr (5, (inr (7, (inr (8, (inr (6, (inl 0))))))))))) = 1;
(filterAlgCheck 4 (inl (6, (inr (1, (inl 0))), (inl 0))) ((inr (1, (inl 0))), (inr (6, (inl 0))))) = 1;
(filterAlgCheck 4 (inl (7, (inr (1, (inl 0))), (inr (8, (inr (6, (inl 0))))))) ((inr (1, (inl 0))), (inr (7, (inr (8, (inr (6, (inl 0))))))))) = 1;
(filterAlgCheck 4 (inl (8, (inr (1, (inl 0))), (inr (6, (inl 0))))) ((inr (1, (inl 0))), (inr (8, (inr (6, (inl 0))))))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (4, (inr (0, (inr (3, (inr (2, (inr (1, (inl 0))))))))), (inr (5, (inr (7, (inr (8, (inr (6, (inl 0))))))))))) (inl (4, (inr (0, (inr (3, (inr (2, (inr (1, (inl 0))))))))), (inr (5, (inr (7, (inr (8, (inr (6, (inl 0)))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl termStr[tt]) (inr (9, (inl 0)))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))))))))))) (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))))))))) (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))))))) (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))))) (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))) (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))) (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))) (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (7, (inr (8, (inr (9, (inl 0))))))) (inr (7, (inr (8, (inr (9, (inl 0)))))))) = 1;
(concatAlgCheck (inr (9, (inl 0))) (inl (8, (inr (9, (inl 0))))) (inr (8, (inr (9, (inl 0)))))) = 1;
(listEq (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0))))))))))))))))))))) (inr (0, (inr (1, (inr (2, (inr (3, (inr (4, (inr (5, (inr (6, (inr (7, (inr (8, (inr (9, (inl 0)))))))))))))))))))))) = 1;
(filterAlgCheck 9 (inl termStr[tt]) ((inl 0), (inl 0))) = 1;
(filterAlgCheck 9 (inl (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))), (inl 0))) ((inr (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (1, (inl 0), (inl 0))) ((inr (1, (inl 0))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))), (inl 0))) ((inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))), (inl 0))) ((inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (4, (inr (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))))), (inl 0))) ((inr (4, (inr (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))), (inl 0))) ((inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (6, (inr (1, (inl 0))), (inl 0))) ((inr (6, (inr (1, (inl 0))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (7, (inr (8, (inr (6, (inr (1, (inl 0))))))), (inl 0))) ((inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))), (inl 0))) = 1;
(filterAlgCheck 9 (inl (8, (inr (6, (inr (1, (inl 0))))), (inl 0))) ((inr (8, (inr (6, (inr (1, (inl 0))))))), (inl 0))) = 1;
(sumEq unitEq (prodEq intEq (prodEq listEq listEq)) (inl (9, (inr (4, (inr (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))))))), (inl 0))) (inl (9, (inr (4, (inr (0, (inr (5, (inr (3, (inr (2, (inr (7, (inr (8, (inr (6, (inr (1, (inl 0))))))))))))))))))), (inl 0)))) = 1;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment