diff --git a/doc/TypePal/Collector/Collector.graffle b/doc/TypePal/Collector/Collector.graffle index 8d05279..dfaa1c0 100644 Binary files a/doc/TypePal/Collector/Collector.graffle and b/doc/TypePal/Collector/Collector.graffle differ diff --git a/doc/TypePal/Collector/Collector.md b/doc/TypePal/Collector/Collector.md index b3fd120..b5e6d94 100644 --- a/doc/TypePal/Collector/Collector.md +++ b/doc/TypePal/Collector/Collector.md @@ -19,8 +19,7 @@ to access and change its internal state. The global services provided by a `Coll * Maintain a single value per scope. This enables decoupling the collection of information from separate but related language constructs. Typical examples are: ** While collecting information from a function declaration: - create a new function scope and associate the required return type with it so - that return statements in the function body can check that + create a new function scope and associate the required return type with it so that return statements in the function body can check that (a) they occur inside a function; (b) that the type of their returned value is compatible with the required return type. ** While collecting information from an optionally labelled loop statement: @@ -46,14 +45,11 @@ Three dozen functions are available that fall into the following categories: * _Define_: define identifiers in various ways. * _Use_: use identifiers in various ways. * _Inference_: create new type variables for type inference. -* _Facts_: establish facts. +* _Facts_: establish or retrieve facts. * _Calculate_: define calculators. * _Require_: define requirements. -Technically, `Collector` is a datatype with a single constructur and a number of functions as fields, -For instance, given a `Collector` named `c`, calling the `define` function amounts to: `c.define(_the-arguments-of-define_)`. -All Collector functions are prefixed with `/* Collector field */` to emphasize that they -are a field of the Collector datatype. +Technically, `Collector` is a datatype with a single constructur and a number of functions as fields. For instance, given a `Collector` named `c`, calling the `define` function amounts to: `c.define(_the-arguments-of-define_)`. All Collector functions are prefixed with `/* Collector field */` to emphasize that they are a field of the Collector datatype. ##### LifeCycle of Collector A new `Collector` is created using the function `newCollector`. @@ -78,7 +74,7 @@ Finally, `run` creates the desired `TModel` that will be used by the ((Solver)): A typical scenario is (for a given a parse tree `pt` of the program to be checked): ```rascal -c = newCollector("my_model", pt); // create Collector +c = newCollector("my_model", pt); // create Collector, default TypePalConfig collect(pt, c); // collect constraints model = c.run(); // create initial TModel to be handled by the Solver ``` @@ -92,11 +88,13 @@ where: * `lc` is a syntactic type from the language under consideration. * `c` is a `Collector`. -IMPORTANT: Each `collect` function is responsible for collecting constraints from its subtrees. +::: Caution +Each `collect` function is responsible for collecting constraints from its subtrees. +::: ##### Configuration -The ((TypePal:Configuration)) can be retrieved or adjusted by the following two functions: +The [Configuration]((TypePal:Configuration)) can be retrieved or adjusted by the following two functions: ```rascal /* Collector field */ TypePalConfig () getConfig; /* Collector field */ void (TypePalConfig cfg) setConfig; @@ -109,12 +107,16 @@ Scope management amounts to entering a new scope, leave the current scope and re ```rascal /* Collector field */ void (Tree inner) enterScope; +/* Collector field */ void (list[Tree] trees) enterCompositeScope; +/* Collector field */ void (Tree inner) enterLubScope; +/* Collector field */ void (list[Tree] trees) enterCompositeLubScope; /* Collector field */ void (Tree inner) leaveScope; +/* Collector field */ void (list[Tree] trees) leaveCompositeScope; /* Collector field */ loc () getScope, ``` In order to check consistency, `leaveScope` has the inner scope that it is supposed to be leaving as argument. -Here is an example how the `let` expression in ((examples::fun)) handles subscopes: +Here is a simple example how the `let` expression in ((examples::fun)) handles subscopes: ```rascal void collect(current: (Expression) `let : = in end`, Collector c) { @@ -125,12 +127,14 @@ void collect(current: (Expression) `let : = ;`, Collector c){ ##### Nested Info -An arbitrary number of push down stacks can be maintained during the topdown traversal of the source code that is being type checked. -A use case is recording that a certain syntax type is encountered and make children aware of this, e.g. "we are inside a parameter list". +An arbitrary number of push down stacks can be maintained during the topdown traversal of the source code that is being type checked. A use case is recording that a certain syntax type is encountered and make children aware of this, e.g. "we are inside a parameter list". Each stack has a string name (`key`) and is created on demand. @@ -206,8 +209,13 @@ Each stack has a string name (`key`) and is created on demand. /* Collector field */ list[value] (str key) getStack, /* Collector field */ void (str key) clearStack, ``` -`push`, `pop`, and `top` perform standard stack operations. `push` creates a stack when needed, while `top` and `pop` require -the existence of the named stack. `getStack` returns all values in the named stack, while `clearStack` resets it to empty. +`push`, `pop`, and `top` perform standard stack operations. `push` creates a stack when needed, while `top` and `pop` require the existence of the named stack. `getStack` returns all values in the named stack, while `clearStack` resets it to empty. + +These stacks are stored in the global store, see [Solver](Solver:getStore). + +:::caution +With the availability of a global store come serious responsibilities. Don't overuse it, do not misuse it. +::: ##### Composition @@ -264,7 +272,7 @@ Similar to `addPathToDef` for the occurrence of a qualified names rather than a `occ` is a parse tree with has a certain type. The effect is to add a `pathRole` path between the current scope and the definition of that type. -A prime example is type checking of ((examples::pascal))'s `with` statement which _opens_ the definition +A prime example is type checking of [Pascal]((examples::pascal))'s `with` statement which _opens_ the definition of a record type and makes all defined fields available in the body of the `with` statement. Here we create a `withPath` between the scope of the with statement and all definitions of the record types of the given record variables: @@ -280,7 +288,9 @@ void collect(current: (WithStatement) `with <{RecordVariable ","}+ recordVars> d } ``` -##### Define +##### Define and Predefine + +###### Define The function `define` adds the definition of a name in the _current_ scope: ```rascal @@ -298,6 +308,19 @@ The function `defineInScope` adds the definition of a name in a _given_ scope: /* Collector field */ void (value scope, str id, IdRole idRole, value def, DefInfo info) defineInScope ``` +###### Predefine + +Most languages depend on predefined names such as `true`, `false`, `exp`, and the like. The function `predefine` adds the definition of such a predefined name in the _current_ scope: + +```rascal +/* Collector field */ void (str id, IdRole idRole, value def, DefInfo info) predefine; +``` + +The function `predefineInScope` adds the definition of a predefined name in a _given_ scope: +```rascal +/* Collector field */ void (value scope, str id, IdRole idRole, value def, DefInfo info) predefineInScope +``` + ##### Use ###### Use an unqualified name @@ -399,6 +422,8 @@ are available *but those may contain type variables*. The bindings that are accumulated during `calculateEager` or `requireEager` are effectuated upon successfull completion of that `calculateEager` or `requireEager`. +##### Fact and getType + ##### Fact The function `fact` registers known type information for a program fragment `src`: @@ -421,6 +446,11 @@ void collect(current: (Exp) `( )`, Collector c){ <1> Registers the fact that the current expression has type `intType`. <2> Registers the fact that the current expression has the same type as the embedded expression `e`. +###### GetType +The function `getType` returns the type of a program fragment `src` (when available) and throws the exception `TypeUnavailable` otherwise: +```rascal +/* Collector field */ void (Tree src) getType; +``` ##### Calculate A calculator computes the type of a subtree `src` by way of an AType-returning function `calculator`. diff --git a/doc/TypePal/Collector/Collector.png b/doc/TypePal/Collector/Collector.png index c2c214d..2936d0f 100644 Binary files a/doc/TypePal/Collector/Collector.png and b/doc/TypePal/Collector/Collector.png differ diff --git a/doc/TypePal/Configuration/TypePalConfig.graffle b/doc/TypePal/Configuration/TypePalConfig.graffle index 37aa3a8..a585705 100644 Binary files a/doc/TypePal/Configuration/TypePalConfig.graffle and b/doc/TypePal/Configuration/TypePalConfig.graffle differ diff --git a/doc/TypePal/Configuration/TypePalConfig.png b/doc/TypePal/Configuration/TypePalConfig.png index 64385f8..a5e95c1 100644 Binary files a/doc/TypePal/Configuration/TypePalConfig.png and b/doc/TypePal/Configuration/TypePalConfig.png differ diff --git a/doc/TypePal/PocketCalculator/PocketCalculator.md b/doc/TypePal/PocketCalculator/PocketCalculator.md index 196cb34..723724c 100644 --- a/doc/TypePal/PocketCalculator/PocketCalculator.md +++ b/doc/TypePal/PocketCalculator/PocketCalculator.md @@ -157,11 +157,13 @@ An expression consisting of a single identifier represents a _use_ of that ident - a matching define is found for one of the given roles: use and definition are connected to each other. - no matching define is found and an error is reported. -NOTE: In larger languages names may be defined in different scopes. Scopes do not play a role in Cal. +::: Note +In larger languages names may be defined in different scopes. Scopes do not play a role in Cal. +::: -NOTE: We do not enforce _define-before-use_ in this example, but see XXX how to achieve this. - -(((TODO:add reference for XXX))) +:::Note +We do not enforce _define-before-use_ in this example, but see [Configuration](Configuration:isAcceptableSimple) how to achieve this. +::: #### Check Exp: Boolean and Integer constants diff --git a/doc/TypePal/Solver/Solver.graffle b/doc/TypePal/Solver/Solver.graffle index 21b077d..aa34d24 100644 Binary files a/doc/TypePal/Solver/Solver.graffle and b/doc/TypePal/Solver/Solver.graffle differ diff --git a/doc/TypePal/Solver/Solver.md b/doc/TypePal/Solver/Solver.md index f8579a5..c5e6a94 100644 --- a/doc/TypePal/Solver/Solver.md +++ b/doc/TypePal/Solver/Solver.md @@ -8,14 +8,11 @@ A `Solver` tries to solve the constraints in a `TModel`; unsolved constraints pr #### Description -The purpose of a Solver is to solve the constraints that have been gathered by the ((Collector)) -and to produce a TModel. -The functions provided by a Solver are summarized below: +The purpose of a Solver is to solve the constraints that have been gathered by the [Collector]((Collector)) and to produce a TModel. The functions provided by a Solver are summarized below: ![]((Solver.png)) -Two dozen functions (some very similar to the ones provided for ((Collector))) are available -that fall into the following categories: +Two dozen functions (some very similar to the ones provided for [Collector]((Collector))) are available that fall into the following categories: * _Lifecycle of Solver_: create a new Solver and use it to solve the constraints in a given TModel. * _Fact_: establish facts. @@ -24,35 +21,21 @@ that fall into the following categories: * _Types_: retrieve the type of a program fragment in various ways, if that type is available. * _Inference_: create new type variables for type inference. * _Reporting_: report errors, warnings and info messages. -* _Global Info_: access global information such as the current ((TypePal:Configuration)), available type facts, - and the global store. - -(((TODO: explain global store better))) +* _Global Info_: access global information such as the current [Configuration]((TypePal:Configuration)), available type facts, and the global store (to be explained in more detail below). -In identical style as used for ((Collector)), `Solver` is a datatype with a single constructur and with a number of functions as fields, -For instance, given a `Solver` named `s`, calling the `getType` function amounts to: `s.getType(_argument-of-getType_)`. -All Solver functions are prefixed with `/* Solver field */` to emphasize that they -are a field of the Solver datatype. +In identical style as used for the [Collector]((Collector)), `Solver` is a datatype with a single constructur and with a number of functions as fields, For instance, given a `Solver` named `s`, calling the `getType` function amounts to: `s.getType(_argument-of-getType_)`. All Solver functions are prefixed with `/* Solver field */` to emphasize that they are a field of the Solver datatype. - -The result of the Solver is an enriched `TModel` that contains, amongst others, messages regarding violated requirements -or types that could not be computed. -It can also be used to generate other usefull information about the program such as a use-def relation and -the used vocabulary (used for name completion). +The result of the Solver is an enriched `TModel` that contains, amongst others, messages regarding violated requirements or types that could not be computed. It can also be used to generate other usefull information about the program such as a use-def relation and the used vocabulary (used for name completion). ## Lifecycle of Solver -Once, an initial TModel has been created by a ((Collector)), a Solver takes over to solve constraints -and produce a final TModel. A new Solver can be created by `newSolver` that comes in two flavours: +Once, an initial TModel has been created by a [Collector]((Collector)), a Solver takes over to solve constraints and produce a final TModel. A new Solver can be created by `newSolver` that comes in two flavours: ```rascal Solver newSolver(Tree pt, TModel tm) Solver newSolver(map[str,Tree] namedTrees, TModel tm){ ``` -The former takes a parse tree and an initial TModel and is intended -to solve the constraints for a single parse tree. -The latter takes a map of named parse trees and an initial TModel and can handle the situation of multiple trees -with mutual dependencies. +The former takes a parse tree and an initial TModel and is intended to solve the constraints for a single parse tree. The latter takes a map of named parse trees and an initial TModel and can handle the situation of multiple trees with mutual dependencies. Finally, `run` creates the final TModel by solving the constraints in the initial TModel: ```rascal @@ -91,10 +74,7 @@ All calculate (and require) functions use the following typing convention: an ar * an `AType`, or * a `Tree`. -In the former case, the AType is used as is. -In the latter case, the type of the tree is used provided that it exists. -Otherwise a `TypeUnavailable()` exception is generated and the calculator or requirement -in which the predicate occurs is re-evaluated at a later time. +In the former case, the AType is used as is. In the latter case, the type of the tree is used provided that it exists. Otherwise a `TypeUnavailable()` exception is generated and the calculator or requirement in which the predicate occurs is re-evaluated at a later time. ### equal @@ -107,31 +87,27 @@ The function `equal` determines whether the types of `l` and `r` are equal, the ```rascal /* Solver field */ bool (value l, value r) subtype ``` -The function `subtype` determines whether the type of `l` is a subtype of the type of `r`; -it calls the user-provided function `getSubType`, see ((TypePal:Configuration)). +The function `subtype` determines whether the type of `l` is a subtype of the type of `r`; it calls the user-provided function `getSubType`, see [Configuration]((TypePal:Configuration)). ### comparable ```rascal /* Solver field */ bool (value l, value r) comparable ``` -The function `comparable` determines whether the type of `l` is comparable with the type of `r`; -it calls the user-provided function `getSubType` twice, see ((TypePal:Configuration)). +The function `comparable` determines whether the type of `l` is comparable with the type of `r`; it calls the user-provided function `getSubType` twice, see [Configuration]((TypePal:Configuration)). ### unify ```rascal /* Solver field */ bool (value l, value r) unify ``` The function `unify` determines whether the type of `l` can be unified with the type of `r` -it calls the user-provided functions `getSubType` and `getLub`, see ((TypePal:Configuration)). -The bindings that may result from unification are effectuated when the enclosing calculate succeeds. +it calls the user-provided functions `getSubType` and `getLub`, see [Configuration]((TypePal:Configuration)). The bindings that may result from unification are effectuated when the enclosing calculate succeeds. ### lub ```rascal /* Solver field */ AType (value l, value r) lub ``` -The function `lub` return the least upper bound of the types of `l` and `r`; -it calls the user-provided function `getLub`, see ((TypePal:Configuration)). +The function `lub` return the least upper bound of the types of `l` and `r`; it calls the user-provided function `getLub`, see [Configuration]((TypePal:Configuration)). ## Require @@ -146,22 +122,19 @@ The function `requireEqual` returns when the types of `l` and `r` are equal, oth /* Solver field */ void (value l, value r, FailMessage fmsg) requireSubType ``` The function `requireSubtype` returns when the type of `l` is a subtype of `r`, otherwise the FailMessage is reported; -it calls the user-provided function `getSubType`, see ((TypePal:Configuration)). +it calls the user-provided function `getSubType`, see [Configuration]((TypePal:Configuration)). ### requireCompare ```rascal /* Solver field */ void (value l, value r, FailMessage fmsg) requireComparable ``` -The function `requireComparable` returns when the type of `l` is comparable with the type of `r`, otherwise the FailMessage is generated; -it calls the user-provided function `getSubType`twice, see ((TypePal:Configuration)). +The function `requireComparable` returns when the type of `l` is comparable with the type of `r`, otherwise the FailMessage is generated; it calls the user-provided function `getSubType`twice, see [Configuration]((TypePal:Configuration)). ### requireUnify ```rascal /* Solver field */ void (value l, value r, FailMessage fmsg) requireUnify ``` -The function `requireUnify just returns when the type of `l` can be unified with the type of `r`, otherwise the FailMessage is reported; -it calls the user-provided functions `getSubType` and `getLub`, see ((TypePal:Configuration)). -The bindings that may result from unification are effectuated when the enclosing require succeeds. +The function `requireUnify just returns when the type of `l` can be unified with the type of `r`, otherwise the FailMessage is reported; it calls the user-provided functions `getSubType` and `getLub`, see [Configuration]((TypePal:Configuration)). The bindings that may result from unification are effectuated when the enclosing require succeeds. ### requireTrue and requireFalse @@ -174,21 +147,17 @@ The function `requireFalse` returns when its condition is false, otherwise the F ## Types -Type-related functions try to retrieve various forms of type information from parts of the source program. -When that information is available, it is returned as result. -When it is not available, the internal exception `TypeUnavailable()` is thrown. -This will abort the execution of the current requirement or calculator which will then be tried later again. +Type-related functions try to retrieve various forms of type information from parts of the source program. When that information is available, it is returned as result. When it is not available, the internal exception `TypeUnavailable()` is thrown. This will abort the execution of the current requirement or calculator which will then be tried later again. ### getType -The workhorse of TypePal is the function `getType` that determines -the type of a given source code fragment in the current scope: +The workhorse of TypePal is the function `getType` that determines the type of a given source code fragment in the current scope: ```rascal /* Solver field */ AType(value src) getType ``` `src` may either be a `Tree` (i.e., a parse tree fragment) or a `loc` (the source location of a parse tree fragment). -Here is how `getType` is used in ((examples::pico)) to check the addition operator: +Here is how `getType` is used in [the Pico example]((examples::pico)) to check the addition operator: * two integer arguments give an integer result; * two string arguments give a string result; @@ -209,8 +178,7 @@ void collect(current: (Expression) ` + `, Collec ``` ### getTypeInScope -The function `getTypeInScope` determines -the type of a given source code fragment in a given scope and given roles: +The function `getTypeInScope` determines the type of a given source code fragment in a given scope and given roles: ```rascal /* Solver field */ AType (Tree occ, loc scope, set[IdRole] idRoles) getTypeInScope ``` @@ -222,9 +190,7 @@ Here * `idRoles` is a set of allowed identifier roles. ### getTypeInScopeFromName -The function `getTypeInScopeFromName` determines the type of a given name that has been bound via given identifier roles -in a given scope. -It is typically used to map a name of a type to its actual type, e.g., +The function `getTypeInScopeFromName` determines the type of a given name that has been bound via given identifier roles in a given scope. It is typically used to map a name of a type to its actual type, e.g., mapping the name `POINT` as it occurs in a declaration to the actual record type of `POINT`. ```rascal @@ -267,17 +233,13 @@ Here: ## Inference -Type inference is supported by the introduction of type variables -using `newTypeVar` in combination with unification primitives -inside `calculateEager` [Calculate](#calculate) and `requireEager` [Require](#require) -such as `requireUnify` and `unify`. The following functions support the computation -with types possibly containing type variables. +Type inference is supported by the introduction of type variables using `newTypeVar` in combination with unification primitives inside `calculateEager` [Calculate](#calculate) and `requireEager` [Require](#require) such as `requireUnify` and `unify`. The following functions support the computation with types possibly containing type variables. ### instantiate ```rascal /* Solver field */ AType (AType atype) instantiate ``` -replaces all type variables occurring in `atype` by their binding (when present). +Replaces all type variables occurring in `atype` by their binding (when present). ### isFullyInstantiated ```rascal @@ -289,29 +251,62 @@ checks whether `atype` contains any occurrences of type variables. ```rascal /* Solver field */ bool(FailMessage fmsg) report /* Solver field */ bool (list[FailMessage] fmsgs) reports +/* Solver field */ bool () reportedErrors ``` +A single message (`report`), or multiple messages can be reported (`reports`). The function `reportedErrors` returns true if any error has been reported. + ## Global Info ### getConfig ```rascal /* Solver field */ TypePalConfig () getConfig ``` -Returns the current ((TypePal:Configuration)). +Returns the current [Configuration]((TypePal:Configuration)). ### getFacts ```rascal /* Solver field */ map[loc, AType]() getFacts ``` -Returns the type facts known to the Solver as mapping from source location to AType. +### getPaths +```rascal +/* Solver field */ Paths() getPaths +``` +Returns all the paths known to the Solver. + +### getDefinitions +```rascal +/* Solver field */ set[Define] (str id, loc scope, set[IdRole] idRoles) getDefinitions +``` +Returns all the defines for a given identifier. + +### getAllDefines +```rascal +/* Solver field */ set[Define] () getAllDefines +``` +Returns all the defines. + +### getDefine +```rascal +/* Solver field */ Define(loc) getDefine, +``` +Returns the define associated with a given source location. ### getStore ```rascal /* Solver field */ map[str,value]() getStore ``` +Returns the global store of the Solver. The global store is a key-value store intended to share information between Collector and Solver as well as pass on information to later users of the typechecker as a whole. Examples taken from the Rascal typechecker include: +* The name of the current module. +* The bill-of-materials (BOM) of the current module, i.e., all used modules including a time stamp. +* The PathConfig used for typechceking. +* The grammar rules defined in the module +* The data declarations defined in the module + +It is also possible to create an arbitrary number of (named) of push down stacks in the global store. These can be used to represent context information during the collect or solve phase, see [Nested info](Collector#nested-info). -Returns the global store of the Solver. The following elements may occur in the store: +:::caution +With the availability of a global store come serious responsibilities. Don't overuse it, do not misuse it. +::: -* Remaining [Nested Info](/docs/Packages/typepal/TypePal/Collector#nested-info) from the collect phase. For instance, a single `push` to a stack during the collect phase will be visible during the solve phase and -can me (mis)used to communicate information between the two phases. diff --git a/doc/TypePal/Solver/Solver.png b/doc/TypePal/Solver/Solver.png index 0e9c6ed..de607b6 100644 Binary files a/doc/TypePal/Solver/Solver.png and b/doc/TypePal/Solver/Solver.png differ