bollu

;;;; -*- Mode: Common-Lisp; Author: Siddharth Bhat -*-
;;;; https://google.github.io/styleguide/lispguide.xml 
;;;; https://jtra.cz/stuff/lisp/sclr/index.html
;;;; https://lispcookbook.github.io/cl-cookbook/data-structures.html
;;;; https://github.com/bollu/mlir-hoopl-rete/blob/master/reading/hoopl-proof-lerner.pdf
;;;; https://learnxinyminutes.com/docs/common-lisp/
;;;; https://lispcookbook.github.io/cl-cookbook/clos.html
;;;; https://malisper.me/debugging-lisp-part-1-recompilation/

;;; errors and restarts:

bollu

Report for stdlib
stdlib [0]           (    2 single benchmarks)
	 wall-clock mean =       241.(113), deviation =   10.59262%

stdlib [1]           (    2 single benchmarks)
	 wall-clock mean =       211.(160), deviation =   20.19648%

Equal program blocks
	 stdlib [0]  ⟷   stdlib [1]
		 wall-clock confidence =   61%, speed up =     12.42%

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