Skip to content
Browse files

Added specialise option to pattern defs

Ignore-this: c9a643ce1ca6b02f82f7b5bd367e6d9f

darcs-hash:20100119142313-228f4-e62df8bf7a68dc44db3bb9b040cd82ed4eb99326.gz
  • Loading branch information...
1 parent 203a435 commit 75b1dab5fc99b759a2e6e6f46626fb531a7649e1 eb committed Jan 19, 2010
Showing with 22 additions and 9 deletions.
  1. +2 −2 Ivor/Datatype.lhs
  2. +13 −6 Ivor/PatternDefs.lhs
  3. +6 −0 Ivor/TT.lhs
  4. +1 −1 ivor.cabal
View
4 Ivor/Datatype.lhs
@@ -63,8 +63,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 Nothing
+> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing
> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
> (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)
View
19 Ivor/PatternDefs.lhs
@@ -9,6 +9,7 @@
> import Ivor.Unify
> import Ivor.Errors
> import Ivor.Values
+> import Ivor.Evaluator
> import Debug.Trace
> import Data.List
@@ -24,8 +25,9 @@ Also return whether the function is definitely total.
> checkDef :: Gamma Name -> Name -> Raw -> [PMRaw] ->
> Bool -> -- Check for coverage
> Bool -> -- Check for well-foundedness
+> Maybe [(Name, Int)] -> -- Names to specialise
> IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
-> checkDef gam fn tyin pats cover wellfounded = do
+> checkDef gam fn tyin pats cover wellfounded spec = 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
@@ -37,7 +39,7 @@ Also return whether the function is definitely total.
> checkNotExists fn gam
> gam' <- gInsert fn (G Undefined ty defplicit) gam
> clauses' <- validClauses gam' fn ty clauses'
-> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses'
+> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec
> wf <- return True
> {- if wellfounded then
> do checkWellFounded gam fn [0..arity-1] pmdef
@@ -175,13 +177,14 @@ 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.
-Each clause may generate auxiliary definitions, so return all definitons created.
+Each clause may generate auxiliary definitions, so return all definitions created.
> matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name ->
> Bool -> -- Check coverage
> [(Indexed Name, Indexed Name)] ->
+> Maybe [(Name, Int)] ->
> IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
-> matchClauses gam fn pats tyin ty@(Ind ty') cover gen = do
+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec = do
> let raws = zip (map mkRaw pats) (map getRet pats)
> (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True
> cv <- if cover then
@@ -217,7 +220,11 @@ Each clause may generate auxiliary definitions, so return all definitons created
> let namesbound = getNames (Sc tmtt)
> checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
> -- trace (show env) $
-> return ((tm, Ind rtmtt', env), [], newdefs, True)
+> let specrtm = case spec of
+> Nothing -> Ind rtmtt'
+> Just [] -> eval_nf gam (Ind rtmtt')
+> Just ns -> trace (show (rtmtt', ns)) $ eval_nf_limit gam (Ind rtmtt') ns
+> return ((tm, specrtm, env), [], newdefs, True)
> mytypecheck gam (clause, (RWith addprf scr pats)) i =
> do -- Get the type of scrutinee, construct the type of the auxiliary definition
> (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn
@@ -244,7 +251,7 @@ Each clause may generate auxiliary definitions, so return all definitons created
> let gam' = insertGam newname (G Undefined newfnTy 0) gam
> newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats)
> (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i
-> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover
+> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec
> return (chk, auxdefs++auxdefs', newdefs, covers)
> addLastArg (RBind n (B Pi arg) x) ty scr addprf
View
6 Ivor/TT.lhs
@@ -308,6 +308,7 @@
> 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.
+> | Specialise [(Name, Int)] -- ^ Specialise the right hand side
> deriving Eq
> -- |Add a new definition to the global state.
@@ -329,6 +330,7 @@
> <- tt $ checkDef ndefs n inty (map mkRawClause clauses)
> (not (elem Ivor.TT.Partial opts))
> (not (elem GenRec opts))
+> (getSpec opts)
> (ndefs',vnewnames)
> <- if (null newnames) then return (ndefs, [])
> else do when (not (Holey `elem` opts)) $
@@ -347,6 +349,10 @@
> insertAll xs gam' tot
> gen nm = nm /= n -- generated if it's not the provided name.
+> getSpec [] = Nothing
+> getSpec (Specialise fns:_) = Just fns
+> getSpec (_:xs) = getSpec xs
+
> -- |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) =>
View
2 ivor.cabal
@@ -1,5 +1,5 @@
Name: ivor
-Version: 0.1.10.1
+Version: 0.1.12
Author: Edwin Brady
License: BSD3
License-file: LICENSE

0 comments on commit 75b1dab

Please sign in to comment.
Something went wrong with that request. Please try again.