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

Typedefify cart (WIP) #51

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

Typedefify cart (WIP) #51

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
00e66c2
add typedefs lists for making morphisms
andrevidela Mar 4, 2020
972e01a
fix parens on makeMorphism
epost Mar 4, 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
42 changes: 28 additions & 14 deletions src/Computer/EcommerceExample.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,6 @@ import Util.Elem

%include c "Computer/ecommerceExample.h"

-- type definitions
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

just as a note, I wouldn't remove this comment until these types become useless (because you can use the types from tdefs.txt). At the moment, if they don't match precisely, it doesn't work

-- these must coincide with the ones defined in tdefs.txt

Natural : TNamed 0
Natural = TName "Natural" $ TMu [("ZZ", T1), ("SS", TVar 0)]

Expand All @@ -64,6 +61,27 @@ CartContent = TName "CartContent" $ TMu [("NilN", T1), ("ConsN", TProd [weakenTD
InvoiceId : TNamed 0
InvoiceId = TName "InvoiceId" $ wrap Natural

-- tdef for transitions
transition1 : TNamed 0
transition1 = TName "Login" (TProd [FRef "InitialState", FRef "CartContent"])

transition2 : TNamed 0
transition2 = TName "AddProduct" (TProd [FRef "CartContent", FRef "CartContent"])

transition3 : TNamed 0
transition3 = TName "Checkout" (TProd [FRef "CartContent", FRef "InvoiceId"])

checkName : TNamed 0 -> Maybe (String, TDef 0, TDef 0)
checkName = ?todo

makeMorphisms : List (String, a : TDef 0 ** b : TDef 0 ** Ty [] (unwrap a) -> IO (Ty [] (unwrap b)))
-> (Fin lenV, Fin lenV, String)
-> Maybe (mor' $ ioClosedTypedefsKleisliCategory FFI_C)
makeMorphisms transitions (_, _, label) = do
(src ** tgt ** func) <- lookup label transitions
pure ((unwrap src) ** (unwrap tgt) ** MkExtensionalTypeMorphism func)


-- functions

readIntFromUser : String -> IO Int
Expand Down Expand Up @@ -124,18 +142,14 @@ checkout (Inn cartContent) = do
randomNat <- generateInvoiceNumber
pure $ natToNatural randomNat

morphismList : List (String, a : TDef 0 ** b : TDef 0 ** Ty [] (unwrap a) -> IO (Ty [] (unwrap b)))
morphismList = [ ("login", InitialState ** CartContent ** login)
, ("addProduct", CartContent ** CartContent ** addProduct)
, ("checkout", CartContent ** InvoiceId ** checkout)
]

edgeAsMorphism : (Fin lenV, Fin lenV, String) -> Maybe (mor' $ ioClosedTypedefsKleisliCategory FFI_C)
edgeAsMorphism (_, _, label) =
if label == "login" then Just ( (unwrap InitialState)
** (unwrap CartContent)
** MkExtensionalTypeMorphism login)
else if label == "addProduct" then Just ( (unwrap CartContent)
** (unwrap CartContent)
** MkExtensionalTypeMorphism addProduct)
else if label == "checkout" then Just ( (unwrap CartContent)
** (unwrap InvoiceId)
** MkExtensionalTypeMorphism checkout)
else Nothing
edgeAsMorphism label = makeMorphisms morphismList label

edgesAsMorphisms : Vect lenE (Fin lenV, Fin lenV, String)
-> Maybe (Vect lenE (mor' $ ioClosedTypedefsKleisliCategory FFI_C))
Expand Down