(Almost) implemented metavariables in pattern matching definitions

Still need to abstract over any local names in the generated type for the hole.

darcs-hash:20080314011734-228f4-e14db3ad9aea7f8803139fd8304279f740d3fcff.gz

Ivor/Datatype.lhs

@@ -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) esch csch eschemes cschemes)
 

Ivor/PatternDefs.lhs

@@ -14,10 +14,13 @@
 
 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.
+
 > checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> 
 >             Bool -> -- Check for coverage
 >             Bool -> -- Check for well-foundedness
->             m (PMFun Name, Indexed Name)
+>             m (PMFun Name, Indexed Name, [(Name, Indexed Name)])
 > 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")]])
@@ -29,9 +32,9 @@ Use the iota schemes from Datatype to represent pattern matching definitions.
 >   checkNotExists fn gam
 >   gam' <- gInsert fn (G Undefined ty defplicit) gam
 >   clauses' <- validClauses gam' fn ty clauses'
->   pmdef <- matchClauses gam' fn pats tyin cover clauses'
+>   (pmdef, newdefs) <- matchClauses gam' fn pats tyin cover clauses'
 >   when wellfounded $ checkWellFounded gam fn [0..arity-1] pmdef
->   return (PMFun arity pmdef, ty)
+>   return (PMFun arity pmdef, ty, newdefs)
 >     where checkNotExists n gam = case lookupval n gam of
 >                                 Just Undefined -> return ()
 >                                 Just _ -> fail $ show n ++ " already defined"
@@ -163,12 +166,13 @@ 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]
+>                 [(Indexed Name, Indexed Name)] -> 
+>                 m ([PMDef Name], [(Name, Indexed Name)])
 > matchClauses gam fn pats tyin cover gen = do
 >    let raws = zip (map mkRaw pats) (map getRet pats)
->    checkpats <- mapM (mytypecheck gam) raws
+>    (checkpats, newdefs) <- mytypechecks gam raws [] []
 >    when cover $ checkCoverage (map fst checkpats) (map fst gen)
->    return $ map (mkScheme gam) checkpats
+>    return $ (map (mkScheme gam) checkpats, newdefs)
 
     where mkRaw (RSch pats r) = mkPBind pats tyin r
           mkPBind [] _ r = r
@@ -177,20 +181,26 @@ names bound in patterns) then type check the right hand side.
 
 >   where mkRaw (RSch pats r) = mkapp (Var fn) pats
 >         getRet (RSch pats r) = r
+>         mytypechecks gam [] acc defs = return (reverse acc, defs)
+>         mytypechecks gam (c:cs) acc defs
+>             = do (cl, cr, newdefs) <- mytypecheck gam c
+>                  mytypechecks gam cs ((cl,cr):acc) (defs++newdefs)
 >         mytypecheck gam (clause, ret) = 
 >             do (tm@(Ind tmtt), pty,
->                 rtm@(Ind rtmtt), rty, env) <-
+>                 rtm@(Ind rtmtt), rty, env, newdefs) <-
 >                   checkAndBindPair gam clause ret
 >                unified <- unifyenv gam env pty rty
+>                let gam' = foldl (\g (n,t) -> extend g (n,G Undefined t 0))
+>                                   gam newdefs
 >                let rtmtt' = substNames unified rtmtt
 >                -- checkConvEnv env gam pty rty $ "Pattern error: " ++ show pty ++ " and " ++ show rty ++ " are not convertible " ++ show unify
->                let namesret = filter notGlobal $ getNames (Sc rtmtt')
+>                let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt')
 >                let namesbound = getNames (Sc tmtt)
 >                checkAllBound namesret namesbound (Ind rtmtt') tmtt
->                return (tm, Ind rtmtt')
->         notGlobal n = case lookupval n gam of
->                         Nothing -> True
->                         _ -> False
+>                return (tm, Ind rtmtt', newdefs)
+>         notGlobal gam n = case lookupval n gam of
+>                               Nothing -> True
+>                               _ -> False
 >         checkAllBound r b rhs clause = do
 >              let unbound = filter (\y -> not (elem y b)) r
 >              if (length unbound == 0) 

Ivor/Shell.lhs

@@ -105,8 +105,9 @@
 >     ctxt <- addTypedDef (context st) (name nm) tm ty
 >     return st { context = ctxt }
 > runCommand (PatternDef nm ty pats opts) st = do
->     ctxt <- addPatternDef (context st) (name nm) ty pats opts
->     return st { context = ctxt }
+>     (ctxt, new) <- addPatternDef (context st) (name nm) ty pats (Holey:opts)
+>     let st' = respondLn st $ ("Need to define: " ++ show new)
+>     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/TT.lhs

@@ -109,6 +109,7 @@
 > import List
 > import Debug.Trace
 > import Data.Typeable
+> import Control.Monad(when)
 
 > -- | Abstract type representing state of the system.
 > newtype Context = Ctxt IState
@@ -207,25 +208,40 @@
 
 > data PattOpt = Partial -- ^ No need to cover all cases
 >              | GenRec -- ^ No termination checking
+>              | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved.
 >   deriving Eq
 
 > -- |Add a new definition to the global state.
 > -- By default, these definitions must cover all cases and be well-founded,
-> -- but can be optionally partial or general recursive
+> -- but can be optionally partial or general recursive.
+> -- Returns the new context, and a list of names which need to be defined
+> -- to complete the definition.
 > addPatternDef :: (IsTerm ty, Monad m) => 
 >                Context -> Name -> ty -- ^ Type
 >                  -> Patterns -- ^ Definition
 >                -> [PattOpt] -- ^ Options to set which definitions will be accepted
->                -> m Context
+>                -> m (Context, [(Name, ViewTerm)])
 > addPatternDef (Ctxt st) n ty pats opts = do
 >         checkNotExists n (defs st)
+>         let ndefs = defs st
 >         inty <- raw ty
 >         let (Patterns clauses) = pats
->         (pmdef, fty) <- checkDef (defs st) n inty (map mkRawClause clauses)
+>         (pmdef, fty, newnames) 
+>                <- checkDef ndefs n inty (map mkRawClause clauses)
 >                            (not (elem Ivor.TT.Partial opts))
 >                            (not (elem GenRec opts))
->         newdefs <- gInsert n (G (PatternDef pmdef) fty defplicit) (defs st)
->         return $ Ctxt st { defs = newdefs }
+>         (ndefs',vnewnames) 
+>                <- if (null newnames) then return (ndefs, [])
+>                      else do when (not (Holey `elem` opts)) $ 
+>                                    fail "No metavariables allowed"
+>                              let vnew = map (\ (n,t) -> 
+>                                              (n, view (Term (t,Ind TTCore.Star)))) newnames
+>                              let ngam = foldl (\g (n, t) ->
+>                                                  extend g (n, G Unreducible t 0))
+>                                               ndefs newnames
+>                              return (ngam, vnew)
+>         newdefs <- gInsert n (G (PatternDef pmdef) fty defplicit) ndefs'
+>         return (Ctxt st { defs = newdefs }, vnewnames)
 
 > -- |Add a new definition, with its type to the global state.
 > -- These definitions can be recursive, so use with care.

Ivor/TTCore.lhs

@@ -45,6 +45,7 @@ representation of the names
 >     | V Int
 >     | Con Int n Int -- Tag, name and arity
 >     | TyCon n Int  -- Name and arity
+>     | Meta n (TT n) -- Metavariable and its type
 >     | Elim n
 >     | App (TT n) (TT n)
 >     | Bind n (Binder (TT n)) (Scope (TT n))
@@ -188,6 +189,7 @@ is dealt with later.
 >     fmap f (V i) = V i
 >     fmap f (Con t x i) = Con t (f x) i
 >     fmap f (TyCon x i) = TyCon (f x) i
+>     fmap f (Meta x t) = Meta (f x) (fmap f t)
 >     fmap f (Elim x) = Elim (f x)
 >     fmap f (App tf a) = App (fmap f tf) (fmap f a)
 >     fmap f (Bind n b sc) = Bind (f n) (fmap (fmap f) b) (fmap (fmap f) sc)
@@ -274,6 +276,7 @@ Same, but for Ps
 >   where
 >     v' (P n) = f n
 >     v' (V i) = V i
+>     v' (Meta n t) = Meta n (v' t)
 >     v' (App f' a) = (App (v' f') (v' a))
 >     v' (Bind n b (Sc sc)) = (Bind n (fmap (v') b) 
 >			          (Sc (v' sc)))
@@ -434,6 +437,33 @@ maybe find a better way, or think carefully about why this is okay...
 >         vinc (V n) = V (n+1) -- So that we weakenv it correctly
 >         vinc x = x
 
+Traverse a term looking for metavariables. Replace them with concrete
+names and return all the new names we need to define for it to be
+a complete definition.
+
+> updateMetas :: TT n -> (TT n, [(n, TT n)])
+> updateMetas tm = runState (ums tm) []
+>    where ums (App f a) = do f' <- ums f
+>                             a' <- ums a
+>                             return (App f' a')
+>          ums (Meta n ty) = do ty' <- ums ty
+>                               mvs <- get
+>                               put ((n,ty'):mvs)
+>                               return (P n)
+>          ums (Bind n (B b ty) (Sc sc)) 
+>                  = do b' <- umsB b
+>                       ty' <- ums ty
+>                       sc' <- ums sc
+>                       return (Bind n (B b' ty') (Sc sc'))
+>          ums x = return x
+>          umsB (Let v) = do v' <- ums v
+>                            return (Let v')
+>          umsB (Guess v) = do v' <- ums v
+>                              return (Guess v')
+>          umsB (Pattern v) = do v' <- ums v
+>                                return (Pattern v')
+>          umsB x = return x
+
 Return all the names used in a scope
 
 > getNames :: Eq n => Scope (TT n) -> [n]
@@ -614,6 +644,7 @@ Apply a function to a list of arguments
 >     (==) (V i) (V j) = i==j
 >     (==) (Con t x i) (Con t' y j) = x==y
 >     (==) (TyCon x i) (TyCon y j) = x==y
+>     (==) (Meta x t) (Meta y t') = x==y && t==t'
 >     (==) (Elim x) (Elim y) = x==y
 >     (==) (App f a) (App f' a') = f==f' && a==a'
 >     (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc'
@@ -712,6 +743,7 @@ Apply a function to a list of arguments
 >        forgetTT (V i) = RAnnot $ "v" ++ (show i)
 >        forgetTT (Con t x i) = Var $ UN (show x)
 >        forgetTT (TyCon x i) = Var $ UN (show x)
+>        forgetTT (Meta n i) = RMeta (UN (show n ++ " : " ++ show i))
 >        forgetTT (Elim x) = Var $ UN (show x)
 >        forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
 >        forgetTT (Bind n (B Lambda t) (Sc sc)) =
@@ -798,6 +830,7 @@ Some handy gadgets for Raw terms
 >        forgetTT (V i) = RAnnot $ "v" ++ (show i)
 >        forgetTT (Con t x i) = Var $ UN (show x)
 >        forgetTT (TyCon x i) = Var $ UN (show x)
+>        forgetTT (Meta x i) = RMeta (UN (show x))
 >        forgetTT (Elim x) = Var $ UN (show x)
 >        forgetTT (App f a) = RApp (forgetTT f) (forgetTT a)
 >        forgetTT (Bind n (B Lambda t) (Sc sc)) =