diff --git a/README.md b/README.md index 2feca438f08b06d26952f9e10026041ebff7b22b..0f21aba92d19a683bdcfcc119794c426d498ee5f 100644 --- a/README.md +++ b/README.md @@ -11,6 +11,8 @@ See `./bin/dhallish` or `./tests/test_dhallish_ctx.rb` for an example on how to *Read [the docs](./docs.md)!* +Installation: `git clone https://gitlab.cs.fau.de/basst/ruby-dhallish.git` or `gem install dhallish` + ```bash # run tests using: ruby ./tests/test.rb @@ -21,15 +23,24 @@ ruby ./tests/test.rb # examples and usage: cat ./tests/examples.dhallish -./bin/dhallish --help ./bin/dhallish < texts/examples.dhallish ``` ### Changes to `dhall-lang`: - 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 +### 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: - `''strings that start with two quotes''` - `Kind` and `Sort` (What are those?) @@ -38,3 +49,4 @@ cat ./tests/examples.dhallish ### 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. + It should be fixed, although the latest release on *rubygems.org* still has this bug. diff --git a/docs.md b/docs.md index 3c801f4988a4b1577a74f3c0f93aea8951e17e12..2af5a0c54fbc9660e88ac45cf59e1a1c3645f904 100644 --- a/docs.md +++ b/docs.md @@ -1,32 +1,95 @@ # Documentation for Dhallish! +### The Executable: + *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). +Install *Dhallish* by installing ruby and then typing `gem install dhallish` into your terminal. *dhallish* accepts the following command line options -- '--pretty': print prettified json -- '--type': print the type of the expression instead of its value +- `--pretty`: print prettified json +- `--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. -*Dhallish* can also be used from other ruby files, if './lib/dhallish.rb' is required from that file. -The following functions from './lib/dhalish.rb' can be used: +*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: -- `evaluate(dhallcode, ctx=nil, expected_type=nil)`: - Arguments: +- `Dhallish::evaluate(dhallcode, ctx=nil, expected_type=nil)` - `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 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 the passed type does not match the actual type, a DhallError is raised. -- `create_ctx(dhallcode, basedir=Dir.pwd)` - Arguments: - - `dhallcode`: A string containing the expression that shall be evaluated +- `Dhallish::create_ctx(dhallcode, basedir=Dir.pwd)` + - `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 -- `create_ctx_from_file(dhallfile, basedir=nil)` - Arguments +- `Dhallish::create_ctx_from_file(dhallfile, basedir=nil)` - `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. diff --git a/lib/stdlib.rb b/lib/stdlib.rb index 4ff0caf9a30136db1c84de4e51a57e2af470ec79..75013990cd225b2c69913b78af36e04664fb12ab 100644 --- a/lib/stdlib.rb +++ b/lib/stdlib.rb @@ -19,6 +19,12 @@ module Dhallish end 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) # Types: