Skip to content

Commit

Permalink
Updating documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
PaulKlint committed Feb 17, 2024
1 parent 507c9ff commit dd0f083
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 13 deletions.
21 changes: 11 additions & 10 deletions doc/TypePal/ConceptsAndDefinitions/ConceptsAndDefinitions.md
Original file line number Diff line number Diff line change
Expand Up @@ -175,20 +175,21 @@ TypePal provides the data type `DefInfo` for this purpose:

```rascal
data DefInfo
= noDefInfo() //<1>
| defType(value contrib) //<2>
| defTypeCall(list[loc] dependsOn, AType(Solver s) getAType) //<3>
| defTypeLub(list[loc] dependsOn, list[loc] defines, list[AType(Solver s)] getATypes) //<4>
= noDefInfo() //<1>
| defType(loc src) //<2>
| defType(Tree tree) //<3>
| defType(AType atype) //<4>
| defTypeCall(list[loc] dependsOn, AType(Solver s) getAType) //<5>
| defTypeLub(list[loc] dependsOn, list[loc] defines, list[AType(Solver s)] getATypes) //<6>
;
```
<1> No information associated with this definition.
<2> Explicitly given AType contribution associated with this definition. `contrib` can either be an `AType`, or a `Tree`.
In the latter case, the type of that tree is used (when it becomes available) for the current definition.
<3> Type of this definition depends on the type of the entities given in `dependsOn`, when those are known,
<2> Explicitly given AType contribution associated with this definition. `src` is a source code location. The type of that source location is used (when it becomes available) for the current definition.
<3> Explicitly given AType contribution associated with this definition. `tree` is a `Tree`. The type of that tree is used (when it becomes available) for the current definition.
<4> Explicitly given AType contribution associated with this definition. `atype` is an `AType`. That type is used for the current definition.
<5> Type of this definition depends on the type of the entities given in `dependsOn`, when those are known,
`getAType` can construct the type of this definition.
`getAType` will only be called by TypePal during constraint solving.
<4> Refine a set of definitions by taking their LUB, mostly used for local type inference.
<6> Refine a set of definitions by taking their LUB, mostly used for local type inference.

The ((Solver)) argument of `getAType` and `getATypes` is the current constraint solver being used.

WARNING: noDefInfo may be removed.
6 changes: 3 additions & 3 deletions doc/TypePal/Overview/Overview.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ An overview of TypePal

#### Description

TypePal is a declarative framework that operates on a model of the program to be type checked that consisting of
TypePal is a declarative framework that operates on a model of the program to be type checked that consists of

* _facts_ that some source code fragment has a known type, e.g., an integer literal is of type integer,
or that its type is equal to the type of another source code fragment, e.g., the type of the expression in parentheses `( e )` is equal to the type of `e`.
Expand All @@ -28,8 +28,8 @@ When a requirement is satisfied or a calculator computes a new type,
this leads to the creation of new facts that may trigger the computation of other requirements and calculators.

Technically, TypePal uses _scope graphs_ for expressing definition and use of names (including their role, scope, name space, and visibility),
and _constraints_ to describe facts, requirements and calculators.
These constraints are such that they can express either type checking or type inference, or a mixture thereof.
and _constraints_ to describe facts, requirements and calculators. These constraints are such that they can express either type checking or type inference, or a mixture thereof.
Under the hood, these constraints are solved in an efficient, data-driven, fashion.
Scope graphs have been inspired by Kastens and Waite, _Name analysis for modern languages: a general solution_, SP&E, 2017.

TypePal is highly parameterized and can be adapted to specific type checking needs.

0 comments on commit dd0f083

Please sign in to comment.