{-# 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

-- Hardcoded
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
-- Hardcoded rules
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