search

cicada-lang / mugda

An implementation of the mugda paper
GNU General Public License v3.0
2 stars 2 forks source link

Can not handle abstraction over constructor #7

Open xieyuheng opened 2 years ago

xieyuheng commented 2 years ago

The following definition of sub-to-zero with an abstraction my-add1 over constructor add1 can not pass termination-check:

(data Nat () ()
  [zero () Nat]
  [add1 ([prev Nat]) Nat])

(fn my-add1 (-> Nat Nat)
  [(x) (add1 x)])

(fn sub-to-zero (-> Nat Nat)
  [((zero)) zero]
  [((add1 (zero))) zero]
  [((add1 (add1 x))) (sub-to-zero (my-add1 x))])

test: https://github.com/cicada-lang/mugda/blob/master/tests/termination/sub-to-zero-indirect-add1.error.mu

xieyuheng commented 2 years ago

We need to compare with Coq and Agda to see should this work or not.

xieyuheng commented 2 years ago

Maybe we can solve this by