Skip to content

Commit

Permalink
unmatchable, axiom
Browse files Browse the repository at this point in the history
  • Loading branch information
KonjacSource committed Sep 9, 2024
1 parent 917afd8 commit f63f860
Show file tree
Hide file tree
Showing 7 changed files with 97 additions and 59 deletions.
1 change: 1 addition & 0 deletions README-zh.md
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ ghci> run "Eaxmple.shitt"
- [x] 无K的模式匹配
- [x] [语法高亮](https://github.com/KonjacSource/shitt-highlight)
- [x] 高阶归纳类型(暂无边界检查)
- [ ] REPL
- [ ] 运算符
- [ ] 停机检查
- [ ] 归纳类型的极性检查
Expand Down
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ ghci> run "Eaxmple.shitt"

## TODO

- [ ] REPL
- [ ] Operators
- [ ] Termination checking
- [ ] Positive checking for data types
Expand Down
33 changes: 22 additions & 11 deletions Test.shitt
Original file line number Diff line number Diff line change
@@ -1,15 +1,26 @@
data N : U where
| zero : ...
| succ : (pre : N) -> ...
data Bool : U where
| true : ...
| false : ...

higher inductive Int : U where
| pos : (n : N) -> ...
| neg : (n : N) -> ...
unmatchable data Interval : U where
| i0 : ...
| i1 : ...

-- This is ok
def reflTrue (i : Interval) : Bool
| i = true

-- -- This is error
-- def trueToFalse (i : Interval) : Bool
-- | i0 = true
-- | i1 = false

higher inductive S1 : U where
| base : ...
| loop : (i : Interval) -> ...
when
| zero = pos zero
| i0 = base
| i1 = base

#eval neg zero -- pos zero
#eval loop i0

def abs (n : Int) : N where
| pos n = n
| neg n = n
91 changes: 50 additions & 41 deletions src/ShiTT/Inductive.hs
Original file line number Diff line number Diff line change
Expand Up @@ -216,10 +216,11 @@ checkClauses ctx coverChGate fun cls = do
case t of
Left ctx -> pure (p,ctx)
Right (_,ctx) -> pure (p,ctx)

-- Coverage Check

when coverChGate $
checkCoverage fun.funName fun.funPara patsWithRes (genInitSp ctx fun.funPara)
when coverChGate $ do
unmatchables <- readIORef allUnmatchableTypes
checkCoverage unmatchables fun.funName fun.funPara patsWithRes (genInitSp ctx fun.funPara)

let rhss' = flip map rhss \case (p, Left _) -> (p, Nothing)
(p, Right x) -> (p, Just x)
Expand All @@ -240,9 +241,20 @@ checkFun ctx fun = do
}
let ctx' =ctx { decls = insertFun preFun ctx.decls }
val <- checkClauses ctx' True fun fun.clauses

-- TODO : HIT.Check Boundary
pure $ preFun { funVal = val }


checkAxiom :: Context -> D.Fun -> IO Fun
checkAxiom ctx fun = do
let preFun = Fun
{ funName = fun.funName
, funPara = fun.funPara
, funRetType = fun.funRetType
, funVal = \ _ _ -> Nothing -- A fake definition, so that we may check the type of the definning function
}
let ctx' =ctx { decls = insertFun preFun ctx.decls }
val <- checkClauses ctx' False fun fun.clauses
pure $ preFun { funVal = val }

unify1 :: NameOrder -> Context -> [Def] -> Value -> Value -> Either CheckError [Def]
Expand Down Expand Up @@ -347,15 +359,27 @@ data MatchResult
deriving Show

-- | ctx |- rhs, extraDef in ctx.
splitMatch1 :: Context -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult
splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of
splitMatch1 :: Context -> [Name] -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult
splitMatch1 ctx unmatchables (_, _, VCon ty_name []) p (v, i)
| D.icit p == i && ty_name `elem` unmatchables
= case (p, v) of
(PVar x _, VPatVar v [])
| isInacc ctx x -> Done [x := VPatVar v []] -- Mark as flexibile
| otherwise -> Done [x := VVar v]
(PVar x _, VVar v)
| isInacc ctx x -> Done [x := VPatVar v []]
| otherwise -> Done [x := VVar v]
(PVar x _, v) -> Done [x := v]
_ -> error "Trying match an unmatchable"

splitMatch1 ctx unmatchables t p (v, i) | D.icit p == i = case (p, v) of
(PVar x _, VPatVar v [])
| isInacc ctx x -> Done [x := VPatVar v []] -- Mark as flexibile
| otherwise -> Done [x := VVar v]
(PVar x _, VVar v)
| isInacc ctx x -> Done [x := VPatVar v []]
| otherwise -> Done [x := VVar v]
(PVar x _, v) -> Done [x := v]
| isInacc ctx x -> Done [x := VPatVar v []] -- Mark as flexibile
| otherwise -> Done [x := VVar v]
(PVar x _, VVar v)
| isInacc ctx x -> Done [x := VPatVar v []]
| otherwise -> Done [x := VVar v]
(PVar x _, v) -> Done [x := v]
(PCon con_name ps _, VCon con_name' vs) -- note that length ps /= length vs, since vs includes data parameters
| con_name == con_name' ->
-- 1. get data definition and constructor definition
Expand All @@ -371,6 +395,7 @@ splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of
-- 3. try match vs against ps under the modified teles
in case splitMatch
ctx
unmatchables
teles
ps
arg_vs
Expand All @@ -392,17 +417,17 @@ splitMatch1 ctx t p (v, i) | D.icit p == i = case (p, v) of
(_,v,_) <- poss
pure [v]
_ -> error $ "\n\nimpossible : " ++ show ctx ++ show t ++ " | " ++ show p ++ " | " ++ show (v, i) ++ "\n"
splitMatch1 _ _ _ _ = error "impossible"
splitMatch1 _ _ _ _ _ = error "impossible"

-- | try match, if stuck, return the pattern with splitted variables.
splitMatch :: Context -> Telescope -> [Pattern] -> Spine -> MatchResult
splitMatch ctx ts ps vs = case (ts, ps, vs) of
splitMatch :: Context -> [Name] -> Telescope -> [Pattern] -> Spine -> MatchResult
splitMatch ctx unmatchables ts ps vs = case (ts, ps, vs) of
([], [], []) -> Done []
(t:ts, p:ps, v:vs) ->
case splitMatch1 ctx t p v of
case splitMatch1 ctx unmatchables t p v of
Failed -> Failed
--
Done defs -> case splitMatch (ctx <: defs) ts ps vs of
Done defs -> case splitMatch (ctx <: defs) unmatchables ts ps vs of
Failed -> Failed
Done defs' -> Done $ defs ++ defs'
Stucked poss -> Stucked do
Expand All @@ -416,13 +441,13 @@ splitMatch ctx ts ps vs = case (ts, ps, vs) of
_ -> error $ "impossible : " ++ show ctx ++ show ts ++ "\n" ++ show ps ++ "\n" ++ show vs


travPattern :: Telescope -> [([Pattern], Context)] -> Spine -> Maybe [Spine]
travPattern ts [] sp = Just [sp] -- passed
travPattern ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx ts ps sp of
Failed -> travPattern ts rest sp
travPattern :: [Name] -> Telescope -> [([Pattern], Context)] -> Spine -> Maybe [Spine]
travPattern unmatchables ts [] sp = Just [sp] -- passed
travPattern unmatchables ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx unmatchables ts ps sp of
Failed -> travPattern unmatchables ts rest sp
Done _ -> Nothing
Stucked new_sps ->
let res = map (travPattern ts pats) new_sps
let res = map (travPattern unmatchables ts pats) new_sps
in if all isNothing res then
Nothing
else Just do
Expand All @@ -431,9 +456,9 @@ travPattern ts pats@((ps,rhs_ctx): rest) sp = case splitMatch rhs_ctx ts ps sp o
Nothing -> []
Just sp -> sp

checkCoverage :: Name -> Telescope -> [([Pattern], Context)] -> Spine -> IO ()
checkCoverage fun_name ts ps sp = do
case travPattern ts ps sp of
checkCoverage :: [Name] -> Name -> Telescope -> [([Pattern], Context)] -> Spine -> IO ()
checkCoverage unmatchables fun_name ts ps sp = do
case travPattern unmatchables ts ps sp of
Nothing -> pure ()
Just sp -> putStrLn ("Warning: Missing patterns on function " ++ fun_name ++ "\n" ++ show sp)

Expand Down Expand Up @@ -482,22 +507,6 @@ checkHData ctx (dat, hcons) = do
, higherCons = hcons'
}


{-
data HData = HData
{ basePart :: Data
, higherCons :: [HConstructor]
}
data HConstructor = HConstructor
{ hconName :: Name
, hconVars :: [Name]
, hconClauses :: Context -> Spine -> Maybe Value
}
-}

-- asValue :: [Def] -> Int -> Pattern -> ((Value, Icit), [Def])
-- asValue fvs nameCount = \case
-- PVar x i -> ((VVar x, i), freeVar (freshName (emptyCtx <: fvs) $ '*':show nameCount ++ x) : fvs)
Expand Down
9 changes: 7 additions & 2 deletions src/ShiTT/Meta.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ import ShiTT.Syntax
import Data.IORef
import System.IO.Unsafe

-- Meta Context
----------------
data MetaEntry = Unsolved | Solved Value
deriving Show

Expand Down Expand Up @@ -45,5 +47,8 @@ allSolved = do
withoutKRef :: IORef Bool
withoutKRef = runIO $ newIORef False

withoutK :: Bool
withoutK = runIO $ readIORef withoutKRef
-- Other Global
---------------

allUnmatchableTypes :: IORef [Name]
allUnmatchableTypes = runIO $ newIORef []
19 changes: 15 additions & 4 deletions src/ShiTT/Parser.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ import Data.IORef
import Control.Category ((>>>))
import Control.Exception hiding (try)
import Test (testContext2)
import ShiTT.Meta (allSolved, reset, withoutKRef)
import ShiTT.Meta (allSolved, reset, withoutKRef, allUnmatchableTypes)


type PatVars = [Name]
Expand Down Expand Up @@ -118,7 +118,11 @@ inCtx name = do


keywords :: [String]
keywords = ["U", "let", "in", "fun", "λ", "data", "where", "def", "fun", "nomatch", "auto", "traceContext", "inductive", "higher", "when"]
keywords = [ "U", "let", "in", "fun", "λ"
, "data", "where", "def", "fun"
, "nomatch", "auto", "traceContext"
, "inductive", "higher", "when"
, "unmatchable", "axiom" ]

pIdent :: Parser Name
pIdent = do
Expand Down Expand Up @@ -275,7 +279,12 @@ Each constructor must give all indexes.
-- Then return the fake definition.
pDataHeader :: Parser Data
pDataHeader = do
isUnmatchable <- (symbol "unmatchable" >> pure True) <|> pure False
data_name <- (symbol "data" <|> symbol "inductive") >> pIdent

when isUnmatchable $ do
liftIO $ modifyIORef allUnmatchableTypes (data_name:)

isFresh data_name
data_para <- pTelescope' -- Adding data parameters to context.
data_ix <- symbol ":" >> pTelescope
Expand Down Expand Up @@ -581,11 +590,13 @@ pTopLevel = choice [data_type, function, command, hdata_type] where
hdat <- liftIO $ checkHData ctx dat
addHData hdat

function = do
function = do
isAxiom <- (symbol "axiom" >> pure True) <|> pure False
let checker = if isAxiom then checkAxiom else checkFun
fun <- pFun
ctx <- getCtx
pos <- getSourcePos
checked_fun <- liftIO $ checkFun ctx fun
checked_fun <- liftIO $ checker ctx fun
`catch` \e -> putStrLn ("In function " ++ fun.funName ++ ":" ++ sourcePosPretty pos) >> case e of
PMErr pm -> error (show pm)
UnifyE u v -> error ("(PatternMatch) Can't unify " ++ show u ++ " with " ++ show v)
Expand Down
2 changes: 1 addition & 1 deletion src/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -392,7 +392,7 @@ splitTest4 = splitCase (testContext <: ("m", natType) :=! VPatVar "m" []) ("v",

-- Context -> (Name, Icit, VType) -> Pattern -> (Value, Icit) -> MatchResult

matchTest1 = I.splitMatch1 testContext2 ("_", Expl, natType) (PCon "zero" [] Expl) (VVar "x" ,Expl)
matchTest1 = I.splitMatch1 testContext2 [] ("_", Expl, natType) (PCon "zero" [] Expl) (VVar "x" ,Expl)

-- matchTest1 = trace (show ps) $ I.match' (testContext2 <: res.typeLevelDef) rhs_ctx ts ps vs
-- where
Expand Down

0 comments on commit f63f860

Please sign in to comment.