ucsd-pl / refscript Goto Github PK

@panagosg7 can you tweak the ts-rs translator to handle

https://github.com/UCSD-PL/RefScript/blob/bitwise/tests/pos/misc/bitwise-00.ts

thanks!

See

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/fb/min-index-01.ts

What is this mysterious null that it is trying to convert to number ????

Also, how would one go about typing reduce in

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/fb/min-index-02.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/foldl1.ts

This should be UNSAFE, preferably with a much more useful error than "rsc: Prelude.foldl1: empty list"

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/alias.ts

Easy workaround is to avoid using type aliases in such situations.

See:

https://github.com/UCSD-PL/RefScript/blob/void/tests/pos/misc/void.ts

As explained in http://stackoverflow.com/questions/4806286/difference-between-void-0-and-undefined, "void 0" is sometimes used instead of "undefined" both because it's fewer characters and because window.undefined is writable (though why anyone would want to write over it...)

See:

https://github.com/UCSD-PL/RefScript/blob/poly/tests/pos/misc/poly-01.ts

Basically, we need to add the polymorphic instantiation variables at the use of idd on line 15 (currently, this is just done at fun-call, but actually needs to happen at any use of a function, including as a parameter as is happening here.)

rsc should catch type-checking (or other errors) thrown by tsc
and raise them and exit gracefully. This will let us (eventually) use
rsc as a drop in replacement for tsc.

See for, example: tests/todo/tscErr.hs

(This may be a good project for @bmcfluff to dip his toes in the code base.)

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/field-scope.ts

@panagosg7 why is this not supported? There is no reason we can't handle this, adding a bogus "undefined" assignment is bad because

https://github.com/UCSD-PL/RefScript/blob/varinit/tests/pos/misc/init-00.ts
https://github.com/UCSD-PL/RefScript/blob/varinit/tests/pos/misc/init-01.ts
https://github.com/UCSD-PL/RefScript/blob/varinit/tests/pos/misc/init-02.ts

A. it forces us to weaken the type (to X + undefined) and
B. that weakened union pervades throughout and is in general unnecessary.

The whole point of the SSA was to support potentially different types and undefined vars in exactly these kinds of cases...

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/short-circuit.ts

Description here: https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/in

See 'in_operator' branch

https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/pos/inclusion/in-00.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/pos/inclusion/in-01.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/pos/inclusion/in-02.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/pos/inclusion/in-03.ts

https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/neg/inclusion/in-00.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/neg/inclusion/in-01.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/neg/inclusion/in-02.ts
https://github.com/UCSD-PL/RefScript/blob/in_operator/tests/neg/inclusion/in-03.ts

Why things are taking so long. e.g.

time rsc tests/pos/simple/error.ts

5.62 real         5.40 user         0.16 sys

The actual body of the file is just

throw new Error("");

And so, the time in fixpoint is instantaneous.

This is not the biggest issue but worth looking into at some point...

We should not be mixing scrapeQualifiers into constraint generation, that should be a strictly external and heuristic process. In other words, scrapeQualifiers should not ever be (transitively) called from consNano and code like:

consCall g l fn es ft0 
  = do (xes, g')    <- consScan consExpr g es
       -- Attempt to gather qualifiers here -- needed for object literal quals
       ts           <- mapM scrapeQualifiers [envFindTy x g' | x <- xes]

should be undone.

https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Function/call
https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Function/apply

Appear in d3 sources:
https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/min.ts
https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/map.ts
https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/extent.ts
etc.

Unit tests:
https://github.com/UCSD-PL/RefScript/blob/variadic/tests/pos/simple/variadic-00.ts
https://github.com/UCSD-PL/RefScript/blob/variadic/tests/pos/simple/variadic-01.ts

https://github.com/UCSD-PL/RefScript/blob/variadic/tests/neg/simple/variadic-00.ts
https://github.com/UCSD-PL/RefScript/blob/variadic/tests/neg/simple/variadic-01.ts

See the function fails in

https://github.com/UCSD-PL/RefScript/blob/truthy_test/tests/pos/unions/choice-00.ts

We should have some means of importing foo.d.ts files (maybe not that exact file, but, say a foo.d.rs file at the same location. This is so that rsc can directly crunch files like:

• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/ascending.ts
• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/descending.ts

etc. Right now, it complains about unbound variable d3 etc.

See:

https://github.com/UCSD-PL/RefScript/blob/float/tests/pos/misc/float-00.ts

No need for anything fancy, just parse and type as "{number | true}".

This may be a good exercise for @bmcfluff (but note that it does touch the type
system...)

It turns out it's not safe to even drop the refinements of the union top-level to the parts of the union:

{ t1 + t2 + ... | p } ---> { t1 | p } + { t2 | p } + ...

The reason is that p could include predicates of the form v = x which would cause "sort mismatch" if dropped to the tis. Even dropping a K-var could be dangerous as a seemingly non-existing predicate of that sort could emerge as part of a K-var instantiation and violate a sort check.

Here's an example that throws an exception due to sort mismatch:

https://github.com/UCSD-PL/RefScript/blob/union_preds/tests/pos/unions/noundef-02.ts

https://github.com/UCSD-PL/RefScript/blob/enumerations/tests/pos/objects/enum-00.ts
https://github.com/UCSD-PL/RefScript/blob/enumerations/tests/pos/objects/enum-01.ts

https://github.com/UCSD-PL/RefScript/blob/enumerations/tests/neg/objects/enum-00.ts
https://github.com/UCSD-PL/RefScript/blob/enumerations/tests/neg/objects/enum-01.ts

See:

https://github.com/UCSD-PL/RefScript/blob/badspec/tests/neg/badspec/badspec-00.ts

Currently reported "SAFE", presumably by using the TS types but we should flag an error
when we get junk specifications (e.g. with undefined types.)

See:

https://github.com/UCSD-PL/RefScript/blob/for-loop/tests/pos/loops/for-06.ts

The first function passes but the second causes "PANIC: Unexpected Error: TypeError: Cannot call method 'toRsForInit' of null"

See:

https://github.com/UCSD-PL/RefScript/blob/func-arg/tests/pos/misc/func-arg.ts

(can also rename arguments as a workaround)

See:

https://github.com/UCSD-PL/RefScript/blob/underscore-var/tests/pos/misc/underscore-00.ts

Note that in other contexts _ seems to work fine:

https://github.com/UCSD-PL/RefScript/blob/underscore-var/tests/pos/misc/underscore-01.ts

See:

https://github.com/UCSD-PL/RefScript/blob/break-statement/tests/pos/loops/break.ts

See:

https://github.com/UCSD-PL/RefScript/blob/unaryplus/tests/pos/operators/choice.ts

Example:

https://github.com/UCSD-PL/RefScript/blob/forin/tests/pos/simple/forin-00.ts
https://github.com/UCSD-PL/RefScript/blob/forin/tests/pos/simple/forin-01.ts

https://github.com/UCSD-PL/RefScript/blob/forin/tests/neg/simple/forin-00.ts
https://github.com/UCSD-PL/RefScript/blob/forin/tests/neg/simple/forin-01.ts

/*@ x :: { } */
declare var x;
x.hasOwnProperty("prop");

See:

https://github.com/UCSD-PL/refscript/blob/798f5369aca055823646fb690d12bf3e4f91333e/tests/todo/weird/slowMul.ts

Examples:
https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/simple/bitVector.ts
https://github.com/UCSD-PL/RefScript/blob/master/tests/neg/simple/bitVector.ts
Are working already but with manual manipulation of bitvectors.

Also:
https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/features/bitVector.ts
Is not working yet, because we haven't encoded axioms like:

 a non-zero number has at least one bit non-zero

or

A & B has at most as many 1s as A or B has

and so on

Also, may as well use TS style type parameter instantiation. In short, get this to work:

https://github.com/UCSD-PL/RefScript/blob/parser/tests/pos/typealias/talias-04.ts

See:

https://github.com/UCSD-PL/RefScript/tree/master/tests/todo/do-while.ts

See

https://github.com/UCSD-PL/RefScript/blob/typealias/tests/pos/typealias/talias-04.ts

puzzled because

https://github.com/UCSD-PL/RefScript/blob/typealias/tests/pos/typealias/talias-03.ts

seems to work fine. Also,

https://github.com/UCSD-PL/RefScript/blob/typealias/tests/neg/typealias/talias-010.ts

should be rejected as it is a soundness bug (of sorts...)

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/weird/this-out-of-scope.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/immutable-field.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/tvar-scope.ts

See:

https://github.com/UCSD-PL/RefScript/blob/arrayspec/tests/pos/arrays/map-00.ts
https://github.com/UCSD-PL/RefScript/blob/arrayspec/tests/pos/arrays/map-01.ts
https://github.com/UCSD-PL/RefScript/blob/arrayspec/tests/pos/arrays/filter-00.ts
https://github.com/UCSD-PL/RefScript/blob/arrayspec/tests/pos/arrays/filter-01.ts

The first of the filter tests, is actually about subtyping: currently we get:

/Users/rjhala/research/liquid/RefScript/tests/pos/arrays/filter-00.ts:14:28-14:34: Error: TC-ERROR
Function type '(x:number + undefined) => boolean' is not a subtype of '(x:number) => boolean'

but of course, the subtyping does hold...

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/string-accessor.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/union-inference.ts

Assume we have a type:

interface A {
  c: int;
  f: forall T . (T) => T; 
}

Then for doing the subtyping:

A <: { f: (int) => int }

we'd have to first unfold A into

{
  c: number;
  f: forall T . (T) => T; 
}

Then deeply instantiate all quantified types:

{
  c: number;
  f: (T0) => T0; 
}

Unify: T0 := int

Finally, do the subtyping:

{ c: number; f: (T0) => T0; } [T0: int] <: { f: (int) => int; } ~> UPCAST

Example:
https://github.com/UCSD-PL/RefScript/blob/poly-subt/tests/pos/simple/contextual.ts

See:

https://github.com/UCSD-PL/RefScript/blob/unaryplus/tests/pos/operators/unary-plus-00.ts

For now, we could type this as:

builtin_PrefixPlus :: (x: number) => {v:number | v = x}

And not worry about the various use-cases listed here.
https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/Arithmetic_Operators#Unary_plus_(.2B)

https://github.com/UCSD-PL/RefScript/blob/fix_funcsigs/tests/neg/simple/fun-05.ts
https://github.com/UCSD-PL/RefScript/blob/fix_funcsigs/tests/pos/simple/fun-05.ts

Safe downcasts based on arbitrary tag checks.

https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/pos/misc/animals.ts
https://github.com/UCSD-PL/RefScript/blob/arbitrary_tags/tests/neg/misc/animals.ts

Hmm. Why is SSA not using weak super type (declared in code -- HTML)

https://github.com/UCSD-PL/RefScript/blob/ssajoin/tests/pos/classes/createElt.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/eq.ts

(though === is usually an acceptable workaround)

Currently when running the following

• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/keys-0.ts
• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/values-0.ts
• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/entries-0.ts
• https://github.com/UCSD-PL/rs-benchmarks/blob/master/d3/src-ts/arrays/permute-0.ts

I get the following parse errors:

$ rsc liquid keys-0.ts 
EXEC: tsc --outDir ./.liquid --refscript keys-0.ts
rsc: Error while parsing: "forall T . ( map: {  } ) => [ string ]"
At position: /Users/rjhala/research/liquid/rs-benchmarks/d3/src-ts/arrays/keys-0.ts:3:15-7:2

$ rsc liquid values-0.ts 
EXEC: tsc --outDir ./.liquid --refscript values-0.ts
rsc: Error while parsing: "forall T . ( map: {  } ) => [ T ]"
At position: /Users/rjhala/research/liquid/rs-benchmarks/d3/src-ts/arrays/values-0.ts:3:17-7:2

$ rsc liquid entries-0.ts 
EXEC: tsc --outDir ./.liquid --refscript entries-0.ts
rsc: Error while parsing: "forall T . ( map: {  } ) => [ { key: string; value: T } ]"
At position: /Users/rjhala/research/liquid/rs-benchmarks/d3/src-ts/arrays/entries-0.ts:3:18-7:2

$ rsc liquid permute-0.ts 
EXEC: tsc --outDir ./.liquid --refscript permute-0.ts
rsc: Error while parsing: "forall T . ( array: [ T ], indexes: [ number ] ) => [ T ]"
At position: /Users/rjhala/research/liquid/rs-benchmarks/d3/src-ts/arrays/permute-0.ts:3:18-7:2

See:

https://github.com/UCSD-PL/RefScript/blob/callable-interface/tests/pos/misc/callable-interface.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/tvar-intersection.ts

Why is rsc throwing a "pattern match error" on

https://github.com/UCSD-PL/RefScript/blob/master/tests/pos/fb/min-index-02.ts

I'm guessing it has to do with a missing type-annotation but a random pattern match error is not very helpful ...

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/null-undef-literals.ts

See:

https://github.com/UCSD-PL/RefScript/blob/master/tests/todo/non-linear.ts