search

HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Nat.show is not working #84

Closed neocastro closed 4 years ago

neocastro commented 4 years ago

Trying to show a Nat by running fmcio hello on 

hello: IO(Unit)
  IO.print(Nat.show,  1)

results in

/usr/lib/node_modules/formality-lang/FormalityCore.js:225
        switch (func.ctor) {
                     ^

TypeError: Cannot read property 'ctor' of undefined
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:225:22)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:224:20)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:224:20)
    at reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:227:20)
    at Object.reduce (/usr/lib/node_modules/formality-lang/FormalityCore.js:227:20)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:201:18)
    at infer (/usr/lib/node_modules/formality-lang/FormalityComp.js:146:26)
    at infer (/usr/lib/node_modules/formality-lang/FormalityComp.js:140:22)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:247:22)
    at check (/usr/lib/node_modules/formality-lang/FormalityComp.js:239:22)
johnchandlerburnham commented 4 years ago

I think this is a problem in Nat.show.digit, since 

hello : String
  String.pure(Nat.show.digit(0,10))

results in the same error.

If I change Nat.show.digit to:

Nat.show.digit(n: Nat, base: Nat): Char
  let m = Nat.mod(n, base)
  case Nat.eql(m, 0):  | '0'; |
  case Nat.eql(m, 1):  | '1'; |
  case Nat.eql(m, 2):  | '2'; |
  case Nat.eql(m, 3):  | '3'; |
  case Nat.eql(m, 4):  | '4'; |
  case Nat.eql(m, 5):  | '5'; |
  case Nat.eql(m, 6):  | '6'; |
  case Nat.eql(m, 7):  | '7'; |
  case Nat.eql(m, 8):  | '8'; |
  case Nat.eql(m, 9):  | '9'; |
  case Nat.eql(m, 10): | 'a'; |
  case Nat.eql(m, 11): | 'b'; |
  case Nat.eql(m, 12): | 'c'; |
  case Nat.eql(m, 13): | 'd'; |
  case Nat.eql(m, 14): | 'e'; |
  case Nat.eql(m, 15): | 'f'; |
    '#';;;;;;;;;;;;;;;;

removing Char.parse, then it Nat.show.digit(0,10) prints '#' which is wrong and your example errors with

undefined:51
  var Nat$show$aux = n$1=>base$2=>str$3=>{var Nat$show$aux=n$1=>base$2=>str$3=>({ctr:'TCO',arg:[n$1,base$2,str$3]});while(true){var R=(()=>{var self=(({_:'Pair.new','a':n$1/base$2,'b':n$1%base$2}));switch(self._){case 'Pair.new':var $18=self.fst;var $19=self.snd;return (()=>{var self=$18;switch(self===0n?'zero':'succ'){case 'zero':return String$cons(Nat$show$digit($19)(base$2))(str$3);case 'succ':var $20=(self-1n);return Nat$show$aux($18)(base$2)(String$cons(Nat$show$digit($19)(base$2))(str$3));}})();}})();if(R.ctr==='TCO')[n$1,base$2,str$3]=R.arg;else return R;}};
                                                                                                                                                                                                                                                                                                                                                                                                                             ^

TypeError: Cannot mix BigInt and other types, use explicit conversions
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:51:414)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:51:504)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:51:510)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:52:63)
    at Nat$show (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:53:42)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:54:15)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:82:3)
    at Object._io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5)
    at Object.<anonymous> (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/fmcio.js:2:21)
    at Module._compile (internal/modules/cjs/loader.js:776:30)

Seems like theres a compiler error, and/or the show functions are wrong. I will test further and update the Nat show functions

johnchandlerburnham commented 4 years ago

Okay, I think this is a problem with how List(Char) gets compiled

String.from_list(xs: List(Char)) : String
  case xs:
  | String.nil;
  | String.cons(xs.head,String.from_list(xs.tail));

String.test : String
  String.from_list(List.nil<>)

errors with

Λ ➜ fmcio String.test
undefined:26
  var String$from_list = (xs$1=>(()=>{var self=xs$1;switch(self.length===0?'nil':'cons'){case 'nil':return String$nil;case 'cons':var $8=self.charCodeAt(0);var $9=self.slice(1);return String$cons($8)(String$from_list($9));}})());
                                                                                                                                              ^

TypeError: self.charCodeAt is not a function
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:26:143)
    at String$from_list (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:26:226)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:28:21)
    at eval (eval at _io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5), <anonymous>:36:3)
    at Object._io_ (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/lib.js:186:5)
    at Object.<anonymous> (/home/jcb/.npm-global/lib/node_modules/formality-lang/bin/fmcio.js:2:21)
    at Module._compile (internal/modules/cjs/loader.js:1151:30)
    at Object.Module._extensions..js (internal/modules/cjs/loader.js:1171:10)
    at Module.load (internal/modules/cjs/loader.js:1000:32)
    at Function.Module._load (internal/modules/cjs/loader.js:899:14)

js output is https://gist.github.com/johnchandlerburnham/7f4000eb3923ed5b72b5124728d94be7

VictorTaelin commented 4 years ago

Thanks. Fixed on https://github.com/moonad/Formality/commit/c286ac61e4e7c378a3be5430b8d4b1e7fa55cdfa