diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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 diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -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 + diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -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 + + + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/infernu.cabal b/infernu.cabal new file mode 100644 --- /dev/null +++ b/infernu.cabal @@ -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 diff --git a/src/Infernu/Builtins/Array.hs b/src/Infernu/Builtins/Array.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Builtins/Array.hs @@ -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 diff --git a/src/Infernu/Builtins/Operators.hs b/src/Infernu/Builtins/Operators.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Builtins/Operators.hs @@ -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) + ] diff --git a/src/Infernu/Builtins/Regex.hs b/src/Infernu/Builtins/Regex.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Builtins/Regex.hs @@ -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 diff --git a/src/Infernu/Builtins/String.hs b/src/Infernu/Builtins/String.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Builtins/String.hs @@ -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 diff --git a/src/Infernu/Builtins/TypeClasses.hs b/src/Infernu/Builtins/TypeClasses.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Builtins/TypeClasses.hs @@ -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 + ]}) + ] diff --git a/src/Infernu/Decycle.hs b/src/Infernu/Decycle.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Decycle.hs @@ -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 diff --git a/src/Infernu/Fix.hs b/src/Infernu/Fix.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Fix.hs @@ -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) diff --git a/src/Infernu/Infer.hs b/src/Infernu/Infer.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Infer.hs @@ -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 + diff --git a/src/Infernu/InferState.hs b/src/Infernu/InferState.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/InferState.hs @@ -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 diff --git a/src/Infernu/Lib.hs b/src/Infernu/Lib.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Lib.hs @@ -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 + diff --git a/src/Infernu/Log.hs b/src/Infernu/Log.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Log.hs @@ -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` () + diff --git a/src/Infernu/Options.hs b/src/Infernu/Options.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Options.hs @@ -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...")) + + diff --git a/src/Infernu/Parse.hs b/src/Infernu/Parse.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Parse.hs @@ -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 (.method + -- (, ...)) by binding the object expression to '__obj__'. + -- So that we get: let __obj__ = 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 "" diff --git a/src/Infernu/Pretty.hs b/src/Infernu/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Pretty.hs @@ -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) diff --git a/src/Infernu/Types.hs b/src/Infernu/Types.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Types.hs @@ -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 diff --git a/src/Infernu/Unify.hs b/src/Infernu/Unify.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Unify.hs @@ -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: , 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: , 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: , 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: , 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: , y: d, ..c} -> TNumber) +-- (this: {x: , y: n, ..m} -> TNumber) +-- (this: {x: , y: p, ..o} -> TNumber) +-- (this: {x: , 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 + + + diff --git a/src/Infernu/Util.hs b/src/Infernu/Util.hs new file mode 100644 --- /dev/null +++ b/src/Infernu/Util.hs @@ -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 ""), message = show parseError } + Right expr -> -- case ES3.isValid expr of + -- False -> Left $ TypeError { source = Source (GenInfo True, Pos.initialPos ""), 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)) diff --git a/test/Demo.hs b/test/Demo.hs new file mode 100644 --- /dev/null +++ b/test/Demo.hs @@ -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) diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE TemplateHaskell, TypeSynonymInstances, FlexibleInstances #-} +module Test where + +import Infernu.Types + +main :: IO () +main = do + res <- runAllTests + print res + return () +