gabriel-fallen

theory Compiler_Demo
  imports Main
begin

type_synonym 'a binop = "'a ⇒ 'a ⇒ 'a"

datatype ('a, 'v) expr
  = Const 'v
  | Var 'a
  | BinOp "'v binop" "('a, 'v) expr" "('a, 'v) expr"

gabriel-fallen

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--higherorder" @-}

module TreeSort where

import Prelude hiding ((.), concat, filter, foldr, map)
import Language.Haskell.Liquid.ProofCombinators


data List a = Nil | Cons a (List a)

gabriel-fallen

theory Radix
imports Main
begin

primrec fold_right :: "('a ⇒ 'b ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b" where
"fold_right f x [] = x" |
"fold_right f x (h#t) = f h (fold_right f x t)"

primrec ordered :: "('a ⇒ 'b::ord) list ⇒ 'a ⇒ 'a ⇒ bool" where
"ordered [] _ _ = True" |

gabriel-fallen

module Parser where

import           Control.Monad.Cont
import           Control.Monad.Except
import           Data.ByteString
import           Streaming
import qualified Streaming.Prelude as S
import           Xeno.Streaming

-- | A record we want to parse from beneath unknown layers of XML

gabriel-fallen

[
  {
    "name": "Home",
    "url": "/"
  },
  {
    "name": "About",
    "url": "/about",
    "submenu": [
      {

gabriel-fallen

<?xml version='1.0' encoding='utf-8'?>
<scheme description="" title="" version="2.0">
	<nodes>
		<node id="0" name="Datasets" position="(246.0, 333.0)" project_name="Orange3" qualified_name="Orange.widgets.data.owdatasets.OWDataSets" title="Datasets" version="" />
		<node id="1" name="Data Table" position="(424.0, 61.0)" project_name="Orange3" qualified_name="Orange.widgets.data.owtable.OWDataTable" title="Data Table" version="" />
		<node id="2" name="Data Info" position="(298.0, 69.0)" project_name="Orange3" qualified_name="Orange.widgets.data.owdatainfo.OWDataInfo" title="Data Info" version="" />
		<node id="3" name="Naive Bayes" position="(445.0, 446.0)" project_name="Orange3" qualified_name="Orange.widgets.model.ownaivebayes.OWNaiveBayes" title="Naive Bayes" version="" />
		<node id="4" name="Test &amp; Score" position="(646.0, 444.0)" project_name="Orange3" qualified_name="Orange.widgets.evaluate.owtestlearners.OWTestLearners" title="Test &amp; Score" version="" />
		<node id="5" name="ROC Analysis" pos

gabriel-fallen

[
  {
    "thumb": "https://photos.smugmug.com/Humor/Lambdacats/i-96QX5wH/2/3729c284/Ti/eager%20cat%20is%20eager%2C%20lazy%20cat%20is%20lazy-Ti.jpg",
    "full": "https://photos.smugmug.com/Humor/Lambdacats/i-96QX5wH/2/3729c284/M/eager%20cat%20is%20eager%2C%20lazy%20cat%20is%20lazy-M.jpg"
  },
  {
    "thumb": "https://photos.smugmug.com/Humor/Lambdacats/i-4mxFBrm/2/3ea8829f/Ti/flip%20concatMap-Ti.jpg",
    "full": "https://photos.smugmug.com/Humor/Lambdacats/i-4mxFBrm/2/3ea8829f/S/flip%20concatMap-S.jpg"
  }
]

gabriel-fallen

namespace Test

open AbstractAnalysis.Common
open Yard.Generators.Common.DataStructures
open Yard.Generators.GLL
open Yard.Generators.GLL.AbstractParser
open GrammarCombinator.Combinators


module Test =

gabriel-fallen

namespace Tests

open System.Diagnostics
open NUnit.Framework

open AbstractAnalysis.Common
open Yard.Generators.Common.DataStructures
open Yard.Generators.GLL.AbstractParser
open Yard.Generators.GLL.ParserCommon
open GrammarCombinator.Combinators

gabriel-fallen

theory Fibonacci_Sums
imports Main
begin

(* Isabelle/HOL/Isar *)

section \<open>Fibonacci numbers and their sums\<close>

fun fib :: "nat \<Rightarrow> nat" where
"fib 0 = 0" |