Added some cmp builtins for Int and a tree relabelling example.

Compile.hs

@@ -207,7 +207,9 @@ compileOp (CmdId id _) = return $ S.EA id
 builtins :: M.Map String String
 builtins = M.fromList [("+", "plus")
                       ,("-", "minus")
-                      ,("eqc" , "eqc")]
+                      ,("eqc" , "eqc")
+                      ,(">", "gt")
+                      ,("<", "lt")]
 
 isBuiltin :: String -> Bool
 isBuiltin x = M.member x builtins

Parser.hs

@@ -368,7 +368,7 @@ letTm p p' = attachLoc $ do reserved "let"
                             return $ Let x t t'
 
 binOpLeft :: MonadicParsing m => m (Use Raw)
-binOpLeft = attachLoc $ do op <- choice $ map symbol ["+","-","*","/"]
+binOpLeft = attachLoc $ do op <- choice $ map symbol ["+","-","*","/",">","<"]
                            return $ RawId op
 
 binOpRight :: MonadicParsing m => m (Use Raw)

RefineSyntax.hs

@@ -512,6 +512,12 @@ makeIntBinOp a c = Def [c] (CType [Port [] (IntTy a) a
                                   ,Port [] (IntTy a) a]
                                   (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a) (IntTy a) a) a) [] a
 
+makeIntBinCmp :: Refined -> Char -> MHDef Refined
+makeIntBinCmp a c = Def [c] (CType [Port [] (IntTy a) a
+                                   ,Port [] (IntTy a) a]
+                             (Peg (Ab (AbVar "£" a) (ItfMap M.empty a) a)
+                              (DTTy "Bool" [] a) a) a) [] a
+
 {-- The initial state for the refinement pass. -}
 
 builtinDataTs :: [DataT Refined]
@@ -541,6 +547,7 @@ builtinItfAliases = []
 
 builtinMHDefs :: [MHDef Refined]
 builtinMHDefs = map (makeIntBinOp (Refined BuiltIn)) "+-" ++
+                map (makeIntBinCmp (Refined BuiltIn)) "><" ++
                 [caseDef, charEq, alphaNumPred]
 
 charEq :: MHDef Refined

examples/prelude.fk

@@ -16,6 +16,10 @@ not : {Bool -> Bool}
 not false = true
 not true  = false
 
+and : Bool -> Bool -> Bool
+and   true    true  = true
+and    _       _    = false
+
 {-- Control structures --}
 
 -- lazy conditional
@@ -37,6 +41,10 @@ eqN : {Nat -> Nat -> Bool}
 eqN zero zero = true
 eqN (suc n) (suc m) = eqN n m
 
+-- Equality on integers
+eqInt : {Int -> Int -> Bool}
+eqInt  n m = if (n < m) {false} {if (n > m) {false} {true}}
+
 -- List operations
 rev' : {List X -> List X -> List X}
 rev' []        ys = ys

examples/relabel.fk

@@ -0,0 +1,43 @@
+include prelude
+
+data Tree X = Leaf X | Node (Tree X) (Tree X)
+
+labels : Tree X -> List X
+labels  (Leaf x) = [x]
+labels  (Node l r) = append (labels l) (labels r)
+
+label : Tree X -> Int -> Pair (Tree Int) Int
+label   (Leaf x)   n   = pair (Leaf n) (n + 1)
+label   (Node l r) n   = case (label l n)
+                         { (pair l' n') ->
+                              case (label r n')
+                              {(pair r' n'') -> pair (Node l' r') n''}
+                         }
+
+relabel : Tree X -> Tree Int
+relabel t = fst (label t 0)
+
+nodups : List Int -> Bool
+nodups      []     = true
+nodups   (x :: xs) = and (not (elem eqInt xs x)) (nodups xs)
+
+-- Now for a stateful version
+
+first : X -> Y -> X
+first   x    y = x
+
+fresh : {[State Int]Int}
+fresh! = first get! (put (get! + 1))
+
+label' : {Tree X   -> [State Int]Tree Int}
+label'  (Leaf x)   = Leaf fresh!
+label'  (Node l r) = Node (label' l) (label' r)
+
+relabelS : Tree X -> Tree Int
+relabelS t = evalState 0 (label' t)
+
+tree : {Tree Bool}
+tree! = Node (Node (Leaf true) (Leaf false)) (Node (Leaf true) (Leaf false))
+
+main : {Bool}
+main! = nodups (labels (relabelS tree!))

shonky/src/Shonky/Semantics.hs

@@ -172,8 +172,26 @@ minus g [a1,a2] = VI (f a1 - f a2)
           _ -> error "minus: argument not an int"
 minus g _ = error "minus: incorrect number of arguments, expected 2."
 
+builtinPred :: Bool -> Val
+builtinPred b = (if b then VA "true" else VA "false") :&& VA ""
+
+lt :: Env -> [Comp] -> Val
+lt g [a1,a2] = builtinPred ((f a1) < (f a2))
+  where f x = case x of
+          Ret (VI n) -> n
+          _ -> error "plus: argument not an int"
+lt g _ = error "plus: incorrect number of arguments, expected 2."
+
+gt :: Env -> [Comp] -> Val
+gt g [a1,a2] = builtinPred ((f a1) > (f a2))
+  where f x = case x of
+          Ret (VI n) -> n
+          _ -> error "plus: argument not an int"
+gt g _ = error "plus: incorrect number of arguments, expected 2."
+
+
 eqc :: Env -> [Comp] -> Val
-eqc g [a1,a2] = (if (f a1) == (f a2) then VA "true" else VA "false") :&& VA ""
+eqc g [a1,a2] = builtinPred ((f a1) == (f a2))
   where f x = case x of
           Ret (VX [c]) -> c
           _ -> error "eqc: argument not a character"
@@ -191,6 +209,7 @@ alphaNumPred g _ =
 
 builtins :: M.Map String (Env -> [Comp] -> Val)
 builtins = M.fromList [("plus", plus), ("minus", minus), ("eqc", eqc)
+                      ,("lt", lt), ("gt", gt)
                       ,("isAlphaNum", alphaNumPred)]
 
 -- Look-up a definition
@@ -455,7 +474,9 @@ txt (u :&& v)  = txt u ++ txt v
 envBuiltins :: Env
 envBuiltins = Empty :/ [DF "plus" [] []
                        ,DF "minus" [] []
-                       ,DF "eqc"   [] []]
+                       ,DF "eqc"   [] []
+                       ,DF "gt"    [] []
+                       ,DF "lt"    [] []]
 
 prog :: Env -> [Def Exp] -> Env
 prog g ds = g' where