Skip to content

Commit

Permalink
Added SpecStatic option
Browse files Browse the repository at this point in the history 
Ignore-this: c216ffd1754ede464d2c9c1fced0167

darcs-hash:20100428110142-228f4-96b0c7d5193f78c80d25ae14d8b864c5f1ea0b39.gz
  • Loading branch information
eb committed Apr 28, 2010
1 parent 4fde442 commit c138e8a
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 31 deletions.
4 changes: 2 additions & 2 deletions Ivor/Datatype.lhs
View file
Expand Up @@ -63,8 +63,8 @@ the context and an executable elimination rule.
> (ev, _) <- typecheck gamma'' erty > (ev, _) <- typecheck gamma'' erty
> (cv, _) <- typecheck gamma'' crty > (cv, _) <- typecheck gamma'' crty
> -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit) > -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)
> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False Nothing > ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False Nothing Nothing
> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing > ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing Nothing
> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps > return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps
> (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes) > (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes)


Expand Down
51 changes: 31 additions & 20 deletions Ivor/Evaluator.lhs
View file
Expand Up @@ -20,11 +20,11 @@
menv :: [(Name, Binder (TT Name))] } menv :: [(Name, Binder (TT Name))] }


> eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name > eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name
> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing) > eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing Nothing)
> in finalise (Ind res) > in finalise (Ind res)


> eval_nf :: Gamma Name -> Indexed Name -> Indexed Name > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name
> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing) > eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing Nothing)
> in finalise (Ind res) > in finalise (Ind res)


> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name > eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
Expand All @@ -37,13 +37,14 @@


> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name > eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
> eval_nf_without gam tm [] = eval_nf gam tm > eval_nf_without gam tm [] = eval_nf gam tm
> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing) > eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing Nothing)
> in finalise (Ind res) > in finalise (Ind res)


> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> Indexed Name > eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] ->
> eval_nf_limit gam tm [] = eval_nf gam tm > Maybe [(Name, ([Int], Int))] -> Indexed Name
> eval_nf_limit gam (Ind tm) ns > eval_nf_limit gam tm [] stat = eval_nf gam tm
> = let res = makePs (evaluate True gam tm Nothing (Just ns)) > eval_nf_limit gam (Ind tm) ns stat
> = let res = makePs (evaluate True gam tm Nothing (Just ns) stat)
> in finalise (Ind res) > in finalise (Ind res)


> type Stack = [TT Name] > type Stack = [TT Name]
Expand All @@ -62,24 +63,27 @@ Code Stack Env Result
(or leave alone for whnf) (or leave alone for whnf)
[[let x = t in e]] xs es [[e]], xs, (Let x t: es) [[let x = t in e]] xs es [[e]], xs, (Let x t: es)


> type EvalState = (Maybe [(Name, Int)], Maybe [(Name, ([Int], Int))])

> evaluate :: Bool -> -- under binders? 'False' gives WHNF > evaluate :: Bool -> -- under binders? 'False' gives WHNF
> Gamma Name -> TT Name -> > Gamma Name -> TT Name ->
> Maybe [Name] -> -- Names not to reduce > Maybe [Name] -> -- Names not to reduce
> Maybe [(Name, Int)] -> -- Names to reduce a maximum number > Maybe [(Name, Int)] -> -- Names to reduce a maximum number
> Maybe [(Name, ([Int], Int))] -> -- Names and list of static args
> TT Name > TT Name
> evaluate open gam tm jns maxns = -- trace ("EVALUATING: " ++ debugTT tm) $ > evaluate open gam tm jns maxns statics = -- trace ("EVALUATING: " ++ debugTT tm) $
> let res = evalState (eval tm [] [] []) maxns > let res = evalState (eval tm [] [] []) (maxns, statics)
> in {- trace ("RESULT: " ++ debugTT res) -} > in {- trace ("RESULT: " ++ debugTT res) -}
> res > res
> where > where
> eval :: TT Name -> Stack -> SEnv -> > eval :: TT Name -> Stack -> SEnv ->
> [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name) > [(Name, TT Name)] -> State EvalState (TT Name)
> eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats > eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats


> eval' (P x) xs env pats > eval' (P x) xs env pats
> = do mns <- get > = do (mns, sts) <- get
> let (use, mns') = usename x jns mns > let (use, mns', sts') = usename x jns mns (sts, (xs, pats))
> put mns' > put (mns', sts)
> case lookup x pats of > case lookup x pats of
> Nothing -> if use then evalP x (lookupval x gam) xs env pats > Nothing -> if use then evalP x (lookupval x gam) xs env pats
> else evalP x Nothing xs env pats > else evalP x Nothing xs env pats
Expand Down Expand Up @@ -138,12 +142,19 @@ Code Stack Env Result
> uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns > uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns
> uniqify' n ns = uniqify n ns > uniqify' n ns = uniqify n ns


> usename x Nothing Nothing = (True, Nothing) usename x _ mns (sts, (stk, pats))
> usename x _ (Just ys) = case lookup x ys of | Just (static, arity) <- lookup x sts
> Just 0 -> (False, Just ys) = useDyn x mns static arity stk pats
> Just n -> (True, Just (update x (n-1) ys))
> _ -> (True, Just ys) > usename x Nothing Nothing (sts, _) = (True, Nothing, sts)
> usename x (Just xs) m = (not (elem x xs), m) > usename x _ (Just ys) (sts, _)
> = case lookup x ys of
> Just 0 -> (False, Just ys, sts)
> Just n -> (True, Just (update x (n-1) ys), sts)
> _ -> (True, Just ys, sts)
> usename x (Just xs) m (sts, _) = (not (elem x xs), m, sts)

useDyn x mns static arity stk pats =


> update x v [] = [] > update x v [] = []
> update x v ((k,_):xs) | x == k = ((x,v):xs) > update x v ((k,_):xs) | x == k = ((x,v):xs)
Expand Down Expand Up @@ -181,7 +192,7 @@ Code Stack Env Result


> match :: Scheme Name -> [TT Name] -> SEnv -> > match :: Scheme Name -> [TT Name] -> SEnv ->
> [(Name, TT Name)] -> > [(Name, TT Name)] ->
> State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack)) > State EvalState (Maybe (TT Name, [(Name, TT Name)], Stack))
> match (Sch pats _ rhs) xs env patvars > match (Sch pats _ rhs) xs env patvars
> = matchargs pats xs rhs env patvars [] > = matchargs pats xs rhs env patvars []
> matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs) > matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)
Expand Down
12 changes: 7 additions & 5 deletions Ivor/PatternDefs.lhs
View file
Expand Up @@ -26,8 +26,9 @@ Also return whether the function is definitely total.
> Bool -> -- Check for coverage > Bool -> -- Check for coverage
> Bool -> -- Check for well-foundedness > Bool -> -- Check for well-foundedness
> Maybe [(Name, Int)] -> -- Names to specialise > Maybe [(Name, Int)] -> -- Names to specialise
> Maybe [(Name, ([Int], Int))] -> -- Names and static args, when specialising
> IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool) > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
> checkDef gam fn tyin pats cover wellfounded spec = do > checkDef gam fn tyin pats cover wellfounded spec specst = do
> --x <- expandCon gam (mkapp (Var (UN "S")) [mkapp (Var (UN "S")) [Var (UN "x")]]) > --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")]]) > --x <- expandCon gam (mkapp (Var (UN "vcons")) [RInfer,RInfer,RInfer,mkapp (Var (UN "vnil")) [Var (UN "foo")]])
> clausesIn <- mapM (expandClause gam) pats > clausesIn <- mapM (expandClause gam) pats
Expand All @@ -39,7 +40,7 @@ Also return whether the function is definitely total.
> checkNotExists fn gam > checkNotExists fn gam
> gam' <- gInsert fn (G Undefined ty defplicit) gam > gam' <- gInsert fn (G Undefined ty defplicit) gam
> clauses' <- validClauses gam' fn ty clauses' > clauses' <- validClauses gam' fn ty clauses'
> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec > (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec specst
> wf <- return True > wf <- return True
> {- if wellfounded then > {- if wellfounded then
> do checkWellFounded gam fn [0..arity-1] pmdef > do checkWellFounded gam fn [0..arity-1] pmdef
Expand Down Expand Up @@ -183,8 +184,9 @@ Each clause may generate auxiliary definitions, so return all definitions create
> Bool -> -- Check coverage > Bool -> -- Check coverage
> [(Indexed Name, Indexed Name)] -> > [(Indexed Name, Indexed Name)] ->
> Maybe [(Name, Int)] -> > Maybe [(Name, Int)] ->
> Maybe [(Name, ([Int], Int))] ->
> IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool) > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec = do > matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec specst = do
> let raws = zip (map mkRaw pats) (map getRet pats) > let raws = zip (map mkRaw pats) (map getRet pats)
> (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True > (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True
> cv <- if cover then > cv <- if cover then
Expand Down Expand Up @@ -223,7 +225,7 @@ Each clause may generate auxiliary definitions, so return all definitions create
> let specrtm = case spec of > let specrtm = case spec of
> Nothing -> Ind rtmtt' > Nothing -> Ind rtmtt'
> Just [] -> eval_nf gam (Ind rtmtt') > Just [] -> eval_nf gam (Ind rtmtt')
> Just ns -> eval_nf_limit gam (Ind rtmtt') ns > Just ns -> eval_nf_limit gam (Ind rtmtt') ns specst
> return ((tm, specrtm, env), [], newdefs, True) > return ((tm, specrtm, env), [], newdefs, True)
> mytypecheck gam (clause, (RWith addprf scr pats)) i = > mytypecheck gam (clause, (RWith addprf scr pats)) i =
> do -- Get the type of scrutinee, construct the type of the auxiliary definition > do -- Get the type of scrutinee, construct the type of the auxiliary definition
Expand Down Expand Up @@ -251,7 +253,7 @@ Each clause may generate auxiliary definitions, so return all definitions create
> let gam' = insertGam newname (G Undefined newfnTy 0) gam > let gam' = insertGam newname (G Undefined newfnTy 0) gam
> newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats) > newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats)
> (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i > (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i
> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec > (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec specst
> return (chk, auxdefs++auxdefs', newdefs, covers) > return (chk, auxdefs++auxdefs', newdefs, covers)


> addLastArg (RBind n (B Pi arg) x) ty scr addprf > addLastArg (RBind n (B Pi arg) x) ty scr addprf
Expand Down
16 changes: 12 additions & 4 deletions Ivor/TT.lhs
View file
Expand Up @@ -312,6 +312,7 @@
> | GenRec -- ^ No termination checking > | GenRec -- ^ No termination checking
> | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved. > | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved.
> | Specialise [(Name, Int)] -- ^ Specialise the right hand side > | Specialise [(Name, Int)] -- ^ Specialise the right hand side
> | SpecStatic [(Name, ([Int], Int))] -- ^ Functions plus static arguments, plus arity, for use when specialising
> deriving Eq > deriving Eq


> -- |Add a new definition to the global state. > -- |Add a new definition to the global state.
Expand All @@ -334,6 +335,7 @@
> (not (elem Ivor.TT.Partial opts)) > (not (elem Ivor.TT.Partial opts))
> (not (elem GenRec opts)) > (not (elem GenRec opts))
> (getSpec opts) > (getSpec opts)
> (getSpecSt opts)
> (ndefs',vnewnames) > (ndefs',vnewnames)
> <- if (null newnames) then return (ndefs, []) > <- if (null newnames) then return (ndefs, [])
> else do when (not (Holey `elem` opts)) $ > else do when (not (Holey `elem` opts)) $
Expand All @@ -356,6 +358,10 @@
> getSpec (Specialise fns:_) = Just fns > getSpec (Specialise fns:_) = Just fns
> getSpec (_:xs) = getSpec xs > getSpec (_:xs) = getSpec xs


> getSpecSt [] = Nothing
> getSpecSt (SpecStatic fns:_) = Just fns
> getSpecSt (_:xs) = getSpecSt xs

> -- |Add a new definition, with its type to the global state. > -- |Add a new definition, with its type to the global state.
> -- These definitions can be recursive, so use with care. > -- These definitions can be recursive, so use with care.
> addTypedDef :: (IsTerm term, IsTerm ty) => > addTypedDef :: (IsTerm term, IsTerm ty) =>
Expand Down Expand Up @@ -794,14 +800,16 @@ Give a parseable but ugly representation of a term.
> -- |Reduce a term and its type to Normal Form (using new evaluator, not > -- |Reduce a term and its type to Normal Form (using new evaluator, not
> -- reducing given names) > -- reducing given names)
> evalnewWithout :: Context -> Term -> [Name] -> Term > evalnewWithout :: Context -> Term -> [Name] -> Term
> evalnewWithout (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_without (defs st) tm ns), > evalnewWithout (Ctxt st) (Term (tm,ty)) ns
> tidyNames (eval_nf_without (defs st) ty ns)) > = Term (tidyNames (eval_nf_without (defs st) tm ns),
> tidyNames (eval_nf_without (defs st) ty ns))
> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing > -- |Reduce a term and its type to Normal Form (using new evaluator, reducing
> -- given names a maximum number of times) > -- given names a maximum number of times)
> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term > evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term
> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_limit (defs st) tm ns, > evalnewLimit (Ctxt st) (Term (tm,ty)) ns
> eval_nf_limit (defs st) ty ns) > = Term (eval_nf_limit (defs st) tm ns Nothing,
> eval_nf_limit (defs st) ty ns Nothing)
> -- |Check a term in the context of the given goal > -- |Check a term in the context of the given goal
> checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term > checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
Expand Down

0 comments on commit c138e8a

Please sign in to comment.