The caledon from mmirman

Caledon stalls when inferring some arguments.

For example, the following will stall when lpn is reached.

defn list : prop → prop
  >| nil = list P
  >| cons = P → list P → list P

defn lp : {P : prop} list P → prop
   | lpn = lp nil
   | lpc = {l : list P} {e : P} lp l → lp (cons e l)

By changing that line to | lpn = lp {P = P} nil, the stalling doesn't happen, but I think Caledon should be smart enough to know that P can't be inferred and report an error instead of stalling.

As an aside, this glitch doesn't occur for this program;

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn append : {P : prop} list P -> list P -> list P -> prop
   | nila = {l : list P} append nil l l
   | nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)

nor this program

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn last : {P : prop} list P -> P -> prop
  | lastn = {e : P} last (cons e nil) e
  | lastc = {l : list P} {le e : P} last l e -> last (cons le l) e

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)

but it does occur for this program

defn num  : prop
   >| zero = num
   >| succ = [n : num] num

defn list : prop -> prop
   >| nil = list P
   >| cons = P -> list P -> list P

defn append : {P : prop} list P -> list P -> list P -> prop
   | nila = {l : list P} append nil l l
   | nilc = {l m n : list P} {a : P} append l m n -> append (cons a l) m (cons a n)

defn last : {P : prop} list P -> P -> prop
  | lastn = {e : P} last (cons e nil) e
  | lastc = {l : list P} {le e : P} last l e -> last (cons le l) e

defn length : {P : prop} list P -> num -> prop
  | lengthn = length nil zero
  | lengthc = {l : list P} {e : P} {n : num} length l n -> length (cons e l) (succ n)

stalling on lengthn. This is an odd glitch which is clearly sensitive to context, but I'm not certain how to describe it beyond these examples.

Parser stalls on some bad inputs.

For whatever reason, the Caledon program will stall, eating up an arbitrarily large amount of memory when encountering certain code which should instead produce syntax errors. Here are some examples of code which, if encountered, will trigger what I'm talking about;

defn unit : prop
  as

defn unit : prop
  as \(P : prop) P . P

defn unit : prop
  as [P : prop] P -> P

defn tt : unit
  as \0 p . p

defn unit : prop
  | tt =

defn unit : prop
  | tt = \(P : prop) . unit

defn unit : prop
   | one  = unit

a(

mmirman / caledon Goto Github PK

caledon's People

Contributors

Stargazers

Watchers

Forkers

caledon's Issues

Caledon stalls when inferring some arguments.

Parser stalls on some bad inputs.

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent