slow-eq.patch

150,152c150,158
< {-# LANGUAGE CPP #-}
< {-# LANGUAGE DeriveFunctor, DeriveFoldable #-}
< {-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase #-}
---
> module Main where
> import Base
> import Charser
> import System
> foreign export ccall "main" main
> {- GHC edition:
> {-# LANGUAGE LambdaCase #-}
> module Main where
> import Control.Applicative (asum)
154,166c160,161
< import Data.Foldable
< import Data.Function
< import Data.List (intersect, union, delete, elemIndex)
< #ifdef __HASTE__
< import Control.Monad
< import Haste.DOM
< import Haste.Events
< import Text.Parsec hiding (space)
< (<>) = (++)
< type Charser = Parsec String ()
< lowerChar = lower; upperChar = upper; alphaNumChar = alphaNum;
< digitChar = digit; space = spaces; some = many1
< #else
---
> import Data.Function ((&))
> import Data.List
170c165
< #endif
---
> -}
172,236c167,178
< #ifdef __HASTE__
< main :: IO ()
< main = withElems ["out", "rules", "order", "term", "knuthbendix", "rewrite"] $
<     \[oEl, rEl, ordEl, tEl, kbB, rwB] -> do
<   let
<     setup buttonName rs precs t = do
<       Just b <- elemById buttonName
<       let
<         go = do
<           setProp oEl "value" ""
<           setProp rEl "value" rs
<           setProp ordEl "value" precs
<           setProp tEl "value" t
<       void $ b `onEvent` Click $ const $ go
<       when (buttonName == "group") go
<   setup "group" (unlines
<     [ "(x * y) * z = x * (y * z)"
<     , "1 * x = x"
<     , "I x * x = 1"
<     ]) "1 * I" "(I x * x) * y"
<   setup "one" "F (F x) = G x" "" "F(F(F(F(F(x)))))"
<   setup "peano" (unlines
<     [ "0 + x = x"
<     , "S x + y = S (x + y)"
<     , "0 * x = 0"
<     , "S x * y = y + (x * y)"]) "" "S(S(S(S(0)))) * S(S(0)) + S(S(S(0)))"
<   setup "sort" (unlines
<     [ "Max 0 x = x"
<     , "Max x 0 = x"
<     , "Max (S x) (S y) = S (Max x y)"
<     , "Min 0 x = 0"
<     , "Min x 0 = 0"
<     , "Min (S x) (S y) = S (Min x y)"
<     , "Sort Nil = Nil"
<     , "Sort (Cons x y) = Insert x (Sort y)"
<     , "Insert x Nil = Cons x Nil"
<     , "Insert x (Cons y z) = Cons (Max x y) (Insert (Min x y) z)"
<     ]) "" $ concat
<       [ "Sort ("
<       , "Cons (S (S (S 0))) ("
<       , "Cons (S 0) ("
<       , "Cons (S (S (S (S 0)))) ("
<       , "Cons (S 0) ("
<       , "Cons (S (S (S (S (S 0)))))  Nil)))))"
<       ]
< 
<   let parseRules = sequence . map (parse rule "") . lines
<   void $ kbB `onEvent` Click $ const $ do
<     parseRules <$> getProp rEl "value" >>= \case
<       Left _ -> setProp oEl "value" "bad rules: parse error"
<       Right rs -> do
<         opList <- words <$> getProp ordEl "value"
<         case knuthBendix (lpoGT $ weigh opList) rs of
<           Nothing -> setProp oEl "value" "completion failed"
<           Just rs' ->  do
<             setProp oEl "value" ""
<             setProp rEl "value" $ unlines $ show <$> rs'
<   void $ rwB `onEvent` Click $ const $ do
<     parseRules <$> getProp rEl "value" >>= \case
<       Left _ -> setProp oEl "value" "bad rules: parse error"
<       Right rs -> parse expr "" <$> getProp tEl "value" >>= \case
<         Left _ -> setProp oEl "value" "bad term: parse error"
<         Right x -> do
<           setProp oEl "value" $ show $ fixRewrite rs x
< #endif
---
> parseRules = sequence . map (parse rule "") . lines
> 
> demo s opList = do
>   rs <- case parseRules s of
>     Left e -> Left $ show e
>     Right rs -> Right rs
>   maybe (Left "completion failed") Right
>     $ knuthBendix (lpoGT $ weigh $ words opList) rs
> 
> main = do
>   print $ parseRules "(x * y) * z = x * (y * z)\n1 * x = x\nI x * x = 1\n"
>   print $ demo "(x * y) * z = x * (y * z)\n1 * x = x\nI x * x = 1\n" "1 * I"
246,247c188,200
< data ExpF a = C String | V a | ExpF a :@ ExpF a deriving (Eq, Functor, Foldable)
< type Exp = ExpF String
---
> data ExpF a = C String | V a | ExpF a :@ ExpF a deriving Eq
> instance Functor ExpF where
>   fmap f = \case
>     V s -> V $ f s
>     x :@ y -> fmap f x :@ fmap f y
>     C s -> C s
> 
> elemExp want = \case
>   V s -> s == want
>   x :@ y -> elemExp want x || elemExp want y
>   C s -> False
> 
> type Exp = ExpF [Char]
268a222
>   sp :: Charser a -> Charser a
299c253
<   a :@ b -> if elem s t then Nothing else Just [(s, t)]
---
>   a :@ b -> if elemExp s t then Nothing else Just [(s, t)]
461c415
<   | V v <- t = s /= t && v `elem` s
---
>   | V v <- t = s /= t && v `elemExp` s
488c442,444
<   where wt s = elemIndex s precs
---
>   where
>   wt s = elemIndex s precs
>   elemIndex x xs = lookup x $ zip xs [0..]
609c565
<        >>= (\e -> rec eqs (delete e todo) [e])
---
>        >>= (\e -> rec eqs (filter (/= e) todo) [e])
667a624,650
> 
> ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
> <script>
> const ctx = {};
> function run() {
>   ctx.inp = (new TextEncoder()).encode(document.getElementById("rules").value);
>   ctx.out = [], ctx.cursor = 0;
>   ctx.instance.exports.main();
>   const out = (new TextDecoder()).decode(Uint8Array.from(ctx.out));
>   console.log(out);
> }
> async function loadWasm() {
>   try {
>     ctx.instance = (await WebAssembly.instantiateStreaming(fetch('eq.wasm'), {env:
>       { putchar: c  => ctx.out.push(c)
>       , eof    : () => ctx.cursor == ctx.inp.length
>       , getchar: () => ctx.inp[ctx.cursor++]
>       }})).instance;
> console.log("running...");
> run();
>   } catch(err) {
>     console.log(err);
>   }
> }
> loadWasm();
> </script>
> ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++