Skip to content
Snippets Groups Projects
Commit e6b86dee authored by Lou Knauer's avatar Lou Knauer
Browse files

docs.md changes made friday morning

parent 18da7bcd
Branches master
No related tags found
No related merge requests found
...@@ -11,6 +11,8 @@ See `./bin/dhallish` or `./tests/test_dhallish_ctx.rb` for an example on how to ...@@ -11,6 +11,8 @@ See `./bin/dhallish` or `./tests/test_dhallish_ctx.rb` for an example on how to
*Read [the docs](./docs.md)!* *Read [the docs](./docs.md)!*
Installation: `git clone https://gitlab.cs.fau.de/basst/ruby-dhallish.git` or `gem install dhallish`
```bash ```bash
# run tests using: # run tests using:
ruby ./tests/test.rb ruby ./tests/test.rb
...@@ -21,15 +23,24 @@ ruby ./tests/test.rb ...@@ -21,15 +23,24 @@ ruby ./tests/test.rb
# examples and usage: # examples and usage:
cat ./tests/examples.dhallish cat ./tests/examples.dhallish
./bin/dhallish --help
./bin/dhallish < texts/examples.dhallish ./bin/dhallish < texts/examples.dhallish
``` ```
### Changes to `dhall-lang`: ### Changes to `dhall-lang`:
- More Operators: `<`, `>`, `<=`, `>=`, `-`, `/` - More Operators: `<`, `>`, `<=`, `>=`, `-`, `/`
- `==` and `!=` do work on Numbers (`Natural`s, `Integer`s and `Double`s) - `==` and `!=` do work on Numbers (`Natural`, `Integer` and `Double`)
- It is possible to get an Optional from an union - It is possible to get an Optional from an union
### TODO:
- Test against `dhall-lang/tests`
- Implement missing features
- Fix bug in unification
- more documentation
- clean up code
- better error messages
- type inference: omit argument types?
- Allowing `\(list: List a) -> a -> ...` directly instead of `\(a: Type) -> \(list: List a) -> a -> ...`?
### Missing Features: ### Missing Features:
- `''strings that start with two quotes''` - `''strings that start with two quotes''`
- `Kind` and `Sort` (What are those?) - `Kind` and `Sort` (What are those?)
...@@ -38,3 +49,4 @@ cat ./tests/examples.dhallish ...@@ -38,3 +49,4 @@ cat ./tests/examples.dhallish
### Known Bugs: ### Known Bugs:
- There is a bug in our unification or substitution that only appears in rare cases when the same name for a generic type is used multiple times. - There is a bug in our unification or substitution that only appears in rare cases when the same name for a generic type is used multiple times.
It should be fixed, although the latest release on *rubygems.org* still has this bug.
# Documentation for Dhallish! # Documentation for Dhallish!
### The Executable:
*Dhallish* is a ruby gem and provides an executable dhallish. This executable reads from *STDIN* and *Dhallish* is a ruby gem and provides an executable dhallish. This executable reads from *STDIN* and
outputs *JSON*. The *JSON* output does not aim to be compatible with [dhall-to-json](https://github.com/dhall-lang/dhall-haskell/tree/master/dhall-json). outputs *JSON*. The *JSON* output does not aim to be compatible with [dhall-to-json](https://github.com/dhall-lang/dhall-haskell/tree/master/dhall-json).
Install *Dhallish* by installing ruby and then typing `gem install dhallish` into your terminal.
*dhallish* accepts the following command line options *dhallish* accepts the following command line options
- '--pretty': print prettified json - `--pretty`: print prettified json
- '--type': print the type of the expression instead of its value - `--type`: print the type of the expression instead of its value (in the current implementation, the input is still evaluated)
If passed a file as a command line argument, *dhallish* reads from that file instead of stdin. If passed a file as a command line argument, *dhallish* reads from that file instead of stdin.
*Dhallish* can also be used from other ruby files, if './lib/dhallish.rb' is required from that file. *Dhallish* can also be used from other ruby files, if `dhallish` is required from that file.
The following functions from './lib/dhalish.rb' can be used: The following functions from `./lib/dhalish.rb` can be used:
- `evaluate(dhallcode, ctx=nil, expected_type=nil)`: - `Dhallish::evaluate(dhallcode, ctx=nil, expected_type=nil)`
Arguments:
- `dhallcode`: A string containing the expression that shall be evaluated - `dhallcode`: A string containing the expression that shall be evaluated
- `ctx`: The context in which the expression is evaluated. If nothing is passed, an empty context is used - `ctx`: The context in which the expression is evaluated. If nothing is passed, an empty context is used.
- `expected_type`: The Dhallish-Type expected by the caller. If nothing is passed, a list is returned where - `expected_type`: The Dhallish-Type expected by the caller. If nothing is passed, a list is returned where
the first element is the value of the expression and the second element is the type. the first element is the value of the expression and the second element is the type.
If a Dhallish-Type is passed and the type of the result matches the expected type, only the value is returned. If a Dhallish-Type is passed and the type of the result matches the expected type, only the value is returned.
If the passed type does not match the actual type, a DhallError is raised. If the passed type does not match the actual type, a DhallError is raised.
- `create_ctx(dhallcode, basedir=Dir.pwd)` - `Dhallish::create_ctx(dhallcode, basedir=Dir.pwd)`
Arguments: - `dhallcode`: A string containing the expression that shall be evaluated.
- `dhallcode`: A string containing the expression that shall be evaluated The special expression `???` must be the return value of *dhallcode* for this function.
A context is returned which can be used in `Dhallish::evaluate()`. All variables and functions defined
where `???` was written will be defined.
- `basedir`: A string containing a path that is used when files are imported from a relative path - `basedir`: A string containing a path that is used when files are imported from a relative path
- `create_ctx_from_file(dhallfile, basedir=nil)` - `Dhallish::create_ctx_from_file(dhallfile, basedir=nil)`
Arguments
- `dhallfile`: A string containing the path to a file that contains dhallish-code - `dhallfile`: A string containing the path to a file that contains dhallish-code
- `basedir`: A string containing a path that is used when files are imported from a relative path - `basedir`: A string containing a path that is used when files are imported from a relative path.
When nil is passed, the base directory of *dhallfile* is used.
- `Dhallish::empty_context(basedir=Dir.pwd)`
- Returns an empty context. *basedir* is used when files are imported from a relative path.
- In this context, only the dhall standard library and types will be defined.
- `Dhallish::define(ctx, name, value, type)`
- Define something of type `type` under the name `name` in `ctx`. Best look at an example below.
### Types:
The *evaluate* function described above returns ether a ruby value and its type or only the ruby value if an expected type is passed.
*Dhallish* represents the types `Natural`, `Integer` ,`Double`, `Bool` and `Text` simply as their ruby equivalents. `List` and `Record` are
represented as ruby lists and hashes. For functions/lambdas, types and unions there are special classes (have a look at `lib/types.rb`).
An `Optional` is represented ether as nil or as its actual value.
- `Dhallish::Types::{Natural, Integer, Double, Text, Bool}` can directly be passed as an expected type
- `Dhallish::Types::List.new(elmtype)` stands for a list with elements of type `elmtype`
- `Dhallish::Types::Optional.new(type)` stands for an optional which may contain something of type `type`
- `Dhallish::Types::Record.new({ "foo" => footype, "bar" => bartype })` stands for a record with the fields `foo` of type `footype` and `bar` or type `bartype`
- `Dhallish::Types::{TextList, NaturalList, IntegerList, DoubleList}` are predefined for convenience
### Examples:
```ruby
require 'dhallish'
num, type = Dhallish::evaluate("42")
# num = 42
# type = Dhallish::Types::Natural
# Dhallish::create_ctx("???") and Dhallish::empty_ctx() are identical
ctx = Dhallish::create_ctx("
let f = \\(x: Natural) -> \\(y: Integer) -> Natural/toInteger x + y
in ???
")
res = Dhallish::evaluate("f 1 +2", ctx, Dhallish::Types::Integer)
# res = 3
# simple define example:
Dhallish::define(ctx, :one, 1, Dhallish::Types::Natural)
res, type = Dhallish::evaluate("one + 1", ctx)
# res = 2, type = Dhallish::Types::Natural
math = Dhallish::BuiltinFunction.new { |firstArg|
Dhallish::BuiltinFunction.new { |secondArg|
"#{firstArg} + #{secondArg} = #{firstArg + secondArg}"
}
}
Dhallish::define(ctx, :math, math,
Dhallish::make_fn_type(
Dhallish::Types::Natural, Dhallish::Types::Natural, Dhallish::Types::Text))
Dhallish::evaluate("(math 1 2) == \"1 + 2 = 3\"", ctx) # = [true, Dhallish::Types::Text]
```
If you want to create new builtin generic functions have a look at `lib/stdlib.rb`.
It is possible to use `Dhallish::make_fn_type` for that as well.
...@@ -19,6 +19,12 @@ module Dhallish ...@@ -19,6 +19,12 @@ module Dhallish
end end
module_function :make_fn_type module_function :make_fn_type
def define(ctx, name, value, type)
ctx["<#TYPES#>"][name.to_s] = type
ctx["<#VALS#>"][name.to_s] = value
end
module_function :define
def fill_context(globalctx, types) def fill_context(globalctx, types)
# Types: # Types:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment