brendanzab

(** This is a demonstration of implementing interpreters in an extensible way
    that offers a partial solution to the expression problem. The idea is that
    the language can be extended with more features after the fact, without
    altering previous definitions. It also has the benefit of grouping the
    related extensions to the syntax and semantic domains together with the
    relevant evaluation rules in a per-feature way.

    This approach used is similar to the one described by Matthias Blume in
    {{:https://www.microsoft.com/en-us/research/video/records-sums-cases-and-exceptions-row-polymorphism-at-work/}
    Records, sums, cases, and exceptions: Row-polymorphism at work}.

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 {

kyoDralliam

From Equations Require Import Equations.
From Coq Require Import ssreflect.

Section Defs.
  Context {A : Type} (R : A -> A -> Prop).

  Definition entire := forall x, exists y, R y x.

  Definition idc_from a0 :=
    exists f : nat -> A, f 0 = a0 /\ forall n, R (f (S n)) (f n).

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.