-
Notifications
You must be signed in to change notification settings - Fork 139
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #2465 from AlecsFerra/develop
Support for lambdas :)
- Loading branch information
Showing
8 changed files
with
311 additions
and
21 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,3 @@ | ||
| [submodule "liquid-fixpoint"] | ||
| path = liquid-fixpoint | ||
| url = https://github.com/ucsd-progsys/liquid-fixpoint.git | ||
| url = https://github.com/ucsd-progsys/liquid-fixpoint.git |
Submodule liquid-fixpoint
updated
7 files
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,54 @@ | ||
| {-# LANGUAGE RankNTypes #-} | ||
|
|
||
| {-@ LIQUID "--reflection" @-} | ||
| {-@ LIQUID "--ple" @-} | ||
| {-@ LIQUID "--etabeta" @-} | ||
|
|
||
| module FuseMapLam where | ||
|
|
||
| import Prelude hiding (map, foldr) | ||
| import Language.Haskell.Liquid.ProofCombinators | ||
|
|
||
| -- When we allow the parser to accept : in refinements this wont be needed | ||
| {-@ reflect append @-} | ||
| append :: a -> [a] -> [a] | ||
| append = (:) | ||
|
|
||
| {-@ reflect map @-} | ||
| map :: (a -> b) -> [a] -> [b] | ||
| map _ [] = [] | ||
| map f (x:xs) = f x : map f xs | ||
|
|
||
| {-@ reflect foldr @-} | ||
| foldr :: (a -> b -> b) -> b -> [a] -> b | ||
| foldr _ e [] = e | ||
| foldr f e (x:xs) = f x (foldr f e xs) | ||
|
|
||
| {-@ reflect build @-} | ||
| build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a] | ||
| build g = g (:) [] | ||
|
|
||
| {-@ reflect mapFB @-} | ||
| mapFB :: forall elt lst a . (elt -> lst -> lst) -> (a -> elt) -> a -> lst -> lst | ||
| mapFB c f = \x ys -> c (f x) ys | ||
|
|
||
|
|
||
| {-@ rewriteMapList :: f:_ -> b:_ -> { foldr (mapFB append f) [] b = map f b } @-} | ||
| rewriteMapList :: (a -> b) -> [a] -> () | ||
| rewriteMapList f [] = trivial | ||
| rewriteMapList f (x:xs) = trivial ? (rewriteMapList f xs) | ||
|
|
||
| {-@ rewriteMapFB :: c:_ -> f:_ -> g:_ -> { mapFB (mapFB c f) g = mapFB c (f . g) } @-} | ||
| rewriteMapFB :: (a -> b -> b) -> (c -> a) -> (d -> c) -> Proof | ||
| rewriteMapFB c f g = trivial | ||
|
|
||
| {-@ rewriteMapFBid :: c:(a -> b -> b) -> { mapFB c (\x:a -> x) = c } @-} | ||
| rewriteMapFBid :: (a -> b -> b) -> () | ||
| rewriteMapFBid c = trivial | ||
|
|
||
| {-@ rewriteMap :: f:(a1 -> a2) -> xs:[a1] | ||
| -> { build (\c:func(1, [a2, @(0), @(0)]) -> \n:@(0) -> foldr (mapFB c f) n xs) | ||
| = map f xs } @-} | ||
| rewriteMap :: (a1 -> a2) -> [a1] -> () | ||
| rewriteMap f [] = trivial | ||
| rewriteMap f (x:xs) = trivial ? rewriteMap f xs |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,215 @@ | ||
| {-# Language GADTs, TypeFamilies, DataKinds #-} | ||
|
|
||
| {-@ LIQUID "--reflection" @-} | ||
| {-@ LIQUID "--ple" @-} | ||
| {-@ LIQUID "--full" @-} | ||
| {-@ LIQUID "--max-case-expand=4" @-} | ||
| {-@ LIQUID "--etabeta" @-} | ||
| {-@ LIQUID "--dependantcase" @-} | ||
|
|
||
| module SKILam where | ||
|
|
||
| import Prelude | ||
|
|
||
| import Language.Haskell.Liquid.ProofCombinators | ||
|
|
||
| {-@ reflect id @-} | ||
| {-@ reflect $ @-} | ||
|
|
||
| data List a = Nil | Cons a (List a) | ||
| deriving (Show) | ||
|
|
||
| data Ty | ||
| = Iota | ||
| | Arrow Ty Ty | ||
| deriving Eq | ||
|
|
||
| type Ctx = List Ty | ||
|
|
||
| data Ref where | ||
| {-@ Here :: σ:Ty -> γ:Ctx -> Prop (Ref σ (Cons σ γ)) @-} | ||
| Here :: Ty -> Ctx -> Ref | ||
|
|
||
| {-@ There :: τ:Ty -> σ:Ty -> γ:Ctx -> Prop (Ref σ γ) | ||
| -> Prop (Ref σ (Cons τ γ)) @-} | ||
| There :: Ty -> Ty -> Ctx -> Ref -> Ref | ||
| data REF = Ref Ty Ctx | ||
|
|
||
| data Term where | ||
| {-@ App :: σ:Ty -> τ:Ty -> γ:Ctx -> Prop (Term γ (Arrow σ τ)) | ||
| -> Prop (Term γ σ) -> Prop (Term γ τ) @-} | ||
| App :: Ty -> Ty -> Ctx -> Term -> Term -> Term | ||
| {-@ Lam :: σ:Ty -> τ:Ty -> γ:Ctx -> Prop (Term (Cons σ γ) τ) | ||
| -> Prop (Term γ (Arrow σ τ)) @-} | ||
| Lam :: Ty -> Ty -> Ctx -> Term -> Term | ||
| {-@ Var :: σ:Ty -> γ:Ctx -> Prop (Ref σ γ) -> Prop (Term γ σ) @-} | ||
| Var :: Ty -> Ctx -> Ref -> Term | ||
| data TERM = Term Ctx Ty | ||
|
|
||
| {-@ measure tlen @-} | ||
| {-@ tlen :: Term -> Nat @-} | ||
| tlen :: Term -> Int | ||
| tlen (App _ _ _ t₁ t₂) = 1 + tlen t₁ + tlen t₂ | ||
| tlen (Lam _ _ _ t) = 1 + tlen t | ||
| tlen (Var _ _ _) = 0 | ||
|
|
||
|
|
||
| -- VFun function is non positive idk how to fix | ||
| {-@ LIQUID "--no-positivity-check" @-} | ||
| data Value where | ||
| {-@ VIota :: Int -> Prop (Value Iota) @-} | ||
| VIota :: Int -> Value | ||
| {-@ VFun :: σ:Ty -> τ:Ty -> (Prop (Value σ) -> Prop (Value τ)) | ||
| -> Prop (Value (Arrow σ τ)) @-} | ||
| VFun :: Ty -> Ty -> (Value -> Value) -> Value | ||
| data VALUE = Value Ty | ||
|
|
||
| data Env where | ||
| {-@ Empty :: Prop (Env Nil) @-} | ||
| Empty :: Env | ||
| {-@ With :: σ:Ty -> γ:Ctx -> Prop (Value σ) -> Prop (Env γ) | ||
| -> Prop (Env (Cons σ γ)) @-} | ||
| With :: Ty -> Ctx -> Value -> Env -> Env | ||
| data ENV = Env Ctx | ||
|
|
||
| {-@ reflect lookupRef @-} | ||
| {-@ lookupRef :: σ:Ty -> γ:Ctx -> r:Prop (Ref σ γ) -> Prop (Env γ) | ||
| -> Prop (Value σ) @-} | ||
| lookupRef :: Ty -> Ctx -> Ref -> Env -> Value | ||
| lookupRef _ _ (Here _ _) (With _ _ a _) = a | ||
| lookupRef σ (Cons γ γs) (There _ _ _ there) (With _ _ _ as) = | ||
| lookupRef σ γs there as | ||
|
|
||
| {-@ reflect eval @-} | ||
| {-@ eval :: σ:Ty -> γ:Ctx -> t:Prop (Term γ σ) -> Prop (Env γ) | ||
| -> Prop (Value σ) @-} | ||
| eval :: Ty -> Ctx -> Term -> Env -> Value | ||
| eval σ γ (App α _ _ t₁ t₂) e = case eval (Arrow α σ) γ t₁ e of | ||
| VFun _ _ f -> f (eval α γ t₂ e) | ||
| eval σ γ (Var _ _ x) e = lookupRef σ γ x e | ||
| eval (Arrow α σ) γ (Lam _ _ _ t) e = VFun α σ (\y -> eval σ (Cons α γ) t (With α γ y e)) | ||
|
|
||
| {-@ reflect makeId @-} | ||
| {-@ makeId :: σ:Ty -> γ:Ctx -> (Prop (Env γ) -> Prop (Value (Arrow σ σ))) @-} | ||
| makeId :: Ty -> Ctx -> (Env -> Value) | ||
| makeId σ γ v = VFun σ σ id | ||
|
|
||
| {-@ reflect makeApp @-} | ||
| {-@ makeApp :: σ:Ty -> τ:Ty -> γ:Ctx | ||
| -> (Prop (Env γ) -> Prop (Value (Arrow σ τ))) | ||
| -> (Prop (Env γ) -> Prop (Value σ)) | ||
| -> Prop (Env γ) -> Prop (Value τ) @-} | ||
| makeApp :: Ty -> Ty -> Ctx -> (Env -> Value) -> (Env -> Value) -> Env -> Value | ||
| makeApp σ τ γ fun arg env = case fun env of | ||
| VFun _ _ f -> f (arg env) | ||
|
|
||
| {-@ reflect makeConst @-} | ||
| {-@ makeConst :: σ:Ty -> τ:Ty -> γ:Ctx | ||
| -> (Prop (Env γ) -> Prop (Value (Arrow σ (Arrow τ σ)))) @-} | ||
| makeConst :: Ty -> Ty -> Ctx -> (Env -> Value) | ||
| makeConst σ τ γ e = VFun σ (Arrow τ σ) $ \x -> VFun τ σ $ \y -> x | ||
|
|
||
|
|
||
| {-@ reflect makeS @-} | ||
| {-@ makeS :: σ:Ty -> τ:Ty -> υ:Ty -> γ:Ctx | ||
| -> (Prop (Env γ) | ||
| -> Prop (Value (Arrow (Arrow σ (Arrow τ υ)) | ||
| (Arrow (Arrow σ τ) (Arrow σ υ)))))@-} | ||
| makeS :: Ty -> Ty -> Ty -> Ctx -> (Env -> Value) | ||
| makeS σ τ υ γ e = VFun (Arrow σ (Arrow τ υ)) (Arrow (Arrow σ τ) (Arrow σ υ)) | ||
| $ \(VFun _ _ x) -> VFun (Arrow σ τ) (Arrow σ υ) $ \(VFun _ _ y) -> VFun σ υ $ \z -> case (x z) | ||
| of VFun _ _ xz -> xz (y z) | ||
|
|
||
|
|
||
| {-@ reflect sType @-} | ||
| sType σ τ υ = Arrow (Arrow σ (Arrow τ υ)) (Arrow (Arrow σ τ) (Arrow σ υ)) | ||
|
|
||
| {-@ reflect kType @-} | ||
| kType σ τ = Arrow σ (Arrow τ σ) | ||
|
|
||
| {-@ reflect iType @-} | ||
| iType σ = Arrow σ σ | ||
|
|
||
| {-@ reflect dom @-} | ||
| {-@ dom :: { σ:Ty | σ /= Iota } -> Ty @-} | ||
| dom (Arrow σ τ) = σ | ||
|
|
||
| {-@ reflect cod @-} | ||
| {-@ cod :: { σ:Ty | σ /= Iota } -> Ty @-} | ||
| cod (Arrow σ τ) = τ | ||
|
|
||
|
|
||
| data Comb where | ||
| {-@ S :: σ:Ty -> τ:Ty -> υ:Ty -> γ:Ctx | ||
| -> Prop (Comb γ (sType σ τ υ) (makeS σ τ υ γ)) @-} | ||
| S :: Ty -> Ty -> Ty -> Ctx -> Comb | ||
| {-@ K :: σ:Ty -> τ:Ty -> γ:Ctx | ||
| -> Prop (Comb γ (kType σ τ) (makeConst σ τ γ)) @-} | ||
| K :: Ty -> Ty -> Ctx -> Comb | ||
| {-@ I :: σ:Ty -> γ:Ctx | ||
| -> Prop (Comb γ (iType σ) (makeId σ γ)) @-} | ||
| I :: Ty -> Ctx -> Comb | ||
| {-@ CApp :: σ:Ty -> τ:Ty -> γ:Ctx | ||
| -> fun:(Prop (Env γ) -> Prop (Value (Arrow σ τ))) | ||
| -> arg:(Prop (Env γ) -> Prop (Value σ)) | ||
| -> Prop (Comb γ (Arrow σ τ) fun) | ||
| -> Prop (Comb γ σ arg) | ||
| -> Prop (Comb γ τ (makeApp σ τ γ fun arg)) @-} | ||
| CApp :: Ty -> Ty -> Ctx -> (Env -> Value) -> (Env -> Value) -> Comb -> Comb | ||
| -> Comb | ||
| {-@ CVar :: σ:Ty -> γ:Ctx -> r:Prop (Ref σ γ) | ||
| -> Prop (Comb γ σ (lookupRef σ γ r)) @-} | ||
| CVar :: Ty -> Ctx -> Ref -> Comb | ||
| data COMB = Comb Ctx Ty (Env -> Value) | ||
|
|
||
| {-@ translate :: σ:Ty -> γ:Ctx -> t:Prop (Term γ σ) | ||
| -> Prop (Comb γ σ (eval σ γ t)) @-} | ||
| translate :: Ty -> Ctx -> Term -> Comb | ||
| translate σ γ (App α _ _ t₁ t₂) = | ||
| CApp α σ γ (eval (Arrow α σ) γ t₁) (eval α γ t₂) t₁ₜ t₂ₜ | ||
| where t₁ₜ = translate (Arrow α σ) γ t₁ | ||
| t₂ₜ = translate α γ t₂ | ||
| translate σ γ (Var _ _ x) = | ||
| CVar σ γ x | ||
| translate (Arrow σ τ) γ (Lam _ _ _ t) = | ||
| bracket σ τ γ (eval τ (Cons σ γ) t) (translate τ (Cons σ γ) t) | ||
|
|
||
| {-@ reflect makeBracketing @-} | ||
| {-@ makeBracketing :: σ:Ty -> τ:Ty -> γ:Ctx | ||
| -> f:(Prop (Env (Cons σ γ)) -> Prop (Value τ)) | ||
| -> Prop (Env γ) | ||
| -> Prop (Value (Arrow σ τ)) @-} | ||
| makeBracketing :: Ty -> Ty -> Ctx -> (Env -> Value) -> Env -> Value | ||
| makeBracketing σ τ γ f env = VFun σ τ $ \x -> f (With σ γ x env) | ||
|
|
||
| {-@ bracket :: σ:Ty -> τ:Ty -> γ:Ctx -> f:(Prop (Env (Cons σ γ)) -> Prop (Value τ)) | ||
| -> Prop (Comb (Cons σ γ) τ f) | ||
| -> Prop (Comb γ (Arrow σ τ) (makeBracketing σ τ γ f)) @-} | ||
| bracket :: Ty -> Ty -> Ctx -> (Env -> Value) -> Comb -> Comb | ||
| bracket σ τ γ f (CApp α _ _ ft₁ ft₂ t₁ t₂) = | ||
| CApp (Arrow σ α) (Arrow σ τ) γ | ||
| (makeApp (Arrow σ (Arrow α τ)) (Arrow (Arrow σ α) (Arrow σ τ)) | ||
| γ (makeS σ α τ γ) (makeBracketing σ (Arrow α τ) γ ft₁)) | ||
| (makeBracketing σ α γ ft₂) st t₂ᵣ | ||
| where t₁ᵣ = bracket σ (Arrow α τ) γ ft₁ t₁ | ||
| t₂ᵣ = bracket σ α γ ft₂ t₂ | ||
| st = CApp (dom $ sType σ α τ) (cod $ sType σ α τ) | ||
| γ | ||
| (makeS σ α τ γ) | ||
| (makeBracketing σ (Arrow α τ) γ ft₁) | ||
| (S σ α τ γ) t₁ᵣ | ||
| bracket σ τ γ f (S τ₁ τ₂ τ₃ _) = | ||
| CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeS τ₁ τ₂ τ₃ γ) | ||
| (K τ σ γ) (S τ₁ τ₂ τ₃ γ) | ||
| bracket σ τ γ f (K τ₁ τ₂ _) = | ||
| CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeConst τ₁ τ₂ γ) | ||
| (K τ σ γ) (K τ₁ τ₂ γ) | ||
| bracket σ τ γ f (I τ₁ _) = | ||
| CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeId τ₁ γ) | ||
| (K τ σ γ) (I τ₁ γ) | ||
| bracket σ τ γ f (CVar _ _ (Here _ _)) = | ||
| I σ γ | ||
| bracket σ τ γ f (CVar _ _ (There _ _ _ there)) = | ||
| CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (lookupRef τ γ there) | ||
| (K τ σ γ) (CVar τ γ there) | ||
|
|
Oops, something went wrong.