Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Make equality proof generation in with rule optional

Ignore-this: a9639836cc96754b2fbad9a15c9893b2

darcs-hash:20090902145525-228f4-1451f93137a0951e5c93e2d35bb7b0bb0393cd11.gz
  • Loading branch information...
commit fd3fab4c1a7776178fa6b4b311ef62cf9f67862e 1 parent bc5c41a
eb authored
View
32 Ivor/PatternDefs.lhs
@@ -216,7 +216,7 @@ Each clause may generate auxiliary definitions, so return all definitons created
> checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
> -- trace (show (unified, rtmtt, tm, rtmtt')) $
> return ((tm, Ind rtmtt', newdefs), [], newdefs, True)
-> mytypecheck gam (clause, (RWith scr pats)) i =
+> 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
> let args = getRawArgs clause
@@ -226,7 +226,7 @@ Each clause may generate auxiliary definitions, so return all definitons created
> let newargs = filter (\ (x,ty) -> x `elem` margNames) env
> newpats <- mapM (getNewPat tm 1) pats
> let newfntyin = forget (mkNewTy newargs clausety)
-> let newfntyin' = addLastArg newfntyin (forget stt) scr
+> let newfntyin' = addLastArg newfntyin (forget stt) scr addprf
> --(newargs ++ [(UN "__scr", B Pi stt),
> -- (UN "__scrEq", B Pi (screq (UN "__scr") scr))]) clausety
> (newfnTy, _) <- trace (show newfntyin') $ check gam env newfntyin' (Just (Ind Star))
@@ -236,19 +236,24 @@ Each clause may generate auxiliary definitions, so return all definitons created
> -- TODO: All pats have to match against args ++ [_]
> -- Final clause returns newname applied to args++scrutinee++refl
> let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++
-> [scr, RApp (RApp (Var (UN "refl")) RInfer) RInfer])
+> [scr] ++ if addprf then
+> [RApp (RApp (Var (UN "refl")) RInfer) RInfer]
+> else [])
> let gam' = insertGam newname (G Undefined newfnTy 0) gam
-> newpdef <- mapM (newp tm newargs 1) (zip newpats pats)
+> newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats)
> (chk, auxdefs, _, _) <- trace (show (newfnTy, newpdef)) $ mytypecheck gam' (clause, (RWRet ret)) i
> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover
> return (chk, auxdefs++auxdefs', newdefs, covers)
-> addLastArg (RBind n (B Pi arg) x) ty scr = RBind n (B Pi arg) (addLastArg x ty scr)
-> addLastArg x ty scr = RBind (UN "__scr") (B Pi ty)
-> (RBind (UN "__scrEq") (B Pi (screq (UN "__scr") scr)) x)
+> addLastArg (RBind n (B Pi arg) x) ty scr addprf
+> = RBind n (B Pi arg) (addLastArg x ty scr addprf)
+> addLastArg x ty scr addprf
+> = RBind (UN "__scr") (B Pi ty)
+> (if addprf then (RBind (UN "__scrEq") (B Pi (screq (UN "__scr") scr)) x)
+> else x)
> screq scrname scr = RApp (RApp (RApp (RApp (Var (UN "Eq")) RInfer) RInfer)
-> (Var scrname)) scr
+> scr) (Var scrname)
> rawApp f [] = f
> rawApp f (a:as) = rawApp (RApp f a) as
@@ -264,13 +269,14 @@ Each clause may generate auxiliary definitions, so return all definitons created
> (argv, argt, _) <- checkAndBind gam [] pargs Nothing
> getMatches argv proto
-> newp proto newargs i (newps, RSch args ret) = do
+> newp proto newargs i addprf (newps, RSch args ret) = do
> ret' <- newpRet ret
-> return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args)++[RInfer]) ret'
-> where newpRet (RWith v schs) =
+> return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args) ++
+> (if addprf then [RInfer] else [])) ret'
+> where newpRet (RWith prf v schs) =
> do newpats <- mapM (getNewPat proto (i+1)) schs
-> newpdef <- mapM (newp proto newargs (i+1)) (zip newpats schs)
-> return (RWith v newpdef)
+> newpdef <- mapM (newp proto newargs (i+1) prf) (zip newpats schs)
+> return (RWith prf v newpdef)
> newpRet r = return r
> lastn i xs = reverse $ take i (reverse xs)
View
2  Ivor/ShellParser.lhs
@@ -139,7 +139,7 @@ which runs it.
> lchar '{'
> pats <- ppatterns nm ext
> lchar '}'
-> return $ PWithClause args scr pats
+> return $ PWithClause False args scr pats
> ppatterns :: String -> Maybe (Parser ViewTerm) -> Parser Patterns
> ppatterns name ext
View
5 Ivor/TT.lhs
@@ -266,6 +266,7 @@
> returnval :: ViewTerm
> }
> | PWithClause {
+> eqproof :: Bool,
> arguments :: [ViewTerm],
> scrutinee :: ViewTerm,
> patterns :: Patterns
@@ -278,8 +279,8 @@
> mkRawClause :: PClause -> RawScheme
> mkRawClause (PClause args ret) =
> RSch (map forget args) (RWRet (forget ret))
-> mkRawClause (PWithClause args scr (Patterns rest)) =
-> RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))
+> mkRawClause (PWithClause prf args scr (Patterns rest)) =
+> RSch (map forget args) (RWith prf (forget scr) (map mkRawClause rest))
> -- ^ Convert a term to matchable pattern form; i.e. the only names allowed
> -- are variables and constructors. Any arbitrary function application is
View
4 Ivor/TTCore.lhs
@@ -149,8 +149,8 @@ This keeps both namespaces separate.
Data declarations and pattern matching
-> data RawWith = RWith Raw [RawScheme] -- match with an extra arg, add new schemes
-> | RWRet Raw
+> data RawWith = RWith Bool Raw [RawScheme] -- match with an extra arg, add new schemes
+> | RWRet Raw -- if Bool is true, add an equality proof
> deriving Show
data With = With [Indexed n]
Please sign in to comment.
Something went wrong with that request. Please try again.