valhallac

Compiler for set-theoretic programming language.
git clone git://git.knutsen.co/valhallac
Log | Files | Refs | README | LICENSE

commit c2a9055923a3dd23ddd5782d0ab1e8e692c19101
parent 0d685187969bfcd3123055f1bee02ece4e490f5f
Author: Demonstrandum <moi@knutsen.co>
Date:   Thu, 26 Nov 2020 01:43:12 +0000

Project status update.

Diffstat:
MREADME.md | 20+++++++++++++-------
Asamples/colon.vh | 56++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Asamples/conditional.vh | 63+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Asamples/converting.vh | 54++++++++++++++++++++++++++++++++++++++++++++++++++++++
Asamples/declaration_v_test.vh | 27+++++++++++++++++++++++++++
Asamples/fixity.vh | 1+
Asamples/hello_someone.vh | 6++++++
Asamples/hello_world_function.vh | 10++++++++++
Asamples/indexed_set.vh | 32++++++++++++++++++++++++++++++++
Asamples/mapping.vh | 35+++++++++++++++++++++++++++++++++++
Msamples/match.vh | 18+++++++++---------
Asamples/moduels.vh | 37+++++++++++++++++++++++++++++++++++++
Asamples/non-modules.vh | 33+++++++++++++++++++++++++++++++++
Msamples/peano_implicit.vh | 6++++--
Asamples/pi.vh | 17+++++++++++++++++
Msamples/product_type.vh | 19+++++++++----------
Msamples/raw_hello_world.vh | 4++--
Asamples/singleton.vh | 46++++++++++++++++++++++++++++++++++++++++++++++
Msamples/subsets.vh | 6+++---
Asamples/syntax.vh | 31+++++++++++++++++++++++++++++++
Msrc/bin.rs | 31+++++++++++++++++++------------
Msrc/syntax/analysis/type_resolver.rs | 2+-
Msrc/syntax/operators.rs | 2+-
Mtest_source.vh | 7+++++++
24 files changed, 516 insertions(+), 47 deletions(-)

diff --git a/README.md b/README.md @@ -1,3 +1,7 @@ +# `valhallac` + +> The Valhalla Compiler + <p align="center"> <img alt="Valhalla Flag" height=230 src="https://github.com/Demonstrandum/valhalla/raw/master/assets/logo.svg.png" /> </p> @@ -8,7 +12,9 @@ machine that the compiled bytecode runs on, which is, [Brokkr VM](https://github.com/Demonstrandum/brokkr). ## IN (HEAVY) DEVELOPMENT +**`[!!]` Planning a complete rewrite, and balancing work.** +--- What's been done so far on the front-end: @@ -43,27 +49,27 @@ What's been done so far on the front-end: for future interpretation and execution by the virtual machine. - [ ] ... -The VM, i.e. the backend for the language, is being developed independently -and will have its own progress and check-list updates. +The VM, i.e. the backend for the language, is being developed separately +and will progress semi-independently. ### Compile & Run #### Requires Rust Nightly for now. In your shell, in the root of this repository, you may write: -```console +```sh cargo run [source-file-to-compile.vh] [-o out-file] [-v] ``` or, have the compiler print out debug information like token streams, syntax trees, symbol tables, bytecode instructions, &ct., use `--features=debug`: -```console +```sh cargo run --features=debug [source-file.vh] ``` For example, you can run. -```console -cargo run test_source.vh -v # (verbose) +```sh +cargo run test_source.vh -v # For verbose output. ``` to demonstrate compilation with the included test-file (`test_source.vh`). The argument of a source-file to compile is, of course, necessary. @@ -95,6 +101,6 @@ gathered, it's not a very popular paradigm... Likely for good reason, but hey, it might be interesting. ### Dependencies -Yikes... +To be significantly reduced. ![deps](https://github.com/Demonstrandum/valhalla/raw/master/graph.png) diff --git a/samples/colon.vh b/samples/colon.vh @@ -0,0 +1,56 @@ +-- What does the colon mean? +:sym -- Symbol +:(x + y) -- Quoted/Symbolic expression +f : A -> B -- Type annotation +do: x y z -- Indented code block + a b c + +-- Note: + +--where: +--let: +--in: +--for: +-- etc. + +-- Are just short for: + +-- where do: +-- let do: +-- in do: +-- for do: + +-- e.g. + +x where: + y = 3 + x = y + 4 + +-- same as, + +x where: y = 3 + x = y + 4 + +-- same as, + +x where do: + y = 3 + x = y + 4 + +-- same as, + +x where do + y = 3 + x = y + 4 +end + +-- same as, + +x where { + y = 3 + x = y + 4 +} + +-- same as, + +x where y = 3, x = y + 4 diff --git a/samples/conditional.vh b/samples/conditional.vh @@ -0,0 +1,63 @@ +-- For example, a piecewise function: +f : 'A -> 'B -> 'C +f a b = piecewise do: + C a b, a == 1 + C b a, b == 1 + C 1 1, otherwise + +-- or +piecewise { + x, p + y, q + z, otherwise +} + +-- or write `cond' instead of `piecewise' +cond do: + x, p + y, q + z, otherwise + + +-- for more trivial branching, (with pattern matching) + +-- Exactly the same as the previous f. +f : 'A -> 'B -> 'C +f a b = match (a, b) do: + (1, _) => C a b + (_, 1) => C b a + (_, _) => C 1 1 + +-- Or, the same again +f : (a : 'A) -> (b : 'B) -> 'C +f = curry f' where + f' : 'A * 'B -> 'C + f' (1, _) = C a b + f' (_, 1) = C a b + f' (_, _) = C 1 1 + +-- Again! +f : (a : 'A) -> (b : 'B) -> 'C +f 1 _ = C a b +f _ 1 = C b a +f _ _ = C 1 1 + +-- And again, +f : 'A -> 'B -> 'C +f a@1 b = C a b +f a b@1 = C b a +f 1 1 = C 1 1 + +-- Example of the special (syntactic) => operator + +S = [ x : Nat => x > 3 ] +Z = filter f Any where f : Any -> Bool + f a = match a do: + x : Nat => x > 3 -- This is exactly like in S. + _ => False + +-- This is how set builder notation works. +-- and how the uses of the => operators are related. + +assert (S == Z) + diff --git a/samples/converting.vh b/samples/converting.vh @@ -0,0 +1,54 @@ +Bool = [ :true + :false ] +True = :true +False = :false + +assert (1 == 1 <- Bool) +assert (1 == 2 <- Bool) +assert ((1 == 1) == :true) +assert ((1 == 2) == :false) + +b : Int +b = :true -- Error. + +from : Bool -> Nat +from :true = 1 +from :false = 0 + +b : Nat +b = :true -- Still an error. + +-- Try again +b : Real +b = from :true -- Works! + +assert (b == 1) + +-- What about other types? +from : Bool -> String -- overloaded. +from :true = "yes" +from :false = "no" + +s : String +s = from :false + +assert (s == "no") + +-- What about: +c = from :true -- Error! +-- We don't know what type we're converting to. + +-- We have to use `as` instead. +c = :true as String +assert (c <- String) +assert (c == "yes") + +-- This is how the `as` operator is defined: +(as) : 'A -> ['B] -> 'B +item as _ = from item -- We know from the type signature that + -- `(from item) <- 'B`, so it is no + -- longer ambiguous! + + + + diff --git a/samples/declaration_v_test.vh b/samples/declaration_v_test.vh @@ -0,0 +1,27 @@ +-- Declare equality +a = 3 +-- Test equality +a == 3 -- True + +-- Declare membership +a : Nat +-- Test memebership +a <- Nat -- True + + +-- Subset (non-strict) +A <: Nat +A -< Nat -- True + + +-- Any test can be made into a declaration: +b : Nat +b = 4 +-- The Test: +3 < b < 5 -- True +-- Made into declaration: +[ b ] = [ n : Nat => 3 < n < 4 ] +-- ^^^ This sets (b=0), by pattent matching on a singleton set. +-- This can ve done for any test, making it into a declaration. +-- (As long as the test is limiting enough, narrowing it down to +-- only a singluar value.) diff --git a/samples/fixity.vh b/samples/fixity.vh @@ -0,0 +1 @@ +-2 3 diff --git a/samples/hello_someone.vh b/samples/hello_someone.vh @@ -0,0 +1,6 @@ +[ :puts, print + :gets, input ] = import :IO + +name = input "> " +puts "Hello, " + name.captialise + "." + diff --git a/samples/hello_world_function.vh b/samples/hello_world_function.vh @@ -0,0 +1,10 @@ +io = import :IO + +let: greeting : String -> String + greeting name = "Hello, %{name.capitalise}." +in module Hello + +io::puts <| Hello::greeting place + where: place : String + place = "World" + diff --git a/samples/indexed_set.vh b/samples/indexed_set.vh @@ -0,0 +1,32 @@ +-- You could maybe equate this with an 'array'. + +-- Indexed set example: +S = [ "b"; "c"; "a" ] +I = [ 0; 1; 2 ] + +-- A is the "array" here +A : I -> S +A 0 = "b" +A 1 = "c" +A 2 = "a" + +-- or, equivalently +A = [ + (0, "b") + (1, "c") + (2, "a") +] + + +-- This is very cumbersome though, hence the alternate syntax +A = [| "b"; "c"; "a" |] + +assert (A 1 == "c") +assert (A -< I * S) -- A is a subset of the cartesian product of I and S. + +-- An indexed ste is similar to, +-- but not the same as a tuple/ordered pair. +a = ("b", "c", "d") +assert (A /= a) +assert <| all [ nth i a == A i => i <- I ] + diff --git a/samples/mapping.vh b/samples/mapping.vh @@ -0,0 +1,35 @@ +vec : Nat^3 + +vec = (1, 2, 3) +-- or +vec = 1,2,3,() +-- or +vec = 1,2,3,Empty + + +map (2 *) vec -- (2, 4, 6) +map (n |-> 2*n - 1) vec -- (1, 3, 5) + +-- Image of A under f <=> map f A +assert <| image vec (2 *) == map (2 *) vec +assert <| image vec (n |-> 2*n - 1) vec == map (n |-> 2*n - 1) vec +assert <| image vec ((+ 1) <> (2 *)) vec == map ((+ 1) <> (2 *)) vec + +-- Essentially: +map : ('A -> 'B) -> 'A^'N -> 'B^'N +map f () = () +map f (x, xs) = (f x, map xs) + +image : 'A^'N -> ('A -> 'B) -> 'B^'N +image = flip map + +map f A -- Read: Mapping of f on A +image A f -- Read: Image if A under f + + +-- Of course, also works with sets (in the standard library): +set = [ 2; 1; 3 ] + +image set (+ 10) == [ 13; 12; 11 ] +map (+ 10) set == [ 11; 13; 12 ] + diff --git a/samples/match.vh b/samples/match.vh @@ -3,29 +3,29 @@ Product = Tagged Nat^2 * Int -- Makes a constructor. prod : Product -prod = [| 2; 7; -66 |] -- Casts implicitly. ---prod = Product [| 2; 7; -66 |] +prod = (2, 7, -66) -- Casts implicitly. +--prod = Product (2, 7, -66) alpha : Boolean -alpha = match prod: - [| 0; 0; i |] => i == 0, - Product [| 2; n; _ |] => n == 2, -- Explicit, but not needed, type is know. - [| _; _; i |] => i <- Nat | [ -1 ], - [| n; m; i |] => do: +alpha = match prod do: + (0, 0, i) => i == 0, + Product (2, n, _) => n == 2, -- Explicit, but not needed, type is know. + (_, _, i) => i <- Nat | [ -1 ], + (n, m, i) => do: n + m == -j where: j = i + m % 3 beta : Number beta = match prod { - [| _; _; i |] => { + (_, _, i) => { j = i + 2 j * m where { k = 8 - i m = k ** 3 } }, - [| _; n; _ |] => n * 8, + (_, n, _) => n * 8, _ => 42 } diff --git a/samples/moduels.vh b/samples/moduels.vh @@ -0,0 +1,37 @@ +module Hello where: + greet name = "Hello, :{name}!" + +bye = module Bye where: + greet name = "Bye, :{name}!" + +Hello::greet "Sam" --> "Hello, Sam!" +Bye::greet "Sam" -- Error! No such module exists. + +bye::greet "Sam" --> "Bye, Sam!" +-- ^^ That works. + +assert (bye <- Module) -- Type of `Module'. + +import :IO +IO::puts "Hi." +io::puts "Hi." -- Error! `io' does not exist. +-- OR: +io = import :IO +io::puts "Hi." +IO::puts "Hi." -- Error! `IO' does not exist. + +-- Syntax is general: +let: + greet name = "Hi, :{name}!" +in module Hi + +Hi::greet "Rostislav" --> "Hi, Rostislav!" + +-- + +member Hello :greet == Hello::greet +IO.memeber :greet == Hello::greet +-- (::) is syntactic sugar for this. +-- i.e. +member m e = m::(eval! e) +m::e = member m :(`e) diff --git a/samples/non-modules.vh b/samples/non-modules.vh @@ -0,0 +1,33 @@ +-- `Real' is the set of all real numbers, not a moudle. +-- But, it can use similar syntax/functions as module, +-- to represent so-called 'members' of the real numbers. + +-- The mathematical constant e = 2.718... +Real::e +-- which is the same as: +member Real :e +-- +assert ((round_to (3 dp) Real::e) == 2.718) +assert ((round_to (3 sf) Real::pi) == 3.14) +-- + +-- Adding a number is done as such: +--member : [Real] -> Real +member Real :my_number = 1337 + +assert (Real::my_number == 1337) + + +-- But for non-pure-number constant, you should +-- just use a module. +-- e.g. + +module Universal where: + c = 2.998E8 + G = 6.67408E-11 + e = -1.602E-19 + mu_0 = 4 * Real::pi * 1E-7 + +schwarzschild_radius m = 2 * Universal::G * m / Universal::c^2 + + diff --git a/samples/peano_implicit.vh b/samples/peano_implicit.vh @@ -2,8 +2,10 @@ import :Prelude io = import :IO -- We don't need to define Zero and Succ, they can exist --- as application of functions, and not mean anything more, --- they perform no computation like normal functions. +-- as application of functions or intances of themselves, +-- and not mean anything more, they perform no computation, +-- unlike normal functions. + N = [ Zero ] | [ Succ n => n <- N ] where: Zero : N Succ : N -> N diff --git a/samples/pi.vh b/samples/pi.vh @@ -0,0 +1,17 @@ +[ (:puts, puts) ] | io = import :IO + +sum : Number^'N -> Number +sum () = 0 +sum (x,xs) = x + sum xs + +product : Number^'N -> Number +product () = 1 +product (x,xs) = x * product xs + +pi n = map ((2 /) <> f) (1..n) |> product |> (* 2) + where: f : Nat -> Real + f 0 = 0 + f k = sqrt (2 + f k) + +puts <| pi 20 + diff --git a/samples/product_type.vh b/samples/product_type.vh @@ -8,7 +8,7 @@ char *name; double r; }; - + int main(void) { struct Prod prod = { 3, 9, "John", -2.6f }; @@ -28,9 +28,8 @@ Prod = Int^2 * String * Real -- Prod is a type (set) of the cartesian product of: -- Two Ints, String and Real. --- [| ... |] denotes an ordered set, or a 'vector' if you will. prod : Prod -- prod is an element of Prod (prod has type Prod). -prod = [| 3; 9; "John"; -2.6 |] -- way to initialise, by just assigning. +prod = (3, 9,"John", -2.6) -- way to initialise, by just assigning. -- Now, to access elements of `prod`, we may index normally. assert (prod[0] is 3) @@ -61,11 +60,11 @@ y = index 1 name = index 2 r = index 3 --- If we don't include the type signatures here, then +-- If we don't include the type signatures here, then -- the functions (x, y, name, etc) would be defined generally -- for any type overloading the `index` function. -IO::put "${prod.x}, ${prod.y}, ${prod.name} ${prod.r}" +IO::put "#{prod.x}, #{prod.y}, #{prod.name} #{prod.r}" -- And we've done the same as the C program, but -- all this can be automated by macros, and we were @@ -84,19 +83,19 @@ y = index 1 v : Vec2D -v = [| 1; 2 |] -- Create a Vec2D. +v = (1, 2) -- Create a Vec2D. -[| n; m |] : Real^2 -[| n; m |] : Vec2D -- these two type signatures mean the same thing, +(n, m) : Real^2 +(n, m) : Vec2D -- these two type signatures mean the same thing, -- Neither type signature are necessary, because we have type inference. -[| n; m |] = v -- pattern matching assignment. +(n, m) = v -- pattern matching assignment. assert (v.x == n) assert (v.y == m) show : Vec2D -> String -- overload `show'. -show v = "(${v.x}, ${v.y})" +show v = "(#{v.x}, #{v.y})" IO::puts v -- this calls `show' impicitly, -- (within the definition of `puts'). diff --git a/samples/raw_hello_world.vh b/samples/raw_hello_world.vh @@ -1,3 +1,3 @@ -# Without using the prelude, or importing IO... +-- Without using the prelude, or importing IO... -_write_stream :STDOUT "Hello, World.\n" +_write_stream :1 "Hello, World.\n" diff --git a/samples/singleton.vh b/samples/singleton.vh @@ -0,0 +1,46 @@ +-- Say we want to represent the smallest non-zero +-- positive number. Call it omega. + +RealPos = filter (> 0) Real \ [0] + +-- Try one (1): +omega_1 = index 0 <| collect [ n : Real => 0 < n < m => m <- RealPos ] +-- This is not quite so great, this will collect the elements +-- into a vector, and since its a singleton, get the first and only +-- element. This elememt will be computed after a while, and we'll +-- get the smallest non-zero, positive 64bit floating-point number. + +-- This is not satisfactory, we want to mathematically represent +-- this concept. + +-- Try two (2): +omega_set = [ n : Real => 0 < n < m => m <- RealPos ] + +-- Verify that this set is indeed a singleton. +assert (singleton? omega_set) --> :true + +-- Extract the singleton: +omega_2 = singleton omega_set + +-- or even better, with a pattern match. +[ omega ] = [ n : Real => 0 < n < m => m <- RealPos ] + +assert (omega_2 == omega) + + +-- Simpler examples: +a : Nat +[ a ] = [ n : Nat => 1 < n < 3 ] + +assert (a == 2) + + +assert (singleton? [ n : Nat => 2 < n < 4 ] == :true) +assert (singleton? [ n : Real => 2 < n < 4 ] == :false) + + + + + + + diff --git a/samples/subsets.vh b/samples/subsets.vh @@ -1,7 +1,7 @@ -- I is subset of the integers. I <: Int -I : Power(Int) -- the same +I : Power(Int) -- the same as above -- n and m are both integers. -[| n; m |] : I^2 -[| n; m |] : I*I -- the same +(n, m) : I^2 +(n, m) : I*I -- the same as above diff --git a/samples/syntax.vh b/samples/syntax.vh @@ -0,0 +1,31 @@ +if_then_else : Bool -> Code -> Code -> 'Value where Code = Quote 'Value +if_then_else condition consequence alternative + = !eval <| piecewise { consequence, condition; alternative, otherwise } + +syntax :(if #p then #c else #a) = if_then_else #p #c #a +-- ^^^ The expression to match ^^^ what it evaluates to +-- Alt. +mixfix (if # then # else #) if_the_else 10 +-- ^^^ ^^^ ^^^ ^^ Mixfix precedence. +-- | | |The function whose parameters are given by the #s. +-- | |The expression to match. +-- |Alternative to {infix, prefix, postfix/suffix} when there are >2 paramters. + +x = if 1 == 1 + then "Hi." + else "Bye." + +assert <| x == "Hi." + +-- Maybe you'd want French syntax, you can define that. + +syntax :(si #p alors #c sinon #a) = if_then_else #p #c #a +-- Alt. +mixfix (si#alors#sinon#) if_then_else 10 + +y = si 1 == 1 + alors "Bonjour." + sinon "Au revoir." + +affirmer = assert +affirmer <| y == "Bonjour." diff --git a/src/bin.rs b/src/bin.rs @@ -2,7 +2,7 @@ use ::valhallac; use std::env; use std::{fs::File, path::Path}; -use std::io::Write; +use std::{fmt, io::Write}; use std::time::Instant; use std::collections::HashMap; @@ -57,13 +57,20 @@ fn collect_flags() -> HashMap<Flags, String> { } else if arg_str.starts_with('-') { let chars = arg_str.split(""); for c in chars { - if c == "-" { continue; } - if c == "v" { - singleton(Flags::Verbose); - } else if c == "o" { - maybe_argument = Some(Flags::Out); - singleton(Flags::Out); - } + match c { + "-" | "" => continue, + "v" => singleton(Flags::Verbose), + "o" => { + maybe_argument = Some(Flags::Out); + singleton(Flags::Out) + }, + "V" => singleton(Flags::Version), + chr => { + argument_error( + format!("`-{}' option does not exist.", chr)); + std::process::exit(1) + } + }; } } } @@ -78,8 +85,8 @@ macro_rules! not_debug { }; } -fn argument_error(msg : &str) { - println!("{} {}", "[**]".red().bold(), msg.bold()); +fn argument_error(msg : impl fmt::Display) { + println!("{} {}", "[**]".red().bold(), msg.to_string().bold()); } lazy_static! { @@ -119,7 +126,7 @@ pub fn main() -> Result<(), Box<dyn std::error::Error>> { for file in files { not_debug!(verbose, { - println!("{}{} `{}'...", *INFO, + println!("{}{} `{}'", *INFO, "Parsing".bold().blue(), file.underline().white()); }); @@ -135,7 +142,7 @@ pub fn main() -> Result<(), Box<dyn std::error::Error>> { // Then compile into series of instructions, // stored as a code block. not_debug!(verbose, { - println!("{}{}...", *INFO, + println!("{}{}", *INFO, "Compiling".bold().blue()); }); let block = valhallac::compile(&root); diff --git a/src/syntax/analysis/type_resolver.rs b/src/syntax/analysis/type_resolver.rs @@ -204,7 +204,7 @@ pub fn resolve_branch(&mut self, branch : &Nodes) -> Nodes { if let Nodes::Call(ref mut appl_1) = *appl_0.callee { if let Nodes::Ident(ref ident_1) = *appl_1.callee { match ident_1.value.as_ref() { - "->" => panic!("We should have prevented this."), + //"->" => panic!("We should have prevented this."), ":" => { self.resolve_annotation(appl_0_clone, appl_1.clone()); // FIXME: Should we really replace the annotation with a nil? diff --git a/src/syntax/operators.rs b/src/syntax/operators.rs @@ -7,7 +7,7 @@ pub enum Side { /// Operator information, including: /// - The string, representing what the operator looks like. -/// - Its precedence (as an i32), the higher the int, the higher the precedence. +/// - Its precedence (as an i32), the higher the int, the higher the precedence /// - Associativity, which can either be left, right, or no associativity. /// - The number of arguments it takes / its arity. Either one, or two. #[derive(Clone, Copy)] diff --git a/test_source.vh b/test_source.vh @@ -1,6 +1,13 @@ -- TODO: Test overloading with `f`. -- TODO: Test casting from subsets of Real, upto Real. +R = Real + +BinaryType = R -> R -> R +(*) : BinaryType +(+) : BinaryType +(-) : BinaryType + f : Real -> Real -> Real f a b = (1 + 1) * a + b -- 2a + b