Permalink
Browse files

Record pattern match totality

darcs-hash:20090508092327-228f4-a8c751c08d3187e50a14cf3d9e19bbe047971efd.gz
  • Loading branch information...
1 parent 69323bd commit ec67c2c72978745a82a5f3eecb6296d7b434a850 eb committed May 8, 2009
Showing with 70 additions and 31 deletions.
  1. +2 −2 Ivor/Datatype.lhs
  2. +1 −1 Ivor/Evaluator.lhs
  3. +4 −4 Ivor/Nobby.lhs
  4. +19 −7 Ivor/PatternDefs.lhs
  5. +1 −1 Ivor/State.lhs
  6. +3 −3 Ivor/TT.lhs
  7. +6 −0 Ivor/TTCore.lhs
  8. +8 −8 Ivor/Typecheck.lhs
  9. +1 −1 Ivor/Unify.lhs
  10. +21 −0 Ivor/ViewTerm.lhs
  11. +2 −2 Makefile
  12. +2 −2 ivor.cabal
View
@@ -61,8 +61,8 @@ the context and an executable elimination rule.
> (ev, _) <- typecheck gamma'' erty
> (cv, _) <- typecheck gamma'' crty
> -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)
-> (esch, _, _) <- checkDef gamma'' er erty eschemes False False
-> (csch, _, _) <- checkDef gamma'' cr crty cschemes False False
+> (esch, _, _, _) <- checkDef gamma'' er erty eschemes False False
+> (csch, _, _, _) <- checkDef gamma'' cr crty cschemes False False
> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
> (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
View
@@ -68,7 +68,7 @@ Code Stack Env Result
> evalP n (Just v) xs env pats
> = case v of
> Fun opts (Ind v) -> eval v xs env pats
-> PatternDef p -> pmatch n p xs env pats
+> PatternDef p _ -> pmatch n p xs env pats
> PrimOp _ f -> case f xs of
> Nothing -> unload (P n) xs pats env
> Just v -> eval v [] env pats
View
@@ -24,7 +24,7 @@ to do with it, when the time comes.
> data Global n
> = Fun [FunOptions] (Indexed n) -- User defined function
> | Partial (Indexed n) [n] -- Unfinished definition
-> | PatternDef (PMFun n) -- Pattern matching definition
+> | PatternDef (PMFun n) Bool -- Pattern matching definition, totality
> | ElimRule ElimRule -- Elimination Rule
> | PrimOp PrimOp EvPrim -- Primitive function
> | DCon Int Int -- Data Constructor, tag and arity
@@ -37,7 +37,7 @@ to do with it, when the time comes.
> constructors :: [n] }
> | NoConstructorsYet
-> data FunOptions = Frozen | Recursive
+> data FunOptions = Frozen | Recursive | Total
> deriving Eq
> instance Show n => Show (Global n) where
@@ -240,11 +240,11 @@ Do the actual evaluation
> Nothing -> evalP (lookupval n gamma)
> where evalP (Just Unreducible) = (MB (BP n,pty n) Empty)
> evalP (Just Undefined) = (MB (BP n, pty n) Empty)
-> evalP (Just (PatternDef p@(PMFun 0 pats))) =
+> evalP (Just (PatternDef p@(PMFun 0 pats) _)) =
> case patmatch gamma g pats [] of
> Nothing -> (MB (BPatDef p n, pty n) Empty)
> Just v -> v
-> evalP (Just (PatternDef p)) = (MB (BPatDef p n, pty n) Empty)
+> evalP (Just (PatternDef p _)) = (MB (BPatDef p n, pty n) Empty)
> evalP (Just (Partial (Ind v) _)) = (MB (BP n, pty n) Empty)
> evalP (Just (PrimOp f _)) = (MB (BPrimOp f n, pty n) Empty)
> evalP (Just (Fun opts (Ind v)))
View
@@ -16,11 +16,12 @@ Use the iota schemes from Datatype to represent pattern matching definitions.
Return the definition and its type, as well as any other names which need
to be defined to complete the definition.
+Also return whether the function is definitely total.
> checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] ->
> Bool -> -- Check for coverage
> Bool -> -- Check for well-foundedness
-> m (PMFun Name, Indexed Name, [(Name, Indexed Name)])
+> m (PMFun Name, Indexed Name, [(Name, Indexed Name)], Bool)
> checkDef gam fn tyin pats cover wellfounded = do
> --x <- expandCon gam (mkapp (Var (UN "S")) [mkapp (Var (UN "S")) [Var (UN "x")]])
> --x <- expandCon gam (mkapp (Var (UN "vcons")) [RInfer,RInfer,RInfer,mkapp (Var (UN "vnil")) [Var (UN "foo")]])
@@ -32,9 +33,15 @@ to be defined to complete the definition.
> checkNotExists fn gam
> gam' <- gInsert fn (G Undefined ty defplicit) gam
> clauses' <- validClauses gam' fn ty clauses'
-> (pmdef, newdefs) <- matchClauses gam' fn pats tyin cover clauses'
-> when wellfounded $ checkWellFounded gam fn [0..arity-1] pmdef
-> return (PMFun arity pmdef, ty, newdefs)
+> (pmdef, newdefs, covers) <- matchClauses gam' fn pats tyin cover clauses'
+> wf <- if wellfounded then
+> do checkWellFounded gam fn [0..arity-1] pmdef
+> return True
+> else case checkWellFounded gam fn [0..arity-1] pmdef of
+> Nothing -> return False
+> _ -> return True
+> let total = wf && covers
+> return (PMFun arity pmdef, ty, newdefs, total)
> where checkNotExists n gam = case lookupval n gam of
> Just Undefined -> return ()
> Just _ -> fail $ show n ++ " already defined"
@@ -167,12 +174,17 @@ names bound in patterns) then type check the right hand side.
> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw ->
> Bool -> -- Check coverage
> [(Indexed Name, Indexed Name)] ->
-> m ([PMDef Name], [(Name, Indexed Name)])
+> m ([PMDef Name], [(Name, Indexed Name)], Bool)
> matchClauses gam fn pats tyin cover gen = do
> let raws = zip (map mkRaw pats) (map getRet pats)
> (checkpats, newdefs) <- mytypechecks gam raws [] []
-> when cover $ checkCoverage (map fst checkpats) (map fst gen)
-> return $ (map (mkScheme gam) checkpats, newdefs)
+> cv <- if cover then
+> do checkCoverage (map fst checkpats) (map fst gen)
+> return True
+> else case checkCoverage (map fst checkpats) (map fst gen) of
+> Nothing -> return False
+> _ -> return True
+> return $ (map (mkScheme gam) checkpats, newdefs, cv)
where mkRaw (RSch pats r) = mkPBind pats tyin r
mkPBind [] _ r = r
View
@@ -106,7 +106,7 @@ Take a data type definition and add constructors and elim rule to the context.
> gInsert n gl ctxt
> addElim ctxt erule schemes = do
> newdefs <- gInsert (fst erule)
-> (G (PatternDef schemes) (snd erule) defplicit)
+> (G (PatternDef schemes True) (snd erule) defplicit)
> ctxt
> return newdefs
View
@@ -267,7 +267,7 @@
> let ndefs = defs st
> inty <- raw ty
> let (Patterns clauses) = pats
-> (pmdef, fty, newnames)
+> (pmdef, fty, newnames, tot)
> <- checkDef ndefs n inty (map mkRawClause clauses)
> (not (elem Ivor.TT.Partial opts))
> (not (elem GenRec opts))
@@ -281,7 +281,7 @@
> extend g (n, G Unreducible t 0))
> ndefs newnames
> return (ngam, vnew)
-> newdefs <- gInsert n (G (PatternDef pmdef) fty defplicit) ndefs'
+> newdefs <- gInsert n (G (PatternDef pmdef tot) fty defplicit) ndefs'
> return (Ctxt st { defs = newdefs }, vnewnames)
> -- |Add a new definition, with its type to the global state.
@@ -819,7 +819,7 @@ Give a parseable but ugly representation of a term.
> getPatternDef :: Monad m => Context -> Name -> m (ViewTerm, Patterns)
> getPatternDef (Ctxt st) n
> = case glookup n (defs st) of
-> Just ((PatternDef pmf),ty) ->
+> Just ((PatternDef pmf _),ty) ->
> return $ (view (Term (ty, Ind TTCore.Star)),
> Patterns (map mkPat (getPats pmf)))
> Just ((Fun _ ind), ty) ->
View
@@ -309,6 +309,12 @@ we get a duff term when we go back to the indexed version.
> --if (i<length ctx) then P (ctx!!i)
> -- else V i) t'
+> makePsUniq :: TT Name -> TT Name
+> makePsUniq t = vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++
+> debugTT t))) t
+> --if (i<length ctx) then P (ctx!!i)
+> -- else V i) t'
+
> makePsEnv env t = let t' = evalState (uniqifyAllState t) env in
> vapp (\ (ctx,i) -> P (traceIndex ctx i
> ("makePsEnv" ++ debugTT t))) t'
View
@@ -106,9 +106,9 @@ constraints and applying it to the term and type.
> -- time do them. Because we don't know what order we can solve
> -- constraints in and they might depend on each other...
> do let cs = nub constraints
-> (subst, nms) <- {-# SCC "name" #-}
-> mkSubst $ (map (\x -> (True,x)) cs)
-> ++ (map (\x -> (False,x)) (reverse cs))
+> (subst, nms) <-
+> mkSubst $ (map (\x -> (True,x)) cs) ++
+> (map (\x -> (False,x)) (reverse cs))
> let tm' = papp subst tm
> let ty' = papp subst ty
> return (Ind tm',Ind ty')
@@ -123,7 +123,7 @@ constraints and applying it to the term and type.
> = do -- (s',nms) <- mkSubst xs
> let x' = papp s' x
> let (Ind y') = normalise gam (Ind (papp s' y))
-> uns <- {-# SCC "substUnify" #-}
+> uns <-
> case unifyenvErr ok gam env (Ind x') (Ind y') of
> Success x' -> return x'
> Failure err -> fail err
@@ -174,13 +174,13 @@ Return a list of the functions we need to define to complete the definition.
> let realNames = mkNames next
> e' <- renameB gam realNames (renameBinders e)
> (v1', t1') <- fixupGam gam realNames (v1, t1)
-> (v1''@(Ind vtm),t1'') <- {-# SCC "convert1" #-}doConversion tm1 gam bs v1' t1' -- (normalise gam t1')
+> (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')
> -- Drop names out of e' that don't appear in v1'' as a result of the
> -- unification.
> let namesbound = getNames (Sc vtm)
> let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')
-> ((v2,t2), (_, _, e'', bs',metas)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} {-# SCC "pairLvlCheck" #-} lvlcheck 0 inf next gam ein tm2 (Just t1')
-> (v2',t2') <- {-# SCC "convert2" #-} doConversion tm2 gam bs' v2 t2 -- (normalise gam t2)
+> ((v2,t2), (_, _, e'', bs',metas)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam ein tm2 (Just t1')
+> (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2)
> if (null metas)
> then return (v1',t1',v2',t2',e'', [])
> else do let (Ind v2tt) = v2'
@@ -291,7 +291,7 @@ typechecker...
> where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)
> mkTT Nothing (Just ((Fun _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((Partial _ _),t)) = return (Ind (P n), t)
-> mkTT Nothing (Just ((PatternDef _),t)) = return (Ind (P n), t)
+> mkTT Nothing (Just ((PatternDef _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just (Unreducible,t)) = return (Ind (P n), t)
> mkTT Nothing (Just (Undefined,t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((ElimRule _),t)) = return (Ind (Elim n), t)
View
@@ -114,7 +114,7 @@ Collect names which do unify, and ignore errors
> un envl envr x y acc
> | x == y || ignore = return acc
> | otherwise = fail $ "Can't unify " ++ show x ++
-> " and " ++ show y ++ " in " ++ show (topx,topy)
+> " and " ++ show y -- ++ " in " ++ show (topx,topy)
> unb envl envr (B b ty) (B b' ty') acc =
> do acc' <- unbb envl envr b b' acc
> un envl envr ty ty' acc'
View
@@ -51,6 +51,7 @@
> -- is for.
> data NameType = Bound | Free | DataCon | TypeCon | ElimOp
> | Unknown -- ^ Use for sending to typechecker.
+> deriving Show
> -- | Construct a term representing a variable
> mkVar :: String -- ^ Variable name
@@ -278,6 +279,26 @@
> dbgshow (UN n) = "UN " ++ show n
> dbgshow (MN (n,i)) = "MN [" ++ show n ++ "," ++ show i ++ "]"
+> -- | Match the second argument against the first, returning a list of
+> -- the names in the first paired with their matches in the second. Returns
+> -- Nothing if there is a match failure. There is no searching under binders.
+> match :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]
+> match t1 t2 = do acc <- m' t1 t2 []
+> checkDups acc [] where
+> m' (Name _ n) t acc = return ((n,t):acc)
+> m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc
+> = do acc' <- m' f f' acc
+> m' a a' acc'
+> m' x y acc | x == y = return acc
+> | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y
+
+> checkDups [] acc = return acc
+> checkDups ((x,t):xs) acc
+> = case lookup x xs of
+> Just t' -> if t == t' then checkDups xs acc
+> else fail $ "Mismatch on " ++ show x
+> Nothing -> checkDups xs ((x,t):acc)
+
> -- |Substitute a name n with a value v in a term f
> subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm
> subst n v nm@(Name _ p) | p == n = v
View
@@ -4,7 +4,7 @@ DB = --user
PREFIX = $(HOME)
# Set this to -p for profiling libraries too
-PROFILE =
+PROFILE =
CABALOPTS = -O
@@ -27,7 +27,7 @@ doc:
test:
make -C tests
-sdist:
+cabal-package:
runhaskell Setup.lhs sdist
jones: .PHONY package install
View
@@ -1,5 +1,5 @@
Name: ivor
-Version: 0.1.7
+Version: 0.1.8
Author: Edwin Brady
License: BSD3
License-file: LICENSE
@@ -10,7 +10,7 @@ Stability: experimental
Build-depends: base, haskell98, parsec, mtl, directory, containers
Extensions: MultiParamTypeClasses, FunctionalDependencies,
ExistentialQuantification, OverlappingInstances
-Category: Theorem provers
+Category: Theorem provers, Dependent Types
Synopsis: Theorem proving library based on dependent type theory
Description: Ivor is a type theory based theorem prover, with a
Haskell API, designed for easy extending and embedding

0 comments on commit ec67c2c

Please sign in to comment.