Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Shallow embedding of ArrayPut and ArrayTake #383

Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Shallow embedding of ArrayPut and ArrayTake #383

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2d076d8
Shallow embedding of ArrayPut and ArrayTake
Aug 20, 2020
8d8cccf
Vincent's modification to map2 shallow compilation
amblafont Oct 6, 2020
d005bc6
Shallow compilation of map2 exprs by inlining iso btw record/pairs
amblafont Oct 7, 2020
4bc2eb5
typo
amblafont Oct 7, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions cogent/isa/shallow/ShallowUtil.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,16 @@ theory ShallowUtil
"Cogent.Util"
begin

fun array_map2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> ('a list \<times> 'b list)"
where
"array_map2 f [] [] = ([], [])"
| "array_map2 f (t # q) (t' # q') = (let (a,b) = f t t' in
let (la, lb) = array_map2 f q q' in
(a # la, b # lb))"

definition nth' :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a"
where "nth' n l = l ! n"

definition
fun_app :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "$" 10)
where
Expand Down
46 changes: 34 additions & 12 deletions cogent/src/Cogent/Isabelle/Shallow.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -221,15 +221,32 @@ shallowExpr (TE _ (Pop _ arr e)) = __todo "shallowExpr: pop"
shallowExpr (TE _ (Singleton e)) = __todo "shallowExpr: singleton"
shallowExpr (TE _ (ArrayMap2 ((v1, v2), fbody) (arr1,arr2))) = do
fbody' <- shallowExpr fbody
let f = mkLambda [snm v1, snm v2] fbody'
tuples <- asks recoverTuples
fbody'' <-
if tuples then return fbody' else do
e_fst <- (shallowGetter fbody 0 (mkId "r"))
e_snd <- (shallowGetter fbody 1 (mkId "r"))
return $ mkLet "r" fbody' (mkPair e_fst e_snd)
let f = mkLambda [snm v1, snm v2] fbody''
arr1' <- shallowExpr arr1
arr2' <- shallowExpr arr2
tuples <- asks recoverTuples
if tuples then return $ mkApp (mkId "map2") [f, mkPair arr1' arr2']
else shallowMaker (exprType fbody)
[("p1" ++ subSymStr "f", arr1), ("p2" ++ subSymStr "f", arr2)]
shallowExpr (TE _ (ArrayTake _ arr idx e)) = __todo "shallowExpr: array take"
shallowExpr (TE _ (ArrayPut arr idx val)) = __todo "shallowExpr: array put"
let body = mkApp (mkId "array_map2") [f, arr1', arr2']
if tuples then return body else do
tn <- findTypeSyn (exprType fbody)
let f = mkApp (mkStr [tn, ".make"]) [mkApp (mkId "fst") [mkId "r"], mkApp (mkId "snd") [mkId "r"]]
return $ mkLet "r" body f

shallowExpr (TE _ (ArrayTake n12 arr idx e)) = do
idx' <- mkApp (mkId "unat") <$> mapM shallowExpr [idx]
let nth' = mkApp (mkId "nth'") [idx']
mkTake n12 arr nth' e
shallowExpr (TE _ (ArrayPut arr idx val)) = do
idx' <- mkApp (mkId "unat") <$> mapM shallowExpr [idx]
earr <- shallowExpr arr
eval <- shallowExpr val
return $ mkApp (mkId "list_update") [earr, idx', eval]
-- list_update :: "'a list ⇒ nat ⇒ 'a ⇒ 'a list"

#endif
shallowExpr (TE _ (Let nm e1 e2)) = shallowLet nm e1 e2
shallowExpr (TE _ (LetBang vs nm e1 e2)) = shallowLet nm e1 e2
Expand Down Expand Up @@ -283,18 +300,23 @@ shallowExpr (TE t (Esac e)) = do
pure $ mkApp (mkStr ["case_",tn]) $ es ++ [e']
shallowExpr (TE _ (Split (n1,n2) e1 e2)) = mkApp <$> mkLambdaE [mkPrettyPair n1 n2] e2 <*> mapM shallowExpr [e1]
shallowExpr (TE _ (Member rec fld)) = shallowExpr rec >>= \e -> shallowGetter rec fld e
shallowExpr (TE _ (Take (n1,n2) rec fld e)) = do
erec <- shallowExpr rec
shallowExpr (TE _ (Take n12 rec fld e)) = do
efield <- mkId <$> getRecordFieldName (exprType rec) fld
let take = mkApp (mkId $ "take" ++ subSymStr "cogent") [erec, efield]
pp = mkPrettyPair n1 n2
mkLet pp take <$> shallowExpr e
mkTake n12 rec efield e
shallowExpr (TE _ (Put rec fld e)) = shallowSetter rec fld e
shallowExpr (TE _ (Promote ty e)) = shallowExpr e
shallowExpr (TE _ (Cast (TPrim pt) (TE _ (ILit n _)))) = pure $ shallowILit n pt
shallowExpr (TE _ (Cast (TPrim pt) e)) =
TermWithType <$> (mkApp (mkId "ucast") <$> ((:[]) <$> shallowExpr e)) <*> pure (shallowPrimType pt)

mkTake :: (Show b) => (VarName, VarName) -> TypedExpr t v VarName b -> Term ->
TypedExpr t ('Suc ('Suc v)) VarName b -> SG Term
mkTake (n1, n2) main accessor e = do
erec <- shallowExpr main
let take = mkApp (mkId $ "take" ++ subSymStr "cogent") [erec, accessor]
pp = mkPrettyPair n1 n2
mkLet pp take <$> shallowExpr e

-- | @'mkL' nm t1 t2@:
--
-- It generates term @(&#x03bb; nm. t2) t1@
Expand Down