Mr solver: sorted insert example

cryptol-saw-core/src/Verifier/SAW/Cryptol/Monadify.hs

@@ -880,6 +880,9 @@ monadifyTerm' _ (asLocalVar -> Just ix) =
   ctx | ix >= length ctx -> fail "Monadification failed: vaiable out of scope!"
   ctx | (_,_,Right mtrm) <- ctx !! ix -> return mtrm
   _ -> fail "Monadification failed: type variable used in term position!"
+monadifyTerm' _ (asTupleValue -> Just []) =
+  return $ ArgMonTerm $
+  fromSemiPureTerm (mkMonType0 unitTypeOpenTerm) unitOpenTerm
 monadifyTerm' _ (asCtor -> Just (pn, args)) =
   monadifyApply (ArgMonTerm $ mkCtorArgMonTerm pn) args
 monadifyTerm' _ (asApplyAll -> (asTypedGlobalDef -> Just glob, args)) =

heapster-saw/examples/either.saw

@@ -3,10 +3,10 @@
 eith_tp <- parse_core "\\ (a b:sort 0) -> Either a b";
 cryptol_add_prim_type "Either" "Either" eith_tp;
 
-left_fun <- parse_core "\\ (a b:sort 0) (x:a) -> Left a b x";
+left_fun <- parse_core "left";
 cryptol_add_prim "Either" "Left" left_fun;
 
-right_fun <- parse_core "\\ (a b:sort 0) (x:b) -> Right a b x";
+right_fun <- parse_core "right";
 cryptol_add_prim "Either" "Right" right_fun;
 
 either_fun <- parse_core "either";

heapster-saw/examples/linked_list.cry

@@ -8,7 +8,20 @@ primitive type List : * -> *
 primitive foldList : {a} Either () (a, List a) -> List a
 primitive unfoldList : {a} List a -> Either () (a, List a)
 
+nil : {a} List a
+nil = foldList (Left ())
+
+cons : {a} a -> List a -> List a
+cons x l = foldList (Right (x,l))
+
 is_elem_spec : [64] -> List [64] -> [64]
 is_elem_spec x l =
   either (\ _ -> 0) (\ (y,l') -> if x == y then 1 else is_elem_spec x l')
          (unfoldList l)
+
+sorted_insert_spec : [64] -> List [64] -> List [64]
+sorted_insert_spec x l =
+  either (\ _ -> cons x nil)
+         (\ (y,l') -> if x <=$ y then cons x (cons y l')
+                      else cons y (sorted_insert_spec x l'))
+         (unfoldList l)

heapster-saw/examples/linked_list_mr_solver.saw

@@ -67,3 +67,13 @@ run_test "is_elem |= noErrorsSpec" (mr_solver is_elem is_elem_noErrorsSpec) true
 */
 
 run_test "is_elem |= is_elem_spec" (mr_solver is_elem {{ is_elem_spec }}) true;
+
+
+monadify_term {{ Right }};
+monadify_term {{ Left }};
+monadify_term {{ nil }};
+monadify_term {{ cons }};
+
+sorted_insert_no_malloc <- parse_core_mod "linked_list" "sorted_insert_no_malloc";
+run_test "sorted_insert_no_malloc |= sorted_insert_spec"
+  (mr_solver sorted_insert_no_malloc {{ sorted_insert_spec }}) true;

saw-core/prelude/Prelude.sawcore

@@ -680,10 +680,19 @@ Either__rec : (s t : sort 0) -> (p : Either s t -> sort 0) ->
                (e : Either s t) -> p e;
 Either__rec s t p f1 f2 e = Either#rec s t p f1 f2 e;
 
+-- The eliminator for the Either type
 either : (a b c : sort 0) -> (a -> c) -> (b -> c) -> Either a b -> c;
 either a b c f g e =
   Either__rec a b (\ (p: Either a b) -> c) f g e;
 
+-- Eta-expanded version of the Left constructor
+left : (a b : sort 0) -> a -> Either a b;
+left a b x = Left a b x;
+
+-- Eta-expanded version of the Right constructor
+right : (a b : sort 0) -> b -> Either a b;
+right a b x = Right a b x;
+
 eitherCong0 : (t x y : sort 0) -> Eq (sort 0) x y ->
                Eq (sort 0) (Either x t) (Either y t);
 eitherCong0 t x y eq =