Serves me right for thinking I could do better than the Haskell report. The code, as it stands, is insufficient to detect at least these conditions

• Empty data declarations

data Bottom : Type where
data Top : Type where
  | TT : Top

=>

data Bottom : Type where {};
data Top : Type where {
  | TT : Top;
};

• Nested module contexts

module Foo where
  module Bar where
  module Baz where

=>

module Foo where {
  module Bar where {};
  module Baz where {};
};

We are currently using a variant of early scheduling but there are smarter alternatives in the world that may come at a low enough computational cost to be useful. See pretty much everything Cliff Click has ever written.

Description

Right now, diagnostics contain a reference to a node in the Syntax tree or token stream. This is really powerful, because it means we can just walk up the tree to get more context when we want to print
an expression out -- and because of the libSyntax-style AST, we can faithfully reprint the code from the original file, with all whitespace intact, back to a string.

We need to find a good predictable set of rules for

• How far to walk up the tree for context
• What textual ornamentation we want for the code (^ and ~~~~~ for pointing and highlights?)
• How to highlight specific expressions in the printed code
• Any other special things we want to do (Rust has some really cool ASCII art diagnostics!)

Currently, the GIRWriter doesn't really like Types all that much. This is current output of Tests/Seismography/switch.gir:

module switch where
@equal : (TYPE, TYPE, TYPE) -> ⊥ {
-- %0                                             -- users: %16, %24, %28, %5
-- %1                                             -- users: %17, %25, %29, %9, %21
-- %2                                             -- users: %14, %18, %26, %30
bb0(%0, %1, %2):
  %3 = function_ref @bb1                          -- user: %5
  %4 = function_ref @bb2                          -- user: %5
  switch_constr %0 ; example.Nat.z : %3 ; example.Nat.s : %4 -- id: %5

-- %6                                             -- users: %12
bb1(%6):
  %7 = function_ref @bb5                          -- user: %9
  %8 = function_ref @bb6                          -- user: %9
  switch_constr %1 ; example.Nat.z : %7 ; example.Nat.s : %8 -- id: %9

-- %10                                            -- users: %13
bb2(%10):
  %11 = function_ref @equal                       -- user: %14
  %12 = copy_value %6                             -- user: %14
  %13 = copy_value %10                            -- user: %14
  apply %11(%12 ; %13 ; %2) : ⊥                   -- id: %14

bb3:
  %15 = data_init_simple example.Bool.false       -- user: %18
  destroy_value %0                                -- id: %16
  destroy_value %1                                -- id: %17
  apply %2(%15) : TYPE                            -- id: %18

bb4:
  %19 = function_ref @bb3                         -- user: %21
  %20 = function_ref @bb4                         -- user: %21
  switch_constr %1 ; example.Nat.z : %19 ; example.Nat.s : %20 -- id: %21

bb5(%22):
  %23 = data_init_simple example.Bool.false       -- user: %26
  destroy_value %0                                -- id: %24
  destroy_value %1                                -- id: %25
  apply %2(%23) : TYPE                            -- id: %26

bb6:
  %27 = data_init_simple example.Bool.true        -- user: %30
  destroy_value %0                                -- id: %28
  destroy_value %1                                -- id: %29
  apply %2(%27) : TYPE                            -- id: %30

} -- end gir function equal

Ideally, it should look closer to this:

@equal : (example.Nat) -> (example.Nat) -> (example.Bool -> _) {
equal(%0 : example.Nat ; %1 : example.Nat ; %return : (example.Bool) -> _):
  %2 = function_ref @bb1
  %3 = function_ref @bb2
  switch_constr %0 : example.Nat ; case example.Nat.z : %2 ; case example.Nat.s : %3

bb1:
  %4 = function_ref @bb3
  %5 = function_ref @bb4
  switch_constr %1 : example.Nat ; case example.Nat.z : %4 ; case example.Nat.s : %5

bb2(%6 : example.Nat):
  %7 = function_ref @bb5
  %8 = function_ref @bb6
  switch_constr %1 : example.Nat ; case example.Nat.z : %7 ; case example.Nat.s : %8

bb3:
  %9 = data_init_simple example.Bool.true : example.Bool
  destroy_value %0 : example.Nat
  destroy_value %1 : example.Nat
  apply %return(%9) : (example.Bool) -> _

bb4(%10 : example.Nat):
  %11 = data_init_simple example.Bool.false : example.Bool
  destroy_value %0 : example.Nat
  destroy_value %1 : example.Nat
  apply %return(%11) : (example.Bool) -> _

bb5:
  %12 = data_init_simple example.Bool.false : example.Bool
  destroy_value %0 : example.Nat
  destroy_value %1 : example.Nat
  apply %return(%12) : (example.Bool) -> _

bb6(%13 : example.Nat):
  %14 = function_ref @equal
  %15 = copy_value %6 : example.Nat
  %16 = copy_value %13 : example.Nat
  apply %14(%15 ; %16 ; %return) : (example.Nat) -> (example.Nat) -> (example.Bool -> _)
}

As part of GraphIR verification we need to check scheduled continuations balance their books properly. Verification must occur along block boundaries because we probably won’t be scheduling destroys any earlier than that.

Relates to #108 and #99.

Hi :)
You both know me, so I’ll jump right in.

I can:

• Model and design data structures. I kinda love it.
• Solve Heuristic Search problems. I’m familiar with A* and many of its recursive and its non-optimal friends.
• Related: also CSP problems, beyond basic backtracking.
• Program very well in C, C#, Java and Python. And anything similar.
• Learn new languages
• Idk, I’ve been TA of CS and a student of CS for many years. I have some or a lot of experience in many areas. You can ask me for if I know something in particular ^^

I haven’t:

• Built a compiler
• Mastered Swift (yet)
• Mastered any full-blown Functional Language (yet).
• Bought a Mac (I work on Linux)
• Got much time until December (uni is a bitch here :p)

Given this, how can I help?

Is there a todo list already? I’ve read #9, which is super cool btw, but it looks more like a macro-design.

How can I help? Gimme Starter Tasks. I wanna learn :3

Sema is aware of absurd patterns, which allow one to omit the body of a function when pattern clauses cause contradictions.

proj : forall {n : N} {X : Type} → Vec X n → Fin n → X
proj [] ()
proj (cons x xs) zero = x
proj (cons x xs) (suc i) = proj xs i

The syntax for this needs to be added to the grammar and to the parser. Scope check need not concern itself with whether performing an inversion on the parameter will introduce a contradiction, it just needs to lower down to an empty Clause.Body.

Comment

Version

cadf474

Environment

All environments

Description

Any expression that begins with an identifier parses incorrectly when parenthesized, because the parser treats it as a typed parameter.

Steps To Reproduce

fool.silt:1:20: error: unexpected token ')' (expected ':')
foo a b c = (a b c)
                  ^ 

Expected Result

That should just parse as a ParenExpr with an ApplicationExpr inside.

Actual Result

The error above.

Additional Information

We should do better at detecting typed parameters.

Description

Graph IR is, fundamentally, a set of interconnected nodes. That doesn't lend itself well to SSA construction, so we instead must 'schedule' operations to establish an ordering of primitive operations and yield us a form amenable to SSA translation.

This is also the time where we infer the necessary destroy/copy operations via the ownership characteristics of Continuation parameters.

Primitive Operations

In #91, @CodaFi started detailing some primitive operations, each of which needs a representation for scheduling.

(These are probably the wrong descriptions and semantics, but I want them written down.)

Implementing references as QualifiedNames is a brittle strategy. It would help to implement some kind of DeclRef enum that yields additional information about names in GIR. Predicated on #99, obviously.

Use splitting trees and some algebraic elbow grease to implement exhaustiveness checking. For reference, see Agda.

Can we have HList / HMap / HSet such that they can be basis of defining structural and both nominative record types. Nominative typing need not mimic OO conventions faithfully but many of what can be done with OO should be doable using above. Also the ability to defining structural data like XML or JSON based these structures. Also you should be easily move from purely structural data representation to graph based hierarchical data and back again easily.

Similar to regular and canonical SIL, it would be nice to have some kind of delimiter that tells you whether a given GIR file contains pre or post optimization code. This can be implemented as a special comment or pragma in the file.

The GIR Parser currently requires the entry block be named the same as the function, but the GIRWriter renumbers it as bb0 anyways. While parsing, references to the function name should just point at the top-level continuation.

@foo : A -> B -> C -> ... -> _ {
bb0(%0 : A ; %1 : B ; %2 : C ; ... ; %return : (Z -> _)):
 -- etc.

bbN:
  %k = function_ref @foo -- points to bb0
}

Implement an unreachable terminator PrimOp that signals that the flow of control must never reach that particular continuation. This will be helpful when compiling pattern matching initially because there is currently no exhaustiveness check (#102).

Just in case we start getting external contributions, I’d like to have a simple set of rules we can point to.

We're currently trapped between a rock and a hard place - a crash in Swift 5.0 and a regression in Swift 5.1. We oughta undo #152 when https://bugs.swift.org/browse/SR-10576 gets resolved.

The GIR parser is currently a hacked-together mess that is relying on the Silt parser to do the heavy lifting. If we're doing this anyways, let's just go all the way and give it some libSyntax nodes and a proper place in the parser.

While we're at it we should take a cue from SIL and let Silt and GIR terms live alongside one another.

The current README is bare, and we have a lot of information that we haven’t explained fully.

Given the requirements, we expect the following phase structure

• Silt: CLI and Executable
• Drill (baby drill): Frontend, Driver
• Lithosphere: SyntaxGen, libSyntax, AST
• Crust: Parse, Shine
• Moho: ScopeCheck, Name Binding
• Mantle: Elaboration into Core Type Theory, TypeChecking
• Mesosphere: Lower TT to Thorin
• Outer Core: Optimizations
• Inner Core: Lower Thorin to LLVM IR

Version

eaace937

Environment

macOS, though this is universal.

Description

Right now, if you open a file without specifying a module, you get this unsatisfying diagnostic:

id x = x

issue.silt:1:1: error: unexpected token 'id' (expected 'module')

I'd prefer to see:

• The parser handle recovery, usually by making a dummy module.
• A better diagnostic that tells the user that a module is required at the top of every file.

Additional Information

You could accomplish this by doing a check in Parser.parseModule and providing another, better diagnostic. You'd then need to update the diagnostic test in DiagnosticTests/Resources/no-module.silt.

Part of #99: We must mangle the full module name into the name of a term as well as normalize Arbitrary Unicode Garbage in symbol names. The GIRWriter can then be updated to account for this.

Implement a general lowering algorithm for declarations and expressions. Implementations are up in the air at the moment. This issue is the umbrella for all others.

Add partial_apply to create a closure by applying a function value to a partial
sequence of its arguments.

We should run SwiftLint and make sure we keep to the LLVM-esque coding style throughout this project.

Part of #99 because requirements will change as we flesh out the lowering algorithm.

A general lowering algorithm from Schedule GraphIR is given in Thorin. This issues serves as an umbrella for our version of this lowering algorithm.