mukeshtiwari

From Coq Require Import 
Relation_Operators Utf8 Psatz Wf_nat.


Section Morp.

  Variable A : Type.
  Variable B : Type.
  Variable leA : A -> A -> Prop. (* A relation on type A *)
  Variable leB : B -> B -> Prop. (* A relation on type B *)

Lapin0t

-- Source: Conor McBride
-- https://personal.cis.strath.ac.uk/conor.mcbride/fooling/Jigger.agda
module Jigger where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + n = n

alpaylan

Require Import Coq.Strings.String.
Require Import Ascii.

Local Open Scope nat_scope.

Inductive Rope :=
| Leaf : string -> nat -> Rope
| Node : Rope -> nat -> Rope -> Rope.

Definition mkRope (s : string) : Rope :=

AndrasKovacs

{-# language
  BlockArguments
, ConstraintKinds
, ImplicitParams
, LambdaCase
, OverloadedStrings
, PatternSynonyms
, Strict
, UnicodeSyntax
#-}

mukeshtiwari

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Import ListNotations.
Require Import Coq.Init.Nat.
Require Import Lia.
Require Import Relation_Definitions.

Declare Scope regex_scope.

AndrasKovacs

Garbage collection with zero cost at non-GC time

Every once in a while I investigate low-level backend options for PL-s, although so far I haven't actually written any such backend for my projects. Recently I've been looking at precise garbage collection in popular backends, and I've been (like on previous occasions) annoyed by limitations and compromises.

I was compelled to think about a system which accommodates precise relocating GC as much as possible. In one extreme configuration, described in this note, there

dreamsmasher

#![feature(fn_traits, unboxed_closures)]

macro_rules! orelse {
    (($($lhs:tt)+), $rhs:tt) => {$($lhs)+};
    ((), ($($rhs:tt)*)) => {$($rhs)*}
}

macro_rules! overload {
    (
        $v:vis fn $fn_name:ident {

jldodds

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope string_scope.

(* Make it print lists one item per line*)
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
  (format "[ '[' x ;  '//' y ;  '//' .. ;  '//' z ']' ]") : list_scope.

AndrasKovacs

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

kayceesrk

?- set_prolog_flag(occurs_check,true).

lookup([(X,A)|_],X,A).
lookup([(Y,_)|T],X,A) :- \+ X = Y, lookup(T,X,A).

/* Rules from the STLC lecture */

pred(D,DD) :- D >= 0, DD is D - 1.

type(_,u,unit,D) :- pred(D,_).