llelf

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}

module ALaCarte where

llelf

#define KXVER 3
#include"k.h"
#include<stdio.h>

#define PK(s,x) O("%15s: %p[r=%d] n=%lld %d..\n",s,x,x->r,x->n,*kI(x))

I main(){
  I i=42;
  K top1=ktn(KI,0), top2=ktn(KI,0), v=ktn(KI,0);
  jk(&top1,r1(v)); jk(&top2,r1(v));

llelf

Module   I32:=Int.     Module   I64:=Int64.
Notation i32:=I32.int. Notation i64:=I64.int.
Notation "[i32 i ]" := (I32.mkint i _)(format "[i32  i ]").
Notation "[i64 i ]" := (I64.mkint i _)(format "[i64  i ]").

Section core.

Inductive Nu := I of i32 | J of i64.
Inductive At := ANu of Nu | AC of ascii.
Inductive Ty := Ti|Tj|TL|Tc.

llelf

   what               k4/k7         k9              example    result                
  ---------------------------------------------------------------------------------
   each-left         a f\:b     a f\:b            (!3)*\:!2    (0 0;0 1;0 2)         
   each-right        a f/:b     a f/:b            (!3)*/:!2    (0 0 0;0 1 2)         
   fold                 f/v        f/v                */6 7    42                    
   fold w/initial     a f/v      a f/v             7*/11 13    1001                  
   scan                 f\v        f\v              -\1 1 1    1 0 -1                
   scan w/initial     a f\v      a f\v             3-\1 1 1    2 1 0                 

llelf

llelf

From QuickChick Require Import QuickChick.
From Coq        Require Import Program.
From mathcomp   Require Import ssreflect ssrfun ssrnat ssrbool eqtype seq.

Program Fixpoint itakep {A} (n:nat) (s:seq A) {measure n} : seq A :=
  if s isn't [::] then
    (if n <= size s as r return (n <= size s = r -> _)
       then fun pf => take n s
       else fun pf => s ++ itakep (n - size s) s) erefl
  else [::].