packages feed

MiniAgda 0.2022.3.11 → 0.2025.7.23

raw patch · 321 files changed

+725/−732 lines, 321 filesdep +MiniAgdadep +optparse-applicativedep +string-qqdep ~basedep ~mtl

Dependencies added: MiniAgda, optparse-applicative, string-qq

Dependency ranges changed: base, mtl

Files

CHANGELOG view
@@ -1,5 +1,7 @@ CHANGELOG for MiniAgda +0.2025.7.23   Drop support for GHC 7, tested with GHC 8.0 - 9.12.2.+ 0.2022.3.11   Fixed compilation with mtl-2.3-rc3, tested with ghc 9.2.2, added cabal test.  0.2020.4.14   Tested compilation with ghc 8.10.1.
MiniAgda.cabal view
@@ -1,6 +1,7 @@ cabal-version:   2.4+  -- 2.4 introduces the ** glob patterns used in data-files name:            MiniAgda-version:         0.2022.3.11+version:         0.2025.7.23 build-type:      Simple license:         MIT license-file:    LICENSE@@ -23,7 +24,12 @@   patterns for a more general handling of coinduction.  tested-with:-  GHC == 9.2.2+  GHC == 9.12.2+  GHC == 9.10.2+  GHC == 9.8.4+  GHC == 9.6.7+  GHC == 9.4.8+  GHC == 9.2.8   GHC == 9.0.2   GHC == 8.10.7   GHC == 8.8.4@@ -31,15 +37,22 @@   GHC == 8.4.4   GHC == 8.2.2   GHC == 8.0.2-  GHC == 7.10.3-  GHC == 7.8.4-  GHC == 7.6.3 -extra-source-files:+extra-doc-files:   CHANGELOG   README.md++extra-source-files:   Makefile   src/Makefile+  stack-9.12.yaml+  stack-9.10.yaml+  stack-9.8.yaml+  stack-9.6.yaml+  stack-9.4.3.yaml+  stack-9.2.5.yaml+  stack-9.0.2.yaml+  stack-8.10.7.yaml  data-files:   test/fail/Makefile@@ -54,19 +67,25 @@   type:     git   location: https://github.com/andreasabel/miniagda -executable miniagda+library   hs-source-dirs:       src   build-depends:        array             >= 0.3    && < 0.6-                      , base              >= 4.6    && < 5-                      , containers        >= 0.3    && < 0.7+                      , base              >= 4.9    && < 5+                      , containers        >= 0.3    && < 1                       , haskell-src-exts  >= 1.21   && < 1.22                           -- haskell-src-exts is a nervous package with incompatibilities                           -- in every new version, thus, we need tight bounds.-                      , mtl               >= 2.2.2  && < 2.4+                      , mtl               >= 2.2.1  && < 2.4+                      , optparse-applicative+                                          >= 0.16.0.0 && < 1+                          -- optparse-applicative-0.16.0.0 adds some1                       , pretty            >= 1.0    && < 1.2+                      , string-qq                       , transformers-  build-tool-depends:   happy:happy       >= 1.15   && < 2++  build-tool-depends:   happy:happy       >= 1.15   && < 3                       , alex:alex         >= 3.0    && < 4+   default-language:     Haskell98   default-extensions:   CPP                         MultiParamTypeClasses@@ -79,14 +98,17 @@                         TupleSections                         NamedFieldPuns                         LambdaCase-  main-is:              Main.hs-  other-modules:        Abstract++  exposed-modules:      Abstract                         Collection                         Concrete                         Eval                         Extract                         HsSyntax                         Lexer+                        License+                        MainLib+                        Options                         Parser                         Polarity                         PrettyTCM@@ -96,27 +118,33 @@                         TCM                         Termination                         ToHaskell-                        Tokens                         TraceError                         TreeShapedOrder                         TypeChecker                         Util                         Value+                        Version                         Warshall+  other-modules:        Paths_MiniAgda+  autogen-modules:      Paths_MiniAgda -  -- TODO: Warning-free-  -- ghc-options:      -Wall-  --                   -fno-warn-type-defaults-  --                   -fno-warn-dodgy-imports-  --                   -fno-warn-unused-binds-  --                   -fno-warn-unused-matches-  --                   -fno-warn-name-shadowing-  --                   -fno-warn-incomplete-patterns+  ghc-options:          -Wall+                        -Wcompat+                        -Wno-type-defaults+                        -Wno-dodgy-imports+                        -Wno-unused-binds+                        -Wno-unused-matches+                        -Wno-name-shadowing+                        -Wno-incomplete-patterns -  if impl(ghc >= 8.0)-    ghc-options:        -Wcompat   if impl(ghc >= 9.2)     ghc-options:        -Wno-incomplete-uni-patterns+                        -Wno-incomplete-record-updates+executable miniagda+  hs-source-dirs:       main+  main-is:              Main.hs+  build-depends:        MiniAgda+  default-language:     Haskell2010  test-suite test   type:                 exitcode-stdio-1.0@@ -124,7 +152,7 @@   main-is:              GoldplateTests.hs   default-language:     Haskell2010   ghc-options:          -threaded-  build-depends:        base >= 4.11+  build-depends:        base >= 4.11 && < 5                           -- goldplate requires ghc >= 8.4                       , process   build-tool-depends:   goldplate:goldplate >= 0.2
README.md view
@@ -10,7 +10,7 @@  A prototypical dependently typed languages with sized types and variances. -## Installation+## Installation from Hackage  Requires `ghc` and `cabal`, for instance via the Haskell Platform or via `ghcup`. In a shell, type@@ -19,11 +19,63 @@   cabal install MiniAgda ``` -To build MiniAgda from source, replace the last command with+## Installation from Stackage -```- make-```+MiniAgda is not on Stackage because it depends on a specific version of `haskell-src-exts` rather than the latest version.+You can install with `stack` from source though, see next section.++## Installation from source++1. Obtain the sources.+   ```+   git clone https://github.com/andreasabel/miniagda+   cd miniagda+   ```++2. Checkout the desired version (optional):+   If you want to build a released version or a branch rather than the latest `master`, switch to this version/branch.+   ```+   git checkout $REF+   ```+   E.g. `REF = v0.2022.3.11` for version `0.2022.3.11` or `REF = unfold` for branch `unfold`.++3. Building and running the tests (optional).++   - With `cabal` (requires `ghc` in your PATH):+     ```+     cabal build --enable-tests+     cabal test+     ```+     After building, you can run MiniAgda locally, e.g.:+     ```+     cabal run miniagda -- examples/Gcd/gcd.ma+     ```++   - With `stack`:+     ```+     stack build --stack-yaml=stack-$GHCVER.yaml+     stack test  --stack-yaml=stack-$GHCVER.yaml+     ```+     At the time of writing (2025-07-23), `GHCVER` can be any of `9.12`, `9.10`, `9.8`, `9.6`, and some older ones.++     After building, you can run MiniAgda locally, e.g.:+     ```+     stack run --stack-yaml=stack-9.12.yaml -- examples/Gcd/gcd.ma+     ```+     You can copy `stack-$GHCVER.yaml` for your choice of `GHCVER` into `stack.yaml` and drop the `--stack-yaml` argument from `stack` invocation.+++4. Install.+   - With `cabal` (requires `ghc` in your PATH):+     ```+     cabal install+     ```+   - With `stack`:+     ```+     stack install --stack-yaml=stack-$GHCVER.yaml+     ```++   Note that the respective installation directory should be on your PATH.  ## Examples
+ main/Main.hs view
@@ -0,0 +1,5 @@+{-# LANGUAGE NoImplicitPrelude #-}++module Main (module X) where++import MainLib as X (main)
src/Abstract.hs view
@@ -13,14 +13,15 @@ import Prelude hiding (showList, map, concat, foldl, pi, null, (<>))  #if !MIN_VERSION_base(4,8,0)-import Control.Applicative hiding (empty)+import Control.Applicative (Applicative, pure, (<*>), (<$>)) #endif import Control.Monad.Writer (Writer, tell) import Control.Monad.Trans  import Control.Arrow (first)-import Data.Monoid hiding ((<>))+import Data.Monoid (All(..)) #if !MIN_VERSION_base(4,8,0)+import Data.Monoid (mempty, mconcat) import Data.Foldable (Foldable, foldMap) import Data.Traversable (Traversable) #endif@@ -220,6 +221,7 @@ paramDec = Dec Param defaultDec = Dec defaultPol -- defaultDec = paramDec -- TODO: Dec { polarity = Rec }+ defaultUpperDec :: Decoration PProd defaultUpperDec = Dec $ pprod SPos   -- a variable may not be erased and its polarity must be below SPos@@ -338,17 +340,15 @@ leqSizeE (Succ e) (Succ e') = leqSizeE e e' leqSizeE Infty _ = False --- plus :: Expr -> Expr -> Expr- -- sorts -------------------------------------------------------------  data Class   = Tm      -- sort of terms, only needed for erasure---  | Ty    -- use Set 0!  -- sort of type(constructor)s, only needed for erasure---  | Ki      -- sort of kinds  -- use Set 0 ... for mor precision+  -- -- | Ty    -- use Set 0!  -- sort of type(constructor)s, only needed for erasure+  -- -- | Ki      -- sort of kinds  -- use Set 0 ... for mor precision   | Size    -- sort of sizes   | TSize   -- sort of Size-  -- | Type    -- no longer used+  -- -- | Type    -- no longer used     deriving (Eq, Ord, Show)  predClass :: Class -> Class@@ -371,11 +371,11 @@ -}  instance Show (Sort Expr) where-  show (SortC c) = show c-  show (Set Zero) = "Set"+  show (SortC c)     = show c+  show (Set Zero)    = "Set"   show (CoSet Infty) = "Set"-  show (Set e) = Util.parens $ ("Set " ++ show e)-  show (CoSet e) = Util.parens $ ("CoSet " ++ show e)+  show (Set e)       = Util.parens $ ("Set " ++ show e)+  show (CoSet e)     = Util.parens $ ("CoSet " ++ show e)  topSort :: Sort Expr topSort = Set Infty@@ -421,8 +421,8 @@ minClass Size _ = Size minClass _ Size = Size minClass TSize TSize = TSize-maxClass :: Class -> Class -> Class +maxClass :: Class -> Class -> Class maxClass Tm c = c maxClass c Tm = c maxClass Size c = c@@ -444,7 +444,7 @@ leSort s s'   = s == s' -} --- s `irrSortFor` s' if a variable of kind s cannot compuationally+-- s `irrSortFor` s' if a variable of kind s cannot computationally -- contribute to produce a value of kind s' irrSortFor :: Sort Expr -> Sort Expr -> Bool irrSortFor (SortC Tm) _          = False -- terms matter for terms and everything@@ -604,15 +604,6 @@   getPol = getPol . getDec   mapPol = mapDec . mapPol -{--instance Functor Dom where-  fmap f dom = dom { typ = f (typ dom) }---- traverse :: Applicative f => (a -> f b) -> t a -> f (t b)-instance Traversable Dom where-  traverse f dom = (\ ty -> dom { typ = ty }) <$> f (typ dom)--}- -- identifiers -------------------------------------------------------  -- |@@ -943,7 +934,7 @@   The whole pattern is not irrefutable, but still you want the pair destructed   lazily by projections. -}---  | IrrP -- pattern which got erased+-- --  | IrrP -- pattern which got erased                deriving (Eq,Ord)  {-@@ -1846,7 +1837,7 @@     (Var name            , []) -> Set.singleton name     (Def (DefId DatK{} _), es) -> injectiveVars es     (Def (DefId ConK{} _), es) -> injectiveVars es-    (Record ri rs        , []) -> Set.unions $ List.map (injectiveVars . snd) rs+    (Record _ri rs       , []) -> Set.unions $ List.map (injectiveVars . snd) rs     (Succ e              , []) -> injectiveVars e     (Lam _ x e           , []) -> Set.delete x (injectiveVars e)     (Quant _ ta b , []) -> injectiveVars ta `Set.union` (injectiveVars b Set.\\ boundVars ta)@@ -1858,7 +1849,7 @@     _                         -> Set.empty  classifyFields :: Co -> Name -> Type -> [FieldInfo]-classifyFields co dataName ty = List.map (classifyField fvs) $ telescope tele+classifyFields _co _19dataName ty = List.map (classifyField fvs) $ telescope tele   where (tele, core) = typeToTele ty         fvs = freeVars core         ivs = injectiveVars core@@ -1975,7 +1966,7 @@ reassembleConstructorType ci = buildPi (cFields ci) where   buildPi [] = cTyCore ci   buildPi (f:fs) = pi (TBind (fName f) $ Domain (fType f) defaultKind (decor (fDec f) (fClass f))) $ buildPi fs-    where decor dec Index = irrelevantDec -- DONE: SWITCH ON!+    where decor _   Index = irrelevantDec -- DONE: SWITCH ON!           decor dec _     = dec  -- Pattern inductive families ----------------------------------------@@ -1997,7 +1988,7 @@ --   Gamma -> D ps -- and returns the list ps of patterns if it is the case isPatIndFamC :: Expr -> Writer All [Pattern]-isPatIndFamC (Def id) = return []+isPatIndFamC (Def _) = return [] isPatIndFamC (App f e) = do   ps <- isPatIndFamC f   p  <- exprToDotPat' e@@ -2015,30 +2006,30 @@ -- TreeShapedOrder tsoFromPatterns :: [Pattern] -> TSO Name tsoFromPatterns ps = TSO.fromList $ List.concat $ List.map loop ps where-  loop (SizeP (Var father) son) = [(son,(1,father))]+  loop (SizeP (Var father) son)        = [(son,(1,father))]   loop (SizeP (Succ (Var father)) son) = [(son,(0,father))]-  loop (SizeP e      son) = []-  loop (ConP _ _ ps)      = List.concat $ List.map loop ps-  loop (PairP p p')       = loop p ++ loop p'-  loop (SuccP   p)        = loop p-  loop (ErasedP p)        = loop p-  loop ProjP{}            = []-  loop VarP{}             = []-  loop DotP{}             = []-  loop UnusableP{}        = []+  loop (SizeP{})                       = []+  loop (ConP _ _ ps)                   = List.concat $ List.map loop ps+  loop (PairP p p')                    = loop p ++ loop p'+  loop (SuccP   p)                     = loop p+  loop (ErasedP p)                     = loop p+  loop ProjP{}                         = []+  loop VarP{}                          = []+  loop DotP{}                          = []+  loop UnusableP{}                     = []  -- for non-dot patterns, patterns overlap if one matches against the other -- infinity size is represented as (DotP Infty) -- I reprogram it here, since it does not need a monad overlap :: Pattern -> Pattern -> Bool-overlap (VarP _) p' = True-overlap p (VarP _)  = True+overlap (VarP _) _ = True+overlap _ (VarP _) = True overlap (ConP _ c ps) (ConP _ c' ps') = c == c' && overlaps ps ps' -- only source of non-overlap overlap (PairP p1 p2) (PairP p1' p2') = overlaps [p1,p2] [p1',p2'] overlap (ProjP n) (ProjP n') = n == n' -- another source of non-overlap -- size patterns always overlap-overlap (SuccP p) _ = True-overlap _ (SuccP p) = True+overlap (SuccP _) _ = True+overlap _ (SuccP _) = True overlap SizeP{} _   = True overlap _ SizeP{}   = True -- dot patterns always overlap (safe approximation)@@ -2103,7 +2094,7 @@  patternToExpr :: Pattern -> Expr patternToExpr (VarP n)       = Var n-patternToExpr (SizeP m n)    = Var n+patternToExpr (SizeP _m n)   = Var n patternToExpr (ConP pi n ps) = List.foldl App (con (coPat pi) n) (List.map patternToExpr ps) -- patternToExpr (ConP co n ps) = Con co n `App` (List.map patternToExpr ps) patternToExpr (PairP p p')   = Pair (patternToExpr p) (patternToExpr p')@@ -2146,7 +2137,7 @@  isSuccessor :: Expr -> Bool isSuccessor (Ann e)  = isSuccessor (unTag e)-isSuccessor (Succ e) = True+isSuccessor (Succ _) = True isSuccessor _        = False  shallowSuccP :: Pattern -> Bool@@ -2186,7 +2177,7 @@       ttt :: Int -> Type -> [TBind] -> ([TBind], Type) --      ttt k (Quant Pi htel tb t2) tel | k /= 0 = ttt (k-1) t2 (telescope htel ++ tb : tel)       ttt k (Quant Pi tb t2) tel | k /= 0 = ttt (k-1) t2 (tb : tel)-      ttt k t tel = (reverse tel, t)+      ttt _ t tel = (reverse tel, t)  ---- modification
src/Concrete.hs view
@@ -5,13 +5,13 @@ import Prelude hiding (null)  import Util-import Abstract (Co,Sized,PiSigma(..),Decoration(..),Dec,Override(..),Measure(..),Bound(..),HasPred(..),LtLe(..),polarity)-import qualified Abstract as A+import Abstract+  (Co, Sized, PiSigma(..), Dec, Override(..), Measure(..), Bound(..), HasPred(..), LtLe(..), polarity) import Polarity  -- | Concrete names. data Name = Name { theName :: String }-  deriving (Eq,Ord)+  deriving (Eq, Ord)  instance Show Name where   show (Name n) = n@@ -20,15 +20,19 @@ data QName   = Qual  { qual :: Name, name :: Name }  -- ^ @X.x@ e.g. qualified constructor.   | QName { name :: Name }                -- ^ @x@.-  deriving (Eq,Ord)+  deriving (Eq, Ord) +unqual :: QName -> Name unqual (QName n) = n  instance Show QName where   show (Qual m n) = show m ++ "." ++ show n   show (QName n)  = show n +set0 :: Expr set0 = Set Zero++ident :: Name -> Expr ident n = Ident (QName n)  -- | Concrete expressions syntax.@@ -236,6 +240,7 @@ prettyTel :: Bool -> Telescope -> String prettyTel inPi = Util.showList " " (prettyTBind inPi) +prettyMaybeType :: Maybe Expr -> String prettyMaybeType = maybe "" $ \ t -> " : " ++ prettyExpr t  prettyExpr :: Expr -> String@@ -269,8 +274,10 @@       Quant pisig tel t2 -> parens $ prettyTel True tel                                   ++ " " ++ show pisig ++ " " ++ prettyExpr t2 +prettyRecordLine :: ([Name], Expr) -> String prettyRecordLine (xs, e) = Util.showList " " show xs ++ " = " ++ prettyExpr e +prettyCase :: Clause -> String prettyCase (Clause Nothing [p] Nothing)  = prettyPattern p prettyCase (Clause Nothing [p] (Just e)) = prettyPattern p ++ " -> " ++ prettyExpr e @@ -287,6 +294,7 @@ prettyExprs :: [Expr] -> String prettyExprs = Util.showList " " prettyExpr +prettyDecl :: Declaration -> String prettyDecl (PatternDecl n ns p) = "pattern " ++ (Util.showList " " show (n:ns)) ++ " = " ++ prettyPattern p  teleToType :: Telescope -> Type -> Type
src/Eval.hs view
@@ -2,6 +2,8 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE CPP #-} +{-# OPTIONS_GHC -fno-warn-orphans #-}+ -- Activate this flag if i < $i should only hold for i < #. -- #define STRICTINFTY @@ -9,24 +11,25 @@  import Prelude hiding (mapM, null, pi) +#if !MIN_VERSION_base(4,8,0) import Control.Applicative+#endif import Control.Monad          hiding (mapM) import Control.Monad.State    (StateT, execStateT, get, gets, put) import Control.Monad.Except   (runExcept, MonadError) import Control.Monad.Reader   (asks, local)  import qualified Data.Array as Array-import Data.Maybe -- fromMaybe-import Data.Monoid hiding ((<>))-import Data.List (find) import qualified Data.List as List-import Data.Map (Map) import qualified Data.Map as Map+#if !MIN_VERSION_base(4,8,0) import Data.Foldable (foldMap)-import Data.Traversable (Traversable, mapM, traverse)-import qualified Data.Traversable as Traversable+import Data.Monoid+import Data.Traversable (traverse)+#endif+import Data.Traversable (mapM) -import Debug.Trace (trace)+-- import Debug.Trace (trace)  import Abstract import Polarity as Pol@@ -39,6 +42,8 @@ import TraceError import Util +traceEta, traceRecord, traceMatch, traceLoop, traceSize :: String -> a -> a+traceEtaM, traceRecordM, traceMatchM, traceLoopM, traceSizeM :: Monad m => String -> m ()  traceEta msg a = a -- trace msg a traceEtaM msg = return () -- traceM msg@@ -114,7 +119,7 @@   reval = reval' emptyVal  instance Reval a => Reval (Maybe a) where-  reval' valu ma = Traversable.traverse (reval' valu) ma+  reval' valu ma = traverse (reval' valu) ma  instance Reval b => Reval (a,b) where   reval' valu (x,v) = (x,) <$> reval' valu v@@ -134,10 +139,10 @@     reval' valu valu'  instance Reval a => Reval (Measure a) where-  reval' valu beta = Traversable.traverse (reval' valu) beta+  reval' valu beta = traverse (reval' valu) beta  instance Reval a => Reval (Bound a) where-  reval' valu beta = Traversable.traverse (reval' valu) beta+  reval' valu beta = traverse (reval' valu) beta  instance Reval Val where   reval' valu u = traceLoop ("reval " ++ show u) $ do@@ -177,11 +182,11 @@       VGuard beta v         -> VGuard <$> reval beta <*> reval v       VQuant pisig x dom fv ->         VQuant pisig x-          <$> Traversable.mapM reval dom+          <$> mapM reval dom           <*> reFun fv     {-       VQuant pisig x dom env b -> do-        dom' <- Traversable.mapM reval dom+        dom' <- mapM reval dom         env' <- reEnv env         return $ VQuant pisig x dom' env' b     -}@@ -284,6 +289,7 @@ equals' (w1:vs1) (w2:vs2) = (equal' w1 w2) `andLazy` (equals' vs1 vs2) equals' vl1 vl2           = return False +equal' :: Val -> Val -> TypeCheck Bool equal' w1 w2 = whnfClos w1 >>= \ v1 -> equal v1 =<< whnfClos w2  {- LEADS TO NON-TERMINATION@@ -317,7 +323,7 @@     (VSort s)            -> return $ Sort $ vSortToSort s     (VBelow ltle v)      -> Below ltle <$> reify v     (VQuant pisig x dom fv) -> do-          dom' <- Traversable.mapM reify dom+          dom' <- mapM reify dom           underAbs_ x dom fv $ \ k xv vb -> do             let x' = unsafeName (suggestion x ++ "~" ++ show k)             piSig pisig (TBind x' dom') <$> reify vb@@ -538,12 +544,12 @@     Lam dec x e1 -> return $ vLam x env e1     Below ltle e -> VBelow ltle <$> whnf env e     Quant pisig (TBind x dom) b -> do-      dom' <- Traversable.mapM (whnf env) dom  -- Pi is strict in its first argument+      dom' <- mapM (whnf env) dom  -- Pi is strict in its first argument       return $ VQuant pisig x dom' $ vLam x env b      -- a measured type evaluates to-    -- * a bounded type if measure present in environment (rhs of funs)-    -- * otherwise to a measured type (lhs of funs)+    -- - a bounded type if measure present in environment (rhs of funs)+    -- - otherwise to a measured type (lhs of funs)     Quant Pi (TMeasure mu) b -> do       muv <- whnfMeasure env mu       bv  <- whnf env b -- not adding measure constraint to context!@@ -690,6 +696,7 @@ piApps tv (v:vs) = do tv' <- piApp tv v                       piApps tv' vs +updateValu :: Valuation -> Int -> Val -> TypeCheck Valuation updateValu valu i v = reval' (sgVal i v) valu  -- in app u v, u might be a VDef (e.g. when coming from reval)@@ -1239,7 +1246,7 @@     -- Here, we need the type!     matchVarP x v = do       let env = fst st-      case find ((x ==) . fst) $ envMap $ fst st of+      case List.find ((x ==) . fst) $ envMap $ fst st of         Nothing     -> return $ Just $ mapFst (\ env -> update env x v) st         Just (y,v') -> ifM (eqValBool tv v v') (return $ Just st) (return Nothing) @@ -1446,6 +1453,7 @@   | ShCoSet (OneOrTwo Val)     -- CoSet i and CoSet j     deriving (Eq, Ord) +shSize :: TypeShape shSize = ShSort (ShSortC Size)  -- typeView does not normalize!@@ -1497,10 +1505,10 @@     _ -> throwErrorMsg $ "sort " ++ show s1 ++ " has different shape than " ++ show s2  whnf12 :: OneOrTwo Env -> OneOrTwo Expr -> TypeCheck (OneOrTwo Val)-whnf12 env12 e12 = Traversable.traverse id $ zipWith12 whnf env12 e12+whnf12 env12 e12 = traverse id $ zipWith12 whnf env12 e12  app12 ::  OneOrTwo Val -> OneOrTwo Val -> TypeCheck (OneOrTwo Val)-app12 fv12 v12 = Traversable.traverse id $ zipWith12 app fv12 v12+app12 fv12 v12 = traverse id $ zipWith12 app fv12 v12  -- if m12 = Nothing, we are checking subtyping, otherwise we are -- comparing objects or higher-kinded types@@ -1604,8 +1612,8 @@                  case mt12 of                    Nothing -> recoverFail $ "leqVal': cannot compare constructor terms without type"                    Just tv12 -> do-                     ct12 <- Traversable.mapM (conType n1) tv12-                     leqVals' f p ct12 vl1 vl2+                     ct12 <- mapM (conType n1) tv12+                     _ <- leqVals' f p ct12 vl1 vl2                      return () {-        leqStructural u1 u2 where@@ -1910,7 +1918,7 @@        (VGen k1, VGen k2) | k1 == k2 -> do         tv12 <- (fmap typ . domain) <$> lookupGen k1-        leqVals' f pol tv12 w1 w2+        _ <- leqVals' f pol tv12 w1 w2         return () {-       (VGen k1, VGen k2) ->@@ -1934,7 +1942,7 @@        (VDef n, VDef m) | n == m ->  do         tv <- lookupSymbTypQ (idName n)-        leqVals' f pol (One tv) w1 w2+        _ <- leqVals' f pol (One tv) w1 w2         return ()        -- check for least or greatest type@@ -2290,8 +2298,8 @@   case pol of     _ | pol == mixed -> do       assert (ltle1 == ltle2) $ "unequal bound types"-      zipWithM (leqSize mixed) mu1  mu2-      zipWithM (leqSize mixed) mu1' mu2'+      zipWithM_ (leqSize mixed) mu1  mu2+      zipWithM_ (leqSize mixed) mu1' mu2'       return ()     Pos | ltle1 == Lt || ltle2 == Le  -> do       lexSizes Le mu2  mu1  -- not strictly smaller
src/Extract.hs view
@@ -150,18 +150,15 @@  import Prelude hiding (pi, null) -import Control.Applicative-import Control.Monad-import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.Writer-import Control.Monad.State+#if !MIN_VERSION_base(4,8,0)+import Control.Applicative ((<$>), (<*>))+#endif+import Control.Monad.Except (runExceptT)+import Control.Monad.Reader (runReaderT)+import Control.Monad.State  (runStateT) -import Data.Char-import Data.Traversable (Traversable)+-- import Data.Char import qualified Data.Traversable as Traversable-import Data.Map (Map)-import qualified Data.Map as Map import qualified Data.Maybe as Maybe  import Text.PrettyPrint@@ -174,8 +171,10 @@ import TraceError import Util +traceExtrM :: Monad m => String -> m () traceExtrM s = return () +runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState)) runExtract sig k = runExceptT (runReaderT (runStateT k (initWithSig sig)) emptyContext)  -- extraction
src/HsSyntax.hs view
@@ -1,5 +1,7 @@ {- 2010-09-17 haskell syntax tools -} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+ module HsSyntax where  import Abstract (PiSigma(..))
src/Lexer.x view
@@ -4,7 +4,7 @@ {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-} {-# OPTIONS_GHC -fno-warn-unused-matches #-} -module Lexer where+module Lexer (AlexPosn, Token(..), alexScanTokens, prettyTok) where  }
+ src/License.hs view
@@ -0,0 +1,35 @@+-- This file was autogenerated from LICENSE, do not edit!!++{-# LANGUAGE QuasiQuotes #-}++module License where++import Data.String.QQ++copyright :: String+copyright = head (lines license)++license :: String+license = [s|+Copyright (c) 2007-2014 Andreas Abel and Karl Mehltretter.++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be+included in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.++|]
− src/Main.hs 
@@ -1,137 +0,0 @@-module Main where--import Prelude hiding (null)--import System.Environment-import System.Exit-import System.IO (stdout, hSetBuffering, BufferMode(..))--import qualified Language.Haskell.Exts.Syntax as H-import qualified Language.Haskell.Exts.Pretty as H--import Lexer-import Parser--import qualified Concrete as C-import qualified Abstract as A-import Abstract (Name)-import ScopeChecker-import Value-import TCM-import TypeChecker-import Extract-import ToHaskell--import Util--main :: IO ()-main = do-  hSetBuffering stdout NoBuffering-  putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"-  args <- getArgs-  mapM_ mainFile args--mainFile :: String -> IO ()-mainFile fileName = do-  putStrLn $ "--- opening " ++ show fileName ++ " ---"-  file <- readFile fileName-  let t = alexScanTokens file-  let cdecls =  parse t-  -- putStrLn "--- parsing ---"-  -- mapM (putStrLn . show) cdecls-  putStrLn "--- scope checking ---"-  adecls <- doScopeCheck cdecls-  -- mapM (putStrLn . show) adecls-  putStrLn "--- type checking ---"-  (edecls, sig) <- doTypeCheck adecls-  putStrLn "--- evaluating ---"-  showAll sig adecls-{--  putStrLn "--- extracting ---"-  edecls <- doExtract sig edecls-  hsmodule <- doTranslate edecls-  putStrLn $ H.prettyPrint hsmodule-  -- printHsDecls hsdecls--}-  putStrLn $ "--- closing " ++ show fileName ++ " ---"---- print extracted program--ppHsMode :: H.PPHsMode-ppHsMode = H.PPHsMode  -- H.defaultMode-  { H.classIndent  = 2-  , H.doIndent     = 3-  , H.multiIfIndent = 3-  , H.caseIndent   = 3-  , H.letIndent    = 4-  , H.whereIndent  = 2-  , H.onsideIndent = 1-  , H.spacing      = False-  , H.layout       = H.PPOffsideRule-  , H.linePragmas  = False-  }--printHsDecls :: [H.Decl ()] -> IO ()-printHsDecls hs = mapM_ (putStrLn . H.prettyPrintWithMode ppHsMode) hs---- all let declarations-allLet :: Signature -> [A.Declaration] -> [(Name,A.Expr)]-allLet sig [] = []-allLet sig (decl:xs) =-    case decl of-      (A.LetDecl True n tel _ e) | null tel ->-          (n,e):(allLet sig xs)-      _ -> allLet sig xs---showAll :: Signature -> [A.Declaration] -> IO ()-showAll sig decl = mapM_ (showLet sig) $ allLet sig decl--showLet :: Signature -> (Name,A.Expr) -> IO ()-showLet sig (n,e) = do-  r <- doWhnf sig e-  case r of-    Right (v,_) -> putStrLn $ show n ++ " has whnf " ++ show v-    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err-                      exitFailure-  r <- doNf sig e-  case r of-    Right (v,_) -> putStrLn $ show n ++ " evaluates to " ++ show v-    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err-                      exitFailure--doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]-doExtract sig decls = do-  k <- runExtract sig $ extractDecls decls-  case k of-    Left err -> do-      putStrLn $ "error during extraction:\n" ++ show err-      exitFailure-    Right (hs, _) ->-      return hs--doTranslate :: [A.EDeclaration] -> IO (H.Module ())-doTranslate decls = do-  k <- runTranslate $ translateModule decls-  case k of-    Left err -> do-      putStrLn $ "error during extraction:\n" ++ show err-      exitFailure-    Right hs ->-      return hs--doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)-doTypeCheck decls = do-  k <- typeCheck decls-  case k of-    Left err -> do-      putStrLn $ "error during typechecking:\n" ++ show err-      exitFailure-    Right (edecls, st) ->-      return (edecls, signature st)--doScopeCheck :: [C.Declaration] -> IO [A.Declaration]-doScopeCheck decl = case scopeCheck decl of-     Left err -> do putStrLn $ "scope check error: " ++ show err-                    exitFailure-     Right (decl',_) -> return $ decl'
+ src/MainLib.hs view
@@ -0,0 +1,138 @@+module MainLib where++import Prelude hiding (null, mapM_)++import Data.Foldable (mapM_)++import System.Exit+import System.IO (stdout, hSetBuffering, BufferMode(..))++import qualified Language.Haskell.Exts.Syntax as H+import qualified Language.Haskell.Exts.Pretty as H++import Lexer+import Parser+import Options++import qualified Concrete as C+import qualified Abstract as A+import Abstract (Name)+import ScopeChecker+import TCM+import TypeChecker+import Extract+import ToHaskell++import Util++main :: IO ()+main = do+  hSetBuffering stdout NoBuffering+  -- putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"+  opts <- options+  mapM_ mainFile $ optInputs opts++mainFile :: String -> IO ()+mainFile fileName = do+  putStrLn $ "--- opening " ++ show fileName ++ " ---"+  file <- readFile fileName+  let t = alexScanTokens file+  let cdecls =  parse t+  -- putStrLn "--- parsing ---"+  -- mapM (putStrLn . show) cdecls+  putStrLn "--- scope checking ---"+  adecls <- doScopeCheck cdecls+  -- mapM (putStrLn . show) adecls+  putStrLn "--- type checking ---"+  (edecls, sig) <- doTypeCheck adecls+  putStrLn "--- evaluating ---"+  showAll sig adecls+{-+  putStrLn "--- extracting ---"+  edecls <- doExtract sig edecls+  hsmodule <- doTranslate edecls+  putStrLn $ H.prettyPrint hsmodule+  -- printHsDecls hsdecls+-}+  putStrLn $ "--- closing " ++ show fileName ++ " ---"++-- print extracted program++ppHsMode :: H.PPHsMode+ppHsMode = H.PPHsMode  -- H.defaultMode+  { H.classIndent  = 2+  , H.doIndent     = 3+  , H.multiIfIndent = 3+  , H.caseIndent   = 3+  , H.letIndent    = 4+  , H.whereIndent  = 2+  , H.onsideIndent = 1+  , H.spacing      = False+  , H.layout       = H.PPOffsideRule+  , H.linePragmas  = False+  }++printHsDecls :: [H.Decl ()] -> IO ()+printHsDecls hs = mapM_ (putStrLn . H.prettyPrintWithMode ppHsMode) hs++-- all let declarations+allLet :: Signature -> [A.Declaration] -> [(Name,A.Expr)]+allLet sig [] = []+allLet sig (decl:xs) =+    case decl of+      (A.LetDecl True n tel _ e) | null tel ->+          (n,e):(allLet sig xs)+      _ -> allLet sig xs+++showAll :: Signature -> [A.Declaration] -> IO ()+showAll sig decl = mapM_ (showLet sig) $ allLet sig decl++showLet :: Signature -> (Name,A.Expr) -> IO ()+showLet sig (n,e) = do+  r <- doWhnf sig e+  case r of+    Right (v,_) -> putStrLn $ show n ++ " has whnf " ++ show v+    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err+                      exitFailure+  r <- doNf sig e+  case r of+    Right (v,_) -> putStrLn $ show n ++ " evaluates to " ++ show v+    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err+                      exitFailure++doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]+doExtract sig decls = do+  k <- runExtract sig $ extractDecls decls+  case k of+    Left err -> do+      putStrLn $ "error during extraction:\n" ++ show err+      exitFailure+    Right (hs, _) ->+      return hs++doTranslate :: [A.EDeclaration] -> IO (H.Module ())+doTranslate decls = do+  k <- runTranslate $ translateModule decls+  case k of+    Left err -> do+      putStrLn $ "error during extraction:\n" ++ show err+      exitFailure+    Right hs ->+      return hs++doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)+doTypeCheck decls = do+  k <- typeCheck decls+  case k of+    Left err -> do+      putStrLn $ "error during typechecking:\n" ++ show err+      exitFailure+    Right (edecls, st) ->+      return (edecls, signature st)++doScopeCheck :: [C.Declaration] -> IO [A.Declaration]+doScopeCheck decl = case scopeCheck decl of+     Left err -> do putStrLn $ "scope check error: " ++ show err+                    exitFailure+     Right (decl',_) -> return $ decl'
src/Makefile view
@@ -17,6 +17,37 @@ default : Main test all : Main test examples lib +# Generate License.hs+#####################++.PHONY: license++license: License.hs++License.hs : ../LICENSE Makefile+	echo "\+-- This file was autogenerated from LICENSE, do not edit!!\n\n\+{-# LANGUAGE QuasiQuotes #-}\n\n\+module License where\n\n\+import Data.String.QQ\n\n\+copyright :: String\n\+copyright = head (lines license)\n\n\+license :: String\n\+license = [s|" > $@+	cat $< >> $@+	echo "\n|]" >> $@++# Generate emacs tags+#####################++.PHONY: TAGS++TAGS :+	hasktags -e *.hs++# Building+##########+ prof-current : miniagda-prof 	miniagda-prof ../examples/FiCS12/fics12-06.ma +RTS -prof -s #	miniagda-prof ../test/succeed/Zero.ma +RTS -prof -s@@ -74,6 +105,9 @@ %arser.hs : %arser.y Lexer.hs 	happy --info=$<-grm.txt $< +# Testing+#########+ test : Main succeed fail  succeed :@@ -100,6 +134,8 @@ 	@echo "======================================================================" 	make -C ../lib +# Cleaning+##########  clean : 	-rm *.o *.hi Main miniagda-prof
+ src/Options.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE CPP #-}++-- | Options given to @MiniAgda@.++module Options where++#if !MIN_VERSION_base(4,11,0)+import Data.Semigroup               ( (<>) )+#endif++import Options.Applicative+import Options.Applicative.NonEmpty ( some1 )++import System.Environment           ( getArgs )++import License                      ( copyright, license )+import Util+import Version                      ( version )++-- | Options given to @MiniAgda@.+data Options = Options+  { optInputs :: List1 FilePath+      -- ^ The source files to type check, from first to last.+  }++self :: String+self = "MiniAgda"++-- | Parse the options given on the command line.+options :: IO Options+options = handleParseResult =<< do parseOptions <$> getArgs++-- | Pure parser for command line given by a list of strings.+parseOptions :: [String] -> ParserResult Options+parseOptions = execParserPure defaultPrefs $ info parser description+  where+  parser = theOptions <**>+    (versionOption <*> numericVersionOption <*> licenseOption <*> helper)++  description = header top <> footer bot+  top = unwords+    [ concat [ self, ":" ]+    , "A prototypical dependently typed pure language with sized types."+    ]+  bot = unwords+    [ "Checks the given MiniAgda files in first-to-last order."+    , "Later files can refer to definitions made in earlier files."+    ]++  versionOption =+    infoOption versionLong+      $  long "version"+      <> short 'V'+      <> help "Show version info."+      <> hidden+  versionText = unwords [ self, "version", version ]+  versionLong = intercalate "\n" $+    [ versionText+    , copyright+    , "This is free software under the MIT license."+    ]++  numericVersionOption =+    infoOption version+      $  long "numeric-version"+      <> help "Show just version number."+      <> hidden++  licenseOption =+    infoOption license+      $  long "license"+      <> help "Show the license text."+      <> hidden++  theOptions = Options+    <$> oInputs++  oInputs :: Parser (List1 FilePath)+  oInputs = some1 $+    strArgument+      $  metavar "FILES"+      <> action "file"+      <> help "Files to check (in first-to-last order)."
src/Parser.y view
@@ -1,6 +1,6 @@ { {-# LANGUAGE BangPatterns #-}-module Parser where+module Parser (parse) where  import qualified Lexer as T import qualified Concrete as C
src/PrettyTCM.hs view
@@ -1,6 +1,8 @@ {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-# LANGUAGE NoImplicitPrelude #-} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+ module PrettyTCM where  import Prelude hiding (sequence, mapM, (<>))@@ -11,7 +13,9 @@ import qualified Util import Value -import Control.Applicative hiding (empty)+#if !MIN_VERSION_base(4,8,0)+import Control.Applicative ((<$>), (<*>))+#endif import Control.Monad ((<=<)) import Data.Traversable
src/ScopeChecker.hs view
@@ -5,11 +5,15 @@       FlexibleContexts, FlexibleInstances, UndecidableInstances,       MultiParamTypeClasses #-} +{-# OPTIONS_GHC -fno-warn-missing-signatures #-}+ module ScopeChecker (scopeCheck) where  import Prelude hiding (mapM, null) +#if !MIN_VERSION_base(4,8,0) import Control.Applicative+#endif import Control.Monad          hiding (mapM) import Control.Monad.Identity (Identity, runIdentity) import Control.Monad.Reader   (ReaderT, runReaderT, MonadReader, ask, asks, local)@@ -22,11 +26,14 @@ import Data.Maybe import Data.Traversable (mapM) -import Debug.Trace+-- import Debug.Trace  import Polarity(Pol(..)) import qualified Polarity as A-import Abstract (Sized,mkExtRef,Co,ConK(..),PrePost(..),MVar,Decoration(..),Override(..),Measure(..),adjustTopDecsM,Arity,polarity,LensPol(..))+import Abstract+  ( Sized, Co, ConK(..), PrePost(..), MVar, Override(..), Measure(..), adjustTopDecsM+  , Arity, polarity, LensPol(..)+  ) import qualified Abstract as A import qualified Concrete as C @@ -34,13 +41,13 @@  import Util --- * scope checker--- check that all identifiers are in scope and global identifiers are only used once--- replaces Ident with Con, Def, Let or Var--- replaces IdentP with ConP or VarP in patterns--- replaces Unknown by a new Meta-Variable--- check pattern length is equal in each clause--- group mutual declarations+-- * Scope checker.+-- - check that all identifiers are in scope and global identifiers are only used once+-- - replaces Ident with Con, Def, Let or Var+-- - replaces IdentP with ConP or VarP in patterns+-- - replaces Unknown by a new Meta-Variable+-- - check pattern length is equal in each clause+-- - group mutual declarations  -- | Entry point for scope checker. scopeCheck :: [C.Declaration] -> Either TraceError ([A.Declaration],SCState)@@ -145,6 +152,7 @@   , nextPolVar :: MVar   } +initSt :: SCState initSt = SCState emptySig 0 0  -- * The scope checking monad.@@ -539,7 +547,7 @@ addFields :: IKind -> Context -> [C.Name] -> ScopeCheck [A.Name] addFields kind delta cfields = do     afields <- mapM (scopeCheckField delta) cfields-    mapM (uncurry $ addANameU kind) $ zip cfields afields+    mapM_ (uncurry $ addANameU kind) $ zip cfields afields     return afields  scopeCheckDataDecl :: C.Declaration -> ScopeCheck A.Declaration@@ -608,12 +616,12 @@   --let addFuns b = mapM (uncurry $ addAName $ FunK b) nxs --  let addFuns b = mapM (\ (n,x) -> addAName (FunK b) n x) nxs   -- addFuns False-  mapM (uncurry $ addANameU $ FunK False) nxs+  mapM_ (uncurry $ addANameU $ FunK False) nxs   arcll' <- mapM (setDefaultPolarity A.Rec . scopeCheckFunClauses) l   -- add names as external ids   --addFuns True   let nxs' = map (mapPair id A.mkExtName) nxs-  mapM (uncurry $ addANameU (LetK)) nxs'+  mapM_ (uncurry $ addANameU (LetK)) nxs' --  mapM (uncurry $ addAName (FunK True)) nxs'   return $ A.MutualFunDecl (isJust ml) co $     zipWith3 (\ ts (_, x') (ar, cls) -> A.Fun ts x' ar cls) tsl' nxs' arcll'
src/TCM.hs view
@@ -9,18 +9,18 @@ import Control.Monad.Except (ExceptT, MonadError) import Control.Monad.Reader (ReaderT, ask, asks, local) +#if !MIN_VERSION_base(4,8,0) import Control.Applicative import Data.Foldable (Foldable)-import qualified Data.Foldable as Foldable import Data.Traversable (Traversable)+#endif import qualified Data.Traversable as Traversable-import Data.Monoid  import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Maybe as Maybe -import Debug.Trace+-- import Debug.Trace  import Abstract import Polarity@@ -38,10 +38,14 @@  import Warshall +traceSig :: String -> a -> a -- traceSig msg a = trace msg a traceSig msg a = a +traceRew :: String -> a -> a traceRew msg a = a -- trace msg a++traceRewM :: Monad m => String -> m () traceRewM msg = return () -- traceM msg {- traceRew msg a = trace msg a@@ -50,7 +54,10 @@  -- metavariables and constraints +traceMeta :: String -> a -> a traceMeta msg a = a -- trace msg a++traceMetaM :: Monad m => String -> m () traceMetaM msg = return () -- traceM msg {- traceMeta msg a = trace msg a@@ -179,6 +186,7 @@ instance Show TCContext where     show ce = show (environ ce) ++ "; " ++ show (context ce) +emptyContext :: TCContext emptyContext = TCContext   { context  = cxtEmpty   , renaming = Map.empty@@ -211,6 +219,8 @@   }  type MetaVars = Map MVar MetaVar++emptyMetaVars :: MetaVars emptyMetaVars = Map.empty  type MScope = [Name] -- ^ names of size variables which are in scope of mvar@@ -221,6 +231,8 @@  type PosConstrnt = Constrnt PPoly DefId () type PositivityGraph = [PosConstrnt]++emptyPosGraph :: PositivityGraph emptyPosGraph = []  -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))@@ -276,6 +288,7 @@ data Rewrite  = Rewrite { lhs :: Val,  rhs :: Val } type Rewrites = [Rewrite] +emptyRewrites :: Rewrites emptyRewrites = []  instance Show Rewrite where@@ -349,6 +362,8 @@       (Map.elems (decs delta))     ) (Map.elems (upperDecs delta)) -}++cxtEmpty :: SemCxt cxtEmpty = SemCxt   { len = 0   , cxt = Map.empty@@ -431,15 +446,6 @@ cxtApplyDec dec delta = delta { upperDecs = Map.map (compDec dec) (upperDecs delta) } -- cxtApplyDec dec delta =  delta { decs = Map.map (fmap $ invCompDec dec) (decs delta) } -{- RETIRED, use cxtApplyDec instead--- clear all "erased" flags (see Pfenning, LICS 2001)--- UPDATE: resurrection sets "target" status to erased---         (as opposed to setting "source" status to non-erased)-cxtResurrect :: SemCxt -> SemCxt-cxtResurrect delta = delta { upperDecs = Map.map (\ dec -> dec { erased = True}) (upperDecs delta) }--- cxtResurrect delta = delta { decs = Map.map (fmap resurrectDec) (decs delta) }--}- -- manipulating the context ------------------------------------------  {-@@ -533,6 +539,7 @@   goImpredicative :: m a -> m a   checkingMutual :: Maybe DefId -> m a -> m a +dontCare :: a dontCare = error "Internal error: tried to retrieve unassigned type of variable"  instance MonadCxt TypeCheck where@@ -898,6 +905,7 @@ underAbs_  :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a underAbs_ x dom fv cont = noConsistencyChecking $ underAbs x dom fv cont +noConsistencyChecking :: TypeCheck a -> TypeCheck a noConsistencyChecking = local $ \ cxt -> cxt { consistencyCheck = False }  -- | No eta, no hypotheses.  First returned val is a @VGen i@.@@ -1006,10 +1014,10 @@ type Signature = Map QName SigDef  -- a signature entry is either--- * a fun/cofun,--- * a defined constant,--- * a constructor, or--- * a data type id with its kind+-- - a fun/cofun,+-- - a defined constant,+-- - a constructor, or+-- - a data type id with its kind -- they share "symbTyp", the type signature of the definition data SigDef   = FunSig  { isCo          :: Co@@ -1104,6 +1112,7 @@ symbKind DataSig{} = kType          -- data types are never universes -} +emptySig :: Signature emptySig = Map.empty  -- Handling constructor types  ------------------------------------------@@ -1383,12 +1392,12 @@     if any id bs then return Nothing else      throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)   mkConstraint w@(VMax vs) v = throwErrorMsg $ "cannot handle constraint " ++ show w ++ " <= " ++ show v-  mkConstraint (VMeta i rho n) (VMeta j rho' m) = retret $ arc (Flex i) (m-n) (Flex j)-  mkConstraint (VMeta i rho n) VInfty      = retret $ arc (Flex i) 0 (Rigid (RConst Infinite))-  mkConstraint (VMeta i rho n) v           = retret $ arc (Flex i) (m-n) (Rigid (RVar j))+  mkConstraint (VMeta i rho n) (VMeta j rho' m) = return $ Just $ arc (Flex i) (m-n) (Flex j)+  mkConstraint (VMeta i rho n) VInfty      = return $ Just $ arc (Flex i) 0 (Rigid (RConst Infinite))+  mkConstraint (VMeta i rho n) v           = return $ Just $ arc (Flex i) (m-n) (Rigid (RVar j))     where (j,m) = vGenSuccs v 0-  mkConstraint VInfty (VMeta i rho n)      = retret $ arc (Rigid (RConst Infinite)) 0 (Flex i)-  mkConstraint v (VMeta j rho m)           = retret $ arc (Rigid (RVar i)) (m-n) (Flex j)+  mkConstraint VInfty (VMeta i rho n)      = return $ Just $ arc (Rigid (RConst Infinite)) 0 (Flex i)+  mkConstraint v (VMeta j rho m)           = return $ Just $ arc (Rigid (RVar i)) (m-n) (Flex j)     where (i,n) = vGenSuccs v 0   mkConstraint v1 v2 = throwErrorMsg $ "mkConstraint undefined for " ++ show (v1,v2) @@ -1428,11 +1437,10 @@ nameOf ((x,VGen i):rho) j | i == j = Just x nameOf (_:rho) j = nameOf rho j +vGenSuccs :: Val -> Int -> (Int, Int) vGenSuccs (VGen k)  m = (k,m) vGenSuccs (VSucc v) m = vGenSuccs v (m+1) vGenSuccs v m = error $ "vGenSuccs fails on " ++ Util.parens (show v) ++ " " ++ show m--retret = return . return  sizeExprToExpr :: Env -> SizeExpr -> Expr sizeExprToExpr rho (SizeConst Infinite) = Infty
src/Termination.hs view
@@ -9,11 +9,9 @@  import qualified Data.List as List import Data.Monoid-import Data.Set (Set)-import qualified Data.Set as Set-import Data.Foldable (Foldable, foldMap)-import qualified Data.Foldable as Foldable-+#if !MIN_VERSION_base(4,8,0)+import Data.Foldable (foldMap)+#endif import Debug.Trace  --import System@@ -28,7 +26,10 @@ import TreeShapedOrder (TSO) import qualified TreeShapedOrder as TSO +traceTerm :: String -> a -> a traceTerm msg a = a -- trace msg a++traceTermM :: Monad m => String -> m () traceTermM msg = return () -- traceM msg {- traceTerm msg a = trace msg a@@ -36,7 +37,10 @@ -}  +traceProg :: String -> a -> a traceProg msg a =  a++traceProgM :: Monad m => String -> m () traceProgM msg = return () {- traceProg msg a = trace msg a@@ -336,6 +340,7 @@       ((Proj Post n1,[]), ProjP n2) | n1 == n2 -> Decr 0       _ -> Un +conView :: (Expr, [Expr]) -> (Expr, [Expr]) conView (Record (NamedRec co n _ _) rs, es) = (Def (DefId (ConK co) n), map snd rs ++ es) conView p = p @@ -495,11 +500,11 @@ type Progress = Writer Any type ProgressH = Writer (Any, Any) +firstHalf :: (Any, Any) firstHalf = (Any True, Any False)-secondHalf = (Any False, Any True) --- fullProgress = Sum 2--- halfProgress = Sum 1+secondHalf :: (Any, Any)+secondHalf = (Any False, Any True)  -- we keep CMSets always in normal form -- progress reported if m is "better" than one of ms@@ -711,11 +716,6 @@ groupCalls (n:nl) cl = (n, [ c | c <- cl , (source c == n) ]) : groupCalls nl cl -} -{--ccFunDecl :: [ ( TypeSig,[Clause]) ] -> [Call]-ccFunDecl funs = complete $ collectCGFunDecl funs--}- collectCGFunDecl :: (?cutoff :: Int) => [(Name,Arity)] -> [Fun] -> [Call] collectCGFunDecl names funs =       concatMap (collectClauses names) funs@@ -729,18 +729,6 @@                 (collectCallsExpr names n pl rhs) ++ (collectClause names n rest)             collectClause names n [] = [] -{- RETIRED-arity :: [Clause] -> Int-arity [] = 0-arity (Clause pl e:l) = length pl--}--{- RETIRED (map)-collectNames :: [Fun] -> [(Name,Arity)]-collectNames [] = []-collectNames (Fun (TypeSig n _) ar cls : rest) = (n,ar) : (collectNames rest)--}- -- | harvest i > j  from  case i { $ j -> ...} tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name tsoCase tso (Var x) [Clause _ [SuccP (VarP y)] _] = TSO.insert y (1,x) tso@@ -783,8 +771,8 @@              (loop tso e1) ++ -- type won't get evaluated              (loop tso e2)           (Quant _ tb@(TBind x dom) e2) -> (loop tso (typ dom)) ++ (loop (tsoBind tso tb) e2)-          (Quant _ (TMeasure mu) e2) -> Foldable.foldMap (loop tso) mu ++ (loop tso e2)-          (Quant _ (TBound beta) e2) -> Foldable.foldMap (loop tso) beta ++ (loop tso e2)+          (Quant _ (TMeasure mu) e2) -> foldMap (loop tso) mu ++ (loop tso e2)+          (Quant _ (TBound beta) e2) -> foldMap (loop tso) beta ++ (loop tso e2)           (Below ltle e) -> loop tso e           (Sing e1 e2) -> (loop tso e1) ++ (loop tso e2)           (Pair e1 e2) -> (loop tso e1) ++ (loop tso e2)@@ -800,7 +788,7 @@           Def{}   -> []           Irr{}   -> []           Proj{}   -> []-          Record ri rs -> Foldable.foldMap (loop tso . snd) rs+          Record ri rs -> foldMap (loop tso . snd) rs           Ann e1 -> loop tso (unTag e1) --          Con{}   -> [] --          Let{}   -> []
src/ToHaskell.hs view
@@ -43,19 +43,17 @@  import Data.Char -import Control.Applicative+#if !MIN_VERSION_base(4,8,0)+import Control.Applicative ((<$>), (<*>))+#endif import Control.Monad-import Control.Monad.Except-import Control.Monad.Reader-import Control.Monad.Writer-import Control.Monad.State+import Control.Monad.Except (ExceptT, runExceptT)+import Control.Monad.Reader (ReaderT, runReaderT)+import Control.Monad.State  (StateT, evalStateT) -import Data.Map (Map)-import qualified Data.Map as Map import qualified Data.Traversable as Trav  import qualified Language.Haskell.Exts.Syntax as Hs-import Text.PrettyPrint  import Polarity import Abstract
− src/Tokens.hs 
@@ -1,28 +0,0 @@-module Tokens where--data Token-  = Id String-  | Data-  | Fun-  | Def-  | Mutual-  | Pattern-  | Set-  | Case-  -- size type-  | Size-  | Infty-  | Succ-  ---  | BrOpen-  | BrClose-  | PrOpen-  | PrClose-  | Sem-  | Col-  | Arrow-  | Eq-  | Lam-  | UScore-  | NotUsed -- so happy doesn't generate overlap case pattern warning-    deriving (Eq,Ord,Show)
src/TraceError.hs view
@@ -1,8 +1,9 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}  module TraceError where -import Control.Monad.Except+import Control.Monad.Except   (MonadError, throwError, catchError) import Control.Monad.IO.Class (MonadIO(..)) import Debug.Trace @@ -63,10 +64,12 @@ boolToError msg False = throwErrorMsg msg  -- defined in Control.Monad.Error.Class in mtl-2.2.2--- instance MonadError () Maybe where---   catchError Nothing k = k ()---   catchError (Just a) k = Just a---   throwError () = Nothing+#if !MIN_VERSION_mtl(2,2,2)+instance MonadError () Maybe where+  catchError Nothing k = k ()+  catchError (Just a) k = Just a+  throwError () = Nothing+#endif  orM :: (MonadError e m) => m a -> m a -> m a orM m1 m2 = m1 `catchError` (const m2)
src/TypeChecker.hs view
@@ -5,27 +5,26 @@  import Prelude hiding (null) -import Control.Applicative hiding (Const) -- ((<$>))-import Control.Monad+#if !MIN_VERSION_base(4,8,0)+import Control.Applicative ((<$>), (<*>))+#endif+import Control.Monad          (foldM, forM, forM_, liftM, unless, when, zipWithM, zipWithM_) import Control.Monad.IO.Class (MonadIO(..)) import Control.Monad.State    (runStateT, get, gets, put) import Control.Monad.Except   (runExceptT, catchError) import Control.Monad.Reader   (runReaderT, ask, asks, local)-import Control.Monad.Trans    (lift)  import qualified Data.List as List import Data.Map (Map)-import qualified Data.Map as Map import Data.Maybe import qualified Data.Foldable as Foldable import qualified Data.Traversable as Traversable -import Debug.Trace (trace)+-- import Debug.Trace (trace)  import qualified Text.PrettyPrint as PP  import Util-import qualified Util as Util  import Abstract hiding (Substitute) import Polarity as Pol@@ -33,18 +32,18 @@ import TCM import Eval import Extract--- import SPos (nocc) -- RETIRED -- import CallStack import PrettyTCM import TraceError -import Warshall hiding (Flex) -- size constraint checking- import Termination  -- import Completness +traceCheck, traceSing, traceAdm :: String -> a -> a+traceCheckM, traceSingM, traceAdmM :: Monad m => String -> m () + traceCheck msg a = a -- trace msg a traceCheckM msg = return () -- traceM msg {-@@ -71,16 +70,20 @@ runWhnf sig tc = (runExceptT (runStateT tc  sig)) -} +doNf :: Signature -> Expr -> IO (Either TraceError (Expr, TCState)) doNf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)++doWhnf :: Signature -> Expr -> IO (Either TraceError (Val, TCState)) doWhnf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)   -- top-level functions ------------------------------------------- -runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a,TCState))+runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a, TCState)) runTypeCheck st tc = runExceptT (runReaderT (runStateT tc st) emptyContext) -- runTypeCheck st tc = runCallStackT (runReaderT (runStateT tc st) emptyContext) [] +typeCheck :: [Declaration] -> IO (Either TraceError ([EDeclaration], TCState)) typeCheck dl = runTypeCheck initSt (typeCheckDecls dl)  -- checking top-level declarations -------------------------------@@ -88,6 +91,7 @@ echo :: MonadIO m => String -> m () echo = liftIO . putStrLn +echoR :: MonadIO m => String -> m () echoR = echo -- echoR s = echo $ "R> " ++ s @@ -100,6 +104,7 @@ echoKindedDef :: (Show n, MonadIO m) => Kind -> n -> Expr -> m () echoKindedDef ki n t = echo $ prettyKind ki ++ "  " ++ show n ++ " = " ++ show t +echoEPrefix :: String echoEPrefix = "E> "  echoTySigE :: (Show n, MonadIO m) => n -> Expr -> m ()@@ -122,7 +127,7 @@ typeCheckDeclaration :: Declaration -> TypeCheck [EDeclaration] typeCheckDeclaration (OverrideDecl Check ds) = do   st <- get-  typeCheckDecls ds+  _ <- typeCheckDecls ds   put st             -- forget the effect of these decls   return [] typeCheckDeclaration (OverrideDecl Fail ds) = do@@ -550,7 +555,7 @@         echoR $ (PP.render $ prettyFun n cls))       funse     -- replace in signature by erased clauses-    zipWithM (enableSig co) (zipWith intersectKind kis $ map kindOf kfse) funse+    zipWithM_ (enableSig co) (zipWith intersectKind kis $ map kindOf kfse) funse     return $ funse    where@@ -593,7 +598,7 @@     kfse <- mapM typeCheckFunSig funs0     let kfuns = zipWith (\ (Kinded ki ts) (Fun ts0 n' ar cls) -> Kinded ki (Fun ts n' ar cls)) kfse funs0     -- zipWithM (addFunSig co) (map kindOf kfse) funs-    mapM (addFunSig co) kfuns+    mapM_ (addFunSig co) kfuns     let funs = map valueOf kfuns     -- type check and solve size constraints     -- return clauses with meta vars resolved@@ -619,7 +624,7 @@       funse     terminationCheck funse     -- replace in signature by erased clauses-    zipWithM enableSig kis funse+    zipWithM_ enableSig kis funse     return $ funse  addFunSig :: Co -> Kinded Fun -> TypeCheck ()@@ -708,26 +713,11 @@   case tv of     VApp (VDef (DefId DatK (QName n))) vs | n == d -> do       telvs <- mapM (\ tb -> whnf' (Var (boundName tb))) $ telescope tel-      enter ("checking datatype parameters in constructor target") $+      _ <- enter ("checking datatype parameters in constructor target") $         leqVals' N mixed (One dv) (take (size tel) vs) telvs       return ()     _ -> throwErrorMsg $ "constructor should produce something in data type " ++ show d -{- RETIRED (syntactic check)-checkTarget :: Name -> Telescope -> Type -> TypeCheck ()-checkTarget d tel tg =-    case spineView tg of-      (Def (DefId Dat n), args) | n == d -> checkParams tel (take (length tel) args)-      _ -> throwErrorMsg $ "target mismatch"  ++ show tg--    where checkParams :: Telescope -> [Expr] -> TypeCheck ()-          checkParams [] [] = return ()-          checkParams (tb : tl) ((Var n') : el) | boundName tb == n'-            = checkParams tl el-          checkParams tl al = throwErrorMsg $ "target param mismatch " ++-            d ++ " " ++ show tel ++ " != " ++ show tg ++ "\ncheckParams " ++ show tl ++ " " ++ show al ++ " failed"--}- -- check that params are types -- check that arguments are stypes -- check that target is set@@ -1212,6 +1202,7 @@   (knes, tv) <- checkSpine es tv   return (kne : knes, tv) +maybeErase :: Polarity pol => pol -> Expr -> Expr maybeErase dec = if erased dec then erasedExpr else id  -- | checking e against (x : A) -> B returns (x,e) and B[e/x]@@ -1623,7 +1614,7 @@       -- clearDots -- NOT NEEDED       (flex,ins,cxt,vt,pe,pv,absp) <- checkPattern neutral [] emptySub tv p       local (\ _ -> cxt) $ do-        mapM (checkGoal ins) flex+        mapM_ (checkGoal ins) flex         tel <- getContextTele -- TODO!         case (absp,mrhs) of            (True,Nothing) -> return $ Kinded NoKind (Clause tel [pe] Nothing)@@ -1673,7 +1664,7 @@     -- Note that cofuns need not be SN, so the strict consistency may be     -- not necessary.     local (\ _ -> cxt { consistencyCheck = (mutualCo cxt == Ind) }) $ do-      mapM (checkGoal ins) flex+      mapM_ (checkGoal ins) flex {-       dots <- openDots       unless (null dots) $@@ -1696,8 +1687,13 @@  type Substitution = Valuation -- [(Int,Val)] -emptySub    = emptyVal-sgSub       = sgVal+emptySub :: Substitution+emptySub = emptyVal++sgSub :: Int -> Val -> Substitution+sgSub = sgVal++lookupSub :: Int -> Substitution -> Maybe Val lookupSub i = lookup i . valuation  type DotFlex = (Int,(Expr,Domain))@@ -2152,23 +2148,7 @@   check  List ($ j) <= List i  -} -{- RETIRED -- checkDot does not need to extract-checkDot :: Substitution -> DotFlex -> TypeCheck ()-checkDot subst (i,(e,it)) = enter ("dot pattern " ++ show e) $-  case (lookup i subst) of-    Nothing -> throwErrorMsg $ "not instantiated"-    Just v -> do-      tv <- substitute subst (typ it)-      ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)-      applyDec (decor it) $ do-        checkExpr e tv-        v' <-  whnf' e -- TODO: has subst erased terms?-        enter ("inferred value " ++ show v ++ " does not match given dot pattern value " ++ show v') $-          eqVal Pos tv v v'--}---- checkDot does not need to extract -- 2012-01-25 now we do since "extraction" turns also con.terms into records checkGoal :: Substitution -> Goal -> TypeCheck () checkGoal subst (DotFlex i me it) = enter ("dot pattern " ++ show me) $@@ -2754,6 +2734,7 @@ lowerSemiCont :: Int -> TVal -> TypeCheck Bool lowerSemiCont i tv = errorToBool $ lowerSemiContinuous i tv +docNotLowerSemi :: Int -> TVal -> TypeCheck Doc docNotLowerSemi i av = text "type " <+> prettyTCM av <+>   text " not lower semi continuous in " <+> prettyTCM (VGen i) @@ -3013,6 +2994,7 @@        _ -> throwErrorMsg "admPattern: IMPOSSIBLE: pattern for a non-function type" +cannotMatchDeep :: Pattern -> TVal -> TypeCheck () cannotMatchDeep p tv = recoverFailDoc $   text "cannot match against deep successor pattern"     <+> text (show p) <+> text "at type" <+> prettyTCM tv
src/Util.hs view
@@ -3,16 +3,20 @@ {-# LANGUAGE TupleSections, NoMonomorphismRestriction,       FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies #-} -module Util where+module Util (module Util, module X) where +-- reexports:+import Data.List as X (intercalate)+ import Prelude hiding (showList, null, (<>))  #if !MIN_VERSION_base(4,8,0)-import Control.Applicative hiding (empty)+import Control.Applicative (Applicative, (<$>)) #endif import Control.Monad import Control.Monad.Writer (Writer, runWriter) +import qualified Data.List.NonEmpty as List1 import qualified Data.List as List import Data.Map (Map) import qualified Data.Map as Map@@ -20,6 +24,8 @@ import Debug.Trace  import Text.PrettyPrint as PP++type List1 = List1.NonEmpty  (+?+) :: String -> String -> String (+?+) _ "[]" = []
src/Value.hs view
@@ -1,16 +1,20 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE LambdaCase #-} {-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}  module Value where  import Prelude hiding (null) +#if !MIN_VERSION_base(4,8,0) import Control.Applicative-import Control.Monad.Except+#endif+import Control.Monad.Except (MonadError)  import qualified Data.List as List import Data.Set (Set) import qualified Data.Set as Set-import Debug.Trace+-- import Debug.Trace  import Abstract import Polarity@@ -73,7 +77,7 @@ isFun VAbs{}                         = True isFun VConst{}                       = True isFun (VUp _ VQuant{ vqPiSig = Pi }) = True-isFun v                              = False+isFun _                              = False  absName :: FVal -> Name absName fv =@@ -92,7 +96,10 @@ newtype Valuation = Valuation { valuation :: [(Int,Val)] }   deriving (Eq,Ord) +emptyVal :: Valuation emptyVal  = Valuation []++sgVal :: Int -> Val -> Valuation sgVal i v = Valuation [(i,v)]  valuateGen :: Int -> Valuation -> Val@@ -104,16 +111,11 @@   { envMap   :: [(Name,a)]          -- the actual map from names to values   , envBound :: Maybe (Measure Val) -- optionally the current termination measure   }-               deriving (Eq,Ord,Show)+  deriving (Eq, Ord, Show)  type EnvMap = [(Name,Val)] type Env = Environ Val -{--data MeasVal = MeasVal [Val]  -- lexicographic termination measure-               deriving (Eq,Ord,Show)--}- -- smart constructors ------------------------------------------------  -- | The value representing type Size.@@ -121,6 +123,7 @@ vSize = VBelow Le VInfty -- 2012-01-28 non-termination bug I have not found -- vSize = VSort $ SortC Size +vFinSize :: Val vFinSize = VBelow Lt VInfty  -- | Ensure we construct the correct value representing Size.@@ -133,17 +136,18 @@ isVSize (VBelow Le VInfty)   = True isVSize _                    = False +vTSize :: Val vTSize = VSort $ SortC TSize  vTopSort :: Val vTopSort = VSort $ Set VInfty  mkClos :: Env -> Expr -> Val-mkClos rho Infty       = VInfty-mkClos rho Zero        = VZero+mkClos _   Infty       = VInfty+mkClos _   Zero        = VZero -- mkClos rho (Succ e)    = VSucc (mkClos rho e)  -- violates an invariant!! succeed/crazys mkClos rho (Below ltle e) = VBelow ltle (mkClos rho e)-mkClos rho (Proj fx n) = VProj fx n+mkClos _   (Proj fx n) = VProj fx n mkClos rho (Var x) = lookupPure rho x mkClos rho (Ann e) = mkClos rho $ unTag e mkClos rho e = VClos rho e@@ -151,23 +155,24 @@   -- VClos (rho { envMap = filterEnv (freeVars e) (envMap rho)}) e  filterEnv :: Set Name -> EnvMap -> EnvMap-filterEnv ns [] = []+filterEnv _  [] = [] filterEnv ns ((x,v) : rho) =   if Set.member x ns then (x,v) : filterEnv (Set.delete x ns) rho    else filterEnv ns rho -vDef id   = VDef id `VApp` []+vDef :: DefId -> Val+vDef x = VDef x `VApp` []++vCon :: ConK -> QName -> Val vCon co n = vDef $ DefId (ConK co) n -- vCon co n = vDef $ DefId (ConK (coToConK co)) n-vFun n    = vDef $ DefId FunK $ QName n-vDat n    = vDef $ DefId DatK n -{- POSSIBLY BREAKS INVARIANT!-vApp :: Val -> [Val] -> Val-vApp f [] = f-vApp f vs = VApp f vs--}+vFun :: Name -> Val+vFun n = vDef $ DefId FunK $ QName n +vDat :: QName -> Val+vDat n = vDef $ DefId DatK n+ vAbs :: Name -> Int -> Val -> FVal vAbs x i v = VAbs x i v emptyVal @@ -175,6 +180,7 @@ arrow = quant Pi prod  = quant Sigma +quant :: PiSigma -> TVal -> Val -> Val quant piSig a b = VQuant piSig x (defaultDomain a) (VConst b)   where x   = fresh "" -- quant piSig a b = VQuant piSig x (defaultDomain a) (Environ [(bla,b)] Nothing) (Var bla)@@ -197,8 +203,8 @@ -- 1. m -- 2. VMax ms  where length ms >= 2 and each mi different {- OLD--- * VSucc^* VGen--- * VMax vs where each v_i = VSucc^* (VGen k_i) and all k_i different+-- - VSucc^* VGen+-- - VMax vs where each v_i = VSucc^* (VGen k_i) and all k_i different --           and vs has length >= 2 -} --@@ -214,14 +220,16 @@             VMax vs -> maxSize $ map succSize vs             VMeta i rho n -> VMeta i rho (n + 1)  -- TODO: integrate + and mvar             _ -> VSucc v++vSucc :: Val -> Val vSucc = succSize  -- "multiplication" of sizes plusSize :: Val -> Val -> Val plusSize VZero v = v plusSize v VZero = v-plusSize VInfty v = VInfty-plusSize v VInfty = VInfty+plusSize VInfty _ = VInfty+plusSize _ VInfty = VInfty plusSize (VMax vs) v = maxSize $ map (plusSize v) vs plusSize v (VMax vs) = maxSize $ map (plusSize v) vs plusSize (VSucc v) v' = succSize $ plusSize v v'@@ -288,7 +296,7 @@  isDataType :: TVal -> Bool isDataType (VApp (VDef (DefId DatK _)) _) = True-isDataType (VSing v tv) = isDataType tv+isDataType (VSing _ tv) = isDataType tv isDataType _ = False  -- * ugly printing -----------------------------------------------------@@ -328,7 +336,7 @@   show (VGuard beta tv) = parens $ show beta ++ " -> " ++ show tv   show (VBelow ltle v) = show ltle ++ " " ++ show v -  show (VQuant pisig x (Domain (VBelow ltle v) ki dec) bv)+  show (VQuant pisig x (Domain (VBelow ltle v) _ki dec) bv)        | (ltle,v) /= (Le,VInfty) =        parens $ (\ p -> if p==defaultPol then "" else show p) (polarity dec) ++                 (if erased dec then brackets binding else parens binding)@@ -351,12 +359,12 @@   show (VAbs x i v valu) = "(\\" ++ show x ++ "@" ++ show i ++ show v ++ showValuation valu ++ ")"   show (VUp v vt) = "(" ++ show v ++ " Up " ++ show vt ++ ")" -showSkipLambda v =-  case v of-    (VLam x env e)    -> show e ++ showEnv env-    (VConst v)        -> show v-    (VAbs x i v valu) -> show v ++ showValuation valu-    v                 -> show v+showSkipLambda :: Val -> String+showSkipLambda = \case+    (VLam _x env e)     -> show e ++ showEnv env+    (VConst v)          -> show v+    (VAbs _x _i v valu) -> show v ++ showValuation valu+    v                   -> show v  showVals :: [Val] -> String showVals [] = ""
+ src/Version.hs view
@@ -0,0 +1,13 @@+-- | Standard module to access version as specified in @.cabal@ file.++module Version ( version ) where++import Data.List    ( intercalate )+import Data.Version ( Version(versionBranch) )++import qualified Paths_MiniAgda as Paths++-- | The program version obtained from the cabal file.++version :: String+version = intercalate "." $ map show $ versionBranch Paths.version
src/Warshall.hs view
@@ -83,9 +83,9 @@ -- constraints ---------------------------------------------------  -- nodes of the graph are either--- * flexible variables (with identifiers drawn from Int),--- * rigid variables (also identified by Ints), or--- * constants (like 0, infinity, or anything between)+-- - flexible variables (with identifiers drawn from Int),+-- - rigid variables (also identified by Ints), or+-- - constants (like 0, infinity, or anything between)  data Node rigid   = Rigid rigid
+ stack-8.10.7.yaml view
@@ -0,0 +1,4 @@+resolver: lts-18.28++extra-deps:+- haskell-src-exts-1.21.1
+ stack-9.0.2.yaml view
@@ -0,0 +1,4 @@+resolver: lts-19.3++extra-deps:+- haskell-src-exts-1.21.1
+ stack-9.10.yaml view
@@ -0,0 +1,4 @@+resolver: lts-24.1++extra-deps:+- haskell-src-exts-1.21.1
+ stack-9.12.yaml view
@@ -0,0 +1,5 @@+resolver: nightly-2025-07-23++extra-deps:+- haskell-src-exts-1.21.1+- goldplate-0.2.2.1@rev:2
+ stack-9.2.5.yaml view
@@ -0,0 +1,4 @@+resolver: lts-20.1++extra-deps:+- haskell-src-exts-1.21.1
+ stack-9.4.3.yaml view
@@ -0,0 +1,7 @@+resolver: nightly-2022-11-20++extra-deps:+- haskell-src-exts-1.21.1+# temporarily use patched goldplate that uses "/" as path separator also under Windows+- git: https://github.com/fugue/goldplate.git+  commit: a671a1dc38d0e73f1598cee5a874d02e520ede71
+ stack-9.6.yaml view
@@ -0,0 +1,4 @@+resolver: lts-22.44++extra-deps:+- haskell-src-exts-1.21.1
+ stack-9.8.yaml view
@@ -0,0 +1,4 @@+resolver: lts-23.27++extra-deps:+- haskell-src-exts-1.21.1
test/GoldplateTests.hs view
@@ -1,5 +1,6 @@-import System.Exit     ( exitWith  )-import System.Process  ( system    )+import System.Environment ( getArgs  )+import System.Exit        ( exitWith  )+import System.Process     ( rawSystem )  main :: IO ()-main = exitWith =<< system ("goldplate test")+main = exitWith =<< rawSystem "goldplate" . ("test" :) =<< getArgs
test/fail/AccCoqTermination.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AccCoqTermination.ma" --- --- scope checking --- --- type checking ---
test/fail/AccImplicit.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AccImplicit.ma" --- --- scope checking --- --- type checking ---
test/fail/BadConstraint.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BadConstraint.ma" --- --- scope checking --- scope check error: f
test/fail/BadConstraint1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BadConstraint1.ma" --- --- scope checking --- scope check error: f
test/fail/BadSizeLambda.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BadSizeLambda.ma" --- --- scope checking --- --- type checking ---
test/fail/BadSizeLambdaCoinductive.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BadSizeLambdaCoinductive.ma" --- --- scope checking --- --- type checking ---
test/fail/BadSizeLambdaInductive.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BadSizeLambdaInductive.ma" --- --- scope checking --- --- type checking ---
test/fail/BigDataInSet0.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BigDataInSet0.ma" --- --- scope checking --- --- type checking ---
test/fail/BoundedFake.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BoundedFake.ma" --- --- scope checking --- --- type checking ---
test/fail/BoundedQStrict.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BoundedQStrict.ma" --- --- scope checking --- --- type checking ---
test/fail/BoundedQWrong.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BoundedQWrong.ma" --- --- scope checking --- --- type checking ---
test/fail/BoxNeg.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BoxNeg.ma" --- --- scope checking --- --- type checking ---
test/fail/CheatSubtypingPos.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "CheatSubtypingPos.ma" --- --- scope checking --- --- type checking ---
test/fail/CoNotLowerSemi.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "CoNotLowerSemi.ma" --- --- scope checking --- --- type checking ---
test/fail/CoNotLowerSemi1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "CoNotLowerSemi1.ma" --- --- scope checking --- --- type checking ---
test/fail/D.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "D.ma" --- --- scope checking --- --- type checking ---
test/fail/D1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "D1.ma" --- --- scope checking --- --- type checking ---
test/fail/DataAtSetInfty.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DataAtSetInfty.ma" --- --- scope checking --- --- type checking ---
test/fail/DeepForcedConstructors.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DeepForcedConstructors.ma" --- --- scope checking --- --- type checking ---
test/fail/DescendAscend.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DescendAscend.ma" --- --- scope checking --- --- type checking ---
test/fail/DescendAscend2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DescendAscend2.ma" --- --- scope checking --- --- type checking ---
test/fail/DoNotEraseDataTeleForConTypes.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DoNotEraseDataTeleForConTypes.ma" --- --- scope checking --- --- type checking ---
test/fail/DottedConstructorsWrong.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DottedConstructorsWrong.ma" --- --- scope checking --- --- type checking ---
test/fail/EndsCoInEmpty.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "EndsCoInEmpty.ma" --- --- scope checking --- --- type checking ---
test/fail/ExistsSPos.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ExistsSPos.ma" --- --- scope checking --- --- type checking ---
test/fail/Fib2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Fib2.ma" --- --- scope checking --- --- type checking ---
test/fail/FinBranchMutualWrong.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "FinBranchMutualWrong.ma" --- --- scope checking --- --- type checking ---
test/fail/FunctionExtensionality.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "FunctionExtensionality.ma" --- --- scope checking --- --- type checking ---
test/fail/HOMatching.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HOMatching.ma" --- --- scope checking --- --- type checking ---
test/fail/HetIdFoolingEta.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HetIdFoolingEta.ma" --- --- scope checking --- --- type checking ---
test/fail/HungryEtaRecord.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HungryEtaRecord.ma" --- --- scope checking --- --- type checking ---
test/fail/IdFoolingEta.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IdFoolingEta.ma" --- --- scope checking --- --- type checking ---
test/fail/IllegalParameter.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IllegalParameter.ma" --- --- scope checking --- scope check error: D
test/fail/InconsistentHypotheses.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "InconsistentHypotheses.ma" --- --- scope checking --- --- type checking ---
test/fail/InjDataLoop.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "InjDataLoop.ma" --- --- scope checking --- --- type checking ---
test/fail/InjDataLoop2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "InjDataLoop2.ma" --- --- scope checking --- --- type checking ---
test/fail/InvalidField.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "InvalidField.ma" --- --- scope checking --- scope check error: D
test/fail/InvalidSizeP.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "InvalidSizeP.ma" --- --- scope checking --- --- type checking ---
test/fail/IrrHeterogeneousEta.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IrrHeterogeneousEta.ma" --- --- scope checking --- --- type checking ---
test/fail/IrrHeterogeneousFun.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IrrHeterogeneousFun.ma" --- --- scope checking --- --- type checking ---
test/fail/MeasureInTelescope.err view
@@ -1,3 +1,2 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasureInTelescope.ma" --- --- scope checking ---
test/fail/MeasureInValue.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasureInValue.ma" --- --- scope checking --- scope check error: f
test/fail/MeasuresTypo.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasuresTypo.ma" --- --- scope checking --- --- type checking ---
test/fail/MixedMeasureLength.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MixedMeasureLength.ma" --- --- scope checking --- scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length
test/fail/MixedMeasuredUnmeasured.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MixedMeasuredUnmeasured.ma" --- --- scope checking --- scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length
test/fail/MuOnlyPosNotSPos.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MuOnlyPosNotSPos.ma" --- --- scope checking --- --- type checking ---
test/fail/MustBeCofun.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MustBeCofun.ma" --- --- scope checking --- --- type checking ---
test/fail/MutualDataNotMon.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MutualDataNotMon.ma" --- --- scope checking --- --- type checking ---
test/fail/MutualNeg.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MutualNeg.ma" --- --- scope checking --- --- type checking ---
test/fail/MutualNeg2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MutualNeg2.ma" --- --- scope checking --- --- type checking ---
test/fail/NatToSize.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NatToSize.ma" --- --- scope checking --- --- type checking ---
test/fail/NegPol.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NegPol.ma" --- --- scope checking --- --- type checking ---
test/fail/NonLinearParameter.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NonLinearParameter.ma" --- --- scope checking --- --- type checking ---
test/fail/NonLinearParameterPattern.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NonLinearParameterPattern.ma" --- --- scope checking --- --- type checking ---
test/fail/NonLinearPatterns.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NonLinearPatterns.ma" --- --- scope checking --- scope check error: nonlin
test/fail/NonPosBoundedData.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NonPosBoundedData.ma" --- --- scope checking --- --- type checking ---
test/fail/NotEnoughParameters.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NotEnoughParameters.ma" --- --- scope checking --- scope check error: D
test/fail/NotForcedConstructors.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NotForcedConstructors.ma" --- --- scope checking --- --- type checking ---
test/fail/NumbersAsIds.err view
@@ -1,3 +1,2 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NumbersAsIds.ma" --- --- scope checking ---
test/fail/OverlappingPatternIndFam-sound.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "OverlappingPatternIndFam-sound.ma" --- --- scope checking --- --- type checking ---
test/fail/OverlappingPatternIndFam.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "OverlappingPatternIndFam.ma" --- --- scope checking --- --- type checking ---
test/fail/PolarityWrongCast.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "PolarityWrongCast.ma" --- --- scope checking --- --- type checking ---
test/fail/RecurseOnErased.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "RecurseOnErased.ma" --- --- scope checking --- --- type checking ---
test/fail/ResurrectFromErasedPattern.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ResurrectFromErasedPattern.ma" --- --- scope checking --- --- type checking ---
test/fail/SPosNotPos.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "SPosNotPos.ma" --- --- scope checking --- --- type checking ---
test/fail/ShadowBinding.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ShadowBinding.ma" --- --- scope checking --- scope check error: (let A = A in A): Identifier A already in context
test/fail/ShadowParameter.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ShadowParameter.ma" --- --- scope checking --- scope check error: Sg
test/fail/ShadowPatternParameter.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ShadowPatternParameter.ma" --- --- scope checking --- scope check error: D
test/fail/SizedDataWrongPol.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "SizedDataWrongPol.ma" --- --- scope checking --- --- type checking ---
test/fail/StoreSize.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StoreSize.ma" --- --- scope checking --- --- type checking ---
test/fail/StreamDupl.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StreamDupl.ma" --- --- scope checking --- --- type checking ---
test/fail/StreamNotSemiCont.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StreamNotSemiCont.ma" --- --- scope checking --- --- type checking ---
test/fail/Tm.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Tm.ma" --- --- scope checking --- --- type checking ---
test/fail/TypeInTypeViaSetInfty.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "TypeInTypeViaSetInfty.ma" --- --- scope checking --- --- type checking ---
test/fail/UlfsCounterexample.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "UlfsCounterexample.ma" --- --- scope checking --- --- type checking ---
test/fail/UlfsCounterexample2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "UlfsCounterexample2.ma" --- --- scope checking --- --- type checking ---
test/fail/VectorPatternNotForced.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "VectorPatternNotForced.ma" --- --- scope checking --- --- type checking ---
test/fail/VeiledParameter.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "VeiledParameter.ma" --- --- scope checking --- scope check error: D
test/fail/absurdPatUnit.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "absurdPatUnit.ma" --- --- scope checking --- --- type checking ---
test/fail/adm/adm1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "adm/adm1.ma" --- --- scope checking --- --- type checking ---
test/fail/adm/adm2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "adm/adm2.ma" --- --- scope checking --- --- type checking ---
test/fail/adm/adm3.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "adm/adm3.ma" --- --- scope checking --- --- type checking ---
test/fail/bfSizePatternIncomplete.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "bfSizePatternIncomplete.ma" --- --- scope checking --- --- type checking ---
test/fail/bfTypeNotAdmissible.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "bfTypeNotAdmissible.ma" --- --- scope checking --- --- type checking ---
test/fail/bigData.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "bigData.ma" --- --- scope checking --- --- type checking ---
test/fail/coSetOmega.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "coSetOmega.ma" --- --- scope checking --- --- type checking ---
test/fail/coSizeInFun.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "coSizeInFun.ma" --- --- scope checking --- --- type checking ---
test/fail/codataNotMonotone.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "codataNotMonotone.ma" --- --- scope checking --- --- type checking ---
test/fail/codyPatternConditionExplicit.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "codyPatternConditionExplicit.ma" --- --- scope checking --- --- type checking ---
test/fail/codyPatternConditionExplicit2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "codyPatternConditionExplicit2.ma" --- --- scope checking --- --- type checking ---
test/fail/cofunIntoBoolTimesStream.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "cofunIntoBoolTimesStream.ma" --- --- scope checking --- --- type checking ---
test/fail/cofunIntoStreamPlusStream.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "cofunIntoStreamPlusStream.ma" --- --- scope checking --- --- type checking ---
test/fail/countingBT.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "countingBT.ma" --- --- scope checking --- --- type checking ---
test/fail/countingMerge.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "countingMerge.ma" --- --- scope checking --- --- type checking ---
test/fail/dataNotMonotone.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "dataNotMonotone.ma" --- --- scope checking --- --- type checking ---
test/fail/drop.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "drop.ma" --- --- scope checking --- --- type checking ---
test/fail/erased1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "erased1.ma" --- --- scope checking --- --- type checking ---
test/fail/f_x_is_f_0.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "f_x_is_f_0.ma" --- --- scope checking --- --- type checking ---
test/fail/fail1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "fail1.ma" --- --- scope checking --- --- type checking ---
test/fail/fibStream.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "fibStream.ma" --- --- scope checking --- --- type checking ---
test/fail/hang.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "hang.ma" --- --- scope checking --- scope check error: f
test/fail/hang2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "hang2.ma" --- --- scope checking --- --- type checking ---
test/fail/huetHullotReverse.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "huetHullotReverse.ma" --- --- scope checking --- --- type checking ---
test/fail/incompleteSizePattern1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "incompleteSizePattern1.ma" --- --- scope checking --- --- type checking ---
test/fail/incompleteSizePattern2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "incompleteSizePattern2.ma" --- --- scope checking --- --- type checking ---
test/fail/inconsistentAssumption.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "inconsistentAssumption.ma" --- --- scope checking --- --- type checking ---
test/fail/inconsistentAssumption2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "inconsistentAssumption2.ma" --- --- scope checking --- --- type checking ---
test/fail/inductiveNotDotPattern.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "inductiveNotDotPattern.ma" --- --- scope checking --- --- type checking ---
test/fail/lengthCoList.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "lengthCoList.ma" --- --- scope checking --- --- type checking ---
test/fail/lengthCoList2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "lengthCoList2.ma" --- --- scope checking --- scope check error: convert3
test/fail/loop.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loop.ma" --- --- scope checking --- --- type checking ---
test/fail/loopAdmStream-Nat.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopAdmStream-Nat.ma" --- --- scope checking --- --- type checking ---
test/fail/loopAdmStream-simplified.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopAdmStream-simplified.ma" --- --- scope checking --- --- type checking ---
test/fail/loopAdmStream.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopAdmStream.ma" --- --- scope checking --- --- type checking ---
test/fail/loopBadTypesHidden.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopBadTypesHidden.ma" --- --- scope checking --- --- type checking ---
test/fail/loopBounded.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopBounded.ma" --- --- scope checking --- --- type checking ---
test/fail/loopOldNoSizePattern.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopOldNoSizePattern.ma" --- --- scope checking --- --- type checking ---
test/fail/loopTypesHiddenInData.err view
@@ -1,3 +1,2 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "loopTypesHiddenInData.ma" --- --- scope checking ---
test/fail/mapStream2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "mapStream2.ma" --- --- scope checking --- --- type checking ---
test/fail/mapStream2sizeMatchDepth2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "mapStream2sizeMatchDepth2.ma" --- --- scope checking --- --- type checking ---
test/fail/matchOnNatSuccI.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "matchOnNatSuccI.ma" --- --- scope checking --- --- type checking ---
test/fail/match_erased.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "match_erased.ma" --- --- scope checking --- --- type checking ---
test/fail/match_on_set.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "match_on_set.ma" --- --- scope checking --- scope check error: bla
test/fail/negativeFam.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "negativeFam.ma" --- --- scope checking --- --- type checking ---
test/fail/notAdmMonotoneArg.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "notAdmMonotoneArg.ma" --- --- scope checking --- --- type checking ---
test/fail/omegaInst.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "omegaInst.ma" --- --- scope checking --- --- type checking ---
test/fail/omegaInst1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "omegaInst1.ma" --- --- scope checking --- --- type checking ---
test/fail/onesStreamUnguarded.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "onesStreamUnguarded.ma" --- --- scope checking --- --- type checking ---
test/fail/partialFunction.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "partialFunction.ma" --- --- scope checking --- --- type checking ---
test/fail/relevantArgErasedMagicVec.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "relevantArgErasedMagicVec.ma" --- --- scope checking --- --- type checking ---
test/fail/scolist_not_lsc1.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "scolist_not_lsc1.ma" --- --- scope checking --- --- type checking ---
test/fail/scolist_not_lsc2.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "scolist_not_lsc2.ma" --- --- scope checking --- --- type checking ---
test/fail/shadowGlobal.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "shadowGlobal.ma" --- --- scope checking --- scope check error: "shadowing of global definitions forbidden": Identifier bla already in signature
test/fail/shouldBeDotPattern_snat.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "shouldBeDotPattern_snat.ma" --- --- scope checking --- --- type checking ---
test/fail/singleton.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "singleton.ma" --- --- scope checking --- --- type checking ---
test/fail/sizePatternSucc.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizePatternSucc.ma" --- --- scope checking --- --- type checking ---
test/fail/stream.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "stream.ma" --- --- scope checking --- scope check error: Stream
test/fail/streamMisc.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "streamMisc.ma" --- --- scope checking --- scope check error: wkStream2
test/fail/stream_x_is_cons_x_tail_x.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "stream_x_is_cons_x_tail_x.ma" --- --- scope checking --- --- type checking ---
test/fail/subtyping_erased.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "subtyping_erased.ma" --- --- scope checking --- --- type checking ---
test/fail/subtyping_erased_wrongdir.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "subtyping_erased_wrongdir.ma" --- --- scope checking --- --- type checking ---
test/fail/swapVariablesWithoutDecrease.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "swapVariablesWithoutDecrease.ma" --- --- scope checking --- --- type checking ---
test/fail/tailBad.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "tailBad.ma" --- --- scope checking --- --- type checking ---
test/fail/vec_eta.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "vec_eta.ma" --- --- scope checking --- --- type checking ---
test/fail/vec_length.err view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "vec_length.ma" --- --- scope checking --- --- type checking ---
test/should-fail/AgdaIssue1015.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AgdaIssue1015.ma" --- --- scope checking --- --- type checking ---
test/should-fail/AgdaIssue1015NonMutual.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AgdaIssue1015NonMutual.ma" --- --- scope checking --- --- type checking ---
test/should-fail/StrictInfty.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StrictInfty.ma" --- --- scope checking --- --- type checking ---
test/should-succeed/Umlaut.err view
@@ -1,3 +1,2 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Umlaut.ma" --- --- scope checking ---
test/succeed/AbsurdMatchNonLin.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AbsurdMatchNonLin.ma" --- --- scope checking --- --- type checking ---
test/succeed/AccDestructorErasedIndex.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AccDestructorErasedIndex.ma" --- --- scope checking --- --- type checking ---
test/succeed/AgdaIssue1052.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AgdaIssue1052.ma" --- --- scope checking --- --- type checking ---
test/succeed/AgdaIssue1055.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AgdaIssue1055.ma" --- --- scope checking --- --- type checking ---
test/succeed/AppendAddSize.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "AppendAddSize.ma" --- --- scope checking --- --- type checking ---
test/succeed/BelowLeInfty.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BelowLeInfty.ma" --- --- scope checking --- --- type checking ---
test/succeed/BigWrap.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BigWrap.ma" --- --- scope checking --- --- type checking ---
test/succeed/BoundedQ.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BoundedQ.ma" --- --- scope checking --- --- type checking ---
test/succeed/BuiltinSigma.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "BuiltinSigma.ma" --- --- scope checking --- --- type checking ---
test/succeed/CoFunReturnsProduct.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "CoFunReturnsProduct.ma" --- --- scope checking --- --- type checking ---
test/succeed/ConorMcBrideCalco09inflationary.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ConorMcBrideCalco09inflationary.ma" --- --- scope checking --- --- type checking ---
test/succeed/ConstructorTelescopes.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ConstructorTelescopes.ma" --- --- scope checking --- --- type checking ---
test/succeed/ConstructorVeiledTarget.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ConstructorVeiledTarget.ma" --- --- scope checking --- --- type checking ---
test/succeed/DataTypesNotFamilies.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DataTypesNotFamilies.ma" --- --- scope checking --- --- type checking ---
test/succeed/DeepMatch.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DeepMatch.ma" --- --- scope checking --- --- type checking ---
test/succeed/DescendAscendTerm.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DescendAscendTerm.ma" --- --- scope checking --- --- type checking ---
test/succeed/DotPatternNotLeftToRightBinding.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DotPatternNotLeftToRightBinding.ma" --- --- scope checking --- --- type checking ---
test/succeed/DottedConstructors.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DottedConstructors.ma" --- --- scope checking --- --- type checking ---
test/succeed/DottedPatSyn.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "DottedPatSyn.ma" --- --- scope checking --- --- type checking ---
test/succeed/Empty.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Empty.ma" --- --- scope checking --- --- type checking ---
test/succeed/EvalBoveCaprettaNotSized.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "EvalBoveCaprettaNotSized.ma" --- --- scope checking --- --- type checking ---
test/succeed/EvenOdd.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "EvenOdd.ma" --- --- scope checking --- --- type checking ---
test/succeed/Evens.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Evens.ma" --- --- scope checking --- --- type checking ---
test/succeed/ExtractLets.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ExtractLets.ma" --- --- scope checking --- --- type checking ---
test/succeed/FakeMutual.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "FakeMutual.ma" --- --- scope checking --- --- type checking ---
test/succeed/Fields.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Fields.ma" --- --- scope checking --- --- type checking ---
test/succeed/FinBranchMutual.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "FinBranchMutual.ma" --- --- scope checking --- --- type checking ---
test/succeed/Fix.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Fix.ma" --- --- scope checking --- --- type checking ---
test/succeed/ForceInConType.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ForceInConType.ma" --- --- scope checking --- --- type checking ---
test/succeed/ForcedMatch.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ForcedMatch.ma" --- --- scope checking --- --- type checking ---
test/succeed/ForcedMatchIdType.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ForcedMatchIdType.ma" --- --- scope checking --- --- type checking ---
test/succeed/ForestRose.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ForestRose.ma" --- --- scope checking --- --- type checking ---
test/succeed/GADT.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "GADT.ma" --- --- scope checking --- --- type checking ---
test/succeed/GoodConstraint.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "GoodConstraint.ma" --- --- scope checking --- --- type checking ---
test/succeed/HEq.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HEq.ma" --- --- scope checking --- --- type checking ---
test/succeed/HVec.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HVec.ma" --- --- scope checking --- --- type checking ---
test/succeed/HungryEtaRecord.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "HungryEtaRecord.ma" --- --- scope checking --- --- type checking ---
test/succeed/IdTypePos.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IdTypePos.ma" --- --- scope checking --- --- type checking ---
test/succeed/IrrHeterogeneousFun.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IrrHeterogeneousFun.ma" --- --- scope checking --- --- type checking ---
test/succeed/IrrHeterogeneousSingleton.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IrrHeterogeneousSingleton.ma" --- --- scope checking --- --- type checking ---
test/succeed/IrrHeterogeneousSize.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "IrrHeterogeneousSize.ma" --- --- scope checking --- --- type checking ---
test/succeed/LargeElim.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "LargeElim.ma" --- --- scope checking --- --- type checking ---
test/succeed/LetTele.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "LetTele.ma" --- --- scope checking --- --- type checking ---
test/succeed/LowerSemiCont.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "LowerSemiCont.ma" --- --- scope checking --- --- type checking ---
test/succeed/MeasureInFunTele.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasureInFunTele.ma" --- --- scope checking --- --- type checking ---
test/succeed/MeasuredHerSubst1.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasuredHerSubst1.ma" --- --- scope checking --- --- type checking ---
test/succeed/MeasuredRose.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MeasuredRose.ma" --- --- scope checking --- --- type checking ---
test/succeed/MergeWith.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MergeWith.ma" --- --- scope checking --- --- type checking ---
test/succeed/MockSig.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MockSig.ma" --- --- scope checking --- --- type checking ---
test/succeed/Mu.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Mu.ma" --- --- scope checking --- --- type checking ---
test/succeed/MultiSigma.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MultiSigma.ma" --- --- scope checking --- --- type checking ---
test/succeed/MutualBigDataKindInf.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MutualBigDataKindInf.ma" --- --- scope checking --- --- type checking ---
test/succeed/MutualRecordsNoEta.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "MutualRecordsNoEta.ma" --- --- scope checking --- --- type checking ---
test/succeed/Nested.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Nested.ma" --- --- scope checking --- --- type checking ---
test/succeed/NewSyntaxTour.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "NewSyntaxTour.ma" --- --- scope checking --- --- type checking ---
test/succeed/Nisse2012-02-17.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Nisse2012-02-17.ma" --- --- scope checking --- --- type checking ---
test/succeed/Nisse2012-03-06.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Nisse2012-03-06.ma" --- --- scope checking --- --- type checking ---
test/succeed/OverloadedConstructors.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "OverloadedConstructors.ma" --- --- scope checking --- --- type checking ---
test/succeed/PTSRule.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "PTSRule.ma" --- --- scope checking --- --- type checking ---
test/succeed/ParseMultBind.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ParseMultBind.ma" --- --- scope checking --- --- type checking ---
test/succeed/ParsePipeOperators.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ParsePipeOperators.ma" --- --- scope checking --- --- type checking ---
test/succeed/Pattern.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Pattern.ma" --- --- scope checking --- --- type checking ---
test/succeed/PatternParameters.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "PatternParameters.ma" --- --- scope checking --- --- type checking ---
test/succeed/Polarities.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Polarities.ma" --- --- scope checking --- --- type checking ---
test/succeed/PredDepType.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "PredDepType.ma" --- --- scope checking --- --- type checking ---
test/succeed/Prelude.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Prelude.ma" --- --- scope checking --- --- type checking ---
test/succeed/Prod.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Prod.ma" --- --- scope checking --- --- type checking ---
test/succeed/Projections.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Projections.ma" --- --- scope checking --- --- type checking ---
test/succeed/Rose.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Rose.ma" --- --- scope checking --- --- type checking ---
test/succeed/SP.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "SP.ma" --- --- scope checking --- --- type checking ---
test/succeed/ScopeCheckFunDef.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ScopeCheckFunDef.ma" --- --- scope checking --- --- type checking ---
test/succeed/SgPredWrongMon.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "SgPredWrongMon.ma" --- --- scope checking --- --- type checking ---
test/succeed/SolverBugStreamFixed.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "SolverBugStreamFixed.ma" --- --- scope checking --- --- type checking ---
test/succeed/Squash.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Squash.ma" --- --- scope checking --- --- type checking ---
test/succeed/Stack.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Stack.ma" --- --- scope checking --- --- type checking ---
test/succeed/StreamDupl.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StreamDupl.ma" --- --- scope checking --- --- type checking ---
test/succeed/StrictBoundedQCoinductive.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "StrictBoundedQCoinductive.ma" --- --- scope checking --- --- type checking ---
test/succeed/UPolyList.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "UPolyList.ma" --- --- scope checking --- --- type checking ---
test/succeed/Universe.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "Universe.ma" --- --- scope checking --- --- type checking ---
test/succeed/VecNotErased.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "VecNotErased.ma" --- --- scope checking --- --- type checking ---
test/succeed/WrapAbsurd.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "WrapAbsurd.ma" --- --- scope checking --- --- type checking ---
test/succeed/absurdPattern.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "absurdPattern.ma" --- --- scope checking --- --- type checking ---
test/succeed/addWith.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "addWith.ma" --- --- scope checking --- --- type checking ---
test/succeed/casePair.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "casePair.ma" --- --- scope checking --- --- type checking ---
test/succeed/caseSList.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "caseSList.ma" --- --- scope checking --- --- type checking ---
test/succeed/conat.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "conat.ma" --- --- scope checking --- --- type checking ---
test/succeed/countConstructors.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "countConstructors.ma" --- --- scope checking --- --- type checking ---
test/succeed/crazys.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "crazys.ma" --- --- scope checking --- --- type checking ---
test/succeed/drop.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "drop.ma" --- --- scope checking --- --- type checking ---
test/succeed/eta.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "eta.ma" --- --- scope checking --- --- type checking ---
test/succeed/eta_unit.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "eta_unit.ma" --- --- scope checking --- --- type checking ---
test/succeed/exists.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "exists.ma" --- --- scope checking --- --- type checking ---
test/succeed/fib.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "fib.ma" --- --- scope checking --- --- type checking ---
test/succeed/fibDeep.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "fibDeep.ma" --- --- scope checking --- --- type checking ---
test/succeed/gcd-either.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "gcd-either.ma" --- --- scope checking --- --- type checking ---
test/succeed/hamming.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "hamming.ma" --- --- scope checking --- --- type checking ---
test/succeed/ho.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "ho.ma" --- --- scope checking --- --- type checking ---
test/succeed/implicitSizeVarUsedExplicitely.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "implicitSizeVarUsedExplicitely.ma" --- --- scope checking --- --- type checking ---
test/succeed/lengthCoList.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "lengthCoList.ma" --- --- scope checking --- --- type checking ---
test/succeed/list.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "list.ma" --- --- scope checking --- --- type checking ---
test/succeed/logic.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "logic.ma" --- --- scope checking --- --- type checking ---
test/succeed/lossyIdentityOnStreams.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "lossyIdentityOnStreams.ma" --- --- scope checking --- --- type checking ---
test/succeed/magicVecLookupProofIrr.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "magicVecLookupProofIrr.ma" --- --- scope checking --- --- type checking ---
test/succeed/mapStream.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "mapStream.ma" --- --- scope checking --- --- type checking ---
test/succeed/max.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "max.ma" --- --- scope checking --- --- type checking ---
test/succeed/measures.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "measures.ma" --- --- scope checking --- --- type checking ---
test/succeed/msort-implicit.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "msort-implicit.ma" --- --- scope checking --- --- type checking ---
test/succeed/msort.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "msort.ma" --- --- scope checking --- --- type checking ---
test/succeed/nat.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "nat.ma" --- --- scope checking --- --- type checking ---
test/succeed/non-record.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "non-record.ma" --- --- scope checking --- --- type checking ---
test/succeed/old_stream.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "old_stream.ma" --- --- scope checking --- --- type checking ---
test/succeed/oldnat.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "oldnat.ma" --- --- scope checking --- --- type checking ---
test/succeed/omegaInst1.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "omegaInst1.ma" --- --- scope checking --- --- type checking ---
test/succeed/omegaInstTailInfty.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "omegaInstTailInfty.ma" --- --- scope checking --- --- type checking ---
test/succeed/pred.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "pred.ma" --- --- scope checking --- --- type checking ---
test/succeed/qsapp.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "qsapp.ma" --- --- scope checking --- --- type checking ---
test/succeed/quicksort-filter-fragment.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "quicksort-filter-fragment.ma" --- --- scope checking --- --- type checking ---
test/succeed/quicksort-filter.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "quicksort-filter.ma" --- --- scope checking --- --- type checking ---
test/succeed/quicksort.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "quicksort.ma" --- --- scope checking --- --- type checking ---
test/succeed/rank2SizeQuantStream.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "rank2SizeQuantStream.ma" --- --- scope checking --- --- type checking ---
test/succeed/record.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "record.ma" --- --- scope checking --- --- type checking ---
test/succeed/shadowDataParam.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "shadowDataParam.ma" --- --- scope checking --- --- type checking ---
test/succeed/sigma.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sigma.ma" --- --- scope checking --- --- type checking ---
test/succeed/simple_nat.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "simple_nat.ma" --- --- scope checking --- --- type checking ---
test/succeed/singleton.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "singleton.ma" --- --- scope checking --- --- type checking ---
test/succeed/sizeFunctions.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizeFunctions.ma" --- --- scope checking --- --- type checking ---
test/succeed/sizedFinitelyBranchingTrees.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizedFinitelyBranchingTrees.ma" --- --- scope checking --- --- type checking ---
test/succeed/sizedMax.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizedMax.ma" --- --- scope checking --- --- type checking ---
test/succeed/sizedMergeWith.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizedMergeWith.ma" --- --- scope checking --- --- type checking ---
test/succeed/sizedOrd.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "sizedOrd.ma" --- --- scope checking --- --- type checking ---
test/succeed/streamIdentityNatRecursive.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "streamIdentityNatRecursive.ma" --- --- scope checking --- --- type checking ---
test/succeed/subset.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "subset.ma" --- --- scope checking --- --- type checking ---
test/succeed/tailStream.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "tailStream.ma" --- --- scope checking --- --- type checking ---
test/succeed/vec.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "vec.ma" --- --- scope checking --- --- type checking ---
test/succeed/wkStream.golden view
@@ -1,4 +1,3 @@-MiniAgda by Andreas Abel and Karl Mehltretter --- opening "wkStream.ma" --- --- scope checking --- --- type checking ---