{-# LANGUAGE OverloadedStrings #-} module DSL where import Language.REST.Op import qualified Language.REST.MetaTerm as MT import Language.REST.RuntimeTerm as RT import Language.REST.Internal.Rewrite import Nat commutes, assocL, assocR :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) -> Rewrite commutes :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite commutes MetaTerm -> MetaTerm -> MetaTerm op = MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm y MetaTerm -> MetaTerm -> Rewrite ~> MetaTerm y MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm x assocL :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite assocL MetaTerm -> MetaTerm -> MetaTerm op = (MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm y) MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm z' MetaTerm -> MetaTerm -> Rewrite ~> MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op` (MetaTerm y MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm z') assocR :: (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite assocR MetaTerm -> MetaTerm -> MetaTerm op = MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op` (MetaTerm y MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm z') MetaTerm -> MetaTerm -> Rewrite ~> (MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm y) MetaTerm -> MetaTerm -> MetaTerm `op` MetaTerm z' distribL, distribR :: (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) -> (MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm) -> Rewrite distribL :: (MetaTerm -> MetaTerm -> MetaTerm) -> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite distribL MetaTerm -> MetaTerm -> MetaTerm op1 MetaTerm -> MetaTerm -> MetaTerm op2 = (MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op1` MetaTerm y) MetaTerm -> MetaTerm -> MetaTerm `op2` MetaTerm z' MetaTerm -> MetaTerm -> Rewrite ~> (MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op2` MetaTerm z') MetaTerm -> MetaTerm -> MetaTerm `op1` (MetaTerm y MetaTerm -> MetaTerm -> MetaTerm `op2` MetaTerm z') distribR :: (MetaTerm -> MetaTerm -> MetaTerm) -> (MetaTerm -> MetaTerm -> MetaTerm) -> Rewrite distribR MetaTerm -> MetaTerm -> MetaTerm op1 MetaTerm -> MetaTerm -> MetaTerm op2 = MetaTerm z' MetaTerm -> MetaTerm -> MetaTerm `op2` (MetaTerm x MetaTerm -> MetaTerm -> MetaTerm `op1` MetaTerm y) MetaTerm -> MetaTerm -> Rewrite ~> (MetaTerm z' MetaTerm -> MetaTerm -> MetaTerm `op2` MetaTerm x) MetaTerm -> MetaTerm -> MetaTerm `op1` (MetaTerm z' MetaTerm -> MetaTerm -> MetaTerm `op2` MetaTerm y) ackOp, plus, minus, times :: Op ackOp :: Op ackOp = Text -> Op Op Text "ack" plus :: Op plus = Text -> Op Op Text "+" minus :: Op minus = Text -> Op Op Text "-" times :: Op times = Text -> Op Op Text "*" a, b, c, d :: RuntimeTerm a :: RuntimeTerm a = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "a") [] b :: RuntimeTerm b = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "b") [] c :: RuntimeTerm c = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "c") [] d :: RuntimeTerm d = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "d") [] x, y, v, w, z' :: MT.MetaTerm x :: MetaTerm x = String -> MetaTerm MT.Var String "X" y :: MetaTerm y = String -> MetaTerm MT.Var String "Y" v :: MetaTerm v = String -> MetaTerm MT.Var String "V" w :: MetaTerm w = String -> MetaTerm MT.Var String "W" z' :: MetaTerm z' = String -> MetaTerm MT.Var String "Z" f, g, h :: Op f :: Op f = Text -> Op Op Text "f" g :: Op g = Text -> Op Op Text "g" h :: Op h = Text -> Op Op Text "h" t1Op, t2Op :: Op t1Op :: Op t1Op = Text -> Op Op Text "t1" t2Op :: Op t2Op = Text -> Op Op Text "t2" t1, t2, t3, t4, t5 :: RuntimeTerm t1 :: RuntimeTerm t1 = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "t1") [] t2 :: RuntimeTerm t2 = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "t2") [] t3 :: RuntimeTerm t3 = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "t3") [] t4 :: RuntimeTerm t4 = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "t4") [] t5 :: RuntimeTerm t5 = Op -> [RuntimeTerm] -> RuntimeTerm App (Text -> Op Op Text "t5") [] zero, one, two :: RuntimeTerm zero :: RuntimeTerm zero = Op -> [RuntimeTerm] -> RuntimeTerm App Op z [] one :: RuntimeTerm one = RuntimeTerm -> RuntimeTerm suc RuntimeTerm zero two :: RuntimeTerm two = RuntimeTerm -> RuntimeTerm suc RuntimeTerm one suc :: RuntimeTerm -> RuntimeTerm suc :: RuntimeTerm -> RuntimeTerm suc RuntimeTerm x1 = Op -> [RuntimeTerm] -> RuntimeTerm App Op s [RuntimeTerm x1] ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm ack :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm ack RuntimeTerm x1 RuntimeTerm y1 = Op -> [RuntimeTerm] -> RuntimeTerm App Op ackOp [RuntimeTerm x1, RuntimeTerm y1] zero' :: MT.MetaTerm zero' :: MetaTerm zero' = RuntimeTerm -> MetaTerm forall a. ToMetaTerm a => a -> MetaTerm MT.toMetaTerm RuntimeTerm zero one' :: MT.MetaTerm one' :: MetaTerm one' = MetaTerm -> MetaTerm suc' MetaTerm zero' suc' :: MT.MetaTerm -> MT.MetaTerm suc' :: MetaTerm -> MetaTerm suc' MetaTerm x1 = Op -> [MetaTerm] -> MetaTerm MT.RWApp Op s [MetaTerm x1] ack' :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm ack' :: MetaTerm -> MetaTerm -> MetaTerm ack' MetaTerm x1 MetaTerm y1 = Op -> [MetaTerm] -> MetaTerm MT.RWApp Op ackOp [MetaTerm x1, MetaTerm y1] infixl 1 .+ (.+) :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm .+ :: RuntimeTerm -> RuntimeTerm -> RuntimeTerm (.+) RuntimeTerm x1 RuntimeTerm y1 = Op -> [RuntimeTerm] -> RuntimeTerm App Op plus [RuntimeTerm x1, RuntimeTerm y1] (#+) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm #+ :: MetaTerm -> MetaTerm -> MetaTerm (#+) MetaTerm x1 MetaTerm y1 = Op -> [MetaTerm] -> MetaTerm MT.RWApp Op plus [MetaTerm x1, MetaTerm y1] (#-) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm #- :: MetaTerm -> MetaTerm -> MetaTerm (#-) MetaTerm x1 MetaTerm y1 = Op -> [MetaTerm] -> MetaTerm MT.RWApp Op minus [MetaTerm x1, MetaTerm y1] (#*) :: MT.MetaTerm -> MT.MetaTerm -> MT.MetaTerm #* :: MetaTerm -> MetaTerm -> MetaTerm (#*) MetaTerm x1 MetaTerm y1 = Op -> [MetaTerm] -> MetaTerm MT.RWApp Op times [MetaTerm x1, MetaTerm y1] infix 0 ~> (~>) :: MT.MetaTerm -> MT.MetaTerm -> Rewrite MetaTerm t ~> :: MetaTerm -> MetaTerm -> Rewrite ~> MetaTerm u = MetaTerm -> MetaTerm -> Maybe String -> Rewrite Rewrite MetaTerm t MetaTerm u Maybe String forall a. Maybe a Nothing infix 0 <~> (<~>) :: MT.MetaTerm -> MT.MetaTerm -> [Rewrite] MetaTerm t <~> :: MetaTerm -> MetaTerm -> [Rewrite] <~> MetaTerm u = [ MetaTerm t MetaTerm -> MetaTerm -> Rewrite ~> MetaTerm u, MetaTerm u MetaTerm -> MetaTerm -> Rewrite ~> MetaTerm t ]