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.

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

[PLC] [Test] Added a couple of unsatated builtins application tests #772

Conversation

effectfully
Copy link
Contributor

This adds a couple of tests that builtins can be partially applied.

But we actually had such terms already. For example

-- |  'sum' as a PLC term.
--
-- > /\(s :: *) -> \(ss : size s) ->
-- >     foldList {integer s} {integer s} (addInteger {s}) (resizeInteger {1} {s} ss 1!0)
sum :: TermLike term TyName Name => term ()
sum = runQuote $ do
    s  <- freshTyName () "s"
    ss <- freshName () "ss"
    let sv  = TyVar () s
        int = TyApp () (TyBuiltin () TyInteger) sv
        add = tyInst () (builtin () (BuiltinName () AddInteger)) sv
    return
        . tyAbs () s (Size ())
        . lamAbs () ss (TyApp () (TyBuiltin () TySize) sv)
        . mkIterApp () (mkIterInst () foldList [int, int])
        $ [ add
          , makeDynBuiltinInt sv (var () ss) 0
          ]

I also changed typed generation of terms a bit: it is now more interesting in that it can generate constants in addition to somewhat long terms. I checked manually and observed that indeed more patterns now get generated than previously.

@michaelpj
Copy link
Contributor

Great 👍

@michaelpj michaelpj merged commit 6949d4d into IntersectMBO:master Mar 27, 2019
@effectfully effectfully deleted the effectfully/test/unsaturated-builtin branch March 27, 2019 09:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants