Commit c2ab6ef0 authored by André Pacak's avatar André Pacak

Systematically derived lookup

parent 5c04f305
......@@ -86,70 +86,90 @@ matchType ty1 ty2 _ | ty1 >= ty2 = Inferred ()
matchType ty1 ty2 err = NotInferred [generalError (show ty1) ty2 err]
-- derived version
-- for every position where a ctx is passed to a function you need to generate a case for this function
-- if checkType ctx t1 ty1 and checkType ctx t2 ty2 are used in the same case you have to have two cases, case t == t1 and t == t2.
-- copy the content and delete everything that has nothing to do with the context (everything within a bind has to be kept)
-- if just the context without a bind is left you need to call invoke on the parent
-- otherwise you need to check if the name used in the bind is equal to the passed name if thats the case you return the bound type
-- otherwise you have to call lookup on the parent
-- TODO what about the cases of requiredType. For everything but the Lam it is obvious that it does not result in a different transformation
-- TODO but does it work with lam too?
lookup :: Term -> Name -> Infer Type
lookup t x = case parent t of
Just p@(Succ _ _) -> lookup p x
Just p@(Add _ _ _) -> lookup p x
Just p@(Mult _ _ _) -> lookup p x
Just p@(Let x' t1 t2 _) | x == x' -> inferType t1
| otherwise -> lookup p x
Just p@(Anno _ _ _) -> lookup p x
Just p@(App _ _ _) -> lookup p x
Just p@(Fst _ _) -> lookup p x
Just p@(Snd _ _) -> lookup p x
Just p@(Lam x' t _) | x == x' -> do
Just p@(Succ t _) -> lookup p x
Just p@(Add t1 t2 _) | t == t1 -> lookup p x
Just p@(Add t1 t2 _) | t == t2 -> lookup p x
Just p@(Mult t1 t2 _) | t == t1 -> lookup p x
Just p@(Mult t1 t2 _) | t == t2 -> lookup p x
Just p@(Let name t' body _) | t == t' -> lookup p x
Just p@(Let name t' body _) | t == body -> do
-- how do we get to name == x => tyt
-- from tyt <- inferType ctx t
-- inferType (Bind ctx name tyt) body
ty <- inferType t'
if x == name
then return ty
else lookup p x
Just p@(Anno term ty _) -> lookup p x
Just p@(App t1 t2 _) | t == t1 -> lookup p x
Just p@(App t1 t2 _) | t == t2 -> lookup p x
Just p@(Fst t _) -> lookup p x
Just p@(Snd t _) -> lookup p x
Just p@(Lam name t _) -> do
ty <- requiredType p
(ty1, _) <- matchFun ty (show p)
return ty1
| otherwise -> lookup p x
Just p@(Pair _ _ _) -> lookup p x
_ -> NotInferred ["Unbound variable " ++ show x]
(ty1, ty2) <- matchFun ty (show p)
if x == name
then return ty1
else lookup p x
Just p@(Pair t1 t2 _) | t == t1 -> lookup p x
Just p@(Pair t1 t2 _) | t == t2 -> lookup p x
_ -> fail ["Unbound variable " ++ show x]
inferType :: Term -> Infer Type
inferType (Zero _) = Inferred Nat
inferType (Succ t _) = inferType t
inferType (Zero _) = return Nat
inferType (Succ t _) = do
checkType t
return Nat
inferType (Add t1 t2 _) = do
ty1 <- inferType t1
matchNat ty1 (show t1)
ty2 <- inferType t2
matchNat ty2 (show t2)
Inferred Nat
checkType t1
checkType t2
return Nat
inferType (Mult t1 t2 _) = do
ty1 <- inferType t1
matchNat ty1 (show t1)
ty2 <- inferType t2
matchNat ty2 (show t2)
Inferred Nat
checkType t1
checkType t2
return Nat
inferType p@(Var name _) = lookup p name
inferType (Let name t body _) = do
tyt <- inferType t
inferType body
inferType (Anno term ty _) = do
checkType term
Inferred ty
return ty
inferType (App t1 t2 _) = do
ty <- inferType t1
(_, ty2) <- matchFun ty (show t1)
(ty1, ty2) <- matchFun ty (show t1)
checkType t2
Inferred ty2
return ty2
inferType (Fst t _) = do
ty <- inferType t
(ty1, _) <- matchProd ty (show t)
Inferred ty1
return ty1
inferType (Snd t _) = do
ty <- inferType t
(_, ty2) <- matchProd ty (show t)
Inferred ty2
inferType t = NotInferred ["Cannot infer type of term " ++ show t]
return ty2
inferType t = fail ["Cannot infer type of term " ++ show t]
checkType :: Term -> Check
checkType p@(Lam name t _) = do
ty <- requiredType p
(ty1, _) <- matchFun ty (show p)
(ty1, ty2) <- matchFun ty (show p)
checkType t
checkType p@(Pair t1 t2 _) = do
ty <- requiredType p
(_, _) <- matchProd ty (show p)
(ty1, ty2) <- matchProd ty (show p)
checkType t1
checkType t2
checkType t = do
......@@ -157,27 +177,39 @@ checkType t = do
ty' <- inferType t
matchType ty ty' (show t)
deleteLastBinding :: Ctx -> Ctx
deleteLastBinding (Bind c _ _) = c
deleteLastBinding Empty = Empty
requiredType :: Term -> Infer Type
requiredType t = case parent t of
-- anno app lam
Just p@(Anno _ ty _) -> return ty
Just p@(App t1 t2 _) | t == t2 -> do
Just (Succ t' _) | t == t' -> return Nat
Just (Add t1 t2 _) | t == t1 ->
return Nat
Just (Add t1 t2 _) | t == t2 ->
return Nat
Just (Mult t1 t2 _) | t == t1 ->
return Nat
Just (Mult t1 t2 _) | t == t2 ->
return Nat
Just (Anno term ty _) | t == term -> return ty
Just (App t1 t2 _) | t == t2 -> do
ty <- inferType t1
(ty1, _) <- matchFun ty (show t1)
(ty1, ty2) <- matchFun ty (show t1)
return ty1
Just p@(Lam _ _ _) -> do
Just p@(Lam name term _) | t == term -> do
-- TODO deconstruction the context should be done up here but why is that?
-- TODO how can we detect that?
-- the idea is that we want to throw away the last binding because the outer invocation of checkType does not know
-- of this binding and a new binding is added for the inner checkType call. Thus the calculation of ty by
-- requiredType should not be passed the binding
-- because we have a context that has a additional binding
ty <- requiredType p
(_, ty2) <- matchFun ty (show p)
-- TODO Need to return AnyType if ty is not a function
-- Need to return AnyType if ty is not a function
-- is this needed? Because matchFun returns NotInferred and top would then return AnyType in bind
(ty1, ty2) <- matchFun ty (show p)
return ty2
Just p@(Pair t1 t2 _) -> do
Just p@(Pair t1 t2 _) | t == t1 -> do
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
if t == t1
then return ty1
else return ty2
return ty1
Just p@(Pair t1 t2 _) | t == t2 -> do
ty <- requiredType p
(ty1, ty2) <- matchProd ty (show p)
return ty2
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment