Petra
=====
<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->
Petra is a very simple term-rewriting language, presented definitionally here as a
self-contained Literate Haskell program, in the public domain, with Falderal tests.
Petra is not meant to stand on its own as a programming language so much as it's
meant to provide an example or starting point from which other term-rewriting-based
systems can be built.
The contents of the Literal Haskell file are also valid Markdown, and the `README.md`
file is a symlink to it, enabling it to be sensibly rendered when viewing the
repository in a git repository viewer such as Forgejo, GitLab, or GitHub.
> module Petra where
> import qualified Data.Map as Map
> import System.Environment
> import Text.ParserCombinators.Parsec
Terms
-----
A term is either an uninterpreted function symbol with subterms, or a variable.
> data Term = Function String [Term]
> | Variable String
> deriving (Eq, Ord)
> instance Show Term where
> show (Variable name) = name
> show (Function name []) = name
> show (Function name children) =
> name ++ "(" ++ mapCommas children ++ ")"
> where
> mapCommas [] = ""
> mapCommas [x] = show x
> mapCommas (x:xs) = (show x) ++ "," ++ mapCommas xs
> data Rule = Rewrite Term Term
> deriving (Eq, Ord)
> instance Show Rule where
> show (Rewrite lhs rhs) = (show lhs) ++ " -> " ++ (show rhs)
> data Program = Program [Rule] Term
> deriving (Eq, Ord, Show)
> type Unifier = Map.Map String Term
Utility
-------
`mapFirst` tries to apply f to each element of the list; at the first
(leftmost) element on which f succeeds, a replacement is made with the
result of f, and all other items of the list are unchanged. If f
succeeds on no element of the list then the whole function fails.
> mapFirst :: (a -> Maybe a) -> [a] -> Maybe [a]
> mapFirst f [] = Nothing
> mapFirst f (x:xs) =
> case (f x) of
> Just x' -> Just (x':xs)
> Nothing -> case mapFirst f xs of
> Just xs' -> Just (x:xs')
> Nothing -> Nothing
Pattern Matching
----------------
Match a pattern against a term. Evaluates to either Just a unifier,
if there was a match, or Nothing, if there was no match.
A pattern which is a function symbol matches only if all of its children do.
> match :: Term -> Term -> Unifier -> Maybe Unifier
> match (Function s a) (Function t b) unifier
> | s == t = matchAll a b unifier
> | otherwise = Nothing
> where
> matchAll [] [] unifier = Just unifier
> matchAll [] (term:terms) unifier = Nothing
> matchAll (term:terms) [] unifier = Nothing
> matchAll (a:as) (b:bs) unifier =
> case match a b unifier of
> Just unifier' -> matchAll as bs unifier'
> Nothing -> Nothing
A pattern which is a variable matches any subject, and yields a unifier
extended with a binding between the variable name and that subject.
> match (Variable name) subject unifier =
> case Map.lookup name unifier of
> Nothing -> Just (Map.insert name subject unifier)
> Just value -> if value == subject then
> Just unifier
> else
> Nothing
> match _ _ _ = Nothing
Instantiation
-------------
Given a unifier that associates variables with terms, replace each variable
in the given term with the term it is associated with (if any).
> expand :: Term -> Unifier -> Term
> expand v@(Variable name) unifier =
> case Map.lookup name unifier of
> Just term -> term
> Nothing -> v
> expand (Function name children) bindings =
> Function name (map (\term -> expand term bindings) children)
Rewriting
---------
Given a term t and a rule r, rewrite tries to apply the rule to the
deepest subterm of t that it can find.
> rewrite :: Term -> Rule -> Maybe Term
> rewrite t@(Function name children) r =
> case mapFirst (\child -> rewrite child r) children of
> Just newchildren -> Just (Function name newchildren)
> Nothing -> rewriteTerm t r
> rewrite t r = rewriteTerm t r
If the term in question is not a function symbol, or if it is a function
symbol but none of its children could be rewritten, just try to match on
the term and possibly substitute it.
> rewriteTerm :: Term -> Rule -> Maybe Term
> rewriteTerm t (Rewrite lhs rhs) =
> case match lhs t Map.empty of
> Just unifier -> Just (expand rhs unifier)
> Nothing -> Nothing
Given a term and a set of rules, try rewriting with each rule until
one succeeds, and repeat this process until no rule succeeds. Return
the rewritten term.
> reduce :: Term -> [Rule] -> Term
> reduce term rules =
> case rewriteAll term rules of
> Just term' -> reduce term' rules
> Nothing -> term
> where
> rewriteAll term [] = Nothing
> rewriteAll term (rule:rules) =
> case rewrite term rule of
> Just term' -> Just term'
> Nothing -> rewriteAll term rules
Parser
------
Term ::= Identifier ["(" Term {"," Term} ")"] | VarName.
Rule ::= Term ("->" | "=>") Term.
Program ::= {Rule ";"} "?" Term.
> sym x = string x >> spaces
> identifier :: Parser String
> identifier = do
> c <- lower
> cs <- many alphaNum
> spaces
> return (c:cs)
> varname :: Parser Term
> varname = do
> c <- upper
> cs <- many alphaNum
> spaces
> return (Variable (c:cs))
> funsym :: Parser Term
> funsym = do
> s <- identifier
> r <- option (Function s []) (do
> sym "("
> l <- sepBy1 (term) (sym ",")
> sym ")"
> return (Function s l))
> return r
> term :: Parser Term
> term = funsym <|> varname
> rule :: Parser Rule
> rule = do
> lhs <- term
> sym "->"
> rhs <- term
> return (Rewrite lhs rhs)
> rules :: Parser [Rule]
> rules = sepEndBy1 rule (sym ";")
> program :: Parser Program
> program = do
> r <- rules
> sym "?"
> t <- term
> return (Program r t)
> parsePetra x = parse (spaces >> program) "" x
Drivers
-------
> main = do
> [inputFilename] <- getArgs
> inputProgram <- readFile inputFilename
> run inputProgram
> repl = do
> line <- getLine
> case line of
> "quit" -> return ()
> programText -> do
> run programText
> repl
> run programText = do
> case parsePetra programText of
> Left err -> putStrLn (show err)
> Right prog ->
> let
> result = interpret prog
> in
> putStrLn (show result)
> return ()
> interpret :: Program -> Term
> interpret (Program rules term) =
> reduce term rules
Falderal Tests
--------------
These tests are written in [Falderal][] 0.14 format.
-> Functionality "Evaluate Petra program" is implemented by
-> shell command "runhaskell Petra.lhs %(test-body-file)"
-> Tests for functionality "Evaluate Petra program"
| foo -> bar;
| ? foo
= bar
| foo -> bar;
| ? goo
= goo
| don(A) -> mon(A);
| ? don(key)
= mon(key)
We don't have a test case for `flip(A,B)->flip(B,A)`, as it would
loop forever.
| flip(A,B) -> done(B,A);
| ? flip(x,y)
= done(y,x)
| same(A,A) -> true;
| ? same(x,y)
= same(x,y)
| same(A,A) -> true;
| ? same(false,false)
= true
| pink -> blue;
| ? color(pink)
= color(blue)
| pink -> blue;
| ? color(pink,pink)
= color(blue,blue)
| f(A,B)->B;
| ? f(f(a,b),c)
= c
| f(A,A)->A;
| ? f(f(a,a),c)
= f(a,c)
| a(A,A)->z; b(B)->b;
| ? a(b(x),b(y))
= z
| and(t,t)->t;
| and(f,X)->f;
| and(X,f)->f;
| or(t,X)->t;
| or(X,t)->t;
| or(f,f)->f;
| ? and(or(t,f),or(f,t))
= t
| not(true) -> false;
| not(false) -> true;
| even(nil) -> true;
| even(cons(H,T)) -> not(even(T));
| ? even(cons(true,cons(true,cons(false,nil))))
= false
[Falderal]: https://catseye.tc/node/Falderal