infernu (empty) → 0.0.0.0
raw patch · 24 files changed
+3586/−0 lines, 24 filesdep +QuickCheckdep +basedep +containerssetup-changed
Dependencies added: QuickCheck, base, containers, derive, digits, either, fgl, infernu, language-ecmascript, mtl, optparse-applicative, parsec, transformers
Files
- LICENSE +280/−0
- Main.hs +27/−0
- README.md +188/−0
- Setup.hs +2/−0
- infernu.cabal +125/−0
- src/Infernu/Builtins/Array.hs +67/−0
- src/Infernu/Builtins/Operators.hs +77/−0
- src/Infernu/Builtins/Regex.hs +31/−0
- src/Infernu/Builtins/String.hs +51/−0
- src/Infernu/Builtins/TypeClasses.hs +32/−0
- src/Infernu/Decycle.hs +30/−0
- src/Infernu/Fix.hs +41/−0
- src/Infernu/Infer.hs +448/−0
- src/Infernu/InferState.hs +425/−0
- src/Infernu/Lib.hs +30/−0
- src/Infernu/Log.hs +27/−0
- src/Infernu/Options.hs +34/−0
- src/Infernu/Parse.hs +281/−0
- src/Infernu/Pretty.hs +227/−0
- src/Infernu/Types.hs +578/−0
- src/Infernu/Unify.hs +481/−0
- src/Infernu/Util.hs +67/−0
- test/Demo.hs +26/−0
- test/Test.hs +11/−0
+ LICENSE view
@@ -0,0 +1,280 @@+ GNU GENERAL PUBLIC LICENSE+ Version 2, June 1991++ Copyright (C) 1989, 1991 Free Software Foundation, Inc.,+ 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA+ Everyone is permitted to copy and distribute verbatim copies+ of this license document, but changing it is not allowed.++ Preamble++ The licenses for most software are designed to take away your+freedom to share and change it. By contrast, the GNU General Public+License is intended to guarantee your freedom to share and change free+software--to make sure the software is free for all its users. This+General Public License applies to most of the Free Software+Foundation's software and to any other program whose authors commit to+using it. (Some other Free Software Foundation software is covered by+the GNU Lesser General Public License instead.) You can apply it to+your programs, too.++ When we speak of free software, we are referring to freedom, not+price. Our General Public Licenses are designed to make sure that you+have the freedom to distribute copies of free software (and charge for+this service if you wish), that you receive source code or can get it+if you want it, that you can change the software or use pieces of it+in new free programs; and that you know you can do these things.++ To protect your rights, we need to make restrictions that forbid+anyone to deny you these rights or to ask you to surrender the rights.+These restrictions translate to certain responsibilities for you if you+distribute copies of the software, or if you modify it.++ For example, if you distribute copies of such a program, whether+gratis or for a fee, you must give the recipients all the rights that+you have. You must make sure that they, too, receive or can get the+source code. And you must show them these terms so they know their+rights.++ We protect your rights with two steps: (1) copyright the software, and+(2) offer you this license which gives you legal permission to copy,+distribute and/or modify the software.++ Also, for each author's protection and ours, we want to make certain+that everyone understands that there is no warranty for this free+software. If the software is modified by someone else and passed on, we+want its recipients to know that what they have is not the original, so+that any problems introduced by others will not reflect on the original+authors' reputations.++ Finally, any free program is threatened constantly by software+patents. We wish to avoid the danger that redistributors of a free+program will individually obtain patent licenses, in effect making the+program proprietary. To prevent this, we have made it clear that any+patent must be licensed for everyone's free use or not licensed at all.++ The precise terms and conditions for copying, distribution and+modification follow.++ GNU GENERAL PUBLIC LICENSE+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION++ 0. This License applies to any program or other work which contains+a notice placed by the copyright holder saying it may be distributed+under the terms of this General Public License. The "Program", below,+refers to any such program or work, and a "work based on the Program"+means either the Program or any derivative work under copyright law:+that is to say, a work containing the Program or a portion of it,+either verbatim or with modifications and/or translated into another+language. (Hereinafter, translation is included without limitation in+the term "modification".) Each licensee is addressed as "you".++Activities other than copying, distribution and modification are not+covered by this License; they are outside its scope. The act of+running the Program is not restricted, and the output from the Program+is covered only if its contents constitute a work based on the+Program (independent of having been made by running the Program).+Whether that is true depends on what the Program does.++ 1. You may copy and distribute verbatim copies of the Program's+source code as you receive it, in any medium, provided that you+conspicuously and appropriately publish on each copy an appropriate+copyright notice and disclaimer of warranty; keep intact all the+notices that refer to this License and to the absence of any warranty;+and give any other recipients of the Program a copy of this License+along with the Program.++You may charge a fee for the physical act of transferring a copy, and+you may at your option offer warranty protection in exchange for a fee.++ 2. You may modify your copy or copies of the Program or any portion+of it, thus forming a work based on the Program, and copy and+distribute such modifications or work under the terms of Section 1+above, provided that you also meet all of these conditions:++ a) You must cause the modified files to carry prominent notices+ stating that you changed the files and the date of any change.++ b) You must cause any work that you distribute or publish, that in+ whole or in part contains or is derived from the Program or any+ part thereof, to be licensed as a whole at no charge to all third+ parties under the terms of this License.++ c) If the modified program normally reads commands interactively+ when run, you must cause it, when started running for such+ interactive use in the most ordinary way, to print or display an+ announcement including an appropriate copyright notice and a+ notice that there is no warranty (or else, saying that you provide+ a warranty) and that users may redistribute the program under+ these conditions, and telling the user how to view a copy of this+ License. (Exception: if the Program itself is interactive but+ does not normally print such an announcement, your work based on+ the Program is not required to print an announcement.)++These requirements apply to the modified work as a whole. If+identifiable sections of that work are not derived from the Program,+and can be reasonably considered independent and separate works in+themselves, then this License, and its terms, do not apply to those+sections when you distribute them as separate works. But when you+distribute the same sections as part of a whole which is a work based+on the Program, the distribution of the whole must be on the terms of+this License, whose permissions for other licensees extend to the+entire whole, and thus to each and every part regardless of who wrote it.++Thus, it is not the intent of this section to claim rights or contest+your rights to work written entirely by you; rather, the intent is to+exercise the right to control the distribution of derivative or+collective works based on the Program.++In addition, mere aggregation of another work not based on the Program+with the Program (or with a work based on the Program) on a volume of+a storage or distribution medium does not bring the other work under+the scope of this License.++ 3. You may copy and distribute the Program (or a work based on it,+under Section 2) in object code or executable form under the terms of+Sections 1 and 2 above provided that you also do one of the following:++ a) Accompany it with the complete corresponding machine-readable+ source code, which must be distributed under the terms of Sections+ 1 and 2 above on a medium customarily used for software interchange; or,++ b) Accompany it with a written offer, valid for at least three+ years, to give any third party, for a charge no more than your+ cost of physically performing source distribution, a complete+ machine-readable copy of the corresponding source code, to be+ distributed under the terms of Sections 1 and 2 above on a medium+ customarily used for software interchange; or,++ c) Accompany it with the information you received as to the offer+ to distribute corresponding source code. (This alternative is+ allowed only for noncommercial distribution and only if you+ received the program in object code or executable form with such+ an offer, in accord with Subsection b above.)++The source code for a work means the preferred form of the work for+making modifications to it. For an executable work, complete source+code means all the source code for all modules it contains, plus any+associated interface definition files, plus the scripts used to+control compilation and installation of the executable. However, as a+special exception, the source code distributed need not include+anything that is normally distributed (in either source or binary+form) with the major components (compiler, kernel, and so on) of the+operating system on which the executable runs, unless that component+itself accompanies the executable.++If distribution of executable or object code is made by offering+access to copy from a designated place, then offering equivalent+access to copy the source code from the same place counts as+distribution of the source code, even though third parties are not+compelled to copy the source along with the object code.++ 4. You may not copy, modify, sublicense, or distribute the Program+except as expressly provided under this License. Any attempt+otherwise to copy, modify, sublicense or distribute the Program is+void, and will automatically terminate your rights under this License.+However, parties who have received copies, or rights, from you under+this License will not have their licenses terminated so long as such+parties remain in full compliance.++ 5. You are not required to accept this License, since you have not+signed it. However, nothing else grants you permission to modify or+distribute the Program or its derivative works. These actions are+prohibited by law if you do not accept this License. Therefore, by+modifying or distributing the Program (or any work based on the+Program), you indicate your acceptance of this License to do so, and+all its terms and conditions for copying, distributing or modifying+the Program or works based on it.++ 6. Each time you redistribute the Program (or any work based on the+Program), the recipient automatically receives a license from the+original licensor to copy, distribute or modify the Program subject to+these terms and conditions. You may not impose any further+restrictions on the recipients' exercise of the rights granted herein.+You are not responsible for enforcing compliance by third parties to+this License.++ 7. If, as a consequence of a court judgment or allegation of patent+infringement or for any other reason (not limited to patent issues),+conditions are imposed on you (whether by court order, agreement or+otherwise) that contradict the conditions of this License, they do not+excuse you from the conditions of this License. If you cannot+distribute so as to satisfy simultaneously your obligations under this+License and any other pertinent obligations, then as a consequence you+may not distribute the Program at all. For example, if a patent+license would not permit royalty-free redistribution of the Program by+all those who receive copies directly or indirectly through you, then+the only way you could satisfy both it and this License would be to+refrain entirely from distribution of the Program.++If any portion of this section is held invalid or unenforceable under+any particular circumstance, the balance of the section is intended to+apply and the section as a whole is intended to apply in other+circumstances.++It is not the purpose of this section to induce you to infringe any+patents or other property right claims or to contest validity of any+such claims; this section has the sole purpose of protecting the+integrity of the free software distribution system, which is+implemented by public license practices. Many people have made+generous contributions to the wide range of software distributed+through that system in reliance on consistent application of that+system; it is up to the author/donor to decide if he or she is willing+to distribute software through any other system and a licensee cannot+impose that choice.++This section is intended to make thoroughly clear what is believed to+be a consequence of the rest of this License.++ 8. If the distribution and/or use of the Program is restricted in+certain countries either by patents or by copyrighted interfaces, the+original copyright holder who places the Program under this License+may add an explicit geographical distribution limitation excluding+those countries, so that distribution is permitted only in or among+countries not thus excluded. In such case, this License incorporates+the limitation as if written in the body of this License.++ 9. The Free Software Foundation may publish revised and/or new versions+of the General Public License from time to time. Such new versions will+be similar in spirit to the present version, but may differ in detail to+address new problems or concerns.++Each version is given a distinguishing version number. If the Program+specifies a version number of this License which applies to it and "any+later version", you have the option of following the terms and conditions+either of that version or of any later version published by the Free+Software Foundation. If the Program does not specify a version number of+this License, you may choose any version ever published by the Free Software+Foundation.++ 10. If you wish to incorporate parts of the Program into other free+programs whose distribution conditions are different, write to the author+to ask for permission. For software which is copyrighted by the Free+Software Foundation, write to the Free Software Foundation; we sometimes+make exceptions for this. Our decision will be guided by the two goals+of preserving the free status of all derivatives of our free software and+of promoting the sharing and reuse of software generally.++ NO WARRANTY++ 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY+FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN+OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES+PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED+OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF+MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS+TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE+PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING,+REPAIR OR CORRECTION.++ 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING+WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR+REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES,+INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING+OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED+TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY+YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER+PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE+POSSIBILITY OF SUCH DAMAGES.++ END OF TERMS AND CONDITIONS
+ Main.hs view
@@ -0,0 +1,27 @@+module Main (main) where++import Control.Monad (forM, when)+import qualified Options.Applicative as OptParse+import System.Exit (exitFailure)+import qualified Text.Parsec.Pos as Pos++import Infernu.Infer (pretty)+import Infernu.Options (Options (..), opts)+import Infernu.Types (QualType, Source (..))+import Infernu.Util++process :: [(Source, QualType)] -> [(Pos.SourceName, [String])] -> String+process ts sourceCodes = concatMap (\(f, ds) -> annotatedSource (filteredTypes f ts) ds) sourceCodes+ where filteredTypes f' = filter (\(Source (_, p), _) -> (Pos.sourceName p == f'))++main :: IO ()+main = do+ options <- OptParse.execParser opts+ let files = optFileNames options+ res <- checkFiles options files+ case res of+ Right ts -> when (not $ optQuiet options) $ do sourceCodes <- forM files $ \f -> do d <- readFile f+ return (f, lines d)+ putStrLn $ process ts sourceCodes+ Left e -> putStrLn (pretty e) >> exitFailure+
+ README.md view
@@ -0,0 +1,188 @@+# Infernu++Static type inference for JavaScript.++See the [intro blog post](https://noamlewis.wordpress.com/2015/01/20/introducing-sjs-a-type-inferer-and-checker-for-javascript/) for a short discussion comparing infernu to **other type checkers**.++*(Formerly known as Inferno / Safe JS / SJS)*++**Features:**++* Full type inference: no type annotations necessary.+* Parametric polymorphism (aka "generics"), based on Hindley-Milner type inference.+* Row-type polymorphism, otherwise known as "static duck typing".+* Simple type classes (which allow for example correct support of JS `+` and `[]` operators).+* Recursive types for true representation of object-oriented methods.+* Correct handling of JS's `this` dynamic scoping rules.++For more information see [Infernu's Type System](docs/type-system.md).++## Installation++### Quick and Dirty++ git clone git@github.com:sinelaw/infernu.git+ cd infernu/+ cabal install++Usage: see `infernu --help`+ +Quick example usage:++ echo 'function getLength(x) { return x.length; }' > getLength.js++ infernu getLength.js++Output:++```javascript+ // getLength : a.({length: b, ..c} -> b)+ function getLength(x) { return x.length; }+```+++### A bit more detailed instructions++1. Install Haskell's **cabal** package manager. See [Haskell.org](https://www.haskell.org/downloads) for some installation options. On ubuntu, I recommend using [Herbert V. Riedel's ppa](https://launchpad.net/~hvr/+archive/ubuntu/ghc).+2. Clone this repository.++Then run:++ cabal update+ cd infernu+ cabal install++The `infernu` executable will be installed to your `~/.cabal/bin`. You may want to add it to your `PATH`.++If you have trouble in the last command due to package incompatibilities, use a **cabal sandbox**:++ cd infernu+ cabal sandbox init+ cabal install++The `infernu` executable will be placed in `infernu/.cabal-sandbox/bin`++++## Examples++### Basic++JavaScript:++ var num = 2;+ var arrNums = [num, num];++Infernu infers:++ // num : Number+ // arrNums : [Number]++That is, an array of numbers.++Objects:++ var obj = { something: 'hi', value: num };++Inferred type:++ // obj : {something: String,+ value: Number}++That is, an object with two properties: 'something', of type string, and 'value' of type number.++### Functions and `this`++In JS, `this` is one truly awful part. `this` is a dynamically scoped variable that takes on values depending on how the current function was invoked. Infernu knows about this (pun intended) and infers types for functions indicating what `this` must be.++For example:++ function useThisData() {+ return this.data + 3;+ }++Infernu infers:++ // useThisData : {data: Number, ..a}.(() -> Number)++In words: a function which expects `this` to be an object with at least one property, "data" of type `Number`. It takes no arguments (hence the empty `()`). It returns a `Number`.++If we call a function that needs `this` incorrectly, Infernu will be angry:++ Error: Could not unify:+ {data: Number, ..a}+ With:+ Undefined++Because we called `useThisData` without a preceding object property access (e.g. `obj.useThisData`), it will get `undefined` for `this`. Infernu is telling us that our expected type for `this` is not unifiable with the type `undefined`.++### Polymorphism++Given the following function:++ function makeData(x) {+ return {data: x};+ }++Infernu infers the following type:++ a.(b -> {data: b})++In words: A function that takes anything for its `this`, and an argument of any type `b`. It returns an object containing a single field, `data` of the same type `b` as the argument.++### Row-type polymorphism (static duck typing)++Given the following function:++ function getData(obj) {+ return obj.data;+ }++Infernu infers:++ h.({data: i, ..j} -> i)++In words: a function taking any type `h` for `this`, and a parameter that contains **at least one property**, named "data" that has some type `i` (could be any type). The function returns the same type `i` as the data property.+++### Type Classes++See [here](docs/type-system.md#type-classes) for more about Infernu's type classes.++The basic example is for the `+` operator:++ function add(x,y) { return x + y; }++The type for `add` is inferred to be:++ // add : Plus b => a.((b, b) -> b)++Meaning: given any type `a` that is an instance of the `Plus` type class, the function takes two `a`s and returns an `a`.++The two instances of `Plus` currently defined are the types `Number` and `String`.++++------------++## TODO++- [ ] consider adding sum types with guards as pattern matchers. required because some functions, like array index access, can return 'undefined' (e.g. if index is out of range)+- [ ] allow empty var decls (use first assignment as starting point for types) - how to prevent uninitialized variable issues?+- [ ] allow defining constructor-object properties using the notation `obj.prototype.something = ...`+- [ ] find a reasonable solution for optional parameters - perhaps using an implicit "Maybe"-like type or implicit type unions, and require guards?+- [ ] when concluding that two recursive types are equivalent, use that information to simplify the resulting types (perhaps using the simpler of the two everywhere)+- [ ] BUG: top-level type of naked object `{a:3}` isn't shown unless it is wrapped in a paren `({a:3})`.+- [ ] support `arguments` (a tuple?) and function `bind`+- [ ] Should we treat functions as objects with properties? the only properties they have are: length (very weird! we might as well leave it out), and call/bind/apply (which need special handling)++### Future++- [ ] type annotations+- [ ] add support for CommonJS modules+- [ ] deal better with inferred polymorphic object properties - requires full rank-n unification++<!-- LocalWords: JS polymorphism Hindley Milner JS's Equi num arrNums Number String getData+ -->+<!-- LocalWords: useThisData Undefined unifiable makeData TODO decls paren CommonJS+ -->
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ infernu.cabal view
@@ -0,0 +1,125 @@+name: infernu+version: 0.0.0.0+synopsis: Type inference and checker for JavaScript (experimental)+description: This version is highly experimental and may set your computer on fire (also, a lot of JS is not supported yet, so it may not be very useful.)+ .+ Infernu is a type checker for JavaScript. Since JavaScript is dynamically and weakly typed, it makes no sense to talk about "type errors" in arbitrary JavaScript code.+ .+ Consequently Infernu makes assumptions about the code and expects it to follow certain rules that+ are not required by plain JavaScript (for example, implicit coercions such as `3 + 'a'` are not+ allowed.)+ .+ Infernu's type system is designed for writing dynamic-looking code in a safe statically type-checked+ environment. Type annotations are not required (though they would be nice to support, for various+ reasons). Instead, Infernu *infers* the types of expressions by examining the code. If the inferred+ types contradict each other, Infernu reports the contradiction as an error.+ .+ Infernu places restrictions on JS programs that are otherwise valid. In other words, Infernu is a+ **subset of JavaScript**. Infernu tries to strike a balance between type system complexity and+ dynamic-style coding flexibility.+ .+ See the .md files included in the package for more information.+ +license: GPL-2+homepage: https://github.com/sinelaw/infernu+bug-reports: https://github.com/sinelaw/infernu/issues+license-file: LICENSE+author: Noam Lewis+maintainer: jones.noamle@gmail.com+copyright: Noam Lewis, 2014-2015+-- category:+build-type: Simple+extra-source-files: README.md+cabal-version: >=1.10+stability: experimental++source-repository head+ type: git+ location: git@github.com:sinelaw/infernu.git++ +flag quickcheck+ default: False+ manual: True++flag trace+ default: False+ manual: True++flag debug+ default: False+ manual: True++library+ hs-source-dirs: src+ exposed-modules: Infernu.Builtins.Array+ , Infernu.Builtins.Operators+ , Infernu.Builtins.Regex+ , Infernu.Builtins.String+ , Infernu.Builtins.TypeClasses+ , Infernu.Decycle+ , Infernu.Fix+ , Infernu.Infer+ , Infernu.InferState+ , Infernu.Lib+ , Infernu.Log+ , Infernu.Options+ , Infernu.Parse+ , Infernu.Pretty+ , Infernu.Types+ , Infernu.Unify+ , Infernu.Util+ -- TODO: use only mtl (not transformers)+ build-depends: base >= 4.8 && < 5, mtl, containers, transformers, either, language-ecmascript, digits, parsec, fgl, optparse-applicative+ default-language: Haskell2010+ ghc-options: -Wall -O2 -rtsopts -threaded+ if flag(debug)+ ghc-options: -g+ if flag(trace)+ cpp-options: -DTRACE+ if flag(quickcheck)+ cpp-options: -DQUICKCHECK+ build-depends: QuickCheck, derive+ default-extensions: TemplateHaskell, DeriveGeneric, FlexibleInstances++executable infernu+ main-is: Main.hs+ build-depends: base, parsec, infernu, optparse-applicative+ default-language: Haskell2010+ ghc-options: -Wall -O2 -rtsopts -threaded+ if flag(debug)+ ghc-options: -g+ if flag(trace)+ cpp-options: -DTRACE+ if flag(quickcheck)+ cpp-options: -DQUICKCHECK+ build-depends: QuickCheck, derive+ default-extensions: TemplateHaskell, DeriveGeneric++executable infernu-demo+ main-is: Demo.hs+ hs-source-dirs: test+ build-depends: base, infernu+ default-language: Haskell2010+ ghc-options: -Wall -O2 -main-is Demo+ if flag(trace)+ cpp-options: -DTRACE+ if flag(quickcheck)+ cpp-options: -DQUICKCHECK+ build-depends: QuickCheck, derive+ default-extensions: TemplateHaskell, DeriveGeneric++executable test+ if flag(quickcheck)+ cpp-options: -DQUICKCHECK+ build-depends: QuickCheck, derive+ default-extensions: TemplateHaskell, DeriveGeneric+ else+ buildable: False+ main-is: Test.hs+ hs-source-dirs: test+ build-depends: base, infernu+ default-language: Haskell2010+ ghc-options: -Wall -O2 -main-is Test+ if flag(trace)+ cpp-options: -DTRACE
+ src/Infernu/Builtins/Array.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE TupleSections #-}+module Infernu.Builtins.Array+ (arrayRowType)+ where++import Control.Monad (foldM, forM)+import Infernu.Types+import Infernu.InferState+import Infernu.Lib (safeLookup)++func :: Type -> Type -> Type -> Type+func this x y = Fix $ TFunc [this, x] y++funcN :: [Fix FType] -> Fix FType -> Fix FType+funcN xs tres = Fix $ TFunc xs tres++string :: Type+string = Fix $ TBody TString++number :: Type+number = Fix $ TBody TNumber++undef :: Type+undef = Fix $ TBody TUndefined++array :: Type -> Type+array t = Fix $ TCons TArray [t]++boolean :: Fix FType+boolean = Fix $ TBody TBoolean++ts :: t -> TScheme t+ts t = TScheme [] $ qualEmpty t++tvar :: TVarName -> Type+tvar = Fix . TBody . TVar++arrayProps :: Type -> [(String, TypeScheme)]+arrayProps elemType = let aType = array elemType in+ [ ("length", ts number)+ , ("concat", ts $ func aType aType aType)+ -- TODO support thisArg (requires type variables)+ , ("every", ts $ func aType (funcN [undef, elemType, number, aType] boolean) boolean) -- missing thisArg+ , ("filter", ts $ func aType (funcN [undef, elemType, number, aType] boolean) aType) -- missing thisArg+ -- TODO support optional argument for fromIndex (last parameter)+ , ("indexOf", ts $ funcN [aType, elemType, number] number)+ , ("join", ts $ func aType string string)+ , ("lastIndexOf", ts $ func aType number number)+ , ("map", TScheme [0] $ qualEmpty (func aType (funcN [undef, elemType, number, aType] (tvar 0)) (array $ tvar 0)))-- requires type variables, and maybe foralls on row properties+ , ("pop", ts $ funcN [aType] elemType)+ , ("push", ts $ funcN [aType, elemType] number)+ , ("reverse", ts $ funcN [aType] aType)+ , ("shift", ts $ funcN [aType] elemType)+ , ("slice", ts $ funcN [aType, number, number] aType)+ , ("some", ts $ func aType (funcN [undef, elemType, number, aType] boolean) aType) -- missing thisArg+ , ("sort", ts $ func aType (funcN [undef, elemType, elemType] number) aType)+ , ("splice", ts $ funcN [aType, number, number] aType)+ , ("unshift", ts $ funcN [aType] elemType)+ ]++-- TODO: when inserting builtin types, do fresh renaming of scheme qvars+arrayRowType :: Type -> Infer (TRowList Type)+arrayRowType elemType = foldM addProp (TRowEnd Nothing) $ arrayProps elemType+ where addProp rowlist (name, propTS) =+ do allocNames <- forM (schemeVars propTS) $ \tvName -> (fresh >>= return . (tvName,))+ let ts' = mapVarNames (safeLookup allocNames) propTS+ return $ TRowProp name ts' rowlist
+ src/Infernu/Builtins/Operators.hs view
@@ -0,0 +1,77 @@+module Infernu.Builtins.Operators+ (builtins)+ where++import Infernu.Types+import qualified Data.Map.Lazy as Map+import Data.Map.Lazy (Map)++ts :: [TVarName] -> Type -> TypeScheme+ts tvs t = TScheme tvs (qualEmpty t)+ +unaryFunc :: Type -> Type -> TypeScheme+unaryFunc t1 t2 = ts [0] $ Fix $ TFunc [Fix $ TBody $ TVar 0, t1] t2++binaryFunc :: Type -> Type -> Type -> Type -> Fix FType+binaryFunc tThis t1 t2 t3 = Fix $ TFunc [tThis, t1, t2] t3++binarySimpleFunc :: Type -> Type -> Type+binarySimpleFunc tThis t = Fix $ TFunc [tThis, t, t] t++binaryFuncS :: Type -> Type -> Type -> TypeScheme+binaryFuncS t1 t2 t3 = ts [0] $ binaryFunc (Fix $ TBody $ TVar 0) t1 t2 t3++tVar :: TVarName -> Type+tVar = Fix . TBody . TVar++tBoolean :: Type+tBoolean = Fix $ TBody TBoolean++tNumber :: Type+tNumber = Fix $ TBody TNumber++tString :: Type+tString = Fix $ TBody TString++numRelation :: TypeScheme+numRelation = binaryFuncS tNumber tNumber tBoolean++numOp :: TypeScheme+numOp = binaryFuncS tNumber tNumber tNumber++builtins :: Map EVarName TypeScheme+builtins = Map.fromList [+ ("!", unaryFunc tBoolean tBoolean),+ ("~", unaryFunc tNumber tNumber),+ ("typeof", ts [0,1] $ Fix $ TFunc [Fix $ TBody $ TVar 1, Fix $ TBody $ TVar 0] tString),+ ("+", TScheme [0,1] $ TQual { qualPred = [TPredIsIn (ClassName "Plus") (tVar 1)]+ , qualType = binarySimpleFunc (tVar 0) (tVar 1) }),+ ("-", numOp),+ ("*", numOp),+ ("/", numOp),+ ("%", numOp),+ ("<<", numOp),+ (">>", numOp),+ (">>>", numOp),+ ("&", numOp),+ ("^", numOp),+ ("|", numOp),+ ("<", numRelation),+ ("<=", numRelation),+ (">", numRelation),+ (">=", numRelation),+ ("===", ts [0, 1, 2] $ Fix $ TFunc [Fix $ TBody $ TVar 2, Fix $ TBody $ TVar 0, Fix $ TBody $ TVar 1] tBoolean),+ ("!==", ts [0, 1, 2] $ Fix $ TFunc [Fix $ TBody $ TVar 2, Fix $ TBody $ TVar 0, Fix $ TBody $ TVar 1] tBoolean),+ ("&&", ts [0, 1] $ Fix $ TFunc [tVar 0, tVar 1, tVar 1] (tVar 1)),+ ("||", ts [0, 1] $ Fix $ TFunc [tVar 0, tVar 1, tVar 1] (tVar 1)),+ -- avoid coercions on == and !=+ ("==", ts [0, 1] $ Fix $ TFunc [Fix $ TBody $ TVar 1, Fix $ TBody $ TVar 0, Fix $ TBody $ TVar 0] tBoolean),+ ("!=", ts [0, 1] $ Fix $ TFunc [Fix $ TBody $ TVar 1, Fix $ TBody $ TVar 0, Fix $ TBody $ TVar 0] tBoolean),+ ("RegExp", ts [0] $ Fix $ TFunc [Fix $ TBody $ TVar 0, tString, tString] (Fix $ TBody TRegex)),+ ("String", ts [1] $ Fix $ TFunc [Fix $ TBody $ TUndefined, Fix $ TBody $ TVar 1] (Fix $ TBody TString)),+ ("Number", ts [1] $ Fix $ TFunc [Fix $ TBody $ TUndefined, Fix $ TBody $ TVar 1] (Fix $ TBody TNumber)),+ ("Boolean", ts [1] $ Fix $ TFunc [Fix $ TBody $ TUndefined, Fix $ TBody $ TVar 1] (Fix $ TBody TBoolean)),+ ("NaN", ts [] tNumber),+ ("Infinity", ts [] tNumber),+ ("undefined", ts [] $ Fix $ TBody TUndefined)+ ]
+ src/Infernu/Builtins/Regex.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE TupleSections #-}+module Infernu.Builtins.Regex+ (regexRowType)+ where++import Control.Monad (foldM, forM)+import Infernu.Types+import Infernu.InferState+import Infernu.Lib (safeLookup)++string :: TQual Type+string = qualEmpty $ Fix $ TBody TString++-- regex :: Type+-- regex = Fix $ TBody TRegex++ts :: TQual t -> TScheme t+ts t = TScheme [] t++regexProps :: [(String, TypeScheme)]+regexProps = + [ ("source", ts string)+ ]++-- TODO: when inserting builtin types, do fresh renaming of scheme qvars+regexRowType :: Infer (TRowList Type)+regexRowType = foldM addProp (TRowEnd Nothing) $ regexProps+ where addProp rowlist (name, propTS) =+ do allocNames <- forM (schemeVars propTS) $ \tvName -> (fresh >>= return . (tvName,))+ let ts' = mapVarNames (safeLookup allocNames) propTS+ return $ TRowProp name ts' rowlist
+ src/Infernu/Builtins/String.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE TupleSections #-}+module Infernu.Builtins.String+ (stringRowType)+ where++import Control.Monad (foldM, forM)+import Infernu.Types+import Infernu.InferState+import Infernu.Lib (safeLookup)++func :: Type -> Type -> Type -> Type+func this x y = Fix $ TFunc [this, x] y++string :: Type+string = Fix $ TBody TString++number :: Type+number = Fix $ TBody TNumber+ +ts :: t -> TScheme t+ts t = TScheme [] $ qualEmpty t++stringProps :: [(String, TypeScheme)]+stringProps = + [ ("length", ts number)+ , ("charAt", ts $ func string number string)+ , ("charCodeAt", ts $ func string number number)+ , ("concat", ts $ func string string string) -- TODO: concat really accepts a variable number of arguments+ , ("indexOf", ts $ func string string number) -- TODO: optional parameter+ , ("lastIndexOf", ts $ func string string number) -- TODO: optional parameter+ , ("localeCompare", ts $ func string string number) -- TODO: optional parameters++-- To support 'match' we need to allow different result types, different for global and non-global+-- regexes. One possibility is to define two regex types RegexSingle and RegexGlobal and use+-- associated types:+-- class Regex r where+-- type R r = r+-- type M RegexLocal = -- match result type for RegexLocal+-- type M RegexGlobal = [String]+-- +-- , ("match", ts $ func string regex+ + ]++-- TODO: when inserting builtin types, do fresh renaming of scheme qvars+stringRowType :: Infer (TRowList Type)+stringRowType = foldM addProp (TRowEnd Nothing) $ stringProps+ where addProp rowlist (name, propTS) =+ do allocNames <- forM (schemeVars propTS) $ \tvName -> (fresh >>= return . (tvName,))+ let ts' = mapVarNames (safeLookup allocNames) propTS+ return $ TRowProp name ts' rowlist
+ src/Infernu/Builtins/TypeClasses.hs view
@@ -0,0 +1,32 @@+module Infernu.Builtins.TypeClasses+ (typeClasses)+ where++import Infernu.Types++typeClasses =+ [ (ClassName "Indexable", Class { classInstances =+ [ TScheme { schemeVars = [0]+ , schemeType = qualEmpty+ $ Fix $ TCons TTuple+ [ Fix $ TCons TArray [Fix $ TBody $ TVar 0]+ , Fix $ TBody TNumber+ , Fix $ TBody $ TVar 0 ]+ }+ , TScheme { schemeVars = [1]+ , schemeType = qualEmpty+ $ Fix $ TCons TTuple+ [ Fix $ TCons TStringMap [Fix $ TBody $ TVar 1]+ , Fix $ TBody TString+ , Fix $ TBody $ TVar 1 ]+ }+ , schemeEmpty $ Fix $ TCons TTuple+ [ Fix $ TBody TString+ , Fix $ TBody TNumber+ , Fix $ TBody TString ]+ ]})+ , (ClassName "Plus", Class { classInstances =+ [ schemeEmpty $ Fix $ TBody TNumber+ , schemeEmpty $ Fix $ TBody TString+ ]})+ ]
+ src/Infernu/Decycle.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE ScopedTypeVariables #-}++-- | copied from https://raw.githubusercontent.com/Peaker/lamdu/wip_integration/bottlelib/Data/Function/Decycle.hs++module Infernu.Decycle(decycleOn, decycle, decycle2, decycle3) where++import qualified Data.Set as Set++-- | A fix for functions that terminates recursive cycles+decycleOn :: forall a b res . Ord b => (a -> b) -> (Maybe (a -> res) -> a -> res) -> a -> res+decycleOn toOrd f = go Set.empty+ where+ go :: Set.Set b -> a -> res+ go visited x = f (mRecurse visited (toOrd x)) x+ + mRecurse :: Set.Set b -> b -> Maybe (a -> res)+ mRecurse visited o = if Set.member o visited+ then Nothing+ else Just $ go (Set.insert o visited)++decycle :: Ord a => (Maybe (a -> res) -> a -> res) -> a -> res+decycle = decycleOn id++decycle2 :: (Ord b, Ord a) => (Maybe (a -> b -> c) -> a -> b -> c) -> a -> b -> c+decycle2 f arg1 arg2 = decycle (\recurse (arg1', arg2') -> f (curry <$> recurse) arg1' arg2') (arg1, arg2)++decycle3 :: (Ord b, Ord a, Ord c) => (Maybe (a -> b -> c -> res) -> a -> b -> c -> res) -> a -> b -> c -> res+decycle3 f arg1 arg2 arg3 = decycle f3 (arg1, arg2, arg3)+ where f3 Nothing (x,y,z) = f Nothing x y z+ f3 (Just rec3) (x,y,z) = f (Just (\a b c -> rec3 (a,b,c))) x y z
+ src/Infernu/Fix.hs view
@@ -0,0 +1,41 @@+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+module Infernu.Fix+ ( Fix(..)+ , fmapReplace+ , replaceFix+ , fixToList+ )+ where++import Data.Foldable (Foldable (..), foldr)+import Prelude hiding (foldr)+++newtype Fix f = Fix { unFix :: f (Fix f) }++instance Show (f (Fix f)) => Show (Fix f) where+ show (Fix x) = "Fix (" ++ (show x) ++ ")"+instance Eq (f (Fix f)) => Eq (Fix f) where+ a == b = unFix a == unFix b+instance Ord (f (Fix f)) => Ord (Fix f) where+ (Fix x) `compare` (Fix y) = x `compare` y++fmapReplace :: (Functor f, Eq (f a)) => (f a -> f b -> a -> b) -> f a -> f b -> f a -> f b+fmapReplace recurse tsource tdest t =+ if t == tsource+ then tdest+ else fmap (recurse tsource tdest) t++replaceFix :: (Functor f, Eq (f (Fix f))) => f (Fix f) -> f (Fix f) -> Fix f -> Fix f+replaceFix tsource tdest (Fix t') = Fix $ fmapReplace replaceFix tsource tdest t'+++-- | Flattens a fix-type to a list of all tree nodes+--+-- >>> fixToList $ (Fix $ TCons TArray [Fix $ TCons TArray [Fix $ TBody TNumber]])+-- [Fix (TCons TArray [Fix (TCons TArray [Fix (TBody TNumber)])]),Fix (TCons TArray [Fix (TBody TNumber)]),Fix (TBody TNumber)]+-- >>> fixToList $ (Fix $ TRow $ TRowProp "x" (TScheme [] $ Fix $ TBody TNumber) (TRowEnd Nothing))+-- [Fix (TRow (TRowProp "x" (TScheme {schemeVars = [], schemeType = Fix (TBody TNumber)}) (TRowEnd Nothing))),Fix (TBody TNumber)]+fixToList :: Foldable t => Fix t -> [Fix t]+fixToList (Fix t) = (Fix t) : (foldr (\t' b -> fixToList t' ++ b) [] t)
+ src/Infernu/Infer.hs view
@@ -0,0 +1,448 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}++module Infernu.Infer+ ( runTypeInference+ , test+ , Pretty(..)+ , pretty+ , getAnnotations+ , minifyVars+ , TypeError+ )+ where+++import Control.Monad (foldM, forM)+import Data.Foldable (Foldable (..))+import Data.Traversable (mapM)+import qualified Data.Graph.Inductive as Graph+import Data.Map.Lazy (Map)+import qualified Data.Map.Lazy as Map+import Data.Maybe (mapMaybe)+import Data.Set (Set)+import qualified Data.Set as Set+import Prelude hiding (foldr, mapM, sequence)++import Data.List (intercalate)++import qualified Infernu.Builtins.Operators as Operators+import Infernu.InferState+import Infernu.Lib (safeLookup)+import Infernu.Log+import Infernu.Pretty+import Infernu.Types+import Infernu.Unify (unify, unifyAll, unifyPending, unifyPredsL, unifyRowPropertyBiased, unifyl)++++getQuantificands :: TypeScheme -> [TVarName]+getQuantificands (TScheme tvars _) = tvars++getAnnotations :: Exp a -> [a]+getAnnotations = foldr (:) []++----------------------------------------------------------------------++closeRowList :: TRowList Type -> TRowList Type+closeRowList (TRowProp n t rest) = TRowProp n t (closeRowList rest)+closeRowList (TRowEnd _) = TRowEnd Nothing+-- TODO: Handle TRowRec, by defining a new named type in which all row types within are closed (recursively).++-- | Replaces a top-level open row type with the closed equivalent.+-- >>> pretty $ closeRow (Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2)))+-- "{a: {aa: Number, ..b}}"+-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "aa" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd Nothing)) (TRowEnd Nothing)] (Fix $ TBody TString))+-- "{a: {aa: Number}}.(() -> String)"+-- >>> pretty $ closeRow (Fix $ TFunc [Fix $ TRow $ TRowProp "a" (schemeEmpty $ Fix $ TRow $ TRowProp "a.a" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd (Just $ RowTVar 1))) (TRowEnd (Just $ RowTVar 2))] (Fix $ TBody TString))+-- "{a: {a.a: Number, ..b}, ..c}.(() -> String)"+closeRow :: Type -> Type+closeRow (Fix (TRow r)) = Fix . TRow $ closeRowList r+closeRow t = t++----------------------------------------------------------------------+++-- For efficiency reasons, types list is returned in reverse order.+accumInfer :: TypeEnv -> [Exp Source] -> Infer [(QualType, Exp (Source, QualType))]+accumInfer env =+ do traceLog ("accumInfer: env: " ++ pretty env)+ foldM accumInfer' []+ where accumInfer' types expr =+ do (t, e) <- inferType env expr+ return ((t,e):types)++inferType :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))+inferType env expr = do+ traceLog (">> " ++ pretty expr ++ " -- env: " ++ pretty env)+ (t, e) <- inferType' env expr+ unifyPending+ s <- getMainSubst+ st <- getState+ traceLog (">> " ++ pretty expr ++ " -- inferred :: " ++ pretty (applySubst s t))+ traceLog (" infer state: " ++ prettyTab 3 st)+ return (applySubst s t, fmap (applySubst s) e)++inferType' :: TypeEnv -> Exp Source -> Infer (QualType, Exp (Source, QualType))+inferType' _ (ELit a lit) = do+ let t = Fix $ TBody $ case lit of+ LitNumber _ -> TNumber+ LitBoolean _ -> TBoolean+ LitString _ -> TString+ LitRegex{} -> TRegex+ LitUndefined -> TUndefined+ LitNull -> TNull+ return (qualEmpty t, ELit (a, qualEmpty t) lit)+inferType' env (EVar a n) =+ do t <- instantiateVar a n env+ return (t, EVar (a, t) n)+inferType' env (EAbs a argNames e2) =+ do argTypes <- forM argNames (const $ Fix . TBody . TVar <$> fresh)+ env' <- foldM (\e (n, t) -> addVarScheme e n $ schemeEmpty t) env $ zip argNames argTypes+ (t1, e2') <- inferType env' e2+ pred' <- unifyPredsL a $ qualPred t1+ let t = TQual pred' $ Fix $ TFunc argTypes (qualType t1)+ return (t, EAbs (a, t) argNames e2')+inferType' env (EApp a e1 eArgs) =+ do tvar <- Fix . TBody . TVar <$> fresh+ (t1, e1') <- inferType env e1+ traceLog $ "EApp: Inferred type for func expr: " ++ pretty t1+ argsTE <- accumInfer env eArgs+ traceLog $ "EApp: Inferred types for func args: " ++ intercalate ", " (map pretty argsTE)+ let rargsTE = reverse argsTE+ tArgs = map fst rargsTE+ eArgs' = map snd rargsTE+ preds = concatMap qualPred $ t1:tArgs+ unify a (qualType t1) (Fix $ TFunc (map qualType tArgs) tvar)+ traceLog $ "Inferred preds: " ++ intercalate ", " (map pretty preds)+ tvar' <- do pred' <- unifyPredsL a preds+ tvarSubsted <- applyMainSubst tvar+ return $ TQual pred' tvarSubsted+ traceLog ("Inferred func application: " ++ pretty tvar')+ return (tvar', EApp (a, tvar') e1' eArgs')+inferType' env (ENew a e1 eArgs) =+ do (t1, e1') <- inferType env e1+ argsTE <- accumInfer env eArgs+ thisT <- Fix . TBody . TVar <$> fresh+ resT <- Fix . TBody . TVar <$> fresh+ let rargsTE = reverse argsTE+ tArgs = thisT : map (qualType . fst) rargsTE+ eArgs' = map snd rargsTE+ preds = concatMap qualPred $ t1 : map fst argsTE+ unify a (qualType t1) (Fix $ TFunc tArgs resT)+ -- constrain 'this' to be a row type:+ rowConstraintVar <- RowTVar <$> fresh+ unify a (Fix . TRow . TRowEnd $ Just rowConstraintVar) thisT+ -- close the row type+ resolvedThisT <- applyMainSubst thisT -- otherwise closeRow will not do what we want.+ unify a thisT (closeRow resolvedThisT)+ -- TODO: If the function returns a row type, it should be the resulting type; other it should be 'thisT'+ preds' <- unifyPredsL a preds+ let thisT' = TQual preds' thisT+ return (thisT', ENew (a, thisT') e1' eArgs')+inferType' env (ELet a n e1 e2) =+ do recType <- Fix . TBody . TVar <$> fresh+ recEnv <- addVarScheme env n $ schemeEmpty recType+ (t1, e1') <- inferType recEnv e1+ unify a (qualType t1) recType+ t' <- generalize e1 env t1+ env' <- addVarScheme env n t'+ (t2, e2') <- inferType env' e2+ preds' <- unifyPredsL a $ concatMap qualPred [t1, t2]+ let resT = TQual preds' $ qualType t2+ return (resT, ELet (a, resT) n e1' e2')+-- | Handling of mutable variable assignment.+-- | Prevent mutable variables from being polymorphic.+inferType' env expr@(EAssign a n expr1 expr2) =+ do traceLog $ "EAssign: " ++ pretty expr+ lvalueScheme <- getVarScheme a n env `failWithM` throwError a ("Unbound variable: " ++ show n ++ " in assignment " ++ pretty expr1)+ traceLog $ "EAssign lvalueScheme: " ++ pretty lvalueScheme+ lvalueT <- instantiate lvalueScheme+ (rvalueT, expr1') <- inferType env expr1+ unify a (qualType lvalueT) (qualType rvalueT)+ (tRest, expr2') <- inferType env expr2+ traceLog $ "EAssign lvalueT: " ++ pretty lvalueT+ traceLog $ "EAssign Invoking unifyAllInstances on scheme: " ++ pretty lvalueScheme+ instancePreds <- unifyAllInstances a $ getQuantificands lvalueScheme+ preds <- unifyPredsL a $ concat $ (instancePreds:) $ map qualPred [lvalueT, rvalueT, tRest] -- TODO should update variable scheme+ -- update the variable scheme, removing perhaps some quantified tvars+ varId <- getVarId n env `failWith` throwError a ("Unbound variable: '" ++ show n ++ "'")+ updatedScheme <- generalize expr1 env (schemeType lvalueScheme)+ _ <- setVarScheme env n updatedScheme varId+ --+ let tRest' = TQual preds $ qualType tRest+ return (tRest', EAssign (a, tRest') n expr1' expr2')+inferType' env (EPropAssign a objExpr n expr1 expr2) =+ do (objT, objExpr') <- inferType env objExpr+ (rvalueT, expr1') <- inferType env expr1+ rowTailVar <- RowTVar <$> fresh+ let rvalueScheme = schemeFromQual rvalueT -- generalize expr1 env rvalueT+ rank0Unify = unify a (qualType objT) $ Fix . TRow $ TRowProp n rvalueScheme $ TRowEnd (Just rowTailVar)+ case unFix (qualType objT) of+ TRow trowList ->+ case Map.lookup n . fst $ flattenRow trowList of+ -- lvalue is known to be a property with some scheme+ Just lvalueScheme ->+ do generalizedRvalue <- generalize expr1 env rvalueT+ unifyRowPropertyBiased a rank0Unify (lvalueScheme, generalizedRvalue)+ Nothing -> rank0Unify+ _ -> rank0Unify+ (expr2T, expr2') <- inferType env expr2 -- TODO what about the pred+ --traceLog "EPropAssign - applying unifyAllInstances"+ --instancePred <- unifyAllInstances a [getRowTVar rowTailVar]+ preds <- unifyPredsL a $ concatMap qualPred [objT, rvalueT, expr2T] -- TODO review+ let tRes = TQual preds $ qualType expr2T+ return (tRes, EPropAssign (a, tRes) objExpr' n expr1' expr2')+inferType' env (EIndexAssign a eArr eIdx expr1 expr2) =+ do (tArr, eArr') <- inferType env eArr+ elemTVarName <- fresh+ arrTVarName <- fresh+ idxTVarName <- fresh+ let elemType = Fix . TBody . TVar $ elemTVarName+-- unify a (qualType tArr) $ Fix $ TCons TArray [elemType]+ unify a (qualType tArr) $ Fix $ TBody $ TVar arrTVarName+ (tId, eIdx') <- inferType env eIdx+ unify a (qualType tId) $ Fix $ TBody $ TVar idxTVarName+ (tExpr1, expr1') <- inferType env expr1+ unify a (qualType tExpr1) elemType+ -- TODO: BUG here, because elemTVarName never has any var instances due to the predicates usage here.+ --traceLog "EIndexAssign - applying unifyAllInstances"+ --instancePred <- unifyAllInstances a [elemTVarName]+ (tExpr2, expr2') <- inferType env expr2+ let curPred = indexAccessPred arrTVarName elemTVarName idxTVarName+ preds <- unifyPredsL a $ concat $ ([curPred]:) $ map qualPred [tArr, tId, tExpr1, tExpr2] -- TODO review+ let tRes = TQual preds $ qualType tExpr2+ return (tRes , EIndexAssign (a, tRes) eArr' eIdx' expr1' expr2')+inferType' env (EArray a exprs) =+ do tv <- Fix . TBody . TVar <$> fresh+ te <- accumInfer env exprs+ let types = map (qualType . fst) te+ unifyl unify a $ zip (tv:types) types+ let t = qualEmpty $ Fix $ TCons TArray [tv]+ return (t, EArray (a,t) $ map snd te)+inferType' env (ETuple a exprs) =+ do te <- accumInfer env exprs+ let t = TQual (concatMap (qualPred . fst) te) $ Fix . TCons TTuple . reverse $ map (qualType . fst) te+ return (t, ETuple (a,t) $ map snd te)+inferType' env (EStringMap a exprs') =+ do let exprs = map snd exprs'+ elemType <- Fix . TBody . TVar <$> fresh+ te <- accumInfer env exprs+ let types = map (qualType . fst) te+ unifyAll a $ elemType:types+ allPreds <- unifyPredsL a . concatMap qualPred $ map fst te+ let t = TQual { qualPred = allPreds, qualType = Fix $ TCons TStringMap [elemType] }+ return (t, EStringMap (a,t) $ zip (map fst exprs') (map snd te))+inferType' env (ERow a isOpen propExprs) =+ do te <- accumInfer env $ map snd propExprs+ endVar <- RowTVar <$> fresh+ let propNamesTypes = zip propExprs (reverse $ map fst te)+ rowEnd' = TRowEnd $ if isOpen then Just endVar else Nothing+ accumRowProp' row ((propName, propExpr), propType) =+ do ts <- generalize propExpr env propType+ return $ TRowProp propName ts row+ rowType <- qualEmpty . Fix . TRow <$> foldM accumRowProp' rowEnd' propNamesTypes+ return (rowType, ERow (a,rowType) isOpen $ zip (map fst propExprs) (map snd te))+inferType' env (ECase a eTest eBranches) =+ do (eType, eTest') <- inferType env eTest+ infPatterns <- accumInfer env $ map (ELit a . fst) eBranches+ let patternTypes = map (qualType . fst) infPatterns+ unifyAll a $ (qualType eType):patternTypes+ infBranches <- accumInfer env $ map snd eBranches+ let branchTypes = map (qualType . fst) infBranches+ unifyAll a branchTypes+ allPreds <- unifyPredsL a . concatMap qualPred $ eType : (map fst infPatterns) ++ (map fst infBranches)+ let tRes = TQual { qualPred = allPreds, qualType = qualType . fst $ head infBranches } -- TODO unsafe head+ return (tRes, ECase (a, tRes) eTest' $ zip (map fst eBranches) (map snd infBranches))+inferType' env (EProp a eObj propName) =+ do (tObj, eObj') <- inferType env eObj+ rowVar <- RowTVar <$> fresh+ propTypeScheme <- schemeEmpty . Fix . TBody . TVar <$> fresh+ --case unFix (qualType tObj) of+-- TRow tRowList -> --TODO+-- _ -> schemeEmpty . Fix . TBody . TVar <$> fresh+ unify a (Fix . TRow $ TRowProp propName propTypeScheme $ TRowEnd (Just rowVar)) (qualType tObj)+ propType <- instantiate propTypeScheme+ return (propType, EProp (a,propType) eObj' propName)+inferType' env (EIndex a eArr eIdx) =+ do (tArr, eArr') <- inferType env eArr+ elemTVarName <- fresh+ arrTVarName <- fresh+ idxTVarName <- fresh+ unify a (qualType tArr) (Fix $ TBody $ TVar arrTVarName)+ (tId, eIdx') <- inferType env eIdx+ unify a (qualType tId) (Fix $ TBody $ TVar idxTVarName)+ let elemType' = qualEmpty $ Fix $ TBody $ TVar elemTVarName+ curPred = indexAccessPred arrTVarName elemTVarName idxTVarName+ preds <- unifyPredsL a $ (curPred:) $ concatMap qualPred [tArr, tId] -- TODO review+ let tRes = TQual preds $ qualType elemType'+ return (tRes, EIndex (a, tRes) eArr' eIdx')++indexAccessPred :: TVarName -> TVarName -> TVarName -> TPred Type+indexAccessPred arrTVarName elemTVarName idxTVarName =+ let --elemType = mkv elemTVarName+ mkv = Fix . TBody . TVar+ in+ TPredIsIn (ClassName "Indexable") (Fix $ TCons TTuple+ [ mkv arrTVarName+ , mkv idxTVarName+ , mkv elemTVarName+ ])+ -- Fix $ TCons TArray [elemType])+ -- , TPredIsIn "Index"+ -- `mkAnd` TPredEq idxTVarName (Fix $ TBody TNumber))+ -- `mkOr` (TPredEq arrTVarName (Fix $ TCons TStringMap [elemType])+ -- `mkAnd` TPredEq idxTVarName (Fix $ TBody TString))++unifyAllInstances :: Source -> [TVarName] -> Infer [TPred Type]+unifyAllInstances a tvs = do+ m <- getVarInstances+ + traceLog $ "unifyAllInstances: " ++ pretty a ++ " Unifying all instances of tvars: " ++ intercalate ", " (map pretty tvs)+ let equivalenceSets = map Set.fromList $ filter (not . null) $ map (mapMaybe $ Graph.lab m) $ map (flip Graph.bfs m) tvs+ unifyAll' equivs =+ do let equivsL = Set.toList equivs+ qequivsL = map qualType equivsL+ traceLog $ "unifyAllInstances - equivalence:" ++ pretty qequivsL+ unifyAll a qequivsL+ return $ concatMap qualPred equivsL+ pred' <- concat <$> mapM unifyAll' equivalenceSets+ unifyPredsL a pred'++createEnv :: Map EVarName TypeScheme -> Infer (Map EVarName VarId)+createEnv builtins = foldM addVarScheme' Map.empty $ Map.toList builtins+ where allTVars :: TypeScheme -> Set TVarName+ allTVars (TScheme qvars t) = freeTypeVars t `Set.union` Set.fromList qvars++ addVarScheme' :: Map EVarName VarId -> (EVarName, TypeScheme) -> Infer (Map EVarName VarId)+ addVarScheme' m (name, tscheme) =+ do allocNames <- forM (Set.toList $ allTVars tscheme)+ $ \tvName -> (tvName,) <$> fresh+ addVarScheme m name $ mapVarNames (safeLookup allocNames) tscheme+++typeInference :: Map EVarName TypeScheme -> Exp Source -> Infer (Exp (Source, QualType))+typeInference builtins e =+ do env <- createEnv builtins+ (_t, e') <- inferType env e+ return e'++----------------------------------------------------------------------+--+-- | Mutable variable being assigned incompatible types:+--+-- >>> let p = emptySource+-- >>> let fun args = EAbs p ("this":args)+-- >>> let var = EVar p+-- >>> let let' = ELet p+-- >>> let tuple = ETuple p+-- >>> let lit = ELit p+-- >>> let app a b = EApp p a [lit LitUndefined, b]+-- >>> let assign = EAssign p+-- >>> let array = EArray p+--+-- x is known to have type forall a. a -> a, and to have been used in a context requiring bool -> bool (e.g. `x True`)+--+-- we now try to assign x := \y -> 2+--+-- This should fail because it "collapses" x to be Number -> Number which is not compatible with bool -> bool+--+-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["y"] (lit (LitNumber 0))) (tuple [var "x", var "y"])))+-- ":1:1*: Error: Could not unify: Number with Boolean"+--+-- The following should succeed because x is immutable and thus polymorphic:+--+-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (tuple [var "x", var "y"]))+-- "(c.(d -> d), (Number, Boolean))"+--+-- The following should fail because x is mutable and therefore a monotype:+--+-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))]) (assign "x" (fun ["z1"] (var "z1")) (tuple [var "x", var "y"])))+-- ":1:1*: Error: Could not unify: Number with Boolean"+--+-- The following should also succeed because "x" is only ever used like this: (x True). The second assignment to x is: x := \z1 -> False, which is specific but matches the usage. Note that x's type is collapsed to: Boolean -> Boolean.+--+-- >>> test $ let' "x" (fun ["z"] (var "z")) (let' "y" (app (var "x") (lit (LitBoolean True))) (assign "x" (fun ["z1"] (lit (LitBoolean False))) (tuple [var "x", var "y"])))+-- "((Boolean -> Boolean), Boolean)"+--+-- | Tests a setter for x being called with something more specific than x's original definition:+-- >>> :{+-- >>> test $ let'+-- >>> "x" (fun ["a"] (var "a"))+-- >>> (let' "setX"+-- >>> (fun ["v"]+-- >>> (let'+-- >>> "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean False))))+-- >>> (let'+-- >>> "_" (app (var "setX") (fun ["a"] (lit (LitString "a"))))+-- >>> (app (var "x") (lit (LitBoolean True)))))+-- >>> :}+-- ":1:1*: Error: Could not unify: String with Boolean"+--+-- >>> test $ tuple [lit (LitBoolean True), lit (LitNumber 2)]+-- "(Boolean, Number)"+--+-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (fun ["y"] (var "y")) (var "id"))+-- "a.(b -> b)"+--+-- >>> test $ let' "id" (fun ["x"] (var "x")) (assign "id" (lit (LitBoolean True)) (var "id"))+-- ":1:1*: Error: Could not unify: a.(b -> b) with Boolean"+--+-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitBoolean False)) (var "x"))+-- "Boolean"+--+-- >>> test $ let' "x" (lit (LitBoolean True)) (assign "x" (lit (LitNumber 3)) (var "x"))+-- ":1:1*: Error: Could not unify: Boolean with Number"+--+-- >>> test $ let' "x" (array [lit (LitBoolean True)]) (var "x")+-- "[Boolean]"+--+-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitBoolean False]) (var "x")+-- "[Boolean]"+--+-- >>> test $ let' "x" (array []) (assign "x" (array []) (var "x"))+-- "[a]"+--+-- >>> test $ let' "x" (array [lit $ LitBoolean True, lit $ LitNumber 2]) (var "x")+-- ":1:1*: Error: Could not unify: Number with Boolean"+--+-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (var "id") (var "id"))+-- "c.(d -> d)"+--+-- >>> test $ let' "id" (fun ["x"] (let' "y" (var "x") (var "y"))) (app (app (var "id") (var "id")) (lit (LitNumber 2)))+-- "Number"+--+-- >>> test $ let' "id" (fun ["x"] (app (var "x") (var "x"))) (var "id")+-- ":1:1*: Error: Occurs check failed: a in (a -> b)"+--+-- >>> test $ fun ["m"] (let' "y" (var "m") (let' "x" (app (var "y") (lit (LitBoolean True))) (var "x")))+-- "a.((Boolean -> b) -> b)"+--+-- >>> test $ app (lit (LitNumber 2)) (lit (LitNumber 2))+-- ":1:1*: Error: Could not unify: Number with (Number -> a)"+--+-- EAssign tests+-- >>> test $ let' "x" (fun ["y"] (lit (LitNumber 0))) (assign "x" (fun ["y"] (var "y")) (var "x"))+-- "a.(Number -> Number)"+--+-- >>> test $ let' "x" (fun ["y"] (var "y")) (assign "x" (fun ["y"] (lit (LitNumber 0))) (var "x"))+-- "a.(Number -> Number)"+--+-- >>> test $ let' "x" (fun ["y"] (var "y")) (tuple [app (var "x") (lit (LitNumber 2)), app (var "x") (lit (LitBoolean True))])+-- "(Number, Boolean)"+--+-- >>> test $ let' "x" (fun ["y"] (var "y")) (app (var "x") (var "x"))+-- "c.(d -> d)"+--+-- >>> test $ let' "x" (fun ["a"] (var "a")) (let' "getX" (fun ["v"] (var "x")) (let' "setX" (fun ["v"] (let' "_" (assign "x" (var "v") (var "x")) (lit (LitBoolean True)))) (let' "_" (app (var "setX") (fun ["a"] (lit (LitString "a")))) (var "getX"))))+-- "e.(f -> d.(String -> String))"+test :: Exp Source -> String+test e = case runTypeInference e of+ Left err -> pretty err+ Right expr -> pretty $ snd . head . getAnnotations . minifyVars $ expr+++runTypeInference :: Exp Source -> Either TypeError (Exp (Source, QualType))+runTypeInference e = runInfer $ typeInference Operators.builtins e+
+ src/Infernu/InferState.hs view
@@ -0,0 +1,425 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE BangPatterns #-}++module Infernu.InferState+ where++import Control.Monad (foldM, forM, forM_, liftM2, when)+import Control.Monad.Trans (lift)+import Control.Monad.Trans.Either (EitherT (..), left, runEitherT, bimapEitherT)+import Control.Monad.Trans.State (StateT (..), evalStateT, get, put, modify, mapStateT)+import Data.Foldable (Foldable (..), msum)+import Data.Traversable (Traversable (..))+import qualified Data.Graph.Inductive as Graph+ +import Data.Functor.Identity (Identity (..), runIdentity)+import qualified Data.Map.Lazy as Map+-- import Data.Map.Lazy (Map)+import Data.Maybe (fromMaybe)+import qualified Data.Set as Set+import Data.Set (Set)+import Prelude hiding (foldr, sequence, mapM)++++import Infernu.Pretty+import Infernu.Types+import Infernu.Log+import qualified Infernu.Builtins.TypeClasses+ +-- | Inference monad. Used as a stateful context for generating fresh type variable names.+type Infer a = StateT InferState (EitherT TypeError Identity) a++emptyInferState :: InferState+emptyInferState = InferState { nameSource = NameSource 2+ , mainSubst = nullSubst+ , varSchemes = Map.empty+ , varInstances = Graph.empty+ , namedTypes = Map.empty+ , pendingUni = Set.empty+ , classes = Map.fromList Infernu.Builtins.TypeClasses.typeClasses+ }++runInferWith :: InferState -> Infer a -> Either TypeError a+runInferWith ns inf = runIdentity . runEitherT $ evalStateT inf ns+ -- where inf' = do res <- inf+ -- unis <- getPendingUnifications+ -- forM unis $ \((a, scheme), t) ->+ -- do inst <- instantiate scheme -- >>= assertNoPred+ -- unify a inst t++runSubInfer :: Infer a -> Infer (Either TypeError a)+runSubInfer a = do+ s <- get+ return $ runInferWith s a++getState :: Infer InferState+getState = get++setState :: InferState -> Infer ()+setState = put+ +runInfer :: Infer a -> Either TypeError a+runInfer = runInferWith emptyInferState++fresh :: Infer TVarName+fresh = do+ modify $ \is -> is { nameSource = (nameSource is) { lastName = lastName (nameSource is) + 1 } }+ lastName . nameSource <$> get++freshVarId :: Infer VarId+freshVarId = VarId <$> fresh++throwError :: Source -> String -> Infer a+throwError p s = lift . left $ TypeError p s++failWith :: Maybe a -> Infer a -> Infer a+failWith action err = case action of+ Nothing -> err+ Just x -> return x++failWithM :: Infer (Maybe a) -> Infer a -> Infer a+failWithM action err = do+ result <- action+ failWith result err++mapError :: (TypeError -> TypeError) -> Infer a -> Infer a+mapError f ma = mapStateT (bimapEitherT f id) ma+ +getVarSchemeByVarId :: VarId -> Infer (Maybe TypeScheme)+getVarSchemeByVarId varId = Map.lookup varId . varSchemes <$> get++getVarId :: EVarName -> TypeEnv -> Maybe VarId+getVarId = Map.lookup++getVarScheme :: Source -> EVarName -> TypeEnv -> Infer (Maybe TypeScheme)+getVarScheme a n env = case getVarId n env of+ Nothing -> throwError a $ "Unbound variable: '" ++ show n ++ "'"+ Just varId -> getVarSchemeByVarId varId++setVarScheme :: TypeEnv -> EVarName -> TypeScheme -> VarId -> Infer TypeEnv+setVarScheme env n scheme varId = do+ modify $ \is -> is { varSchemes = trace ("Inserting scheme for " ++ pretty n ++ ": " ++ pretty scheme) . Map.insert varId scheme $ varSchemes is }+ return $ Map.insert n varId env++addVarScheme :: TypeEnv -> EVarName -> TypeScheme -> Infer TypeEnv+addVarScheme env n scheme = do+ varId <- tracePretty ("-- '" ++ pretty n ++ "' = varId") <$> freshVarId+ setVarScheme env n scheme varId++--addPendingUnification :: (Source, Type, (ClasSet TypeScheme) -> Infer ()+addPendingUnification :: (Source, Type, (ClassName, Set TypeScheme)) -> Infer ()+addPendingUnification ts = do+ modify $ \is -> is { pendingUni = Set.insert ts $ pendingUni is }+ return ()++getPendingUnifications :: Infer (Set (Source, Type, (ClassName, Set TypeScheme)))+getPendingUnifications = pendingUni <$> get++setPendingUnifications :: (Set (Source, Type, (ClassName, Set TypeScheme))) -> Infer ()+setPendingUnifications ts = do+ modify $ \is -> is { pendingUni = ts }+ return ()+ +----------------------------------------------------------------------+++addVarInstance :: TVarName -> TVarName -> Infer ()+addVarInstance x y = modify $ \is -> is { varInstances = tracePretty "updated equivs" $ addEquivalence x y (varInstances is) }++getFreeTVars :: TypeEnv -> Infer (Set TVarName)+getFreeTVars env = do+ let collectFreeTVs s varId = Set.union s <$> curFreeTVs+ where curFreeTVs = tr . maybe Set.empty freeTypeVars <$> getVarSchemeByVarId varId+ tr = tracePretty $ " collected from " ++ pretty varId ++ " free type variables: "+ foldM collectFreeTVs Set.empty (Map.elems env)++addNamedType :: TypeId -> Type -> TypeScheme -> Infer ()+addNamedType tid t scheme = do+ traceLog ("===> Introducing named type: " ++ pretty tid ++ " => " ++ pretty scheme)+ modify $ \is -> is { namedTypes = Map.insert tid (t, scheme) $ namedTypes is }+ return ()++-- | Compares schemes up to alpha equivalence including named type constructors equivalence (TCons+-- TName...).+-- +-- >>> let mkNamedType tid ts = Fix $ TCons (TName (TypeId tid)) ts+-- +-- >>> areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (Fix $ TBody TNumber)) (mkNamedType 1 [], schemeEmpty (Fix $ TBody TString))+-- False+-- >>> areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (mkNamedType 0 [])) (mkNamedType 1 [], schemeEmpty (mkNamedType 1 []))+-- True+-- >>> :{+-- areEquivalentNamedTypes (mkNamedType 0 [], schemeEmpty (Fix $ TFunc [Fix $ TBody TNumber] (mkNamedType 0 [])))+-- (mkNamedType 1 [], schemeEmpty (Fix $ TFunc [Fix $ TBody TNumber] (mkNamedType 1 [])))+-- :}+-- True+-- +-- >>> :{+-- areEquivalentNamedTypes (mkNamedType 0 [Fix $ TBody $ TVar 10], TScheme [10] (qualEmpty $ Fix $ TFunc [Fix $ TBody $ TVar 10] (mkNamedType 0 [Fix $ TBody $ TVar 10])))+-- (mkNamedType 1 [Fix $ TBody $ TVar 11], TScheme [11] (qualEmpty $ Fix $ TFunc [Fix $ TBody $ TVar 11] (mkNamedType 1 [Fix $ TBody $ TVar 11])))+-- :}+-- True+areEquivalentNamedTypes :: (Type, TypeScheme) -> (Type, TypeScheme) -> Bool+areEquivalentNamedTypes (t1, s1) (t2, s2) = s2 == (s2 { schemeType = applySubst subst $ replaceFixQual (unFix t1) (unFix t2) $ schemeType s1 })+ where subst = foldr (\(x,y) s -> singletonSubst x (Fix $ TBody $ TVar y) `composeSubst` s) nullSubst $ zip (schemeVars s1) (schemeVars s2)++-- | Returns a TQual with the `src` type replaced everywhere with the `dest` type.+replaceFixQual :: (Functor f, Eq (f (Fix f))) => f (Fix f) -> f (Fix f) -> TQual (Fix f) -> TQual (Fix f)+replaceFixQual src dest (TQual preds t) = TQual (map (replacePredType' $ replaceFix src dest) preds) (replaceFix src dest t)+ where replacePredType' f p = p { predType = f $ predType p } -- TODO needs some lens goodness+ +-- Checks if a given type variable appears in the given type *only* as a parameter to a recursive+-- type name. If yes, returns the name of recursive types (and position within) in which it+-- appears; otherwise returns Nothing.+--isRecParamOnly :: TVarName -> Maybe (TypeId, Int) -> Type -> Maybe [(TypeId, Int)]+isRecParamOnly+ :: (Num t, Enum t) =>+ TVarName -> Maybe (TypeId, t) -> Type -> Maybe [(TypeId, t)]+isRecParamOnly n1 typeId t1 =+ case unFix t1 of+ TBody (TVar n1') -> if n1' == n1 then sequence [typeId] else Just []+ TBody _ -> Just []+ TCons (TName typeId') subTs -> recurseIntoNamedType typeId' subTs+ TCons _ subTs -> msum $ map (isRecParamOnly n1 Nothing) subTs+ TFunc ts tres -> (isRecParamOnly n1 Nothing) tres `mappend` msum (map (isRecParamOnly n1 Nothing) ts)+ TRow rlist -> isRecParamRecList n1 rlist+ where isRecParamRecList n' rlist' =+ case rlist' of+ TRowEnd _ -> Just []+ -- TODO: assumes the quanitified vars in TScheme do not shadow other type variable names+ -- TODO: Can we safely ignore preds here?+ TRowProp _ (TScheme _ t') rlist'' -> liftM2 (++) (isRecParamOnly n1 Nothing $ qualType t') (isRecParamRecList n' rlist'')+ TRowRec typeId' subTs -> recurseIntoNamedType typeId' subTs+ where recurseIntoNamedType typeId' subTs = msum $ map (\(t,i) -> isRecParamOnly n1 (Just (typeId', i)) t) $ zip subTs [0..]++dropAt :: Integral a => a -> [b] -> [b]+dropAt _ [] = []+dropAt 0 (_:xs) = xs+dropAt n (_:xs) = dropAt (n-1) xs++replaceRecType :: TypeId -> TypeId -> Int -> Type -> Type+replaceRecType typeId newTypeId indexToDrop t1 =+ let replace' = replaceRecType typeId newTypeId indexToDrop+ mapTs' = map replace'+ in case unFix t1 of+ TBody _ -> t1+ TCons (TName typeId') subTs -> if typeId == typeId'+ then Fix $ TCons (TName newTypeId) $ dropAt indexToDrop subTs+ else t1+ TCons n subTs -> Fix $ TCons n $ mapTs' subTs+ TFunc ts tres -> Fix $ TFunc (mapTs' ts) (replace' tres)+ TRow rlist -> Fix $ TRow $ go rlist+ where go rlist' =+ case rlist' of+ TRowEnd _ -> rlist'+ TRowProp p (TScheme qv t') rlist'' -> TRowProp p (TScheme qv (t' { qualType = replace' $ qualType t' })) (go rlist'')+ TRowRec tid ts -> if typeId == tid+ then TRowRec newTypeId $ dropAt indexToDrop ts+ else rlist'++allocNamedType :: TVarName -> Type -> Infer Type+allocNamedType n t =+ do typeId <- TypeId <$> fresh+ let namedType = TCons (TName typeId) $ map (Fix . TBody . TVar) $ Set.toList $ freeTypeVars t `Set.difference` Set.singleton n+ target = replaceFix (TBody (TVar n)) namedType t+ scheme <- unsafeGeneralize Map.empty $ qualEmpty target+ traceLog $ "===> Generated scheme for mu type: " ++ pretty scheme+ currentNamedTypes <- filter (areEquivalentNamedTypes (Fix namedType, scheme)) . map snd . Map.toList . namedTypes <$> get+ case currentNamedTypes of+ [] -> do addNamedType typeId (Fix namedType) scheme+ return $ Fix namedType+ (otherNT, _):_ -> return otherNT++resolveSimpleMutualRecursion :: TVarName -> Type -> TypeId -> Int -> Infer Type+resolveSimpleMutualRecursion n t tid ix =+ do (Fix (TCons (TName _) ts), scheme) <- (Map.lookup tid . namedTypes <$> get) `failWithM` error "oh no." -- TODO+ newTypeId <- TypeId <$> fresh+ let qVars' = dropAt ix $ schemeVars scheme+ replaceOldNamedType = replaceRecType tid newTypeId ix+ sType' = (schemeType scheme) { qualType = replaceOldNamedType $ qualType $ schemeType scheme }+ newTs = dropAt ix $ ts+ newNamedType = Fix (TCons (TName newTypeId) newTs)+ --updatedNamedType = Fix (TCons (TName tid) newTs)+ updatedScheme = applySubst (singletonSubst n newNamedType) $ TScheme qVars' sType'+ + addNamedType newTypeId newNamedType updatedScheme+ -- TODO: we could alternatively update the existing named type, but that will break it's schema (will now take less params?)+ --addNamedType tid updatedNamedType updatedScheme+ return $ replaceOldNamedType t+ + +getNamedType :: TVarName -> Type -> Infer Type+getNamedType n t =+ do let recTypeParamPos = isRecParamOnly n Nothing t+ traceLog ("isRecParamOnly: " ++ pretty n ++ " in " ++ pretty t ++ ": " ++ (show $ fmap pretty $ recTypeParamPos))+ case recTypeParamPos of+ Just [(tid, ix)] -> resolveSimpleMutualRecursion n t tid ix+ -- either the variable appears outside a recursive type's type parameter list, or it appears+ -- in more than one such position:+ _ -> allocNamedType n t +++unrollNameByScheme :: Substable a => [Type] -> [TVarName] -> a -> a+unrollNameByScheme ts qvars t = applySubst subst t+ where assocs = zip qvars ts+ subst = foldr (\(tvar,destType) s -> singletonSubst tvar destType `composeSubst` s) nullSubst assocs++-- | Unrolls (expands) a TName recursive type by plugging in the holes from the given list of types.+-- Similar to instantiation, but uses a pre-defined set of type instances instead of using fresh+-- type variables.+unrollName :: Source -> TypeId -> [Type] -> Infer QualType+unrollName a tid ts =+ -- TODO: Is it safe to ignore the scheme preds here?+ do (TScheme qvars t) <- (fmap snd . Map.lookup tid . namedTypes <$> get) `failWithM` throwError a "Unknown type id"+ return $ unrollNameByScheme ts qvars t+ +-- | Applies a subsitution onto the state (basically on the variable -> scheme map).+--+-- >>> :{+-- runInfer $ do+-- let t = TScheme [0] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))+-- let tenv = Map.empty+-- tenv' <- addVarScheme tenv "x" t+-- applySubstInfer $ Map.singleton 0 (Fix $ TBody TString)+-- varSchemes <$> get+-- :}+-- Right (fromList [(VarId 3,TScheme {schemeVars = [], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody TString)] Fix (TBody (TVar 1)))}})])+--+applySubstInfer :: TSubst -> Infer ()+applySubstInfer s =+ do traceLog ("applying subst: " ++ pretty s)+ modify $ applySubst s++-- | Instantiate a type scheme by giving fresh names to all quantified type variables.+--+-- For example:+--+-- >>> runInferWith (emptyInferState { nameSource = NameSource 2 }) . instantiate $ TScheme [0] (TQual { qualPred = [], qualType = Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1)) }) +-- Right (TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 3))] Fix (TBody (TVar 1)))})+--+-- In the above example, type variable 0 has been replaced with a fresh one (3), while the unqualified free type variable 1 has been left as-is.+--+-- >>> :{+-- runInfer $ do+-- let t = TScheme [0] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))+-- let tenv = Map.empty+-- tenv' <- addVarScheme tenv "x" t+-- instantiateVar emptySource "x" tenv'+-- :}+-- Right (TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 4))] Fix (TBody (TVar 1)))})+--+instantiateScheme :: Bool -> TypeScheme -> Infer QualType+instantiateScheme shouldAddVarInstances (TScheme tvarNames t) = do+ allocNames <- forM tvarNames $ \tvName -> do+ freshName <- fresh+ return (tvName, freshName)+ when shouldAddVarInstances $ forM_ allocNames $ uncurry addVarInstance+ let replaceVar n = fromMaybe n $ lookup n allocNames+ return $ mapVarNames replaceVar t++instantiate :: TypeScheme -> Infer QualType+instantiate = instantiateScheme True++instantiateVar :: Source -> EVarName -> TypeEnv -> Infer QualType+instantiateVar a n env = do+ varId <- getVarId n env `failWith` throwError a ("Unbound variable: '" ++ show n ++ "'")+ scheme <- getVarSchemeByVarId varId `failWithM` throwError a ("Assertion failed: missing var scheme for: '" ++ show n ++ "'")+ tracePretty ("Instantiated var '" ++ pretty n ++ "' with scheme: " ++ pretty scheme ++ " to") <$> instantiate scheme++----------------------------------------------------------------------+-- | Generalizes a type to a type scheme, i.e. wraps it in a "forall" that quantifies over all+-- type variables that are free in the given type, but are not free in the type environment.+--+-- Example:+--+-- >>> runInfer $ generalize (ELit "bla" LitUndefined) Map.empty $ qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))+-- Right (TScheme {schemeVars = [0,1], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 1)))}})+--+-- >>> :{+-- runInfer $ do+-- let t = TScheme [1] (TQual [] (Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 1))))+-- tenv <- addVarScheme Map.empty "x" t+-- generalize (ELit "bla" LitUndefined) tenv (qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 2)))+-- :}+-- Right (TScheme {schemeVars = [2], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 2)))}})+--+-- In this example the steps were:+--+-- 1. Environment: { x :: forall 0. 0 -> 1 }+--+-- 2. generalize (1 -> 2)+--+-- 3. result: forall 2. 1 -> 2+--+-- >>> let expr = ELit "foo" LitUndefined+--+-- >>> runInfer $ generalize expr Map.empty (qualEmpty $ Fix $ TFunc [Fix $ TBody (TVar 0)] (Fix $ TBody (TVar 0)))+-- Right (TScheme {schemeVars = [0], schemeType = TQual {qualPred = [], qualType = Fix (TFunc [Fix (TBody (TVar 0))] Fix (TBody (TVar 0)))}})+--+-- >>> runInfer $ generalize expr Map.empty (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody (TVar 1))] (Fix $ TBody (TVar 0)))+-- Right (TScheme {schemeVars = [0,1], schemeType = TQual {qualPred = [TPredIsIn {predClass = ClassName "Bla", predType = Fix (TBody (TVar 1))}], qualType = Fix (TBody (TVar 0))}})+--+-- TODO add tests for monotypes+unsafeGeneralize :: TypeEnv -> QualType -> Infer TypeScheme+unsafeGeneralize tenv t = do+ traceLog $ "Generalizing: " ++ pretty t+ s <- getMainSubst+ let t' = applySubst s t+ unboundVars <- Set.difference (freeTypeVars t') <$> getFreeTVars tenv+ traceLog $ "Generalization result: unbound vars = " ++ pretty unboundVars ++ ", type = " ++ pretty t'+ return $ TScheme (Set.toList unboundVars) t'++isExpansive :: Exp a -> Bool+isExpansive (EVar _ _) = False+isExpansive (EApp _ _ _) = True+isExpansive (EAssign _ _ _ _) = True+isExpansive (EPropAssign _ _ _ _ _) = True+isExpansive (EIndexAssign _ _ _ _ _) = True+isExpansive (ELet _ _ _ _) = True+isExpansive (EAbs _ _ _) = False+isExpansive (ELit _ _) = False+isExpansive (EArray _ _) = True+isExpansive (ETuple _ _) = True+isExpansive (EStringMap _ _) = True+isExpansive (ERow _ _ _) = True+isExpansive (ECase _ ep es) = any isExpansive (ep:map snd es)+isExpansive (EProp _ e _) = isExpansive e+isExpansive (EIndex _ a b) = any isExpansive [a, b]+isExpansive (ENew _ _ _) = True+++generalize :: Exp a -> TypeEnv -> QualType -> Infer TypeScheme+generalize exp' env t = if isExpansive exp'+ then return $ TScheme [] t+ else unsafeGeneralize env t++minifyVarsFunc :: (VarNames a) => a -> TVarName -> TVarName+minifyVarsFunc xs n = fromMaybe n $ Map.lookup n vars+ where vars = Map.fromList $ zip (Set.toList $ freeTypeVars xs) ([0..] :: [TVarName])++minifyVars :: (VarNames a) => a -> a+minifyVars xs = mapVarNames (minifyVarsFunc xs) xs++getVarInstances :: Infer (Graph.Gr QualType ())+getVarInstances = varInstances <$> get+++getMainSubst :: Infer TSubst+getMainSubst = mainSubst <$> get++applyMainSubst :: Substable b => b -> Infer b+applyMainSubst x =+ do s <- getMainSubst+ return $ applySubst s x+++substVar :: TSubst -> TVarName -> TVarName+substVar subst x = let varX = Fix (TBody (TVar x))+ in case applySubst subst varX of+ Fix (TBody (TVar zx)) -> zx+ _ -> x++lookupClass :: ClassName -> Infer (Maybe (Class Type))+lookupClass cs = Map.lookup cs . classes <$> get
+ src/Infernu/Lib.hs view
@@ -0,0 +1,30 @@+module Infernu.Lib where++import Data.Maybe (fromMaybe)+import Data.Map.Lazy (Map)+import qualified Data.Map.Lazy as Map+import Data.Set (Set)+import qualified Data.Set as Set+++matchZip :: [a] -> [b] -> Maybe [(a,b)]+matchZip [] [] = Just []+matchZip (_:_) [] = Nothing+matchZip [] (_:_) = Nothing+matchZip (x:xs) (y:ys) = fmap ((x,y):) $ matchZip xs ys++safeLookup :: Eq a => [(a,a)] -> a -> a+safeLookup assoc n = fromMaybe n $ lookup n assoc++-- | Creates an inverse map. Multiple keys mapping to the same values are collected into Sets.+--+-- >>> flipMap $ Map.fromList [(1,2),(2,2)]+-- fromList [(2,fromList [1,2])]+flipMap :: (Ord k, Ord v) => Map k v -> Map v (Set k)+flipMap m = Map.foldrWithKey (\k v m' -> Map.alter (Just . addKeyToSet' k) v m') Map.empty m+ where addKeyToSet' k Nothing = Set.singleton k+ addKeyToSet' k (Just s) = Set.insert k s++splatMap :: Ord k => Map (Set k) a -> Map k a+splatMap m = Map.foldrWithKey (\ks v m' -> foldr (\k m'' -> Map.insert k v m'') m' (Set.toList ks)) Map.empty m+
+ src/Infernu/Log.hs view
@@ -0,0 +1,27 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE BangPatterns #-}++module Infernu.Log+ (trace, tracePretty, traceLog, traceLogVal)+ where++import Infernu.Pretty+++#if TRACE+import Debug.Trace (trace)+#else+trace :: a -> b -> b+trace _ y = y+#endif++tracePretty :: Pretty a => String -> a -> a+tracePretty prefix x = trace (prefix ++ " " ++ pretty x) x++traceLogVal :: Applicative f => String -> a -> f a+traceLogVal !s !r = pure $! trace s r `seq` r++traceLog :: Applicative f => String -> f ()+traceLog !s = pure $! trace s () `seq` ()+
+ src/Infernu/Options.hs view
@@ -0,0 +1,34 @@+module Infernu.Options+ (Options(..), defaultOptions, opts)+ where++import Options.Applicative ++data Options = Options+ { optQuiet :: Bool+ , optShowCore :: Bool+ , optShowParsed :: Bool+ , optFileNames :: [String]+ }++defaultOptions :: Options+defaultOptions = Options { optQuiet = False, optShowCore = False, optShowParsed = False, optFileNames = [] }+ +opts :: ParserInfo Options+opts = info (helper <*> parseOpts)+ ( fullDesc+ <> progDesc "Infer types in the given JavaScript FILES and check for type errors. Unless -q is given, the source annotated with type signatures is outputted."+ <> header "infernu - static type checker for JavaScript using full type inference" )+ +parseOpts :: Parser Options+parseOpts = Options+ <$> switch (long "quiet"+ <> short 'q'+ <> help "Report only errors; don't output the annotated source with inferred types")+ <*> switch (long "dump-translation"+ <> help "Dump internal translation (used for debugging infernu)" )+ <*> switch (long "dump-parsed"+ <> help "Dump parsed JS syntax tree (used for debugging infernu)" )+ <*> some (argument str (metavar "FILES..."))+ +
+ src/Infernu/Parse.hs view
@@ -0,0 +1,281 @@+module Infernu.Parse+ (translate)+ where++import Control.Arrow ((***))+import Data.Maybe (mapMaybe, catMaybes)+import qualified Language.ECMAScript3.PrettyPrint as ES3PP+import qualified Language.ECMAScript3.Syntax as ES3+import Infernu.Types+import qualified Text.Parsec.Pos as Pos+import qualified Infernu.Log as Log+ +-- | A 'magic' impossible variable name that can never occur in valid JS syntax.+poo :: EVarName+poo = "_/_"++-- | A dummy expression that does nothing (but has a type).+empty :: a -> Exp (GenInfo, a)+empty z = ELit (gen z) LitUndefined -- EVar z poo+ +errorNotSupported :: (Show a, ES3PP.Pretty b) => String -> a -> b -> c+errorNotSupported featureName sourcePos expr = error $ "Not supported: '" ++ featureName ++ "' at " ++ show sourcePos ++ " in\n" ++ show (ES3PP.prettyPrint expr)++foldStmts :: Show a => [ES3.Statement a] -> Exp (GenInfo, a) -> Exp (GenInfo, a)+foldStmts [] expr = expr+foldStmts [x] expr = fromStatement x expr+foldStmts (x:xs) expr = fromStatement x (foldStmts xs expr)++-- Doesn't carry context over from one statement to the next (good for branching)+parallelStmts :: Show a => a -> [ES3.Statement a] -> Exp (GenInfo, a) -> Exp (GenInfo, a)+parallelStmts _ [] expr = expr+parallelStmts z stmts expr = ETuple (gen z) $ expr : map (flip fromStatement $ empty z) stmts+ +chainExprs :: Show a => a -> Exp (GenInfo, a) -> (Exp (GenInfo, a) -> Exp (GenInfo, a)) -> Exp (GenInfo, a) -> Exp (GenInfo, a)+chainExprs a init' getExpr expr = ELet (gen a) poo init' $ getExpr expr++singleStmt :: Show a => a -> Exp a -> Exp a -> Exp a+singleStmt a exp' = ELet a poo exp'++gen :: a -> (GenInfo, a)+gen x = (GenInfo True Nothing, x)++src :: a -> (GenInfo, a)+src x = (GenInfo False Nothing, x) ++decl :: a -> String -> (GenInfo, a)+decl x n = (GenInfo False (Just n), x)+ +fromStatement :: Show a => ES3.Statement a -> Exp (GenInfo, a) -> Exp (GenInfo, a)+fromStatement (ES3.BlockStmt _ stmts) = foldStmts stmts+fromStatement (ES3.EmptyStmt _) = id+fromStatement (ES3.ExprStmt z e) = singleStmt (gen z) $ fromExpression e+-- TODO: The if/while/do conversion is hacky+fromStatement (ES3.IfStmt z pred' thenS elseS) = chainExprs z (EArray (gen z) [fromExpression pred', ELit (gen z) (LitBoolean False)]) $ parallelStmts z [thenS, elseS]+fromStatement (ES3.IfSingleStmt z pred' thenS) = chainExprs z (EArray (gen z) [fromExpression pred', ELit (gen z) (LitBoolean False)]) $ fromStatement thenS+fromStatement (ES3.WhileStmt z pred' loopS) = chainExprs z (EArray (gen z) [fromExpression pred', ELit (gen z) (LitBoolean False)]) $ fromStatement loopS+fromStatement (ES3.DoWhileStmt z loopS pred') = chainExprs z (EArray (gen z) [fromExpression pred', ELit (gen z) (LitBoolean False)]) $ fromStatement loopS+fromStatement (ES3.BreakStmt _ _) = id -- TODO verify we can ignore this+fromStatement (ES3.ContinueStmt _ _) = id -- TODO verify we can ignore this+-- try/catch/finally are indepdendent branches that shouldn't be sharing context. catch is a like an+-- abstraction over the (optional) exception-bound name.+fromStatement (ES3.TryStmt z stmt mCatch mFinally) = chainExprs z catchExpr $ parallelStmts z ([stmt] ++ finallyS)+ where catchExpr = case mCatch of+ Just (ES3.CatchClause _ (ES3.Id z' e) s) -> EAbs (gen z') [e] (fromStatement s $ empty z')+ Nothing -> empty z+ finallyS = case mFinally of+ Just f -> [f]+ Nothing -> []+fromStatement (ES3.ThrowStmt _ _) = id+fromStatement s@(ES3.WithStmt z _ _) = errorNotSupported "with" z s+fromStatement s@(ES3.ForInStmt z _ _ _) = errorNotSupported "for .. in" z s+fromStatement (ES3.LabelledStmt _ _ s) = fromStatement s+fromStatement (ES3.ForStmt z init' test increment body) = case init' of+ ES3.NoInit -> forBody+ ES3.VarInit varDecls -> chainDecls varDecls . forBody+ ES3.ExprInit expr -> chainExprs z (fromExpression expr) forBody+ where forBody = chainExprs z test'' rest+ test'' = case test of+ Nothing -> EVar (gen z) poo+ Just test' -> EArray (gen z) [fromExpression test', ELit (gen z) (LitBoolean False)]+ body' = fromStatement body+ rest = case increment of+ Nothing -> body'+ Just increment' -> chainExprs z (fromExpression increment') body'++fromStatement (ES3.SwitchStmt z switch cases) = chainExprs z (EArray (gen z) tests) . parallelStmts z $ concatMap getCaseBody cases+ where tests = fromExpression switch : mapMaybe (fmap fromExpression . getCaseTest) cases+ getCaseTest (ES3.CaseDefault _ _) = Nothing+ getCaseTest (ES3.CaseClause _ test' _) = Just test'+ getCaseBody (ES3.CaseDefault _ body') = body'+ getCaseBody (ES3.CaseClause _ _ body') = body'++fromStatement (ES3.VarDeclStmt _ decls) = chainDecls decls+fromStatement (ES3.FunctionStmt z name args stmts) = toNamedAbs z args stmts name+fromStatement (ES3.ReturnStmt z x) = EIndexAssign (gen z) (EVar (gen z) "return") (ELit (gen z) $ LitNumber 0)+ $ case x of+ Nothing -> ELit (gen z) LitUndefined+ Just x' -> fromExpression x'++-- | Creates an EAbs (function abstraction)+toAbs :: Show a => a -> [ES3.Id c] -> [ES3.Statement a] -> Exp (GenInfo, a)+toAbs z args stmts = EAbs (src z) ("this" : map ES3.unId args) body'+ -- TODO: this can lead to problems if "return" was never called (there's a partial function here - dereferencing array element 0)+ where body' = case any hasReturn stmts of+ True -> ELet (gen z) "return" (EArray (gen z) []) $ foldStmts stmts $ (EIndex (gen z) (EVar (gen z) "return") (ELit (gen z) $ LitNumber 0))+ False -> ELet (gen z) "return" (empty z) $ foldStmts stmts $ (ELit (gen z) LitUndefined)+++hasReturn :: ES3.Statement a -> Bool+hasReturn (ES3.BlockStmt _ stmts) = any hasReturn stmts+hasReturn (ES3.EmptyStmt _) = False+hasReturn (ES3.ExprStmt _ _) = False+hasReturn (ES3.IfStmt _ _ thenS elseS) = any hasReturn [thenS, elseS]+hasReturn (ES3.IfSingleStmt _ _ thenS) = hasReturn thenS+hasReturn (ES3.WhileStmt _ _ loopS) = hasReturn loopS+hasReturn (ES3.DoWhileStmt _ loopS _) = hasReturn loopS+hasReturn (ES3.BreakStmt _ _) = False+hasReturn (ES3.ContinueStmt _ _) = False+hasReturn (ES3.TryStmt _ stmt mCatch mFinally) = any hasReturn (stmt : finallyS ++ catchS)+ where catchS = case mCatch of+ Just (ES3.CatchClause _ _ s) -> [s]+ Nothing -> []+ finallyS = case mFinally of+ Just f -> [f]+ Nothing -> []+hasReturn (ES3.ThrowStmt _ _) = False+hasReturn (ES3.WithStmt _ _ s) = hasReturn s+hasReturn (ES3.ForInStmt _ _ _ s) = hasReturn s+hasReturn (ES3.LabelledStmt _ _ s) = hasReturn s+hasReturn (ES3.ForStmt _ _ _ _ body) = hasReturn body+hasReturn (ES3.SwitchStmt _ _ cases) = and $ map fromCase cases+ where fromCase (ES3.CaseClause _ _ s) = any hasReturn s+ fromCase (ES3.CaseDefault _ stmts) = any hasReturn stmts+hasReturn (ES3.VarDeclStmt _ _) = False+hasReturn (ES3.FunctionStmt _ _ _ _) = False+hasReturn (ES3.ReturnStmt _ _) = True+++addDecl :: Show a => a -> String -> Exp (GenInfo, a) -> Exp (GenInfo, a) +addDecl z name expr = Log.trace ("addDecl: " ++ show res) res+ where res = mapTopAnnotation (const $ decl z name) expr + +toNamedAbs :: Show a => a -> [ES3.Id c] -> [ES3.Statement a] -> ES3.Id a -> Exp (GenInfo, a) -> Exp (GenInfo, a)+toNamedAbs z args stmts (ES3.Id zn name) letBody = let abs' = addDecl zn name $ toAbs z args stmts+ in ELet (gen z) name abs' letBody++chainDecls :: Show a => [ES3.VarDecl a] -> Exp (GenInfo, a) -> Exp (GenInfo, a)+chainDecls [] k = k+chainDecls (ES3.VarDecl z' (ES3.Id _ name) Nothing:xs) k = ELet (gen z') name (ELit (gen z') LitUndefined) (chainDecls xs k)+chainDecls (ES3.VarDecl z' (ES3.Id _ name) (Just v):xs) k = ELet (gen z') name (addDecl z' name $ fromExpression v) (chainDecls xs k)++makeThis :: Show a => a -> Exp a+makeThis z = ELit z $ LitNull -- TODO should be undefined++fromExpression :: Show a => ES3.Expression a -> Exp (GenInfo, a)+fromExpression (ES3.StringLit z s) = ELit (src z) $ LitString s+fromExpression (ES3.RegexpLit z s g i) = ELit (src z) $ LitRegex s g i+fromExpression (ES3.BoolLit z s) = ELit (src z) $ LitBoolean s+fromExpression (ES3.IntLit z s) = ELit (src z) (LitNumber $ fromIntegral s)+fromExpression (ES3.NumLit z s) = ELit (src z) $ LitNumber s+fromExpression (ES3.NullLit z) = ELit (src z) LitNull+fromExpression (ES3.ArrayLit z exprs) = EArray (src z) $ map fromExpression exprs+fromExpression (ES3.ObjectLit z props) = let stringProps = map (fromPropString . fst) props+ in if all (\x -> x /= Nothing) stringProps+ then EStringMap (src z) $ zip (catMaybes stringProps) (map (fromExpression . snd) props) + else ERow (src z) False $ map (fromProp *** fromExpression) props+fromExpression (ES3.BracketRef z arrExpr indexExpr) = EIndex (src z) (fromExpression arrExpr) (fromExpression indexExpr)+fromExpression (ES3.VarRef z name) = EVar (src z) $ ES3.unId name+fromExpression (ES3.CondExpr z ePred eThen eElse) = ECase (src z) (fromExpression ePred) [(LitBoolean True, fromExpression eThen), (LitBoolean False, fromExpression eElse)]+fromExpression (ES3.CallExpr z expr argExprs) =+ -- Instead of simply translating, here we also do some specific simplification by defining+ -- (adding an ELet) for the object expression if the function is a method call.+ -- The idea is to prevent duplicate expressions in the output tree (<complicated expr>.method+ -- (<complicated expr>, ...)) by binding the object expression to '__obj__'.+ -- So that we get: let __obj__ = <complicated expr> in __obj__.method(__obj__, ...)+ case expr of+ ES3.DotRef z' varExpr@(ES3.VarRef _ _) (ES3.Id _ propName) -> appExpr (Just propName) (EProp (src z') var propName) var+ where var = fromExpression varExpr+ ES3.DotRef z' objExpr (ES3.Id _ propName) -> ELet (gen z') objVarName obj $ appExpr (Just propName) (EProp (src z') objVar propName) objVar+ where obj = fromExpression objExpr+ objVar = EVar (gen z') objVarName+ objVarName = "_/obj/_"+ _ -> appExpr Nothing (fromExpression expr) (ELit (gen z) LitUndefined)+ where appExpr (Just "call") _ obj = (EApp (src z) obj (map fromExpression argExprs)) -- TODO: may be wrong if object expression is not a function!+ appExpr _ funcExpr thisExpr = (EApp (src z) funcExpr (thisExpr : map fromExpression argExprs))+ --error $ "Assetion failed: expecting at least 'this'"+fromExpression (ES3.AssignExpr z op target expr) = assignExpr+ where sz = src z+ (assignExpr, oldValue) = case target of+ ES3.LVar _ name -> (assignToVar z name value, EVar sz name)+ ES3.LDot _ objExpr name -> (assignToProperty z objExpr name value, EProp sz (fromExpression objExpr) name)+ ES3.LBracket _ objExpr idxExpr -> (assignToIndex z objExpr idxExpr value, EIndex sz (fromExpression objExpr) (fromExpression idxExpr))+ expr' = fromExpression expr+ value = case op of+ ES3.OpAssign -> expr'+ ES3.OpAssignAdd -> applyOpFunc z ES3.OpAdd [oldValue, expr']+ ES3.OpAssignSub -> applyOpFunc z ES3.OpSub [oldValue, expr']+ ES3.OpAssignMul -> applyOpFunc z ES3.OpMul [oldValue, expr']+ ES3.OpAssignDiv -> applyOpFunc z ES3.OpDiv [oldValue, expr']+ ES3.OpAssignMod -> applyOpFunc z ES3.OpMod [oldValue, expr']+ ES3.OpAssignLShift -> applyOpFunc z ES3.OpLShift [oldValue, expr']+ ES3.OpAssignSpRShift -> applyOpFunc z ES3.OpSpRShift [oldValue, expr']+ ES3.OpAssignZfRShift -> applyOpFunc z ES3.OpZfRShift [oldValue, expr']+ ES3.OpAssignBAnd -> applyOpFunc z ES3.OpBAnd [oldValue, expr']+ ES3.OpAssignBXor -> applyOpFunc z ES3.OpBXor [oldValue, expr']+ ES3.OpAssignBOr -> applyOpFunc z ES3.OpBOr [oldValue, expr']++fromExpression (ES3.FuncExpr z Nothing argNames stmts) = toAbs z argNames stmts+fromExpression (ES3.FuncExpr z (Just name) argNames stmts) = toNamedAbs z argNames stmts name (EVar (gen z) $ ES3.unId name)++fromExpression e@(ES3.ListExpr z exprs) =+ case exprs of+ [] -> errorNotSupported "empty list (,) expression" z e+ [x] -> fromExpression x+ -- Should the let here use an allocated name here?+ xs -> ELet (gen z) poo (ETuple (gen z) (tail exprs')) (head exprs')+ where exprs' = reverse . map fromExpression $ xs+fromExpression (ES3.ThisRef z) = EVar (src z) "this"+fromExpression (ES3.DotRef z expr propId) = EProp (src z) (fromExpression expr) (ES3.unId propId)+fromExpression (ES3.NewExpr z expr argExprs) = ENew (src z) (fromExpression expr) (map fromExpression argExprs)+-- ELet z "__this__" (ERow z True []) (ELet z "_bla_" (EApp z (fromExpression expr) ((EVar z "__this__") : map fromExpression argExprs)) (EVar z "__this__"))+fromExpression e@(ES3.PrefixExpr z op expr) =+ case op of+ -- prefix +/- are converted to 0-x and 0+x+ ES3.PrefixPlus -> EApp (gen z) (opFunc z ES3.OpAdd) [makeThis (gen z), ELit (gen z) $ LitNumber 0, fromExpression expr]+ ES3.PrefixMinus -> EApp (gen z) (opFunc z ES3.OpSub) [makeThis (gen z), ELit (gen z) $ LitNumber 0, fromExpression expr]+ -- delete, void unsupported+ ES3.PrefixVoid -> errorNotSupported "void" z e+ ES3.PrefixDelete -> errorNotSupported "delete" z e+ -- all the rest are expected to exist as unary builtin functions+ _ -> EApp (src z) (EVar (gen z) $ show . ES3PP.prettyPrint $ op) [makeThis (gen z), fromExpression expr]+fromExpression (ES3.InfixExpr z op e1 e2) = EApp (gen z) (EVar (gen z) $ show . ES3PP.prettyPrint $ op) [makeThis (gen z), fromExpression e1, fromExpression e2]+fromExpression (ES3.UnaryAssignExpr z op (ES3.LVar _ name)) = assignToVar z name $ addConstant z op (EVar (src z) name)+fromExpression (ES3.UnaryAssignExpr z op (ES3.LDot _ objExpr name)) = assignToProperty z objExpr name $ addConstant z op (EProp (src z) objExpr' name)+ where objExpr' = fromExpression objExpr+fromExpression (ES3.UnaryAssignExpr z op (ES3.LBracket _ objExpr idxExpr)) = assignToIndex z objExpr idxExpr $ addConstant z op (EIndex (src z) objExpr' idxExpr')+ where objExpr' = fromExpression objExpr+ idxExpr' = fromExpression idxExpr++opFunc :: a -> ES3.InfixOp -> Exp (GenInfo, a)+opFunc z op = EVar (gen z) $ show . ES3PP.prettyPrint $ op++applyOpFunc :: Show a => a -> ES3.InfixOp -> [Exp (GenInfo, a)] -> Exp (GenInfo, a)+applyOpFunc z op exprs = EApp (gen z) (opFunc z op) (makeThis (gen z) : exprs)++-- TODO: the translation results in equivalent types, but currently ignore pre vs. postfix so the data flow is wrong.+addConstant :: Show a => a -> ES3.UnaryAssignOp -> Exp (GenInfo, a) -> Exp (GenInfo, a)+addConstant z op expr = EApp (gen z) (opFunc z ES3.OpAdd) [makeThis (gen z), expr, ELit (gen z) $ LitNumber x]+ where x = case op of+ ES3.PrefixInc -> 1+ ES3.PrefixDec -> -1+ ES3.PostfixInc -> 1+ ES3.PostfixDec -> -1++assignToVar :: Show a => a -> EVarName -> Exp (GenInfo, a) -> Exp (GenInfo, a)+assignToVar z name expr = EAssign (src z) name expr (EVar (src z) name)++assignToProperty :: Show a => a -> ES3.Expression a -> EPropName -> Exp (GenInfo, a) -> Exp (GenInfo, a)+assignToProperty z objExpr name expr = EPropAssign (src z) objExpr' name expr (EProp (src z) objExpr' name)+ where objExpr' = fromExpression objExpr++assignToIndex :: Show a => a -> ES3.Expression a -> ES3.Expression a -> Exp (GenInfo, a) -> Exp (GenInfo, a)+assignToIndex z objExpr idxExpr expr = EIndexAssign (src z) objExpr' idxExpr' expr (EIndex (src z) objExpr' idxExpr')+ where objExpr' = fromExpression objExpr+ idxExpr' = fromExpression idxExpr+++fromProp :: ES3.Prop a -> String+fromProp (ES3.PropId _ (ES3.Id _ x)) = x+fromProp (ES3.PropString _ x) = x+fromProp (ES3.PropNum _ x) = show x++fromPropString :: ES3.Prop a -> Maybe String+fromPropString (ES3.PropString _ x) = Just x+fromPropString _ = Nothing+ +-- -- ------------------------------------------------------------------------++translate :: [ES3.Statement Pos.SourcePos] -> Exp (GenInfo, Pos.SourcePos)+translate js = ELet (gen pos) poo (empty pos) $ foldStmts js $ EVar (gen pos) poo+ where pos = Pos.initialPos "<global>"
+ src/Infernu/Pretty.hs view
@@ -0,0 +1,227 @@+{-# LANGUAGE FlexibleInstances #-}+module Infernu.Pretty where+++import Infernu.Types++ +import Data.Char (chr, ord)+import qualified Data.Char as Char+import qualified Data.Digits as Digits+import Data.List (intercalate)+import qualified Data.Map.Lazy as Map+import qualified Data.Graph.Inductive as Graph++import qualified Data.Set as Set+import qualified Text.Parsec.Pos as Pos++tab :: Int -> String+tab t = replicate (t*4) ' '++class Pretty a where+ prettyTab :: Int -> a -> String++instance Pretty a => Pretty (Maybe a) where+ prettyTab _ x = maybe "Nothing" pretty x++instance (Pretty a, Pretty b) => Pretty (a,b) where+ prettyTab _ (a,b) = "(" ++ pretty a ++ ", " ++ pretty b ++ ")"++instance (Pretty a, Pretty b, Pretty c) => Pretty (a,b,c) where+ prettyTab _ (a,b,c) = "(" ++ pretty a ++ ", " ++ pretty b ++ ", " ++ pretty c ++ ")"++prettyList :: Pretty a => [a] -> String+prettyList [] = "[]"+prettyList xs = "[" ++ intercalate "," (map pretty xs) ++ "]"++instance Pretty [String] where+ prettyTab _ = prettyList++instance Pretty [Type] where+ prettyTab _ = prettyList++instance (Pretty a, Pretty b) => Pretty [(a,b)] where+ prettyTab _ xs = "[" ++ intercalate "," (map pretty xs) ++ "]"++pretty :: Pretty a => a -> String+pretty = prettyTab 0++instance Pretty Source where+ prettyTab _ (Source (genInfo, pos)) = pretty pos ++ (if isGen genInfo then "*" else "") ++ (maybe "" (\x -> pretty x ++ " : ") $ declName genInfo)+ +instance Pretty LitVal where+ prettyTab _ (LitNumber x) = show x+ prettyTab _ (LitBoolean x) = show x+ prettyTab _ (LitString x) = show x+ prettyTab _ (LitRegex x g i) = "/" ++ x ++ "/" ++ (if g then "g" else "") ++ (if i then "i" else "") ++ (if g || i then "/" else "")+ prettyTab _ LitUndefined = "undefined"+ prettyTab _ LitNull = "null"++instance Pretty EVarName where+ prettyTab _ x = x+++nakedSingleOrTuple :: [String] -> String+nakedSingleOrTuple [] = "()"+nakedSingleOrTuple [x] = x+nakedSingleOrTuple xs = "(" ++ intercalate ", " xs ++ ")"++instance Pretty (Exp a) where+ prettyTab t (EVar _ n) = prettyTab t n+ prettyTab t (EApp _ e1 args) = "(" ++ prettyTab t e1 ++ " " ++ nakedSingleOrTuple (map (prettyTab t) args) ++")"+ prettyTab t (EAbs _ args e) = "(\\" ++ nakedSingleOrTuple (map (prettyTab t) args) ++ " -> " ++ prettyTab (t+1) e ++ ")"+ prettyTab t (ELet _ n e1 e2) = "\n" ++ tab t ++ "let " ++ letLine n e1 e2+ where letLine n' e' eBody = prettyTab t n'+ ++ " = "+ ++ prettyTab (t+1) e'+ ++ "\n" ++ tab (t+1)+ ++ case eBody of+ (ELet _ nb e1b e2b) -> letLine nb e1b e2b+ _ -> pretty " in " ++ prettyTab (t+1) eBody+ prettyTab t (ELit _ l) = prettyTab t l+ prettyTab t (EAssign _ n e1 e2) = prettyTab t n ++ " := " ++ prettyTab t e1 ++ ";\n" ++ tab (t+1) ++ prettyTab (t+1) e2+ prettyTab t (EPropAssign _ obj n e1 e2) = prettyTab t obj ++ "." ++ prettyTab t n ++ " := " ++ prettyTab t e1 ++ ";\n" ++ tab (t+1) ++ prettyTab (t+1) e2+ prettyTab t (EIndexAssign _ obj i e1 e2) = prettyTab t obj ++ "[" ++ prettyTab t i ++ "] := " ++ prettyTab t e1 ++ ";\n" ++ tab (t+1) ++ prettyTab (t+1) e2+ prettyTab t (EArray _ es) = "[" ++ intercalate ", " (map (prettyTab t) es) ++ "]"+ prettyTab t (ETuple _ es) = "(" ++ intercalate ", " (map (prettyTab t) es) ++ ")"+ prettyTab t (ERow _ isOpen props) = "{" ++ intercalate ", " (map (\(n,v) -> prettyTab t n ++ ": " ++ prettyTab t v) props) ++ (if isOpen then ", " else "") ++ "}"+ prettyTab t (ECase _ ep es) = "case " ++ prettyTab t ep ++ " of\n" ++ (concatMap formatBranch' es)+ where formatBranch' (pat, branch) = tab (t+1)+ ++ prettyTab (t+1) pat+ ++ " -> "+ ++ prettyTab (t+1) branch+ prettyTab t (EProp _ e n) = prettyTab t e ++ "." ++ pretty n+ prettyTab t (EIndex _ e1 e2) = prettyTab t e1 ++ "[" ++ prettyTab t e2 ++ "]"+ prettyTab t (ENew _ e args) = "new " ++ prettyTab t e ++ " " ++ nakedSingleOrTuple (map (prettyTab t) args)+ prettyTab t (EStringMap _ exprs) = "<" ++ intercalate ", " (map (\(n,v) -> prettyTab t n ++ " => " ++ prettyTab t v) exprs) ++ ">"++toChr :: Int -> Char+toChr n = chr (ord 'a' + (n - 1))++-- |+-- >>> prettyTab 0 (0 :: TVarName)+-- "a"+-- >>> prettyTab 0 (26 :: TVarName)+-- "aa"+instance Pretty TVarName where+ prettyTab _ n = foldr ((++) . (:[]) . toChr) [] (Digits.digits 26 (n + 1))++instance Pretty Bool where+ prettyTab _ x = show x++instance Pretty TypeId where+ prettyTab _ (TypeId n) = capitalize $ pretty n+ where capitalize [] = []+ capitalize (x:xs) = Char.toUpper x : xs++instance Pretty TBody where+ prettyTab t (TVar n) = prettyTab t n+ prettyTab _ x = case show x of+ 'T':xs -> xs+ xs -> xs++instance Pretty TConsName where+ prettyTab _ = show++instance Pretty RowTVar where+ prettyTab _ t = ".." ++ pretty (getRowTVar t)++instance Pretty Type where+ prettyTab x = prettyType x . unFix++instance Pretty (FType Type) where+ prettyTab = prettyType+ +prettyType :: Int -> FType Type -> String+prettyType n (TBody t) = prettyTab n t+prettyType n (TFunc ts tres) = wrapThis this $ "(" ++ args ++ " -> " ++ prettyTab n tres ++ ")"+ where nonThisArgs = map (prettyTab n) . drop 1 $ ts+ (this, args) = case ts of+ [] -> (Nothing, nakedSingleOrTuple nonThisArgs)+ (this_:_) -> (Just this_, nakedSingleOrTuple nonThisArgs)+ wrapThis Nothing s = s+ wrapThis (Just (Fix (TBody TUndefined))) s = s+ wrapThis (Just t) s = prettyTab n t ++ "." ++ s+-- prettyTab _ (TCons TFunc ts) = error $ "Malformed TFunc: " ++ intercalate ", " (map pretty ts)+prettyType n (TCons TArray [t]) = "[" ++ prettyTab n t ++ "]"+prettyType n (TCons TArray ts) = error $ "Malformed TArray: " ++ intercalate ", " (map (prettyTab n) ts)+prettyType n (TCons TTuple ts) = "(" ++ intercalate ", " (map (prettyTab n) ts) ++ ")"+prettyType _ (TCons (TName name) _) = "<" ++ pretty name ++ ">" -- : " ++ (unwords $ map (prettyTab n) ts) ++ ">"+prettyType n (TCons TStringMap [t]) = "Map " ++ prettyTab n t+prettyType n (TCons TStringMap ts) = error $ "Malformed TStringMap: " ++ intercalate ", " (map (prettyTab n) ts) +prettyType t (TRow list) = "{"+ ++ body'+ ++ (case r of+ FlatRowEndTVar r' -> maybe "" ((", "++) . pretty) r'+ FlatRowEndRec tid ts -> ", " ++ prettyTab (t+1) (Fix $ TCons (TName tid) ts) -- TODO+ )+ ++ "}"+ where (props, r) = flattenRow list+ printProp' = (\(n,v) -> prettyTab (t+1) n ++ ": " ++ prettyTab (t+1) v)+ body' = case Map.toList props of+ [] -> ""+ [p] -> printProp' p+ ps -> "\n" ++ tab (t+1) ++ intercalate (",\n" ++ tab (t+1)) (map printProp' ps) ++ "\n" ++ tab t++instance Pretty ClassName where+ prettyTab _ (ClassName c) = c+ +instance (Pretty t) => Pretty (TPred t) where+ prettyTab _ (TPredIsIn cn t) = pretty cn ++ " " ++ pretty t+ +instance (Pretty t) => Pretty [TPred t] where+ prettyTab n p = intercalate ", " $ map (prettyTab n) p++instance (VarNames t, Pretty t) => Pretty (TQual t) where+ prettyTab n (TQual [] t) = prettyTab n t+ prettyTab n (TQual preds t) = prettyTab n preds ++ " => " ++ prettyTab n t++instance (Ord t, VarNames t, Pretty t) => Pretty (TScheme t) where+ prettyTab n (TScheme vars t) = forall ++ prettyTab n t+ where forall = if null vars then "" else "forall " ++ unwords (map (prettyTab n) vars) ++ ". "++instance (Pretty a, Pretty b) => Pretty (Either a b) where+ prettyTab n (Left x) = "Error: " ++ prettyTab n x+ prettyTab n (Right x) = prettyTab n x++instance (Pretty k, Pretty v) => Pretty (Map.Map k v) where+ prettyTab n s = "Map (" ++ str' ++ ")"+ where str' = intercalate ", " . map (\(k,v) -> prettyTab n k ++ " => " ++ prettyTab n v) . Map.toList $ s++instance (Pretty k) => Pretty (Set.Set k) where+ prettyTab n s = "Set {" ++ str' ++ "}"+ where str' = intercalate ", " . map (prettyTab n) . Set.toList $ s++instance Pretty Pos.SourcePos where+ prettyTab _ p = Pos.sourceName p ++ ":" ++ show (Pos.sourceLine p) ++ ":" ++ show (Pos.sourceColumn p)++instance Pretty GenInfo where+ prettyTab _ g = show g+ +instance Pretty TypeError where+ prettyTab t (TypeError s m) = prettyTab t s ++ ": Error: " ++ prettyTab (t+1) m++instance Pretty NameSource where+ prettyTab _ = show++instance Pretty VarId where+ prettyTab _ = show++instance (Ord t, VarNames t, Pretty t) => Pretty (Class t) where+ prettyTab n c = "{ instances = [" ++ s' ++ "] }"+ where s' = intercalate ", " . map (prettyTab n) $ classInstances c++instance (Show a, Show b) => Pretty (Graph.Gr a b) where+ prettyTab _ = Graph.prettify+ +instance Pretty InferState where+ prettyTab t (InferState ns sub vs vi tn cs pu) = "InferState { nameSource: "+ ++ pretty ns ++ newline+ ++ ", subst: " ++ pretty sub ++ newline+ ++ ", varSchemes: " ++ pretty vs ++ newline+ ++ ", varInstances: " ++ pretty vi ++ newline+ ++ ", namedTypes: " ++ pretty tn ++ newline+ ++ ", pendingUni: " ++ pretty pu ++ newline+ ++ ", classes: " ++ pretty cs ++ newline+ ++ "}"+ where newline = "\n" ++ tab (t+1)
+ src/Infernu/Types.hs view
@@ -0,0 +1,578 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveFunctor #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE UndecidableInstances #-}++module Infernu.Types+ (GenInfo(..)+ , Source(..)+ , emptySource+ , Exp(..)+ , LitVal(..)+ , EVarName+ , TVarName+ , TBody(..)+ , TConsName(..)+ , TypeId(..)+ , Type+ , Fix(..)+ , replaceFix+ , FType(..)+ , TypeError(..)+ , InferState(..)+ , RowTVar(..)+ , getRowTVar+ , liftRowTVar+ , FlatRowEnd(..)+ , TRowList(..)+ , ClassName(..)+ , Class(..)+ , TPred(..)+ , TQual(..)+ , qualEmpty+ , QualType+ , TScheme(..)+ , schemeEmpty+ , schemeFromQual+ , TypeScheme+ , TypeEnv+ , Substable(..)+ , flattenRow+ , unflattenRow+ , TSubst+ , nullSubst+ , composeSubst+ , singletonSubst+ , VarId(..)+ , NameSource(..)+ , addEquivalence+ , VarNames(freeTypeVars, mapVarNames)+ , EPropName+ , mapTopAnnotation+#ifdef QUICKCHECK+ , runAllTests+#endif+ ) where++import Data.Foldable (Foldable (..), foldr)+import qualified Data.Map.Lazy as Map+import Data.Maybe (fromMaybe)+import qualified Data.Set as Set+import qualified Data.Graph.Inductive as Graph+import Prelude hiding (foldr)+import qualified Text.Parsec.Pos as Pos++import Infernu.Fix (Fix (..), replaceFix)++#ifdef QUICKCHECK+import Data.DeriveTH+import Data.Map.Lazy (Map)+import qualified Data.Map.Lazy as Map+import Test.QuickCheck (choose, resize)+import Test.QuickCheck.All+import Test.QuickCheck.Arbitrary (Arbitrary (..))+#endif++data GenInfo = GenInfo { isGen :: Bool, declName :: Maybe String }+ deriving (Show, Eq, Ord)++type EVarName = String+type EPropName = String++data LitVal = LitNumber Double+ | LitBoolean Bool+ | LitString String+ | LitRegex String Bool Bool+ | LitUndefined+ | LitNull+ deriving (Show, Eq, Ord)++data Exp a = EVar a EVarName+ | EApp a (Exp a) [Exp a]+ | EAbs a [EVarName] (Exp a)+ | ELet a EVarName (Exp a) (Exp a)+ | ELit a LitVal+ | EAssign a EVarName (Exp a) (Exp a)+ | EPropAssign a (Exp a) EPropName (Exp a) (Exp a)+ | EIndexAssign a (Exp a) (Exp a) (Exp a) (Exp a)+ | EArray a [Exp a]+ | ETuple a [Exp a]+ | ERow a Bool [(EPropName, Exp a)]+ | EStringMap a [(String, Exp a)]+ | ECase a (Exp a) [(LitVal, Exp a)]+ | EProp a (Exp a) EPropName+ -- TODO EIndex should not be part of the AST. should be a builtin function using+ -- pattern matching instead+ | EIndex a (Exp a) (Exp a)+ -- TODO consider better options for causing rows to become closed outside the 'new' call+ | ENew a (Exp a) [Exp a]+ deriving (Show, Eq, Ord, Functor, Foldable)++----------------------------------------------------------------------+ +type TVarName = Int++data TBody = TVar TVarName+ | TNumber | TBoolean | TString | TRegex | TUndefined | TNull+ deriving (Show, Eq, Ord)++newtype TypeId = TypeId TVarName+ deriving (Show, Eq, Ord)++data TConsName = TArray | TTuple | TName TypeId | TStringMap+ deriving (Show, Eq, Ord)++newtype RowTVar = RowTVar TVarName+ deriving (Show, Eq, Ord)++getRowTVar :: RowTVar -> TVarName+getRowTVar (RowTVar x) = x++liftRowTVar :: (TVarName -> TVarName) -> RowTVar -> RowTVar+liftRowTVar f (RowTVar x) = RowTVar (f x)++-- | Row type.+data TRowList t = TRowProp EPropName (TScheme t) (TRowList t)+ | TRowEnd (Maybe RowTVar)+ | TRowRec TypeId [t]+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++data FType t = TBody TBody+ | TCons TConsName [t]+ -- | TFunc (functions) are Profunctor-types. Arguments could have been a single 't'+ -- and always wrapped in a Tuple - but are expanded to a list here for convenience+ | TFunc [t] t + | TRow (TRowList t)+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++type Type = Fix FType++newtype Source = Source (GenInfo, Pos.SourcePos)+ deriving (Show, Eq, Ord)++emptySource :: Source+emptySource = Source (GenInfo True Nothing, Pos.initialPos "")+ +data TypeError = TypeError { source :: Source, message :: String }+ deriving (Show, Eq, Ord)++----------------------------------------------------------------------++class VarNames a where+ freeTypeVars :: a -> Set.Set TVarName+ mapVarNames :: (TVarName -> TVarName) -> a -> a++ freeTypeVars' :: (VarNames a, Foldable f) => f a -> Set.Set TVarName+ freeTypeVars' = foldr (Set.union . freeTypeVars) Set.empty++ mapVarNames' :: (VarNames a, Functor f) => (TVarName -> TVarName) -> f a -> f a+ mapVarNames' f = fmap (mapVarNames f)+++instance VarNames (TVarName) where+ freeTypeVars = Set.singleton+ mapVarNames f = f++instance VarNames (TBody) where+ mapVarNames f (TVar x) = TVar $ f x+ mapVarNames _ t = t++ freeTypeVars (TVar n) = Set.singleton n+ freeTypeVars _ = Set.empty++instance VarNames t => VarNames (Map.Map a t) where+ freeTypeVars = freeTypeVars'+ mapVarNames = mapVarNames'+instance VarNames t => VarNames [t] where+ freeTypeVars = freeTypeVars'+ mapVarNames = mapVarNames'+instance VarNames t => VarNames (a, t) where+ freeTypeVars = freeTypeVars'+ mapVarNames = mapVarNames'+instance VarNames t => VarNames (Exp (a, t)) where+ freeTypeVars = freeTypeVars'+ mapVarNames = mapVarNames'++-- | VarNames instance for TRowList+--+-- >>> freeTypeVars (TRowProp "x" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd $ Just $ RowTVar 1))+-- fromList [1]+-- >>> freeTypeVars (TRowProp "x" (schemeEmpty $ Fix $ TBody $ TVar 2) (TRowEnd Nothing))+-- fromList [2]+-- >>> freeTypeVars (TRowProp "x" (schemeEmpty $ Fix $ TBody $ TVar 2) (TRowEnd $ Just $ RowTVar 1))+-- fromList [1,2]+-- >>> freeTypeVars (TRowProp "x" (schemeEmpty $ Fix $ TBody $ TVar 2) (TRowProp "y" (schemeEmpty $ Fix $ TBody $ TVar 3) (TRowEnd $ Just $ RowTVar 1)))+-- fromList [1,2,3]+instance VarNames t => VarNames (TRowList t) where+ freeTypeVars (TRowEnd (Just (RowTVar n))) = Set.singleton n+ freeTypeVars (TRowEnd _) = Set.empty+ freeTypeVars (TRowProp _ t r) = Set.union (freeTypeVars t) (freeTypeVars r)+ freeTypeVars (TRowRec _ ts) = foldr (Set.union . freeTypeVars) Set.empty ts++ mapVarNames f (TRowEnd n) = TRowEnd $ fmap (liftRowTVar f) n+ mapVarNames f (TRowProp n t r) = TRowProp n (mapVarNames f t) (mapVarNames f r)+ mapVarNames f (TRowRec tid ts) = TRowRec tid (mapVarNames f ts)++-- | VarNames instance for Type t+--+-- >>> freeTypeVars (Fix $ TBody TNumber)+-- fromList []+-- >>> freeTypeVars (Fix $ TBody $ TVar 0)+-- fromList [0]+-- >>> freeTypeVars (Fix $ TFunc [Fix $ TBody $ TVar 0] (Fix $ TBody $ TVar 1))+-- fromList [0,1]+-- >>> freeTypeVars (Fix $ TFunc [] (Fix $ TBody $ TVar 1))+-- fromList [1]+-- >>> freeTypeVars $ (Fix $ (TRow (TRowEnd (Just $ RowTVar 3))) :: Type)+-- fromList [3]+instance VarNames Type where+ freeTypeVars (Fix (TBody b)) = freeTypeVars b+ freeTypeVars (Fix (TRow trlist)) = freeTypeVars trlist+ freeTypeVars (Fix t) = freeTypeVars' t++ mapVarNames f (Fix (TBody b)) = Fix $ TBody $ mapVarNames f b+ mapVarNames f (Fix (TRow trlist)) = Fix $ TRow $ mapVarNames f trlist+ mapVarNames f (Fix t) = Fix $ mapVarNames' f t++instance VarNames (FType (Fix FType)) where+ freeTypeVars = freeTypeVars . Fix+ mapVarNames f = unFix . mapVarNames f . Fix++-- instance VarNames a => VarNames (FType a) where+-- freeTypeVars = freeTypeVars'+-- -- (TBody t) = freeTypeVars t+-- -- freeTypeVars (TCons _ ts) = freeTypeVars ts+-- -- freeTypeVars (TRow r) = freeTypeVars r++-- mapVarNames = mapVarNames'+-- -- mapVarNames f (TBody t) = TBody $ mapVarNames f t+-- -- mapVarNames f (TCons n ts) = TCons n $ mapVarNames f ts+-- -- mapVarNames f (TRow r) = TRow $ mapVarNames f r++----------------------------------------------------------------------++type TSubst = Map.Map TVarName Type++nullSubst :: TSubst+nullSubst = Map.empty++-- | composeSubst should obey the law:+-- applySubst (composeSubst new old) t = applySubst new (applySubst old t)+-- >>> composeSubst (Map.fromList []) (Map.fromList [])+-- fromList []+-- >>> composeSubst (Map.fromList [(0,Fix (TBody (TVar 1)))]) (Map.fromList [])+-- fromList [(0,Fix (TBody (TVar 1)))]+-- >>> composeSubst (Map.fromList []) (Map.fromList [(0,Fix (TBody (TVar 1)))])+-- fromList [(0,Fix (TBody (TVar 1)))]+-- >>> composeSubst (Map.fromList [(1,Fix (TBody (TVar 2)))]) (Map.fromList [(0,Fix (TBody (TVar 1)))])+-- fromList [(0,Fix (TBody (TVar 2))),(1,Fix (TBody (TVar 2)))]+-- >>> composeSubst (Map.fromList [(0,Fix (TBody (TVar 1)))]) (Map.fromList [(1,Fix (TBody (TVar 2)))])+-- fromList [(0,Fix (TBody (TVar 2))),(1,Fix (TBody (TVar 2)))]+composeSubst :: TSubst -> TSubst -> TSubst+composeSubst new old = applySubst new old `Map.union` new++singletonSubst :: TVarName -> Type -> TSubst+singletonSubst = Map.singleton++#ifdef QUICKCHECK+prop_composeSubst :: TSubst -> TSubst -> Type -> Bool+prop_composeSubst new old t = applySubst (composeSubst new old) t == applySubst new (applySubst old t)+#endif++----------------------------------------------------------------------++class Substable a where+ applySubst :: TSubst -> a -> a++ applySubst' :: (Functor f, Substable a) => TSubst -> f a -> f a+ applySubst' s = fmap $ applySubst s++-- for convenience only:+instance Substable a => Substable (Maybe a) where+ applySubst = applySubst'+instance Substable a => Substable [a] where+ applySubst = applySubst'+instance Substable a => Substable (Map.Map b a) where+ applySubst = applySubst'+instance Substable b => Substable (a, b) where+ applySubst = applySubst'++instance (Ord a, Substable a) => Substable (Set.Set a) where+ applySubst s = Set.map (applySubst s)++----------------------------------------------------------------------++-- | applySubst for Types+-- >>> applySubst (Map.fromList [(0, Fix $ TBody TNumber)]) (Fix $ TBody $ TVar 0)+-- Fix (TBody TNumber)+-- >>> applySubst (Map.fromList [(0, Fix $ TRow $ TRowEnd Nothing)]) (Fix $ TBody $ TVar 0)+-- Fix (TRow (TRowEnd Nothing))+-- >>> applySubst (Map.fromList [(0, Fix $ TRow $ TRowEnd Nothing)]) (Fix $ TRow $ TRowEnd $ Just $ RowTVar 0)+-- Fix (TRow (TRowEnd Nothing))+-- >>> applySubst (Map.fromList [(0, Fix $ TRow $ TRowEnd Nothing)]) (Fix $ TRow $ TRowProp "bla" (schemeEmpty $ Fix $ TBody TString) (TRowEnd $ Just $ RowTVar 0))+-- Fix (TRow (TRowProp "bla" (TScheme {schemeVars = [], schemeType = TQual {qualPred = [], qualType = Fix (TBody TString)}}) (TRowEnd Nothing)))+instance Substable Type where+ applySubst :: TSubst -> Type -> Type+ applySubst s ft@(Fix t) =+ case t of+ TBody (TVar n) -> substT' n t+ TRow r -> Fix $ TRow $ applySubst s r+ _ -> if ft `elem` Map.elems s+ then ft+ else Fix $ fmap (applySubst s) t+ where substT' n defaultT = fromMaybe (Fix defaultT) $ Map.lookup n s+ --traverse (fmap f) t+ --where f t@(TBody (TVar n)) = t --fromMaybe t $ Map.lookup n s+ -- f t = t+ -- applySubst s t@(TBody (TVar n)) = fromMaybe t $ Map.lookup n s+ -- applySubst _ t@(TBody _) = t+ -- applySubst s (TCons n ts) = TCons n (applySubst s ts)+ -- applySubst s (TRow r) = TRow $ applySubst s r++----------------------------------------------------------------------++sortRow :: TRowList t -> TRowList t+sortRow row = row -- TODO implement++data FlatRowEnd t = FlatRowEndTVar (Maybe RowTVar) | FlatRowEndRec TypeId [t]++flattenRow :: TRowList t -> (Map.Map EPropName (TScheme t), FlatRowEnd t)+flattenRow = flattenRow' (Map.empty, FlatRowEndTVar Nothing)+ where flattenRow' :: (Map.Map EPropName (TScheme t), FlatRowEnd t) -> TRowList t -> (Map.Map EPropName (TScheme t), FlatRowEnd t)+ flattenRow' (m,r) (TRowProp n t rest) = flattenRow' (Map.insert n t m, r) rest+ flattenRow' (m,_) (TRowEnd r') = (m, FlatRowEndTVar r')+ flattenRow' (m,_) (TRowRec tid ts) = (m, FlatRowEndRec tid ts)++unflattenRow :: Map.Map EPropName (TScheme t) -> FlatRowEnd t -> (EPropName -> Bool) -> TRowList t+unflattenRow m r f = Map.foldrWithKey (\n t l -> if f n then TRowProp n t l else l) rend m+ where rend = case r of+ FlatRowEndTVar r' -> TRowEnd r'+ FlatRowEndRec tid ts -> TRowRec tid ts++instance Substable (TRowList Type) where+ applySubst s (TRowProp propName propType rest) = sortRow $ TRowProp propName (applySubst s propType) (applySubst s rest)+ applySubst s t@(TRowEnd (Just (RowTVar tvarName))) =+ case Map.lookup tvarName s of+ Nothing -> t+ Just (Fix (TRow tRowList)) -> tRowList+ Just (Fix (TCons (TName tid) ts)) -> TRowRec tid ts+ Just (Fix (TBody (TVar n))) -> TRowEnd $ Just $ RowTVar n+ Just t' -> error $ "Cannot subst row variable into non-row: " ++ show t'+ applySubst _ (TRowEnd Nothing) = TRowEnd Nothing+ applySubst s (TRowRec tid ts) = TRowRec tid $ applySubst s ts++----------------------------------------------------------------------+newtype ClassName = ClassName String+ deriving (Show, Eq, Ord)++data Class t = Class { --classSupers :: [ClassName],+ classInstances :: [TScheme t] }+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++data TPred t = TPredIsIn { predClass :: ClassName, predType :: t }+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++data TQual t = TQual { qualPred :: [TPred t], qualType :: t }+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++qualEmpty :: t -> TQual t+qualEmpty = TQual []++type QualType = TQual Type++data TScheme t = TScheme { schemeVars :: [TVarName]+ , schemeType :: TQual t }+ deriving (Show, Eq, Ord, Functor, Foldable, Traversable)++schemeEmpty :: t -> TScheme t+schemeEmpty t = TScheme [] $ qualEmpty t++schemeFromQual :: TQual t -> TScheme t+schemeFromQual = TScheme []++type TypeScheme = TScheme Type++instance VarNames t => VarNames (TQual t) where+ freeTypeVars (TQual p t) = freeTypeVars p `Set.union` freeTypeVars t+ mapVarNames f (TQual p t) = TQual (mapVarNames f p) (mapVarNames f t)++-- | Substable instance for TQual+-- >>> let qt = TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody (TVar 0))] (Fix $ TBody (TVar 0))+-- >>> let s = singletonSubst 0 (Fix $ TBody TNumber)+-- >>> applySubst s qt+-- TQual {qualPred = [TPredIsIn {predClass = ClassName "Bla", predType = Fix (TBody TNumber)}], qualType = Fix (TBody TNumber)}+instance (Substable t, VarNames t) => Substable (TQual t) where+ applySubst s (TQual preds t) = TQual (applySubst s preds) (applySubst s t)++instance VarNames t => VarNames (TPred t) where+ freeTypeVars (TPredIsIn _ t) = freeTypeVars t+ mapVarNames f (TPredIsIn n t) = TPredIsIn n $ mapVarNames f t++instance Substable t => Substable (TPred t) where+ applySubst s (TPredIsIn n t) = TPredIsIn n $ applySubst s t++-- | VarNames instance for TScheme+-- >>> let sc v t = TScheme v (qualEmpty t)+-- >>> freeTypeVars $ sc [0, 1] (Fix $ TBody $ TVar 2)+-- fromList [2]+-- >>> freeTypeVars $ sc [0, 1] (Fix $ TBody $ TVar 1)+-- fromList []+-- >>> freeTypeVars $ sc [0] (Fix $ TBody $ TVar 1)+-- fromList [1]+-- >>> freeTypeVars $ sc [0] (Fix $ TBody $ TVar 0)+-- fromList []+-- >>> freeTypeVars $ schemeEmpty (Fix $ TBody $ TVar 1)+-- fromList [1]+-- >>> freeTypeVars $ schemeEmpty (Fix $ TBody $ TNumber)+-- fromList []+-- >>> freeTypeVars $ sc [1] (Fix $ TBody $ TNumber)+-- fromList []+-- >>> freeTypeVars $ TScheme [0, 1] (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody $ TVar 0)] (Fix $ TBody $ TVar 0))+-- fromList []+-- >>> freeTypeVars $ TScheme [0, 1] (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody $ TVar 0)] (Fix $ TBody $ TVar 2))+-- fromList [2]+-- >>> freeTypeVars $ TScheme [0, 1] (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody $ TVar 2)] (Fix $ TBody $ TVar 2))+-- fromList [2]+-- >>> freeTypeVars $ TScheme [0, 1] (TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody $ TVar 2)] (Fix $ TBody $ TVar 0))+-- fromList [2]+instance VarNames t => VarNames (TScheme t) where+ freeTypeVars (TScheme qvars t) = freeTypeVars t `Set.difference` Set.fromList qvars+ mapVarNames f (TScheme qvars t) = TScheme (map f qvars) (mapVarNames f t)++instance (VarNames t, Substable t) => Substable (TScheme t) where+ applySubst = schemeForceApplySubst++-- | Substitution on TScheme that doesn't touch quantified variables+-- Useful for normal substitution+schemeQApplySubst :: (VarNames t, Substable t) => TSubst -> TScheme t -> TScheme t+schemeQApplySubst s (TScheme qvars t) = TScheme qvars $ applySubst (foldr Map.delete s qvars) t++-- | Substitution on TScheme that *does* replace even quantified variables+-- Useful for un-generalizing mutable variables+schemeForceApplySubst :: (VarNames t, Substable t) => TSubst -> TScheme t -> TScheme t+schemeForceApplySubst s (TScheme qvars t) = TScheme qvars' t'+ where qvars' = Set.toList $ Set.fromList qvars `Set.intersection` freeTypeVars t'+ t' = applySubst s t+++newtype VarId = VarId Int+ deriving (Show, Eq, Ord)++-- | Type environment: maps AST variables (not type variables!) to quantified type schemes.+--+-- Note: instance of Substable+type TypeEnv = Map.Map EVarName VarId++-- Used internally to generate fresh type variable names+data NameSource = NameSource { lastName :: TVarName }+ deriving (Show, Eq)+++data InferState = InferState { nameSource :: NameSource+ , mainSubst :: TSubst+ -- must be stateful because we sometimes discover that a variable is mutable.+ , varSchemes :: Map.Map VarId TypeScheme+ , varInstances :: Graph.Gr QualType ()+ , namedTypes :: Map.Map TypeId (Type, TypeScheme)+ , classes :: Map.Map ClassName (Class Type)+ , pendingUni :: Set.Set (Source, Type, (ClassName, Set.Set TypeScheme))+ }+ deriving (Show, Eq)+++-- | VarNames instance for InferState+-- >>> :{+-- varInstances+-- $ mapVarNames (\k -> k + 1)+-- $ emptyInferState { varInstances = Map.fromList [ (0, Set.fromList [ qualEmpty $ Fix $ TBody $ TVar 0, qualEmpty $ Fix $ TBody $ TVar 1])+-- , (1, Set.fromList [ qualEmpty $ Fix $ TBody $ TVar 0+-- , TQual [TPredIsIn (ClassName "Bla") (Fix $ TBody $ TVar 3)] (Fix $ TBody $ TVar 1)+-- ])+-- ]}+-- :}+-- fromList [(1,fromList [TQual {qualPred = [], qualType = Fix (TBody (TVar 1))},TQual {qualPred = [], qualType = Fix (TBody (TVar 2))}]),(2,fromList [TQual {qualPred = [], qualType = Fix (TBody (TVar 1))},TQual {qualPred = [TPredIsIn {predClass = ClassName "Bla", predType = Fix (TBody (TVar 4))}], qualType = Fix (TBody (TVar 2))}])]+instance VarNames InferState where+ freeTypeVars = freeTypeVars . varSchemes+ mapVarNames f is = is { varSchemes = mapVarNames f $ varSchemes is+ , varInstances = Graph.nmap (mapVarNames f) $ varInstances is+ }++instance Substable InferState where+ applySubst s is = is { varSchemes = applySubst s (varSchemes is)+ , mainSubst = s `composeSubst` mainSubst is+ , varInstances = Graph.nmap (applySubst s) $ varInstances is+ }+ +-- | Adds a pair of equivalent items to an equivalence map.+-- >>> import Infernu.Pretty+-- >>> let m1 = addEquivalence 1 2 Map.empty+-- >>> pretty m1+-- "Map (b => Set {b, c}, c => Set {b, c})"+-- >>> pretty $ addEquivalence 1 3 m1+-- "Map (b => Set {b, c, d}, c => Set {b, c, d}, d => Set {b, c, d})"+-- >>> pretty $ addEquivalence 3 1 m1+-- "Map (b => Set {b, c, d}, c => Set {b, c, d}, d => Set {b, c, d})"+-- >>> pretty $ addEquivalence 4 5 m1+-- "Map (b => Set {b, c}, c => Set {b, c}, e => Set {e, f}, f => Set {e, f})"+-- >>> pretty $ addEquivalence 1 4 $ addEquivalence 4 5 m1+-- "Map (b => Set {b, c, e, f}, c => Set {b, c, e, f}, e => Set {b, c, e, f}, f => Set {b, c, e, f})"+addEquivalence :: TVarName -> TVarName -> Graph.Gr QualType () -> Graph.Gr QualType ()+addEquivalence x y gr = Graph.insEdge (x,y,()) . insTVar x . insTVar y $ gr+ where insTVar tv g = if Graph.gelem tv g+ then g+ else Graph.insNode (tv, qualEmpty $ Fix . TBody $ TVar tv) g+++----------------------------------------------------------------------+-- TODO: Horrible, terrible boilerplate. get rid of it.+mapTopAnnotation :: (a -> a) -> Exp a -> Exp a+mapTopAnnotation f expr =+ case expr of+ (EVar a b) -> EVar (f a) b+ (EApp a x y) -> EApp (f a) x y+ (EAbs a x y) -> EAbs (f a) x y+ (ELet a x y z) -> ELet (f a) x y z+ (ELit a x) -> ELit (f a) x+ (EAssign a x y z) -> EAssign (f a) x y z+ (EPropAssign a x y z v) -> EPropAssign (f a) x y z v+ (EIndexAssign a x y z v) -> EIndexAssign (f a) x y z v+ (EArray a x) -> EArray (f a) x+ (ETuple a x) -> ETuple (f a) x+ (ERow a x y) -> ERow (f a) x y+ (EStringMap a x) -> EStringMap (f a) x+ (ECase a x ys) -> ECase (f a) x ys+ (EProp a x y) -> EProp (f a) x y+ (EIndex a x y) -> EIndex (f a) x y+ (ENew a x y) -> ENew (f a) x y++----------------------------------------------------------------------++#ifdef QUICKCHECK+-- Test runner+return []++instance (Ord k, Arbitrary k, Arbitrary v) => Arbitrary (Map k v) where+ arbitrary = Map.fromList <$> resize 2 arbitrary+ shrink m = map (flip Map.delete m) (Map.keys m)++$( derive makeArbitrary ''TypeId )+$( derive makeArbitrary ''RowTVar )+$( derive makeArbitrary ''TRowList )+$( derive makeArbitrary ''TConsName )+$( derive makeArbitrary ''TBody )+$( derive makeArbitrary ''FType )++instance Arbitrary (Fix FType) where+ arbitrary = Fix <$> arbitrary+++{-# WARNING runAllTests "QuickCheck runner, do not use!" #-}+runAllTests :: IO Bool+runAllTests = $(quickCheckAll)++#endif
+ src/Infernu/Unify.hs view
@@ -0,0 +1,481 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE TupleSections #-}++module Infernu.Unify+ (unify, unifyAll, unifyl, unifyRowPropertyBiased, unifyPredsL, unifyPending)+ where+++import Control.Monad (forM, forM_, when, unless)+import Data.List (intercalate)++import Data.Either (rights)+import Data.Map.Lazy (Map)+import qualified Data.Map.Lazy as Map+import Data.Maybe (catMaybes, mapMaybe)++import Data.Set (Set)+import qualified Data.Set as Set++import Infernu.Builtins.Array (arrayRowType)+import Infernu.Builtins.Regex (regexRowType)+import Infernu.Builtins.String (stringRowType)+import Infernu.Decycle+import Infernu.InferState+import Infernu.Lib (matchZip)+import Infernu.Log+import Infernu.Pretty+import Infernu.Types+++----------------------------------------------------------------------++tryMakeRow :: FType Type -> Infer (Maybe (TRowList Type))+tryMakeRow (TCons TArray [t]) = Just <$> arrayRowType t+tryMakeRow (TBody TRegex) = Just <$> regexRowType+tryMakeRow (TBody TString) = Just <$> stringRowType+tryMakeRow _ = return Nothing++----------------------------------------------------------------------+++type UnifyF = Source -> Type -> Type -> Infer ()++unify :: UnifyF+unify = decycledUnify++-- | Unifies given types, using the namedTypes from the infer state+-- >>> let p = emptySource+-- >>> let u x y = runInfer $ unify p x y >> getMainSubst+-- >>> let du x y = unify p x y >> getMainSubst+-- >>> let fromRight (Right x) = x+--+-- >>> u (Fix $ TBody $ TVar 0) (Fix $ TBody $ TVar 1)+-- Right (fromList [(0,Fix (TBody (TVar 1)))])+-- >>> u (Fix $ TBody $ TVar 1) (Fix $ TBody $ TVar 0)+-- Right (fromList [(1,Fix (TBody (TVar 0)))])+--+-- >>> u (Fix $ TBody $ TNumber) (Fix $ TBody $ TVar 0)+-- Right (fromList [(0,Fix (TBody TNumber))])+-- >>> u (Fix $ TBody $ TVar 0) (Fix $ TBody $ TNumber)+-- Right (fromList [(0,Fix (TBody TNumber))])+--+-- >>> u (Fix $ TBody $ TVar 0) (Fix $ TRow $ TRowEnd $ Just $ RowTVar 1)+-- Right (fromList [(0,Fix (TRow (TRowEnd (Just (RowTVar 1)))))])+--+-- >>> u (Fix $ TBody $ TVar 0) (Fix $ TRow $ TRowProp "x" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd $ Just $ RowTVar 1))+-- Right (fromList [(0,Fix (TRow (TRowProp "x" (TScheme {schemeVars = [], schemeType = TQual {qualPred = [], qualType = Fix (TBody TNumber)}}) (TRowEnd (Just (RowTVar 1))))))])+--+-- >>> let row1 z = (Fix $ TRow $ TRowProp "x" (schemeEmpty $ Fix $ TBody TNumber) (TRowEnd z))+-- >>> let sCloseRow = fromRight $ u (row1 $ Just $ RowTVar 1) (row1 Nothing)+-- >>> pretty $ applySubst sCloseRow (row1 $ Just $ RowTVar 1)+-- "{x: Number}"+--+-- Simple recursive type:+--+-- >>> let tvar0 = Fix $ TBody $ TVar 0+-- >>> let tvar3 = Fix $ TBody $ TVar 3+-- >>> let recRow = Fix $ TRow $ TRowProp "x" (schemeEmpty tvar0) $ TRowProp "y" (schemeEmpty tvar3) (TRowEnd $ Just $ RowTVar 2)+-- >>> let s = fromRight $ u tvar0 recRow+-- >>> s+-- fromList [(0,Fix (TCons (TName (TypeId 1)) [Fix (TBody (TVar 2)),Fix (TBody (TVar 3))]))]+-- >>> applySubst s tvar0+-- Fix (TCons (TName (TypeId 1)) [Fix (TBody (TVar 2)),Fix (TBody (TVar 3))])+--+-- >>> :{+-- pretty $ runInfer $ do+-- s <- du tvar0 recRow+-- let (Fix (TCons (TName n1) targs1)) = applySubst s tvar0+-- t <- unrollName p n1 targs1+-- return t+-- :}+-- "{x: <Named Type: mu 'B'. c d>, y: d, ..c}"+--+-- Unifying a rolled recursive type with its (unequal) unrolling should yield a null subst:+--+-- >>> :{+-- runInfer $ do+-- s <- du tvar0 recRow+-- let rolledT = applySubst s tvar0+-- let (Fix (TCons (TName n1) targs1)) = rolledT+-- unrolledT <- unrollName p n1 targs1+-- du rolledT unrolledT+-- return (rolledT == unrolledT)+-- :}+-- Right False+--+-- >>> :{+-- pretty $ runInfer $ do+-- du tvar0 recRow+-- let tvar4 = Fix . TBody . TVar $ 4+-- tvar5 = Fix . TBody . TVar $ 5+-- s2 <- du recRow (Fix $ TRow $ TRowProp "x" (schemeEmpty tvar4) $ TRowProp "y" (schemeEmpty tvar5) (TRowEnd Nothing))+-- return $ applySubst s2 recRow+-- :}+-- "{x: <Named Type: mu 'B'. {} f>, y: f}"+--+-- >>> let rec2 = Fix $ TCons TFunc [recRow, Fix $ TBody TNumber]+-- >>> :{+-- pretty $ runInfer $ do+-- s1 <- du tvar0 rec2+-- return $ applySubst s1 $ qualEmpty rec2+-- :}+-- "(this: {x: <Named Type: mu 'B'. c d>, y: d, ..c} -> TNumber)"+--+-- >>> :{+-- runInfer $ do+-- s1 <- du tvar0 rec2+-- s2 <- du tvar0 rec2+-- return $ (applySubst s1 (qualEmpty rec2) == applySubst s2 (qualEmpty rec2))+-- :}+-- Right True+--+--+-- Test generalization/instantiation of recursive types+--+-- >>> :{+-- pretty $ runInfer $ do+-- s1 <- du tvar0 rec2+-- generalize (ELit "bla" LitUndefined) Map.empty $ applySubst s1 $ qualEmpty rec2+-- :}+-- "forall c d. (this: {x: <Named Type: mu 'B'. c d>, y: d, ..c} -> TNumber)"+--+-- >>> :{+-- putStrLn $ fromRight $ runInfer $ do+-- s1 <- du tvar0 rec2+-- tscheme <- generalize (ELit "bla" LitUndefined) Map.empty $ applySubst s1 $ qualEmpty rec2+-- Control.Monad.forM_ [1,2..10] $ const fresh+-- t1 <- instantiate tscheme+-- t2 <- instantiate tscheme+-- unrolledT1 <- unrollName p (TypeId 1) [Fix $ TRow $ TRowEnd Nothing]+-- return $ concat $ Data.List.intersperse "\n"+-- [ pretty tscheme+-- , pretty t1+-- , pretty t2+-- , pretty unrolledT1+-- ]+-- :}+-- forall c d. (this: {x: <Named Type: mu 'B'. c d>, y: d, ..c} -> TNumber)+-- (this: {x: <Named Type: mu 'B'. m n>, y: n, ..m} -> TNumber)+-- (this: {x: <Named Type: mu 'B'. o p>, y: p, ..o} -> TNumber)+-- (this: {x: <Named Type: mu 'B'. {} d>, y: d} -> TNumber)+--+--+decycledUnify :: UnifyF+decycledUnify = decycle3 unify''++unlessEq :: (Monad m, Eq a) => a -> a -> m () -> m ()+unlessEq x y = unless (x == y)++mkTypeErrorMessage :: Pretty a => a -> a -> Maybe TypeError -> [Char]+mkTypeErrorMessage t1 t2 mte =+ concat [ "\n"+ , " Failed unifying: "+ , prettyTab 6 t1+ , "\n"+ , " With: "+ , prettyTab 6 t2+ , case mte of+ Nothing -> ""+ -- " With: "+ Just te -> "\n Because: " ++ prettyTab 2 (message te)+ ]+ +unify'' :: Maybe UnifyF -> UnifyF+unify'' Nothing _ t1 t2 = traceLog $ "breaking infinite recursion cycle, when unifying: " ++ pretty t1 ++ " ~ " ++ pretty t2+unify'' (Just recurse) a t1 t2 =+ do traceLog $ "unifying: " ++ pretty t1 ++ " ~ " ++ pretty t2+ s <- getMainSubst+ let t1' = unFix $ applySubst s t1+ t2' = unFix $ applySubst s t2+ traceLog $ "unifying (substed): " ++ pretty t1 ++ " ~ " ++ pretty t2+ let wrap' te = TypeError { source = source te,+ message = mkTypeErrorMessage t1 t2 (Just te)+ }+ mapError wrap' $ unify' recurse a t1' t2'++unificationError :: (VarNames x, Pretty x) => Source -> x -> x -> Infer b+unificationError pos x y = throwError pos $ mkTypeErrorMessage a b Nothing+ where [a, b] = minifyVars [x, y]++assertNoPred :: QualType -> Infer Type+assertNoPred q =+ do unless (null $ qualPred q) $ fail $ "Assertion failed: pred in " ++ pretty q+ return $ qualType q++-- | Main unification function+unify' :: UnifyF -> Source -> FType (Fix FType) -> FType (Fix FType) -> Infer ()++-- | Type variables+unify' _ a (TBody (TVar n)) t = varBind a n (Fix t)+unify' _ a t (TBody (TVar n)) = varBind a n (Fix t)++-- | undefined+unify' _ _ (TBody TUndefined) _ = return () -- TODO verify this is ok. undefined being treated as "bottom" type here.++-- | Two simple types+unify' _ a (TBody x) (TBody y) = unlessEq x y $ unificationError a x y++-- | Two recursive types+unify' recurse a t1@(TCons (TName n1) targs1) t2@(TCons (TName n2) targs2) =+ if n1 == n2+ then case matchZip targs1 targs2 of+ Nothing -> unificationError a t1 t2+ Just targs -> unifyl recurse a targs+ else+ do let unroll' = unrollName a+ t1' <- unroll' n1 targs1+ t2' <- unroll' n2 targs2+ -- TODO don't ignore qual preds...+ mapM_ assertNoPred [t1', t2']+ recurse a (qualType t1') (qualType t2')++-- | A recursive type and another type+unify' recurse a (TCons (TName n1) targs1) t2 =+ unrollName a n1 targs1+ >>= assertNoPred+ >>= flip (recurse a) (Fix t2)+unify' recurse a t1 (TCons (TName n2) targs2) =+ unrollName a n2 targs2+ >>= assertNoPred+ >>= recurse a (Fix t1)++-- | A type constructor vs. a simple type+unify' _ a t1@(TBody _) t2@(TCons _ _) = unificationError a t1 t2+unify' _ a t1@(TCons _ _) t2@(TBody _) = unificationError a t1 t2+ +-- | A function vs. a simple type+unify' _ a t1@(TBody _) t2@(TFunc _ _) = unificationError a t1 t2+unify' _ a t1@(TFunc _ _) t2@(TBody _) = unificationError a t1 t2++-- | A function vs. a type constructor +unify' _ a t1@(TFunc _ _) t2@(TCons _ _) = unificationError a t1 t2+unify' _ a t1@(TCons _ _) t2@(TFunc _ _) = unificationError a t1 t2++-- | Two type constructors+unify' recurse a t1@(TCons n1 ts1) t2@(TCons n2 ts2) =+ do when (n1 /= n2) $ unificationError a t1 t2+ case matchZip ts1 ts2 of+ Nothing -> unificationError a t1 t2+ Just ts -> unifyl recurse a ts++-- | Two functions+-- TODO: handle func return type (contravariance) by swapping the unify rhs/lhs for the last TCons TFunc targ+unify' recurse a t1@(TFunc ts1 tres1) t2@(TFunc ts2 tres2) =+ case matchZip ts1 ts2 of+ Nothing -> unificationError a t1 t2+ Just ts -> do unifyl recurse a ts+ recurse a tres2 tres1+ +-- | Type constructor vs. row type+unify' r a (TRow tRowList) t2@(TCons _ _) = unifyTryMakeRow r a True tRowList t2+unify' r a t1@(TCons _ _) (TRow tRowList) = unifyTryMakeRow r a False tRowList t1+unify' r a (TRow tRowList) t2@(TBody _) = unifyTryMakeRow r a True tRowList t2+unify' r a t1@(TBody _) (TRow tRowList) = unifyTryMakeRow r a False tRowList t1+unify' r a (TRow tRowList) t2@(TFunc _ _) = unifyTryMakeRow r a True tRowList t2+unify' r a t1@(TFunc _ _) (TRow tRowList) = unifyTryMakeRow r a False tRowList t1+++-- | Two row types+-- TODO: un-hackify!+unify' recurse a t1@(TRow row1) t2@(TRow row2) =+ unlessEq t1 t2 $ do+ let (m2, r2) = flattenRow row2+ names2 = Set.fromList $ Map.keys m2+ (m1, r1) = flattenRow row1+ names1 = Set.fromList $ Map.keys m1+ commonNames = Set.toList $ names1 `Set.intersection` names2++ --namesToTypes :: Map EPropName (TScheme t) -> [EPropName] -> [t]+ -- TODO: This ignores quantified variables in the schemes.+ -- It should be AT LEAST alpha-equivalence below (in the unifyl)+ namesToTypes m = mapMaybe $ flip Map.lookup m++ --commonTypes :: [(Type, Type)]+ commonTypes = zip (namesToTypes m1 commonNames) (namesToTypes m2 commonNames)++ forM_ commonTypes $ \(ts1, ts2) -> unifyRowPropertyBiased' recurse a (unificationError a ts1 ts2) (ts1, ts2)+ r <- RowTVar <$> fresh+ unifyRows recurse a r (t1, names1, m1) (t2, names2, r2)+ unifyRows recurse a r (t2, names2, m2) (t1, names1, r1)+++unifyTryMakeRow :: UnifyF -> Source -> Bool -> TRowList Type -> FType Type -> Infer ()+unifyTryMakeRow r a leftBiased tRowList t2 =+ do let tRow = TRow tRowList+ res <- tryMakeRow t2+ case res of+ Nothing -> unificationError a tRow t2+ Just rowType -> if leftBiased+ then r a (Fix tRow) (Fix $ TRow rowType)+ else r a (Fix $ TRow rowType) (Fix tRow)+++unifyRowPropertyBiased :: Source -> Infer () -> (TypeScheme, TypeScheme) -> Infer ()+unifyRowPropertyBiased = unifyRowPropertyBiased' unify++-- | TODO: This hacky piece of code implements a simple 'subtyping' relation between+-- type schemes. The logic is that if the LHS type is "more specific" than we allow+-- unifying with the RHS. Instead of actually checking properly for subtyping+-- (including co/contra variance, etc.) we allow normal unification in two cases,+-- and fail all others:+--+-- 1. If the LHS is not quanitified at all+-- 2. If the LHS is a function type quantified only on the type of 'this'+--+unifyRowPropertyBiased' :: UnifyF -> Source -> Infer () -> (TypeScheme, TypeScheme) -> Infer ()+unifyRowPropertyBiased' recurse a errorAction (scheme1s, scheme2s) =+ do traceLog ("Unifying type schemes: " ++ pretty scheme1s ++ " ~ " ++ pretty scheme2s)+ let crap = Fix $ TBody TUndefined+ unifySchemes' = do traceLog ("Unifying schemes: " ++ pretty scheme1s ++ " ~~ " ++ pretty scheme2s)+ scheme1T <- instantiate scheme1s+ scheme2T <- instantiate scheme2s+ -- TODO unify predicates properly (review this) - specificaly (==)+ -- should prevent cycles!+ --Pred.unify (unify a) (qualPred scheme1) (qualPred scheme2)+ -- TODO do something with pred'+ unifyPredsL a $ (qualPred scheme1T) ++ (qualPred scheme2T)+ recurse a (qualType scheme1T) (qualType scheme2T)+ isSimpleScheme =+ -- TODO: note we are left-biased here - assuming that t1 is the 'target', can be more specific than t2+ case scheme1s of+ TScheme [] _ -> True+ _ -> False+ -- TODO should do biased type scheme unification here+ unless (areEquivalentNamedTypes (crap, scheme1s) (crap, scheme2s))+ $ if isSimpleScheme || (length (schemeVars scheme1s) == length (schemeVars scheme2s)) -- isSimpleScheme+ then unifySchemes'+ else errorAction++unifyRows :: (VarNames x, Pretty x) => UnifyF -> Source -> RowTVar+ -> (x, Set EPropName, Map EPropName TypeScheme)+ -> (x, Set EPropName, FlatRowEnd Type)+ -> Infer ()+unifyRows recurse a r (t1, names1, m1) (t2, names2, r2) =+ do let in1NotIn2 = names1 `Set.difference` names2+ rowTail = case r2 of+ FlatRowEndTVar (Just _) -> FlatRowEndTVar $ Just r+ _ -> r2+-- fmap (const r) r2+ in1NotIn2row = tracePretty "in1NotIn2row" $ Fix . TRow . unflattenRow m1 rowTail $ flip Set.member in1NotIn2++ case r2 of+ FlatRowEndTVar Nothing -> if Set.null in1NotIn2+ then varBind a (getRowTVar r) (Fix $ TRow $ TRowEnd Nothing)+ else unificationError a t1 t2+ FlatRowEndTVar (Just r2') -> recurse a in1NotIn2row (Fix . TBody . TVar $ getRowTVar r2')+ FlatRowEndRec tid ts -> recurse a in1NotIn2row (Fix $ TCons (TName tid) ts)++-- | Unifies pairs of types, accumulating the substs+unifyl :: UnifyF -> Source -> [(Type, Type)] -> Infer ()+unifyl r a = mapM_ $ uncurry $ r a++-- | Checks if a type var name appears as a free type variable nested somewhere inside a row type.+--+-- >>> getSingleton $ isInsideRowType 0 (Fix (TBody $ TVar 0))+-- Nothing+-- >>> getSingleton $ isInsideRowType 0 (Fix (TRow $ TRowEnd (Just $ RowTVar 0)))+-- Just Fix (TRow (TRowEnd (Just (RowTVar 0))))+-- >>> getSingleton $ isInsideRowType 0 (Fix (TRow $ TRowEnd (Just $ RowTVar 1)))+-- Nothing+-- >>> getSingleton $ isInsideRowType 0 (Fix (TFunc [Fix $ TBody $ TVar 0] (Fix $ TRow $ TRowEnd (Just $ RowTVar 1))))+-- Nothing+-- >>> getSingleton $ isInsideRowType 0 (Fix (TFunc [Fix $ TBody $ TVar 1] (Fix $ TRow $ TRowEnd (Just $ RowTVar 0))))+-- Just Fix (TRow (TRowEnd (Just (RowTVar 0))))+isInsideRowType :: TVarName -> Type -> Set Type+isInsideRowType n (Fix t) =+ case t of+ TRow t' -> if n `Set.member` freeTypeVars t'+ then Set.singleton $ Fix t+ else Set.empty+ _ -> foldr (\x l -> isInsideRowType n x `Set.union` l) Set.empty t+-- _ -> unOrBool $ fst (traverse (\x -> (OrBool $ isInsideRowType n x, x)) t)++getSingleton :: Set a -> Maybe a+getSingleton s = case foldr (:) [] s of+ [x] -> Just x+ _ -> Nothing++varBind :: Source -> TVarName -> Type -> Infer ()+varBind a n t =+ do s <- varBind' a n t+ applySubstInfer s++varBind' :: Source -> TVarName -> Type -> Infer TSubst+varBind' a n t | t == Fix (TBody (TVar n)) = return nullSubst+ | Just rowT <- getSingleton $ isInsideRowType n t =+ do traceLog ("===> Generalizing mu-type: " ++ pretty n ++ " recursive in: " ++ pretty t ++ ", found enclosing row type: " ++ " = " ++ pretty rowT)+ recVar <- fresh+ let withRecVar = replaceFix (unFix rowT) (TBody (TVar recVar)) t+ recT = replaceFix (TBody (TVar n)) (unFix withRecVar) rowT+ namedType <- getNamedType recVar recT+ -- let (TCons (TName n1) targs1) = unFix namedType+ -- t' <- unrollName a n1 targs1+ traceLog $ "===> Resulting mu type: " ++ pretty n ++ " = " ++ pretty withRecVar+ return $ singletonSubst recVar namedType `composeSubst` singletonSubst n withRecVar+ | n `Set.member` freeTypeVars t = let f = minifyVarsFunc t+ in throwError a $ "Occurs check failed: " ++ pretty (f n) ++ " in " ++ pretty (mapVarNames f t)+ | otherwise = return $ singletonSubst n t++unifyAll :: Source -> [Type] -> Infer ()+unifyAll a ts = unifyl decycledUnify a $ zip ts (drop 1 ts)+++unifyPredsL :: Source -> [TPred Type] -> Infer [TPred Type]+unifyPredsL a ps = catMaybes <$>+ do forM ps $ \p@(TPredIsIn className t) ->+ do entry <- ((a,t,) . (className,) . Set.fromList . classInstances) <$> lookupClass className+ `failWithM` throwError a ("Unknown class: " ++ pretty className ++ " in pred list: " ++ pretty ps)+ remainingAmbiguities <- unifyAmbiguousEntry entry+ case remainingAmbiguities of+ Nothing -> return Nothing+ Just ambig ->+ do addPendingUnification ambig+ return $ Just p++isRight :: Either a b -> Bool+isRight (Right _) = True+isRight _ = False++catLefts :: [Either a b] -> [a]+catLefts [] = []+catLefts (Left a:xs) = a:(catLefts xs)+catLefts (Right _:xs) = catLefts xs+ +unifyAmbiguousEntry :: (Source, Type, (ClassName, Set TypeScheme)) -> Infer (Maybe (Source, Type, (ClassName, Set TypeScheme)))+unifyAmbiguousEntry (a, t, (ClassName className, tss)) = + do let unifAction ts =+ do inst <- instantiateScheme False ts >>= assertNoPred+ unify a inst t+ unifyResults <- forM (Set.toList tss) $ \instScheme -> (instScheme, ) <$> runSubInfer (unifAction instScheme >> getState)+ let survivors = filter (isRight . snd) unifyResults+ case rights $ map snd survivors of+ [] -> do t' <- applyMainSubst t+ throwError a $ concat [ intercalate "\n\n" $ "" : (map (prettyTab 2 . message) . catLefts $ map snd $ unifyResults)+ , "\n\n"+ , "While trying to find matching instance of typeclass "+ , "\n "+ , prettyTab 1 className+ , "\nfor type:\n "+ , prettyTab 1 t'+ ]+ [newState] -> setState newState >> return Nothing+ _ -> return . Just . (\x -> (a, t, (ClassName className, x))) . Set.fromList . map fst $ survivors++unifyPending :: Infer ()+unifyPending = getPendingUnifications >>= loop+ where loop pu =+ do newEntries <- forM (Set.toList pu) unifyAmbiguousEntry+ let pu' = Set.fromList $ catMaybes newEntries+ setPendingUnifications pu'+ when (pu' /= pu) $ loop pu'+ +-- do newEntries <- forM (Set.toList pu) $ \entry@((src, ts), t) ->+-- do t' <- applyMainSubst t+-- let unifAction = do inst <- instantiate ts >>= assertNoPred+-- inst' <- applyMainSubst inst+-- unify src inst' t'+-- result <- runSubInfer $ unifAction >> getState+++
+ src/Infernu/Util.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE CPP #-}+module Infernu.Util (checkFiles, annotatedSource, checkSource) where++import Control.Monad (forM, when)+import Data.Maybe (catMaybes)+import Data.List (intercalate)+import qualified Data.Set as Set+import qualified Language.ECMAScript3.Parser as ES3Parser+import qualified Language.ECMAScript3.PrettyPrint as ES3Pretty+import qualified Language.ECMAScript3.Syntax as ES3+import qualified Text.Parsec.Pos as Pos++import Infernu.Options (Options(..))+import Infernu.Parse (translate)+-- TODO move pretty stuff to Pretty module+import Infernu.Infer (getAnnotations, minifyVars, runTypeInference)+import Infernu.Pretty (pretty)+import Infernu.Types (GenInfo (..), QualType, Source (..), TypeError (..))++zipByPos :: [(Pos.SourcePos, String)] -> [(Int, String)] -> [String]+zipByPos [] xs = map snd xs+zipByPos _ [] = []+zipByPos ps'@((pos, s):ps) xs'@((i,x):xs) = if Pos.sourceLine pos == i+ then formattedAnnotation : zipByPos ps xs'+ else x : zipByPos ps' xs+ where indentToColumn n = replicate (n-1) ' '+ isMultiline = length sLines > 1+ sLines = lines s+ formattedAnnotation = if isMultiline+ then ("/*"+ ++ indentToColumn (Pos.sourceColumn pos - 2)+ ++ head sLines+ ++ "\n"+ ++ (intercalate "\n" . map (\l -> indentToColumn (Pos.sourceColumn pos) ++ l) $ tail sLines) ++ " */")+ else "//" ++ indentToColumn (Pos.sourceColumn pos - 2) ++ s+++indexList :: [a] -> [(Int, a)]+indexList = zip [1..]+++checkSource :: String -> Either TypeError [(Source, QualType)]+checkSource src = case ES3Parser.parseFromString src of+ Left parseError -> Left $ TypeError { source = Source (GenInfo True Nothing, Pos.initialPos "<global>"), message = show parseError }+ Right expr -> -- case ES3.isValid expr of+ -- False -> Left $ TypeError { source = Source (GenInfo True, Pos.initialPos "<global>"), message = "Invalid syntax" }+ -- True ->+ fmap getAnnotations $ fmap minifyVars $ runTypeInference $ fmap Source $ translate $ ES3.unJavaScript expr++checkFiles :: Options -> [String] -> IO (Either TypeError [(Source, QualType)])+checkFiles options fileNames = do+ expr <- concatMap ES3.unJavaScript <$> forM fileNames ES3Parser.parseFromFile+ when (optShowParsed options) $ putStrLn $ show $ ES3Pretty.prettyPrint expr+ let expr' = fmap Source $ translate $ expr+ when (optShowCore options) $ putStrLn $ pretty expr'+ let expr'' = fmap minifyVars $ runTypeInference expr'+ res = fmap getAnnotations expr''+ return res++annotatedSource :: [(Source, QualType)] -> [String] -> String+annotatedSource xs sourceCode = unlines $ zipByPos (prettyRes $ unGenInfo $ filterGen xs) indexedSource+ where indexedSource = indexList sourceCode+ unGenInfo :: [(Source, QualType)] -> [(String, Pos.SourcePos, QualType)]+ unGenInfo = catMaybes . map (\(Source (g, s), q) -> fmap (\n -> (n, s, q)) $ declName g)+ filterGen :: [(Source, QualType)] -> [(Source, QualType)]+ filterGen = filter (\(Source (g, _), _) -> not . isGen $ g)+ prettyRes = Set.toList . Set.fromList . fmap (\(n, s, q) -> (s, pretty n ++ " : " ++ pretty q))
+ test/Demo.hs view
@@ -0,0 +1,26 @@+module Demo where++import Data.Bool (bool)+import Data.List (intercalate)+import Infernu.Infer (pretty)+import Infernu.Util (checkFiles)+import Infernu.Options (defaultOptions)+import System.Environment (getArgs)++isRight :: Either a b -> Bool+isRight (Right _) = True+isRight _ = False++main :: IO ()+main = do+ args <- getArgs+ let [shouldPassS, fileName] = args+ res <- fmap last <$> checkFiles defaultOptions [fileName]+ let shouldPass = if shouldPassS == "y" then id else not+ typeChecked = isRight res+ message = case res of+ Left e -> pretty e+ Right _ -> ""+ toOk = bool "FAIL" "OK" . shouldPass+ --print $ fmap (pretty . snd) res+ putStrLn $ "// " ++ toOk typeChecked ++ " " ++ (intercalate " | " $ lines message)
+ test/Test.hs view
@@ -0,0 +1,11 @@+{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances #-}+module Test where++import Infernu.Types++main :: IO ()+main = do+ res <- runAllTests+ print res+ return ()+