{-# 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]
"(" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
t [Char] -> [Char] -> [Char]
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 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
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 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
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 ([Char] -> [Char]) -> [Char] -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char] -> [Char]
forall r. PrintfType r => [Char] -> r
printf [Char]
"%s %s" (Op -> [Char]
opToLH Op
op) ([[Char]] -> [Char]
unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (RuntimeTerm -> [Char]) -> [RuntimeTerm] -> [[Char]]
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]
"    " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
L.intercalate [Char]
"\n=== " ([[Char]]
proofSteps [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [Bool -> RuntimeTerm -> [Char]
toLH Bool
False RuntimeTerm
result]) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"\n*** QED"
  where
    proofSteps :: [String]
    proofSteps :: [[Char]]
proofSteps = (Step Rewrite RuntimeTerm a -> Int -> [Char])
-> [Step Rewrite RuntimeTerm a] -> [Int] -> [[Char]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((Step Rewrite RuntimeTerm a, Int) -> [Char])
-> Step Rewrite RuntimeTerm a -> Int -> [Char]
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Step Rewrite RuntimeTerm a, Int) -> [Char]
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 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" ? " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ HashMap [Char] RuntimeTerm -> [Char]
forall {a}. Ord a => HashMap a RuntimeTerm -> [Char]
toLemma HashMap [Char] RuntimeTerm
lemma
      where
        lemma :: HashMap [Char] RuntimeTerm
lemma = [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
-> HashMap [Char] RuntimeTerm
go (RuntimeTerm -> [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
subTerms RuntimeTerm
t)

        lemmaName :: Text
lemmaName = Text -> ([Char] -> Text) -> Maybe [Char] -> Text
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) (((a, RuntimeTerm) -> RuntimeTerm)
-> [(a, RuntimeTerm)] -> [RuntimeTerm]
forall a b. (a -> b) -> [a] -> [b]
map (a, RuntimeTerm) -> RuntimeTerm
forall a b. (a, b) -> b
snd ([(a, RuntimeTerm)] -> [RuntimeTerm])
-> [(a, RuntimeTerm)] -> [RuntimeTerm]
forall a b. (a -> b) -> a -> b
$ [(a, RuntimeTerm)] -> [(a, RuntimeTerm)]
forall a. Ord a => [a] -> [a]
L.sort ([(a, RuntimeTerm)] -> [(a, RuntimeTerm)])
-> [(a, RuntimeTerm)] -> [(a, RuntimeTerm)]
forall a b. (a -> b) -> a -> b
$ HashMap a RuntimeTerm -> [(a, RuntimeTerm)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap a RuntimeTerm
s))

        go :: [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
-> HashMap [Char] RuntimeTerm
go []            = HashMap [Char] RuntimeTerm
forall a. HasCallStack => a
undefined
        go ((RuntimeTerm
st, RuntimeTerm -> RuntimeTerm
f): [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
_) | Just HashMap [Char] RuntimeTerm
su <- MetaTerm
-> RuntimeTerm
-> HashMap [Char] RuntimeTerm
-> Maybe (HashMap [Char] RuntimeTerm)
unify MetaTerm
lhs RuntimeTerm
st HashMap [Char] RuntimeTerm
forall k v. HashMap k v
M.empty
                        , RuntimeTerm -> RuntimeTerm
f (HashMap [Char] RuntimeTerm -> MetaTerm -> RuntimeTerm
subst HashMap [Char] RuntimeTerm
su MetaTerm
rhs) RuntimeTerm -> RuntimeTerm -> Bool
forall a. Eq a => a -> a -> Bool
== RuntimeTerm
nextTerm
                        = HashMap [Char] RuntimeTerm
su
        go ((RuntimeTerm, RuntimeTerm -> RuntimeTerm)
_:[(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
xs)       = [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
-> HashMap [Char] RuntimeTerm
go [(RuntimeTerm, RuntimeTerm -> RuntimeTerm)]
xs

        nextTerm :: RuntimeTerm
nextTerm = if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< ([Step Rewrite RuntimeTerm a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Step Rewrite RuntimeTerm a]
steps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) then (PathTerm Rewrite RuntimeTerm -> RuntimeTerm
forall rule term. PathTerm rule term -> term
pathTerm (PathTerm Rewrite RuntimeTerm -> RuntimeTerm)
-> (Step Rewrite RuntimeTerm a -> PathTerm Rewrite RuntimeTerm)
-> Step Rewrite RuntimeTerm a
-> RuntimeTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Step Rewrite RuntimeTerm a -> PathTerm Rewrite RuntimeTerm
forall rule term a. Step rule term a -> PathTerm rule term
term) ([Step Rewrite RuntimeTerm a]
steps [Step Rewrite RuntimeTerm a] -> Int -> Step Rewrite RuntimeTerm a
forall a. HasCallStack => [a] -> Int -> a
!! (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) else RuntimeTerm
result