C Compilation issues.

[mariari]

I tried to compile my tak program to C, but when I try to compile that with gcc I get

tak.c: In function ‘takclosbranch_257’:
tak.c:627:28: error: too few arguments to function ‘(V_71_t * (*)(minijuvix_function_t *, V_71_t *, V_71_t *, V_71_t *, Unit_241_t *))fa0->fun’
  627 |                   Box_385(((V_71_t * (*)(minijuvix_function_t *,
      |                           ~^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  628 |                                          V_71_t *,
      |                                          ~~~~~~~~~
  629 |                                          V_71_t *,
      |                                          ~~~~~~~~~
  630 |                                          V_71_t *,
      |                                          ~~~~~~~~~
  631 |                                          Unit_241_t *)) fa0->fun)(fa0, fa1, fa2, fa3)),
      |                                          ~~~~~~~~~~~~~~~~~~~~~~~~
tak.c: In function ‘main’:

with a bunch of different warnings. The code can be found here

module Tak;

open import Prelude;
open import Data.Nat;
open import Data.Nat.Ord;
open import Complex;
     import Data.Bool;
open import Data.Ord;

-① : ℕ → ℕ;
-① (suc x) ≔ x;
-① zero    ≔ zero;


inductive Unit {
  unit : Unit;
};

inductive Thunk (A : Type) {
  box : (Unit → A) → Thunk A;
};

call : {A : Type} → Thunk A → A;
call (box thunk) ≔ thunk unit;

if : {A : Type} → Data.Bool.Bool → (Thunk A) → (Thunk A) → A;
if Data.Bool.true  then else ≔ call then;
if Data.Bool.false then else ≔ call else;

tak-clos-else : ℕ → Unit → ℕ;
tak-clos-else z unit ≔ z;

terminating
tak-clos-branch : (ℕ → ℕ → ℕ → Unit → ℕ) → ℕ → ℕ → ℕ → ℕ;
tak-clos-branch tak-clos-then x y z ≔
  if (isLT (compare y x))
     (box (tak-clos-then x y z))
     (box (tak-clos-else z));

terminating
tak-clos-then : ℕ → ℕ → ℕ → Unit → ℕ;
tak-clos-then x y z unit ≔
   tak-clos-branch tak-clos-then
                  (tak-clos-branch tak-clos-then (-① x) y z)
                  (tak-clos-branch tak-clos-then (-① y) z x)
                  (tak-clos-branch tak-clos-then (-① z) x y);


terminating
tak' : ℕ → ℕ → ℕ → ℕ;
tak' ≔ tak-clos-branch tak-clos-then;

terminating tak      : ℕ → ℕ → ℕ → ℕ;
terminating tak-then : ℕ → ℕ → ℕ → Unit -> ℕ;
            tak-else : ℕ → Unit → ℕ;

tak-then x y z unit ≔
  (tak (tak (-① x) y z)
       (tak (-① y) z x)
       (tak (-① z) x y));

tak-else z unit ≔ z;

tak x y z ≔
  if (isLT (compare y x))
     (box (tak-then x y z))
     (box (tak-else z));

main : ℕ;
main ≔ tak zero zero zero;

end;

[paulcadman]

I can reproduce this, but I need to investigate more why the closure generation fails in this case.

[lukaszcz]

I think this is the same issue as #1596. Partial application will be fixed with the new backend.