diff --git a/app/Main.hs b/app/Main.hs index 8b4303ee..41e6a689 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,5 +1,6 @@ -{-# LANGUAGE OverloadedStrings #-} + {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} module Main where @@ -8,7 +9,7 @@ import Pretty () import System.Console.GetOpt import System.Environment import Prelude -import Server (run) +import Server (runOnPort, runOnStdio) main :: IO () main = do @@ -16,10 +17,10 @@ main = do case mode of ModeHelp -> putStrLn $ usageInfo usage options ModeLSP -> do - _ <- run False port + _ <- runOnStdio "/Users/vince/Documents/gcl-vscode/server_log.txt" return () ModeDev -> do - _ <- run True port + _ <- runOnPort port return () -------------------------------------------------------------------------------- diff --git a/examples/divmod.gcl b/examples/divmod.gcl index 3390b328..c05d10c8 100644 --- a/examples/divmod.gcl +++ b/examples/divmod.gcl @@ -6,6 +6,10 @@ var q, b, r : Int b := B { PowOf2 b, bnd: A - b } do b ≤ A -> b := b * 2 od + +[! + +!] { PowOf2 b ∧ b > A } q, r := 0, A diff --git a/examples/factor.gcl b/examples/factor.gcl index 8bd88a15..f6ff84de 100644 --- a/examples/factor.gcl +++ b/examples/factor.gcl @@ -3,9 +3,15 @@ var p, x, y, n : Int var mod : Int -> Int -> Int {: P = x * y + p = N - Q = x > 0 ∧ y > 0 + Q = x > 0 ∧ y > 0 ∧ 1 > 0 :} +p := p + 1 +[! +!] +[! + +!] p,x,y := N-1, 1, 1 { P ∧ Q, bnd: p } diff --git a/examples/fastmul_with_holes.gcl b/examples/fastmul_with_holes.gcl new file mode 100644 index 00000000..4a8136c9 --- /dev/null +++ b/examples/fastmul_with_holes.gcl @@ -0,0 +1,30 @@ +con A, B : Int { A ≥ 0 ∧ B ≥ 0 } +con even, odd : Int -> Bool +var r, a, b : Int + +{: INV = a * b + r = A * B ∧ 0 ≤ b :} + +a, b, r := A, B, 0 +{ INV, bnd: b } +do b ≠ 0 -> + if even b -> + b := b / 2 + | odd b -> + a := 3 + a := 3 + [! + + !] + [! + ? + + !] + r := a + fi +od +{ r = A * B } + + + + + diff --git a/gcl.cabal b/gcl.cabal index 0c698b48..e3165b9b 100644 --- a/gcl.cabal +++ b/gcl.cabal @@ -36,7 +36,7 @@ library GCL.WP.Explanation GCL.WP.SP GCL.WP.Struct - GCL.WP.Type + GCL.WP.Types GCL.WP.Util GCL.WP.WP Pretty @@ -45,6 +45,7 @@ library Pretty.Concrete Pretty.Error Pretty.Predicate + Pretty.Typed Pretty.Util Pretty.Variadic Render @@ -54,34 +55,26 @@ library Render.Predicate Render.Syntax.Abstract Render.Syntax.Common + Render.Syntax.Typed Server - Server.CustomMethod Server.GoToDefn Server.Handler Server.Handler.AutoCompletion - Server.Handler.CustomMethod - Server.Handler.Diagnostic - Server.Handler.GoToDefn + Server.Handler.GoToDefinition + Server.Handler.Guabao.Refine + Server.Handler.Guabao.Reload Server.Handler.Hover - Server.Handler2 - Server.Handler2.CustomMethod - Server.Handler2.CustomMethod.HelloWorld - Server.Handler2.CustomMethod.InsertProofTemplate - Server.Handler2.CustomMethod.Inspect - Server.Handler2.CustomMethod.Refine - Server.Handler2.CustomMethod.Reload - Server.Handler2.CustomMethod.SubstituteRedex - Server.Handler2.CustomMethod.Utils - Server.Handler2.GoToDefinition - Server.Handler2.Hover - Server.Handler2.Initialized - Server.Handler2.SemanticTokens - Server.Handler2.Utils + Server.Handler.Initialized + Server.Handler.OnDidChangeTextDocument + Server.Handler.SemanticTokens Server.Highlighting Server.Hover Server.IntervalMap + Server.Load Server.Monad - Server.Pipeline + Server.Notification.Error + Server.Notification.Update + Server.PositionMapping Server.SrcLoc Syntax.Abstract Syntax.Abstract.Instances.Json @@ -105,16 +98,24 @@ library Syntax.Parser.Util Syntax.Substitution Syntax.Typed + Syntax.Typed.Instances.Free + Syntax.Typed.Instances.Located + Syntax.Typed.Instances.Substitution + Syntax.Typed.Operator + Syntax.Typed.Types + Syntax.Typed.Util other-modules: Paths_gcl hs-source-dirs: src ghc-options: -Wall -Werror=incomplete-patterns -fno-warn-orphans build-depends: - aeson + Diff + , aeson , base >=4.7 && <5 , bytestring , containers + , deepseq , free , hashable , lens @@ -145,10 +146,12 @@ executable gcl app ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N -Werror=incomplete-patterns -fno-warn-orphans build-depends: - aeson + Diff + , aeson , base >=4.7 && <5 , bytestring , containers + , deepseq , free , gcl , hashable @@ -202,7 +205,7 @@ test-suite gcl-test GCL.WP.Explanation GCL.WP.SP GCL.WP.Struct - GCL.WP.Type + GCL.WP.Types GCL.WP.Util GCL.WP.WP Pretty @@ -211,6 +214,7 @@ test-suite gcl-test Pretty.Concrete Pretty.Error Pretty.Predicate + Pretty.Typed Pretty.Util Pretty.Variadic Render @@ -220,34 +224,26 @@ test-suite gcl-test Render.Predicate Render.Syntax.Abstract Render.Syntax.Common + Render.Syntax.Typed Server - Server.CustomMethod Server.GoToDefn Server.Handler Server.Handler.AutoCompletion - Server.Handler.CustomMethod - Server.Handler.Diagnostic - Server.Handler.GoToDefn + Server.Handler.GoToDefinition + Server.Handler.Guabao.Refine + Server.Handler.Guabao.Reload Server.Handler.Hover - Server.Handler2 - Server.Handler2.CustomMethod - Server.Handler2.CustomMethod.HelloWorld - Server.Handler2.CustomMethod.InsertProofTemplate - Server.Handler2.CustomMethod.Inspect - Server.Handler2.CustomMethod.Refine - Server.Handler2.CustomMethod.Reload - Server.Handler2.CustomMethod.SubstituteRedex - Server.Handler2.CustomMethod.Utils - Server.Handler2.GoToDefinition - Server.Handler2.Hover - Server.Handler2.Initialized - Server.Handler2.SemanticTokens - Server.Handler2.Utils + Server.Handler.Initialized + Server.Handler.OnDidChangeTextDocument + Server.Handler.SemanticTokens Server.Highlighting Server.Hover Server.IntervalMap + Server.Load Server.Monad - Server.Pipeline + Server.Notification.Error + Server.Notification.Update + Server.PositionMapping Server.SrcLoc Syntax.Abstract Syntax.Abstract.Instances.Json @@ -271,16 +267,24 @@ test-suite gcl-test Syntax.Parser.Util Syntax.Substitution Syntax.Typed + Syntax.Typed.Instances.Free + Syntax.Typed.Instances.Located + Syntax.Typed.Instances.Substitution + Syntax.Typed.Operator + Syntax.Typed.Types + Syntax.Typed.Util Paths_gcl hs-source-dirs: test src ghc-options: -Wall -Werror=incomplete-patterns -fno-warn-orphans build-depends: - aeson + Diff + , aeson , base >=4.7 && <5 , bytestring , containers + , deepseq , directory , filepath , free diff --git a/log.txt b/log.txt new file mode 100644 index 00000000..5b062eaa --- /dev/null +++ b/log.txt @@ -0,0 +1,22 @@ +=== Log file Start === +SInitialized is called. +STextDocumentDidOpen is called. +load start +load start +load start 2 +load start 3 +loaded file state +current version determined +load: source read +load: file read +load: source parsed +load: swept +load: elaborated +load: fileState created +load: fileState saved +STextDocumentDidOpen is finished. + + ---> Syntax Highlighting + ---> Syntax Highlighting + ---> Syntax Highlighting + ---> Syntax Highlighting<-- Goto Definition \ No newline at end of file diff --git a/package.yaml b/package.yaml index f88551e9..53ee4aed 100644 --- a/package.yaml +++ b/package.yaml @@ -1,15 +1,15 @@ -name: gcl -version: 0.1.0.0 +name: gcl +version: 0.1.0.0 #synopsis: #description: -homepage: https://github.com/scmlab/gcl -license: BSD3 -author: Author name here -maintainer: banacorn@gmail.com -copyright: something -category: language +homepage: https://github.com/scmlab/gcl +license: BSD3 +author: Author name here +maintainer: banacorn@gmail.com +copyright: something +category: language extra-source-files: -- README.md + - README.md dependencies: - base >= 4.7 && < 5 @@ -30,12 +30,14 @@ dependencies: - regex-applicative - random - vector - - lsp + - lsp - lens - multiset - transformers - template-haskell - multistate + - deepseq + - Diff library: source-dirs: src @@ -60,7 +62,6 @@ executables: - -Werror=incomplete-patterns - -fno-warn-orphans - tests: gcl-test: main: Test.hs diff --git a/src/Data/Loc/Range.hs b/src/Data/Loc/Range.hs index 537499c3..523e9ae3 100644 --- a/src/Data/Loc/Range.hs +++ b/src/Data/Loc/Range.hs @@ -6,7 +6,7 @@ module Data.Loc.Range where import Data.Aeson ( FromJSON(..) - , ToJSON(..) + , ToJSON(..), object, (.=), withObject, (.:) ) import qualified Data.List as List import Data.List.NonEmpty ( NonEmpty ) @@ -166,18 +166,30 @@ instance Ranged (R a) where -- | Make Pos instances of FromJSON and ToJSON instance ToJSON Pos where - toJSON (Pos filepath line column offset) = - toJSON (filepath, line, column, offset) + toJSON (Pos file line col byte) = + object [ "file" .= file + , "line" .= line + , "column" .= col + , "byte" .= byte + ] instance FromJSON Pos where - parseJSON v = do - (filepath, line, column, offset) <- parseJSON v - return $ Pos filepath line column offset + parseJSON = withObject "Pos" $ \v -> + Pos <$> v .: "file" + <*> v .: "line" + <*> v .: "column" + <*> v .: "byte" -- | Make Range instances of FromJSON and ToJSON -instance FromJSON Range - -instance ToJSON Range +instance FromJSON Range where + parseJSON = withObject "Range" $ \v -> + Range <$> v .: "start" + <*> v .: "end" +instance ToJSON Range where + toJSON (Range start end) = + object [ "start" .= start + , "end" .= end + ] -------------------------------------------------------------------------------- diff --git a/src/Error.hs b/src/Error.hs index 12ad0450..fdf1f8d7 100644 --- a/src/Error.hs +++ b/src/Error.hs @@ -3,10 +3,11 @@ module Error where import GCL.Type ( TypeError ) -import GCL.WP.Type ( StructError ) +import GCL.WP.Types ( StructError ) import GHC.Generics import Syntax.Common ( ) import Syntax.Parser.Error ( ParseError ) +import qualified Data.Aeson.Types as JSON -------------------------------------------------------------------------------- @@ -17,4 +18,5 @@ data Error | StructError StructError | CannotReadFile FilePath | Others String - deriving (Eq, Show, Generic) + deriving (Eq, Show) + diff --git a/src/GCL/Common.hs b/src/GCL/Common.hs index b706ea2e..ad626234 100644 --- a/src/GCL/Common.hs +++ b/src/GCL/Common.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleInstances, UndecidableInstances, MultiParamTypeClasses, FlexibleContexts #-} +{-# LANGUAGE DeriveGeneric #-} module GCL.Common where import Control.Monad.RWS ( RWST(..) ) @@ -16,10 +17,26 @@ import qualified Data.Text as Text import Data.Loc.Range ( Range ) import Syntax.Abstract import Syntax.Common.Types +import GHC.Generics data Index = Index Name | Hole Range deriving (Eq, Show, Ord) +data TypeInfo = + TypeDefnCtorInfo Type + | ConstTypeInfo Type + | VarTypeInfo Type + deriving (Eq, Show, Generic) + +toTypeEnv :: [(Index, TypeInfo)] -> TypeEnv +toTypeEnv infos = + (\(index, info) -> + case info of + TypeDefnCtorInfo ty -> (index, ty) + ConstTypeInfo ty -> (index, ty) + VarTypeInfo ty -> (index, ty) + ) <$> infos + type TypeEnv = [(Index, Type)] -- get a fresh variable @@ -35,6 +52,9 @@ freshName prefix l = Name <$> freshPre prefix <*> pure l freshName' :: Fresh m => Text -> m Name freshName' prefix = freshName prefix NoLoc +freshNames :: Fresh m => [Text] -> m [Name] +freshNames = mapM freshName' + class Counterous m where countUp :: m Int @@ -106,7 +126,7 @@ instance Free Type where freeVars (TMetaVar n ) = Set.singleton n instance {-# OVERLAPS #-} Free TypeEnv where - freeVars env = foldMap freeVars $ Map.elems $ Map.fromList env + freeVars env = foldMap freeVars $ Map.elems $ Map.fromList env instance Free Expr where freeVars (Var x _ ) = Set.singleton x diff --git a/src/GCL/Predicate.hs b/src/GCL/Predicate.hs index 54d6cfe1..1a3ed337 100644 --- a/src/GCL/Predicate.hs +++ b/src/GCL/Predicate.hs @@ -3,6 +3,7 @@ module GCL.Predicate where import Data.Aeson ( ToJSON ) +import qualified Data.Aeson as JSON import Data.Loc ( L , Loc(..) , Located(locOf) @@ -17,9 +18,12 @@ import qualified Data.Set as Set import GHC.Generics ( Generic ) import GCL.Common import Render.Element -import Syntax.Abstract ( Expr ) +import Syntax.Typed ( Expr ) import Syntax.Common ( Name ) +-- | A predicate is an expression, whose type happens to be Bool. +type Pred = Expr +{- -- | Predicates data Pred = Constant Expr @@ -90,7 +94,7 @@ instance Eq Stmt where If l xs == If m ys = l == m && xs == ys Spec l _ == Spec m _ = l == m _ == _ = False - +-} -------------------------------------------------------------------------------- -- | Proof obligation @@ -109,10 +113,14 @@ instance Ord PO where instance Located PO where locOf (PO _ _ _ _ o) = locOf o +-- instance ToJSON PO + data InfMode = Primary -- the main inference mode | Secondary -- non-functional postconditions. ignore assertions deriving (Eq, Show, Generic) +instance ToJSON InfMode + data Origin = AtAbort Loc | AtSkip Loc @@ -158,11 +166,12 @@ data Spec = Specification , specPreCond :: Pred , specPostCond :: Pred , specRange :: Range + , specTypeEnv :: [(Index, TypeInfo)] } deriving (Eq, Show, Generic) instance Located Spec where - locOf (Specification _ _ _ l) = locOf l + locOf (Specification _ _ _ l _) = locOf l instance Ranged Spec where - rangeOf (Specification _ _ _ r) = r + rangeOf (Specification _ _ _ r _) = r diff --git a/src/GCL/Predicate/Located.hs b/src/GCL/Predicate/Located.hs index ea35757b..68c9acce 100644 --- a/src/GCL/Predicate/Located.hs +++ b/src/GCL/Predicate/Located.hs @@ -1,9 +1,9 @@ module GCL.Predicate.Located where import Data.Loc (Located, locOf, Loc (..)) -import GCL.Predicate (Pred (..), Stmt (..)) - +import GCL.Predicate (Pred (..)) +{- instance Located Pred where locOf (Constant _) = NoLoc locOf (GuardIf _ l) = l @@ -22,10 +22,10 @@ instance Located Stmt where locOf (Do l _ _) = locOf l locOf (If l _) = locOf l locOf (Spec l _) = locOf l - +-} -- instance Ord Loc where -- compare NoLoc NoLoc = EQ -- compare NoLoc (Loc _ _) = LT -- compare (Loc _ _) NoLoc = GT --- compare (Loc x _) (Loc y _) = compare x y \ No newline at end of file +-- compare (Loc x _) (Loc y _) = compare x y diff --git a/src/GCL/Predicate/Util.hs b/src/GCL/Predicate/Util.hs index f3b1017a..3da5f054 100644 --- a/src/GCL/Predicate/Util.hs +++ b/src/GCL/Predicate/Util.hs @@ -9,7 +9,7 @@ import GCL.Predicate.Located () import Syntax.Abstract (Expr) import qualified Syntax.Abstract.Operator as A import Data.Loc.Range (Range(Range)) - +{- toExpr :: Pred -> Expr toExpr (Constant e) = e toExpr (Bound e _) = e @@ -63,19 +63,19 @@ precond (Assign l _ _) = unLoc l precond (Do l _ _) = unLoc l precond (If l _) = unLoc l precond (Spec l _) = unLoc l - +-} -- | Return lines within a Spec without indentation specPayloadWithoutIndentation :: Text -> Spec -> [Text] specPayloadWithoutIndentation source spec = let Range start end = specRange spec spansMultipleLines = posLine start /= posLine end - in if spansMultipleLines - then + in if spansMultipleLines + then let payload = Text.drop (posCoff start) $ Text.take (posCoff end) source linesWithIndentation = init $ tail $ Text.lines payload splittedIndentedLines = map (Text.break (not . Char.isSpace)) linesWithIndentation smallestIndentation = minimum $ map (Text.length . fst) splittedIndentedLines trimmedLines = map (\(indentation, content) -> Text.drop smallestIndentation indentation <> content) splittedIndentedLines in trimmedLines - else - [Text.strip $ Text.drop (posCoff start + 2) $ Text.take (posCoff end - 2) source] \ No newline at end of file + else + [Text.strip $ Text.drop (posCoff start + 2) $ Text.take (posCoff end - 2) source] diff --git a/src/GCL/Substitution.hs b/src/GCL/Substitution.hs index 492ce2b9..720a45e4 100644 --- a/src/GCL/Substitution.hs +++ b/src/GCL/Substitution.hs @@ -1,22 +1,8 @@ {-# LANGUAGE FlexibleInstances, FlexibleContexts, - OverloadedStrings, LambdaCase #-} + OverloadedStrings, LambdaCase, MonoLocalBinds #-} -module GCL.Substitution - ( run - , buildRedexMap - , step - , Decls - -- TODO: don't export these - , Substitutable - , Reducible - , CollectRedexes - ) where +module GCL.Substitution where -import Control.Monad.RWS -import Data.Foldable ( toList ) -import qualified Data.IntMap as IntMap -import Data.IntMap ( IntMap ) -import qualified Data.List.NonEmpty as NonEmpty import Data.Loc ( locOf ) import Data.Map ( Map ) import qualified Data.Map as Map @@ -25,328 +11,47 @@ import qualified Data.Set as Set import Data.Set ( Set ) import Data.Text ( Text ) import GCL.Common ( Free(freeVars) - , Counterous(..) + -- , Counterous(..) , Fresh(..) - , FreshState + -- , FreshState , freshPre ) -import GCL.Predicate ( PO(PO) - , Pred(..) - ) -import Syntax.Abstract ( Chain(..) - , CaseClause(..) - , Expr(..) - , FuncClause(..) - , Mapping - , Pattern(..) - , extractBinder - ) +-- import GCL.Predicate ( PO(PO) +-- , Pred(..) +-- ) +-- import Syntax.Abstract ( Chain(..) +-- , CaseClause(..) +-- , Expr(..) +-- , FuncClause(..) +-- , Mapping +-- , Pattern(..) +-- , extractBinder +-- ) +import qualified Syntax.Abstract as A +import qualified Syntax.Typed as T import Syntax.Common ( Name(Name) , nameToText ) ------------------------------------------------------------------ -run - :: MonadState FreshState m - => (Substitutable a, Reducible a, CollectRedexes a) - => Decls -- declarations - -- -> Int -- initial redex ID counter - -> [Name] -- name of variables to be substituted - -> [Expr] -- values to be substituted for - -> a - -> m (a, IntMap (Int, Expr)) -run decls names exprs predicate = runM decls $ do - output <- subst mapping predicate >>= reduce - return (output, buildRedexMap output) - where - mapping :: Mapping - mapping = mappingFromSubstitution names exprs - -buildRedexMap :: CollectRedexes a => a -> IntMap (Int, Expr) -buildRedexMap = IntMap.fromList . map (\(i, e) -> (i, (i, e))) . collectRedexes +syntaxSubst :: [Name] -> [T.Expr] -> T.Expr -> T.Expr +syntaxSubst xs es e = T.Subst e (zip xs es) + -- SCM: For now. A lot more to do. -step :: MonadState FreshState m => Decls -> Expr -> m Expr -step decls expr = runM decls $ go expr - where - go :: Expr -> M Expr - go (App f x l) = App <$> go f <*> pure x <*> pure l >>= reduce - go (RedexKernel _ value _ mappings) = - foldM (flip subst) value (reverse $ toList mappings) >>= reduce - go (RedexShell _ e) = go e - go others = return others +------------------------------------------------------------------ +type Mapping = Map Text A.Expr -mappingFromSubstitution :: [Name] -> [Expr] -> Mapping +mappingFromSubstitution :: [Name] -> [A.Expr] -> Mapping mappingFromSubstitution xs es = Map.mapKeys nameToText $ Map.fromList $ zip xs es ------------------------------------------------------------------- - -type Decls = Map Text (Maybe Expr) -type M = RWS Decls () Int - -instance Counterous M where - countUp = do i <- get - put (succ i) - return i - -runM :: MonadState FreshState m => Decls -> M b -> m b -runM decls p = do - counter <- get - let (output, counter', _) = runRWS p decls counter - put counter' - return output - ------------------------------------------------------------------- - -class CollectRedexes a where - collectRedexes :: a -> [(Int, Expr)] - -instance CollectRedexes PO where - collectRedexes (PO pre post _ _ _) = - collectRedexes pre <> collectRedexes post - -instance CollectRedexes Pred where - collectRedexes predicate = case predicate of - Constant x -> collectRedexes x - GuardIf x _ -> collectRedexes x - GuardLoop x _ -> collectRedexes x - Assertion x _ -> collectRedexes x - LoopInvariant x y _ -> collectRedexes x <> collectRedexes y - Bound x _ -> collectRedexes x - Conjunct xs -> xs >>= collectRedexes - Disjunct xs -> xs >>= collectRedexes - Negate x -> collectRedexes x - -instance CollectRedexes Expr where - collectRedexes expr = case expr of - App x y _ -> collectRedexes x <> collectRedexes y - Lam _ x _ -> collectRedexes x - Quant _ _ _ x _ -> collectRedexes x - RedexKernel{} -> [] - RedexShell i e -> [(i, e)] - ArrIdx x y _ -> collectRedexes x <> collectRedexes y - ArrUpd x y z _ -> collectRedexes x <> collectRedexes y <> collectRedexes z - Case _ xs _ -> xs >>= collectRedexes - _ -> [] - -instance CollectRedexes CaseClause where - collectRedexes (CaseClause _ x) = collectRedexes x - ------------------------------------------------------------------- - - -class Reducible a where - reduce :: a -> M a - -instance Reducible Expr where - -- perform substitution when there's a redex - reduce expr = case expr of - App f x l1 -> do - f' <- reduce f - x' <- reduce x - case f' of - RedexShell _ e -> RedexShell <$> countUp <*> reduce (App e x' l1) - Lam n body _ -> subst (mappingFromSubstitution [n] [x']) body - _ -> return $ App f' x' l1 - Lam binder body l -> Lam binder <$> reduce body <*> return l - Quant op binders range body l -> - Quant op binders range <$> reduce body <*> return l - RedexShell i e -> RedexShell i <$> reduce e - ArrIdx array index l -> ArrIdx <$> reduce array <*> reduce index <*> pure l - ArrUpd array index value l -> - ArrUpd <$> reduce array <*> reduce index <*> reduce value <*> pure l - _ -> return expr - -instance Reducible Pred where - reduce = \case - Constant a -> Constant <$> reduce a - GuardIf a l -> GuardIf <$> reduce a <*> pure l - GuardLoop a l -> GuardLoop <$> reduce a <*> pure l - Assertion a l -> Assertion <$> reduce a <*> pure l - LoopInvariant a b l -> LoopInvariant <$> reduce a <*> reduce b <*> pure l - Bound a l -> Bound <$> reduce a <*> pure l - Conjunct as -> Conjunct <$> mapM reduce as - Disjunct as -> Disjunct <$> mapM reduce as - Negate a -> Negate <$> reduce a - ------------------------------------------------------------------- - -class Substitutable a where - subst :: Mapping -> a -> M a - -instance Substitutable Expr where - subst mapping expr = case expr of - - Lit{} -> return expr - - Var name _ -> case Map.lookup (nameToText name) mapping of - Just value -> return value - Nothing -> do - decls <- ask - index <- countUp - case Map.lookup (nameToText name) decls of - Just (Just binding) -> do - let e = RedexKernel - name - binding - (freeVars binding) - -- NonEmpty.singleton is only available after base-4.15 - (NonEmpty.fromList [shrinkMapping binding mapping]) - return $ RedexShell index e - Just Nothing -> return expr - Nothing -> return expr - - Const name _ -> case Map.lookup (nameToText name) mapping of - Just value -> reduce value - Nothing -> do - decls <- ask - index <- countUp - case Map.lookup (nameToText name) decls of - Just (Just binding) -> do - let e = RedexKernel - name - binding - (freeVars binding) - -- NonEmpty.singleton is only available after base-4.15 - (NonEmpty.fromList [shrinkMapping binding mapping]) - return $ RedexShell index e - Just Nothing -> return expr - Nothing -> return expr - - Op{} -> return expr - - Chain ch -> Chain <$> subst mapping ch - - App f x l -> App <$> subst mapping f <*> subst mapping x <*> pure l - - Lam binder body l -> do - - -- we need to rename binders to avoid capturing - -- only the free vars that is also present in `body` will be renamed - let (capturableNames, shrinkedMapping) = - getCapturableNamesAndShrinkMapping mapping body - - -- rename captured binder - renamings <- produceBinderRenamings capturableNames [binder] - let renamedBinder = renameBinder renamings binder - - Lam renamedBinder - <$> subst (renamingToMapping renamings <> shrinkedMapping) body - <*> pure l - - Func name clauses l -> - Func name <$> mapM (subst mapping) clauses <*> pure l - - Tuple es -> Tuple <$> mapM (subst mapping) es - - Quant op binders range body l -> do - -- rename binders to avoid capturing only when necessary! - let (capturableNames, shrinkedMapping) = - getCapturableNamesAndShrinkMapping mapping expr - - -- rename captured binder - renamings <- produceBinderRenamings capturableNames binders - let renamedBinders = map (renameBinder renamings) binders - - Quant op renamedBinders - <$> subst (renamingToMapping renamings <> shrinkedMapping) range - <*> subst (renamingToMapping renamings <> shrinkedMapping) body - <*> pure l - - -- apply new mappings on the outside instead of merging them (Issue #54) - -- NOTE: - -- when shrinking the applied outer new mapping - -- free variables occured from the inner old mapping - -- should be taken into consideration - RedexKernel name e fv mappings -> - let - removeSubstitutedVars :: Mapping -> Set Name -> Set Name - removeSubstitutedVars m = - Set.filter (\v -> not $ Set.member (nameToText v) (Map.keysSet m)) - - - outermostMapping = NonEmpty.head mappings - - fv' = - fv <> Set.unions (map freeVars $ Map.elems outermostMapping) - newFreeVars = removeSubstitutedVars mapping fv - <> Set.unions (map freeVars $ Map.elems outermostMapping) - - shrinkedMapping = - Map.restrictKeys mapping (Set.map nameToText fv') - in - return $ RedexKernel name - e - newFreeVars - (NonEmpty.cons shrinkedMapping mappings) - - RedexShell _ e -> RedexShell <$> countUp <*> subst mapping e - - ArrIdx array index l -> - ArrIdx <$> subst mapping array <*> subst mapping index <*> pure l - - ArrUpd array index value l -> - ArrUpd - <$> subst mapping array - <*> subst mapping index - <*> subst mapping value - <*> pure l - - -- apply subst on body of cases only - Case e cases l -> do - cases' <- forM cases - $ \(CaseClause patt body) -> CaseClause patt <$> subst mapping body - return $ Case e cases' l - -instance Substitutable Chain where - subst mapping ch = case ch of - Pure expr loc -> Pure <$> subst mapping expr <*> pure loc - More ch' op expr loc -> More <$> subst mapping ch' <*> pure op <*> subst mapping expr <*> pure loc - -instance Substitutable FuncClause where - subst mapping (FuncClause patterns body) = do - -- we need to rename binders to avoid capturing - -- only the free vars that is also present in `body` will be renamed - let (capturableNames, shrinkedMapping) = - getCapturableNamesAndShrinkMapping mapping body - - -- renaming captured binders in patterns - let bindersInPatterns = patterns >>= extractBinder - renamings <- produceBinderRenamings capturableNames bindersInPatterns - let renamedPatterns = map (renameBindersInPattern renamings) patterns - - FuncClause renamedPatterns - <$> subst (renamingToMapping renamings <> shrinkedMapping) body - -renameBindersInPattern :: Map Name Name -> Pattern -> Pattern -renameBindersInPattern renamings patt = case patt of - PattLit _ -> patt - PattBinder binder -> PattBinder $ renameBinder renamings binder - PattWildcard _ -> patt - PattConstructor name patts -> - PattConstructor name $ map (renameBindersInPattern renamings) patts - -instance Substitutable Pred where - subst mapping = \case - Constant a -> Constant <$> subst mapping a - GuardIf a l -> GuardIf <$> subst mapping a <*> pure l - GuardLoop a l -> GuardLoop <$> subst mapping a <*> pure l - Assertion a l -> Assertion <$> subst mapping a <*> pure l - LoopInvariant a b l -> - LoopInvariant <$> subst mapping a <*> subst mapping b <*> pure l - Bound a l -> Bound <$> subst mapping a <*> pure l - Conjunct as -> Conjunct <$> mapM (subst mapping) as - Disjunct as -> Disjunct <$> mapM (subst mapping) as - Negate a -> Negate <$> subst mapping a - ------------------------------------------------------------------- -- produce a binder "renaming", if any binder is in the set of "capturableNames" -produceBinderRenamings :: Set Text -> [Name] -> M (Map Name Name) +produceBinderRenamings :: Fresh m => Set Text -> [Name] -> m (Map Name Name) produceBinderRenamings capturableNames binders = mconcat <$> mapM go binders where - go :: Name -> M (Map Name Name) + go :: Fresh m => Name -> m (Map Name Name) go binder = if Set.member (nameToText binder) capturableNames then do -- CAPTURED! returns the alpha renamed binder @@ -366,14 +71,14 @@ renameBinder renamings binder = renamingToMapping :: Map Name Name -> Mapping renamingToMapping = Map.fromList - . map (\(old, new) -> (nameToText old, Var new (locOf old))) + . map (\(old, new) -> (nameToText old, A.Var new (locOf old))) . Map.toList ------------------------------------------------------------------ -- | Perform Alpha renaming only when necessary -- returns a set of free names that is susceptible to capturing -- also returns a Mapping that is reduced further with only free variables in "body" -getCapturableNamesAndShrinkMapping :: Mapping -> Expr -> (Set Text, Mapping) +getCapturableNamesAndShrinkMapping :: Mapping -> A.Expr -> (Set Text, Mapping) getCapturableNamesAndShrinkMapping mapping body = let -- collect all free variables in "body" @@ -390,7 +95,7 @@ getCapturableNamesAndShrinkMapping mapping body = ------------------------------------------------------------------ -- | Shrink the Mapping in Substs -shrinkMapping :: Expr -> Mapping -> Mapping +shrinkMapping :: A.Expr -> Mapping -> Mapping shrinkMapping expr mapping = let -- collect all free variables in the expression diff --git a/src/GCL/Type.hs b/src/GCL/Type.hs index 06fcf0a4..d429210f 100644 --- a/src/GCL/Type.hs +++ b/src/GCL/Type.hs @@ -40,7 +40,7 @@ import Prelude hiding ( EQ import Syntax.Abstract import Syntax.Abstract.Util import Syntax.Common -import qualified Syntax.Typed as Typed +import qualified Syntax.Typed as T data TypeError = NotInScope Name @@ -54,8 +54,6 @@ data TypeError | MissingArguments [Name] deriving (Show, Eq, Generic) -instance ToJSON TypeError - instance Located TypeError where locOf (NotInScope n ) = locOf n locOf (UnifyFailed _ _ l ) = l @@ -67,12 +65,6 @@ instance Located TypeError where locOf (RedundantExprs exprs) = locOf exprs locOf (MissingArguments ns ) = locOf ns -data TypeInfo = - TypeDefnCtorInfo Type - | ConstTypeInfo Type - | VarTypeInfo Type - deriving (Eq, Show) - instance Substitutable Type TypeInfo where subst s (TypeDefnCtorInfo t) = TypeDefnCtorInfo (subst s t) subst s (ConstTypeInfo t) = ConstTypeInfo (subst s t) @@ -91,6 +83,7 @@ duplicationCheck ns = -------------------------------------------------------------------------------- -- The elaboration monad +-- TODO: It seems the TypeInfo is not necessary. Refactor it. type ElaboratorM = StateT (FreshState, [(Index, TypeDefnInfo)], [(Index, TypeInfo)]) (Except TypeError) instance Counterous ElaboratorM where @@ -100,9 +93,9 @@ instance Counterous ElaboratorM where return count runElaboration - :: Elab a => a -> Either TypeError (Typed a) -runElaboration a = do - ((_, elaborated, _), _state) <- runExcept (runStateT (elaborate a mempty) (0, mempty, mempty)) + :: Elab a => a -> [(Index, TypeInfo)] -> Either TypeError (Typed a) +runElaboration a env = do + ((_, elaborated, _), _state) <- runExcept (runStateT (elaborate a env) (0, mempty, mempty)) Right elaborated -------------------------------------------------------------------------------- @@ -129,7 +122,7 @@ instance CollectIds [Definition] where duplicationCheck $ ((\(FuncDefn name _) -> name) <$> funcDefns) <> gatherCtorNames typeDefns -- Gather the type definitions. -- Type definitions are collected first because signatures and function definitions may depend on them. - collectTypeDefns typeDefns + collectTypeDefns typeDefns -- Add signatures into the state one by one. collectFuncSigs funcSigs -- Get the original explicit signatures. @@ -145,15 +138,14 @@ instance CollectIds [Definition] where let gathered = second ConstTypeInfo <$> zip defined freshVars modify (\(freshState, typeDefnInfos, origInfos) -> (freshState, typeDefnInfos, gathered <> origInfos)) -- Get the previously gathered type infos. - (_, _, infos') <- get - let env = second typeInfoToType <$> infos' + (_, _, env) <- get -- Do a `foldlM` to elaborate multiple definitions together. (_, names, tys, _sub) <- foldlM (\(context, names, tys, sub) funcDefn -> do case funcDefn of (FuncDefn name expr) -> do - (ty, _, sub1) <- elaborate expr context -- Calling `head` is safe for the meantime. - unifySub <- unifies (subst sub1 (fromJust $ lookup (Index name) context)) (fromJust ty) (locOf name) -- the first `fromJust` should also be safe. + (ty, _, sub1) <- elaborate expr context + unifySub <- unifies (typeInfoToType $ subst sub1 (fromJust $ lookup (Index name) context)) (fromJust ty) (locOf name) -- the first `fromJust` should also be safe. -- We see if there are signatures restricting the type of function definitions. case lookup (Index name) sigEnv of -- If there is, we save the restricted type. @@ -166,7 +158,7 @@ instance CollectIds [Definition] where ) (env, mempty, mempty, mempty) funcDefns -- Generalize the types of definitions, i.e. change free type variables into metavariables. mapM_ (\(name, ty) -> do - ty' <- generalize ty env -- TODO: Why??? + ty' <- generalize ty (second typeInfoToType <$> env) -- TODO: Why??? let info = (Index name, ConstTypeInfo ty') modify (\(freshState, typeDefnInfos, origInfos) -> (freshState, typeDefnInfos, info : origInfos)) ) (zip names tys) @@ -178,7 +170,7 @@ instance CollectIds [Definition] where d @ FuncDefnSig {} -> (typeDefns, d : sigs, funcDefns) d @ FuncDefn {} -> (typeDefns, sigs, d : funcDefns) ) mempty defs - + gatherCtorNames :: [Definition] -> [Name] gatherCtorNames defs = do def <- defs @@ -210,7 +202,7 @@ instance CollectIds [Definition] where collectFuncSigs :: [Definition] -> ElaboratorM () collectFuncSigs funcSigs = - mapM_ (\(FuncDefnSig n t _ _) -> do + mapM_ (\(FuncDefnSig n t _ _) -> do let infos = (Index n, ConstTypeInfo t) modify (\(freshState, typeDefnInfos, origInfos) -> (freshState, typeDefnInfos, infos : origInfos)) ) funcSigs @@ -235,14 +227,14 @@ instance CollectIds Declaration where -- The type family `Typed` turns data into its typed version. type family Typed untyped where - Typed Definition = Typed.TypedDefinition - Typed Declaration = Typed.TypedDeclaration - Typed TypeDefnCtor = Typed.TypedTypeDefnCtor - Typed Program = Typed.TypedProgram - Typed Stmt = Typed.TypedStmt - Typed GdCmd = Typed.TypedGdCmd - Typed Expr = Typed.TypedExpr - Typed Chain = Typed.TypedChain + Typed Definition = T.Definition + Typed Declaration = T.Declaration + Typed TypeDefnCtor = T.TypeDefnCtor + Typed Program = T.Program + Typed Stmt = T.Stmt + Typed GdCmd = T.GdCmd + Typed Expr = T.Expr + Typed Chain = T.Chain Typed Name = Name Typed ChainOp = Op Typed ArithOp = Op @@ -254,13 +246,13 @@ type family Typed untyped where Typed (Maybe a) = Maybe (Typed a) class Located a => Elab a where - elaborate :: a -> TypeEnv -> ElaboratorM (Maybe Type, Typed a, Subs Type) + elaborate :: a -> [(Index, TypeInfo)] -> ElaboratorM (Maybe Type, Typed a, Subs Type) -- Note that we pass the collected ids into each sections of the program. -- After `collectIds`, we don't need to change the state. instance Elab Program where - elaborate (Program defns decls exprs stmts loc) _env = do + elaborate (Program defns decls exprs stmts loc) env = do mapM_ collectIds decls -- The `reverse` here shouldn't be needed now. In the past, it was a trick to make things work. -- I still keep it as-is in case of future refactoring / rewriting. @@ -269,26 +261,26 @@ instance Elab Program where modify (\(freshState, origInfos, typeInfos) -> (freshState, tcons <> origInfos, typeInfos)) (_, _, infos) <- get typedDefns <- mapM (\defn -> do - typedDefn <- elaborate defn $ second typeInfoToType <$> infos + typedDefn <- elaborate defn $ env <> infos let (_, typed, _) = typedDefn return typed ) defns typedDecls <- mapM (\decl -> do - typedDecl <- elaborate decl $ second typeInfoToType <$> infos + typedDecl <- elaborate decl $ env <> infos let (_, typed, _) = typedDecl return typed ) decls typedExprs <- mapM (\expr -> do - typedExpr <- elaborate expr $ second typeInfoToType <$> infos + typedExpr <- elaborate expr $ env <> infos let (_, typed, _) = typedExpr return typed ) exprs typedStmts <- mapM (\stmt -> do - typedStmt <- elaborate stmt $ second typeInfoToType <$> infos + typedStmt <- elaborate stmt $ env <> infos let (_, typed, _) = typedStmt return typed ) stmts - return (Nothing, Typed.Program typedDefns typedDecls typedExprs typedStmts loc, mempty) + return (Nothing, T.Program typedDefns typedDecls typedExprs typedStmts loc, mempty) where collectTCon (TypeDefn n args _ _) = [(Index n, TypeDefnInfo args)] collectTCon _ = [] @@ -301,7 +293,7 @@ instance Elab Definition where (_, typed, _) <- elaborate ctor env return typed ) ctors - return (Nothing, Typed.TypeDefn name args ctors' loc, mempty) + return (Nothing, T.TypeDefn name args ctors' loc, mempty) where scopeCheck :: MonadError TypeError m => Set.Set Name -> Name -> m () scopeCheck m n = if Set.member n m then return () else throwError $ NotInScope n @@ -310,28 +302,28 @@ instance Elab Definition where (_, typed, _) <- elaborate expr env return typed ) maybeExpr - return (Nothing, Typed.FuncDefnSig name ty expr' loc, mempty) + return (Nothing, T.FuncDefnSig name ty expr' loc, mempty) elaborate (FuncDefn name expr) env = do (_, typed, _) <- elaborate expr env - return (Nothing, Typed.FuncDefn name typed, mempty) + return (Nothing, T.FuncDefn name typed, mempty) instance Elab TypeDefnCtor where elaborate (TypeDefnCtor name ts) _ = do - return (Nothing, Typed.TypedTypeDefnCtor name ts, mempty) + return (Nothing, T.TypeDefnCtor name ts, mempty) instance Elab Declaration where elaborate (ConstDecl names ty prop loc) env = case prop of Just p -> do (_, p', _) <- elaborate p env - return (Nothing, Typed.ConstDecl names ty (Just p') loc, mempty) - Nothing -> return (Nothing, Typed.ConstDecl names ty Nothing loc, mempty) + return (Nothing, T.ConstDecl names ty (Just p') loc, mempty) + Nothing -> return (Nothing, T.ConstDecl names ty Nothing loc, mempty) elaborate (VarDecl names ty prop loc) env = case prop of Just p -> do (_, p', _) <- elaborate p env - return (Nothing, Typed.VarDecl names ty (Just p') loc, mempty) - Nothing -> return (Nothing, Typed.VarDecl names ty Nothing loc, mempty) + return (Nothing, T.VarDecl names ty (Just p') loc, mempty) + Nothing -> return (Nothing, T.VarDecl names ty Nothing loc, mempty) -- This function is used during elaborating stmts. checkAssign :: [(Index, TypeInfo)] -> Name -> ElaboratorM Type @@ -342,8 +334,8 @@ checkAssign infos name = do Nothing -> throwError $ NotInScope name instance Elab Stmt where - elaborate (Skip loc ) _ = return (Nothing, Typed.Skip loc, mempty) - elaborate (Abort loc ) _ = return (Nothing, Typed.Abort loc, mempty) + elaborate (Skip loc ) _ = return (Nothing, T.Skip loc, mempty) + elaborate (Abort loc ) _ = return (Nothing, T.Abort loc, mempty) elaborate (Assign names exprs loc) env = do duplicationCheck names let ass = zip names exprs @@ -352,14 +344,13 @@ instance Elab Stmt where | an < length exprs -> throwError $ RedundantExprs (drop an exprs) | an < length names -> throwError $ RedundantNames (drop an names) | otherwise -> do - (_, _, infos) <- get exprs' <- mapM (\(name, expr) -> do - ty <- checkAssign infos name + ty <- checkAssign env name (ty', typedExpr, _) <- elaborate expr env _ <- unifies ty (fromJust ty') $ locOf expr return typedExpr ) ass - return (Nothing, Typed.Assign names exprs' loc, mempty) + return (Nothing, T.Assign names exprs' loc, mempty) elaborate (AAssign arr index e loc) env = do tv <- freshVar (arrTy, typedArr, arrSub) <- elaborate arr env @@ -368,12 +359,12 @@ instance Elab Stmt where uniSubArr <- unifies (subst (indexSub `compose` uniSubIndex) (fromJust arrTy)) (TFunc (tInt NoLoc) tv NoLoc) (locOf arr) (eTy, typedE, eSub) <- elaborate e $ subst (uniSubArr `compose` uniSubIndex `compose` indexSub `compose` arrSub) env _ <- unifies (subst eSub $ fromJust eTy) (subst uniSubArr tv) (locOf e) - return (Nothing, Typed.AAssign typedArr typedIndex typedE loc, mempty) + return (Nothing, T.AAssign typedArr typedIndex typedE loc, mempty) elaborate (Assert expr loc ) env = do (ty, _, sub) <- elaborate expr env _ <- unifies (subst sub $ fromJust ty) (tBool NoLoc) (locOf expr) (_, typedExpr, _) <- elaborate expr env - return (Nothing, Typed.Assert typedExpr loc, mempty) + return (Nothing, T.Assert typedExpr loc, mempty) elaborate (LoopInvariant e1 e2 loc) env = do (ty1, _, sub1) <- elaborate e1 env _ <- unifies (subst sub1 $ fromJust ty1) (tBool NoLoc) (locOf e1) @@ -381,24 +372,25 @@ instance Elab Stmt where (ty2, _, sub2) <- elaborate e2 env _ <- unifies (subst sub2 $ fromJust ty2) (tInt NoLoc) (locOf e2) (_, e2', _) <- elaborate e2 env - return (Nothing, Typed.LoopInvariant e1' e2' loc, mempty) + return (Nothing, T.LoopInvariant e1' e2' loc, mempty) elaborate (Do gds loc) env = do gds' <- mapM (\gd -> do (_, typed, _) <- elaborate gd env return typed ) gds - return (Nothing, Typed.Do gds' loc, mempty) + return (Nothing, T.Do gds' loc, mempty) elaborate (If gds loc) env = do gds' <- mapM (\gd -> do (_, typed, _) <- elaborate gd env return typed ) gds - return (Nothing, Typed.If gds' loc, mempty) - elaborate (Spec text range) _ = return (Nothing, Typed.Spec text range, mempty) - elaborate (Proof text1 text2 range) _ = return (Nothing, Typed.Proof text1 text2 range, mempty) - elaborate (Alloc var exprs loc) env = do + return (Nothing, T.If gds' loc, mempty) + elaborate (Spec text range) _ = do (_, _, infos) <- get - ty <- checkAssign infos var + return (Nothing, T.Spec text range infos, mempty) + elaborate (Proof text1 text2 range) _ = return (Nothing, T.Proof text1 text2 range, mempty) + elaborate (Alloc var exprs loc) env = do + ty <- checkAssign env var _ <- unifies ty (tInt NoLoc) $ locOf var typedExprs <- mapM @@ -407,24 +399,23 @@ instance Elab Stmt where _ <- unifies (fromJust ty') (tInt NoLoc) (locOf expr) return typedExpr ) exprs - return (Nothing, Typed.Alloc var typedExprs loc, mempty) + return (Nothing, T.Alloc var typedExprs loc, mempty) elaborate (HLookup name expr loc) env = do - (_, _, infos) <- get - ty <- checkAssign infos name + ty <- checkAssign env name _ <- unifies ty (tInt NoLoc) $ locOf name (ty', typedExpr, _) <- elaborate expr env _ <- unifies (fromJust ty') (tInt NoLoc) (locOf expr) - return (Nothing, Typed.HLookup name typedExpr loc, mempty) + return (Nothing, T.HLookup name typedExpr loc, mempty) elaborate (HMutate left right loc) env = do (ty, typedLeft, _) <- elaborate left env _ <- unifies (fromJust ty) (tInt NoLoc) (locOf left) (ty', typedRight, _) <- elaborate right env _ <- unifies (fromJust ty') (tInt NoLoc) (locOf right) - return (Nothing, Typed.HMutate typedLeft typedRight loc, mempty) + return (Nothing, T.HMutate typedLeft typedRight loc, mempty) elaborate (Dispose expr loc) env = do (ty, typedExpr, _) <- elaborate expr env _ <- unifies (fromJust ty) (tInt NoLoc) (locOf expr) - return (Nothing, Typed.Dispose typedExpr loc, mempty) + return (Nothing, T.Dispose typedExpr loc, mempty) elaborate Block {} env = undefined -- TODO: Implement blocks. instance Elab GdCmd where @@ -436,7 +427,7 @@ instance Elab GdCmd where (_, typed, _) <- elaborate stmt env return typed ) stmts - return (Nothing, Typed.TypedGdCmd e' s' loc, mempty) + return (Nothing, T.GdCmd e' s' loc, mempty) instantiate :: Fresh m => Type -> m Type instantiate ty = do @@ -456,26 +447,26 @@ instantiate ty = do -- Γ ⊢ e : t ↓ (v . s) instance Elab Expr where - elaborate (Lit lit loc) _ = let ty = litTypes lit loc in return (Just ty, Typed.Lit lit ty loc, mempty) + elaborate (Lit lit loc) _ = let ty = litTypes lit loc in return (Just ty, T.Lit lit ty loc, mempty) -- x : t ∈ Γ -- t ⊑ u ---- Var, Const, Op -- -- Γ ⊢ x ↑ (∅, t) elaborate (Var x loc) env = case lookup (Index x) env of - Just ty -> do - ty' <- instantiate ty - return (Just ty', Typed.Var x ty' loc, mempty) + Just info -> do + ty' <- instantiate $ typeInfoToType info + return (Just ty', T.Var x ty' loc, mempty) Nothing -> throwError $ NotInScope x elaborate (Const x loc) env = case lookup (Index x) env of - Just ty -> do - ty' <- instantiate ty - return (Just ty', Typed.Const x ty' loc, mempty) + Just info -> do + ty' <- instantiate $ typeInfoToType info + return (Just ty', T.Const x ty' loc, mempty) Nothing -> throwError $ NotInScope x elaborate (Op o) env = do (ty, op, sub) <- elaborate o env ty' <- instantiate $ fromJust ty - return (Just ty', subst sub (Typed.Op op ty'), sub) - elaborate (Chain ch) env = (\(ty, typed, sub) -> (ty, Typed.Chain typed, sub)) <$> elaborate ch env + return (Just ty', subst sub (T.Op op ty'), sub) + elaborate (Chain ch) env = (\(ty, typed, sub) -> (ty, T.Chain typed, sub)) <$> elaborate ch env -- Γ ⊢ e1 ↑ (s1, t1) -- s1 Γ ⊢ e2 ↑ (s2, t2) -- b fresh v = unify (s2 t1, t2 -> b) @@ -487,17 +478,17 @@ instance Elab Expr where (ty2, typedExpr2, sub2) <- elaborate e2 $ subst sub1 env sub3 <- unifies (subst sub2 $ fromJust ty1) (TFunc (fromJust ty2) tv NoLoc) loc let sub = sub3 `compose` sub2 `compose` sub1 - return (Just $ subst sub3 tv, subst sub (Typed.App typedExpr1 typedExpr2 loc), sub) + return (Just $ subst sub3 tv, subst sub (T.App typedExpr1 typedExpr2 loc), sub) -- a fresh -- Γ, x : a ⊢ e ↑ (s, t) ---- Lam ---------------------- -- Γ ⊢ (λ x . e) ↑ (s, s a -> t) elaborate (Lam bound expr loc) env = do tv <- freshVar - let newEnv = (Index bound, tv) : env + let newEnv = (Index bound, ConstTypeInfo tv) : env (ty1, typedExpr1, sub1) <- elaborate expr newEnv let returnTy = TFunc (subst sub1 tv) (fromJust ty1) loc - return (Just returnTy, subst sub1 (Typed.Lam bound (subst sub1 tv) typedExpr1 loc), sub1) + return (Just returnTy, subst sub1 (T.Lam bound (subst sub1 tv) typedExpr1 loc), sub1) elaborate (Func name clauses l) env = undefined -- Γ ⊢ e1 ↑ (s1, t1) -- s1 Γ ⊢ e2 ↑ (s2, t2) @@ -512,12 +503,12 @@ instance Elab Expr where Op (Hash _) -> do tvs <- replicateM (length bound) freshVar let newEnv = subst quantSub env - (resTy, resTypedExpr, resSub) <- elaborate restriction $ zip (Index <$> bound) tvs <> newEnv + (resTy, resTypedExpr, resSub) <- elaborate restriction $ zip (Index <$> bound) (ConstTypeInfo <$> tvs) <> newEnv uniSub2 <- unifies (fromJust resTy) (tBool NoLoc) (locOf restriction) (innerTy, innerTypedExpr, innerSub) <- elaborate inner newEnv uniSub3 <- unifies (subst innerSub $ fromJust innerTy) (tBool NoLoc) (locOf inner) let sub = uniSub3 `compose` innerSub `compose` uniSub2 `compose` resSub `compose` quantSub - return (Just $ subst quantSub tv, subst sub (Typed.Quant quantTypedExpr bound resTypedExpr innerTypedExpr loc), sub) + return (Just $ subst quantSub tv, subst sub (T.Quant quantTypedExpr bound resTypedExpr innerTypedExpr loc), sub) -- a fresh Γ ⊢ ⊕ : (a -> a -> a) ↓ s⊕ -- b fresh s⊕ Γ, i : b ⊢ R : Bool ↓ sR -- sR (s⊕ Γ), i : sR b ⊢ B : sR (s⊕ a) ↓ sB @@ -527,13 +518,13 @@ instance Elab Expr where uniSub <- unifies (subst quantSub $ fromJust quantTy) (tv ~-> tv ~-> tv) (locOf quantifier) tvs <- replicateM (length bound) freshVar let newEnv = subst (uniSub `compose` quantSub) env - (resTy, resTypedExpr, resSub) <- elaborate restriction $ zip (Index <$> bound) tvs <> newEnv + (resTy, resTypedExpr, resSub) <- elaborate restriction $ zip (Index <$> bound) (ConstTypeInfo <$> tvs) <> newEnv uniSub2 <- unifies (fromJust resTy) (tBool NoLoc) (locOf restriction) let newEnv' = subst (uniSub2 `compose` resSub) newEnv - (innerTy, innerTypedExpr, innerSub) <- elaborate inner $ zip (Index <$> bound) (subst (uniSub2 `compose` resSub) <$> tvs) <> newEnv' + (innerTy, innerTypedExpr, innerSub) <- elaborate inner $ zip (Index <$> bound) (subst (uniSub2 `compose` resSub) . ConstTypeInfo <$> tvs) <> newEnv' uniSub3 <- unifies (subst innerSub $ fromJust innerTy) (subst (uniSub2 `compose` resSub `compose` uniSub `compose` quantSub) tv) (locOf inner) return (Just $ subst (uniSub3 `compose` innerSub `compose` uniSub2 `compose` resSub `compose` uniSub `compose` quantSub) tv, - subst (uniSub3 `compose` innerSub `compose` uniSub2 `compose` resSub `compose` uniSub `compose` quantSub) (Typed.Quant quantTypedExpr bound resTypedExpr innerTypedExpr loc), + subst (uniSub3 `compose` innerSub `compose` uniSub2 `compose` resSub `compose` uniSub `compose` quantSub) (T.Quant quantTypedExpr bound resTypedExpr innerTypedExpr loc), uniSub3 `compose` innerSub `compose` uniSub2 `compose` resSub) elaborate (RedexShell _ expr) env = undefined elaborate (RedexKernel n _ _ _) env = undefined @@ -548,7 +539,7 @@ instance Elab Expr where sub3 <- unifies (subst sub2 $ fromJust ty2) (tInt NoLoc) (locOf e2) sub4 <- unifies (subst (sub3 `compose` sub2) (fromJust ty1)) (TFunc (tInt NoLoc) tv NoLoc) loc let sub = sub4 `compose` sub3 `compose` sub2 `compose` sub1 - return (Just $ subst sub3 tv, subst sub (Typed.ArrIdx typedExpr1 typedExpr2 loc), sub) + return (Just $ subst sub3 tv, subst sub (T.ArrIdx typedExpr1 typedExpr2 loc), sub) -- b fresh Γ ⊢ a : Array .. of b ↓ sa -- sa Γ ⊢ i : Int ↓ si -- si (sa Γ) ⊢ e : si (sa b) ↓ se @@ -563,7 +554,7 @@ instance Elab Expr where (eTy, typedE, eSub) <- elaborate e $ subst (uniSubArr `compose` uniSubIndex `compose` indexSub `compose` arrSub) env uniSubExpr <- unifies (subst eSub $ fromJust eTy) (subst uniSubArr tv) (locOf e) let sub = uniSubExpr `compose` eSub `compose` uniSubArr `compose` uniSubIndex `compose` indexSub `compose` arrSub - return (subst uniSubArr arrTy, subst sub (Typed.ArrUpd typedArr typedIndex typedE loc), sub) + return (subst uniSubArr arrTy, subst sub (T.ArrUpd typedArr typedIndex typedE loc), sub) elaborate (Case expr cs l) env = undefined -- TODO: Implement pattern matching. instance Elab Chain where -- TODO: Make sure the below implementation is correct. @@ -576,7 +567,7 @@ instance Elab Chain where -- TODO: Make sure the below implementation is correct (ty2, typedExpr2, sub2) <- elaborate e2 $ subst (chainSub <> sub1) env unifyTy <- unifies (fromJust ty1 ~-> fromJust ty2 ~-> tv) opTy' loc2 let sub = chainSub <> opSub <> sub1 <> sub2 - return (Just $ subst unifyTy tv, subst sub $ Typed.More typedChain opTyped (subst unifyTy opTy') typedExpr2, sub) + return (Just $ subst unifyTy tv, subst sub $ T.More typedChain opTyped (subst unifyTy opTy') typedExpr2, sub) elaborate (More (Pure e1 _loc1) op e2 loc2) env = do tv <- freshVar (opTy, opTyped, opSub) <- elaborate op env @@ -585,7 +576,7 @@ instance Elab Chain where -- TODO: Make sure the below implementation is correct (ty2, typedExpr2, sub2) <- elaborate e2 $ subst sub1 env unifyTy <- unifies (fromJust ty1 ~-> fromJust ty2 ~-> tv) opTy' loc2 let sub = unifyTy <> sub2 <> sub1 <> opSub - return (Just $ subst unifyTy tv, subst sub $ Typed.More (Typed.Pure typedExpr1) opTyped (subst unifyTy opTy') typedExpr2, sub) + return (Just $ subst unifyTy tv, subst sub $ T.More (T.Pure typedExpr1) opTyped (subst unifyTy opTy') typedExpr2, sub) elaborate (Pure _expr _loc) _ = error "Chain of length 1 shouldn't exist." instance Elab ChainOp where @@ -733,18 +724,19 @@ instance Substitutable Type Type where subst s t@(TVar n _) = Map.findWithDefault t n s subst s t@(TMetaVar n) = Map.findWithDefault t n s -instance Substitutable Type Typed.TypedExpr where - subst s (Typed.Lit lit ty loc) = Typed.Lit lit (subst s ty) loc - subst s (Typed.Var name ty loc) = Typed.Var name (subst s ty) loc - subst s (Typed.Const name ty loc) = Typed.Const name (subst s ty) loc - subst s (Typed.Op op ty) = Typed.Op op $ subst s ty - subst s (Typed.Chain ch) = Typed.Chain $ subst s ch - subst s (Typed.App e1 e2 loc) = Typed.App (subst s e1) (subst s e2) loc - subst s (Typed.Lam name ty expr loc) = Typed.Lam name (subst s ty) (subst s expr) loc - subst s (Typed.Quant quantifier vars restriction inner loc) = Typed.Quant (subst s quantifier) vars (subst s restriction) (subst s inner) loc - subst s (Typed.ArrIdx arr index loc) = Typed.ArrIdx (subst s arr) (subst s index) loc - subst s (Typed.ArrUpd arr index expr loc) = Typed.ArrUpd (subst s arr) (subst s index) (subst s expr) loc - -instance Substitutable Type Typed.TypedChain where - subst s (Typed.Pure expr) = Typed.Pure $ subst s expr - subst s (Typed.More ch op ty expr) = Typed.More (subst s ch) op (subst s ty) (subst s expr) \ No newline at end of file +instance Substitutable Type T.Expr where + subst s (T.Lit lit ty loc) = T.Lit lit (subst s ty) loc + subst s (T.Var name ty loc) = T.Var name (subst s ty) loc + subst s (T.Const name ty loc) = T.Const name (subst s ty) loc + subst s (T.Op op ty) = T.Op op $ subst s ty + subst s (T.Chain ch) = T.Chain $ subst s ch + subst s (T.App e1 e2 loc) = T.App (subst s e1) (subst s e2) loc + subst s (T.Lam name ty expr loc) = T.Lam name (subst s ty) (subst s expr) loc + subst s (T.Quant quantifier vars restriction inner loc) = T.Quant (subst s quantifier) vars (subst s restriction) (subst s inner) loc + subst s (T.ArrIdx arr index loc) = T.ArrIdx (subst s arr) (subst s index) loc + subst s (T.ArrUpd arr index expr loc) = T.ArrUpd (subst s arr) (subst s index) (subst s expr) loc + subst s (T.Subst e es) = T.Subst (subst s e) [(x, subst s ex) | (x, ex) <- es] + +instance Substitutable Type T.Chain where + subst s (T.Pure expr) = T.Pure $ subst s expr + subst s (T.More ch op ty expr) = T.More (subst s ch) op (subst s ty) (subst s expr) diff --git a/src/GCL/WP.hs b/src/GCL/WP.hs index ff716dc0..35d7eb80 100644 --- a/src/GCL/WP.hs +++ b/src/GCL/WP.hs @@ -3,7 +3,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE LambdaCase #-} -module GCL.WP (WP, TM, sweep) where +module GCL.WP (WP, TM, sweep, structStmts, runWP) where import Control.Monad.Except ( MonadError(throwError) , runExcept @@ -16,40 +16,40 @@ import Data.Loc ( Located(..) ) import qualified Data.Map as Map import GCL.Predicate ( InfMode(..) , PO(..) - , Pred(..) + , Pred , Spec(..) ) -import qualified GCL.Substitution as Substitution -import GCL.WP.Type -import qualified Syntax.Abstract as A -import qualified Syntax.Abstract.Operator as A -import qualified Syntax.Abstract.Util as A +import Syntax.Typed +import Syntax.Typed.Operator ( true ) +import Syntax.Typed.Util ( declaredNames + , programToScopeForSubstitution ) import Syntax.Common.Types ( nameToText ) +import GCL.WP.Types import GCL.WP.Struct import GCL.WP.WP import GCL.WP.SP -import GCL.WP.Util runWP :: WP a - -> (Substitution.Decls, [[Text]]) + -> (Decls, [[Text]]) + -> Int -> Either StructError - (a, Int, ([PO], [Spec], [StructWarning], IntMap (Int, A.Expr))) -runWP p decls = runExcept $ runRWST p decls 0 + (a, Int, ([PO], [Spec], [StructWarning], IntMap (Int, Expr))) +runWP p decls counter = runExcept $ runRWST p decls counter sweep - :: A.Program - -> Either StructError ([PO], [Spec], [StructWarning], IntMap (Int, A.Expr), Int) -sweep program@(A.Program _ decs _props stmts _) = do - let decls = A.programToScopeForSubstitution program + :: Program + -> Either StructError ([PO], [Spec], [StructWarning], IntMap (Int, Expr), Int) +sweep program@(Program _ decs _props stmts _) = do + let decls = programToScopeForSubstitution program let dnames = [map nameToText $ declaredNames decs] (_, counter, (pos, specs, warnings, redexes)) <- - runWP (structProgram stmts) (decls, dnames) + runWP (structProgram stmts) (decls, dnames) 0 -- update Proof Obligations with corresponding Proof Anchors let proofAnchors = stmts >>= \case - A.Proof anchor _ r -> [(anchor,r)] - _ -> [] + Proof anchor _ r -> [(anchor,r)] + _ -> [] -- make a table of (#hash, range) from Proof Anchors let table = Map.fromList proofAnchors let updatePO po = case Map.lookup (poAnchorHash po) table of @@ -65,36 +65,33 @@ sweep program@(A.Program _ decs _props stmts _) = do data ProgView = ProgViewEmpty - | ProgViewOkay Pred [A.Stmt] Pred - | ProgViewMissingPrecondition [A.Stmt] Pred - | ProgViewMissingPostcondition Pred [A.Stmt] - | ProgViewMissingBoth [A.Stmt] + | ProgViewOkay Pred [Stmt] Pred + | ProgViewMissingPrecondition [Stmt] Pred + | ProgViewMissingPostcondition Pred [Stmt] + | ProgViewMissingBoth [Stmt] -progView :: [A.Stmt] -> ProgView +progView :: [Stmt] -> ProgView progView [] = ProgViewEmpty -progView [A.Assert pre l] = do - ProgViewMissingPrecondition [] (Assertion pre l) +progView [Assert pre _] = do + ProgViewMissingPrecondition [] pre progView stmts = do case (head stmts, last stmts) of - (A.Assert pre l, A.Assert post m) -> do - ProgViewOkay (Assertion pre l) - (init (tail stmts)) - (Assertion post m) - (A.Assert pre l, _) -> do - ProgViewMissingPostcondition (Assertion pre l) - (tail stmts) - (_, A.Assert post m) -> do - ProgViewMissingPrecondition (init stmts) (Assertion post m) + (Assert pre _, Assert post _) -> do + ProgViewOkay pre (init (tail stmts)) post + (Assert pre _, _) -> do + ProgViewMissingPostcondition pre (tail stmts) + (_, Assert post _) -> do + ProgViewMissingPrecondition (init stmts) post _ -> ProgViewMissingBoth stmts -structProgram :: [A.Stmt] -> WP () +structProgram :: [Stmt] -> WP () structProgram stmts = do case progView (removeLastProofs stmts) of ProgViewEmpty -> return () ProgViewOkay pre stmts' post -> structStmts Primary (pre, Nothing) stmts' post ProgViewMissingPrecondition stmts' post -> - structStmts Primary (Constant A.true, Nothing) stmts' post + structStmts Primary (true, Nothing) stmts' post ProgViewMissingPostcondition _ stmts' -> throwError . MissingPostcondition . locOf . last $ stmts' ProgViewMissingBoth stmts' -> @@ -102,17 +99,17 @@ structProgram stmts = do where -- ignore Proofs after the Postcondition - removeLastProofs :: [A.Stmt] -> [A.Stmt] + removeLastProofs :: [Stmt] -> [Stmt] removeLastProofs = List.dropWhileEnd isProof - isProof :: A.Stmt -> Bool - isProof A.Proof{} = True - isProof _ = False + isProof :: Stmt -> Bool + isProof Proof{} = True + isProof _ = False -- tying the knots -structStmts :: InfMode -> (Pred, Maybe A.Expr) -> [A.Stmt] -> Pred -> WP () +structStmts :: InfMode -> (Pred, Maybe Expr) -> [Stmt] -> Pred -> WP () structStmts = this where (this, structSegs, struct) = structFunctions (wpSegs, wpSStmts, diff --git a/src/GCL/WP/Explanation.hs b/src/GCL/WP/Explanation.hs index a5edd0cb..e25ed2df 100644 --- a/src/GCL/WP/Explanation.hs +++ b/src/GCL/WP/Explanation.hs @@ -4,7 +4,8 @@ module GCL.WP.Explanation where import Data.Loc import Data.Text (Text) -import Syntax.Abstract +import Syntax.Abstract.Operator ( tInt ) +import Syntax.Typed import Syntax.Common ( Name(..) ) import GCL.Predicate import Render @@ -59,7 +60,7 @@ explainTermination inv guards bnd l = Explain <> "remain true (that is, whilst looping), the bound" <> (codeE . render) bnd <> "should be greater then" - <> (codeE . render) (Lit (Num 0) NoLoc) + <> (codeE . render) (Lit (Num 0) tInt NoLoc) , originInfMode = Primary , originHighlightPartial = True , originLoc = l diff --git a/src/GCL/WP/SP.hs b/src/GCL/WP/SP.hs index 310727af..bd958589 100644 --- a/src/GCL/WP/SP.hs +++ b/src/GCL/WP/SP.hs @@ -6,36 +6,39 @@ import Control.Arrow ( first ) import Control.Monad.Except ( MonadError(throwError) , forM ) import Data.Loc ( Loc(..) ) -import GCL.Predicate ( Pred(..) ) -import GCL.Predicate.Util ( disjunct - , guardLoop - , toExpr - ) +import GCL.Predicate ( Pred ) import GCL.Common -import Pretty ( toText ) -import GCL.WP.Type -import GCL.WP.Util -import qualified Syntax.Abstract as A -import qualified Syntax.Abstract.Operator as A -import qualified Syntax.Abstract.Util as A -import Syntax.Common ( Name(Name) - , nameToText ) +import GCL.Substitution ( syntaxSubst ) +import GCL.WP.Types +import GCL.WP.Util +import Syntax.Typed +import Syntax.Typed.Operator ( true + , eqq + , nameVar + , neg + , disjunct + , conj + , conjunct + , exists ) +import Syntax.Typed.Util ( getGuards + , typeOf ) +import Syntax.Common ( nameToText ) spFunctions :: (TstructSegs, Tstruct) -> TspSStmts spFunctions (structSegs, struct) = spSStmts where - spStmts :: (Pred, Maybe A.Expr) -> [A.Stmt] -> WP Pred + spStmts :: (Pred, Maybe Expr) -> [Stmt] -> WP Pred spStmts (pre, bnd) = spSegs (pre, bnd) . groupStmts - spSegs :: (Pred, Maybe A.Expr) -> [SegElm] -> WP Pred + spSegs :: (Pred, Maybe Expr) -> [SegElm] -> WP Pred spSegs (pre, bnd) segs = case split segs of (ls, Nothing ) -> spSegs' (pre, bnd) ls - (ls, Just (SAsrt (A.Assert p l), rs)) -> do - structSegs (pre, bnd) ls (Assertion p l) - spSegs' (Assertion p l, Nothing) rs - (ls, Just (SAsrt (A.LoopInvariant p bd l), rs)) -> do - structSegs (pre, bnd) ls (Assertion p l) - spSegs' (Assertion p l, Just bd) rs + (ls, Just (SAsrt (Assert p _), rs)) -> do + structSegs (pre, bnd) ls p + spSegs' (p, Nothing) rs + (ls, Just (SAsrt (LoopInvariant p bd _), rs)) -> do + structSegs (pre, bnd) ls p + spSegs' (p, Just bd) rs (_, _) -> error "missing case in spSegs" where split :: [SegElm] -> ([SegElm], Maybe (SegElm, [SegElm])) @@ -47,71 +50,62 @@ spFunctions (structSegs, struct) = spSStmts (ls, r@(Just _)) -> (s : ls, r) -- spSeg' deals with a block with no assertions - spSegs' :: (Pred, Maybe A.Expr) -> [SegElm] -> WP Pred + spSegs' :: (Pred, Maybe Expr) -> [SegElm] -> WP Pred spSegs' (pre', _ ) [] = return pre' spSegs' (pre', bnd') (SStmts ss : segs') = do pre'' <- spSStmts (pre', bnd') ss spSegs' (pre'', Nothing) segs' - spSegs' (pre', bnd') (SSpec (A.Spec _ range) : segs') = do - tellSpec pre' pre' range + spSegs' (pre', bnd') (SSpec (Spec _ range tenv) : segs') = do + tellSpec pre' pre' tenv range spSegs' (pre', bnd') segs' spSegs' _ _ = error "missing case in spSegs'" -- the "simple" version - spSStmts :: (Pred, Maybe A.Expr) -> [A.Stmt] -> WP Pred + spSStmts :: (Pred, Maybe Expr) -> [Stmt] -> WP Pred spSStmts (pre, _ ) [] = return pre spSStmts (pre, bnd) (stmt : stmts) = do pre' <- sp (pre, bnd) stmt spSStmts (pre', Nothing) stmts - sp :: (Pred, Maybe A.Expr) -> A.Stmt -> WP Pred - sp (_ , _) (A.Abort _ ) = return (Constant A.true) + sp :: (Pred, Maybe Expr) -> Stmt -> WP Pred + sp (_ , _) (Abort _ ) = return true - sp (pre, _) (A.Skip _ ) = return pre + sp (pre, _) (Skip _ ) = return pre - sp (pre, _) (A.Assign xs es l) = do + sp (pre, _) (Assign xs es _) = do -- {P} x := E { (exists x' :: x = E[x'/x] && P[x'/x]) } -- generate fresh names from the assignees "xs" - freshNames <- forM xs $ \x -> do - x' <- freshPre (toText x) - return $ Name x' NoLoc - let freshVars = map (`A.Var` l) freshNames + freNames <- freshNames (map nameToText xs) + let freVars = zipWith nameVar freNames (map typeOf es) -- substitute "xs"s with fresh names in "pre" - pre' <- substitute xs freshVars (toExpr pre) + let pre' = syntaxSubst xs freVars pre + let pairs = zip freVars es + let predicates = [x `eqq` syntaxSubst xs freVars e | (x, e) <- pairs] + return $ exists freNames (conjunct predicates) pre' - -- - let pairs = zip xs es - predicates <- forM pairs $ \(x, e) -> do - e' <- substitute xs freshVars e - return $ A.nameVar x `A.eqq` e' - return $ Constant (A.exists freshNames (A.conjunct predicates) pre') - - sp (pre, _) (A.AAssign (A.Var x _) i e _) = do + sp (pre, _) (AAssign (Var x t _) i e _) = do -- {P} x[I] := E { (exist x' :: x = x'[I[x'/x] -> E[x'/x]] && P[x'/x]) } - x' <- freshPre (nameToText x) - - pre' <- substitute [x] [A.variable x'] (toExpr pre) - i' <- substitute [x] [A.variable x'] i - e' <- substitute [x] [A.variable x'] e - - return $ Constant - (A.exists [Name x' NoLoc] - (A.nameVar x `A.eqq` A.ArrUpd (A.variable x') i' e' NoLoc) + xn <- freshName' (nameToText x) + let x' = nameVar xn t + let pre' = syntaxSubst [x] [x'] pre + let i' = syntaxSubst [x] [x'] i + let e' = syntaxSubst [x] [x'] e + return $ exists [xn] + (nameVar x t `eqq` ArrUpd x' i' e' NoLoc) pre' - ) - sp (_ , _) (A.AAssign _ _ _ l) = throwError (MultiDimArrayAsgnNotImp l) + sp (_ , _) (AAssign _ _ _ l) = throwError (MultiDimArrayAsgnNotImp l) - sp (pre, _) (A.If gcmds _ ) = do - posts <- forM gcmds $ \(A.GdCmd guard body _) -> - Constant - . toExpr - <$> spStmts (Constant (guard `A.conj` toExpr pre), Nothing) body + sp (pre, _) (If gcmds _ ) = do + posts <- forM gcmds $ \(GdCmd guard body _) -> + spStmts (guard `conj` pre, Nothing) body return (disjunct posts) - sp (pre, bnd) (A.Do gcmds l) = do - let guards = A.getGuards gcmds - let post = Conjunct (pre : map (Negate . guardLoop) guards) - struct (pre, bnd) (A.Do gcmds l) post + + sp (pre, bnd) (Do gcmds l) = do + let guards = getGuards gcmds + let post = conjunct (pre : map neg guards) + struct (pre, bnd) (Do gcmds l) post return post + sp (pre, _) _ = return pre diff --git a/src/GCL/WP/Struct.hs b/src/GCL/WP/Struct.hs index d86e9cbc..c2de4746 100644 --- a/src/GCL/WP/Struct.hs +++ b/src/GCL/WP/Struct.hs @@ -11,37 +11,33 @@ import Data.Loc ( Loc(..) import Data.Loc.Range ( fromLoc ) import Data.Map ( fromList ) import GCL.Predicate ( InfMode(..) - , Origin(..) - , Pred(..) - ) -import GCL.Predicate.Util ( guardIf - , guardLoop - ) + , Pred + , Origin(..)) import GCL.Common ( freshName ) -import GCL.WP.Type -import GCL.WP.Explanation -import GCL.WP.Util -import qualified Syntax.Abstract as A -import qualified Syntax.Abstract.Operator as A -import qualified Syntax.Abstract.Util as A -import Syntax.Common.Types ( Name(..) - , nameToText ) +import GCL.WP.Types +import GCL.WP.Explanation +import GCL.WP.Util +import Syntax.Abstract.Operator ( tInt ) +import Syntax.Typed +import Syntax.Typed.Util ( getGuards, declaredNamesTypes ) +import Syntax.Typed.Operator ( eqq , gte , lt, neg + , disjunct + , conj, conjunct + ) +import Syntax.Typed.Instances.Substitution () +import Syntax.Common.Types ( Name(..), nameToText ) import Syntax.Substitution --- import Debug.Trace --- import Prettyprinter --- import Prettyprinter.Render.String - type RecFns = (TwpSegs, TwpSStmts, Twp, TspSStmts) structFunctions :: (TwpSegs, TwpSStmts, Twp, TspSStmts) -> (TstructStmts, TstructSegs, Tstruct) structFunctions (wpSegs, wpSStmts, wp, spSStmts) = - (structStmts, structSegs, struct) + (structStmts, structSegs, struct) where - structStmts :: InfMode -> (Pred, Maybe A.Expr) -> [A.Stmt] -> Pred -> WP () + structStmts :: InfMode -> (Pred, Maybe Expr) -> [Stmt] -> Pred -> WP () structStmts Primary pre stmts post = structSegs pre (groupStmts stmts) post structStmts Secondary (pre, _) stmts post = case stripAsserts stmts of Nothing -> return () -- skip if the program is incomplete @@ -52,46 +48,44 @@ structFunctions (wpSegs, wpSStmts, wp, spSStmts) = post' (emptyExplain "Assertion (Secondary)" (locOf pre)) - structSegs :: (Pred, Maybe A.Expr) -> [SegElm] -> Pred -> WP () + structSegs :: (Pred, Maybe Expr) -> [SegElm] -> Pred -> WP () structSegs (pre, _) [] post = do case locOf pre of NoLoc -> tellPO pre post (AtAssertion (locOf post)) others -> tellPO pre post (AtAssertion others) - structSegs (pre, _) (SAsrt (A.Assert p l) : segs) post = do - let assert = Assertion p l - tellPO pre assert (AtAssertion (locOf pre)) - structSegs (assert, Nothing) segs post - structSegs (pre, _) (SAsrt (A.LoopInvariant p bnd l) : segs) post = do - let loopInv = LoopInvariant p bnd l - tellPO pre loopInv origin - structSegs (loopInv, Just bnd) segs post + structSegs (pre, _) (SAsrt (Assert p _) : segs) post = do + tellPO pre p (AtAssertion (locOf pre)) + structSegs (p, Nothing) segs post + structSegs (pre, _) (SAsrt (LoopInvariant p bnd l) : segs) post = do + tellPO pre p origin + structSegs (p, Just bnd) segs post where startsWithDo :: [SegElm] -> Bool - startsWithDo (SStmts (A.Do _ _ : _) : _) = True + startsWithDo (SStmts (Do _ _ : _) : _) = True startsWithDo _ = False origin = if startsWithDo segs then AtLoop l else AtAssertion l structSegs (pre, bnd) [SStmts ss] post = structSStmts (pre, bnd) ss post - structSegs (pre, bnd) (SStmts ss : SAsrt (A.Assert p l) : segs) post = do - structSStmts (pre, bnd) ss (Assertion p l) - structSegs (Assertion p l, Nothing) segs post - structSegs (pre, bnd) (SStmts ss : SAsrt (A.LoopInvariant p bd l) : segs) post + structSegs (pre, bnd) (SStmts ss : SAsrt (Assert p _) : segs) post = do + structSStmts (pre, bnd) ss p + structSegs (p, Nothing) segs post + structSegs (pre, bnd) (SStmts ss : SAsrt (LoopInvariant p bd _) : segs) post = do - structSStmts (pre, bnd) ss (LoopInvariant p bd l) - structSegs (LoopInvariant p bd l, Just bd) segs post - structSegs (pre, bnd) (SStmts ss : SSpec (A.Spec _ range) : segs) post = do + structSStmts (pre, bnd) ss p + structSegs (p, Just bd) segs post + structSegs (pre, bnd) (SStmts ss : SSpec (Spec _ range tenv) : segs) post = do post' <- wpSegs segs post pre' <- spSStmts (pre, bnd) ss - tellSpec pre' post' range - structSegs (pre, _) (SSpec (A.Spec _ range) : segs) post = do + tellSpec pre' post' tenv range + structSegs (pre, _) (SSpec (Spec _ range tenv) : segs) post = do post' <- wpSegs segs post - tellSpec pre post' range + tellSpec pre post' tenv range structSegs _ _ _ = error "Missing case in structSegs" -- 'simple' version of struct stmts -- there are no assertions, -- invariants, or specs in the list of statements. - structSStmts :: (Pred, Maybe A.Expr) -> [A.Stmt] -> Pred -> WP () + structSStmts :: (Pred, Maybe Expr) -> [Stmt] -> Pred -> WP () structSStmts (pre, _) [] post = do case locOf pre of NoLoc -> tellPO pre post (AtAssertion (locOf post)) @@ -100,82 +94,85 @@ structFunctions (wpSegs, wpSStmts, wp, spSStmts) = post' <- wpSStmts stmts post struct (pre, bnd) stmt post' - struct :: (Pred, Maybe A.Expr) -> A.Stmt -> Pred -> WP () - struct (pre, _) s@(A.Abort l) post = tellPO' (AtAbort l) pre =<< wp s post - struct (pre, _) s@(A.Skip l) post = tellPO' (AtSkip l) pre =<< wp s post - struct (pre, _) s@(A.Assign vars exprs l) post = do + struct :: (Pred, Maybe Expr) -> Stmt -> Pred -> WP () + struct (pre, _) s@(Abort l) post = tellPO' (AtAbort l) pre =<< wp s post + struct (pre, _) s@(Skip l) post = tellPO' (AtSkip l) pre =<< wp s post + struct (pre, _) s@(Assign vars exprs l) post = do tellPO' origin pre =<< wp s post where origin :: Origin origin = explainAssignment pre post vars exprs l - struct (pre, _) s@(A.AAssign _ _ _ l) post = do + struct (pre, _) s@(AAssign _ _ _ l) post = do tellPO' (AtAssignment l) pre =<< wp s post - struct (pre, _) (A.If gcmds l) post = do + struct (pre, _) (If gcmds l) post = do tellPO pre (disjunctGuards gcmds) (AtIf l) - forM_ gcmds $ \(A.GdCmd guard body _) -> - structStmts Primary (Conjunct [pre, guardIf guard], Nothing) body post - struct (inv, Just bnd) (A.Do gcmds l) post = do - let guards = A.getGuards gcmds - tellPO (Conjunct (inv : map (Negate . guardLoop) guards)) + forM_ gcmds $ \(GdCmd guard body _) -> + structStmts Primary (pre `conj` guard, Nothing) body post + struct (inv, Just bnd) (Do gcmds l) post = do + let guards = getGuards gcmds + tellPO (conjunct (inv : map neg guards)) post (explainAfterLoop inv guards l) forM_ gcmds (structGdcmdInduct inv) - tellPO (Conjunct [inv, Disjunct (map guardLoop guards)]) - (Bound (bnd `A.gte` A.Lit (A.Num 0) NoLoc) NoLoc) + tellPO (inv `conj` disjunct guards) + (bnd `gte` Lit (Num 0) tInt NoLoc) (explainTermination inv guards bnd l) forM_ gcmds (structGdcmdBnd inv bnd) - struct (inv, Nothing) (A.Do gcmds l) post = do + + struct (inv, Nothing) (Do gcmds l) post = do case fromLoc l of Nothing -> return () Just rng -> throwWarning (MissingBound rng) - let guards = A.getGuards gcmds - tellPO (Conjunct (inv : map (Negate . guardLoop) guards)) post (AtLoop l) + let guards = getGuards gcmds + tellPO (conjunct (inv : map neg guards)) post (AtLoop l) forM_ gcmds (structGdcmdInduct inv) - struct _ (A.Proof _ _ _) _ = return () - -- TODO: - struct (pre, _) (A.Block prog _) post = structBlock pre prog post - struct (pre, _) s@(A.Alloc _ _ l) post = + struct _ (Proof _ _ _) _ = return () + + struct (pre, _) (Block prog _) post = structBlock pre prog post + + struct (pre, _) s@(Alloc _ _ l) post = tellPO' (AtAbort l) pre =<< wp s post - struct (pre, _) s@(A.HLookup _ _ l) post = + struct (pre, _) s@(HLookup _ _ l) post = tellPO' (AtAbort l) pre =<< wp s post - struct (pre, _) s@(A.HMutate _ _ l) post = + struct (pre, _) s@(HMutate _ _ l) post = tellPO' (AtAbort l) pre =<< wp s post - struct (pre, _) s@(A.Dispose _ l) post = + struct (pre, _) s@(Dispose _ l) post = tellPO' (AtAbort l) pre =<< wp s post + struct _ _ _ = error "missing case in struct" - structGdcmdInduct :: Pred -> A.GdCmd -> WP () - structGdcmdInduct inv (A.GdCmd guard body _) = - structStmts Primary (Conjunct [inv, guardLoop guard], Nothing) body inv + structGdcmdInduct :: Pred -> GdCmd -> WP () + structGdcmdInduct inv (GdCmd guard body _) = + structStmts Primary (inv `conj` guard, Nothing) body inv - structGdcmdBnd :: Pred -> A.Expr -> A.GdCmd -> WP () - structGdcmdBnd inv bnd (A.GdCmd guard body _) = withFreshVar $ \oldbnd -> do + structGdcmdBnd :: Pred -> Expr -> GdCmd -> WP () + structGdcmdBnd inv bnd (GdCmd guard body _) = withFreshVar tInt $ \oldbnd -> do structStmts Secondary - (Conjunct [inv, Bound (bnd `A.eqq` oldbnd) NoLoc, guardLoop guard], Nothing) + (conjunct [inv, bnd `eqq` oldbnd,guard], Nothing) body - (Bound (bnd `A.lt` oldbnd) NoLoc) + (bnd `lt` oldbnd) - structBlock :: Pred -> A.Program -> Pred -> WP () - structBlock pre (A.Program _ decls _props stmts _) post = do - let localNames = declaredNames decls + structBlock :: Pred -> Program -> Pred -> WP () + structBlock pre (Program _ decls _props stmts _) post = do + let localNames = declaredNamesTypes decls (xs, ys) <- withLocalScopes (\scopes -> - withScopeExtension (map nameToText localNames) + withScopeExtension (map (nameToText . fst) localNames) (calcLocalRenaming (concat scopes) localNames)) stmts' <- subst (toSubst ys) stmts - withScopeExtension (xs ++ (map (nameToText . snd) ys)) + withScopeExtension (xs ++ (map (nameToText . fst . snd) ys)) (structStmts Primary (pre, Nothing) stmts' post) - where toSubst = fromList . map (\(n, n') -> (n, A.Var n' (locOf n'))) + where toSubst = fromList . map (\(n, (n',t)) -> (n, Var n' t (locOf n'))) -calcLocalRenaming :: [Text] -> [Name] -> WP ([Text], [(Text, Name)]) +calcLocalRenaming :: [Text] -> [(Name, Type)] -> WP ([Text], [(Text, (Name, Type))]) calcLocalRenaming _ [] = return ([], []) -calcLocalRenaming scope (x:xs) - | t `elem` scope = do - x' <- freshName t (locOf x) - second ((t,x') :) <$> calcLocalRenaming scope xs +calcLocalRenaming scope ((x,t):xs) + | tx `elem` scope = do + x' <- freshName tx (locOf x) + second ((tx,(x',t)) :) <$> calcLocalRenaming scope xs | otherwise = - first (t:) <$> calcLocalRenaming scope xs - where t = nameToText x + first (tx:) <$> calcLocalRenaming scope xs + where tx = nameToText x -- debugging diff --git a/src/GCL/WP/Type.hs b/src/GCL/WP/Types.hs similarity index 64% rename from src/GCL/WP/Type.hs rename to src/GCL/WP/Types.hs index fecc6d91..5a9943de 100644 --- a/src/GCL/WP/Type.hs +++ b/src/GCL/WP/Types.hs @@ -1,7 +1,7 @@ {-# LANGUAGE DeriveGeneric, FlexibleContexts, FlexibleInstances #-} -module GCL.WP.Type where +module GCL.WP.Types where import GHC.Generics ( Generic ) import Control.Monad.Except ( Except ) @@ -10,22 +10,24 @@ import Control.Monad.RWS ( MonadState(..) import Data.IntMap ( IntMap ) import Data.Aeson (ToJSON) import Data.Text ( Text ) +import Data.Map ( Map ) import Data.Loc (Loc (..), Located (..)) import Data.Loc.Range (Range) import GCL.Common import GCL.Predicate ( InfMode(..) - , PO(..), Pred(..), Spec (..)) -import qualified GCL.Substitution as Substitution -import qualified Syntax.Abstract as A + , PO(..), Pred, Spec (..)) +import Syntax.Typed -- The WP monad. type TM = Except StructError +type Decls = Map Text (Maybe Expr) + type WP = RWST - (Substitution.Decls, [[Text]]) - ([PO], [Spec], [StructWarning], IntMap (Int, A.Expr)) + (Decls, [[Text]]) + ([PO], [Spec], [StructWarning], IntMap (Int, Expr)) Int TM @@ -36,23 +38,23 @@ instance Counterous WP where --- -data SegElm = SAsrt A.Stmt - | SSpec A.Stmt - | SStmts [A.Stmt] +data SegElm = SAsrt Stmt + | SSpec Stmt + | SStmts [Stmt] -- types of mutually recursive functions -type TstructStmts = InfMode -> (Pred, Maybe A.Expr) -> [A.Stmt] -> Pred -> WP () -type TstructSegs = (Pred, Maybe A.Expr) -> [SegElm] -> Pred -> WP () -type Tstruct = (Pred, Maybe A.Expr) -> A.Stmt -> Pred -> WP () +type TstructStmts = InfMode -> (Pred, Maybe Expr) -> [Stmt] -> Pred -> WP () +type TstructSegs = (Pred, Maybe Expr) -> [SegElm] -> Pred -> WP () +type Tstruct = (Pred, Maybe Expr) -> Stmt -> Pred -> WP () type TwpSegs = [SegElm] -> Pred -> WP Pred -type TwpSStmts = [A.Stmt] -> Pred -> WP Pred -type Twp = A.Stmt -> Pred -> WP Pred +type TwpSStmts = [Stmt] -> Pred -> WP Pred +type Twp = Stmt -> Pred -> WP Pred -type TspStmts = (Pred, Maybe A.Expr) -> [A.Stmt] -> WP Pred -type TspSegs = (Pred, Maybe A.Expr) -> [SegElm] -> WP Pred -type TspSStmts = (Pred, Maybe A.Expr) -> [A.Stmt] -> WP Pred +type TspStmts = (Pred, Maybe Expr) -> [Stmt] -> WP Pred +type TspSegs = (Pred, Maybe Expr) -> [SegElm] -> WP Pred +type TspSStmts = (Pred, Maybe Expr) -> [Stmt] -> WP Pred --- @@ -80,7 +82,5 @@ instance Located StructError where locOf (MultiDimArrayAsgnNotImp l) = l locOf (LocalVarExceedScope l) = l -instance ToJSON StructError - -- freshPreInScope prefix scope -- generates a fresh name, with prefix, that does not appear in scope diff --git a/src/GCL/WP/Util.hs b/src/GCL/WP/Util.hs index 81faf2f2..78fa4da0 100644 --- a/src/GCL/WP/Util.hs +++ b/src/GCL/WP/Util.hs @@ -19,116 +19,99 @@ import qualified Data.Text as Text import qualified Data.Hashable as Hashable import GCL.Predicate ( Origin(..) , PO(..) - , Pred(..) + , Pred , Spec(Specification) ) -import GCL.Predicate.Util ( disjunct - , guardIf - , toExpr - ) import GCL.Common ( Fresh(..) , Counterous(..) + , TypeEnv , freshName' + , Index + , TypeInfo ) -import qualified Syntax.Abstract as A -import qualified Syntax.Abstract.Util as A +import Syntax.Typed +import Syntax.Typed.Util +import Syntax.Typed.Operator ( disjunct ) import Syntax.Common ( Name(..) , nameToText ) -import qualified GCL.Substitution as Substitution import Numeric ( showHex ) import Pretty ( toString ) -import GCL.WP.Type +import GCL.WP.Types -- Syntax Manipulation --- grouping a sequence of statement by assertions and specs -groupStmts :: [A.Stmt] -> [SegElm] +groupStmts :: [Stmt] -> [SegElm] groupStmts [] = [] -groupStmts (s@(A.Assert _ _) : stmts) = SAsrt s : groupStmts stmts -groupStmts (s@A.LoopInvariant{} : stmts) = SAsrt s : groupStmts stmts -groupStmts (s@(A.Spec _ _) : stmts) = SSpec s : groupStmts stmts +groupStmts (s@(Assert _ _) : stmts) = SAsrt s : groupStmts stmts +groupStmts (s@LoopInvariant{} : stmts) = SAsrt s : groupStmts stmts +groupStmts (s@(Spec _ _ _) : stmts) = SSpec s : groupStmts stmts groupStmts (s : stmts) = case groupStmts stmts of [] -> [SStmts [s]] (SStmts ss : segs) -> SStmts (s : ss) : segs (s' : segs) -> SStmts [s] : s' : segs + --- removing assertions (while keeping loop invariants). --- succeed if there are no specs. -stripAsserts :: [A.Stmt] -> Maybe [A.Stmt] +stripAsserts :: [Stmt] -> Maybe [Stmt] stripAsserts [] = Just [] -stripAsserts (A.Assert _ _ : stmts) = stripAsserts stmts -stripAsserts (s1@A.LoopInvariant{} : s2@A.Do{} : stmts) = +stripAsserts (Assert _ _ : stmts) = stripAsserts stmts +stripAsserts (s1@LoopInvariant{} : s2@Do{} : stmts) = (s1 :) <$> stripAsserts (s2 : stmts) -stripAsserts (A.LoopInvariant{} : stmts) = stripAsserts stmts -stripAsserts (A.Spec _ _ : _ ) = Nothing -stripAsserts (A.If gcmds l : stmts) = do - gcmds' <- forM gcmds $ \(A.GdCmd guard body l') -> do +stripAsserts (LoopInvariant{} : stmts) = stripAsserts stmts +stripAsserts (Spec _ _ _ : _ ) = Nothing +stripAsserts (If gcmds l : stmts) = do + gcmds' <- forM gcmds $ \(GdCmd guard body l') -> do body' <- stripAsserts body - return (A.GdCmd guard body' l') + return (GdCmd guard body' l') stmts' <- stripAsserts stmts - return (A.If gcmds' l : stmts') -stripAsserts (A.Do gcmds l : stmts) = do - gcmds' <- forM gcmds $ \(A.GdCmd guard body l') -> do + return (If gcmds' l : stmts') +stripAsserts (Do gcmds l : stmts) = do + gcmds' <- forM gcmds $ \(GdCmd guard body l') -> do body' <- stripAsserts body - return (A.GdCmd guard body' l') + return (GdCmd guard body' l') stmts' <- stripAsserts stmts - return (A.Do gcmds' l : stmts') + return (Do gcmds' l : stmts') stripAsserts (s : stmts) = (s :) <$> stripAsserts stmts -disjunctGuards :: [A.GdCmd] -> Pred -disjunctGuards = disjunct . map guardIf . A.getGuards +disjunctGuards :: [GdCmd] -> Pred +disjunctGuards = disjunct . getGuards -- PO handling tellPO :: Pred -> Pred -> Origin -> WP () -tellPO p q origin = unless (toExpr p == toExpr q) $ do - p' <- substitute [] [] p - q' <- substitute [] [] q +tellPO p q origin = unless (p == q) $ do + -- p' <- substitute [] [] p + -- q' <- substitute [] [] q let anchorHash = - Text.pack $ showHex (abs (Hashable.hash (toString (p', q')))) "" - tell ([PO p' q' anchorHash Nothing origin], [], [], mempty) + Text.pack $ showHex (abs (Hashable.hash (toString (p, q)))) "" + tell ([PO p q anchorHash Nothing origin], [], [], mempty) tellPO' :: Origin -> Pred -> Pred -> WP () tellPO' l p q = tellPO p q l -tellSpec :: Pred -> Pred -> Range -> WP () -tellSpec p q l = do - p' <- substitute [] [] p - q' <- substitute [] [] q +tellSpec :: Pred -> Pred -> [(Index, TypeInfo)] -> Range -> WP () +tellSpec p q typeEnv l = do + -- p' <- substitute [] [] p + -- q' <- substitute [] [] q i <- countUp - tell ([], [Specification i p' q' l], [], mempty) + tell ([], [Specification i p q l typeEnv], [], mempty) throwWarning :: StructWarning -> WP () throwWarning warning = tell ([], [], [warning], mempty) --- ugly imports - -substitute - :: ( Substitution.Substitutable a - , Substitution.Reducible a - , Substitution.CollectRedexes a - ) - => [Name] - -> [A.Expr] - -> a - -> WP a -substitute xs es expr = do - (decls, _) <- ask - (result, redexes) <- Substitution.run decls xs es expr - tell ([], [], [], redexes) - return result - -- Misc. -withFreshVar :: (A.Expr -> WP a) -> WP a -withFreshVar f = do +withFreshVar :: Type -> (Expr -> WP a) -> WP a +withFreshVar t f = do name <- freshName' "bnd" - let var = A.Var name NoLoc + let var = Var name t NoLoc withRWST (\(decls, scopes) st -> ((Map.insert (nameToText name) Nothing decls, scopes), st)) @@ -143,11 +126,6 @@ withScopeExtension :: [Text] -> WP a -> WP a withScopeExtension names = local (\(defns, scopes) -> (defns, names:scopes)) -declaredNames :: [A.Declaration] -> [Name] -declaredNames decls = concat . map extractNames $ decls - where extractNames (A.ConstDecl ns _ _ _) = ns - extractNames (A.VarDecl ns _ _ _) = ns - freshPreInScope :: Text -> [Text] -> Text freshPreInScope pref scope | not (pref `elem` scope) = pref diff --git a/src/GCL/WP/WP.hs b/src/GCL/WP/WP.hs index 1584996f..fa456765 100644 --- a/src/GCL/WP/WP.hs +++ b/src/GCL/WP/WP.hs @@ -9,33 +9,34 @@ import Control.Monad.Except ( MonadError(throwError) import Data.Text ( Text ) import Data.Loc ( Loc(..), locOf ) import Data.Map ( fromList ) -import GCL.Predicate ( Pred(..) ) -import GCL.Predicate.Util ( conjunct - , toExpr - ) +import GCL.Predicate ( Pred ) import GCL.Common ( Fresh(..) , freshName , freshName' ) -import Pretty ( toText ) -import GCL.WP.Type -import GCL.WP.Util -import qualified Syntax.Abstract as A -import qualified Syntax.Abstract.Operator as A -import qualified Syntax.Abstract.Util as A -import Syntax.Common.Types ( Name(..) - , nameToText ) -import Syntax.Substitution - --- import Debug.Trace --- import Prettyprinter --- import Prettyprinter.Render.String +import GCL.Substitution ( syntaxSubst ) +import GCL.WP.Types +import GCL.WP.Util +import Syntax.Abstract.Operator ( tInt ) +import Syntax.Typed +import Syntax.Typed.Util ( getGuards, declaredNamesTypes ) +import Syntax.Typed.Operator ( nameVar, number, add + , false, true, neg + , conj, conjunct, implies + , forAll, exists + , pointsTo, sConj, sImp + , sconjunct + ) +import Syntax.Common.Types ( Name(..) + , nameToText ) +import Syntax.Typed.Instances.Substitution () +import Syntax.Substitution wpFunctions :: TstructSegs -> (TwpSegs, TwpSStmts, Twp) wpFunctions structSegs = (wpSegs, wpSStmts, wp) where - wpStmts :: [A.Stmt] -> Pred -> WP Pred + wpStmts :: [Stmt] -> Pred -> WP Pred wpStmts = wpSegs . groupStmts -- handels segments without a precondition. @@ -45,124 +46,120 @@ wpFunctions structSegs = (wpSegs, wpSStmts, wp) wpSegs (SStmts ss : segs) post = do post' <- wpSegs segs post wpSStmts ss post' - wpSegs (SSpec (A.Spec _ range) : segs) post = do + wpSegs (SSpec (Spec _ range tenv) : segs) post = do post' <- wpSegs segs post - tellSpec post' post' range + tellSpec post' post' tenv range return post' - wpSegs (SAsrt (A.Assert p l) : segs) post = do - structSegs (Assertion p l, Nothing) segs post - return (Assertion p l) - wpSegs (SAsrt (A.LoopInvariant p bd l) : segs) post = do - structSegs (LoopInvariant p bd l, Just bd) segs post - return (Assertion p l) -- SCM: erasing bound information? + wpSegs (SAsrt (Assert p _) : segs) post = do + structSegs (p, Nothing) segs post + return p + wpSegs (SAsrt (LoopInvariant p bd _) : segs) post = do + structSegs (p, Just bd) segs post + return p -- SCM: erasing bound information? wpSegs _ _ = error "Missing case in wpSegs" -- "simple" version of wpStmts. -- no assertions and specs (in the outer level), -- but may contain invariants in secondary run - wpSStmts :: [A.Stmt] -> Pred -> WP Pred + wpSStmts :: [Stmt] -> Pred -> WP Pred wpSStmts [] post = return post - wpSStmts (A.LoopInvariant inv _ _ : A.Do gcmds _ : stmts) post = do -- this happens only in secondary run + wpSStmts (LoopInvariant inv _ _ : Do gcmds _ : stmts) post = do -- this happens only in secondary run post' <- wpSStmts stmts post - let guards = A.getGuards gcmds - return - . Constant - $ inv - `A.conj` ( (inv `A.conj` A.conjunct (map A.neg guards)) - `A.implies` toExpr post' - ) + let guards = getGuards gcmds + return $ inv `conj` + ((inv `conj` conjunct (map neg guards)) `implies` post') wpSStmts (stmt : stmts) post = do post' <- wpSStmts stmts post wp stmt post' - wp :: A.Stmt -> Pred -> WP Pred - wp (A.Abort _ ) _ = return (Constant A.false) - wp (A.Skip _ ) post = return post + wp :: Stmt -> Pred -> WP Pred + wp (Abort _ ) _ = return false + wp (Skip _ ) post = return post - wp (A.Assign xs es _) post = substitute xs es post + wp (Assign xs es _) post = return $ syntaxSubst xs es post - wp (A.AAssign (A.Var x _) i e _) post = - substitute [x] [A.ArrUpd (A.nameVar x) i e NoLoc] post + wp (AAssign (Var x t _) i e _) post = + return $ syntaxSubst [x] [ArrUpd (nameVar x t) i e NoLoc] post - wp (A.AAssign _ _ _ l) _ = throwError (MultiDimArrayAsgnNotImp l) + wp (AAssign _ _ _ l) _ = throwError (MultiDimArrayAsgnNotImp l) - wp (A.Do _ l ) _ = throwError $ MissingAssertion l -- shouldn't happen + wp (Do _ l ) _ = throwError $ MissingAssertion l -- shouldn't happen - wp (A.If gcmds _ ) post = do - pres <- forM gcmds $ \(A.GdCmd guard body _) -> - Constant . (guard `A.imply`) . toExpr <$> wpStmts body post + wp (If gcmds _ ) post = do + pres <- forM gcmds $ \(GdCmd guard body _) -> + (guard `implies`) <$> wpStmts body post return (conjunct (disjunctGuards gcmds : pres)) - wp (A.Proof _ _ _ ) post = return post + wp (Proof _ _ _ ) post = return post - wp (A.Alloc x (e : es) _) post = do -- non-empty + wp (Alloc x (e : es) _) post = do -- non-empty {- wp (x := es) P = (forall x', (x' -> es) -* P[x'/x])-} - x' <- freshName' (toText x) -- generate fresh name using the exisiting "x" - post' <- substitute [x] [A.nameVar x'] (toExpr post) + x' <- freshName' (nameToText x) -- generate fresh name using the existing "x" + let post' = syntaxSubst [x] [nameVar x' tInt] post - return $ Constant (A.forAll [x'] A.true (newallocs x' `A.sImp` post')) + return $ forAll [x'] true (newallocs x' `sImp` post') where - newallocs x' = A.sconjunct - ( (A.nameVar x' `A.pointsTo` e) - : zipWith (\i -> A.pointsTo (A.nameVar x' `A.add` A.number i)) [1 ..] es + newallocs x' = sconjunct + ( (nameVar x' tInt `pointsTo` e) + : zipWith (\i -> pointsTo (nameVar x' tInt `add` number i)) [1 ..] es ) - wp (A.HLookup x e _) post = do + wp (HLookup x e _) post = do {- wp (x := *e) P = (exists v . (e->v) * ((e->v) -* P[v/x])) -} - v <- freshName' (toText x) -- generate fresh name using the exisiting "x" - post' <- substitute [x] [A.nameVar v] (toExpr post) + v <- freshName' (nameToText x) -- generate fresh name using the exisiting "x" + let post' = syntaxSubst [x] [nameVar v tInt] post - return $ Constant - (A.exists [v] A.true (entry v `A.sConj` (entry v `A.sImp` post'))) - where entry v = e `A.pointsTo` A.nameVar v + return $ exists [v] true (entry v `sConj` (entry v `sImp` post')) + where entry v = e `pointsTo` nameVar v tInt - wp (A.HMutate e1 e2 _) post = do + wp (HMutate e1 e2 _) post = do {- wp (e1* := e2) P = (e1->_) * ((e1->e2) -* P) -} e1_allocated <- allocated e1 - return $ Constant - (e1_allocated `A.sConj` ((e1 `A.pointsTo` e2) `A.sImp` toExpr post)) + return $ e1_allocated `sConj` ((e1 `pointsTo` e2) `sImp` post) - wp (A.Dispose e _) post = do + wp (Dispose e _) post = do {- wp (dispose e) P = (e -> _) * P -} e_allocated <- allocated e - return $ Constant (e_allocated `A.sConj` toExpr post) + return $ e_allocated `sConj` post + -- TODO: - wp (A.Block prog _) post = wpBlock prog post + wp (Block prog _) post = wpBlock prog post wp _ _ = error "missing case in wp" - wpBlock :: A.Program -> Pred -> WP Pred - wpBlock (A.Program _ decls _props stmts _) post = do - let localNames = declaredNames decls + wpBlock :: Program -> Pred -> WP Pred + wpBlock (Program _ decls _props stmts _) post = do + let localNames = declaredNamesTypes decls (xs, ys) <- withLocalScopes (\scopes -> - withScopeExtension (map nameToText localNames) + withScopeExtension (map (nameToText . fst) localNames) (calcLocalRenaming (concat scopes) localNames)) stmts' <- subst (toSubst ys) stmts - withScopeExtension (xs ++ (map (nameToText . snd) ys)) + withScopeExtension (xs ++ (map (nameToText . fst . snd) ys)) (wpStmts stmts' post) -- if any (`member` (fv pre)) (declaredNames decls) -- then throwError (LocalVarExceedScope l) -- else return pre - where toSubst = fromList . map (\(n, n') -> (n, A.Var n' (locOf n'))) + where toSubst = fromList . map (\(n, (n', t)) -> (n, Var n' t (locOf n'))) -calcLocalRenaming :: [Text] -> [Name] -> WP ([Text], [(Text, Name)]) +calcLocalRenaming :: [Text] -> [(Name, Type)] -> WP ([Text], [(Text, (Name, Type))]) calcLocalRenaming _ [] = return ([], []) -calcLocalRenaming scope (x:xs) - | t `elem` scope = do - x' <- freshName t (locOf x) - second ((t,x') :) <$> calcLocalRenaming scope xs +calcLocalRenaming scope ((x, t):xs) + | tx `elem` scope = do + x' <- freshName tx (locOf x) + second ((tx,(x',t)) :) <$> calcLocalRenaming scope xs | otherwise = - first (t:) <$> calcLocalRenaming scope xs - where t = nameToText x + first (tx:) <$> calcLocalRenaming scope xs + where tx = nameToText x + -toMapping :: [(Text, Name)] -> A.Mapping -toMapping = fromList . map cvt - where cvt (x, y) = (x, A.Var y (locOf y)) +-- toMapping :: [(Text, Name)] -> A.Mapping +-- toMapping = fromList . map cvt +-- where cvt (x, y) = (x, A.Var y (locOf y)) -allocated :: Fresh m => A.Expr -> m A.Expr +allocated :: Fresh m => Expr -> m Expr allocated e = do v <- freshName' "new" - return (A.exists [v] A.true (e `A.pointsTo` A.nameVar v)) + return (exists [v] true (e `pointsTo` nameVar v tInt)) -- allocated e = e -> _ -- debugging diff --git a/src/Pretty.hs b/src/Pretty.hs index 8b13c849..6c962bfc 100644 --- a/src/Pretty.hs +++ b/src/Pretty.hs @@ -13,6 +13,7 @@ import Pretty.Abstract ( ) import Pretty.Concrete ( ) import Pretty.Error ( ) import Pretty.Predicate ( ) +import Pretty.Typed ( ) import Pretty.Util import Prettyprinter diff --git a/src/Pretty/Error.hs b/src/Pretty/Error.hs index 5eac4c0a..0b8e96bf 100644 --- a/src/Pretty/Error.hs +++ b/src/Pretty/Error.hs @@ -8,7 +8,7 @@ import Data.Loc import Prettyprinter import Error import GCL.Type ( TypeError(..) ) -import GCL.WP.Type ( StructError(..) +import GCL.WP.Types ( StructError(..) , StructWarning(..) ) import Prelude hiding ( Ordering(..) ) diff --git a/src/Pretty/Predicate.hs b/src/Pretty/Predicate.hs index 1dbe83d9..528a67a7 100644 --- a/src/Pretty/Predicate.hs +++ b/src/Pretty/Predicate.hs @@ -12,6 +12,7 @@ import Render.Class (PrecContext(NoContext)) -------------------------------------------------------------------------------- +{- -- | Pred instance PrettyPrec Pred where prettyPrec = fromRenderPrec @@ -58,7 +59,7 @@ instance Show GdCmd where instance Pretty GdCmd where pretty (GdCmd guard struct) = " |" <+> pretty guard <+> "=>" <+> line <> " " <> align (pretty struct) - +-} -------------------------------------------------------------------------------- -- | Origin @@ -72,4 +73,4 @@ instance Pretty PO where pretty = fromRenderSection instance Pretty Spec where - pretty = fromRenderSection \ No newline at end of file + pretty = fromRenderSection diff --git a/src/Pretty/Typed.hs b/src/Pretty/Typed.hs new file mode 100644 index 00000000..768e5559 --- /dev/null +++ b/src/Pretty/Typed.hs @@ -0,0 +1,119 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Pretty.Typed + () where + +import Prelude hiding ( Ordering(..) ) +import Pretty.Common ( ) +import Pretty.Util +import Prettyprinter +import Render.Error ( ) +import Render.Predicate ( ) +import Render.Syntax.Common ( ) +import Syntax.Typed +import Pretty.Abstract ( ) +import Render.Class (PrecContext(NoContext)) + +-------------------------------------------------------------------------------- + +-- | Program +instance Pretty Program where + pretty (Program _ decls props stmts _) = + vsep $ map pretty decls ++ map pretty props ++ map pretty stmts + +-------------------------------------------------------------------------------- + +-- | Declaration +instance Pretty Declaration where + pretty (ConstDecl names t Nothing _) = + "con " <> hsep (punctuate ", " (map pretty names)) <> ": " <> pretty t + pretty (ConstDecl names t (Just p) _) = + "con " + <> hsep (punctuate ", " (map pretty names)) + <> ": " + <> pretty t + <> "{ " + <> pretty p + <> " }" + pretty (VarDecl names t Nothing _) = + "var " <> hsep (punctuate ", " (map pretty names)) <> ": " <> pretty t + pretty (VarDecl names t (Just p) _) = + "var " + <> hsep (punctuate ", " (map pretty names)) + <> ": " + <> pretty t + <> "{ " + <> pretty p + <> " }" + +instance Pretty Definition where + pretty (TypeDefn name binders qdcons _) = + "data " <> pretty name <+> hsep (map pretty binders) <> "= " <> hsep + (punctuate "| " (map pretty qdcons)) + pretty (FuncDefnSig name typ Nothing _) = pretty name <> ": " <> pretty typ + pretty (FuncDefnSig name typ (Just prop) _) = + pretty name <> ": " <> pretty typ <> "{ " <> pretty prop <> " }" + pretty (FuncDefn name expr) = pretty name <+> " = " <+> pretty expr + +instance Pretty TypeDefnCtor where + pretty (TypeDefnCtor cn ts) = pretty cn <+> hsep (pretty <$> ts) + +-------------------------------------------------------------------------------- + +-- | Stmt +instance Pretty Stmt where + pretty (Skip _) = "skip" + pretty (Abort _) = "abort" + pretty (Assign xs es _) = + hsep (punctuate ", " (map pretty xs)) <> ":= " <> hsep + (punctuate ", " (map pretty es)) + pretty (AAssign x i e _) = + pretty x <> "[" <> pretty i <> "]" <> ":=" <> pretty e + pretty (Assert p _) = "{ " <> pretty p <> " }" + pretty (LoopInvariant p bnd _) = + "{ " <> pretty p <> " , bnd: " <> pretty bnd <> " }" + pretty (Do gdCmds _) = + "do" <> line <> vsep (map (\x -> " |" <+> pretty x <> line) gdCmds) <> "od" + pretty (If gdCmds _) = + "if" <> line <> vsep (map (\x -> " |" <+> pretty x <> line) gdCmds) <> "fi" + pretty (Spec content _ _) = "[!" <> pretty content <> "!]" + pretty (Proof anchor contents _) = + -- "{-" <> vsep (map (\x -> pretty x <> line) anchors) <> "-}" + "{- #" <> pretty anchor <> line <> pretty contents <> line <> "-}" + pretty (Alloc x es _) = + pretty x + <+> ":=" + <+> "new (" + <+> hsep (punctuate ", " (map pretty es)) + <+> ")" + pretty (HLookup x e _) = pretty x <+> ":=" <+> pretty e <> "*" + pretty (HMutate e1 e2 _) = pretty e1 <> "*" <+> ":=" <+> pretty e2 + pretty (Dispose e _ ) = "free" <+> pretty e + pretty (Block p _ ) = "|[" <+> pretty p <+> "]|" + +instance Pretty GdCmd where + pretty (GdCmd guard body _) = + pretty guard <+> "->" <+> vsep (map pretty body) + +-- instance Pretty ProofAnchor where +-- pretty (ProofAnchor hash _) = "#" <+> pretty hash + +-- instance Pretty TextContents where +-- pretty (TextContents text _) = pretty text + +-------------------------------------------------------------------------------- + +-- | Expr +instance Pretty Expr where + pretty = prettyPrec NoContext + +instance PrettyPrec Expr where + prettyPrec = fromRenderPrec + +-- instance Pretty Pattern where +-- pretty = prettyPrec NoContext +-- +-- instance PrettyPrec Pattern where +-- prettyPrec = fromRenderPrec + +-------------------------------------------------------------------------------- diff --git a/src/Render/Error.hs b/src/Render/Error.hs index 88fa5191..f833a253 100644 --- a/src/Render/Error.hs +++ b/src/Render/Error.hs @@ -7,7 +7,7 @@ import Data.Loc ( locOf ) import Data.Loc.Range import Error import GCL.Type ( TypeError(..) ) -import GCL.WP.Type ( StructError(..) ) +import GCL.WP.Types ( StructError(..) ) import Render.Class import Render.Element import Render.Syntax.Abstract ( ) diff --git a/src/Render/Predicate.hs b/src/Render/Predicate.hs index 1f447dff..6933133f 100644 --- a/src/Render/Predicate.hs +++ b/src/Render/Predicate.hs @@ -6,12 +6,13 @@ import Data.Loc ( locOf, Loc (NoLoc) ) import Data.Loc.Range ( fromLoc ) import qualified Data.Text as Text import GCL.Predicate -import GCL.WP.Type +import GCL.WP.Types import Render.Class import Render.Element import Render.Syntax.Abstract ( ) import Syntax.Abstract.Types ( Expr(..) ) import Syntax.Common.Types ( ArithOp (..) ) +import Render.Syntax.Typed instance Render StructWarning where render (MissingBound _) @@ -27,7 +28,7 @@ instance RenderSection StructWarning where Section Yellow [Header "Excess Bound" (Just range), Paragraph (render x)] instance RenderSection Spec where - renderSection (Specification _ pre post range) = Section + renderSection (Specification _ pre post range _) = Section Blue [ Header "Precondition" (Just range) , Code (render pre) @@ -35,8 +36,8 @@ instance RenderSection Spec where , Code (render post) ] -instance Render Pred where - renderPrec n x = renderPrec n (exprOfPred x) +-- instance Render Pred where +-- renderPrec n x = renderPrec n (exprOfPred x) -- renderPrec n x = case x of -- Constant p -> renderPrec n p -- GuardIf p _ -> renderPrec n p @@ -48,6 +49,7 @@ instance Render Pred where -- Disjunct ps -> punctuateE " ∨" (map render ps) -- Negate p -> "¬" <+> renderPrec n p +{- exprOfPred :: Pred -> Expr exprOfPred p = case p of Constant ex -> ex @@ -57,7 +59,7 @@ exprOfPred p = case p of LoopInvariant ex _ _ -> ex Bound ex _ -> ex Conjunct prs -> case map exprOfPred prs of - [] -> error "Impossible case: incomplete Pred (in Render.Predicate.exprOfPred, Conjunct case)" + [] -> error "Impossible case: incomplete Pred (in Render.Predicate.exprOfPred, Conjunct case)" [ex] -> ex x : y : exprs -> foldl (makeOpExpr conjOp) (makeOpExpr conjOp x y) @@ -68,15 +70,15 @@ exprOfPred p = case p of x : y : exprs -> foldl (makeOpExpr disjOp) (makeOpExpr disjOp x y) exprs - Negate pr -> + Negate pr -> let ex = exprOfPred pr in App (Op $ NegU NoLoc) ex (locOf ex) - where -- TODO: Maybe we don't need `Op` here. This requires further investigation. + where -- TODO: Maybe we don't need `Op` here. This requires further investigation. conjOp = Op $ ConjU NoLoc disjOp = Op $ DisjU NoLoc makeOpExpr :: Expr -> Expr -> Expr -> Expr makeOpExpr op x y = App (App op x (locOf x)) y (locOf y) - +-} instance RenderSection PO where renderSection (PO pre post anchorHash anchorLoc origin) = @@ -93,7 +95,7 @@ instance RenderSection PO where Explain _ x _ _ _ -> [Paragraph x] _ -> [Paragraph "explanation not available"] --- as header +-- as header instance Render Origin where render AtAbort{} = "Abort" render AtSkip{} = "Skip" diff --git a/src/Render/Syntax/Typed.hs b/src/Render/Syntax/Typed.hs new file mode 100644 index 00000000..102b7aff --- /dev/null +++ b/src/Render/Syntax/Typed.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} + +module Render.Syntax.Typed where + +import Render.Class +import Render.Element +import Render.Syntax.Common ( ) +import Render.Syntax.Abstract hiding ( handleExpr ) +import Syntax.Typed +import Syntax.Common ( ArithOp(..) + , Fixity(..) + , Op(..) + , classify + ) + +------------------------------------------------------------------------------ + + +-- | Expr +instance Render Expr where + renderPrec prec expr = handleExpr prec expr + +handleExpr :: PrecContext -> Expr -> Inlines +handleExpr _ (Lit x _ l) = tempHandleLoc l $ render x +handleExpr _ (Var x _ l) = tempHandleLoc l $ render x +handleExpr _ (Const x _ l) = tempHandleLoc l $ render x +handleExpr _ (Op _ _) = error "erroneous syntax given to render" +handleExpr _ (Chain ch) = render ch +handleExpr n (App (App (Op (ArithOp op) _) left _) right _) = --binary operators + parensIf n (Just (ArithOp op)) $ + renderPrec (HOLEOp (ArithOp op)) left + <+> render op + <+> renderPrec (OpHOLE (ArithOp op)) right +handleExpr n (App (Op (ArithOp op) _) e _) = case classify (ArithOp op) of --unary operators, this case shouldn't be former than the binary case + (Prefix, _) -> parensIf n (Just (ArithOp op)) $ render op <+> renderPrec (OpHOLE (ArithOp op)) e + (Postfix, _) -> parensIf n (Just (ArithOp op)) $ renderPrec (HOLEOp (ArithOp op)) e <+> render op + _ -> error "erroneous syntax given to render" +handleExpr n (App f e _) = -- should only be normal applications + parensIf n Nothing $ renderPrec HOLEApp f <+> renderPrec AppHOLE e + +handleExpr prec (Lam p _ q _) = + let ifparens = case prec of + NoContext -> id + _ -> parensE + in + ifparens $ "λ" <+> render p <+> "→" <+> render q +handleExpr _ (Quant op xs r t _) = + "⟨" + <+> renderQOp op + <+> horzE (map render xs) + <+> ":" + <+> render r + <+> ":" + <+> render t + <+> "⟩" + where + renderQOp (Op (ArithOp (Conj _)) _) = "∀" + renderQOp (Op (ArithOp (ConjU _)) _) = "∀" + renderQOp (Op (ArithOp (Disj _)) _) = "∃" + renderQOp (Op (ArithOp (DisjU _)) _) = "∃" + renderQOp (Op (ArithOp (Add _)) _) = "Σ" + renderQOp (Op (ArithOp (Mul _)) _) = "Π" + renderQOp (Op op' _) = render op' + renderQOp op' = render op' +handleExpr _ (ArrIdx e1 e2 _) = render e1 <> "[" <> render e2 <> "]" +handleExpr _ (ArrUpd e1 e2 e3 _) = + "(" <+> render e1 <+> ":" <+> render e2 <+> "↣" <+> render e3 <+> ")" + -- SCM: need to print parenthesis around e1 when necessary. +handleExpr n (Subst e subs) = + parensIf n Nothing $ + handleExpr AppHOLE e <+> "[" <+> + renderManySepByComma vs <+> "\\" <+> + renderManySepByComma es <+> "]" + where (vs, es) = unzip subs + +instance Render Chain where -- Hopefully this is correct. + render (Pure expr) = render expr + render (More ch op _ expr) = render ch <+> render op <+> render expr diff --git a/src/SCM/simpleExpo.gcl b/src/SCM/simpleExpo.gcl deleted file mode 100644 index ef8a7e55..00000000 --- a/src/SCM/simpleExpo.gcl +++ /dev/null @@ -1,9 +0,0 @@ -var x, y, n : Int - -n := 5 -x,y := 0,1 - -{ True, bnd: n - x } -do x /= n -> x, y := x + 1, y + y -od -{ True } diff --git a/src/SCM/tst.gcl b/src/SCM/tst.gcl deleted file mode 100644 index 6c2ad107..00000000 --- a/src/SCM/tst.gcl +++ /dev/null @@ -1,9 +0,0 @@ -var x,y,z : Int - -x,y := 1,1 - -if x >= y -> z := 0 - | x <= y -> z := 1 -fi - -{ True } diff --git a/src/Server.hs b/src/Server.hs index 1abcfa16..0d1bffa9 100644 --- a/src/Server.hs +++ b/src/Server.hs @@ -1,3 +1,4 @@ + module Server where import Control.Concurrent ( forkIO @@ -5,7 +6,7 @@ import Control.Concurrent ( forkIO ) import Control.Monad.Except hiding ( guard ) import qualified Data.Text.IO as Text -import GHC.IO.IOMode ( IOMode(ReadWriteMode) ) +import GHC.IO.IOMode ( IOMode(..) ) import Language.LSP.Server import qualified Language.LSP.Types as LSP hiding ( TextDocumentSyncClientCapabilities(..) @@ -14,56 +15,65 @@ import Network.Simple.TCP ( HostPreference(Host) , serve ) import Network.Socket ( socketToHandle ) -import Server.Handler2 ( handlers ) -import Server.Monad +import Server.Handler ( handlers ) +import Server.Monad (initGlobalEnv, runServerM, logChannel, GlobalState) +import qualified Data.Text as Text -------------------------------------------------------------------------------- --- entry point of the LSP server -run :: Bool -> String -> IO Int -run devMode port = do +runOnPort :: String -> IO Int +runOnPort port = do env <- initGlobalEnv - if devMode - then do - _threadId <- forkIO (printLog env) - serve (Host "127.0.0.1") port $ \(sock, _remoteAddr) -> do - putStrLn $ "== connection established at " ++ port ++ " ==" - handle <- socketToHandle sock ReadWriteMode - _ <- runServerWithHandles handle handle (serverDefn env) - putStrLn "== dev server closed ==" - else do - runServer (serverDefn env) + _threadId <- forkIO (printLog env) + serve (Host "127.0.0.1") port $ \(sock, _remoteAddr) -> do + putStrLn $ "== connection established at " ++ port ++ " ==" + handle <- socketToHandle sock ReadWriteMode + _ <- runServerWithHandles handle handle (serverDefn env) + putStrLn "== dev server closed ==" where - printLog :: GlobalEnv -> IO () + printLog :: GlobalState -> IO () printLog env = forever $ do - result <- readChan (globalChan env) - when devMode $ do - Text.putStrLn result - serverDefn :: GlobalEnv -> ServerDefinition () - serverDefn env = ServerDefinition - { defaultConfig = () - , onConfigurationChange = const $ pure $ Right () - , doInitialize = \ctxEnv _req -> pure $ Right ctxEnv - , staticHandlers = handlers - , interpretHandler = \ctxEnv -> Iso (runServerM env ctxEnv) liftIO - , options = lspOptions - } + result <- readChan (logChannel env) + Text.putStrLn result + +-- entry point of the LSP server +runOnStdio :: FilePath -> IO Int +runOnStdio logFile = do + env <- initGlobalEnv + writeFile logFile "=== Log file Start ===\n" + _threadId <- forkIO (writeLog env) + runServer (serverDefn env) + where + writeLog :: GlobalState -> IO () + writeLog env = forever $ do + result <- readChan (logChannel env) + appendFile logFile (Text.unpack result) + +serverDefn :: GlobalState -> ServerDefinition () +serverDefn env = ServerDefinition + { defaultConfig = () + , onConfigurationChange = const $ pure $ Right () + , doInitialize = \ctxEnv _req -> pure $ Right ctxEnv + , staticHandlers = handlers + , interpretHandler = \ctxEnv -> Iso (runServerM env ctxEnv) liftIO + , options = lspOptions + } - lspOptions :: Options - lspOptions = defaultOptions { textDocumentSync = Just syncOptions - , completionTriggerCharacters = Just ['\\'] - } +lspOptions :: Options +lspOptions = defaultOptions { textDocumentSync = Just syncOptions + , completionTriggerCharacters = Just ['\\'] + } - -- these `TextDocumentSyncOptions` are essential for receiving notifications from the client - syncOptions :: LSP.TextDocumentSyncOptions - syncOptions = LSP.TextDocumentSyncOptions - { LSP._openClose = Just True -- receive open and close notifications from the client - , LSP._change = Just LSP.TdSyncIncremental -- receive change notifications from the client - , LSP._willSave = Just False -- receive willSave notifications from the client - , LSP._willSaveWaitUntil = Just False -- receive willSave notifications from the client - , LSP._save = Just $ LSP.InR saveOptions - } +-- these `TextDocumentSyncOptions` are essential for receiving notifications from the client +syncOptions :: LSP.TextDocumentSyncOptions +syncOptions = LSP.TextDocumentSyncOptions + { LSP._openClose = Just True -- receive open and close notifications from the client + , LSP._change = Just LSP.TdSyncIncremental -- receive change notifications from the client + , LSP._willSave = Just False -- receive willSave notifications from the client + , LSP._willSaveWaitUntil = Just False -- receive willSave notifications from the client + , LSP._save = Just $ LSP.InR saveOptions + } - -- includes the document content on save, so that we don't have to read it from the disk - saveOptions :: LSP.SaveOptions - saveOptions = LSP.SaveOptions (Just True) +-- includes the document content on save, so that we don't have to read it from the disk +saveOptions :: LSP.SaveOptions +saveOptions = LSP.SaveOptions (Just True) diff --git a/src/Server/CustomMethod.hs b/src/Server/CustomMethod.hs deleted file mode 100644 index 367294f7..00000000 --- a/src/Server/CustomMethod.hs +++ /dev/null @@ -1,107 +0,0 @@ -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} - -module Server.CustomMethod where - -import Data.Aeson ( FromJSON - , ToJSON - ) -import Data.Loc.Range -import Data.Text ( Text ) -import GCL.Predicate ( InfMode - , Origin - , PO - , Spec - ) -import GHC.Generics ( Generic ) -import Pretty -import Render - --------------------------------------------------------------------------------- - --- | Response -data ResKind - -- display stuff at the panel - = ResDisplay Int [Section] - -- mark Specs (holes) in the editor - | ResUpdateSpecs [(Int, Text, Text, Range)] - -- mark Proof Obligations in the editor - | ResMarkPOs [Range] - -- perform subsititution in expressions in the panel - | ResSubstitute Int Inlines - -- emit console.log for debugging - | ResConsoleLog Text - deriving (Eq, Generic) - -instance ToJSON ResKind - -instance Pretty ResKind where - pretty (ResDisplay _ _ ) = "Display" - pretty (ResUpdateSpecs _ ) = "UpdateSpecs" - pretty (ResMarkPOs _ ) = "ResMarkPOs" - pretty (ResSubstitute i x) = "Substitute " <> pretty i <> " : " <> pretty x - pretty (ResConsoleLog x ) = "ConsoleLog " <> pretty x - -instance Show ResKind where - show = toString - -data Response - = Res FilePath [ResKind] - | CannotDecodeRequest String - deriving (Generic) - -instance ToJSON Response - -instance Show Response where - show (Res _path kinds ) = show kinds - show (CannotDecodeRequest s) = "CannotDecodeRequest " <> s - --------------------------------------------------------------------------------- - --- | Requests from the client -data ReqKind - = ReqInspect Range - | ReqRefine Range - | ReqInsertAnchor Text - | ReqSubstitute Int - | ReqDebug - -- new - | ReqHelloWorld Range - | ReqReload - | ReqRefine2 Range Text - | ReqInsertProofTemplate Range Text - deriving Generic - -instance FromJSON ReqKind - -instance Show ReqKind where - show (ReqInspect range) = "Inspect " <> show (ShortRange range) - show (ReqRefine range) = "Refine " <> show (ShortRange range) - show (ReqInsertAnchor hash ) = "InsertAnchor " <> show hash - show (ReqSubstitute i ) = "Substitute " <> show i - show ReqDebug = "Debug" - show (ReqHelloWorld range) = "HelloWorld " <> show (ShortRange range) - show ReqReload = "Reload" - show (ReqRefine2 range text) = "Refine2 " <> show (ShortRange range) - <> " " <> show text - show (ReqInsertProofTemplate range hash) - = "InsertProofTemplate " <> show (ShortRange range) - <> " " <> show hash - -data Request = Req FilePath ReqKind - deriving Generic - -instance FromJSON Request - -instance Show Request where - show (Req _path kind) = show kind - --------------------------------------------------------------------------------- - -instance ToJSON Origin -instance ToJSON InfMode - -instance ToJSON PO - -instance ToJSON Spec diff --git a/src/Server/Handler.hs b/src/Server/Handler.hs index 5fd4d18c..51174e91 100644 --- a/src/Server/Handler.hs +++ b/src/Server/Handler.hs @@ -2,108 +2,126 @@ {-# LANGUAGE DisambiguateRecordFields #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BlockArguments #-} + {-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# HLINT ignore "Use lambda-case" #-} -module Server.Handler - ( handlers - ) where +module Server.Handler ( handlers ) where +import Control.Monad ( when ) import Control.Lens ( (^.) ) -import qualified Data.Aeson as JSON +import qualified Data.Aeson as JSON +import Data.Text (Text) import Language.LSP.Server ( Handlers , notificationHandler , requestHandler ) -import Server.Monad hiding (logText) -import Server.Pipeline -import Error ( Error ) -import qualified Language.LSP.Types as J -import qualified Language.LSP.Types.Lens as J +import qualified Language.LSP.Types as LSP +import qualified Language.LSP.Types.Lens as LSP +import qualified Language.LSP.Server as LSP + +import qualified Server.Handler.Initialized as Initialized +import qualified Server.Handler.GoToDefinition as GoToDefinition import qualified Server.Handler.AutoCompletion as AutoCompletion -import qualified Server.Handler.CustomMethod as CustomMethod -import qualified Server.Handler.GoToDefn as GoToDefn import qualified Server.Handler.Hover as Hover +import qualified Server.Handler.SemanticTokens as SemanticTokens +import qualified Server.Handler.Guabao.Reload as Reload +import qualified Server.Handler.Guabao.Refine as Refine +import Server.Monad (ServerM, sendDebugMessage, logText) +import Server.Load (load) +import qualified Server.Handler.OnDidChangeTextDocument as OnDidChangeTextDocument +import qualified Data.Text as Text -- handlers of the LSP server handlers :: Handlers ServerM handlers = mconcat - [ notificationHandler J.SInitialized $ \_not -> do - pure () - , - -- autocompletion - requestHandler J.STextDocumentCompletion $ \req responder -> do - let completionContext = req ^. J.params . J.context - let position = req ^. J.params . J.position - AutoCompletion.handler position completionContext >>= responder . Right - , - -- custom methods, not part of LSP - requestHandler (J.SCustomMethod "guabao") $ \req responder -> do - let params = req ^. J.params - CustomMethod.handler params (responder . Right . JSON.toJSON) - , notificationHandler J.STextDocumentDidChange $ \ntf -> do - let uri = ntf ^. (J.params . J.textDocument . J.uri) - interpret uri (customRequestToNotification uri) $ do - muted <- isMuted - if muted - then return [] - else do - logText "\n ---> TextDocumentDidChange" - source <- getSource - parsed <- parse source - converted <- convert parsed - typeChecked <- typeCheck converted - swept <- sweep typeChecked - generateResponseAndDiagnostics swept - , notificationHandler J.STextDocumentDidOpen $ \ntf -> do - let uri = ntf ^. (J.params . J.textDocument . J.uri) - let source = ntf ^. (J.params . J.textDocument . J.text) - interpret uri (customRequestToNotification uri) $ do - logText "\n ---> TextDocumentDidOpen" - parsed <- parse source - converted <- convert parsed - typeChecked <- typeCheck converted - swept <- sweep typeChecked - generateResponseAndDiagnostics swept - , -- Goto Definition - requestHandler J.STextDocumentDefinition $ \req responder -> do - let uri = req ^. (J.params . J.textDocument . J.uri) - let pos = req ^. (J.params . J.position) - GoToDefn.handler uri pos (responder . Right . J.InR . J.InR . J.List) - , -- Hover - requestHandler J.STextDocumentHover $ \req responder -> do - let uri = req ^. (J.params . J.textDocument . J.uri) - let pos = req ^. (J.params . J.position) - Hover.handler uri pos (responder . Right) - , requestHandler J.STextDocumentSemanticTokensFull $ \req responder -> do - let uri = req ^. (J.params . J.textDocument . J.uri) - interpret uri (responder . ignoreErrors) $ do - logText "\n ---> Syntax Highlighting" - let legend = J.SemanticTokensLegend - (J.List J.knownSemanticTokenTypes) - (J.List J.knownSemanticTokenModifiers) - stage <- load - let - highlightings = case stage of - Raw _ -> [] - Parsed result -> parsedHighlighings result - Converted result -> - parsedHighlighings (convertedPreviousStage result) - TypeChecked result -> parsedHighlighings - (convertedPreviousStage (typeCheckedPreviousStage result)) - Swept result -> parsedHighlighings - (convertedPreviousStage - (typeCheckedPreviousStage (sweptPreviousStage result)) - ) - let tokens = J.makeSemanticTokens legend highlightings - case tokens of - Left t -> return $ Left $ J.ResponseError J.InternalError t Nothing - Right tokens' -> return $ Right $ Just tokens' + [ -- "initialized" - after initialize + notificationHandler LSP.SInitialized $ \_ntf -> do + logText "SInitialized is called.\n" + Initialized.handler + , -- "textDocument/didOpen" - after open + notificationHandler LSP.STextDocumentDidOpen $ \ntf -> do + logText "STextDocumentDidOpen start\n" + let uri = ntf ^. (LSP.params . LSP.textDocument . LSP.uri) + case LSP.uriToFilePath uri of + Nothing -> return () + Just filePath -> load filePath + logText "STextDocumentDidOpen end\n" + , -- "textDocument/didChange" - after every edition + notificationHandler LSP.STextDocumentDidChange $ \ntf -> do + logText "STextDocumentDidChange start\n" + let uri :: LSP.Uri = ntf ^. (LSP.params . LSP.textDocument . LSP.uri) + let (LSP.List changes) = ntf ^. (LSP.params . LSP.contentChanges) + case LSP.uriToFilePath uri of + Nothing -> return () + Just filePath -> OnDidChangeTextDocument.handler filePath changes + logText "STextDocumentDidChange end\n" + , -- "textDocument/completion" - auto-completion + requestHandler LSP.STextDocumentCompletion $ \req responder -> do + let completionContext = req ^. LSP.params . LSP.context + let position = req ^. LSP.params . LSP.position + AutoCompletion.handler position completionContext >>= (responder . Right . LSP.InR) + , -- "textDocument/definition" - go to definition + requestHandler LSP.STextDocumentDefinition $ \req responder -> do + logText "STextDocumentDefinition is called.\n" + let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) + let position = req ^. (LSP.params . LSP.position) + GoToDefinition.handler uri position (responder . Right . LSP.InR . LSP.InR . LSP.List) + logText "STextDocumentDefinition is finished.\n" + , -- "textDocument/hover" - get hover information + requestHandler LSP.STextDocumentHover $ \req responder -> do + let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) + let pos = req ^. (LSP.params . LSP.position) + Hover.handler uri pos (responder . Right) + , -- "textDocument/semanticTokens/full" - get all semantic tokens + requestHandler LSP.STextDocumentSemanticTokensFull $ \req responder -> do + let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) + SemanticTokens.handler uri responder + , -- "guabao/reload" - reload + requestHandler (LSP.SCustomMethod "guabao/reload") $ jsonMiddleware Reload.handler + , -- "guabao/refine" - refine + requestHandler (LSP.SCustomMethod "guabao/refine") $ jsonMiddleware Refine.handler ] -ignoreErrors - :: ([Error], Maybe (Either J.ResponseError (Maybe J.SemanticTokens))) - -> Either J.ResponseError (Maybe J.SemanticTokens) -ignoreErrors (_, Nothing) = Left $ J.ResponseError J.InternalError "?" Nothing -ignoreErrors (_, Just xs) = xs +type CustomMethodHandler params result error = params -> (result -> ServerM ()) -> (error -> ServerM ()) -> ServerM () + +jsonMiddleware :: (JSON.FromJSON params, JSON.ToJSON result, JSON.ToJSON error) + => CustomMethodHandler params result error + -> LSP.Handler ServerM (LSP.CustomMethod :: LSP.Method LSP.FromClient LSP.Request) +jsonMiddleware handler req responder = do + logText "json: decoding request\n" + let json = req ^. LSP.params + logText . Text.pack $ show json + case decodeMessageParams json of + Left error -> do + logText "json: decoding failed with\n" + logText (Text.pack . show $ JSON.encode json) + responder (Left error) + Right params -> do + logText "json: decoding succeeded\n" + handler params + (responder . Right . JSON.toJSON) + (responder. Left . makeInternalError) + +decodeMessageParams :: forall a. JSON.FromJSON a => JSON.Value -> Either LSP.ResponseError a +decodeMessageParams json = do + case JSON.fromJSON json :: JSON.Result a of + JSON.Success params -> Right params + JSON.Error msg -> Left (makeParseError ("Json decoding failed." <> Text.pack msg)) + +makeInternalError :: JSON.ToJSON e => e -> LSP.ResponseError +makeInternalError error = LSP.ResponseError + { _code = LSP.InternalError + , _message = "" + , _xdata = Just (JSON.toJSON error) + } + +makeParseError :: Text -> LSP.ResponseError +makeParseError message = LSP.ResponseError + { _code = LSP.ParseError + , _message = message + , _xdata = Nothing + } diff --git a/src/Server/Handler/AutoCompletion.hs b/src/Server/Handler/AutoCompletion.hs index 7734abac..2f3c1332 100644 --- a/src/Server/Handler/AutoCompletion.hs +++ b/src/Server/Handler/AutoCompletion.hs @@ -1,34 +1,45 @@ {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DuplicateRecordFields #-} + module Server.Handler.AutoCompletion where import Data.Text ( Text ) import Language.LSP.Types -import Server.Monad -- To control the behaviour of autocomplete -- see https://github.com/haskell/lsp/blob/bf95cd94f3301fe391093912e6156de7cb5c1289/lsp-types/src/Language/LSP/Types/Completion.hs -handler :: Position -> Maybe CompletionContext -> ServerM (a |? CompletionList) -handler position completionContext = do - if shouldTriggerCompletion completionContext - then return $ InR $ CompletionList True (List (items position)) - else return $ InR $ CompletionList True (List []) +handler :: Monad m => Position -> Maybe CompletionContext -> m CompletionList +handler position completionContext + | shouldTriggerUnicodeCompletion completionContext + = return $ CompletionList True (List (unicodeCompletionItems position)) + | shouldTriggerDighole completionContext + = return $ CompletionList False (List [specBracketsCompletionItem position]) + | otherwise + = return $ CompletionList True (List []) -- https://github.com/haskell/lsp/blob/bf95cd94f3301fe391093912e6156de7cb5c1289/lsp-types/src/Language/LSP/Types/Completion.hs#L360-L371 -- trigger Unicode symbol completion when: -- 1. a backslash "\" is being typed -- 2. current completion is incomplete -shouldTriggerCompletion :: Maybe CompletionContext -> Bool -shouldTriggerCompletion (Just (CompletionContext CtTriggerCharacter (Just "\\"))) +shouldTriggerUnicodeCompletion :: Maybe CompletionContext -> Bool +shouldTriggerUnicodeCompletion (Just (CompletionContext CtTriggerCharacter (Just "\\"))) + = True +shouldTriggerUnicodeCompletion (Just (CompletionContext CtTriggerForIncompleteCompletions _)) = True -shouldTriggerCompletion (Just (CompletionContext CtTriggerForIncompleteCompletions _)) +shouldTriggerUnicodeCompletion _ + = False + +-- turn '?' into spec brackets '[! !]' +shouldTriggerDighole :: Maybe CompletionContext -> Bool +shouldTriggerDighole (Just (CompletionContext CtTriggerCharacter (Just "?"))) = True -shouldTriggerCompletion _ = False +shouldTriggerDighole _ + = False --- list of `CompletionItem`s -items :: Position -> [CompletionItem] -items position = mconcat +-- list of `CompletionItem`s for unicode symbols +unicodeCompletionItems :: Position -> [CompletionItem] +unicodeCompletionItems position = mconcat [ makeItems position [" "] (Just CiOperator) @@ -161,27 +172,52 @@ makeItems -> Text -> [CompletionItem] makeItems position labels kind symbol detail doc = flip map labels $ \label -> - CompletionItem label -- The label of this completion item. + CompletionItem + label -- The label of this completion item. -- By default also the text that is inserted when selecting this completion. - kind -- could be CIOperator, CiValue or whatever - Nothing -- for marking deprecated stuff - (Just detail) -- human-readable string - (Just $ CompletionDocString doc) -- also human-readable string - Nothing -- deprecated - Nothing -- select thie item when showing - Nothing -- how to sort completion items - Nothing -- how to filter completion items - (Just symbol) -- the symbol we wanna insert - (Just PlainText) -- could be a "Snippet" (with holes) or just plain text - Nothing -- how whitespace and indentation is handled during completion - Nothing -- TextEdit to be applied when this item has been selected (but not completed yet) - removeSlash -- TextEdit to be applied when this item has been completed - (Just (List [" ", "\\"])) -- commit characters - Nothing -- command to be executed after completion - Nothing -- ??? - + kind -- could be CIOperator, CiValue or whatever + Nothing -- for marking deprecated stuff + (Just detail) -- human-readable string + (Just $ CompletionDocString doc) -- also human-readable string + Nothing -- deprecated + Nothing -- select thie item when showing + Nothing -- how to sort completion items + Nothing -- how to filter completion items + (Just symbol) -- the symbol we wanna insert + (Just PlainText) -- could be a "Snippet" (with holes) or just plain text + Nothing -- how whitespace and indentation is handled during completion + Nothing -- TextEdit to be applied when this item has been selected (but not completed yet) + removeSlash -- TextEdit to be applied when this item has been completed + (Just (List [" ", "\\"])) -- commit characters + Nothing -- command to be executed after completion + Nothing -- ??? where Position ln col = position removeSlash = - Just $ List [TextEdit (Range (Position ln (col - 1)) position) ""] + Just $ List [TextEdit (Range (Position ln (col - 1)) position) ""] -- tempReplaceWithSymbol = Just $ CompletionEditText $ TextEdit (Range position (Position ln (col + 1 ))) "symbol" + +specBracketsCompletionItem :: Position -> CompletionItem +specBracketsCompletionItem position = CompletionItem + { _label = "?" + , _kind = Just CiSnippet + , _tags = Nothing + , _detail = Nothing + , _documentation = Just (CompletionDocString "Type \"?\" and a space to insert a spec.") + , _deprecated = Nothing + , _preselect = Just True + , _sortText = Nothing + , _filterText = Nothing + , _insertText = Just "[! !]" + , _insertTextFormat = Just PlainText + , _insertTextMode = Nothing + , _textEdit = removeQuestionMark + , _additionalTextEdits = Nothing + , _commitCharacters = Just (List [" "]) + , _command = Nothing + , _xdata = Nothing + } + where + Position line column = position + removeQuestionMark = + Just $ CompletionEditText $ TextEdit (Range (Position line (column - 1)) position) "" \ No newline at end of file diff --git a/src/Server/Handler/CustomMethod.hs b/src/Server/Handler/CustomMethod.hs deleted file mode 100644 index 8d011d31..00000000 --- a/src/Server/Handler/CustomMethod.hs +++ /dev/null @@ -1,204 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE LambdaCase #-} -module Server.Handler.CustomMethod where - -import Control.Monad.Except ( throwError ) -import Control.Monad.State ( runState ) -import qualified Data.Aeson as JSON -import qualified Data.IntMap as IntMap -import Data.Loc ( Located(locOf) - , posCol - ) -import Data.Loc.Range -import qualified Data.Text as Text -import Data.Text ( Text ) -import Error ( Error(Others) ) -import GCL.Predicate -import qualified GCL.Substitution as Substitution -import Render ( Render(render), Section (Section), Deco(..), Block(..) ) -import Render.Predicate ( exprOfPred ) -import Pretty -import Server.CustomMethod -import Server.Monad hiding ( logText, bumpVersion ) -import Server.Pipeline -import Syntax.Abstract.Util ( programToScopeForSubstitution - ) - -import qualified Language.LSP.Types as J -import Data.String (IsString(fromString)) -import Server.Handler.Diagnostic (makeDiagnostic) - - -handleInspect :: Range -> PipelineM [ResKind] -handleInspect range = do - setLastSelection range - stage <- load - case stage of - Swept swept -> generateResponseAndDiagnostics swept - _ -> return [] - -handleRefine :: Range -> PipelineM [ResKind] -handleRefine range = do - mute True - setLastSelection range - source <- getSource - -- find the spec and its content in the source - (spec, payloadLines) <- refine source range - - -- add indentation to the content - let indentedPayload = case payloadLines of - [] -> "" - [x] -> x - (x : xs) -> - let indentation = - Text.replicate (posCol (rangeStart (specRange spec)) - 1) " " - in Text.unlines $ x : map (indentation <>) xs - - -- remove the brackets of the spec and leave only the content - source' <- editText (specRange spec) indentedPayload - - -- reload - parsed <- parse source' - converted <- convert parsed - typeChecked <- typeCheck converted - mute False - swept <- sweep typeChecked - - generateResponseAndDiagnostics swept - -handleInsertAnchor :: Text -> PipelineM [ResKind] -handleInsertAnchor hash = do - -- mute the event listener before editing the source - mute True - - -- range for appending the template of proof - source <- getSource - (_, abstract) <- parseProgram source - parsed <- parse source - converted <- convert parsed - typeChecked <- typeCheck converted - swept <- sweep typeChecked - -- read the PO here - let thePO = lookup hash $ map (\x->(poAnchorHash x,x)) (sweptPOs swept) - - -- template of proof to be appended to the source - let template = case thePO of - Nothing -> "" - Just po -> "{- #" <> hash <> "\n" - <> preExpr <> "\n" - <> "⇒" <> "\n" - <> postExpr <> "\n" - <> Text.pack (replicate len '=') - <> "\n\n-}\n" - where - preExpr = docToText $ pretty $ exprOfPred $ poPre po - postExpr = docToText $ pretty $ exprOfPred $ poPost po - len = max (max (Text.length preExpr) (Text.length postExpr) - 2) 5 - -- then insert - range <- case fromLoc (locOf abstract) of - Nothing -> throwError [Others "Cannot read the range of the program"] - Just x -> return x - - source' <- editText (Range (rangeEnd range) (rangeEnd range)) - ("\n\n" <> template) - -- - parsed' <- parse source' - converted' <- convert parsed' - typeChecked' <- typeCheck converted' - mute False - swept' <- sweep typeChecked' - generateResponseAndDiagnostics swept' - --- handleInsertAnchor :: Text -> PipelineM [ResKind] --- handleInsertAnchor hash = do --- -- mute the event listener before editing the source --- mute True --- -- template of proof to be appended to the source --- let template = "{- #" <> hash <> "\n\n-}" --- -- range for appending the template of proof --- source <- getSource --- (_, abstract) <- parseProgram source --- range <- case fromLoc (locOf abstract) of --- Nothing -> throwError [Others "Cannot read the range of the program"] --- Just x -> return x - --- source' <- editText (Range (rangeEnd range) (rangeEnd range)) --- ("\n\n" <> template) --- parsed <- parse source' --- converted <- convert parsed --- typeChecked <- typeCheck converted --- mute False --- swept <- sweep typeChecked --- generateResponseAndDiagnostics swept - -handleSubst :: Int -> PipelineM [ResKind] -handleSubst i = do - stage <- load - logText $ Text.pack $ "Substituting Redex " <> show i - -- - case stage of - Raw _ -> return [] - Parsed _ -> return [] - Converted _ -> return [] - TypeChecked _ -> return [] - Swept result -> do - let program = convertedProgram - (typeCheckedPreviousStage (sweptPreviousStage result)) - case IntMap.lookup i (sweptRedexes result) of - Nothing -> return [] - Just (_, redex) -> do - let scope = programToScopeForSubstitution program - let (newExpr, counter) = - runState (Substitution.step scope redex) (sweptCounter result) - let redexesInNewExpr = Substitution.buildRedexMap newExpr - let newResult = result - { sweptCounter = counter - , sweptRedexes = sweptRedexes result <> redexesInNewExpr - } - save (Swept newResult) - return [ResSubstitute i (render newExpr)] - -handleHelloWorld :: Range -> PipelineM [ResKind] -handleHelloWorld range = do - logText "Hello, world!" - _ <- sendDiagnostics [makeDiagnostic Nothing range "Hello, World?" "This is a warning" ] - version <- bumpVersion - let titleBlock = Header "Hello, world" Nothing - let contentBlock = Paragraph $ fromString "LSP server successfully responded." - return [ResDisplay version [Section Blue [titleBlock, contentBlock]]] - -handleCustomMethod :: ReqKind -> PipelineM [ResKind] -handleCustomMethod = \case - ReqInspect range -> handleInspect range - ReqRefine range -> handleRefine range - ReqInsertAnchor hash -> handleInsertAnchor hash - ReqSubstitute i -> handleSubst i - ReqDebug -> return $ error "crash!" - ReqHelloWorld range -> handleHelloWorld range - _ -> return $ error "Not yet implemented." - -handler :: JSON.Value -> (Response -> ServerM ()) -> ServerM () -handler params responder = do - -- JSON Value => Request => Response - case JSON.fromJSON params of - JSON.Error msg -> do - -- logText - -- $ " --> CustomMethod: CannotDecodeRequest " - -- <> Text.pack (show msg) - -- <> " " - -- <> Text.pack (show params) - responder $ CannotDecodeRequest $ show msg ++ "\n" ++ show params - JSON.Success requests -> handleRequests requests - where - -- make the type explicit to appease the type checker - handleRequests :: [Request] -> ServerM () - handleRequests = mapM_ handleRequest - - -- convert Request to Response and Diagnostics - handleRequest :: Request -> ServerM () - handleRequest request@(Req filepath kind) = - interpret (J.filePathToUri filepath) - (customRequestResponder filepath responder) - $ do - logText $ "\n ---> Custom Reqeust: " <> Text.pack (show request) - handleCustomMethod kind diff --git a/src/Server/Handler/Diagnostic.hs b/src/Server/Handler/Diagnostic.hs deleted file mode 100644 index 44e691f9..00000000 --- a/src/Server/Handler/Diagnostic.hs +++ /dev/null @@ -1,182 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE FlexibleInstances #-} -module Server.Handler.Diagnostic where - -import Data.Loc hiding ( fromLoc ) -import Data.Loc.Range -import Data.Loc.Util ( translate ) -import Data.Text ( Text ) -import qualified Data.Text as Text -import Error ( Error(..) ) -import GCL.Predicate ( Origin(..) - , PO(..) - ) -import GCL.Type ( TypeError(..) ) -import GCL.WP.Type ( StructError(..) - , StructWarning(..) - ) -import Language.LSP.Types hiding ( ParseError - , Range - , TextDocumentSyncClientCapabilities(..) - , line - ) -import Pretty -import qualified Server.SrcLoc as SrcLoc -import Syntax.Parser.Error as Parser - ( ParseError(..) ) - -instance Collect StructError Diagnostic where - collect (MissingAssertion loc) = makeError - loc - "Assertion Missing" - "Assertion before the DO construct is missing" - collect (MissingPostcondition loc) = makeError - loc - "Postcondition Missing" - "The last statement of the program should be an assertion" - collect (MultiDimArrayAsgnNotImp loc) = - makeError loc "Assignment to Multi-Dimensional Array" "Not implemented yet" - collect (LocalVarExceedScope loc) = - makeError loc "Local variable(s) exceeded scope" - "Variables defined in a block must not remain in preconditions out of the block" - -instance Collect Error Diagnostic where - collect (ParseError err) = collect err - collect (StructError err) = collect err - collect (TypeError err) = collect err - collect _ = [] - -instance Collect Parser.ParseError Diagnostic where - collect (LexicalError pos) = makeError (Loc pos pos) "Lexical error" mempty - collect (SyntacticError pairs _) = concatMap -- the second argument is parsing log, used for debugging - (\(loc, msg) -> makeError loc "Parse error" (Text.pack msg)) - pairs - -instance Collect TypeError Diagnostic where - collect (NotInScope name) = - makeError (locOf name) "Not in scope" - $ docToText - $ "The definition " - <> pretty name - <> " is not in scope" - collect (UnifyFailed s t loc) = - makeError loc "Cannot unify types" - $ docToText - $ "Cannot unify:" - <+> pretty s - <> line - <> "with :" - <+> pretty t - - collect (RecursiveType var t loc) = - makeError loc "Recursive type variable" - $ docToText - $ "Recursive type variable:" - <+> pretty var - <> line - <> "in type :" - <+> pretty t - - collect (AssignToConst n) = - makeError (locOf n) "Assigned To Const" - $ docToText - $ "Assigned to constant:" - <+> pretty n - - collect (UndefinedType n) = - makeError (locOf n) "Undefined Type" - $ docToText - $ "Type" - <+> pretty n - <+> "is undefined" - - collect (DuplicatedIdentifiers ns) = - makeError (locOf ns) "Duplicated Identifiers" - $ docToText - $ "Duplicated identifiers" - <+> pretty ns - - collect (RedundantNames ns) = - makeError (locOf ns) "Redundant Names" - $ docToText - $ "Redundant names" - <+> pretty ns - - collect (RedundantExprs exprs) = - makeError (locOf exprs) "Redundant Exprs" - $ docToText - $ "Redundant exprs" - <+> pretty exprs - - collect (MissingArguments ns) = - makeError (locOf ns) "Missing Arguments" - $ docToText - $ "Missing arguments" - <+> pretty ns - -instance Collect StructWarning Diagnostic where - collect (MissingBound range) = makeWarning - (locOf range) - "Bound Missing" - "Bound missing at the end of the assertion before the DO construct \" , bnd : ... }\"" - collect (ExcessBound range) = makeWarning - (locOf range) - "Excess Bound" - "Unnecessary bound annotation at this assertion" - -instance Collect PO Diagnostic where - collect (PO _pre _post _anchorHash _anchorLoc origin) = makeWarning loc - title - "" - where - -- we only mark the opening tokens ("do" and "if") for loops & conditionals - first2Char :: Loc -> Loc - first2Char NoLoc = NoLoc - first2Char (Loc start _) = Loc start (translate 2 start) - - loc :: Loc - loc = case origin of - AtLoop l -> first2Char l - AtTermination l -> first2Char l - AtIf l -> first2Char l - Explain _ _ _ True l -> first2Char l -- Explain with "originHighlightPartial" as True - others -> locOf others - - title :: Text - title = toText origin - -makeError :: Loc -> Text -> Text -> [Diagnostic] -makeError loc title body = case fromLoc loc of - Nothing -> [] - Just range -> [makeDiagnostic (Just DsError) range title body] - -makeWarning :: Loc -> Text -> Text -> [Diagnostic] -makeWarning loc title body = case fromLoc loc of - Nothing -> [] - Just range -> [makeDiagnostic (Just DsWarning) range title body] - -makeDiagnostic - :: Maybe DiagnosticSeverity -> Range -> Text -> Text -> Diagnostic -makeDiagnostic severity range title body = Diagnostic - (SrcLoc.toLSPRange range) - severity - Nothing - Nothing - title - Nothing - (Just $ List [DiagnosticRelatedInformation (SrcLoc.toLSPLocation range) body]) - --------------------------------------------------------------------------------- - -class Collect a b where - collect :: a -> [b] - -instance Collect a b => Collect (Maybe a) b where - collect Nothing = [] - collect (Just x) = collect x - -instance (Collect a x, Collect b x) => Collect (Either a b) x where - collect (Left a) = collect a - collect (Right a) = collect a diff --git a/src/Server/Handler/GoToDefinition.hs b/src/Server/Handler/GoToDefinition.hs new file mode 100644 index 00000000..fd667f68 --- /dev/null +++ b/src/Server/Handler/GoToDefinition.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Use forM_" #-} + +module Server.Handler.GoToDefinition where + +import qualified Language.LSP.Types as LSP +import Server.Monad (ServerM, FileState (..), readSource, loadFileState, logText) + + +import qualified Server.SrcLoc as SrcLoc +import qualified Server.IntervalMap as IntervalMap +import Server.PositionMapping( PositionResult( PositionExact ), fromDelta, PositionDelta, toCurrentRange, PositionMapping(..), toCurrentRange' ) + +handler :: LSP.Uri -> LSP.Position -> ([LSP.LocationLink] -> ServerM ()) -> ServerM () +handler uri lspPosition responder = do + case LSP.uriToFilePath uri of + Nothing -> responder [] + Just filePath -> do + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> responder [] + Just FileState + { definitionLinks + , positionDelta + , toOffsetMap + } -> do + case (fromDelta positionDelta) lspPosition of + PositionExact oldLspPosition -> do + let oldPos = SrcLoc.fromLSPPosition toOffsetMap filePath oldLspPosition + case IntervalMap.lookup oldPos definitionLinks of + Nothing -> responder [] + Just locationLink -> responder $ translateLocationLinks positionDelta [locationLink] + _ -> responder [] + +-- TODO: currently, we assume source and target are in the same file +-- and translate both source and target with the same positionDelta +-- extend this translation to use positionDelta of other fileUri if target is in another file +translateLocationLinks :: PositionDelta -> [LSP.LocationLink] -> [LSP.LocationLink] +translateLocationLinks delta links = do + link <- links + case translateLocationLink delta link of + Nothing -> [] + Just link' -> [link'] + +translateLocationLink :: PositionDelta -> LSP.LocationLink -> Maybe LSP.LocationLink +translateLocationLink delta (LSP.LocationLink maybeSource targetUri targetRange targetSelection) = do + let maybeSource' = do + source <- maybeSource + translateRange source + targetRange' <- translateRange targetRange + targetSelection' <- translateRange targetSelection + return (LSP.LocationLink maybeSource' targetUri targetRange' targetSelection') + where + translateRange :: LSP.Range -> Maybe LSP.Range + translateRange = toCurrentRange' delta \ No newline at end of file diff --git a/src/Server/Handler/GoToDefn.hs b/src/Server/Handler/GoToDefn.hs deleted file mode 100644 index e5f68708..00000000 --- a/src/Server/Handler/GoToDefn.hs +++ /dev/null @@ -1,48 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} - -module Server.Handler.GoToDefn - ( handler - ) where - -import Data.Maybe ( maybeToList ) -import Error ( Error ) -import Language.LSP.Types hiding ( Range ) -import qualified Language.LSP.Types as LSP -import Server.Monad hiding ( logText ) -import Server.Pipeline -import qualified Server.SrcLoc as SrcLoc -import qualified Server.IntervalMap as IntervalMap - -ignoreErrors :: ([Error], Maybe [LSP.LocationLink]) -> [LSP.LocationLink] -ignoreErrors (_, Nothing) = [] -ignoreErrors (_, Just xs) = xs - -handler :: Uri -> Position -> ([LSP.LocationLink] -> ServerM ()) -> ServerM () -handler uri position responder = do - case uriToFilePath uri of - Nothing -> return () - Just filepath -> do - interpret uri (responder . ignoreErrors) $ do - logText "<-- Goto Definition" - source <- getSource - - let table = SrcLoc.makeToOffset source - let pos = SrcLoc.fromLSPPosition table filepath position - - stage <- load - let - tokenMap = case stage of - Raw _ -> Nothing - Parsed _result -> Nothing - Converted result -> Just $ convertedIntervalMap result - TypeChecked result -> - Just $ convertedIntervalMap (typeCheckedPreviousStage result) - Swept result -> - Just $ convertedIntervalMap - (typeCheckedPreviousStage (sweptPreviousStage result)) - - return $ maybeToList $ case tokenMap of - Nothing -> Nothing - Just xs -> IntervalMap.lookup pos xs \ No newline at end of file diff --git a/src/Server/Handler/Guabao/Refine.hs b/src/Server/Handler/Guabao/Refine.hs new file mode 100644 index 00000000..dbc6ab65 --- /dev/null +++ b/src/Server/Handler/Guabao/Refine.hs @@ -0,0 +1,312 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -Wno-name-shadowing #-} + +module Server.Handler.Guabao.Refine where + +import qualified Data.Aeson as JSON +import GHC.Generics ( Generic ) +import Data.Bifunctor ( bimap ) +import Control.Monad.Except ( runExcept ) +import Server.Monad (ServerM, FileState(..), loadFileState, editTexts, pushSpecs, deleteSpec, Versioned, pushPos, updateIdCounter, logText, saveFileState) +import Server.Notification.Update (sendUpdateNotification) +import Server.Notification.Error (sendErrorNotification) + +import qualified Syntax.Parser as Parser +import Syntax.Parser.Error ( ParseError(..) ) +import Syntax.Parser.Lexer (TokStream(..), scan) +import Language.Lexer.Applicative ( TokenStream(..)) + +import Error (Error (ParseError, TypeError, StructError, Others)) +import GCL.Predicate (Spec(..), PO (..), InfMode(..), Origin (..)) +import GCL.Common (TypeEnv, Index, TypeInfo) +import GCL.Type (Elab(..), TypeError, runElaboration, Typed) +import Data.Loc.Range (Range (..), rangeStart) +import Data.Text (Text, split, unlines, lines) +import Data.List (find, maximumBy) +import Data.Loc (Pos(..), Loc(..), L(..)) +import qualified Data.Map as Map +import qualified Syntax.Concrete as C +import qualified Syntax.Abstract as A +import qualified Syntax.Typed as T +import GCL.WP.Types (StructError, StructWarning) +import GCL.WP +import qualified Data.Text as Text +import Pretty (pretty) + +data RefineParams = RefineParams + { filePath :: FilePath + , implText :: Text + , specLines :: Range + , implStart :: Pos + } + deriving (Eq, Show, Generic) + +instance JSON.FromJSON RefineParams +instance JSON.ToJSON RefineParams + +-- Assumes. specLines contains all the lines from "[!" to "!]" +-- Assumes. implText contains the lines between but not including "[!" and "!]" +-- Assumes. implStart is the start of the line following "[!" +handler :: RefineParams -> (() -> ServerM ()) -> (() -> ServerM ()) -> ServerM () +handler _params@RefineParams{filePath, specLines, implText, implStart} onFinish _ = do + logText "refine: start\n" + logText " params\n" + logText . Text.pack . show $ _params + logText "\n" + logText " specLines:\n" + logText . Text.pack . show $ specLines + logText "\n" + -- 把上次 load 的資料拿出來 + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> do + logText " no fileState matched\n" + return () + Just fileState -> do + logText " fileState loaded\n" + logText " implText:\n" + logText implText + logText "\n" + -- 挖洞 + -- let (Range implStart _) = implLines + -- let implStart = rangeStart implLines + let (Range specStart _) = specLines + -- let implStart = getImplStart specStart + case digImplHoles implStart filePath implText of + Left err -> do + logText " parse error\n" + onError (ParseError err) + Right holelessImplText -> do + logText " holes digged\n" + logText " (after)\n" + logText holelessImplText + logText "\n" + -- text to concrete + -- (use specStart as the starting position in parse/toAbstract/elaborate) + logText " parsing\n" + logText " specStart =\n" + logText . Text.pack . show . pretty $ specStart + logText "\n" + case parseFragment implStart holelessImplText of + Left err -> onError (ParseError err) + Right concreteImpl -> do + -- concrete to abstract + logText " text parsed\n" + case toAbstractFragment concreteImpl of + Nothing -> do + onError (Others "holes still found after digging all holes") + error "should not happen\n" + Just abstractImpl -> do + logText " abstracted\n" + -- get spec (along with its type environment) + let FileState{specifications} = fileState + logText " looking for specs\n" + case lookupSpecByLines specifications specLines of + Nothing -> do + logText " spec not found at range, should reload\n" + onError (Others "spec not found at range, should reload") + Just spec -> do + logText " matching spec found\n" + -- elaborate + let typeEnv = specTypeEnv spec + logText " type env:\n" + logText (Text.pack $ show typeEnv) + logText "\n" + -- TODO: + -- 1. Load: 在 elaborate program 的時候，要把 specTypeEnv 加到 spec 裡 (Andy) ok + -- 2. Load: 在 sweep 的時候，改成輸入 elaborated program，把 elaborated program 裡面的 spec 的 typeEnv 加到輸出的 [Spec] 裡 (SCM) + -- 3. Refine: elaborateFragment 裡面要正確使用 typeEnv (Andy) ok + case elaborateFragment typeEnv abstractImpl of + Left err -> do + logText " type error\n" + onError (TypeError err) + Right typedImpl -> do + -- get POs and specs + logText " type checked\n" + let FileState{idCount} = fileState + case sweepFragment idCount spec typedImpl of + Left err -> onError (StructError err) + Right (innerPos, innerSpecs, warnings, idCount') -> do + logText " swept\n" + -- delete outer spec (by id) + deleteSpec filePath spec + logText " outer spec deleted (refine)\n" + -- add inner specs to fileState + let FileState{editedVersion} = fileState + updateIdCounter filePath idCount' + logText " counter updated (refine)\n" + let innerSpecs' = predictAndTranslateSpecRanges innerSpecs + let innerPos' = predictAndTranslatePosRanges innerPos + pushSpecs (editedVersion + 1) filePath innerSpecs' + pushPos (editedVersion + 1) filePath innerPos' + -- let FileState{specifications, proofObligations} = fileState + -- let fileState' = fileState + -- { specifications = specifications ++ Prelude.map (\spec -> (editedVersion + 1, spec)) innerSpecs' + -- , proofObligations = proofObligations ++ Prelude.map (\po -> (editedVersion + 1, po)) innerPos' + -- } + + -- saveFileState filePath fileState' + + logText " new specs and POs added (refine)\n" + -- send notification to update Specs and POs + logText "refine: success\n" + sendUpdateNotification filePath + -- -- clear errors + sendErrorNotification filePath [] + logText "refine: update notification sent\n" + -- edit source (dig holes + remove outer brackets) + editTexts filePath [(specLines, holelessImplText)] do + logText " text edited (refine)\n" + onFinish () + logText "refine: end\n" + where + onError :: Error -> ServerM () + onError err = do + logText "refine: error\n\t" + logText $ Text.pack (show $ pretty err) + logText "\n" + sendErrorNotification filePath [err] + logText "refine: update notification sent\n" + minusOneLine :: Pos -> Pos + minusOneLine (Pos filePath line column byte) = Pos filePath (line - 1) column 0 + predictAndTranslateSpecRanges :: [Spec] -> [Spec] + predictAndTranslateSpecRanges = map (\spec@Specification{specRange} -> spec{specRange = minusOneLine' specRange}) + where + minusOneLine' :: Range -> Range + minusOneLine' (Range start end) = Range (minusOneLine start) (minusOneLine end) + predictAndTranslatePosRanges :: [PO] -> [PO] + predictAndTranslatePosRanges = map (\po@PO{poOrigin} -> po{poOrigin = modifyOriginLocation minusOneLine' poOrigin}) + where + minusOneLine' :: Loc -> Loc + minusOneLine' NoLoc = NoLoc + minusOneLine' (Loc start end) = Loc (minusOneLine start) (minusOneLine end) + modifyOriginLocation :: (Loc -> Loc) -> Origin -> Origin + modifyOriginLocation f (AtAbort l) = AtAbort (f l) + modifyOriginLocation f (AtSkip l) = AtSkip (f l) + modifyOriginLocation f (AtSpec l) = AtSpec (f l) + modifyOriginLocation f (AtAssignment l) = AtAssignment (f l) + modifyOriginLocation f (AtAssertion l) = AtAssertion (f l) + modifyOriginLocation f (AtIf l) = AtIf (f l) + modifyOriginLocation f (AtLoop l) = AtLoop (f l) + modifyOriginLocation f (AtTermination l) = AtTermination (f l) + modifyOriginLocation f (Explain h e i p l) = Explain h e i p (f l) + +-- 把每一行都拿掉 +removeOneIndentation :: Text -> Text +removeOneIndentation implText = Text.intercalate "\n" $ map (Text.drop 4) (Text.lines implText) + +lookupSpecByLines :: [Versioned Spec] -> Range -> Maybe Spec +lookupSpecByLines specs targetLines = do + (_version, spec) <- find (\(_, Specification{specRange}) -> coverSameLines specRange targetLines) specs + return spec + where + coverSameLines :: Range -> Range -> Bool + coverSameLines (Range (Pos _ lineStart _ _) (Pos _ lineEnd _ _)) (Range (Pos _ lineStart' _ _) (Pos _ lineEnd' _ _)) + = (lineStart == lineStart') && (lineEnd == lineEnd') + +collectFragmentHoles :: [C.Stmt] -> [Range] +collectFragmentHoles concreteFragment = do + statement <- concreteFragment + case statement of + C.SpecQM range -> return range + _ -> [] + +digImplHoles :: Pos -> FilePath -> Text -> Either ParseError Text +digImplHoles parseStart filePath implText = + -- use `parseStart` for absolute positions in error messages + case parseFragment parseStart implText of + Left err -> Left err + Right _ -> + -- use `Pos filePath 1 1 0` for relative position of the hole reported + case parseFragment (Pos filePath 1 1 0) implText of + Left _ -> error "should not happen" + Right concreteImpl -> + case collectFragmentHoles concreteImpl of + [] -> return implText + Range start _ : _ -> digImplHoles parseStart filePath $ digFragementHole start implText + where + digFragementHole :: Pos -> Text -> Text + digFragementHole (Pos _path lineNumber col _charOff) fullText = + Text.intercalate "\n" linesEdited + where + allLines :: [Text] + allLines = Text.lines fullText -- split fullText by '\n' + lineToEdit :: Text + lineToEdit = allLines !! (lineNumber - 1) + beforeHole = Text.take (col-1) lineToEdit + afterHole = Text.drop col lineToEdit -- lineToEdit + indentation n = Text.replicate n " " + lineEdited :: Text + lineEdited = beforeHole <> "[!\n" <> + indentation (col-1) <> "\n" <> + indentation (col-1) <> "!]" <> afterHole + linesEdited :: [Text] + linesEdited = take (lineNumber - 1) allLines ++ [lineEdited] ++ drop lineNumber allLines + +-- `fragmentStart :: Pos` is used to translate the locations in the parse result +parseFragment :: Pos -> Text -> Either ParseError [C.Stmt] +parseFragment fragmentStart fragment = do + let Pos filePath _ _ _ = fragmentStart + case Syntax.Parser.Lexer.scan filePath fragment of + Left err -> Left (LexicalError err) + Right tokens -> do + let tokens' = translateTokStream fragmentStart tokens + case Parser.parse Parser.statements filePath tokens' of + Left (errors,logMsg) -> Left (SyntacticError errors logMsg) + Right val -> Right val + where + translateRange :: Pos -> Pos -> Pos + translateRange _fragmentStart@(Pos _ lineStart colStart coStart) + (Pos path lineOffset colOffset coOffset) + = Pos path line col co + where + line = lineStart + lineOffset - 1 + col = if lineOffset == 1 + then colStart + colOffset - 1 + else colOffset + co = coStart + coOffset + + translateLoc :: Pos -> Loc -> Loc + translateLoc fragmentStart (Loc left right) + = Loc (translateRange fragmentStart left) (translateRange fragmentStart right) + translateLoc _ NoLoc = NoLoc + + translateTokStream :: Pos -> Syntax.Parser.Lexer.TokStream -> Syntax.Parser.Lexer.TokStream + translateTokStream fragmentStart (TsToken (L loc x) rest) + = TsToken (L (translateLoc fragmentStart loc) x) (translateTokStream fragmentStart rest) + translateTokStream _ TsEof = TsEof + translateTokStream _ (TsError e) = TsError e + +toAbstractFragment :: [C.Stmt] -> Maybe [A.Stmt] +toAbstractFragment concreteFragment = + case runExcept $ C.toAbstract concreteFragment of + Left _ -> Nothing + Right abstractFragment -> Just abstractFragment + +elaborateFragment :: Elab a => [(Index, TypeInfo)] -> a -> Either TypeError (Typed a) +elaborateFragment typeEnv abstractFragment = do + runElaboration abstractFragment typeEnv + +instance Elab [A.Stmt] where + -- elaborate :: a -> TypeEnv -> ElaboratorM (Maybe Type, Typed a, Subs Type) + elaborate stmts env = do + typed <- mapM (\stmt -> do + (_, typed, _) <- elaborate stmt env + return typed + ) stmts + return (Nothing, typed, mempty) + + +sweepFragment :: Int -> Spec -> [T.Stmt] -> Either StructError ([PO], [Spec], [StructWarning], Int) +sweepFragment counter (Specification _ pre post _ _) impl = + bimap id (\(_, counter', (pos, specs, sws, _)) -> + (pos, specs, sws, counter')) + $ runWP (structStmts Primary (pre, Nothing) impl post) + (Map.empty, []) -- SCM: this can't be right. + counter diff --git a/src/Server/Handler/Guabao/Reload.hs b/src/Server/Handler/Guabao/Reload.hs new file mode 100644 index 00000000..1d41ade0 --- /dev/null +++ b/src/Server/Handler/Guabao/Reload.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE DuplicateRecordFields #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE DeriveGeneric #-} + +module Server.Handler.Guabao.Reload where + +import qualified Data.Aeson.Types as JSON +import GHC.Generics ( Generic ) +import Server.Monad (ServerM, FileState(..), Versioned, sendDebugMessage) +import Error (Error) +import GCL.Predicate (Spec, PO) +import Server.Load (load) + +data ReloadParams = ReloadParams { filePath :: FilePath } + deriving (Eq, Show, Generic) + +instance JSON.FromJSON ReloadParams +instance JSON.ToJSON ReloadParams + +handler :: ReloadParams -> (() -> ServerM ()) -> (() -> ServerM ()) -> ServerM () +handler ReloadParams{filePath} onResult _ = do + load filePath + onResult () diff --git a/src/Server/Handler/Hover.hs b/src/Server/Handler/Hover.hs index eaebc53b..84c747ad 100644 --- a/src/Server/Handler/Hover.hs +++ b/src/Server/Handler/Hover.hs @@ -1,53 +1,47 @@ -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE FlexibleInstances #-} -module Server.Handler.Hover - ( handler - ) where +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE NamedFieldPuns #-} -import Error ( Error ) -import Server.Monad hiding ( logText ) +module Server.Handler.Hover where -import Data.Loc ( posCoff ) -import Language.LSP.Types hiding ( Range ) -import Pretty ( toText ) -import Server.Pipeline +import qualified Language.LSP.Types as LSP import qualified Server.SrcLoc as SrcLoc -import qualified Server.IntervalMap as IntervalMap - -ignoreErrors :: ([Error], Maybe (Maybe Hover)) -> Maybe Hover -ignoreErrors (_, Nothing) = Nothing -ignoreErrors (_, Just xs) = xs - -handler :: Uri -> Position -> (Maybe Hover -> ServerM ()) -> ServerM () -handler uri position responder = case uriToFilePath uri of - Nothing -> return () - Just filepath -> do - interpret uri (responder . ignoreErrors) $ do - source <- getSource - let table = SrcLoc.makeToOffset source - let pos = SrcLoc.fromLSPPosition table filepath position - logText $ " ---> Hover " <> toText (posCoff pos) - - stage <- load - - let - tokenMap = case stage of - Raw _ -> Nothing - Parsed _ -> Nothing - Converted _ -> Nothing - TypeChecked result -> Just $ typeCheckedIntervalMap result - Swept result -> - Just $ typeCheckedIntervalMap (sweptPreviousStage result) - - case tokenMap of - Nothing -> return Nothing - Just xs -> case IntervalMap.lookup pos xs of - Nothing -> do - -- logText $ toText xs - logText " < Hover (not found)" - return Nothing - Just (hover, _) -> do - logText $ " < Hover " <> toText hover - return (Just hover) +import qualified Server.IntervalMap as IntervalMap +import Server.PositionMapping (PositionDelta, toCurrentRange, PositionMapping(..), PositionResult(..), fromDelta) + +import Server.Monad (ServerM, FileState (..), loadFileState, logText) + +handler :: LSP.Uri -> LSP.Position -> (Maybe LSP.Hover -> ServerM ()) -> ServerM () +handler uri lspPosition responder = do + logText "hover: start\n" + case LSP.uriToFilePath uri of + Nothing -> do + logText "hover: failed - uri not valid\n" + responder Nothing + Just filePath -> do + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> do + logText "hover: failed - not loaded yet\n" + responder Nothing + Just FileState{hoverInfos, positionDelta, toOffsetMap} -> do + case fromDelta positionDelta lspPosition of + PositionExact oldLspPosition -> do + let oldPos = SrcLoc.fromLSPPosition toOffsetMap filePath oldLspPosition + case IntervalMap.lookup oldPos hoverInfos of + Nothing -> do + logText "hover: not exist - no information for this position\n" + responder Nothing + Just (hover, _type) -> do + logText "hover: success\n" + responder $ Just $ toCurrentHover positionDelta hover + logText "hover: response sent\n" + _ -> do + logText "hover: not exist - new position after last reload\n" + responder Nothing + logText "hover: end\n" + +toCurrentHover :: PositionDelta -> LSP.Hover -> LSP.Hover +toCurrentHover positionDelta (LSP.Hover contents maybeRange) + = LSP.Hover contents (maybeRange >>= toCurrentRange (PositionMapping positionDelta)) \ No newline at end of file diff --git a/src/Server/Handler2/Initialized.hs b/src/Server/Handler/Initialized.hs similarity index 53% rename from src/Server/Handler2/Initialized.hs rename to src/Server/Handler/Initialized.hs index 3185bafd..81dad27b 100644 --- a/src/Server/Handler2/Initialized.hs +++ b/src/Server/Handler/Initialized.hs @@ -1,26 +1,21 @@ {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} -module Server.Handler2.Initialized (handler) where +module Server.Handler.Initialized (handler) where import qualified Data.Text as Text import qualified Language.LSP.Server as LSP import qualified Language.LSP.Types as LSP -import Server.Handler2.Utils import Server.Monad (ServerM) handler :: ServerM () handler = do - logText "initialized" + -- logText "initialized" let requestParams = LSP.ShowMessageRequestParams LSP.MtInfo "GCL Server Initialized." Nothing - _ <- LSP.sendRequest LSP.SWindowShowMessageRequest requestParams $ \case - Right _ -> - LSP.sendNotification LSP.SWindowShowMessage (LSP.ShowMessageParams LSP.MtInfo "BTW, nice to meet you!") - Left err -> - LSP.sendNotification LSP.SWindowShowMessage (LSP.ShowMessageParams LSP.MtError $ "Oops, something went wrong...\n" <> Text.pack (show err)) + _ <- LSP.sendRequest LSP.SWindowShowMessageRequest requestParams $ \_ -> return () return () \ No newline at end of file diff --git a/src/Server/Handler/OnDidChangeTextDocument.hs b/src/Server/Handler/OnDidChangeTextDocument.hs new file mode 100644 index 00000000..78a788b4 --- /dev/null +++ b/src/Server/Handler/OnDidChangeTextDocument.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Server.Handler.OnDidChangeTextDocument where + +import Server.Monad (ServerM, FileState (..), modifyFileState, Versioned, logText, logFileState) +import Server.Notification.Update (sendUpdateNotification) +import GCL.Predicate (Spec(..), PO (..), Origin (..)) +import Server.PositionMapping (mkDelta, applyChange, toCurrentRange', PositionDelta) +import qualified Language.LSP.Types as LSP +import qualified Server.SrcLoc as SrcLoc +import Data.Loc.Range (Range (..), fromLoc) +import Data.Loc (Loc (..), Located (..)) + +handler :: FilePath -> [LSP.TextDocumentContentChangeEvent] -> ServerM () +handler filePath changes = do + modifyFileState filePath (\filesState@FileState{positionDelta, editedVersion, specifications, proofObligations} -> + filesState + { positionDelta = foldl applyChange positionDelta changes + , editedVersion = editedVersion + 1 + , specifications = translateThroughOneVersion translateSpecRange editedVersion specifications + , proofObligations = translateThroughOneVersion translatePoRange editedVersion proofObligations + } + ) + logFileState filePath (map (\(version, Specification{specRange}) -> (version, specRange)) . specifications) + + -- send notification to update Specs and POs + logText "didChange: fileState modified\n" + sendUpdateNotification filePath + logText "didChange: upate notification sent\n" + where + translateThroughOneVersion + :: (FilePath -> PositionDelta -> a -> Maybe a) + -> Int -> [Versioned a] -> [Versioned a] + translateThroughOneVersion translator fromVersion versioned = do + (version, a) <- versioned + let delta :: PositionDelta = mkDelta changes + if fromVersion == version then + case translator filePath delta a of + Nothing -> [] + Just spec' -> [(version + 1, spec')] + else if fromVersion + 1 == version then + [(version, a)] + else error "should not happen" + +-- 目前只維護 specRange，而沒有更新 specPre 和 specPost 裡面的位置資訊 +-- 如果未來前端有需要的話，請在這裡維護 +translateSpecRange :: FilePath -> PositionDelta -> Spec -> Maybe Spec +translateSpecRange filePath delta spec@Specification{specRange = oldRange} = do + let oldLspRange :: LSP.Range = SrcLoc.toLSPRange oldRange + currentLspRange :: LSP.Range <- toCurrentRange' delta oldLspRange + let newRange = SrcLoc.fromLSPRangeWithoutCharacterOffset filePath currentLspRange + return $ spec {specRange = newRange} + +-- 目前只維護 poOrigin 裡面的 location，而沒有更新 poPre 和 poPost 裡面的位置資訊 +-- 如果未來前端有需要的話，請在這裡維護 +translatePoRange :: FilePath -> PositionDelta -> PO -> Maybe PO +translatePoRange filePath delta po@PO{poOrigin} = do + oldRange :: Range <- fromLoc (locOf poOrigin) + let oldLspRange :: LSP.Range = SrcLoc.toLSPRange oldRange + currentLspRange :: LSP.Range <- toCurrentRange' delta oldLspRange + let _newRange@(Range x y) = SrcLoc.fromLSPRangeWithoutCharacterOffset filePath currentLspRange + return $ po {poOrigin = setOriginLocation (Loc x y) poOrigin} + +setOriginLocation :: Loc -> Origin -> Origin +setOriginLocation l (AtAbort _) = AtAbort l +setOriginLocation l (AtSkip _) = AtSkip l +setOriginLocation l (AtSpec _) = AtSpec l +setOriginLocation l (AtAssignment _) = AtAssignment l +setOriginLocation l (AtAssertion _) = AtAssertion l +setOriginLocation l (AtIf _) = AtIf l +setOriginLocation l (AtLoop _) = AtLoop l +setOriginLocation l (AtTermination _) = AtTermination l +setOriginLocation l (Explain h e i p _) = Explain h e i p l diff --git a/src/Server/Handler/SemanticTokens.hs b/src/Server/Handler/SemanticTokens.hs new file mode 100644 index 00000000..2db9384f --- /dev/null +++ b/src/Server/Handler/SemanticTokens.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE DuplicateRecordFields #-} + +module Server.Handler.SemanticTokens where + +import Server.Monad (ServerM, FileState (..), loadFileState, logText) +import qualified Language.LSP.Types as LSP +import Language.LSP.Types (SemanticTokenAbsolute(..), Position(..)) +import Server.PositionMapping (PositionDelta(..), PositionResult(..)) + +handler :: LSP.Uri -> (Either LSP.ResponseError (Maybe LSP.SemanticTokens) -> ServerM ()) -> ServerM () +handler fileUri responder = do + logText "semantic token: start\n" + case LSP.uriToFilePath fileUri of + Nothing -> respondError (LSP.ResponseError LSP.InvalidParams "Invalid uri" Nothing) + Just filePath -> do + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> respondError (LSP.ResponseError LSP.ServerNotInitialized "Please reload before requesting for semantic tokens." Nothing) + Just (FileState{semanticTokens = oldSemanticTokenAbsolutes, positionDelta}) + -> do + let newSemanticTokenAbsolutes = translatePositions positionDelta oldSemanticTokenAbsolutes + let legend = LSP.SemanticTokensLegend + (LSP.List LSP.knownSemanticTokenTypes) + (LSP.List LSP.knownSemanticTokenModifiers) + case LSP.makeSemanticTokens legend newSemanticTokenAbsolutes of + Left _errorMessage -> respondError (LSP.ResponseError LSP.InternalError _errorMessage Nothing) + Right semanticTokens -> respondResult semanticTokens + where + respondResult :: LSP.SemanticTokens -> ServerM () + respondResult result = responder (Right $ Just result) + respondError :: LSP.ResponseError -> ServerM () + respondError err = responder (Left err) + +translatePosition :: PositionDelta -> LSP.SemanticTokenAbsolute -> Maybe LSP.SemanticTokenAbsolute +translatePosition PositionDelta{toDelta} oldToken@(LSP.SemanticTokenAbsolute{line, startChar}) = + case toDelta oldPosition of + PositionExact (Position{_line, _character}) -> Just (oldToken{line = _line, startChar = _character}) + _ -> Nothing + where + oldPosition :: LSP.Position + oldPosition = LSP.Position line startChar + +translatePositions :: PositionDelta -> [LSP.SemanticTokenAbsolute] -> [LSP.SemanticTokenAbsolute] +translatePositions positionDelta oldTokens = do + oldToken <- oldTokens + case translatePosition positionDelta oldToken of + Nothing -> [] + Just newToken -> return newToken \ No newline at end of file diff --git a/src/Server/Handler2.hs b/src/Server/Handler2.hs deleted file mode 100644 index 4dcaa4b1..00000000 --- a/src/Server/Handler2.hs +++ /dev/null @@ -1,56 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DisambiguateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PolyKinds #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} - -module Server.Handler2 ( handlers ) where - -import Control.Lens ( (^.) ) -import qualified Data.Aeson as JSON -import Language.LSP.Server ( Handlers - , notificationHandler - , requestHandler - ) -import Server.Monad hiding (logText) - -import qualified Language.LSP.Types as LSP -import qualified Language.LSP.Types.Lens as LSP -import qualified Server.Handler2.Initialized as Initialized -import qualified Server.Handler.AutoCompletion as AutoCompletion -import qualified Server.Handler2.CustomMethod as CustomMethod -import qualified Server.Handler2.GoToDefinition as GoToDefinition -import qualified Server.Handler2.Hover as Hover -import qualified Server.Handler2.SemanticTokens as SemanticTokens - --- handlers of the LSP server -handlers :: Handlers ServerM -handlers = mconcat - [ -- "initialized" - after initialize - notificationHandler LSP.SInitialized $ \_ntf -> do - Initialized.handler - , -- "textDocument/completion" - autocompletion - requestHandler LSP.STextDocumentCompletion $ \req responder -> do - let completionContext = req ^. LSP.params . LSP.context - let position = req ^. LSP.params . LSP.position - AutoCompletion.handler position completionContext >>= responder . Right - , -- "textDocument/definition" - go to definition - requestHandler LSP.STextDocumentDefinition $ \req responder -> do - let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) - let pos = req ^. (LSP.params . LSP.position) - GoToDefinition.handler uri pos (responder . Right . LSP.InR . LSP.InR . LSP.List) - , -- "textDocument/hover" - get hover information - requestHandler LSP.STextDocumentHover $ \req responder -> do - let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) - let pos = req ^. (LSP.params . LSP.position) - Hover.handler uri pos (responder . Right) - , -- "textDocument/semanticTokens/full" - get all semantic tokens - requestHandler LSP.STextDocumentSemanticTokensFull $ \req responder -> do - let uri = req ^. (LSP.params . LSP.textDocument . LSP.uri) - SemanticTokens.handler uri responder - , -- "guabao" - reload, refine, inspect and etc. - requestHandler (LSP.SCustomMethod "guabao") $ \req responder -> do - let params = req ^. LSP.params - CustomMethod.handler params (responder . Right . JSON.toJSON) - ] - diff --git a/src/Server/Handler2/CustomMethod.hs b/src/Server/Handler2/CustomMethod.hs deleted file mode 100644 index 42875d22..00000000 --- a/src/Server/Handler2/CustomMethod.hs +++ /dev/null @@ -1,51 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE BlockArguments #-} - -module Server.Handler2.CustomMethod where - -import qualified Data.Aeson.Types as JSON - -import Server.CustomMethod (Response (..), Request (..), ReqKind (..), ResKind (..)) -import Server.Monad (ServerM) -import qualified Server.Monad (convertErrorsToResponsesAndDiagnostics) -import Error (Error(..)) - -import Server.Handler2.Utils -import qualified Server.Handler2.CustomMethod.Reload as Reload (handler) -import qualified Server.Handler2.CustomMethod.Inspect as Inspect (handler) -import qualified Server.Handler2.CustomMethod.Refine as Refine (slowHandler) -import qualified Server.Handler2.CustomMethod.InsertProofTemplate - as InsertProofTemplate (slowHandler) -import qualified Server.Handler2.CustomMethod.SubstituteRedex - as SubstituteRedex (handler) -import qualified Server.Handler2.CustomMethod.HelloWorld as HelloWorld (handler) - - -handler :: JSON.Value -> (Response -> ServerM ()) -> ServerM () -handler params responder = do - case JSON.fromJSON params :: JSON.Result [Request] of - JSON.Success [request] -> dispatchRequest request - JSON.Success _ -> error "should not happen" - JSON.Error msg -> responder $ CannotDecodeRequest $ show msg ++ "\n" ++ show params - where - dispatchRequest :: Request -> ServerM () - dispatchRequest _request@(Req filePath reqKind) = do - case reqKind of - ReqReload -> Reload.handler filePath respondResult reportError - ReqInspect range -> Inspect.handler range respondResult reportError - ReqRefine2 range text -> Refine.slowHandler range text respondResult reportError - ReqInsertProofTemplate range hash -> InsertProofTemplate.slowHandler filePath range hash respondResult reportError - ReqSubstitute redexNumber -> SubstituteRedex.handler filePath redexNumber respondResult reportError - ReqHelloWorld range -> HelloWorld.handler range respondResult reportError - _ -> reportError (Others "Not implemented yet.") - where - reportError :: Error -> ServerM () - reportError err = do - (responsesFromError, diagnosticsFromError) - <- Server.Monad.convertErrorsToResponsesAndDiagnostics [err] - sendDiagnostics filePath diagnosticsFromError - responder (Res filePath responsesFromError) - respondResult :: [ResKind] -> ServerM () - respondResult results = responder (Res filePath results) diff --git a/src/Server/Handler2/CustomMethod/HelloWorld.hs b/src/Server/Handler2/CustomMethod/HelloWorld.hs deleted file mode 100644 index 3b54a4c5..00000000 --- a/src/Server/Handler2/CustomMethod/HelloWorld.hs +++ /dev/null @@ -1,61 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE ScopedTypeVariables #-} -module Server.Handler2.CustomMethod.HelloWorld (handler) where - -import Data.String (fromString) -import Data.Loc.Range (Range (..), rangeFile, rangeStart, rangeEnd) - -import Render (Section (..), Deco (..), Block (..)) -import Error (Error(..)) - -import Server.Monad (ServerM) -import Server.Handler2.Utils -import Server.CustomMethod (ResKind (..)) -import Data.Loc (Pos (..), posFile, posLine, posCol, posCoff) -import Server.Handler.Diagnostic (makeDiagnostic) - - -handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handler range onFinish onError = do - let filepath :: FilePath = rangeFile range - replaceWithHelloworld filepath range (do - let helloWorldRange = rangeAfterReplacedWithHelloWorld range - let diagnosticOnHelloWorld = makeDiagnostic Nothing helloWorldRange "Hello, World?" "This is a warning" - _ <- sendDiagnostics filepath [diagnosticOnHelloWorld] - version <- bumpVersion - onFinish [ - ResDisplay version [ - Section Blue [ - Header "Hello, world" Nothing - , Paragraph $ fromString "LSP server successfully responded." - ] - ] - ] - ) onError - -replaceWithHelloworld :: FilePath -> Range -> ServerM () -> (Error -> ServerM ()) -> ServerM () -replaceWithHelloworld filepath range onFinish onError = do - maybeSource <- getSource filepath - case maybeSource of - Nothing -> onError (CannotReadFile filepath) - Just source -> do - logText "before replacement" - logText source - logText "\n" - editText range "Hello, World!\n" $ do - maybeSource' <- getSource filepath - case maybeSource' of - Nothing -> onError (CannotReadFile filepath) - Just source' -> do - logText "after replacement" - logText source' - logText "\n" - onFinish - -rangeAfterReplacedWithHelloWorld :: Range -> Range -rangeAfterReplacedWithHelloWorld range = - Range (rangeStart range) (addToCoff 13 $ rangeEnd range) - where - addToCoff :: Int -> Pos -> Pos - addToCoff offset pos = Pos (posFile pos) (posLine pos) (posCol pos) (posCoff pos + offset) diff --git a/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs b/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs deleted file mode 100644 index f735522e..00000000 --- a/src/Server/Handler2/CustomMethod/InsertProofTemplate.hs +++ /dev/null @@ -1,52 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE OverloadedStrings #-} - -module Server.Handler2.CustomMethod.InsertProofTemplate (slowHandler) where - -import Data.Text (Text) -import qualified Data.Text as Text -import qualified Data.List as List - -import Data.Loc.Range (Range (..)) -import Render.Predicate (exprOfPred) -import GCL.Predicate (PO(..)) -import Pretty (docToText, Pretty (..)) - -import Server.Monad (ServerM, LoadedProgram(..)) -import Server.Handler2.Utils -import Server.Handler2.CustomMethod.Reload as Reload -import Server.CustomMethod (ResKind) -import Error (Error (..)) - -slowHandler :: FilePath -> Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -slowHandler sourceFilePath rangeToInsertProof proofObligationHash onFinish onError = do - -- reload source - Reload.reload sourceFilePath (\loadedProgram -> do - -- find proof obligation by hash - let proofObligations :: [PO] = _proofObligations loadedProgram - case findProofObligationByHash proofObligations proofObligationHash of - Nothing -> onError (Others "Proof obligation not found.") - Just proofObligation -> do - -- insert proof template - let proofTemplate :: Text = makeProofTemplate proofObligation - editText rangeToInsertProof ("\n\n" <> proofTemplate) do - -- reload, send diagnostics and respond hint updates - Reload.handler sourceFilePath onFinish onError - ) onError - where - findProofObligationByHash :: [PO] -> Text -> Maybe PO - findProofObligationByHash proofObligations hash = - List.find (\po -> poAnchorHash po == hash) proofObligations - makeProofTemplate :: PO -> Text - makeProofTemplate proofObligation = - "{- #" <> poAnchorHash proofObligation <> "\n" - <> preExpr <> "\n" - <> "⇒" <> "\n" - <> postExpr <> "\n" - <> Text.pack (replicate len '=') - <> "\n\n-}\n" - where - preExpr = docToText $ pretty $ exprOfPred $ poPre proofObligation - postExpr = docToText $ pretty $ exprOfPred $ poPost proofObligation - len = max (max (Text.length preExpr) (Text.length postExpr) - 2) 5 diff --git a/src/Server/Handler2/CustomMethod/Inspect.hs b/src/Server/Handler2/CustomMethod/Inspect.hs deleted file mode 100644 index 657f06b8..00000000 --- a/src/Server/Handler2/CustomMethod/Inspect.hs +++ /dev/null @@ -1,21 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables #-} -module Server.Handler2.CustomMethod.Inspect (handler) where - -import Data.Loc.Range (Range (..), rangeFile) - -import Server.Handler2.Utils (dumpProgram) -import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram) -import Server.CustomMethod (ResKind) -import Server.Monad (ServerM) -import Error (Error (..)) - -handler :: Range -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handler rangeToInspect onFinish onError = do - let filePath :: FilePath = rangeFile rangeToInspect - maybeLoadedProgram <- dumpProgram filePath - case maybeLoadedProgram of - Nothing -> onError (Others "Please reload before inspect.") - Just loadedProgam -> do - response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgam (Just rangeToInspect) - onFinish response - diff --git a/src/Server/Handler2/CustomMethod/Refine.hs b/src/Server/Handler2/CustomMethod/Refine.hs deleted file mode 100644 index 3e7c8f9a..00000000 --- a/src/Server/Handler2/CustomMethod/Refine.hs +++ /dev/null @@ -1,55 +0,0 @@ -{-# LANGUAGE BlockArguments #-} -{-# LANGUAGE ScopedTypeVariables #-} - -module Server.Handler2.CustomMethod.Refine (slowHandler) where - -import Data.Loc.Range (Range (..), rangeFile) - -import Server.Monad (ServerM) -import Server.Handler2.Utils -import Server.Handler2.CustomMethod.Reload as Reload -import Data.Text (Text) -import Server.CustomMethod (ResKind) -import Error (Error) - -slowHandler :: Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -slowHandler specRange filledText onFinish onError = do - -- remove brackets - editText specRange filledText do - -- reload source - let filePath :: FilePath = rangeFile specRange - Reload.handler filePath onFinish onError - --- 檢查 text typecheck 過了的話 --- 更新 loadedProgram (concrete/ abstract/ pos/ specs ...etc) --- (會比重新load有效率嗎？laziness? --- 用新的loadedProgram更新view - --- handler :: Range -> Text -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () --- handler specRange filledText onFinish onError = do --- let filePath :: FilePath = rangeFile specRange --- maybeLoadedProgram <- dumpProgram filePath --- case maybeLoadedProgram of --- Nothing -> _ --- Just loadedProgram -> do --- let (refinedProgram, newRangeToFocus) = refine loadedProgram specRange filledText --- _ <- cacheProgram filePath refinedProgram --- response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath refinedProgram newRangeToFocus --- onFinish response - --- refine :: LoadedProgram -> Range -> Text -> (LoadedProgram, Maybe Range) --- refine loadedProgram specRange filledText = --- ( LoadedProgram --- { _concreteProgram = _ --- , _highlightingInfos = _ --- , _abstractProgram = _ --- , _scopingInfo = _ --- , _typeCheckingInfo = _ --- , _proofObligations = _ --- , _specifiations = _ --- , _warnings = _ --- , _redexes = _ --- , _variableCounter = _ --- } --- , _ --- ) \ No newline at end of file diff --git a/src/Server/Handler2/CustomMethod/Reload.hs b/src/Server/Handler2/CustomMethod/Reload.hs deleted file mode 100644 index dc55a14f..00000000 --- a/src/Server/Handler2/CustomMethod/Reload.hs +++ /dev/null @@ -1,110 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE BlockArguments #-} -module Server.Handler2.CustomMethod.Reload (handler, reload) where - -import Data.Text (Text) - -import qualified GCL.WP as WP -import qualified Syntax.Concrete as C -import qualified Syntax.Parser as Parser -import qualified Syntax.Abstract as A -import qualified Data.Text as Text -import Error (Error(..)) -import Control.Monad.Except (runExcept) -import Pretty (toText) -import Data.Loc hiding ( fromLoc ) -import qualified GCL.Type as TypeChecking -import qualified Data.List as List -import Data.List (sortOn) - -import Server.CustomMethod (ResKind (..)) -import Server.Monad (ServerM, LoadedProgram (..)) -import Server.Highlighting (collectHighlighting) -import Server.Hover (collectHoverInfo) -import Server.GoToDefn (collectLocationLinks) - -import Server.Handler2.Utils -import Server.Handler2.CustomMethod.Utils (sendDiagnosticsAndMakeResponseFromLoadedProgram) -import Data.Loc.Range (Range, rangeStart) -import Syntax.Typed (TypedProgram) - - -handler :: FilePath -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handler filePath onFinish onError = do - reload filePath (\loadedProgram -> do - response <- sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgram Nothing - onFinish response - ) onError - -reload :: FilePath -> (LoadedProgram -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -reload filepath onFinish onError = do - -- load source - maybeSource <- getSource filepath - case maybeSource of - Nothing -> onError (CannotReadFile filepath) - Just source -> - -- parse source into concrete syntax - case parse filepath source of - Left err -> onError err - Right concrete -> - -- dig holes and convert to abstract syntax - toAbstract filepath concrete (\abstract -> do - -- type check - case typeCheck abstract of - Left err -> onError err - Right typedAst -> - -- calculate proof obligations, specs and other hints - case WP.sweep abstract of - Left err -> onError (StructError err) - Right (pos, specs, warnings, redexes, counter) -> do - -- cache all results - let loadedProgram = LoadedProgram - { _concreteProgram = concrete - , _highlightingInfos = collectHighlighting concrete - , _abstractProgram = abstract - , _scopingInfo = collectLocationLinks abstract - , _typeCheckingInfo = collectHoverInfo typedAst - , _proofObligations = List.sort pos - , _specifiations = sortOn locOf specs - , _warnings = warnings - , _redexes = redexes - , _variableCounter = counter - } - _ <- cacheProgram filepath loadedProgram - onFinish loadedProgram - ) onError - -parse :: FilePath -> Text -> Either Error C.Program -parse filepath source = - case Parser.scanAndParse Parser.program filepath source of - Left err -> Left (ParseError err) - Right program -> Right program - -toAbstract :: FilePath -> C.Program -> (A.Program -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -toAbstract filepath concrete onFinish onError = do - case runExcept $ C.toAbstract concrete of - Left rangeToDigHole -> do - _ <- digHole rangeToDigHole do - maybeSource <- getSource filepath - case maybeSource of - Nothing -> onError (CannotReadFile filepath) - Just source' -> case parse filepath source' of - Left err -> onError err - Right concrete' -> toAbstract filepath concrete' onFinish onError - return () - Right abstract -> onFinish abstract - where - digHole :: Range -> ServerM () -> ServerM () - digHole range _onFinish = do - logText $ " < DigHole " <> toText range - let indent = Text.replicate (posCol (rangeStart range) - 1) " " - let holeText = "[!\n" <> indent <> "\n" <> indent <> "!]" - editText range holeText _onFinish - -typeCheck :: A.Program -> Either Error TypedProgram -typeCheck abstract = do - case TypeChecking.runElaboration abstract of - Left e -> Left (TypeError e) - Right typedProgram -> return typedProgram - diff --git a/src/Server/Handler2/CustomMethod/SubstituteRedex.hs b/src/Server/Handler2/CustomMethod/SubstituteRedex.hs deleted file mode 100644 index e20425ac..00000000 --- a/src/Server/Handler2/CustomMethod/SubstituteRedex.hs +++ /dev/null @@ -1,43 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables #-} - -module Server.Handler2.CustomMethod.SubstituteRedex (handler) where - -import qualified Syntax.Abstract as A -import Error (Error(..)) - -import Server.Monad (ServerM, LoadedProgram(..)) -import Server.CustomMethod (ResKind(..)) -import Server.Handler2.Utils - -import qualified GCL.Substitution as Substitution -import Data.IntMap (IntMap) -import qualified Data.IntMap as IntMap -import Data.Map (Map) -import Data.Text (Text) -import Syntax.Abstract.Types (Expr) -import qualified Syntax.Abstract.Util as A -import Control.Monad.State (runState) -import Render (Render(..)) - -handler :: FilePath -> Int -> ([ResKind] -> ServerM ()) -> (Error -> ServerM ()) -> ServerM () -handler filePath redexNumber onFinish onError = do - maybeLoadedProgram <- dumpProgram filePath - case maybeLoadedProgram of - Nothing -> onError (Others "Please reload before inspect.") - Just loadedProgram -> do - let redexes :: IntMap (Int, A.Expr) = _redexes loadedProgram - let abstract :: A.Program = _abstractProgram loadedProgram - let variableCounter :: Int = _variableCounter loadedProgram - case IntMap.lookup redexNumber redexes of - Nothing -> onError (Others "Redex not found.") - Just (_, redex) -> do - let scope :: Map Text (Maybe Expr) = A.programToScopeForSubstitution abstract - let (newExpr, variableCounter') = - runState (Substitution.step scope redex) variableCounter - let redexesInNewExpr = Substitution.buildRedexMap newExpr - let loadedProgram' = loadedProgram - { _variableCounter = variableCounter' - , _redexes = redexes <> redexesInNewExpr - } - _ <- cacheProgram filePath loadedProgram' - onFinish [ResSubstitute redexNumber (render newExpr)] \ No newline at end of file diff --git a/src/Server/Handler2/CustomMethod/Utils.hs b/src/Server/Handler2/CustomMethod/Utils.hs deleted file mode 100644 index 72bac9c0..00000000 --- a/src/Server/Handler2/CustomMethod/Utils.hs +++ /dev/null @@ -1,86 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Server.Handler2.CustomMethod.Utils where -import Server.Monad (LoadedProgram(..), ServerM) -import qualified Syntax.Abstract as A -import Data.Loc.Range (Range, fromLoc, withinRange) -import Syntax.Abstract (Expr) -import GCL.Predicate (PO (..), Spec (..)) -import GCL.WP.Type (StructWarning) -import Server.CustomMethod (ResKind (..)) -import Data.Text (Text) -import Render (Section (..), Render (..), RenderSection (..), Block (..), Deco (..)) -import Server.Handler.Diagnostic (Collect(..)) -import Server.Handler2.Utils (sendDiagnostics, bumpVersion) -import Data.Maybe (mapMaybe) -import Data.Loc (locOf) -import Pretty (toText) - -sendDiagnosticsAndMakeResponseFromLoadedProgram :: FilePath -> LoadedProgram -> Maybe Range -> ServerM [ResKind] -sendDiagnosticsAndMakeResponseFromLoadedProgram filePath loadedProgram rangeToFocus = do - -- destructure and get needed data - let (LoadedProgram - _ _ (A.Program _ _ globalProperties _ _) - _ _ proofObligations specs warnings _ _ - ) = loadedProgram - - -- send warnings as diagnostics - let diagnostics = concatMap collect warnings - sendDiagnostics filePath diagnostics - - -- send reponse for client to render hints - version' <- bumpVersion - let response = makeResponseFromHints version' rangeToFocus (globalProperties, proofObligations, specs, warnings) - return response - -makeResponseFromHints :: Int -> Maybe Range -> ([Expr], [PO], [Spec], [StructWarning]) -> [ResKind] -makeResponseFromHints version rangeToInspect _hints@(globalProperties, proofObligations, specs, warnings) = - [ ResMarkPOs rangesOfProofObligations - , ResUpdateSpecs (map encodeSpec specs) - , ResDisplay version sections - ] - where - rangesOfProofObligations :: [Range] - rangesOfProofObligations = mapMaybe (fromLoc . locOf) proofObligations - encodeSpec :: Spec -> (Int, Text, Text, Range) - encodeSpec spec = - ( specID spec - , toText $ render (specPreCond spec) - , toText $ render (specPostCond spec) - , specRange spec - ) - sections :: [Section] - sections = mconcat - [ warningsSections - , specsSections - , proofObligationSections - , globalPropertiesSections - ] - where - warningsSections :: [Section] - warningsSections = map renderSection warnings - specsSections :: [Section] - specsSections = map renderSection specsToDisplay - where - specsToDisplay :: [Spec] - specsToDisplay = case rangeToInspect of - Nothing -> specs - Just selectedRange -> filter (withinRange selectedRange) specs - proofObligationSections :: [Section] - proofObligationSections = map renderSection proofObligationsToDisplay - where - proofObligationsToDisplay :: [PO] - proofObligationsToDisplay = case rangeToInspect of - Nothing -> proofObligations - Just selectedRange -> filter (selectedRange `covers`) proofObligations - where - covers :: Range -> PO -> Bool - covers range po = case poAnchorLoc po of - Nothing -> withinRange range po - Just anchor -> withinRange range po || withinRange range anchor - globalPropertiesSections :: [Section] - globalPropertiesSections = map - (\expr -> Section - Plain - [Header "Property" (fromLoc (locOf expr)), Code (render expr)] - ) - globalProperties diff --git a/src/Server/Handler2/GoToDefinition.hs b/src/Server/Handler2/GoToDefinition.hs deleted file mode 100644 index bff75935..00000000 --- a/src/Server/Handler2/GoToDefinition.hs +++ /dev/null @@ -1,35 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} -{-# HLINT ignore "Use forM_" #-} - -module Server.Handler2.GoToDefinition (handler) where - -import qualified Language.LSP.Types as LSP -import Server.Monad (ServerM, LoadedProgram (..)) - - -import qualified Server.SrcLoc as SrcLoc -import qualified Server.IntervalMap as IntervalMap - -import Server.Handler2.Utils - -handler :: LSP.Uri -> LSP.Position -> ([LSP.LocationLink] -> ServerM ()) -> ServerM () -handler uri position responder = do - case LSP.uriToFilePath uri of - Nothing -> return () - Just filePath -> do - logText "<-- Goto Definition" - maybeSource <- getSource filePath - case maybeSource of - Nothing -> responder [] - Just source -> do - let table = SrcLoc.makeToOffset source - let positions' = SrcLoc.fromLSPPosition table filePath position - - maybeLoadedProgram <- dumpProgram filePath - case maybeLoadedProgram of - Nothing -> responder [] - Just loadedProgram -> do - case IntervalMap.lookup positions' (_scopingInfo loadedProgram) of - Nothing -> responder [] - Just locationLink -> responder [locationLink] \ No newline at end of file diff --git a/src/Server/Handler2/Hover.hs b/src/Server/Handler2/Hover.hs deleted file mode 100644 index 393ee5f5..00000000 --- a/src/Server/Handler2/Hover.hs +++ /dev/null @@ -1,41 +0,0 @@ -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE FlexibleInstances #-} - -module Server.Handler2.Hover - ( handler - ) where - -import Data.Loc ( posCoff ) -import Language.LSP.Types hiding ( Range ) -import Pretty ( toText ) -import qualified Server.SrcLoc as SrcLoc -import qualified Server.IntervalMap as IntervalMap - -import Server.Handler2.Utils -import Server.Monad (ServerM, LoadedProgram (..)) - -handler :: Uri -> Position -> (Maybe Hover -> ServerM ()) -> ServerM () -handler uri position responder = case uriToFilePath uri of - Nothing -> responder Nothing - Just filepath -> do - maybeSource <- getSource filepath - case maybeSource of - Nothing -> responder Nothing - Just source -> do - let table = SrcLoc.makeToOffset source - let pos = SrcLoc.fromLSPPosition table filepath position - logText $ " ---> Hover " <> toText (posCoff pos) - - maybeLoadedProgram <- dumpProgram filepath - case maybeLoadedProgram of - Nothing -> responder Nothing - Just loadedProgram -> do - case IntervalMap.lookup pos (_typeCheckingInfo loadedProgram) of - Nothing -> do - -- logText $ toText xs - logText " < Hover (not found)" - responder Nothing - Just (hover, _) -> do - logText $ " < Hover " <> toText hover - responder (Just hover) \ No newline at end of file diff --git a/src/Server/Handler2/SemanticTokens.hs b/src/Server/Handler2/SemanticTokens.hs deleted file mode 100644 index 8caa9f8b..00000000 --- a/src/Server/Handler2/SemanticTokens.hs +++ /dev/null @@ -1,28 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} -module Server.Handler2.SemanticTokens where - -import Server.Monad (ServerM, LoadedProgram (..)) -import qualified Language.LSP.Types as LSP -import Server.Handler2.Utils - -handler :: LSP.Uri -> (Either LSP.ResponseError (Maybe LSP.SemanticTokens) -> ServerM ()) -> ServerM () -handler fileUri responder = do - case LSP.uriToFilePath fileUri of - Nothing -> respondError (LSP.ResponseError LSP.InvalidParams "Invalid uri" Nothing) - Just filePath -> do - logText "\n ---> Syntax Highlighting" - let legend = LSP.SemanticTokensLegend - (LSP.List LSP.knownSemanticTokenTypes) - (LSP.List LSP.knownSemanticTokenModifiers) - maybeLoadedProgram <- dumpProgram filePath - case maybeLoadedProgram of - Nothing -> responder $ pure Nothing - Just loadedProgram -> do - case LSP.makeSemanticTokens legend $ _highlightingInfos loadedProgram of - Left errorMessage -> respondError (LSP.ResponseError LSP.InternalError errorMessage Nothing) - Right semanticTokens -> respondResult semanticTokens - where - respondResult :: LSP.SemanticTokens -> ServerM () - respondResult result = responder (Right $ Just result) - respondError :: LSP.ResponseError -> ServerM () - respondError err = responder (Left err) \ No newline at end of file diff --git a/src/Server/Handler2/Utils.hs b/src/Server/Handler2/Utils.hs deleted file mode 100644 index 3140b75d..00000000 --- a/src/Server/Handler2/Utils.hs +++ /dev/null @@ -1,81 +0,0 @@ -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE DuplicateRecordFields #-} -{-# LANGUAGE OverloadedStrings #-} - -module Server.Handler2.Utils where - -import qualified Language.LSP.VFS as LSP -import Server.Monad (ServerM, LoadedProgram, GlobalEnv (..)) -import qualified Server.Monad -import Data.Text (Text) -import qualified Language.LSP.Types as LSP -import qualified Language.LSP.Server as LSP -import Data.Loc.Range (Range, rangeFile) -import qualified Server.SrcLoc as SrcLoc -import qualified Data.Map as Map -import Control.Monad.Reader.Class (asks) -import Data.IORef (readIORef, modifyIORef') -import Control.Monad.Cont (liftIO) -import Control.Monad.Trans.Class (lift) - --- Basic Instructions for our ServerM programs -- - -getSource :: FilePath -> ServerM (Maybe Text) -getSource filepath = fmap LSP.virtualFileText - <$> LSP.getVirtualFile (LSP.toNormalizedUri (LSP.filePathToUri filepath)) - -logText :: Text -> ServerM () -logText = Server.Monad.logText - -bumpVersion :: ServerM Int -bumpVersion = Server.Monad.bumpVersion - -sendDiagnostics :: FilePath -> [LSP.Diagnostic] -> ServerM () -sendDiagnostics = Server.Monad.sendDiagnosticsLSP - - -editTexts :: FilePath -> [(Range, Text)] -> ServerM () -> ServerM () -editTexts filepath rangeTextPairs onSuccess = do - let requestParams :: LSP.ApplyWorkspaceEditParams - = LSP.ApplyWorkspaceEditParams { - _label = Just "Resolve Spec", - _edit = LSP.WorkspaceEdit { - _changes = Nothing, - _documentChanges = Just (LSP.List [LSP.InL textDocumentEdit]), - _changeAnnotations = Nothing - } - } - _requestId <- LSP.sendRequest LSP.SWorkspaceApplyEdit requestParams (\_ -> onSuccess) - return () - - where - textDocumentEdit :: LSP.TextDocumentEdit - textDocumentEdit = LSP.TextDocumentEdit { - _textDocument = LSP.VersionedTextDocumentIdentifier (LSP.filePathToUri filepath) (Just 0), - _edits = LSP.List (map LSP.InL textEdits) - } - textEdits :: [LSP.TextEdit] - textEdits = map makeTextEdit rangeTextPairs - makeTextEdit :: (Range, Text) -> LSP.TextEdit - makeTextEdit (range, textToReplace) = LSP.TextEdit { - _range = SrcLoc.toLSPRange range, - _newText = textToReplace - } - - -editText :: Range -> Text -> ServerM () -> ServerM () -editText range textToReplace = editTexts (rangeFile range) [(range, textToReplace)] - -cacheProgram :: FilePath -> LoadedProgram -> ServerM LoadedProgram -cacheProgram filepath loadedProgram = do - ref <- lift $ asks loadedPrograms - liftIO $ modifyIORef' ref (Map.insert filepath loadedProgram) - return loadedProgram - -dumpProgram :: FilePath -> ServerM (Maybe LoadedProgram) -dumpProgram filepath = do - ref <- lift $ asks loadedPrograms - mapping <- liftIO $ readIORef ref - case Map.lookup filepath mapping of - Nothing -> return Nothing - Just loadedProgram -> return $ Just loadedProgram \ No newline at end of file diff --git a/src/Server/Hover.hs b/src/Server/Hover.hs index 1bfec1e3..2074c9bf 100644 --- a/src/Server/Hover.hs +++ b/src/Server/Hover.hs @@ -20,7 +20,7 @@ import qualified Server.IntervalMap as IntervalMap import Syntax.Abstract import Syntax.Typed as Typed -collectHoverInfo :: Typed.TypedProgram -> IntervalMap (J.Hover, Type) +collectHoverInfo :: Typed.Program -> IntervalMap (J.Hover, Type) collectHoverInfo = collect instance Pretty J.Hover where @@ -50,31 +50,31 @@ instance Collect a => Collect [a] where -------------------------------------------------------------------------------- -- Program -instance Collect Typed.TypedProgram where +instance Collect Typed.Program where collect (Typed.Program defns decls exprs stmts _) = foldMap collect defns <> foldMap collect decls <> foldMap collect exprs <> foldMap collect stmts -------------------------------------------------------------------------------- -- Definition -instance Collect Typed.TypedDefinition where +instance Collect Typed.Definition where collect (Typed.TypeDefn _ _ ctors _) = foldMap collect ctors collect (Typed.FuncDefnSig arg t prop _) = annotateType arg t <> maybe mempty collect prop collect (Typed.FuncDefn _name expr) = collect expr -instance Collect Typed.TypedTypeDefnCtor where - collect (Typed.TypedTypeDefnCtor _name _tys) = mempty +instance Collect Typed.TypeDefnCtor where + collect (Typed.TypeDefnCtor _name _tys) = mempty -------------------------------------------------------------------------------- -- Declaration -instance Collect Typed.TypedDeclaration where +instance Collect Typed.Declaration where collect (Typed.ConstDecl names ty expr _) = annotateType names ty <> maybe mempty collect expr collect (Typed.VarDecl names ty expr _) = annotateType names ty <> maybe mempty collect expr -------------------------------------------------------------------------------- -- Stmt -instance Collect Typed.TypedStmt where -- TODO: Display hover info for names. +instance Collect Typed.Stmt where -- TODO: Display hover info for names. collect (Typed.Skip _) = mempty collect (Typed.Abort _) = mempty collect (Typed.Assign _names exprs _) = foldMap collect exprs @@ -89,14 +89,14 @@ instance Collect Typed.TypedStmt where -- TODO: Display hover info for names. collect (Typed.HLookup _name expr _) = collect expr collect (Typed.HMutate e1 e2 _) = collect e1 <> collect e2 collect (Typed.Dispose expr _) = collect expr - collect (Typed.Block program _) = collect program + collect (Typed.Block program _) = collect program -instance Collect Typed.TypedGdCmd where - collect (Typed.TypedGdCmd gd stmts _) = collect gd <> foldMap collect stmts +instance Collect Typed.GdCmd where + collect (Typed.GdCmd gd stmts _) = collect gd <> foldMap collect stmts -------------------------------------------------------------------------------- -instance Collect Typed.TypedExpr where +instance Collect Typed.Expr where collect (Typed.Lit _lit ty loc) = annotateType loc ty collect (Typed.Var name ty _) = annotateType name ty collect (Typed.Const name ty _) = annotateType name ty @@ -107,8 +107,9 @@ instance Collect Typed.TypedExpr where collect (Typed.Quant quantifier _bound restriction inner _) = collect quantifier <> collect restriction <> collect inner collect (Typed.ArrIdx expr1 expr2 _) = collect expr1 <> collect expr2 collect (Typed.ArrUpd arr index expr _) = collect arr <> collect index <> collect expr + collect (Typed.Subst e sb) = collect e <> foldMap collect (map snd sb) -instance Collect Typed.TypedChain where +instance Collect Typed.Chain where collect (Typed.Pure expr) = collect expr collect (Typed.More chain op ty expr) = collect chain <> annotateType op ty <> collect expr @@ -149,4 +150,4 @@ instance Collect Type (J.Hover, Type) Interval where instance Collect Type (J.Hover, Type) Endpoint where collect = \case Including x -> collect x - Excluding x -> collect x -} \ No newline at end of file + Excluding x -> collect x -} diff --git a/src/Server/Load.hs b/src/Server/Load.hs new file mode 100644 index 00000000..c8cfcc08 --- /dev/null +++ b/src/Server/Load.hs @@ -0,0 +1,166 @@ +{-# LANGUAGE BlockArguments #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -Wno-name-shadowing #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use join" #-} + +module Server.Load where + + + +import Server.Monad (ServerM, FileState(..), loadFileState, saveFileState, readSource, digHoles, logText, logText) +import Data.Text (Text) + +import Data.Loc.Range (Range) + +import qualified GCL.WP as WP +import qualified Syntax.Concrete as C +import qualified Syntax.Parser as Parser +import qualified Syntax.Abstract as A +import qualified Syntax.Typed as T +import Error (Error(..)) +import Server.Highlighting (collectHighlighting) +import Server.GoToDefn (collectLocationLinks) +import Server.Hover (collectHoverInfo) +import Control.Monad.Except (runExcept) +import Server.PositionMapping (idDelta) +import qualified Server.SrcLoc as SrcLoc +import qualified GCL.Type as TypeChecking +import GCL.WP.Types (StructError, StructWarning) +import GCL.Predicate (PO, Spec) +import Server.Notification.Update (sendUpdateNotification) +import qualified Data.Text as Text +import qualified Data.Aeson as JSON +import Pretty (Pretty(..)) +import Syntax.Concrete.Types (SepBy (..), GdCmd (..)) +import Server.Notification.Error (sendErrorNotification) + +load :: FilePath -> ServerM () +load filePath = do + logText "load: start\n" + maybeFileState <- loadFileState filePath + let currentVersion = case maybeFileState of + Nothing -> 0 + Just FileState{editedVersion} -> editedVersion + + -- read source + maybeSource <- readSource filePath + case maybeSource of + Nothing -> do + logText " read error" + onError (CannotReadFile filePath) + Just source -> do + logText " source read \n" + -- parse source into concrete syntax + case parse filePath source of + Left err -> do + logText " parse error" + onError err + Right concrete -> do + logText " source parsed \n" + case reportHolesOrToAbstract concrete of + Left [] -> do + logText " should not happen\n" + logText . Text.pack $ show concrete + Left holes -> do + logText " should dig holes\n" + digHoles filePath holes do + logText " holes digged\n" + load filePath + Right abstract -> do + logText " all holes digged\n" + logText " abstract program generated\n" + case elaborate abstract of + Left err -> do + logText " elaborate error\n" + onError err + Right elaborated -> do + logText " program elaborated\n" + case WP.sweep elaborated of + Left err -> do + logText " sweep error\n" + onError (StructError err) + Right (pos, specs, warnings, redexes, idCount) -> do + let fileState = FileState + { refinedVersion = currentVersion + , specifications = map (\spec -> (currentVersion, spec)) specs + , proofObligations = map (\po -> (currentVersion, po)) pos + , warnings = warnings + + -- to support other LSP methods in a light-weighted manner + , loadedVersion = currentVersion + , toOffsetMap = SrcLoc.makeToOffset source + , concrete = concrete + , semanticTokens = collectHighlighting concrete + , abstract = abstract + , idCount = idCount + , definitionLinks = collectLocationLinks abstract + , elaborated = elaborated + , hoverInfos = collectHoverInfo elaborated + + , positionDelta = idDelta + , editedVersion = currentVersion + } + logText " fileState created\n" + saveFileState filePath fileState + logText " fileState updated\n" + onSuccess + logText "load: end\n" + where + onSuccess :: ServerM () + onSuccess = do + logText "load: success\n" + sendUpdateNotification filePath + -- clear errors + sendErrorNotification filePath [] + logText "load: update notification sent\n" + onError :: Error -> ServerM () + onError err = do + logText "load: error\n\t" + logText $ Text.pack (show $ JSON.encode err) + logText "\n" + sendErrorNotification filePath [err] + logText "load: update notification sent\n" + +parse :: FilePath -> Text -> Either Error C.Program +parse filepath source = + case Parser.scanAndParse Parser.program filepath source of + Left err -> Left (ParseError err) + Right concrete -> Right concrete + +reportHolesOrToAbstract :: C.Program -> Either [Range] A.Program +reportHolesOrToAbstract concrete = + case collectHoles concrete of + [] -> case runExcept $ C.toAbstract concrete of + Left _ -> error "should dig all holes before calling Concrete.toAbstract" + Right abstract -> Right abstract + holes -> Left holes + +collectHoles :: C.Program -> [Range] +collectHoles (C.Program _ statements) = collectHolesFromStatements statements + +collectHolesFromStatements :: [C.Stmt] -> [Range] +collectHolesFromStatements statements = do + statement <- statements + case statement of + C.SpecQM range -> [range] + C.Block _ program _ -> collectHoles program + C.Do _ commands _ -> collectHolesFromGdCmd commands + C.If _ commands _ -> collectHolesFromGdCmd commands + _ -> [] + +mapSepBy :: (a -> b) -> SepBy s a -> [b] +mapSepBy f (Head c) = [f c] +mapSepBy f (Delim c _ cs) = f c : mapSepBy f cs + +collectHolesFromGdCmd :: SepBy s C.GdCmd -> [Range] +collectHolesFromGdCmd s = do + ranges <- mapSepBy (\(GdCmd _ _ statements) -> collectHolesFromStatements statements) s + ranges + +elaborate :: A.Program -> Either Error T.Program +elaborate abstract = do + case TypeChecking.runElaboration abstract mempty of + Left e -> Left (TypeError e) + Right typedProgram -> return typedProgram diff --git a/src/Server/Monad.hs b/src/Server/Monad.hs index 53afa465..dc04566f 100644 --- a/src/Server/Monad.hs +++ b/src/Server/Monad.hs @@ -1,297 +1,315 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} {-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE LambdaCase #-} - -module Server.Monad - ( ServerM - , GlobalEnv(..) - , initGlobalEnv - , runServerM - , customRequestResponder - , customRequestToNotification - , interpret - , logText - , sendDiagnosticsLSP - , convertErrorsToResponsesAndDiagnostics - , bumpVersion - , LoadedProgram(..) - ) where +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +module Server.Monad where + +import Data.Text +import qualified Data.Map as Map import Control.Concurrent ( Chan , newChan , writeChan ) import Control.Monad.Reader -import Control.Monad.Trans.Free -import qualified Data.Aeson as JSON import Data.IORef ( IORef - , modifyIORef' - , newIORef + , modifyIORef , readIORef - , writeIORef + , newIORef ) import Data.Map ( Map ) -import qualified Data.Map as Map -import qualified Data.Maybe as Maybe -import Data.Text ( Text ) -import Error -import qualified Language.LSP.Diagnostics as J -import qualified Language.LSP.Server as J -import qualified Language.LSP.Types as J -import qualified Language.LSP.VFS as J -import Pretty ( toText ) -import Render -import Server.CustomMethod -import Server.Handler.Diagnostic ( collect ) -import Server.Pipeline ( Instruction(..) - , PipelineM - , PipelineState(..) - , initState - , runPipelineM - ) -import qualified Server.Pipeline as DSL -import qualified Server.SrcLoc as SrcLoc -import GCL.WP.Type (StructWarning) +import qualified Language.LSP.Types as LSP +import qualified Language.LSP.Server as LSP +import qualified Language.LSP.VFS as LSP +import qualified Language.LSP.Diagnostics as LSP +import qualified Data.Aeson as JSON +import GCL.Predicate (Spec (Specification, specID), PO) +import qualified Syntax.Abstract as Abstract +import qualified Syntax.Concrete as Concrete +import qualified Syntax.Typed as Typed import Server.IntervalMap (IntervalMap) -import Syntax.Abstract as A hiding ( Pure ) -import Syntax.Concrete as C hiding ( Pure ) -import GCL.Predicate (PO, Spec) -import Data.IntMap (IntMap) - - --------------------------------------------------------------------------------- - -interpret - :: Show a - => J.Uri - -> (([Error], Maybe a) -> ServerM ()) - -> PipelineM a - -> ServerM () -interpret uri continuation p = case J.uriToFilePath uri of - Nothing -> pure () - Just filepath -> executeOneStep filepath continuation p - -executeOneStep - :: Show a - => FilePath - -> (([Error], Maybe a) -> ServerM ()) - -> PipelineM a - -> ServerM () -executeOneStep filepath continuation p = do - state <- getState filepath - case runPipelineM filepath state p of - Right (result, newState, ()) -> do - -- persist the new state - setState filepath newState - -- see if the computation has completed - case result of - Pure value -> continuation (pipelineErrors newState, Just value) - Free command -> handleCommand filepath continuation command - Left errors -> do -- got errors from computation - - oldState <- getState filepath - logText " [ event ] unmute" - let newState = - oldState { pipelineErrors = errors -- update errors for later inspection - , pipelineMute = False } -- unmute on error! - setState filepath newState - - continuation (errors, Nothing) - -handleCommand - :: Show a - => FilePath - -> (([Error], Maybe a) -> ServerM ()) - -> Instruction (PipelineM a) - -> ServerM () -handleCommand filepath continuation = \case - EditText range text next -> do - -- apply edit - let removeSpec = J.TextEdit (SrcLoc.toLSPRange range) text - - let identifier = - J.VersionedTextDocumentIdentifier (J.filePathToUri filepath) (Just 0) - let textDocumentEdit = - J.TextDocumentEdit identifier (J.List [J.InL removeSpec]) - let change = J.InL textDocumentEdit - let workspaceEdit = - J.WorkspaceEdit Nothing (Just (J.List [change])) Nothing - let applyWorkspaceEditParams = - J.ApplyWorkspaceEditParams (Just "Resolve Spec") workspaceEdit - let callback _ = executeOneStep filepath continuation $ do - DSL.getSource >>= next - - void $ J.sendRequest J.SWorkspaceApplyEdit applyWorkspaceEditParams callback - GetSource next -> do - result <- fmap J.virtualFileText - <$> J.getVirtualFile (J.toNormalizedUri (J.filePathToUri filepath)) - case result of - Nothing -> continuation ([CannotReadFile filepath], Nothing) - Just source -> executeOneStep filepath continuation (next source) - Log text next -> do - logText text - executeOneStep filepath continuation next - SendDiagnostics diagnostics next -> do - -- send diagnostics - sendDiagnosticsLSP filepath diagnostics - executeOneStep filepath continuation next - --------------------------------------------------------------------------------- +import Server.PositionMapping (PositionDelta) +import Data.Loc.Range (Range, rangeStart) +import qualified Server.SrcLoc as SrcLoc +import qualified Data.Text as Text +import Data.Loc (posCol) +import Data.Version (Version(Version)) +import GCL.WP.Types (StructWarning) +import Language.LSP.Types.Lens (HasMessage(message)) -- | State shared by all clients and requests -data GlobalEnv = GlobalEnv - { -- Channel for printing log - globalChan :: Chan Text - , - -- Counter for generating fresh numbers - globalCounter :: IORef Int - , globalCurrentStage :: IORef (Map FilePath PipelineState) - -- NEW: book keeping abstract syntax and hints - , loadedPrograms :: IORef (Map FilePath LoadedProgram) +data GlobalState = GlobalState + { logChannel :: Chan Text -- Channel for printing log + , filesState :: IORef (Map FilePath FileState) } -data LoadedProgram = LoadedProgram - { _concreteProgram :: C.Program - , _highlightingInfos :: [J.SemanticTokenAbsolute] - , _abstractProgram :: A.Program - , _scopingInfo :: IntervalMap J.LocationLink - , _typeCheckingInfo :: IntervalMap (J.Hover, A.Type) - , _proofObligations :: [PO] - , _specifiations :: [Spec] - , _warnings :: [StructWarning] - , _redexes :: IntMap (Int, A.Expr) - , _variableCounter :: Int +type Versioned a = (Int, a) + +data FileState = FileState + -- main states for Reload and Refine + { refinedVersion :: Int -- the version number of the last refine + , specifications :: [Versioned Spec] -- editedVersion or (editedVersion + 1) + , proofObligations :: [Versioned PO] -- editedVersion + , warnings :: [StructWarning] + + -- to support other LSP methods in a light-weighted manner + , loadedVersion :: Int -- the version number of the last reload + , toOffsetMap :: SrcLoc.ToOffset + , concrete :: Concrete.Program + , semanticTokens :: [LSP.SemanticTokenAbsolute] + , abstract :: Abstract.Program + , idCount :: Int + , definitionLinks :: IntervalMap LSP.LocationLink + , hoverInfos :: IntervalMap (LSP.Hover, Abstract.Type) + , elaborated :: Typed.Program + , positionDelta :: PositionDelta -- loadedVersion ~> editedVersion + , editedVersion :: Int -- the version number of the last change } -- | Constructs an initial global state -initGlobalEnv :: IO GlobalEnv +initGlobalEnv :: IO GlobalState initGlobalEnv = - GlobalEnv + GlobalState <$> newChan - -- <*> newIORef Map.empty - <*> newIORef 0 - <*> newIORef Map.empty <*> newIORef Map.empty -------------------------------------------------------------------------------- -type ServerM = J.LspT () (ReaderT GlobalEnv IO) +type ServerM = LSP.LspT () (ReaderT GlobalState IO) -runServerM :: GlobalEnv -> J.LanguageContextEnv () -> ServerM a -> IO a -runServerM env ctxEnv program = runReaderT (J.runLspT ctxEnv program) env +runServerM :: GlobalState -> LSP.LanguageContextEnv () -> ServerM a -> IO a +runServerM globalState ctxEnv program = runReaderT (LSP.runLspT ctxEnv program) globalState -------------------------------------------------------------------------------- --- | Helper functions for side effects +-- | Helper functions for side effects -- display Text logText :: Text -> ServerM () logText s = do - chan <- lift $ asks globalChan + chan <- lift $ asks logChannel liftIO $ writeChan chan s +loadFileState :: FilePath -> ServerM (Maybe FileState) +loadFileState filePath = do + logText "ask file state ref\n" + fileStateRef <- lift $ asks filesState + logText "ask file state map\n" + fileStateMap <- liftIO $ readIORef fileStateRef + logText "lookup file state map\n" + case Map.lookup filePath fileStateMap of + Nothing -> do + logText " not found\n" + return Nothing + Just loadedFileState -> do + logText " found\n" + return $ Just loadedFileState + +saveFileState :: FilePath -> FileState -> ServerM () +saveFileState filePath fileState = do + fileStateRef <- lift $ asks filesState + liftIO $ modifyIORef fileStateRef (Map.insert filePath fileState) + +logFileState :: Show a => FilePath -> (FileState -> a) -> ServerM () +logFileState filePath f = do + logText "====== " + logText . Text.pack $ filePath + logText " ======\n" + logText "\n" + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> logText "not loaded yet\n" + Just fileState -> do + logText "loaded\n" + logText . Text.pack . show $ f fileState + logText "\n" + logText "=======================\n" + +modifyFileState :: FilePath -> (FileState -> FileState) -> ServerM () +modifyFileState filePath modifier = do + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> return () + Just fileState -> do + let fileState' = modifier fileState + saveFileState filePath fileState' + +bumpVersion :: FilePath -> ServerM () +bumpVersion filePath = do + modifyFileState filePath (\fileState@FileState{editedVersion} -> fileState {editedVersion = editedVersion + 1}) + +updateIdCounter :: FilePath -> + Int -> ServerM () +updateIdCounter filePath count = do + modifyFileState filePath (\fileState -> fileState {idCount = count}) + +saveEditedVersion :: FilePath -> Int -> ServerM () +saveEditedVersion filePath version = do + modifyFileState filePath (\fileState -> fileState {editedVersion = version}) + +pushSpecs :: Int -> FilePath -> [Spec] -> ServerM () +pushSpecs version filePath newSpecs = do + let newVersionedSpecs :: [Versioned Spec] = Prelude.map (\spec -> (version, spec)) newSpecs + modifyFileState filePath (\fileState@FileState{specifications} -> + fileState{specifications = specifications ++ newVersionedSpecs}) + +pushPos :: Int -> FilePath -> [PO] -> ServerM () +pushPos version filePath newPos = do + let newVersionedPos :: [Versioned PO] = Prelude.map (\po -> (version, po)) newPos + modifyFileState filePath (\fileState@FileState{proofObligations} -> + fileState{proofObligations = proofObligations ++ newVersionedPos}) + +deleteSpec :: FilePath -> Spec -> ServerM () +deleteSpec filePath Specification{specID = targetSpecId} = do + modifyFileState filePath (\filesState@FileState{specifications} -> + filesState{specifications = Prelude.filter (\(_, Specification{specID}) -> specID /= targetSpecId) specifications}) + +readSource :: FilePath -> ServerM (Maybe Text) +readSource filepath = fmap LSP.virtualFileText + <$> LSP.getVirtualFile (LSP.toNormalizedUri (LSP.filePathToUri filepath)) + +modifyPositionDelta :: FilePath -> (PositionDelta -> PositionDelta) -> ServerM () +modifyPositionDelta filePath modifier = do + modifyFileState filePath (\fileState@FileState{positionDelta} -> fileState{positionDelta = modifier positionDelta}) + + +editTexts :: FilePath -> [(Range, Text)] -> ServerM () -> ServerM () +editTexts filepath rangeTextPairs onSuccess = do + let requestParams :: LSP.ApplyWorkspaceEditParams + = LSP.ApplyWorkspaceEditParams { + _label = Just "Resolve Spec", + _edit = LSP.WorkspaceEdit { + _changes = Nothing, + _documentChanges = Just (LSP.List [LSP.InL textDocumentEdit]), + _changeAnnotations = Nothing + } + } + _requestId <- LSP.sendRequest LSP.SWorkspaceApplyEdit requestParams (\_ -> onSuccess) + return () + + where + textDocumentEdit :: LSP.TextDocumentEdit + textDocumentEdit = LSP.TextDocumentEdit { + _textDocument = LSP.VersionedTextDocumentIdentifier (LSP.filePathToUri filepath) (Just 0), + _edits = LSP.List (Prelude.map LSP.InL textEdits) + } + textEdits :: [LSP.TextEdit] + textEdits = Prelude.map makeTextEdit rangeTextPairs + makeTextEdit :: (Range, Text) -> LSP.TextEdit + makeTextEdit (range, textToReplace) = LSP.TextEdit { + _range = SrcLoc.toLSPRange range, + _newText = textToReplace + } + +sendCustomNotification :: Text -> JSON.Value -> ServerM () +sendCustomNotification methodId json = LSP.sendNotification (LSP.SCustomMethod methodId) json + + -- send diagnostics -- NOTE: existing diagnostics would be erased if `diagnostics` is empty -sendDiagnosticsLSP :: FilePath -> [J.Diagnostic] -> ServerM () -sendDiagnosticsLSP filepath diagnostics = do - version <- bumpVersion - J.publishDiagnostics 100 - (J.toNormalizedUri (J.filePathToUri filepath)) - (Just version) - (J.partitionBySource diagnostics) - -bumpVersion :: ServerM Int -bumpVersion = do - ref <- lift $ asks globalCounter - n <- liftIO $ readIORef ref - liftIO $ writeIORef ref (succ n) - return n - -setState :: FilePath -> PipelineState -> ServerM () -setState filepath state = do - ref <- lift $ asks globalCurrentStage - liftIO $ modifyIORef' ref (Map.insert filepath state) - -getState :: FilePath -> ServerM PipelineState -getState filepath = do - ref <- lift $ asks globalCurrentStage - mapping <- liftIO $ readIORef ref - case Map.lookup filepath mapping of - Nothing -> return $ initState filepath - Just state -> return state +sendDiagnostics :: FilePath -> [LSP.Diagnostic] -> ServerM () +sendDiagnostics filePath diagnostics = do + maybeFileState <- loadFileState filePath + let maybeVersion = fmap editedVersion maybeFileState + LSP.publishDiagnostics 100 + (LSP.toNormalizedUri (LSP.filePathToUri filePath)) + maybeVersion + (LSP.partitionBySource diagnostics) + +digHoles :: FilePath -> [Range] -> ServerM () -> ServerM () +digHoles filePath ranges onFinish = do + -- logText $ " < DigHoles " <> (map ranges toText) + let indent range = Text.replicate (posCol (rangeStart range) - 1) " " + let diggedText range = "[!\n" <> indent range <> "\n" <> indent range <> "!]" + editTexts filePath (Prelude.map (\range -> (range, diggedText range)) ranges) onFinish + +sendDebugMessage :: Text -> ServerM () +sendDebugMessage message = do + let requestParams = + LSP.ShowMessageRequestParams + LSP.MtInfo + message + Nothing + LSP.sendRequest LSP.SWindowShowMessageRequest requestParams (\_ -> return ()) + return () + +-- -------------------------------------------------------------------------------- + +-- convertErrorsToResponsesAndDiagnostics +-- :: [Error] -> ServerM ([ResKind], [J.Diagnostic]) +-- convertErrorsToResponsesAndDiagnostics errors = do + +-- -- convert [Error] to [ResKind] +-- version <- bumpVersion +-- let responses = +-- [ResDisplay version (map renderSection errors), ResUpdateSpecs []] + +-- -- collect Diagnostics from [Error] +-- let diagnostics = errors >>= collect + +-- return (responses, diagnostics) + +-- -- when responding to CustomMethod requests +-- -- ignore `result` when there's `error` +-- customRequestResponder +-- :: FilePath +-- -> (Response -> ServerM ()) +-- -> ([Error], Maybe [ResKind]) +-- -> ServerM () +-- customRequestResponder filepath responder (errors, result) = if null errors +-- then do +-- let responsesFromResult = Maybe.fromMaybe [] result + +-- logText +-- $ " < Notify with " +-- <> toText (length responsesFromResult) +-- <> " custom responses" + +-- sendDiagnosticsLSP filepath [] +-- responder (Res filepath responsesFromResult) +-- else do +-- (responsesFromError, diagnosticsFromError) <- +-- convertErrorsToResponsesAndDiagnostics errors + +-- logText +-- $ " < Notify " +-- <> toText (length errors) +-- <> " errors with " +-- <> toText (length responsesFromError) +-- <> " custom responses and " +-- <> toText (length diagnosticsFromError) +-- <> " diagnostics" + +-- sendDiagnosticsLSP filepath diagnosticsFromError +-- responder (Res filepath responsesFromError) + +-- -- when responding to events like `STextDocumentDidChange` +-- -- combine both `result` AND `error` +-- customRequestToNotification +-- :: J.LSP.Uri -> ([Error], Maybe [ResKind]) -> ServerM () +-- customRequestToNotification uri (errors, result) = case J.uriToFilePath uri of +-- Nothing -> pure () +-- Just filepath -> do +-- (responsesFromError, diagnosticsFromError) <- +-- convertErrorsToResponsesAndDiagnostics errors +-- let responsesFromResult = Maybe.fromMaybe [] result +-- let responses = responsesFromError <> responsesFromResult + +-- logText +-- $ " < Respond with " +-- <> toText (length responses) +-- <> " custom responses and " +-- <> toText (length diagnosticsFromError) +-- <> " diagnostics" + +-- -- send diagnostics +-- sendDiagnosticsLSP filepath diagnosticsFromError +-- -- send responses +-- J.sendNotification (J.SCustomMethod "guabao") $ JSON.toJSON $ Res +-- filepath +-- responses -------------------------------------------------------------------------------- - -convertErrorsToResponsesAndDiagnostics - :: [Error] -> ServerM ([ResKind], [J.Diagnostic]) -convertErrorsToResponsesAndDiagnostics errors = do - - -- convert [Error] to [ResKind] - version <- bumpVersion - let responses = - [ResDisplay version (map renderSection errors), ResUpdateSpecs []] - - -- collect Diagnostics from [Error] - let diagnostics = errors >>= collect - - return (responses, diagnostics) - --- when responding to CustomMethod requests --- ignore `result` when there's `error` -customRequestResponder - :: FilePath - -> (Response -> ServerM ()) - -> ([Error], Maybe [ResKind]) - -> ServerM () -customRequestResponder filepath responder (errors, result) = if null errors - then do - let responsesFromResult = Maybe.fromMaybe [] result - - logText - $ " < Notify with " - <> toText (length responsesFromResult) - <> " custom responses" - - sendDiagnosticsLSP filepath [] - responder (Res filepath responsesFromResult) - else do - (responsesFromError, diagnosticsFromError) <- - convertErrorsToResponsesAndDiagnostics errors - - logText - $ " < Notify " - <> toText (length errors) - <> " errors with " - <> toText (length responsesFromError) - <> " custom responses and " - <> toText (length diagnosticsFromError) - <> " diagnostics" - - sendDiagnosticsLSP filepath diagnosticsFromError - responder (Res filepath responsesFromError) - --- when responding to events like `STextDocumentDidChange` --- combine both `result` AND `error` -customRequestToNotification - :: J.Uri -> ([Error], Maybe [ResKind]) -> ServerM () -customRequestToNotification uri (errors, result) = case J.uriToFilePath uri of - Nothing -> pure () - Just filepath -> do - (responsesFromError, diagnosticsFromError) <- - convertErrorsToResponsesAndDiagnostics errors - let responsesFromResult = Maybe.fromMaybe [] result - let responses = responsesFromError <> responsesFromResult - - logText - $ " < Respond with " - <> toText (length responses) - <> " custom responses and " - <> toText (length diagnosticsFromError) - <> " diagnostics" - - -- send diagnostics - sendDiagnosticsLSP filepath diagnosticsFromError - -- send responses - J.sendNotification (J.SCustomMethod "guabao") $ JSON.toJSON $ Res - filepath - responses diff --git a/src/Server/Notification/Error.hs b/src/Server/Notification/Error.hs new file mode 100644 index 00000000..c1a99379 --- /dev/null +++ b/src/Server/Notification/Error.hs @@ -0,0 +1,141 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE InstanceSigs #-} + +module Server.Notification.Error where + +import qualified Data.Aeson as JSON +import Data.Aeson ((.=), object) +import qualified Server.Monad as Server +import Pretty.Predicate ( ) +import Data.Loc (Loc(..), Pos (..)) +import Data.Text.Prettyprint.Doc +import qualified Data.Text as Text +import Pretty.Typed () +import Data.List.NonEmpty (NonEmpty ((:|))) +import Syntax.Parser.Error (ParseError(..)) +import GCL.Type (TypeError(..)) +import Error (Error (..)) +import Server.Monad (ServerM) +import GCL.WP.Types (StructError (..)) + + +sendErrorNotification :: FilePath -> [Error] -> ServerM () +sendErrorNotification filePath errors = do + let json :: JSON.Value = makeErrorNotificationJson filePath errors + Server.sendCustomNotification "guabao/error" json + +makeErrorNotificationJson :: FilePath -> [Error] -> JSON.Value +makeErrorNotificationJson filePath errors = JSON.object + [ "filePath" .= JSON.toJSON filePath + , "errors" .= JSON.toJSON errors + ] + +instance JSON.ToJSON Error where + toJSON :: Error -> JSON.Value + toJSON (CannotReadFile filePath) = object + [ "tag" .= JSON.String "CannotReadFile" + , "filePath" .= JSON.toJSON filePath + ] + toJSON (ParseError err) = object + [ "tag" .= JSON.String "ParseError" + , "message" .= JSON.toJSON err + ] + toJSON (TypeError err) = object + [ "tag" .= JSON.String "TypeError" + , "message" .= JSON.toJSON err + ] + toJSON (StructError err) = object + [ "tag" .= JSON.String "StructError" + , "message" .= JSON.toJSON err + ] + toJSON (Others message) = object + [ "tag" .= JSON.String "Others" + , "message" .= JSON.toJSON message + ] + +toLspPositionJSON :: Pos -> JSON.Value +toLspPositionJSON (Pos filepath line column offset) = object + [ "line" .= JSON.toJSON (line - 1) + , "character" .= JSON.toJSON (column - 1) + ] + + +instance JSON.ToJSON ParseError where + toJSON :: ParseError -> JSON.Value + toJSON (LexicalError position) = object + [ "tag" .= JSON.String "LexicalError" + , "position" .= toLspPositionJSON position + ] + toJSON (SyntacticError locatedSymbols message) = object + [ "tag" .= JSON.String "SyntacticError" + , "locatedSymbols" .= JSON.toJSON (locatedSymbolsToJSON locatedSymbols) + , "message" .= JSON.toJSON message + ] + where + locatedSymbolsToJSON :: NonEmpty (Loc, String) -> JSON.Value + locatedSymbolsToJSON (x :| xs) = JSON.toJSON $ map (\(loc, s) -> object [ + "location" .= JSON.toJSON loc + , "symbol" .= JSON.toJSON s + ]) (x:xs) + +instance JSON.ToJSON TypeError where + toJSON :: TypeError -> JSON.Value + toJSON (NotInScope symbol) = object + [ "tag" .= JSON.String "NotInScope" + , "symbol" .= JSON.toJSON symbol + ] + toJSON (UnifyFailed type1 type2 loc) = object + [ "tag" .= JSON.String "UnifyFailed" + , "location" .= JSON.toJSON loc + , "typeExpressions" .= JSON.toJSON (map (show . pretty) [type1, type2]) + ] + toJSON (RecursiveType n t loc) = object + [ "tag" .= JSON.String "RecursiveType" + , "typeVariable" .= JSON.toJSON n + , "typeExpression" .= t + , "location" .= JSON.toJSON loc + ] + toJSON (AssignToConst name) = object + [ "tag" .= JSON.String "AssignToConst" + , "constSymbol" .= JSON.toJSON name + ] + toJSON (UndefinedType name) = object + [ "tag" .= JSON.String "UndefinedType" + , "typeVariable" .= JSON.toJSON name + ] + toJSON (DuplicatedIdentifiers names) = object + [ "tag" .= JSON.String "DuplicatedIdentifiers" + , "identifiers" .= JSON.toJSON (map JSON.toJSON names) + ] + toJSON (RedundantNames names) = object + [ "tag" .= JSON.String "RedundantNames" + , "names" .= JSON.toJSON (map JSON.toJSON names) + ] + toJSON (RedundantExprs expressions) = object + [ "tag" .= JSON.String "RedundantExprs" + , "expressions" .= JSON.toJSON (map (JSON.String . Text.pack . show . pretty) expressions) + ] + toJSON (MissingArguments names) = object + [ "tag" .= JSON.String "MissingArguments" + , "argumentNames" .= JSON.toJSON (map JSON.toJSON names) + ] + +instance JSON.ToJSON StructError where + toJSON :: StructError -> JSON.Value + toJSON (MissingAssertion loc) = object + [ "tag" .= JSON.String "MissingAssertion" + , "location" .= JSON.toJSON loc + ] + toJSON (MissingPostcondition loc) = object + [ "tag" .= JSON.String "MissingPostcondition" + , "location" .= JSON.toJSON loc + ] + toJSON (MultiDimArrayAsgnNotImp loc) = object + [ "tag" .= JSON.String "MultiDimArrayAsgnNotImp" + , "location" .= JSON.toJSON loc + ] + toJSON (LocalVarExceedScope loc) = object + [ "tag" .= JSON.String "LocalVarExceedScope" + , "location" .= JSON.toJSON loc + ] \ No newline at end of file diff --git a/src/Server/Notification/Update.hs b/src/Server/Notification/Update.hs new file mode 100644 index 00000000..fbfde591 --- /dev/null +++ b/src/Server/Notification/Update.hs @@ -0,0 +1,109 @@ +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE InstanceSigs #-} + +module Server.Notification.Update where + +import qualified Data.Aeson as JSON +import Data.Aeson ((.=), object) +import qualified Server.Monad as Server +import Server.Monad (FileState(..), ServerM, loadFileState) +import GCL.Predicate (Spec(..), PO(..), Origin(..)) +import GCL.WP.Types (StructWarning(..)) +import Server.SrcLoc (toLSPRange) +import Pretty.Predicate ( ) +import Data.Text.Prettyprint.Doc +import Pretty.Typed () + + +sendUpdateNotification :: FilePath -> ServerM () +sendUpdateNotification filePath = do + maybeFileState <- loadFileState filePath + case maybeFileState of + Nothing -> return () + Just fileState -> do + let json :: JSON.Value = makeUpdateNotificationJson filePath fileState + Server.sendCustomNotification "guabao/update" json + + +makeUpdateNotificationJson :: FilePath -> FileState -> JSON.Value +makeUpdateNotificationJson filePath FileState{specifications, proofObligations, warnings} = JSON.object + [ "filePath" .= JSON.toJSON filePath + , "specs" .= JSON.toJSON (map snd specifications) + , "pos" .= JSON.toJSON (map snd proofObligations) + , "warnings" .= JSON.toJSON warnings + ] + +instance JSON.ToJSON Spec where + toJSON :: Spec -> JSON.Value + toJSON Specification{..} = + object [ "id" .= JSON.toJSON (show specID) + , "preCondition" .= JSON.toJSON (show $ pretty specPreCond) + , "postCondition" .= JSON.toJSON (show $ pretty specPostCond) + , "specRange" .= JSON.toJSON (toLSPRange specRange) + ] + +instance JSON.ToJSON StructWarning where + toJSON :: StructWarning -> JSON.Value + toJSON (MissingBound range) = + object [ "tag" .= JSON.String "MissingBound" + , "range" .= JSON.toJSON (toLSPRange range) + ] + toJSON (ExcessBound range) = + object [ "tag" .= JSON.String "ExcessBound" + , "range" .= JSON.toJSON (toLSPRange range) + ] + +instance JSON.ToJSON PO where + toJSON :: PO -> JSON.Value + toJSON PO{..} = object + [ "assumption" .= JSON.toJSON (show $ pretty poPre) + , "goal" .= JSON.toJSON (show $ pretty poPost) + , "hash" .= JSON.toJSON poAnchorHash + , "proofLocation" .= case poAnchorLoc of + Nothing -> JSON.Null + Just range -> JSON.toJSON (toLSPRange range) + , "origin" .= JSON.toJSON poOrigin + ] + +-- tag: "Abort" | "Skip" | "Spec" | "Assignment" | "Conditional" | "Loop invariant" | "Loop termination"; +instance JSON.ToJSON Origin where + toJSON :: Origin -> JSON.Value + toJSON (AtAbort loc) = object + [ "tag" .= JSON.String "Abort" + , "location" .= JSON.toJSON loc + ] + toJSON (AtSkip loc) = object + [ "tag" .= JSON.String "Skip" + , "location" .= JSON.toJSON loc + ] + toJSON (AtSpec loc) = object + [ "tag" .= JSON.String "Spec" + , "location" .= JSON.toJSON loc + ] + toJSON (AtAssignment loc) = object + [ "tag" .= JSON.String "Assignment" + , "location" .= JSON.toJSON loc + ] + toJSON (AtAssertion loc) = object + [ "tag" .= JSON.String "Assertion" + , "location" .= JSON.toJSON loc + ] + toJSON (AtIf loc) = object + [ "tag" .= JSON.String "Conditional" + , "location" .= JSON.toJSON loc + ] + toJSON (AtLoop loc) = object + [ "tag" .= JSON.String "Loop invariant" + , "location" .= JSON.toJSON loc + ] + toJSON (AtTermination loc) = object + [ "tag" .= JSON.String "Loop termination" + , "location" .= JSON.toJSON loc + ] + toJSON Explain{originHeader, originLoc} = object + [ "tag" .= JSON.String originHeader + , "location" .= JSON.toJSON originLoc + ] diff --git a/src/Server/Pipeline.hs b/src/Server/Pipeline.hs deleted file mode 100644 index 8aa7bfe0..00000000 --- a/src/Server/Pipeline.hs +++ /dev/null @@ -1,562 +0,0 @@ -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} - -module Server.Pipeline where - -import Control.Monad.Cont -import Control.Monad.Except -import Control.Monad.RWS hiding ( state ) -import Control.Monad.Trans.Free -import Data.IntMap ( IntMap ) -import Data.List ( find - , sortOn - ) -import qualified Data.List as List -import Data.Loc hiding ( fromLoc ) -import Data.Loc.Range -import Data.Maybe ( mapMaybe ) -import Data.Text ( Text ) -import qualified Data.Text as Text -import Error -import GCL.Predicate -import GCL.Predicate.Util ( specPayloadWithoutIndentation - --, toExpr - ) -import qualified GCL.Type as TypeChecking -import qualified GCL.WP as WP -import GCL.WP.Type ( StructWarning ) -import qualified Language.LSP.Types as J -import Prelude hiding ( span ) -import Pretty ( Pretty(pretty) - , toText - , vsep - ) -import Render -import Server.CustomMethod -import Server.GoToDefn ( collectLocationLinks ) -import Server.Handler.Diagnostic ( Collect(collect) ) -import Server.Highlighting ( collectHighlighting ) -import Server.Hover ( collectHoverInfo ) -import Server.IntervalMap ( IntervalMap ) -import qualified Syntax.Abstract as A -import Syntax.Abstract ( Type ) -import Syntax.Concrete ( ToAbstract(toAbstract) ) -import qualified Syntax.Concrete as C - -----added for eliminateRedexes -import qualified Data.IntMap as IntMap -import qualified GCL.Substitution as Substitution -import Syntax.Abstract.Util ( programToScopeForSubstitution - ) -import Control.Monad.State ( runState ) -import qualified Syntax.Parser as Parser -import Syntax.Parser ( Parser ) - --------------------------------------------------------------------------------- --- | Stages of the processing pipeline --- --- ┌───────────────────┐ --- │ Raw │ : Text --- └───────────────────┘ --- │ --- parse error ◀────────┤ parse --- │ --- ▼ --- ┌───────────────────┐ --- ┌─────────▶│ Parsed │ : Concrete Syntax --- │ └───────────────────┘ Highlighting info --- │ --- request to dig hole ◀────────┤ toAbstract --- │ --- ▼ --- ┌───────────────────┐ --- │ Converted │ : Abstract Syntax --- └───────────────────┘ Scoping info --- │ --- type error ◀────────┤ typeCheck --- │ --- ▼ --- ┌───────────────────┐ --- │ TypeChecked │ : Abstract Syntax --- └───────────────────┘ Typing info --- │ --- sweep error ◀────────┤ "sweep" --- │ --- ▼ --- ┌───────────────────┐ --- │ Swept │ : POs & whatnots --- └───────────────────┘ --- -data Stage = Raw FilePath - | Parsed ParseResult - | Converted ConvertResult - | TypeChecked TypeCheckResult - | Swept SweepResult - deriving (Show, Eq) - -instance Pretty Stage where - pretty stage = case stage of - Raw filepath -> "Raw " <> pretty filepath - Parsed _result -> "Parsed" - Converted _result -> "Converted" - TypeChecked _result -> "TypeChecked" - Swept result -> pretty result - -instance Pretty SweepResult where - pretty result = - "Sweep Result { " - <> vsep - [ "POs: " <> pretty (sweptPOs result) - , "Specs: " <> pretty (sweptSpecs result) - , "Props: " <> pretty (sweptProps result) - , "Warnings: " <> pretty (sweptWarnings result) - ] - <> " }" - - --------------------------------------------------------------------------------- - -data ParseResult = ParseResult - { parsedProgram :: C.Program -- Concrete syntax of parsed program - , parsedHighlighings :: [J.SemanticTokenAbsolute] -- Highlighting infos - } - deriving (Show, Eq) - --- | Converts raw Text to concrete syntax and Highlighting info --- persists the result -parse :: Text -> PipelineM ParseResult -parse source = do - program <- parseWithParser Parser.program source - let parsed = ParseResult { parsedProgram = program - , parsedHighlighings = collectHighlighting program - } - save (Parsed parsed) - return parsed - --------------------------------------------------------------------------------- - -data ConvertResult = ConvertResult - { convertedPreviousStage :: ParseResult - , convertedProgram :: A.Program -- abstract syntax - , convertedIntervalMap :: IntervalMap J.LocationLink -- scoping info - } - deriving (Show, Eq) - --- | Converts concrete syntax to abstract syntax and scoping info --- persists the result -convert :: ParseResult -> PipelineM ConvertResult -convert result = do - converted <- case runExcept (toAbstract (parsedProgram result)) of - Left (Range start end) -> -- should dig hole! - digHole (Range start end) >>= parse >>= convert - Right program -> return $ ConvertResult - { convertedPreviousStage = result - , convertedProgram = program - , convertedIntervalMap = collectLocationLinks program - } - save (Converted converted) -- save the current progress - return converted - --------------------------------------------------------------------------------- - -data TypeCheckResult = TypeCheckResult - { typeCheckedPreviousStage :: ConvertResult - , typeCheckedIntervalMap :: IntervalMap (J.Hover, Type) -- type checking info - } - deriving (Show, Eq) - --- | Converts concrete syntax to abstract syntax and scoping info --- persists the result -typeCheck :: ConvertResult -> PipelineM TypeCheckResult -typeCheck result = do - let program = convertedProgram result - undefined {- -- (This function is no longer needed) - (_, scopeTree) <- case TypeChecking.runTypeCheck program of - Left e -> throwError [TypeError e] - Right v -> return v - - let typeChecked = TypeCheckResult - { typeCheckedPreviousStage = result - , typeCheckedIntervalMap = collectHoverInfo program scopeTree - } - save (TypeChecked typeChecked) -- save the current progress - return typeChecked --} --------------------------------------------------------------------------------- - -data SweepResult = SweepResult - { sweptPreviousStage :: TypeCheckResult - , sweptPOs :: [PO] - -- Specs (holes) - , sweptSpecs :: [Spec] - -- Global properties - , sweptProps :: [A.Expr] - -- Warnings - , sweptWarnings :: [StructWarning] - -- Redexes waiting to be reduce by the client on demand - , sweptRedexes :: IntMap (Int, A.Expr) - -- counter for generating fresh variables - , sweptCounter :: Int - } - deriving (Show, Eq) - --- | Converts abstract syntax to POs and other stuff --- persists the result -sweep :: TypeCheckResult -> PipelineM SweepResult -sweep result = do - let abstract@(A.Program _ _ globalProps _ _) = - convertedProgram (typeCheckedPreviousStage result) - swept <- case WP.sweep abstract of - Left e -> throwError [StructError e] - Right (pos, specs, warings, redexes, counter) -> return $ SweepResult - { sweptPreviousStage = result - , sweptPOs = List.sort pos - , sweptSpecs = sortOn locOf specs - , sweptProps = globalProps - , sweptWarnings = warings - , sweptRedexes = redexes - , sweptCounter = counter - } - save (Swept swept) -- save the current progress - return swept - --------------------------------------------------------------------------------- --- | Monad for handling the pipeline --- --- Side effects: --- Reader: FilePath --- State: PipelineState --- Exception: [Error] --- --- Also, PipelineM is also a free monad of Instruction --- which allows us to "compile" a PipelineM program into a series of Instructions --- We can then decide to run these compiled Instructions in the real world --- or simulate them for testing - -type PipelineM - = FreeT Instruction (RWST FilePath () PipelineState (Except [Error])) - --- PipelineM a --- ~> a | Instruction (PipelineM a) --- ~> a | Instruction (a | Instruction (PipelineM a)) --- ~~ a | Instruction a | (Instruction (Instruction a)) | ... - -runPipelineM - :: FilePath - -> PipelineState - -> PipelineM a - -> Either - [Error] - (FreeF Instruction a (PipelineM a), PipelineState, ()) -runPipelineM filepath st p = runExcept (runRWST (runFreeT p) filepath st) - --------------------------------------------------------------------------------- --- | The State - -data PipelineState = PipelineState - { pipelineErrors :: [Error] - , pipelineStage :: Stage - , pipelineMute :: Bool -- state for indicating whether we should ignore events like `STextDocumentDidChange` - , pipelineMouseSelection :: Maybe Range -- text selections (including cursor position) - , pipelineCounter :: Int -- counter for generating different IDs for Responses - } - deriving (Show, Eq) - --------------------------------------------------------------------------------- --- The "assembly code" for making LSP responses - -data Instruction next - = EditText - Range -- ^ Range to replace - Text -- ^ Text to replace with - (Text -> next) -- ^ Continuation with the text of the whole file after the edit - | GetSource (Text -> next) -- ^ Read the content of a file from the LSP filesystem - | Log Text next -- ^ Make some noise - | SendDiagnostics [J.Diagnostic] next -- ^ Send Diagnostics - deriving (Functor) - - -initState :: FilePath -> PipelineState -initState filepath = PipelineState [] (Raw filepath) False Nothing 0 - --------------------------------------------------------------------------------- --- PipelineM functions - -editText :: Range -> Text -> PipelineM Text -editText range inserted = do - - let Range start end = range - source <- getSource - let (_, rest) = Text.splitAt (posCoff start) source - let (replaced, _) = Text.splitAt (posCoff end - posCoff start) rest - - - case (Text.null replaced, Text.null inserted) of - -- no-op - (True, True) -> return () - -- deletion - (True, False) -> - logText - $ " [ edit ] Delete " - <> toText range - <> " \"" - <> replaced - <> "\"" - -- insertion - (False, True) -> - logText - $ " [ edit ] Insert " - <> toText range - <> " \"" - <> inserted - <> "\"" - -- replacement - (False, False) -> - logText - $ " [ edit ] Replace " - <> toText range - <> " \"" - <> replaced - <> "\" \n with \"" - <> inserted - <> "\"" - - liftF (EditText range inserted id) - -getFilePath :: PipelineM FilePath -getFilePath = ask - -getSource :: PipelineM Text -getSource = liftF (GetSource id) - -load :: PipelineM Stage -load = do - stage <- gets pipelineStage - case stage of - Raw _ -> logText " [ load ] from Raw" - Parsed _ -> logText " [ load ] from Parsed" - Converted _ -> logText " [ load ] from Converted" - TypeChecked _ -> logText " [ load ] from TypeChecked" - Swept _ -> logText " [ load ] from Swept" - return stage - -getErrors :: PipelineM [Error] -getErrors = gets pipelineErrors - -isMuted :: PipelineM Bool -isMuted = gets pipelineMute - -mute :: Bool -> PipelineM () -mute m = do - if m then logText " [ event ] mute" else logText " [ event ] unmute" - modify' $ \state -> state { pipelineMute = m } - -setErrors :: [Error] -> PipelineM () -setErrors e = modify' $ \state -> state { pipelineErrors = e } - --- | Save current progress and remove existing Errors -save :: Stage -> PipelineM () -save stage = do - case stage of - Raw _ -> logText " [ save ] Raw" - Parsed _ -> logText " [ save ] Parsed" - Converted _ -> logText " [ save ] Converted" - TypeChecked _ -> logText " [ save ] TypeChecked" - Swept _ -> logText " [ save ] Swept" - modify' $ \state -> state { pipelineErrors = [], pipelineStage = stage } - -setLastSelection :: Range -> PipelineM () -setLastSelection selection = do - logText $ " [ save ] Mouse selection: " <> toText (ShortRange selection) - modify' $ \state -> state { pipelineMouseSelection = Just selection } - -getLastSelection :: PipelineM (Maybe Range) -getLastSelection = do - sel <- gets pipelineMouseSelection - case sel of - Nothing -> logText " [ load ] Mouse selection: Nothing" - Just r -> - logText $ " [ load ] Mouse selection: " <> toText (ShortRange r) - - return sel - -logText :: Text -> PipelineM () -logText text = liftF (Log text ()) - - -bumpVersion :: PipelineM Int -bumpVersion = do - i <- gets pipelineCounter - -- logText $ " - Bump counter " <> toText i <> " => " <> toText (succ i) - modify' $ \state -> state { pipelineCounter = succ i } - return i - -sendDiagnostics :: [J.Diagnostic] -> PipelineM () -sendDiagnostics xs = do - logText $ " < Send Diagnostics " <> toText (length xs) - liftF (SendDiagnostics xs ()) - ------------------------------------------------------------------------------- - --- converts the "?" at a given location to "[! !]" --- and returns the modified source and the difference of source length -digHole :: Range -> PipelineM Text -digHole range = do - logText $ " < DigHole " <> toText range - let indent = Text.replicate (posCol (rangeStart range) - 1) " " - let holeText = "[!\n" <> indent <> "\n" <> indent <> "!]" - editText range holeText - --- | Try to parse a piece of text in a Spec -refine :: Text -> Range -> PipelineM (Spec, [Text]) -refine source range = do - result <- findPointedSpec - case result of - Nothing -> - throwError [Others "Please place the cursor in side a Spec to refine it"] - Just spec -> do - source' <- getSource - - let payload = Text.unlines $ specPayloadWithoutIndentation source' spec - -- HACK, `pStmts` will kaput if we feed empty strings into it - let payloadIsEmpty = Text.null (Text.strip payload) - if payloadIsEmpty - then return () - else void $ parseWithParser Parser.statements1 payload - return (spec, specPayloadWithoutIndentation source' spec) - where - findPointedSpec :: PipelineM (Maybe Spec) - findPointedSpec = do - parsed <- parse source - converted <- convert parsed - typeChecked <- typeCheck converted - swept <- sweep typeChecked - let specs = sweptSpecs swept - return $ find (withinRange range) specs - --------------------------------------------------------------------------------- - -parseWithParser :: Parser a -> Text -> PipelineM a -parseWithParser parser source = do - filepath <- getFilePath - case Parser.scanAndParse parser filepath source of - Left err -> throwError [ParseError err] - Right val -> return val - -parseProgram :: Text -> PipelineM (C.Program, A.Program) -parseProgram source = do - concrete <- parseWithParser Parser.program source - case runExcept (toAbstract concrete) of - Left (Range start end) -> digHole (Range start end) >>= parseProgram - Right abstract -> return (concrete, abstract) - --------------------------------------------------------------------------------- - -generateResponseAndDiagnostics :: SweepResult -> PipelineM [ResKind] -generateResponseAndDiagnostics result = do - let (SweepResult _ pos specs globalProps warnings _redexes _) = result - - -- get Specs around the mouse selection - lastSelection <- getLastSelection - let overlappedSpecs = case lastSelection of - Nothing -> specs - Just selection -> filter (withinRange selection) specs - -- get POs around the mouse selection (including their corresponding Proofs) - - let withinPOrange sel po = case poAnchorLoc po of - Nothing -> withinRange sel po - Just anchor -> withinRange sel po || withinRange sel anchor - - let overlappedPOs = case lastSelection of - Nothing -> pos - Just selection -> filter (withinPOrange selection) pos - -- render stuff - let warningsSections = - if null warnings then [] else map renderSection warnings - let globalPropsSections = if null globalProps - then [] - else map - (\expr -> Section - Plain - [Header "Property" (fromLoc (locOf expr)), Code (render expr)] - ) - globalProps - let specsSections = - if null overlappedSpecs then [] else map renderSection overlappedSpecs - let poSections = - if null overlappedPOs then [] else map renderSection overlappedPOs - let sections = mconcat - [warningsSections, specsSections, poSections, globalPropsSections] - - version <- bumpVersion - let encodeSpec spec = - ( specID spec - , toText $ render (specPreCond spec) - , toText $ render (specPostCond spec) - , specRange spec - ) - - let rangesOfPOs = mapMaybe (fromLoc . locOf) pos - let responses = - [ ResDisplay version sections - , ResUpdateSpecs (map encodeSpec specs) - , ResMarkPOs rangesOfPOs - ] - let diagnostics = concatMap collect warnings - sendDiagnostics diagnostics - - return responses - - ----------------- - -reduceRedex :: Int -> PipelineM A.Expr -reduceRedex i = do - stage <- load - logText $ Text.pack $ "Substituting Redex " <> show i - -- - case stage of - Swept result -> do - let program = convertedProgram - (typeCheckedPreviousStage (sweptPreviousStage result)) - case IntMap.lookup i (sweptRedexes result) of - Nothing -> throwError [Others $ "Cannot find the redex with index: "<>show i] - Just (_, redex) -> do - let scope = programToScopeForSubstitution program - let (newExpr, counter) = - runState (Substitution.step scope redex) (sweptCounter result) - let redexesInNewExpr = Substitution.buildRedexMap newExpr - let newResult = result - { sweptCounter = counter - , sweptRedexes = sweptRedexes result <> redexesInNewExpr - } - save (Swept newResult) - return newExpr - - _ -> throwError [Others "Invoked reduceRedex in a wrong stage."] - -- TODO: extend applicable stages - --- | The returned Expr should contain no redex(any RedexShell or RedexKernel). --- But this requirement isn't satisfied yet (see TODO in function definition). -eliminateRedexes :: Int -> A.Expr -> PipelineM A.Expr -eliminateRedexes steps expr - | steps <= 0 = return expr - | otherwise = case expr of - A.RedexShell n _ -> reduceRedex n >>= eliminateRedexes (steps-1) - A.App ex1 ex2 l -> do - -- this case might not be this simple? - ex1' <- eliminateRedexes steps ex1 - ex2' <- eliminateRedexes steps ex2 - return (A.App ex1' ex2' l) - A.Lam n ex l -> do - ex' <- eliminateRedexes steps ex - return $ A.Lam n ex' l - -- TODO: complete cases below: - -- A.Func na ne loc -> _ - -- A.Tuple exs -> _ - -- A.Quant ex nas ex' ex3 loc -> _ - -- A.ArrIdx ex ex' loc -> _ - -- A.ArrUpd ex ex' ex3 loc -> _ - -- A.Case ex ccs loc -> _ - _ -> return expr diff --git a/src/Server/PositionMapping.hs b/src/Server/PositionMapping.hs new file mode 100644 index 00000000..06c6994e --- /dev/null +++ b/src/Server/PositionMapping.hs @@ -0,0 +1,249 @@ +-- Copyright (c) 2019 The DAML Authors. All rights reserved. +-- SPDX-License-Identifier: Apache-2.0 +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE OverloadedStrings #-} + + +module Server.PositionMapping + ( PositionMapping(..) + , PositionResult(..) + , lowerRange + , upperRange + , positionResultToMaybe + , fromCurrentPosition + , toCurrentPosition + , PositionDelta(..) + , addOldDelta + , idDelta + , composeDelta + , mkDelta + , toCurrentRange + , fromCurrentRange + , applyChange + , zeroMapping + , deltaFromDiff + -- toCurrent and fromCurrent are mainly exposed for testing + , toCurrent + , fromCurrent + , toCurrentRange' + , fromCurrentRange' + ) where + +import Control.DeepSeq + +import Control.Monad +import Data.Algorithm.Diff +import Data.Bifunctor +import Data.List +import qualified Data.Text as T +import qualified Data.Vector.Unboxed as V + +import Language.LSP.Types (Position (Position), + Range (Range), + TextDocumentContentChangeEvent (TextDocumentContentChangeEvent) + ) + +-- | Either an exact position, or the range of text that was substituted +data PositionResult a + = PositionRange -- ^ Fields need to be non-strict otherwise bind is exponential + { unsafeLowerRange :: a + , unsafeUpperRange :: a } + | PositionExact !a + deriving (Eq,Ord,Show,Functor) + +lowerRange :: PositionResult a -> a +lowerRange (PositionExact a) = a +lowerRange (PositionRange lower _) = lower + +upperRange :: PositionResult a -> a +upperRange (PositionExact a) = a +upperRange (PositionRange _ upper) = upper + +positionResultToMaybe :: PositionResult a -> Maybe a +positionResultToMaybe (PositionExact a) = Just a +positionResultToMaybe _ = Nothing + +instance Applicative PositionResult where + pure = PositionExact + (PositionExact f) <*> a = fmap f a + (PositionRange f g) <*> (PositionExact a) = PositionRange (f a) (g a) + (PositionRange f g) <*> (PositionRange lower upper) = PositionRange (f lower) (g upper) + +instance Monad PositionResult where + (PositionExact a) >>= f = f a + (PositionRange lower upper) >>= f = PositionRange lower' upper' + where + lower' = lowerRange $ f lower + upper' = upperRange $ f upper + +-- The position delta is the difference between two versions +data PositionDelta = PositionDelta + { toDelta :: !(Position -> PositionResult Position) + , fromDelta :: !(Position -> PositionResult Position) + } + +instance Show PositionDelta where + show PositionDelta{} = "PositionDelta{..}" + +instance NFData PositionDelta where + rnf (PositionDelta a b) = a `seq` b `seq` () + +fromCurrentPosition :: PositionMapping -> Position -> Maybe Position +fromCurrentPosition (PositionMapping pm) = positionResultToMaybe . fromDelta pm + +toCurrentPosition :: PositionMapping -> Position -> Maybe Position +toCurrentPosition (PositionMapping pm) = positionResultToMaybe . toDelta pm + +-- A position mapping is the difference from the current version to +-- a specific version +newtype PositionMapping = PositionMapping PositionDelta + +toCurrentRange :: PositionMapping -> Range -> Maybe Range +toCurrentRange mapping (Range a b) = + Range <$> toCurrentPosition mapping a <*> toCurrentPosition mapping b + + +toCurrentRange' :: PositionDelta -> Range -> Maybe Range +toCurrentRange' = toCurrentRange . PositionMapping + +fromCurrentRange :: PositionMapping -> Range -> Maybe Range +fromCurrentRange mapping (Range a b) = + Range <$> fromCurrentPosition mapping a <*> fromCurrentPosition mapping b + + +fromCurrentRange' :: PositionDelta -> Range -> Maybe Range +fromCurrentRange' = fromCurrentRange . PositionMapping + +zeroMapping :: PositionMapping +zeroMapping = PositionMapping idDelta + +-- | Compose two position mappings. Composes in the same way as function +-- composition (ie the second argument is applied to the position first). +composeDelta :: PositionDelta + -> PositionDelta + -> PositionDelta +composeDelta (PositionDelta to1 from1) (PositionDelta to2 from2) = + PositionDelta (to1 <=< to2) + (from1 >=> from2) + +idDelta :: PositionDelta +idDelta = PositionDelta pure pure + +-- | Convert a set of changes into a delta from k to k + 1 +mkDelta :: [TextDocumentContentChangeEvent] -> PositionDelta +mkDelta cs = foldl' applyChange idDelta cs + +-- | addOldDelta +-- Add a old delta onto a Mapping k n to make a Mapping (k - 1) n +addOldDelta :: + PositionDelta -- ^ delta from version k - 1 to version k + -> PositionMapping -- ^ The input mapping is from version k to version n + -> PositionMapping -- ^ The output mapping is from version k - 1 to version n +addOldDelta delta (PositionMapping pm) = PositionMapping (composeDelta pm delta) + +-- TODO: We currently ignore the right hand side (if there is only text), as +-- that was what was done with lsp* 1.6 packages +applyChange :: PositionDelta -> TextDocumentContentChangeEvent -> PositionDelta +applyChange PositionDelta{..} (TextDocumentContentChangeEvent (Just range) _ text) = PositionDelta + { toDelta = toCurrent range text <=< toDelta + , fromDelta = fromDelta <=< fromCurrent range text + } +applyChange posMapping _ = posMapping + +toCurrent :: Range -> T.Text -> Position -> PositionResult Position +toCurrent (Range start@(Position startLine startColumn) end@(Position endLine endColumn)) t (Position line column) + | line < startLine || line == startLine && column < startColumn = + -- Position is before the change and thereby unchanged. + PositionExact $ Position line column + | line > endLine || line == endLine && column >= endColumn = + -- Position is after the change so increase line and column number + -- as necessary. + PositionExact $ newLine `seq` newColumn `seq` Position newLine newColumn + | otherwise = PositionRange start end + -- Position is in the region that was changed. + where + lineDiff = linesNew - linesOld + linesNew = T.count "\n" t + linesOld = fromIntegral endLine - fromIntegral startLine + newEndColumn :: Int + newEndColumn + | linesNew == 0 = fromIntegral $ fromIntegral startColumn + T.length t + | otherwise = fromIntegral $ T.length $ T.takeWhileEnd (/= '\n') t + newColumn :: Int + newColumn + | line == endLine = fromIntegral $ (fromIntegral column + newEndColumn) - fromIntegral endColumn + | otherwise = column + newLine :: Int + newLine = fromIntegral $ fromIntegral line + lineDiff + +fromCurrent :: Range -> T.Text -> Position -> PositionResult Position +fromCurrent (Range start@(Position startLine startColumn) end@(Position endLine endColumn)) t (Position line column) + | line < startLine || line == startLine && column < startColumn = + -- Position is before the change and thereby unchanged + PositionExact $ Position line column + | line > newEndLine || line == newEndLine && column >= newEndColumn = + -- Position is after the change so increase line and column number + -- as necessary. + PositionExact $ newLine `seq` newColumn `seq` Position newLine newColumn + | otherwise = PositionRange start end + -- Position is in the region that was changed. + where + lineDiff = linesNew - linesOld + linesNew = T.count "\n" t + linesOld = fromIntegral endLine - fromIntegral startLine + newEndLine :: Int + newEndLine = fromIntegral $ fromIntegral endLine + lineDiff + newEndColumn :: Int + newEndColumn + | linesNew == 0 = fromIntegral $ fromIntegral startColumn + T.length t + | otherwise = fromIntegral $ T.length $ T.takeWhileEnd (/= '\n') t + newColumn :: Int + newColumn + | line == newEndLine = fromIntegral $ (fromIntegral column + fromIntegral endColumn) - newEndColumn + | otherwise = column + newLine :: Int + newLine = fromIntegral $ fromIntegral line - lineDiff + +deltaFromDiff :: T.Text -> T.Text -> PositionDelta +deltaFromDiff (T.lines -> old) (T.lines -> new) = + PositionDelta (lookupPos (fromIntegral lnew) o2nPrevs o2nNexts old2new) (lookupPos (fromIntegral lold) n2oPrevs n2oNexts new2old) + where + !lnew = length new + !lold = length old + + diff = getDiff old new + + (V.fromList -> !old2new, V.fromList -> !new2old) = go diff 0 0 + + -- Compute previous and next lines that mapped successfully + !o2nPrevs = V.prescanl' f (-1) old2new + !o2nNexts = V.prescanr' (flip f) lnew old2new + + !n2oPrevs = V.prescanl' f (-1) new2old + !n2oNexts = V.prescanr' (flip f) lold new2old + + f :: Int -> Int -> Int + f !a !b = if b == -1 then a else b + + lookupPos :: Int -> V.Vector Int -> V.Vector Int -> V.Vector Int -> Position -> PositionResult Position + lookupPos end prevs nexts xs (Position line col) + | line >= fromIntegral (V.length xs) = PositionRange (Position end 0) (Position end 0) + | otherwise = case V.unsafeIndex xs (fromIntegral line) of + -1 -> + -- look for the previous and next lines that mapped successfully + let !prev = 1 + V.unsafeIndex prevs (fromIntegral line) + !next = V.unsafeIndex nexts (fromIntegral line) + in PositionRange (Position (fromIntegral prev) 0) (Position (fromIntegral next) 0) + line' -> PositionExact (Position (fromIntegral line') col) + + -- Construct a mapping between lines in the diff + -- -1 for unsuccessful mapping + go :: [Diff T.Text] -> Int -> Int -> ([Int], [Int]) + go [] _ _ = ([],[]) + go (Both _ _ : xs) !glold !glnew = bimap (glnew :) (glold :) $ go xs (glold+1) (glnew+1) + go (First _ : xs) !glold !glnew = first (-1 :) $ go xs (glold+1) glnew + go (Second _ : xs) !glold !glnew = second (-1 :) $ go xs glold (glnew+1) diff --git a/src/Server/SrcLoc.hs b/src/Server/SrcLoc.hs index 9fd191ef..bed64472 100644 --- a/src/Server/SrcLoc.hs +++ b/src/Server/SrcLoc.hs @@ -12,6 +12,7 @@ module Server.SrcLoc , toLSPLocation , toLSPRange , toLSPPosition + , fromLSPRangeWithoutCharacterOffset ) where import Data.IntMap ( IntMap ) @@ -42,6 +43,19 @@ fromLSPPosition table filepath (J.Position line col) = Pos (fromIntegral col + 1) -- starts at 1 (fromIntegral (toOffset table (line, col))) -- starts at 0 +fromLSPRangeWithoutCharacterOffset :: FilePath -> J.Range -> Range +fromLSPRangeWithoutCharacterOffset filepath (J.Range start end) = Range + (fromLSPPositionWithoutCharacterOffset filepath start) + (fromLSPPositionWithoutCharacterOffset filepath end) + +-- | LSP Position -> Data.Loc.Pos +fromLSPPositionWithoutCharacterOffset :: FilePath -> J.Position -> Pos +fromLSPPositionWithoutCharacterOffset filepath (J.Position line col) = Pos + filepath + (fromIntegral line + 1) -- starts at 1 + (fromIntegral col + 1) -- starts at 1 + (-1) -- discard this field + toLSPLocation :: Range -> J.Location toLSPLocation (Range start end) = J.Location (J.Uri $ Text.pack $ posFile start) (toLSPRange (Range start end)) diff --git a/src/Syntax/Abstract/Instances/Json.hs b/src/Syntax/Abstract/Instances/Json.hs index 1bfac60b..442b8ebd 100644 --- a/src/Syntax/Abstract/Instances/Json.hs +++ b/src/Syntax/Abstract/Instances/Json.hs @@ -16,9 +16,4 @@ instance ToJSON CaseClause instance ToJSON Pattern instance ToJSON Lit -instance FromJSON Expr -instance FromJSON Chain -instance FromJSON FuncClause -instance FromJSON CaseClause -instance FromJSON Pattern instance FromJSON Lit diff --git a/src/Syntax/Abstract/Operator.hs b/src/Syntax/Abstract/Operator.hs index c636352a..616141a2 100644 --- a/src/Syntax/Abstract/Operator.hs +++ b/src/Syntax/Abstract/Operator.hs @@ -3,6 +3,8 @@ module Syntax.Abstract.Operator where import Syntax.Abstract ( Expr(..) , Lit(..) , Chain(..) + , Type(..) + , TBase(..) ) import Syntax.Common import Data.Text ( Text ) @@ -82,3 +84,14 @@ sImp = (arith . SImp) NoLoc sconjunct :: [Expr] -> Expr sconjunct [] = true sconjunct xs = foldl1 sConj xs + +-- | Frequently Used Types / Type Operators + +tBool :: Type +tBool = TBase TBool NoLoc + +tInt :: Type +tInt = TBase TInt NoLoc + +tFunc :: Type -> Type -> Type +s `tFunc` t = TFunc s t NoLoc diff --git a/src/Syntax/Abstract/Types.hs b/src/Syntax/Abstract/Types.hs index bb10adf3..f857e144 100644 --- a/src/Syntax/Abstract/Types.hs +++ b/src/Syntax/Abstract/Types.hs @@ -97,7 +97,7 @@ data TBase = TInt | TBool | TChar data Type = TBase TBase Loc | TArray Interval Type Loc - -- TTuple has no srcloc info because it has no conrete syntax at the moment + -- TTuple has no srcloc info because it has no conrete syntax at the moment | TTuple [Type] | TFunc Type Type Loc | TApp Type Type Loc @@ -118,10 +118,10 @@ data Expr | App Expr Expr Loc | Lam Name Expr Loc | Func Name (NonEmpty FuncClause) Loc - -- Tuple has no srcloc info because it has no conrete syntax at the moment + -- Tuple has no srcloc info because it has no conrete syntax at the moment | Tuple [Expr] | Quant Expr [Name] Expr Expr Loc - -- The innermost part of a Redex + -- The innermost part of a Redex -- should look something like `P [ x \ a ] [ y \ b ]` | RedexKernel Name -- the variable to be substituted @@ -129,12 +129,12 @@ data Expr (Set Name) -- free variables in that expression -- NOTE, the expression may be some definition like "P", -- in that case, the free variables should be that of after it's been expanded - (NonEmpty Mapping) + (NonEmpty Mapping) -- a list of mappings of substitutions to be displayed to users (the `[ x \ a ] [ y \ b ]` part) -- The order is reflected. -- The outermost part of a Redex | RedexShell - Int -- for identifying Redexes in frontend-backend interactions + Int -- for identifying Redexes in frontend-backend interactions Expr -- should either be `RedexKernel` or `App (App (App ... RedexKernel arg0) ... argn` | ArrIdx Expr Expr Loc | ArrUpd Expr Expr Expr Loc @@ -153,11 +153,11 @@ type Mapping = Map Text Expr -------------------------------------------------------------------------------- -- | Pattern matching --- pattern -> expr +-- pattern -> expr data CaseClause = CaseClause Pattern Expr deriving (Eq, Show, Generic) --- pattern0 pattern1 pattern2 ... -> expr +-- pattern0 pattern1 pattern2 ... -> expr data FuncClause = FuncClause [Pattern] Expr deriving (Eq, Show, Generic) @@ -174,6 +174,7 @@ extractBinder (PattBinder x ) = [x] extractBinder (PattWildcard _ ) = [] extractBinder (PattConstructor _ xs) = xs >>= extractBinder + ---------------------------------------------------------------- -- | Literals diff --git a/src/Syntax/Abstract/Util.hs b/src/Syntax/Abstract/Util.hs index d86ef585..ec8b7501 100644 --- a/src/Syntax/Abstract/Util.hs +++ b/src/Syntax/Abstract/Util.hs @@ -44,6 +44,11 @@ wrapLam :: [Name] -> Expr -> Expr wrapLam [] body = body wrapLam (x : xs) body = let b = wrapLam xs body in Lam x b (x <--> b) +declaredNames :: [Declaration] -> [Name] +declaredNames decls = concat . map extractNames $ decls + where extractNames (ConstDecl ns _ _ _) = ns + extractNames (VarDecl ns _ _ _) = ns + -- function definition => Just Expr -- constant/variable declaration => Nothing diff --git a/src/Syntax/Common/Instances/Json.hs b/src/Syntax/Common/Instances/Json.hs index 53d6bd22..2a2ee455 100644 --- a/src/Syntax/Common/Instances/Json.hs +++ b/src/Syntax/Common/Instances/Json.hs @@ -1,48 +1,38 @@ {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE InstanceSigs #-} module Syntax.Common.Instances.Json where import Syntax.Common.Types import Data.Aeson import Data.Aeson.Types (Parser) -import Data.Loc (Loc(..), Pos) +import Data.Loc (Loc(..), Pos (..)) -instance ToJSON Name +instance ToJSON Name where + toJSON :: Name -> Value + toJSON (Name text loc) = object + [ "symbol" .= String text + , "location" .= toJSON loc + ] instance ToJSONKey Name -instance FromJSON Name -instance FromJSONKey Name - instance ToJSON ChainOp -instance FromJSON ChainOp instance ToJSON ArithOp -instance FromJSON ArithOp instance ToJSON TypeOp -instance FromJSON TypeOp instance ToJSON Op -instance FromJSON Op instance ToJSON Loc where - toJSON NoLoc = - object - [ "tag" .= String "NoLoc" - ] - toJSON (Loc start end) = - object - [ "tag" .= String "Loc", - "contents" .= (start, end) - ] - -instance FromJSON Loc where - parseJSON = withObject "Loc" $ \v -> do - result <- v .:? "tag" :: Parser (Maybe String) - case result of - Just "Loc" -> do - positions <- (v .:? "contents") :: Parser (Maybe (Pos, Pos)) - case positions of - Just (start, end) -> return $ Loc start end - Nothing -> return NoLoc - _ -> return NoLoc \ No newline at end of file + toJSON :: Loc -> Value + toJSON NoLoc = Null + toJSON (Loc (Pos filePath line column _) (Pos _ line' column' _)) = object + [ "filePath" .= toJSON filePath + , "start" .= object + ["line" .= (line - 1) + , "character" .= (column - 1)] + , "end" .= object + ["line" .= (line' - 1) + , "character" .= (column' - 1)] + ] diff --git a/src/Syntax/Common/Types.hs b/src/Syntax/Common/Types.hs index 65bd9b03..e649f7ba 100644 --- a/src/Syntax/Common/Types.hs +++ b/src/Syntax/Common/Types.hs @@ -141,7 +141,7 @@ initOrderIndex = 1 classificationMap :: Map Op (Fixity,Int) classificationMap = Map.fromList $ concat $ zipWith f [initOrderIndex..] precedenceOrder - where + where f :: Int -> [(Op,Fixity)] -> [(Op,(Fixity,Int))] f n = map (second (,n)) @@ -176,9 +176,9 @@ classificationMap = Map.fromList $ concat $ zipWith f [initOrderIndex..] precede -- classifyArithOp (Max _) = InfixL 4 -- classifyArithOp (Min _) = InfixL 4 --- classifyArithOp (PointsTo _) = Infix 5 --- classifyArithOp (SConj _) = InfixL 6 --- classifyArithOp (SImp _) = Infix 7 +-- classifyArithOp (PointsTo _) = Infix 5 +-- classifyArithOp (SConj _) = InfixL 6 +-- classifyArithOp (SImp _) = Infix 7 -- classifyArithOp (Disj _) = InfixL 9 -- classifyArithOp (DisjU _) = InfixL 9 @@ -190,7 +190,7 @@ classificationMap = Map.fromList $ concat $ zipWith f [initOrderIndex..] precede classify :: Op -> (Fixity,Int) -classify op = fromMaybe (error "Operator's precedenceOrder is not completely defined.") +classify op = fromMaybe (error "Operator's precedenceOrder is not completely defined.") $ Map.lookup (wipeLoc op) classificationMap precOf :: Op -> Int @@ -246,7 +246,7 @@ wipeLoc op = case op of isAssocOp :: Op -> Bool isAssocOp (ArithOp (Mul _)) = True isAssocOp (ArithOp (Add _)) = True -isAssocOp (ArithOp (Conj _)) = True +isAssocOp (ArithOp (Conj _)) = True isAssocOp (ArithOp (ConjU _)) = True isAssocOp (ArithOp (Disj _)) = True isAssocOp (ArithOp (DisjU _)) = True diff --git a/src/Syntax/Concrete/Types.hs b/src/Syntax/Concrete/Types.hs index 38eeb286..8cfdd978 100644 --- a/src/Syntax/Concrete/Types.hs +++ b/src/Syntax/Concrete/Types.hs @@ -97,7 +97,7 @@ data Stmt | LoopInvariant (Token "{") Expr (Token ",") (Token "bnd") (Token ":") Expr (Token "}") | Do (Token "do") (SepBy "|" GdCmd) (Token "od") | If (Token "if") (SepBy "|" GdCmd) (Token "fi") - | SpecQM Range -- ? to be rewritten as {!!} + | SpecQM Range -- ? to be rewritten as [!!] | Spec (Token "[!") [L Tok] (Token "!]") | Proof Text Text Text Range -- anchor, the content of the block, the whole proof block (for pretty's reconstruction) | Alloc Name (Token ":=") (Token "new") (Token "(") (SepBy "," Expr) (Token ")") @@ -198,4 +198,4 @@ data Pattern data Lit = LitInt Int Range | LitBool Bool Range | LitChar Char Range deriving (Show, Eq, Generic) --------------------------------------------------------------------------------- +-------------------------------------------------------------------------------- \ No newline at end of file diff --git a/src/Syntax/Parser/Error.hs b/src/Syntax/Parser/Error.hs index 2272cd07..b76dce0e 100644 --- a/src/Syntax/Parser/Error.hs +++ b/src/Syntax/Parser/Error.hs @@ -1,13 +1,15 @@ +{-# LANGUAGE DeriveGeneric #-} module Syntax.Parser.Error where import Data.List.NonEmpty ( NonEmpty ) import Data.Loc ( Loc , Pos ) - +import GHC.Generics ( Generic ) +import qualified Data.Aeson.Types as JSON -------------------------------------------------------------------------------- -- | Error data ParseError = LexicalError Pos | SyntacticError (NonEmpty (Loc, String)) String -- The second argument is for parsing log. - deriving (Eq, Show) + deriving (Eq, Show, Generic) \ No newline at end of file diff --git a/src/Syntax/Substitution.hs b/src/Syntax/Substitution.hs index 584d9bd5..5e00b0cd 100644 --- a/src/Syntax/Substitution.hs +++ b/src/Syntax/Substitution.hs @@ -1,5 +1,5 @@ {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, - FlexibleContexts #-} + FlexibleContexts, MonoLocalBinds, FunctionalDependencies #-} module Syntax.Substitution where import Control.Monad ( forM ) @@ -10,8 +10,9 @@ import Data.Set ( Set ) import qualified Data.Set as Set import Data.Loc ( Loc ) import GCL.Common -import GCL.WP.Util ( declaredNames ) +-- import GCL.WP.Util ( declaredNames ) import Syntax.Abstract.Types +import Syntax.Abstract.Util ( declaredNames ) import Syntax.Common type Subst b = Map Text b @@ -20,16 +21,15 @@ class Substitutable m a b where subst :: Subst b -> a -> m a -- types that has a concept of a "variable" -class Variableous e where - isVar :: e -> Maybe Name - mkVar :: Name -> Loc -> e +class Variableous e t | e -> t where -- t denotes the type of the variable + isVar :: e -> Maybe (Name, t) + mkVar :: Name -> t -> Loc -> e -instance Variableous Expr where - isVar (Var x _) = Just x - isVar (Const x _) = Just x +instance Variableous Expr () where + isVar (Var x _) = Just (x, ()) + isVar (Const x _) = Just (x, ()) isVar _ = Nothing - mkVar = Var - + mkVar x () l = Var x l instance Fresh m => Substitutable m Expr Expr where subst _ e@(Lit _ _) = return e @@ -44,13 +44,13 @@ instance Fresh m => Substitutable m Expr Expr where subst sb (Lam x e l) | nameToText x `elem` keys sb = return (Lam x e l) | otherwise = do - (xs', e', _) <- substBinder sb [x] e + (xs', e', _) <- substBinderTypeless sb [x] e return (Lam (head xs') e' l) subst sb (Func f clauses l) = Func f <$> mapM (subst sb) clauses <*> pure l subst sb (Tuple es) = Tuple <$> mapM (subst sb) es subst sb (Quant op xs ran body l) = do - (xs', (ran', body'), _) <- substBinder sb xs (ran, body) + (xs', (ran', body'), _) <- substBinderTypeless sb xs (ran, body) return $ Quant op xs' ran' body' l subst _ (RedexKernel _ _ _ _) = error "not knowing what is going on here" subst _ (RedexShell _ _) = error "not knowing what is going on here" @@ -63,6 +63,13 @@ instance Fresh m => Substitutable m Expr Expr where $ \(CaseClause patt body) -> CaseClause patt <$> subst sb body return $ Case e cases' l +-- just a wrapper calling substBinder, when e is typeless Expr +substBinderTypeless :: (Fresh m, Substitutable m a Expr, Free a) => + Subst Expr -> [Name] -> a -> m ([Name], a, Subst Expr) +substBinderTypeless sb binders body = + (\(binders', body', sb') -> (map fst binders', body', sb')) + <$> (substBinder sb [(b,()) | b <- binders] body) + instance Fresh m => Substitutable m Chain Expr where subst sb (Pure expr loc) = Pure <$> subst sb expr <*> pure loc subst sb (More ch' op expr loc) = More <$> subst sb ch' <*> pure op <*> subst sb expr <*> pure loc @@ -106,7 +113,7 @@ instance Fresh m => Substitutable m GdCmd Expr where instance Fresh m => Substitutable m Program Expr where subst sb (Program defns decls props stmts l) = do (_, (decls', props', stmts'), _) <- - substBinder sb locals (decls, props, stmts) + substBinderTypeless sb locals (decls, props, stmts) return $ Program defns decls' props' stmts' l -- SCM: TODO: deal with defns where locals = declaredNames decls @@ -146,16 +153,16 @@ instance (Monad m, Substitutable m a b) => -- where (xs', e') <- substBinder sb xs e. -- It performs substitution on e, while renaming xs if necessary. -substBinder :: (Fresh m, Variableous e, +substBinder :: (Fresh m, Variableous e t, Substitutable m a e, Free e, Free a) => - Subst e -> [Name] -> a -> m ([Name], a, Subst e) + Subst e -> [(Name, t)] -> a -> m ([(Name, t)], a, Subst e) substBinder sb binders body = do sb'' <- genBinderRenaming fvsb binders - let binders' = renameVars sb'' binders + let binders' = zip (renameVars sb'' (map fst binders)) (map snd binders) let sbnew = sb'' <> sb' body' <- subst sbnew body return $ (binders', body', sbnew) - where sb' = shrinkSubst binders (freeVarsT body) sb + where sb' = shrinkSubst (map fst binders) (freeVarsT body) sb fvsb = Set.unions . map freeVarsT . elems $ sb' -- Utilities @@ -166,23 +173,23 @@ shrinkSubst binders ns subs = where substractKeys sb bs = filterWithKey (\k _ -> not (k `elem` bs)) sb -genBinderRenaming :: (Fresh m, Variableous e) => - Set Text -> [Name] -> m (Subst e) +genBinderRenaming :: (Fresh m, Variableous e t) => + Set Text -> [(Name, t)] -> m (Subst e) genBinderRenaming _ [] = return empty -genBinderRenaming fvs (Name x l : xs) +genBinderRenaming fvs ((Name x l, t) : xs) | x `Set.member` fvs = do x' <- freshName x l - insert x (mkVar x' l) <$> genBinderRenaming fvs xs + insert x (mkVar x' t l) <$> genBinderRenaming fvs xs | otherwise = genBinderRenaming fvs xs -renameVars :: Variableous e => Subst e -> [Name] -> [Name] +renameVars :: Variableous e t => Subst e -> [Name] -> [Name] renameVars sb = map (renameVar sb) -renameVar :: Variableous e => Subst e -> Name -> Name +renameVar :: Variableous e t => Subst e -> Name -> Name renameVar sb x = case lookup (nameToText x) sb of Nothing -> x Just e -> case isVar e of - Just y -> y + Just (y, _) -> y Nothing -> error "variable should be substituted for a variable" --- SCM: we assume that renameVars always succeed. -- Do we need to raise a catchable error? diff --git a/src/Syntax/Typed.hs b/src/Syntax/Typed.hs index 874a450d..b91c3a82 100644 --- a/src/Syntax/Typed.hs +++ b/src/Syntax/Typed.hs @@ -1,68 +1,6 @@ -module Syntax.Typed where +module Syntax.Typed ( + module Syntax.Typed.Types + ) where -import Data.Text ( Text ) -import Data.Loc ( Loc ) -import Data.Loc.Range ( Range ) -import Syntax.Abstract.Types ( Lit, Type ) -import Syntax.Common.Types ( Name, Op ) - -data TypedProgram = Program [TypedDefinition] -- definitions (the functional language part) - [TypedDeclaration] -- constant and variable declarations - [TypedExpr] -- global properties - [TypedStmt] -- main program - Loc - deriving (Eq, Show) - -data TypedDefinition - = TypeDefn Name [Name] [TypedTypeDefnCtor] Loc - | FuncDefnSig Name Type (Maybe TypedExpr) Loc - | FuncDefn Name TypedExpr - deriving (Eq, Show) - -data TypedTypeDefnCtor = TypedTypeDefnCtor Name [Name] - deriving (Eq, Show) - -data TypedDeclaration - = ConstDecl [Name] Type (Maybe TypedExpr) Loc - | VarDecl [Name] Type (Maybe TypedExpr) Loc - deriving (Eq, Show) - -data TypedStmt - = Skip Loc - | Abort Loc - | Assign [Name] [TypedExpr] Loc - | AAssign TypedExpr TypedExpr TypedExpr Loc - | Assert TypedExpr Loc - | LoopInvariant TypedExpr TypedExpr Loc - | Do [TypedGdCmd] Loc - | If [TypedGdCmd] Loc - | Spec Text Range - | Proof Text Text Range - | Alloc Name [TypedExpr] Loc -- p := new (e1,e2,..,en) - | HLookup Name TypedExpr Loc -- x := *e - | HMutate TypedExpr TypedExpr Loc -- *e1 := e2 - | Dispose TypedExpr Loc -- dispose e - | Block TypedProgram Loc - deriving (Eq, Show) - -data TypedGdCmd = TypedGdCmd TypedExpr [TypedStmt] Loc - deriving (Eq, Show) - -data TypedExpr - = Lit Lit Type Loc - | Var Name Type Loc - | Const Name Type Loc - | Op Op Type - | Chain TypedChain - | App TypedExpr TypedExpr Loc - | Lam Name Type TypedExpr Loc - | Quant TypedExpr [Name] TypedExpr TypedExpr Loc - | ArrIdx TypedExpr TypedExpr Loc - | ArrUpd TypedExpr TypedExpr TypedExpr Loc - deriving (Eq, Show) - -- FIXME: Other constructors. - -data TypedChain - = Pure TypedExpr - | More TypedChain Op Type TypedExpr - deriving (Eq, Show) \ No newline at end of file +import Syntax.Typed.Types +import Syntax.Typed.Instances.Located () diff --git a/src/Syntax/Typed/Instances/Free.hs b/src/Syntax/Typed/Instances/Free.hs new file mode 100644 index 00000000..095e661f --- /dev/null +++ b/src/Syntax/Typed/Instances/Free.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, + FlexibleContexts, MonoLocalBinds #-} +module Syntax.Typed.Instances.Free where + +import Data.Set ( Set + , (\\) + ) +import qualified Data.Set as Set +import Syntax.Typed.Types +import GCL.Common +import Syntax.Common + +instance Free Expr where + freeVars (Var x _ _ ) = Set.singleton x + freeVars (Const x _ _ ) = Set.singleton x + freeVars (Op _ _ ) = mempty + freeVars (Chain chain ) = freeVars chain + freeVars (Lit _ _ _ ) = mempty + freeVars (App e1 e2 _ ) = freeVars e1 <> freeVars e2 + freeVars (Lam x _ e _ ) = freeVars e \\ Set.singleton x + freeVars (Quant op xs range term _) = + (freeVars op <> freeVars range <> freeVars term) \\ Set.fromList xs + freeVars (ArrIdx e1 e2 _ ) = freeVars e1 <> freeVars e2 + freeVars (ArrUpd e1 e2 e3 _ ) = freeVars e1 <> freeVars e2 <> freeVars e3 + freeVars (Subst e sb) = (freeVars e \\ Set.fromList dom) <> freeVars rng + where dom = map fst sb + rng = map snd sb + +instance Free Chain where + freeVars (Pure expr) = freeVars expr + freeVars (More chain _op _ expr) = freeVars chain <> freeVars expr + +instance Free Declaration where + freeVars (ConstDecl ns _ expr _) = + Set.fromList ns <> freeVars expr + freeVars (VarDecl ns _ expr _) = + Set.fromList ns <> freeVars expr + +instance Free Stmt where + freeVars (Skip _) = mempty + freeVars (Abort _) = mempty + freeVars (Assign ns es _) = + Set.fromList ns <> Set.unions (map freeVars es) + freeVars (AAssign a i e _) = + freeVars a <> freeVars i <> freeVars e + freeVars (Assert p _) = freeVars p + freeVars (LoopInvariant p b _) = freeVars p <> freeVars b + freeVars (Do gdcmds _) = Set.unions (map freeVars gdcmds) + freeVars (If gdcmds _) = Set.unions (map freeVars gdcmds) + freeVars (Spec _ _ _) = mempty + freeVars (Proof _ _ _) = mempty + freeVars (Alloc x es _) = + Set.singleton x <> Set.unions (map freeVars es) + freeVars (HLookup x e _) = + Set.singleton x <> freeVars e + freeVars (HMutate e1 e2 _) = freeVars e1 <> freeVars e2 + freeVars (Dispose e _) = freeVars e + freeVars (Block prog _) = freeVars prog + +instance Free GdCmd where + freeVars (GdCmd g stmts _) = + freeVars g <> Set.unions (map freeVars stmts) + +instance Free Program where + freeVars (Program _defns decls props stmts _) = + foldMap freeVars decls <> foldMap freeVars props <> foldMap freeVars stmts + -- SCM: TODO: deal with defns later. diff --git a/src/Syntax/Typed/Instances/Located.hs b/src/Syntax/Typed/Instances/Located.hs new file mode 100644 index 00000000..fe1da6de --- /dev/null +++ b/src/Syntax/Typed/Instances/Located.hs @@ -0,0 +1,58 @@ +module Syntax.Typed.Instances.Located where + +import Data.Loc +import Prelude hiding ( Ordering(..) ) +import Syntax.Typed.Types +import Syntax.Common ( ) + +instance Located Program where + locOf (Program _ _ _ _ l) = l + +instance Located Declaration where + locOf (ConstDecl _ _ _ l) = l + locOf (VarDecl _ _ _ l) = l + +instance Located Definition where + locOf (TypeDefn _ _ _ r) = r + locOf (FuncDefnSig _ _ _ r) = r + locOf (FuncDefn l r ) = l <--> r + +instance Located TypeDefnCtor where + locOf (TypeDefnCtor l r) = l <--> r + +instance Located Stmt where + locOf (Skip l ) = l + locOf (Abort l ) = l + locOf (Assign _ _ l ) = l + locOf (AAssign _ _ _ l ) = l + locOf (Assert _ l ) = l + locOf (LoopInvariant _ _ l) = l + locOf (Do _ l ) = l + locOf (If _ l ) = l + locOf (Spec _ r _ ) = locOf r + locOf (Proof _ _ r ) = locOf r + locOf (Alloc _ _ l ) = l + locOf (HLookup _ _ l ) = l + locOf (HMutate _ _ l ) = l + locOf (Dispose _ l ) = l + locOf (Block _ l ) = l + +instance Located GdCmd where + locOf (GdCmd _ _ l) = l + +instance Located Expr where + locOf (Lit _ _ l) = l + locOf (Var _ _ l) = l + locOf (Const _ _ l) = l + locOf (Op op _ ) = locOf op + locOf (Chain chain ) = locOf chain + locOf (App _ _ l) = l + locOf (Lam _ _ _ l) = l + locOf (Quant _ _ _ _ l) = l + locOf (ArrIdx _ _ l) = l + locOf (ArrUpd _ _ _ l) = l + locOf (Subst _ _) = NoLoc + +instance Located Chain where + locOf (Pure e ) = locOf e + locOf (More _ _ _ e) = locOf e diff --git a/src/Syntax/Typed/Instances/Substitution.hs b/src/Syntax/Typed/Instances/Substitution.hs new file mode 100644 index 00000000..6e0b893e --- /dev/null +++ b/src/Syntax/Typed/Instances/Substitution.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, + FlexibleContexts, MonoLocalBinds #-} +module Syntax.Typed.Instances.Substitution where + +import Control.Monad ( forM ) +import Prelude hiding ( lookup ) +import Data.Loc +import Data.Map hiding ( map ) +import qualified Data.Map as Map +import Prelude hiding ( Ordering(..) ) +import Syntax.Typed.Types +import Syntax.Substitution +import GCL.Common +import Syntax.Common +import Syntax.Typed.Instances.Free () + +instance Variableous Expr Type where + isVar (Var x t _) = Just (x, t) + isVar (Const x t _) = Just (x, t) + isVar _ = Nothing + mkVar x t l = Var x t l + +instance Fresh m => Substitutable m Expr Expr where + subst _ e@(Lit _ _ _) = return e + subst sb (Var x t l) = + return . maybe (Var x t l) id $ Map.lookup (nameToText x) sb + subst sb (Const x t l) = + return . maybe (Const x t l) id $ Map.lookup (nameToText x) sb + subst _ e@(Op _ _) = return e + subst sb (Chain ch) = Chain <$> subst sb ch + subst sb (App e1 e2 l) = + App <$> subst sb e1 <*> subst sb e2 <*> pure l + subst sb (Lam x t e l) + | nameToText x `elem` keys sb = return (Lam x t e l) + | otherwise = do + (xs, e', _) <- substBinder sb [(x,t)] e + let x' = fst (head xs) + return (Lam x' t e' l) + subst sb (Quant op xs ran body l) = do + (xs', (ran', body'), _) <- undefined -- SCM, TODO substBinder sb xs (ran, body) + return $ Quant op xs' ran' body' l + subst sb (ArrIdx a i l) = + ArrIdx <$> subst sb a <*> subst sb i <*> pure l + subst sb (ArrUpd a i v l) = + ArrUpd <$> subst sb a <*> subst sb i <*> subst sb v <*> pure l + subst sb (Subst e tb) = + Subst <$> subst sb e <*> forM tb (\(x, f) -> + (,) x <$> subst sb f) + +instance Fresh m => Substitutable m Chain Expr where + subst sb (Pure expr) = Pure <$> subst sb expr + subst sb (More ch' op t expr) = More <$> subst sb ch' <*> pure op <*> pure t <*> subst sb expr + +instance Fresh m => Substitutable m Stmt Expr where diff --git a/src/Syntax/Typed/Operator.hs b/src/Syntax/Typed/Operator.hs new file mode 100644 index 00000000..ad408843 --- /dev/null +++ b/src/Syntax/Typed/Operator.hs @@ -0,0 +1,100 @@ +module Syntax.Typed.Operator where + +import Syntax.Abstract.Operator ( tBool, tInt, tFunc ) +import Syntax.Typed.Types +import Syntax.Typed.Util ( typeOf ) +import Syntax.Typed.Instances.Located +import Syntax.Common +import Data.Text ( Text ) +import Data.Loc ( Loc(..) + , (<-->) + , locOf + ) +import Prelude hiding ( Ordering(..) ) + +unary :: ArithOp -> Type -> Expr -> Expr +unary op t x = App (Op (ArithOp op) t) x (x <--> op) + +arith :: ArithOp -> Type -> Expr -> Expr -> Expr +arith op t x y = App (App (Op (ArithOp op) t) x (x <--> op)) y (x <--> y) + +chain :: ChainOp -> Type -> Expr -> Expr -> Expr -- TODO: This might be wrong. Needs further investigation. +chain op t x y = Chain (More (Pure x) (ChainOp op) t y) + +neg :: Expr -> Expr +neg = unary (NegU NoLoc) (tBool `tFunc` tBool) + + -- Type of binary logic operators: Bool -> Bool -> Bool + -- Type of binary Int operators: Int -> Int -> Int, etc. + -- Because they are used in many occassions. + +tBinLogicOp :: Type +tBinLogicOp = tBool `tFunc` (tBool `tFunc` tBool) + +tBinIntOp :: Type +tBinIntOp = tInt `tFunc` (tInt `tFunc` tInt) + +tBinIntROp :: Type +tBinIntROp = tInt `tFunc` (tInt `tFunc` tBool) + +lt, gt, gte, lte :: Expr -> Expr -> Expr +lt = chain (LT NoLoc) tBinIntROp +gt = chain (GT NoLoc) tBinIntROp +gte = chain (GTEU NoLoc) tBinIntROp +lte = chain (LTEU NoLoc) tBinIntROp + +conj, disj, implies :: Expr -> Expr -> Expr +conj = arith (ConjU NoLoc) tBinLogicOp +disj = arith (DisjU NoLoc) tBinLogicOp +implies = arith (ImpliesU NoLoc) tBinLogicOp + +add :: Expr -> Expr -> Expr +add = arith (Add NoLoc) tBinIntOp + +eqq :: Expr -> Expr -> Expr +e0 `eqq` e1 = + Chain (More (Pure e0) (ChainOp (EQ NoLoc)) (typeOf e0) e1) + +true, false :: Expr +true = Lit (Bol True) tBool NoLoc +false = Lit (Bol False) tBool NoLoc + +conjunct :: [Expr] -> Expr +conjunct [] = true +conjunct xs = foldl1 conj xs + +disjunct :: [Expr] -> Expr +disjunct [] = false +disjunct xs = foldl1 disj xs + +predEq :: Expr -> Expr -> Bool +predEq = (==) + +constant :: Text -> Type -> Expr +constant x t = Const (Name x NoLoc) t NoLoc + +variable :: Text -> Type -> Expr +variable x t = Var (Name x NoLoc) t NoLoc + +nameVar :: Name -> Type -> Expr +nameVar x t = Var x t NoLoc + +number :: Int -> Expr +number n = Lit (Num n) tInt NoLoc + +exists :: [Name] -> Expr -> Expr -> Expr +exists xs ran term = Quant (Op (ArithOp (DisjU NoLoc)) tBinLogicOp) + xs ran term NoLoc + +forAll :: [Name] -> Expr -> Expr -> Expr +forAll xs ran term = Quant (Op (ArithOp (ConjU NoLoc)) tBinLogicOp) + xs ran term NoLoc + +pointsTo, sConj, sImp :: Expr -> Expr -> Expr +pointsTo = arith (PointsTo NoLoc) tBinIntOp +sConj = arith (SConj NoLoc) tBinLogicOp +sImp = arith (SImp NoLoc) tBinLogicOp + +sconjunct :: [Expr] -> Expr +sconjunct [] = true +sconjunct xs = foldl1 sConj xs diff --git a/src/Syntax/Typed/Types.hs b/src/Syntax/Typed/Types.hs new file mode 100644 index 00000000..2cb98ad7 --- /dev/null +++ b/src/Syntax/Typed/Types.hs @@ -0,0 +1,74 @@ +module Syntax.Typed.Types ( + module Syntax.Typed.Types, + Lit(..), Type(..), TBase(..) + ) where + +import Data.Text ( Text ) +import Data.Loc ( Loc ) +import Data.Loc.Range ( Range ) +import Syntax.Abstract.Types ( Lit(..), Type(..), TBase(..) ) +import Syntax.Common.Types ( Name, Op ) +import GCL.Common ( TypeEnv, Index, TypeInfo ) + +data Program = Program [Definition] -- definitions (the functional language part) + [Declaration] -- constant and variable declarations + [Expr] -- global properties + [Stmt] -- main program + Loc + deriving (Eq, Show) + +data Definition + = TypeDefn Name [Name] [TypeDefnCtor] Loc + | FuncDefnSig Name Type (Maybe Expr) Loc + | FuncDefn Name Expr + deriving (Eq, Show) + +data TypeDefnCtor = TypeDefnCtor Name [Name] + deriving (Eq, Show) + +data Declaration + = ConstDecl [Name] Type (Maybe Expr) Loc + | VarDecl [Name] Type (Maybe Expr) Loc + deriving (Eq, Show) + +data Stmt + = Skip Loc + | Abort Loc + | Assign [Name] [Expr] Loc + | AAssign Expr Expr Expr Loc + | Assert Expr Loc + | LoopInvariant Expr Expr Loc + | Do [GdCmd] Loc + | If [GdCmd] Loc + | Spec Text Range [(Index, TypeInfo)] + | Proof Text Text Range + | Alloc Name [Expr] Loc -- p := new (e1,e2,..,en) + | HLookup Name Expr Loc -- x := *e + | HMutate Expr Expr Loc -- *e1 := e2 + | Dispose Expr Loc -- dispose e + | Block Program Loc + deriving (Eq, Show) + +data GdCmd = GdCmd Expr [Stmt] Loc + deriving (Eq, Show) + +data Expr + = Lit Lit Type Loc + | Var Name Type Loc + | Const Name Type Loc + | Op Op Type + | Chain Chain + | App Expr Expr Loc + | Lam Name Type Expr Loc + | Quant Expr [Name] Expr Expr Loc + | ArrIdx Expr Expr Loc + | ArrUpd Expr Expr Expr Loc + + | Subst Expr [(Name, Expr)] + deriving (Eq, Show) + -- FIXME: Other constructors. + +data Chain + = Pure Expr + | More Chain Op Type Expr + deriving (Eq, Show) diff --git a/src/Syntax/Typed/Util.hs b/src/Syntax/Typed/Util.hs new file mode 100644 index 00000000..0532ba49 --- /dev/null +++ b/src/Syntax/Typed/Util.hs @@ -0,0 +1,76 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Syntax.Typed.Util where + +import Control.Arrow ( second ) +import Data.Map ( Map ) +import qualified Data.Map as Map +import qualified Data.Maybe as Maybe +import Data.Text ( Text ) +import Data.Loc ( (<-->), Loc(..) ) +import Syntax.Typed +import Syntax.Common ( Name(..), nameToText ) + + +getGuards :: [GdCmd] -> [Expr] +getGuards = fst . unzipGdCmds + +unzipGdCmds :: [GdCmd] -> ([Expr], [[Stmt]]) +unzipGdCmds = unzip . map (\(GdCmd x y _) -> (x, y)) + +wrapLam :: [(Name, Type)] -> Expr -> Expr +wrapLam [] body = body +wrapLam ((x,t) : xs) body = let b = wrapLam xs body in Lam x t b (x <--> b) + +declaredNames :: [Declaration] -> [Name] +declaredNames decls = concat . map extractNames $ decls + where extractNames (ConstDecl ns _ _ _) = ns + extractNames (VarDecl ns _ _ _) = ns + +declaredNamesTypes :: [Declaration] -> [(Name, Type)] +declaredNamesTypes decls = concat . map extractNames $ decls + where extractNames (ConstDecl ns t _ _) = [(n, t) | n <- ns] + extractNames (VarDecl ns t _ _) = [(n, t) | n <- ns] + +typeOf :: Expr -> Type +typeOf (Lit _ t _) = t +typeOf (Var _ t _) = t +typeOf (Const _ t _) = t +typeOf (Op _ t) = t +typeOf (Chain ch) = typeOfChain ch +typeOf (App e0 _ _) = case typeOf e0 of + TFunc _ t _ -> t + _ -> error "left term not having function type in a typed expression" +typeOf (Lam _ t0 e _) = TFunc t0 (typeOf e) NoLoc +typeOf (Quant _ _ _ body _) = typeOf body +typeOf (ArrIdx arr _ _) = case typeOf arr of + TArray _ t _ -> t + TFunc _ t _ -> t + _ -> error "indexed term not an array in a typed expression " +typeOf (ArrUpd arr _ _ _) = typeOf arr +typeOf (Subst e _) = typeOf e + +typeOfChain :: Chain -> Type +typeOfChain (Pure e) = typeOf e -- SCM: shouldn't happen? +typeOfChain (More _ _ _ _) = TBase TBool NoLoc + + +programToScopeForSubstitution :: Program -> Map Text (Maybe Expr) +programToScopeForSubstitution (Program defns decls _ _ _) = + Map.mapKeys nameToText + $ foldMap extractDeclaration decls + <> ( Map.fromList + . map (second Just) + . Maybe.mapMaybe pickFuncDefn + ) + defns + where + extractDeclaration :: Declaration -> Map Name (Maybe Expr) + extractDeclaration (ConstDecl names _ _ _) = + Map.fromList (zip names (repeat Nothing)) + extractDeclaration (VarDecl names _ _ _) = + Map.fromList (zip names (repeat Nothing)) + +pickFuncDefn :: Definition -> Maybe (Name, Expr) +pickFuncDefn (FuncDefn n expr) = Just (n, expr) +pickFuncDefn _ = Nothing