Work

.gitignore

@@ -0,0 +1 @@
+build/**

Array.idr

@@ -0,0 +1,20 @@
+module Array
+
+import Data.Vect
+import Data.SortedMap
+import Math
+
+import Language
+
+public export
+Array : Nat -> Language -> Language
+Array k (MkLanguage val constants rators) = 
+  MkLanguage (Vect k val) 
+             (map (replicate k) constants)
+             (map (\(n ** op) => (n ** scatterOp n op)) rators)
+  where
+    scatterOp : (n : Nat) -> Operator val n -> Operator (Vect k val) n
+    scatterOp n (MkOperator name denotation) = 
+      MkOperator name (traverse denotation . sequence)
+
+

Bus.idr

@@ -0,0 +1,84 @@
+module Bus
+
+import Data.Vect
+import Data.Fuel
+import Data.List.Elem
+import Data.SortedMap
+import Language
+import Control.Monad.State
+import Control.Monad.State.State
+
+%default total
+
+data Sum : Nat -> Type where
+  Plus : (n : Nat) -> (m : Nat) -> Sum (n + m)
+
+sumsOf : (n : Nat) -> List (Sum n)
+sumsOf k = rewrite sym (plusZeroRightNeutral k) in walk k 0
+  where 
+    walk : (n : Nat) -> (m : Nat) -> List (Sum (n + m))
+    walk 0 m = [Plus 0 m]
+    walk (S j) m = 
+      let k = Plus (S j) m
+          p = rewrite plusSuccRightSucc j m in walk j (S m) 
+      in  k :: p
+
+partitions : (sm : Nat) -> (n : Nat) -> List (Vect n Nat)
+partitions 0 0 = [[]]
+partitions sm 0 = []
+partitions sm (S 0) = [[sm]]
+partitions sm (S k) = 
+  do (Plus me you) <- sumsOf sm
+     ps <- partitions you k
+     pure $ me :: ps
+
+record Subterm (l : Language) where
+  constructor MkSubterm
+  term : Term l.Val
+  val : l.Val
+
+record Corpus (l : Language) where
+  constructor MkCorpus
+  byDeno : SortedMap l.Val (Subterm l)
+  bySize : List (List (Subterm l))
+
+initialCorpus : (l : Language) -> Ord l.Val => Env l.Val -> Corpus l
+initialCorpus l nv = 
+  let 
+    lits : List (Subterm l)
+    lits = map (\c => MkSubterm (Constant c) c) l.constants
+    syms : List (Subterm l)
+    syms = map (\(k, v) => MkSubterm (Symbol k) v) (SortedMap.toList nv)
+    consts = lits ++ syms
+    denos : SortedMap l.Val (Subterm l)
+    denos = SortedMap.fromList $ map (\c => (val c, c)) consts
+  in
+    MkCorpus denos [consts]
+
+grow : (l : Language) -> Ord l.Val => Corpus l -> Corpus l
+grow l (MkCorpus byDeno bySize) = 
+    let newGen = generate (values l.rators)
+        newDenos = SortedMap.fromList $ map (\c => (val c, c)) newGen in
+    MkCorpus (mergeLeft byDeno newDenos) (bySize ++ [values newDenos])
+  where
+    size : Nat
+    size = length bySize
+    ofSize : Nat -> List (Subterm l)
+    ofSize b = join $ toList $ fst <$> indexElem b bySize
+    generate : List (n ** Operator l.Val n) -> List (Subterm l)
+    generate ops = do (arity ** op@(MkOperator _ deno)) <- ops
+                      budgets <- partitions (pred size) arity
+                      subterms <- sequence $ map ofSize budgets
+                      value <- toList $ deno $ map val subterms
+                      guard $ isNothing $ lookup value byDeno
+                      pure $ MkSubterm (Application op (map term subterms)) value
+
+export
+bus : (f : Fuel) -> (l : Language) -> Ord l.Val => 
+      (nv : Env l.Val) -> (expected : l.Val) -> Maybe (Term l.Val)
+bus f l nv ex = term <$> loop f (initialCorpus l nv)
+  where
+    loop : Fuel -> Corpus l -> Maybe (Subterm l)
+    loop Dry c@(MkCorpus byDeno bySize) = lookup ex byDeno 
+    loop (More x) c@(MkCorpus byDeno bySize) = lookup ex byDeno <|> loop x (grow l c)
+

Bus.ipkg

@@ -0,0 +1,7 @@
+package bus
+
+modules = Tests
+        , Language
+        , Bus
+
+depends = prelude, base, contrib

Language.idr

@@ -0,0 +1,98 @@
+module Language
+
+import Data.Vect
+import Data.List
+import Data.Fuel
+import Data.List.Elem
+import Data.String
+import Sexpr
+import Decidable.Equality
+import Data.SortedMap
+
+%default total
+
+public export
+nary : (n : Nat) -> Type -> Type
+nary 0 t = t
+nary (S k) t = t -> nary k t
+
+public export
+ncurry : {n : Nat} -> nary n a -> Vect n a -> a
+ncurry       x [] = x
+ncurry       x (y :: xs) = ncurry (x y) xs
+
+public export
+record Operator Value (arity : Nat) where
+  constructor MkOperator
+  name : String
+  denotation : Vect arity Value -> Maybe Value
+
+public export
+record Language where
+  constructor MkLanguage
+  Val : Type
+  constants : List Val
+  rators : SortedMap String (n ** (Operator Val n))
+
+public export
+data Term : Type -> Type where
+  Symbol : String -> Term t
+  Constant : t -> Term t
+  Application : {n : Nat} -> Operator t n -> Vect n (Term t) -> Term t
+
+public export 
+Show (Operator v n) where
+  show = name
+
+public export
+Show v => Show (Term v) where
+  show (Application x xs) = 
+    let seq = toList $ x.name :: (map (\s => show (assert_smaller xs s)) xs) in 
+    "(\{unwords seq})"
+  show (Constant x) = show x
+  show (Symbol str) = str
+
+public export
+Env : Type -> Type
+Env val = SortedMap String val
+
+export
+eval : Env v -> Term v -> Maybe v
+eval env (Symbol str) = lookup str env
+eval env (Constant x) = Just x
+eval env (Application (MkOperator name denotation) xs) = 
+  do subterms <- sequence $ map (\k => eval env (assert_smaller xs k)) xs
+     denotation subterms
+
+operatorsOfArity : (l : Language) -> (n : Nat) -> List (Operator l.Val n)
+operatorsOfArity l n = search (values l.rators)
+  where 
+    search : List (ar ** Operator l.Val ar) -> List (Operator l.Val n)
+    search [] = []
+    search (((ar ** op)) :: xs) = 
+      case decEq ar n of
+        (Yes Refl) => op :: search xs
+        (No contra) => search xs
+
+-- public export
+-- construct : (l : Language) -> Sexpr -> Maybe (Term l.Val)
+-- construct l (Atom str) = 
+--   do (k, ks) <- strUncons str
+--      if k == '?' 
+--      then Just (Symbol ks)
+--      else 
+
+--   case lookup str l.rators of
+--     (Just ((0 ** op))) => Just $ MkTerm 0 op []
+--     _ => Nothing
+-- construct l (App ((Atom str) :: xs)) = 
+--   do let vc = Vect.fromList xs
+--      (ar ** op) <- lookup str l.rators
+--      case decEq (length xs) ar of
+--        (Yes Refl) => do subterms <- 
+--                             sequence $ map (\k => 
+--                                              construct l (assert_smaller xs k))
+--                                            vc
+--                         pure $ MkTerm ar op subterms
+--        (No contra) => Nothing
+-- construct l _ = Nothing

Math.idr

@@ -0,0 +1,21 @@
+
+module Math
+
+import Data.Vect  
+import Data.SortedMap  
+import Language  
+
+public export
+Math : Language
+Math = MkLanguage Integer constants (SortedMap.fromList operators)
+  where
+    constants = the (List Integer) [0, 1]
+    binop : String -> (Integer -> Integer -> Integer) -> (String, (DPair Nat (Operator Integer)))
+    binop nm fn = (nm, (2 ** MkOperator nm $ Just . (ncurry fn)))
+    eqInt : Integer -> Integer -> Integer
+    eqInt m n = if m == n then 1 else 0
+    ltInt : Integer -> Integer -> Integer
+    ltInt m n = if m < n then 1 else 0
+    operators = the (List _) [ ("-", (1 ** (MkOperator "-" $ \[k] => Just (-k))))
+                             , binop "+" (+) , binop "*" (*)
+                             , binop "<" ltInt , binop "=" eqInt]

Sexpr.idr

@@ -0,0 +1,44 @@
+module Sexpr
+
+import Data.String
+-- import Data.String.Parser
+
+%default total 
+
+public export
+data Sexpr = App (List Sexpr) | Atom String
+
+isSpecial : Char -> Bool
+isSpecial c = c == '(' || c == ')' || isSpace c
+
+parseAtom : String -> Maybe (String, String)
+parseAtom s with (strM s)
+  parseAtom "" | StrNil = Just ("", "")
+  parseAtom s@(strCons c str) | (StrCons c str) = 
+    if isSpecial c
+    then Just ("", s)
+    else 
+      let rst = parseAtom (assert_smaller s str) in
+      map (mapFst (strCons c)) rst
+
+mutual
+  parseList : String -> Maybe (List Sexpr, String)
+  parseList i = (do (p, rs) <- parseSexpr i
+                    (ps, rs) <- parseList (assert_smaller i rs)
+                    pure (p :: ps, rs))
+                <|> Just ([], i)
+
+  parseSexpr : String -> Maybe (Sexpr, String)
+  parseSexpr s =
+    case strUncons s of
+      Nothing => Nothing
+      Just ('(', rst) =>
+        do (res, rst) <- parseList (assert_smaller s rst)
+           case strUncons rst of
+             Just (')', rst) => pure $ (App res, rst)
+             _               => Nothing
+      Just (')', rst) => Nothing
+      Just (c, str) =>
+        if isSpace c
+        then parseSexpr (assert_smaller s str)
+        else map (mapFst Atom) (parseAtom s)

String.idr

@@ -0,0 +1,22 @@
+
+module String
+
+import Data.Vect  
+import Data.String  
+import Data.SortedMap  
+import Language  
+
+partial
+public export
+Strings : Language
+Strings = MkLanguage String constants (SortedMap.fromList operators)
+  where
+    constants = the (List String) [" ", ".", "-", "*", "0", "1", "2", "-1"]
+    binop : String -> (String -> String -> String) -> (String, (DPair Nat (Operator String)))
+    binop nm fn = (nm, (2 ** MkOperator nm $ Just . (ncurry fn)))
+    idx : String -> String -> Maybe String
+    idx str ix = 
+      do i <- parseInteger ix
+         pure $ pack [strIndex str $ i `mod` (strLength str)]
+    operators = the (List _) [ binop "concat" (++)
+                             , ("index", (2 ** MkOperator "index" (\[a, b] => idx a b))) ] 

Tests.idr

@@ -0,0 +1,36 @@
+
+import Data.Vect
+import Data.SortedMap
+import Data.Fuel
+import Bus
+import Math
+import String
+import Array
+import Language
+
+testI : Vect 4 Integer -> List (String, Vect 4 Integer) -> IO ()
+testI xs ys = 
+ do printLn "Free Variables:"
+    traverse_ (\(s, v) => printLn "\{s} => \{show v}") ys
+    printLn "Expected Values:"
+    printLn $ show xs
+    let res = bus (limit 10) (Array 4 Math) (SortedMap.fromList ys) xs
+    printLn $ "Generated Code: " ++ show res
+
+partial
+testS : Vect 4 String -> List (String, Vect 4 String) -> IO ()
+testS xs ys = 
+ do printLn "Free Variables:"
+    traverse_ (\(s, v) => printLn "\{s} => \{show v}") ys
+    printLn "Expected Values:"
+    printLn $ show xs
+    let res = bus (limit 10) (Array 4 Strings) (SortedMap.fromList ys) xs
+    printLn $ "Generated Code: " ++ show res
+
+partial
+main : IO ()
+main = do
+  testI [1, 2, 3, 4] [("x", [0, 1, 2, 3])]
+  testI [2, 4, 6, 8] [("x", [2, 4, 6, 8])]
+  testI [3, 6, 9, 12] [("x", [2, 4, 6, 8]), ("y", [3, 2, 3, 4])]
+  testS ["a", "b", "c", "d"] [("x", ["aa", "ab", "ac", "ad"])]

run.sh

@@ -0,0 +1,3 @@
+#!/bin/sh
+
+IDRIS2_CG="node" idris2 Tests.idr -x main