bollu

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The compiler panics with the error:

bollu

-- example on parsing arith language via macros
inductive Arith: Type :=
   | Mul : Arith -> Arith -> Arith -- e :* f
   | Symbol : String -> Arith -- variable

declare_syntax_cat arith

syntax term : arith -- int for Arith.Int
syntax str : arith -- strings for Arith.Symbol
syntax:70 arith "*" arith : arith -- Arith.Mul

bollu

nductive Foo
| mk: Int -> Foo

instance : Inhabited Foo where
  default := Foo.mk 42

constant odd : Int -> Foo
constant even : Int -> Foo

-- | in reality these are partial mutually defined functions.

bollu

inductive Maybe (a : Type) : Type where 
| ok: a -> Maybe a
| err: Maybe a

structure P (a: Type) where 
   runP: String -> Maybe (String × a)

def ppure {a: Type} (v: a): P a := { runP :=  λ s => Maybe.ok (s, v) }

def pbind {a b: Type} (pa: P a) (a2pb : a -> P b): P b := 

bollu

#include <iomanip>
#include <iostream>
#include <map>
#include <queue>
#include <set>
#include <vector>
using namespace std;
using ll = long long;
using rr = double;

bollu

C <-g- D <-lim-   (J -> D) <-f._ -  (J -> C)
C      D          (J -> D)          (J -> C)
C -f-> D -const-> (J -> D)  -g._ -> (J -> C)

bollu

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
type Nat f g = forall x. f x -> g x
type Hom a b = a -> b

class Indexable f where 
    type family IxTy f :: *

bollu

define i8* @l_even(i8* %0) !dbg !3 {
  %2 = call i8* @lean_unsigned_to_nat(i64 0), !dbg !7
  %3 = call i8 @lean_nat_dec_eq(i8* %0, i8* %2), !dbg !9
  %4 = icmp eq i8 %3, 0, !dbg !10
  br i1 %4, label %5, label %9, !dbg !11

5:                                                ; preds = %1
  %6 = call i8* @lean_unsigned_to_nat(i64 1), !dbg !12
  %7 = call i8* @lean_nat_sub(i8* %0, i8* %6), !dbg !13
  %8 = call i8* @l_odd(i8* %7), !dbg !14

bollu

In my opinion, one of the problems with MLIR's freedom of operation semantics is that we have no idea what the Region attached to an Operation actually means. Hence, it's impossible to automatically extend well-known SSA constructs such as GVN, CSE, ... into Regions, simply because we have no idea about the dominance relationship between the parent region containing the operation, and the child regions of the operation.

Here's a proposal on how we fix this. We add two three instructions into the base IR:

run: args * Region -> value
callcc: label * args * Region -> ()

bollu

/usr/bin/env python3
N = 10
def p(x): print(x, end="")

# forward decl
p("int even(")
for i in range(N):
    if i > 0: p(", ")
    p("int")
p(");\n");