| Line No. | Rev | Author | Line |
|---|---|---|---|
| 1 | 7 | paulosilva | |
| 2 | {-# OPTIONS_GHC -Wall #-} | ||
| 3 | |||
| 4 | ------------------------------------------------------------------------------- | ||
| 5 | |||
| 6 | {- | | ||
| 7 | Module : Galculator.StepEval | ||
| 8 | Description : | ||
| 9 | Copyright : (c) Paulo Silva | ||
| 10 | License : LGPL | ||
| 11 | |||
| 12 | Maintainer : paufil@di.uminho.pt | ||
| 13 | Stability : experimental | ||
| 14 | Portability : portable | ||
| 15 | |||
| 16 | -} | ||
| 17 | |||
| 18 | ------------------------------------------------------------------------------- | ||
| 19 | |||
| 20 | module Galculator.StepEval ( | ||
| 21 | stepEval | ||
| 22 | ) where | ||
| 23 | |||
| 24 | import Control.GalcError | ||
| 25 | import Control.Monad.Error | ||
| 26 | import Control.Monad.Fresh | ||
| 27 | import Data.Existential | ||
| 28 | import Galculator.Evaluate | ||
| 29 | import Galculator.Rule | ||
| 30 | import Galculator.State | ||
| 31 | import Galculator.Proof | ||
| 32 | import Language.Law.Syntax | ||
| 33 | import Language.R.Equality | ||
| 34 | import Language.R.Match | ||
| 35 | import qualified Language.R.Refresh as RR | ||
| 36 | import Language.R.SafeCast | ||
| 37 | import Language.R.Syntax | ||
| 38 | import Language.R.SyntaxADT | ||
| 39 | import qualified Language.R.TypeInference as RI | ||
| 40 | import qualified Language.R.Verify as RV | ||
| 41 | import Language.Step.Syntax | ||
| 42 | import Language.Type.Constraint | ||
| 43 | import Language.Type.Syntax | ||
| 44 | import Language.Type.Unification | ||
| 45 | |||
| 46 | ------------------------------------------------------------------------------- | ||
| 47 | |||
| 48 | eitherId :: Either a a -> a | ||
| 49 | eitherId = either id id | ||
| 50 | |||
| 51 | ------------------------------------------------------------------------------- | ||
| 52 | |||
| 53 | eitherFunct :: (a -> c) -> (b -> d) -> Either a b -> Either c d | ||
| 54 | eitherFunct f g = either (Left . f) (Right . g) | ||
| 55 | |||
| 56 | ------------------------------------------------------------------------------- | ||
| 57 | |||
| 58 | compileR :: S -> GalcStateT RType | ||
| 59 | compileR s = do | ||
| 60 | env <- getEnvironment | ||
| 61 | RI.infer =<< RR.refresh =<< RV.verify env s | ||
| 62 | |||
| 63 | ------------------------------------------------------------------------------- | ||
| 64 | stepEval :: Step -> GalcStateT () | ||
| 65 | ------------------------------------------------------------------------------- | ||
| 66 | stepEval (Comb comb) = | ||
| 67 | inMode [ProofMode, IndirectProofMode] $ updateProof $ \prf -> do | ||
| 68 | rl <- evalCombinator comb | ||
| 69 | Exists t r <- getCurExpr | ||
| 70 | return $ maybe prf | ||
| 71 | (\(expr, proof) -> | ||
| 72 | prf {curExpr = eitherFunct (const (Exists t expr)) (const (Exists t expr)) (curExpr prf), | ||
| 73 | curProof = addStep (RewriteStep (eitherId (curExpr prf)) proof) (curProof prf)}) (rewrite rl t r) | ||
| 74 | ------------------------------------------------------------------------------- | ||
| 75 | stepEval (Indirect ord'') = inMode [ProofMode] $ (updateProof $ \prf -> do | ||
| 76 | let cexpr = eitherId . curExpr $ prf | ||
| 77 | ord' <- either compileR compileR ord'' | ||
| 78 | let ord = either (const (Left ord')) (const (Right ord')) ord'' | ||
| 79 | nexpr <- either (auxLeft cexpr) (auxRight cexpr) ord | ||
| 80 | return $ prf { | ||
| 81 | curExpr = eitherFunct (const nexpr) (const nexpr) (curExpr prf), | ||
| 82 | curProof = addStep (IndirectProof cexpr ord []) (curProof prf) } ) | ||
| 83 | >> enterIndirectProofMode | ||
| 84 | where | ||
| 85 | auxLeft :: RType -> RType -> GalcStateT RType | ||
| 86 | auxLeft (Exists te e) (Exists to o) = do | ||
| 87 | t1 <- getFreshLift (TVar . ('t':)); t2 <- getFreshLift (TVar . ('t':)) | ||
| 88 | constr <- unify [to :=: Ord t2, te :=: Fun t2 t1] | ||
| 89 | Hide t1' <- typeRewrite constr t1 | ||
| 90 | Hide t2' <- typeRewrite constr t2 | ||
| 91 | o' <- rCast constr (Ord t2') o | ||
| 92 | e' <- rCast constr (Fun t2' t1') e | ||
| 93 | return $ Exists (Rel t2' t1') (COMP t2' (ORD o') (FUN e')) | ||
| 94 | auxRight :: RType -> RType -> GalcStateT RType | ||
| 95 | auxRight (Exists te e) (Exists to o) = do | ||
| 96 | t1 <- getFreshLift (TVar . ('t':)); t2 <- getFreshLift (TVar . ('t':)) | ||
| 97 | constr <- unify [to :=: Ord t2, te :=: Fun t2 t1] | ||
| 98 | Hide t1' <- typeRewrite constr t1 | ||
| 99 | Hide t2' <- typeRewrite constr t2 | ||
| 100 | o' <- rCast constr (Ord t2') o | ||
| 101 | e' <- rCast constr (Fun t2' t1') e | ||
| 102 | return $ Exists (Rel t1' t2') (COMP t2' (CONV (FUN e')) (ORD o')) | ||
| 103 | ------------------------------------------------------------------------------- | ||
| 104 | stepEval IndirectEnd = inMode [IndirectProofMode] $ (updateProof $ \prf -> do | ||
| 105 | let cexpr = eitherId . curExpr $ prf | ||
| 106 | ord <- getOrd . curProof $ prf | ||
| 107 | nexpr <- either (auxLeft cexpr) (auxRight cexpr) ord | ||
| 108 | return $ prf {curExpr = eitherFunct (const nexpr) (const nexpr) (curExpr prf), | ||
| 109 | curProof = addStep QED (curProof prf)}) >> enterProofMode | ||
| 110 | where | ||
| 111 | auxLeft :: RType -> RType -> GalcStateT RType | ||
| 112 | auxLeft (Exists te e) (Exists to o) = do | ||
| 113 | t1 <- getFreshLift (TVar . ('t':)); t2 <- getFreshLift (TVar . ('t':)) | ||
| 114 | constr <- unify [to :=: Ord t2, te :=: Rel t2 t1] | ||
| 115 | Hide t1' <- typeRewrite constr t1 | ||
| 116 | Hide t2' <- typeRewrite constr t2 | ||
| 117 | o' <- rCast constr (Ord t2') o | ||
| 118 | e' <- rCast constr (Rel t2' t1') e | ||
| 119 | r <- getFreshLift (Var . ('r':)) | ||
| 120 | rConstr <- rMatch (COMP t2' (ORD o') (FUN r)) e' | ||
| 121 | let r' = rSubst rConstr (Fun t2' t1') r | ||
| 122 | return $ Exists (Fun t2' t1') r' | ||
| 123 | auxRight :: RType -> RType -> GalcStateT RType | ||
| 124 | auxRight (Exists te e) (Exists to o) = do | ||
| 125 | t1 <- getFreshLift (TVar . ('t':)); t2 <- getFreshLift (TVar . ('t':)) | ||
| 126 | constr <- unify [to :=: Ord t2, te :=: Rel t1 t2] | ||
| 127 | Hide t1' <- typeRewrite constr t1 | ||
| 128 | Hide t2' <- typeRewrite constr t2 | ||
| 129 | o' <- rCast constr (Ord t2') o | ||
| 130 | e' <- rCast constr (Rel t1' t2') e | ||
| 131 | r <- getFreshLift (Var . ('r':)) | ||
| 132 | rConstr <- rMatch (COMP t2' (CONV (FUN r)) (ORD o')) e' | ||
| 133 | let r' = rSubst rConstr (Fun t2' t1') r | ||
| 134 | return $ Exists (Fun t2' t1') r' | ||
| 135 | ------------------------------------------------------------------------------- | ||
| 136 | stepEval LeftP = inMode [SetProofMode] $ (updateProof $ \prf -> | ||
| 137 | return $ prf {curExpr = Left $ getLeft (expression prf)}) >> enterProofMode | ||
| 138 | ------------------------------------------------------------------------------- | ||
| 139 | stepEval Qed = inMode [ProofMode] $ (updateProof $ \prf -> | ||
| 140 | either (aux getRight prf) (aux getLeft prf) (curExpr prf)) >> | ||
| 141 | enterFinalProofMode | ||
| 142 | where | ||
| 143 | aux f p expr = | ||
| 144 | if req' expr (f (expression p)) | ||
| 145 | then return $ p {curProof = addStep QED (curProof p)} | ||
| 146 | else throwError $ QedError (show expr) (show (f (expression p))) | ||
| 147 | req' (Exists _ r) (Exists _ r') = req r r' | ||
| 148 | ------------------------------------------------------------------------------- | ||
| 149 | stepEval RightP = inMode [SetProofMode] $ (updateProof $ \prf -> | ||
| 150 | return $ prf {curExpr = Right $ getRight (expression prf)}) >> enterProofMode | ||
| 151 | ------------------------------------------------------------------------------- | ||
| 152 | stepEval (SeqC s1 s2) = | ||
| 153 | stepEval s1 >> stepEval s2 | ||
| 154 | ------------------------------------------------------------------------------- |