sdfsdf.idr

-- makeHasIO "what" Private ["c:foo","javascript:borp"] `[ prim_gob : Int -> Int -> PrimIO Int ]
-- This generates:
-- %foreign "c:foo" "javascript:borp"
-- prim_gob : Int -> Int -> PrimIO Int
-- And:
-- private
-- what : HasIO io => Int -> Int -> io Int
makeHasIO : String -> Visibility -> List String -> List Decl -> Elab ()
makeHasIO funname0 vis str ys = do
    [(IClaim pfc pmw pvis _ pty@(MkTy tyfc primname primty))] <- pure ys
      | _ => fail "bad format"
    let funty = IPi EmptyFC MW AutoImplicit Nothing
               `(HasIO ~(IBindVar EmptyFC "io"))
               (spiderType primty)
        funname = UN funname0
        primclaim = IClaim pfc pmw pvis [ForeignFn str] pty
        funclaim = IClaim EmptyFC pmw vis [] (MkTy tyfc funname funty)
        varnames = map (("var" ++) . show) [0..]
        lvars = IBindVar EmptyFC <$> take (argCount primty) varnames
        rvars = IVar EmptyFC . UN <$> take (argCount primty) varnames
        lhs = foldl (\xs,x => `(~xs ~x)) (IVar EmptyFC funname) lvars
        rhs = IApp EmptyFC `(primIO) (foldl (\xs,x => `(~xs ~x)) (IVar EmptyFC primname) rvars)
        patclause = PatClause EmptyFC lhs rhs
        funbody = IDef EmptyFC funname [patclause]
    declare [primclaim] -- declare the primitive as-given
    declare [funclaim, funbody] -- declare our HasIO version
    pure ()
  where
    argCount : TTImp -> Nat
    argCount (IPi _ _ _ _ _ retty) = S (argCount retty)
    argCount retty = Z
    
    spiderType : TTImp -> TTImp -- replace 'PrimIO' with 'io'
    spiderType (IPi a b c d e retty) = IPi a b c d e (spiderType retty)
    spiderType (IApp _ `(PrimIO) retty) = IApp EmptyFC (IBindVar EmptyFC "io") retty
    spiderType ty = ty

-- try :t prim_gob 
-- try :t what
-- try :printdef what
-- try :exec what 15 3 >>= printLn
%runElab makeHasIO "what" Private [believe_me `("C:div,libc,math.h")] `[ prim_gob : Int -> Int -> PrimIO Int ]