Pattern matching syntax

(but just the syntax, it doesn't work yet)

darcs-hash:20070118112457-974a0-98e1a260b9066033df50ebddfe73140741341b79.gz

Ivor/Datatype.lhs

@@ -68,8 +68,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)
->	 esch <- checkSchemes gamma''' er eschemes
->	 csch <- checkSchemes gamma''' er cschemes
+>	 esch <- mapM (checkScheme gamma''' er) eschemes
+>	 csch <- mapM (checkScheme gamma''' er) cschemes
 >	 return (Data (ty,G (TCon (arity gamma kv) erdata) kv) consv numps
 >                    (er,ev) (cr,cv) esch csch eschemes cschemes)
 
@@ -81,13 +81,6 @@ the context and an executable elimination rule.
 >		  (rest,gamma'') <- checkCons gamma' (t+1) cs
 >	          return (((cn,ccon):rest), gamma'')
 
-> checkSchemes :: Monad m => 
->	          Gamma Name -> Name -> [RawScheme] -> m [Scheme Name]
-> checkSchemes gamma n [] = return []
-> checkSchemes gamma n (i:is) = do di <- checkScheme gamma n i
->			           dis <- checkSchemes gamma n is
->				   return (di:dis)
-
 checkScheme takes a raw iota scheme and returns a scheme with a well-typed
 RHS (or fails if there is a type error).
 
@@ -113,7 +106,8 @@ Make a pattern from a raw term. Anything weird, just make it a "PTerm".
 >        where mkPatV n (Just (DCon t x)) = PCon t n tyname []
 >              mkPatV n (Just (TCon x _)) = PCon 0 n (UN "Type") []
 >              mkPatV n _ = PVar n
->              tyname = getTyName gam n
+>              tyname = case (getTyName gam n) of
+>                         Just x -> x
 > mkPat gam (RApp f a) = pat' (unwind f a)
 >   where unwind (RApp f s) a = let (f',as) = unwind f s in
 >				    (f',(mkPat gam a):as)
@@ -124,7 +118,8 @@ Make a pattern from a raw term. Anything weird, just make it a "PTerm".
 >         mkPatV n (Just (DCon t x)) as = PCon t n tyname as
 >         mkPatV n (Just (TCon x _)) as = PCon 0 n (UN "Type") as
 >         mkPatV _ _ _ = PTerm
->         tyname = getTyName gam (getname (getappfun f))
+>         tyname = case (getTyName gam (getname (getappfun f))) of
+>                    Just x -> x
 >         getname (Var n) = n
 > mkPat gam _ {-(RBind _ _ _)-} = PTerm
 > {-
@@ -134,16 +129,6 @@ Make a pattern from a raw term. Anything weird, just make it a "PTerm".
 > mkPat gam x = error $ "Can't make a pattern from " ++ show x
 > -}
 
-Given how we construct patterns, this can't fail. Oh yes.
-
-> getTyName :: Gamma Name -> Name -> Name
-> getTyName  gam n = case lookuptype n gam of
->                            Just (Ind ty) -> getFnName ty
->   where getFnName (TyCon x _) = x
->         getFnName (App f x) = getFnName f
->         getFnName (Bind _ _ (Sc x)) = getFnName x
->         getFnName x = MN ("Dunno: "++show x, 0)
-
 Get the pattern variables from the patterns, and work out what the projection 
 function for each name is.
 

Ivor/Nobby.lhs

@@ -66,6 +66,17 @@ to do with it, when the time comes.
 > glookup ::  Eq n => n -> Gamma n -> Maybe (Global n,Indexed n)
 > glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (lookup n xs)
 
+Get a type name from the context
+
+> getTyName :: Monad m => Gamma Name -> Name -> m Name
+> getTyName  gam n = case lookuptype n gam of
+>                            Just (Ind ty) -> return $ getFnName ty
+>                            Nothing -> fail $ "No such name " ++ show n
+>   where getFnName (TyCon x _) = x
+>         getFnName (App f x) = getFnName f
+>         getFnName (Bind _ _ (Sc x)) = getFnName x
+>         getFnName x = MN ("Dunno: "++show x, 0)
+
 > insertGam :: n -> Gval n -> Gamma n -> Gamma n
 > insertGam nm val (Gam gam) = Gam $ (nm,val):gam
 

Ivor/PatternDefs.lhs

@@ -0,0 +1,45 @@
+> {-# OPTIONS_GHC -fglasgow-exts #-}
+
+> module Ivor.PatternDefs where
+
+> import Ivor.Gadgets
+> import Ivor.TTCore
+> import Ivor.Datatype
+> import Ivor.Nobby
+> import Ivor.Typecheck
+
+> import Debug.Trace
+
+Use the iota schemes from Datatype to represent pattern matching definitions.
+
+> type PMRaw = RawScheme
+> type PMDef n = Scheme n
+
+> data PMFun n = PMFun [PMDef n]
+>    deriving Show
+
+> checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> m (PMFun Name)
+> checkDef gam n ty rschs = do 
+>     schs <- mapM (checkClause gam n ty) rschs
+>     -- TODO: Coverage and termination checking
+>     return $ PMFun schs
+
+> checkClause :: Monad m => Gamma Name -> Name -> Raw -> PMRaw -> 
+>                m (PMDef Name)
+> checkClause gam n ty sch@(RSch args ret) = trace (show sch) $ do
+>     (argscheck, bs) <- checkArgs [] args ty
+>     (ret, _) <- check gam bs (getrettype ty) Nothing
+>     return $ Sch argscheck ret
+>   where checkArgs bindings [] _ = return ([], bindings)
+>         checkArgs bindings (x:xs) (RBind nm (B Pi t) ts) = trace (show x ++ " : " ++ show t ++ ", " ++ show bindings) $ do
+>             (xcheck, bs) <- checkPatt gam bindings Nothing x t
+>             (Ind tyc, _) <- check gam bs t (Just (Ind Star))
+>             (xscheck, bs') <- checkArgs ((nm,B Pi tyc):bs) xs ts
+>             return (xcheck:xscheck, bs')
+
+         mkEnv = map (\ (n,Ind t) -> (n, B Pi t))
+
+
+
+ checkClause gam n (RSch pats ret) =
+

Ivor/Shell.lhs

@@ -100,6 +100,9 @@
 > runCommand (TypedDef nm tm ty) st = do
 >     ctxt <- addTypedDef (context st) (name nm) tm ty
 >     return st { context = ctxt }
+> runCommand (PatternDef nm ty pats) st = do
+>     ctxt <- addPatternDef (context st) (name nm) ty pats
+>     return st { context = ctxt }
 > runCommand (Data dat) st = do ctxt <- addData (context st) dat
 >                               return st { context = ctxt }
 > runCommand (Axiom nm tm) st = do ctxt <- addAxiom (context st) (name nm) tm

Ivor/ShellParser.lhs

@@ -36,6 +36,7 @@
 
 > data Command = Def String ViewTerm
 >              | TypedDef String ViewTerm ViewTerm
+>              | PatternDef String ViewTerm Patterns
 >              | Data Inductive
 >              | Axiom String ViewTerm
 >              | Declare String ViewTerm
@@ -115,6 +116,28 @@ which runs it.
 >          lchar '=' ; term <- pTerm ext ; semi
 >          return $ TypedDef name term ty
 
+> pclause :: Maybe (Parser ViewTerm) -> Parser PClause
+> pclause ext
+>     = do name <- identifier; 
+>          args <- many (pNoApp ext)
+>          lchar '=' ;
+>          ret <- pTerm ext
+>          return $ PClause args ret
+
+> ppatterns :: Maybe (Parser ViewTerm) -> Parser Patterns
+> ppatterns ext
+>     = do clauses <- sepBy (pclause ext) (lchar '|' )
+>          return $ Patterns clauses
+
+> ppatternDef :: Maybe (Parser ViewTerm) -> Parser Command
+> ppatternDef ext
+>     = do reserved "Patt"
+>          name <- identifier ; lchar ':' ; ty <- pTerm ext
+>          lchar '='
+>          patts <- ppatterns ext
+>          semi
+>          return $ PatternDef name ty patts
+
 > pdata :: Maybe (Parser ViewTerm) -> Parser Command
 > pdata ext = do reserved "Data"
 >                datadef <- pInductive ext ; semi
@@ -270,7 +293,7 @@ which runs it.
 > command :: Maybe (Parser ViewTerm) -> Parser Command
 > command ext = tryall [def ext, typeddef ext, pdata ext, axiom ext, 
 >                       ptheorem ext, pdeclare ext, pinter ext, pforget, 
->                       eval ext, check ext, 
+>                       eval ext, check ext, ppatternDef ext,
 >                       pdrop, repldata, pqed, pprint, pfreeze, pthaw, pprf, 
 >                       pundo, psuspend, presume, pgenrec, pjme,
 >                       pload, pcompile, pfocus, pdump, pprfstate, pprims,

Ivor/TT.lhs

@@ -23,6 +23,8 @@
 >               theorem,interactive,
 >               addPrimitive,addBinOp,addPrimFn,addExternalFn,
 >               addEquality,forgetDef,addGenRec,
+>               -- * Pattern matching definitions
+>               PClause(..), Patterns(..),addPatternDef,
 >               -- * Manipulating Proof State
 >               proving,numUnsolved,suspend,resume,
 >               save, restore, clearSaved,
@@ -100,6 +102,7 @@
 > import qualified Ivor.Tactics as Tactics
 > import Ivor.Compiler as Compiler
 > import Ivor.CodegenC
+> import Ivor.PatternDefs
 
 > import List
 > import Debug.Trace
@@ -186,6 +189,28 @@
 >                                 Just _ -> fail $ show n ++ " already defined"
 >                                 Nothing -> return ()
 
+> data PClause = PClause {
+>                         arguments :: [ViewTerm],
+>                         returnval :: ViewTerm
+>                        }
+
+> data Patterns = Patterns [PClause]
+
+> mkRawClause :: PClause -> RawScheme
+> mkRawClause (PClause args ret) =
+>     RSch (map forget args) (forget ret)
+
+> -- |Add a new definition, with its type to the global state.
+> -- These definitions can be recursive, so use with care.
+> addPatternDef :: (IsTerm ty, Monad m) => 
+>                Context -> Name -> ty -> Patterns -> m Context
+> addPatternDef (Ctxt st) n ty pats = do
+>         checkNotExists n (defs st)
+>         inty <- raw ty
+>         let (Patterns clauses) = pats
+>         foo <- checkDef (defs st) n inty (map mkRawClause clauses)
+>         trace (show foo) $ fail "unfinished"
+
 > -- |Add a new definition, with its type to the global state.
 > -- These definitions can be recursive, so use with care.
 > addTypedDef :: (IsTerm term, IsTerm ty, Monad m) => 

Ivor/Typecheck.lhs

@@ -260,6 +260,48 @@ Insert inferred values into the term
 >       (Ind Star) -> return (B (Guess vv) tv)
 >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
 
+Check a raw term representing a pattern. Return the pattern, and the 
+extended environment.
+
+> checkPatt :: Monad m => Gamma Name -> Env Name -> Maybe (Pattern Name) ->
+>              Raw -> Raw -> 
+>              m (Pattern Name, Env Name)
+> checkPatt gam env acc (Var n) ty = trace (show n ++ ": "++ show env) $ do
+>      (Ind tyc, _) <- check gam env ty (Just (Ind Star))
+>      (pat, t) <- mkVarPatt (lookupi n env 0) (glookup n gam) (Ind tyc)
+>      --checkConvEnv env gam (Ind tyc) (Ind t) $
+>      --   show ty ++ " and " ++ show t ++ " are not convertible"
+>      return (combinepats acc pat, (n, (B Pi tyc)):env)
+>   where
+>        mkVarPatt (Just (i, B _ t)) _ _ = return (PVar n, t)
+>        mkVarPatt Nothing (Just ((DCon tag i), (Ind t))) _
+>            = do tyname <- getTyName gam n
+>                 return (PCon tag n tyname [], t)
+>        mkVarPatt Nothing Nothing (Ind defty) = return (PVar n, defty)
+>        lookupi x [] _ = Nothing
+>        lookupi x ((n,t):xs) i | x == n = Just (i,t)
+>        lookupi x (_:xs) i = lookupi x xs (i+1)
+
+> checkPatt gam env acc (RApp f a) ty = do
+>      (Ind tyc, _) <- trace (show ty) $ check gam env ty (Just (Ind Star))
+>      let (RBind _ _ fscope) = ty
+>      let (Bind nm (B _ nmt) _) = tyc
+>      (fpat, fbindingsin) <- checkPatt gam env Nothing f ty
+>      let fbindings = ((nm,(B Pi nmt)):fbindingsin)
+>      (apat, abindings) <- checkPatt gam (fbindings++env) 
+>                                       (Just fpat) a fscope
+>      return (combinepats (Just fpat) apat, fbindings++abindings)
+
+   where
+        mkEnv = map (\ (n,Ind t) -> (n, B Pi t))
+
+> checkPatt gam env acc RInfer ty = return (combinepats acc PTerm, env)
+> checkPatt gam env _ _ _ = fail "Invalid pattern"
+
+> combinepats Nothing x = x
+> combinepats (Just (PVar n)) x = error "can't apply things to a variable"
+> combinepats (Just (PCon tag n ty args)) x = PCon tag n ty (args++[x])
+
 > discharge :: Monad m =>
 >              Gamma Name -> Name -> Binder (TT Name) -> 
 >	       (Scope (TT Name)) -> (Scope (TT Name)) ->

ivor.cabal

@@ -20,5 +20,6 @@ Other-modules:	Ivor.Nobby, Ivor.TTCore, Ivor.State,
 		Ivor.CodegenC, Ivor.Datatype, Ivor.Display,
 		Ivor.ICompile, Ivor.MakeData, Ivor.Unify,
 		Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,
-		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix
+		Ivor.RunTT, Ivor.Compiler, Ivor.Prefix,
+		Ivor.PatternDefs
 

lib/vect.tt

@@ -4,6 +4,12 @@ Data Vect (A:*):(n:Nat)*
     = vnil:Vect A O
     | vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);
 
+Patt lookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A {
+    lookup _ _ (fz _) (vcons _ _ x xs) = x
+  | lookup _ _ (fs _ i) (vcons _ _ x xs) = lookup _ _ i xs
+};
+
+
 Data Fin : (n:Nat)*
     = fz : (k:Nat)(Fin (S k))
     | fs : (k:Nat)(i:Fin k)(Fin (S k));