Changed pattern syntax, and added options

(Partial, and Rec, although they currently do nothing)t

darcs-hash:20070129004404-974a0-9562c0ae1eae68e4755010318e6690e4da4e60bc.gz

Ivor/PatternDefs.lhs

@@ -10,12 +10,15 @@
 
 > import Debug.Trace
 > import Data.List
+> import Monad
 
 Use the iota schemes from Datatype to represent pattern matching definitions.
 
 > checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> 
+>             Bool -> -- Check for coverage
+>             Bool -> -- Check for well-foundedness
 >             m (PMFun Name, Indexed Name)
-> checkDef gam fn tyin pats = do 
+> 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")]])
 >   clausesIn <- mapM (expandClause gam) pats
@@ -26,8 +29,8 @@ Use the iota schemes from Datatype to represent pattern matching definitions.
 >   checkNotExists fn gam
 >   gam' <- gInsert fn (G Undefined ty) gam
 >   clauses' <- validClauses gam' fn ty clauses'
->   pmdef <- matchClauses gam' fn pats tyin clauses'
->   checkWellFounded pmdef
+>   pmdef <- matchClauses gam' fn pats tyin cover clauses'
+>   when wellfounded $ checkWellFounded pmdef
 >   return (PMFun arity pmdef, ty)
 >     where checkNotExists n gam = case lookupval n gam of
 >                                 Just Undefined -> return ()
@@ -48,12 +51,13 @@ For each Raw clause, try to match it against a generated and checked clause.
 Match up the inferred arguments to the names (so getting the types of the
 names bound in patterns) then type check the right hand side.
 
-> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw -> 
+> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw ->
+>                 Bool -> -- Check coverage
 >                 [(Indexed Name, Indexed Name)] -> m [PMDef Name]
-> matchClauses gam fn pats tyin gen = do
+> matchClauses gam fn pats tyin cover gen = do
 >    let raws = zip (map mkRaw pats) (map getRet pats)
 >    checkpats <- mapM (mytypecheck gam) raws
->    checkCoverage (map fst checkpats) (map fst gen)
+>    when cover $ checkCoverage (map fst checkpats) (map fst gen)
 >    return $ map (mkScheme gam) checkpats
 
     where mkRaw (RSch pats r) = mkPBind pats tyin r

Ivor/Shell.lhs

@@ -100,8 +100,8 @@
 > 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
+> runCommand (PatternDef nm ty pats opts) st = do
+>     ctxt <- addPatternDef (context st) (name nm) ty pats opts
 >     return st { context = ctxt }
 > runCommand (Data dat) st = do ctxt <- addData (context st) dat
 >                               return st { context = ctxt }
@@ -175,9 +175,10 @@
 >                         let st' = respondLn st $ 
 >                                      showProofState st { context = ctxt }
 >                         return st' { context = ctxt }
-> runCommand (GenRec n) st = do ctxt <- addGenRec (context st) (name n)
->                               let st' = respondLn st $ "Added general recursion rule"
->                               return st' { context = ctxt }
+> runCommand (Ivor.ShellParser.GenRec n) st 
+>     = do ctxt <- addGenRec (context st) (name n)
+>          let st' = respondLn st $ "Added general recursion rule"
+>          return st' { context = ctxt }
 > runCommand (JMEq n c) st = do ctxt <- addEquality (context st) (name n) 
 >                                         (name c)
 >                               let st' = respondLn st $ "Added dependent equality"

Ivor/ShellParser.lhs

@@ -37,7 +37,7 @@
 
 > data Command = Def String ViewTerm
 >              | TypedDef String ViewTerm ViewTerm
->              | PatternDef String ViewTerm Patterns
+>              | PatternDef String ViewTerm Patterns [PattOpt]
 >              | Data Inductive
 >              | Axiom String ViewTerm
 >              | Declare String ViewTerm
@@ -131,14 +131,21 @@ which runs it.
 >     = do clauses <- sepBy (pclause name ext) (lchar '|' )
 >          return $ Patterns clauses
 
+> pPattOpt :: Parser PattOpt
+> pPattOpt = do reserved "Partial"
+>               return Partial
+>            <|> do reserved "Rec"
+>                   return Ivor.TT.GenRec
+
 > ppatternDef :: Maybe (Parser ViewTerm) -> Parser Command
 > ppatternDef ext
->     = do reserved "Patt"
+>     = do reserved "Match"
+>          opts <- many pPattOpt
 >          name <- identifier ; lchar ':' ; ty <- pTerm ext
 >          lchar '='
 >          patts <- ppatterns name ext
 >          semi
->          return $ PatternDef name ty patts
+>          return $ PatternDef name ty patts opts
 
 > pdata :: Maybe (Parser ViewTerm) -> Parser Command
 > pdata ext = do reserved "Data"
@@ -213,7 +220,7 @@ which runs it.
 > pgenrec :: Parser Command
 > pgenrec = do reserved "General" ; 
 >              nm <- identifier ; semi
->              return $ GenRec nm
+>              return $ Ivor.ShellParser.GenRec nm
 
 > pjme :: Parser Command
 > pjme = do reserved "Equality" ; 

Ivor/TT.lhs

@@ -24,7 +24,7 @@
 >               addPrimitive,addBinOp,addPrimFn,addExternalFn,
 >               addEquality,forgetDef,addGenRec,
 >               -- * Pattern matching definitions
->               PClause(..), Patterns(..),addPatternDef,
+>               PClause(..), Patterns(..),PattOpt(..),addPatternDef,
 >               -- * Manipulating Proof State
 >               proving,numUnsolved,suspend,resume,
 >               save, restore, clearSaved,
@@ -200,15 +200,23 @@
 > mkRawClause (PClause args ret) =
 >     RSch (map forget args) (forget ret)
 
+> data PattOpt = Partial -- ^ No need to cover all cases
+>              | GenRec -- ^ No termination checking
+>   deriving Eq
+
 > -- |Add a new definition, with its type to the global state.
-> -- These definitions can be recursive, so use with care.
+> -- By default, these definitions must cover all cases and be well-founded,
+> -- but can be optionally partial/general recursive
 > addPatternDef :: (IsTerm ty, Monad m) => 
->                Context -> Name -> ty -> Patterns -> m Context
-> addPatternDef (Ctxt st) n ty pats = do
+>                Context -> Name -> ty -> Patterns -> 
+>                [PattOpt] -> -- ^ Options to set which definitions will be accepted
+>                m Context
+> addPatternDef (Ctxt st) n ty pats opts = do
 >         checkNotExists n (defs st)
 >         inty <- raw ty
 >         let (Patterns clauses) = pats
 >         (pmdef, fty) <- checkDef (defs st) n inty (map mkRawClause clauses)
+>                            (elem Ivor.TT.Partial opts) (elem GenRec opts)
 >         newdefs <- gInsert n (G (PatternDef pmdef) fty) (defs st)
 >         return $ Ctxt st { defs = newdefs }
 
@@ -494,9 +502,9 @@ Slightly annoying, but we'll cope.
 > resume :: Monad m => Context -> Name -> m Context
 > resume ctxt@(Ctxt st) n = 
 >     case glookup n (defs st) of
->         Just ((Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
->                                      st' <- resumeProof st n
->                                      return (Ctxt st')
+>         Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
+>                                                 st' <- resumeProof st n
+>                                                 return (Ctxt st')
 >         Just (Unreducible,ty) -> 
 >             do let st' = st { defs = remove n (defs st) }
 >                theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))

tests/patt.tt

@@ -7,11 +7,11 @@ Data ValEnv : (n:Nat)(G:Env n)* =
  | extend : (T:*)(t:T)(n:Nat)(G:Env n)(Gv:ValEnv n G)
               (ValEnv (S n) (vcons * n T G));
 
-Patt vlookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
+Match vlookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
     vlookup _ _ (fz _) (vcons _ _ x xs) = x
   | vlookup _ _ (fs n i) (vcons _ n x xs) = vlookup _ _ i xs;
 
-Patt envlookup : (n:Nat)(i:Fin n)(G:Env n)(Gv:ValEnv n G)(vlookup _ _ i G) =
+Match envlookup : (n:Nat)(i:Fin n)(G:Env n)(Gv:ValEnv n G)(vlookup _ _ i G) =
     envlookup _ (fz _) _ (extend _ t _ _ r) = t
   | envlookup _ (fs _ i) _ (extend _ t _ _ r) = envlookup _ i _ r;
 
@@ -33,11 +33,11 @@ Data Le : (n:Nat)(m:Nat)* =
    leO : (n:Nat)(Le O n)
  | leS : (n,m:Nat)(Le n m)->(Le (S n) (S m)); 
 
-Patt minus : (m,n:Nat)(Le n m)->Nat =
+Match minus : (m,n:Nat)(Le n m)->Nat =
     minus m O (leO m) = m
   | minus (S m) (S n) (leS n m p) = minus m n p;
 
-Patt plusp : Nat -> Nat -> Nat =
+Match plusp : Nat -> Nat -> Nat =
     plusp O x = x
   | plusp (S x) y = S (plusp x y);
 
@@ -46,7 +46,7 @@ Data tree (A:*) : (n:Nat)* =
  | node : (n:Nat)(left:tree A n)(a:A)
           (m:Nat)(right:tree A m)(tree A (S (plus n m)));
 
-Patt treeSum : (n:Nat)(t:tree Nat n)Nat =
+Match treeSum : (n:Nat)(t:tree Nat n)Nat =
    treeSum _ (leaf _) = O
  | treeSum _ (node _ _ l a _ r) = plus a (plus (treeSum _ l) (treeSum _ r));
 
@@ -55,11 +55,11 @@ testTree = node _ _ (node _ _ (leaf _) (S (S O)) _ (leaf _)) O
 
 testvec = (vcons _ _ (S (S (S (S O)))) (vcons _ _ (S (S (S O))) (vcons _ _ (S (S O)) (vnil Nat))));
 
-Patt vadd : (n:Nat)(xs,ys:Vect Nat n)->(Vect Nat n) =
+Match vadd : (n:Nat)(xs,ys:Vect Nat n)->(Vect Nat n) =
     vadd _ (vnil _) (vnil _) = vnil Nat
   | vadd _ (vcons _ _ x xs) (vcons _ _ y ys)
        = vcons _ _ (plus x y) (vadd _ xs ys);
 
-Patt vtail : (A:*)(n:Nat)(xs:Vect A (S n))(Vect A n) =
+Match vtail : (A:*)(n:Nat)(xs:Vect A (S n))(Vect A n) =
     vtail _ _ (vcons _ _ _ xs) = xs;