{-# LANGUAGE OverloadedStrings #-}
module Language.REST.ProofGen where
import qualified Data.HashMap.Strict as M
import qualified Data.List as L
import qualified Data.Text as T
import Text.Printf
import Language.REST.Path
import Language.REST.Internal.Rewrite
import Language.REST.RuntimeTerm
import Language.REST.Op
opToLH :: Op -> String
opToLH :: Op -> [Char]
opToLH (Op Text
"union") = [Char]
"mp"
opToLH (Op Text
"toMS") = [Char]
"multiset_of"
opToLH (Op Text
op) = Text -> [Char]
T.unpack Text
op
withParens :: Bool -> String -> String
withParens :: Bool -> [Char] -> [Char]
withParens Bool
True [Char]
t = [Char]
"(" forall a. [a] -> [a] -> [a]
++ [Char]
t forall a. [a] -> [a] -> [a]
++ [Char]
")"
withParens Bool
False [Char]
t = [Char]
t
toLH :: Bool -> RuntimeTerm -> String
toLH :: Bool -> RuntimeTerm -> [Char]
toLH Bool
parens (App Op
"m" [RuntimeTerm
arg]) = Bool -> [Char] -> [Char]
withParens Bool
parens forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
printf [Char]
"Multiset [%s]" (Bool -> RuntimeTerm -> [Char]
toLH Bool
False RuntimeTerm
arg)
toLH Bool
parens (App Op
"cons" [RuntimeTerm
x, RuntimeTerm
xs]) = Bool -> [Char] -> [Char]
withParens Bool
parens forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s:%s" (Bool -> RuntimeTerm -> [Char]
toLH Bool
True RuntimeTerm
x) (Bool -> RuntimeTerm -> [Char]
toLH Bool
True RuntimeTerm
xs)
toLH Bool
_ (App Op
op []) = Op -> [Char]
opToLH Op
op
toLH Bool
parens (App Op
op [RuntimeTerm]
args) =
Bool -> [Char] -> [Char]
withParens Bool
parens forall a b. (a -> b) -> a -> b
$ forall r. PrintfType r => [Char] -> r
printf [Char]
"%s %s" (Op -> [Char]
opToLH Op
op) ([[Char]] -> [Char]
unwords forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Bool -> RuntimeTerm -> [Char]
toLH Bool
True) [RuntimeTerm]
args)
toProof :: Path Rewrite RuntimeTerm a -> String
toProof :: forall a. Path Rewrite RuntimeTerm a -> [Char]
toProof ([Step Rewrite RuntimeTerm a]
steps, PathTerm RuntimeTerm
result HashSet (RuntimeTerm, Rewrite)
_) = [Char]
" " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
L.intercalate [Char]
"\n=== " ([[Char]]
proofSteps forall a. [a] -> [a] -> [a]
++ [Bool -> RuntimeTerm -> [Char]
toLH Bool
False RuntimeTerm
result]) forall a. [a] -> [a] -> [a]
++ [Char]
"\n*** QED"
where
proofSteps :: [String]
proofSteps :: [[Char]]
proofSteps = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall a b c. ((a, b) -> c) -> a -> b -> c
curry forall {a}. (Step Rewrite RuntimeTerm a, Int) -> [Char]
proofStep) [Step Rewrite RuntimeTerm a]
steps [Int
0..]
proofStep :: (Step Rewrite RuntimeTerm a, Int) -> [Char]
proofStep (Step (PathTerm RuntimeTerm
t HashSet (RuntimeTerm, Rewrite)
_) Rewrite
_ a
_ Bool
True, Int
_) = Bool -> RuntimeTerm -> [Char]
toLH Bool
False RuntimeTerm
t
proofStep (Step (PathTerm RuntimeTerm
t HashSet (RuntimeTerm, Rewrite)
_) (Rewrite MetaTerm
lhs MetaTerm
rhs Maybe [Char]
name) a
_ Bool
False, Int
i) = Bool -> RuntimeTerm -> [Char]
toLH Bool
False RuntimeTerm
t forall a. [a] -> [a] -> [a]
++ [Char]
" ? " forall a. [a] -> [a] -> [a]
++ forall {a}. Ord a => HashMap a RuntimeTerm -> [Char]
toLemma Subst
lemma
where
lemma :: Subst
lemma = [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] -> Subst
go (RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
subTerms RuntimeTerm
t)
lemmaName :: Text
lemmaName = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text
"lemma" [Char] -> Text
T.pack Maybe [Char]
name
toLemma :: HashMap a RuntimeTerm -> [Char]
toLemma HashMap a RuntimeTerm
s = Bool -> RuntimeTerm -> [Char]
toLH Bool
False (Op -> [RuntimeTerm] -> RuntimeTerm
App (Text -> Op
Op Text
lemmaName) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
L.sort forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [(k, v)]
M.toList HashMap a RuntimeTerm
s))
go :: [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] -> Subst
go [] = forall a. HasCallStack => a
undefined
go ((RuntimeTerm
st, RuntimeTerm -> RuntimeTerm
f): [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
_) | Just Subst
su <- MetaTerm -> RuntimeTerm -> Subst -> Maybe Subst
unify MetaTerm
lhs RuntimeTerm
st forall k v. HashMap k v
M.empty
, RuntimeTerm -> RuntimeTerm
f (Subst -> MetaTerm -> RuntimeTerm
subst Subst
su MetaTerm
rhs) forall a. Eq a => a -> a -> Bool
== RuntimeTerm
nextTerm
= Subst
su
go ((RuntimeTerm, RuntimeTerm -> RuntimeTerm)
_:[(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
xs) = [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)] -> Subst
go [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
xs
nextTerm :: RuntimeTerm
nextTerm = if Int
i forall a. Ord a => a -> a -> Bool
< (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step Rewrite RuntimeTerm a]
steps forall a. Num a => a -> a -> a
- Int
1) then (forall rule term. PathTerm rule term -> term
pathTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall rule term a. Step rule term a -> PathTerm rule term
term) ([Step Rewrite RuntimeTerm a]
steps forall a. [a] -> Int -> a
!! (Int
i forall a. Num a => a -> a -> a
+ Int
1)) else RuntimeTerm
result