Alexander Chichigin gabriel-fallen
gabriel-fallen
/ wasm.pi
Last active
September 1, 2022 18:59
Simple AST->WASM (text format) compiler.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| %% Primitive AST->WASM (text format) compiler. | |
| %% Type = | |
| %% | bool | |
| %% | int | |
| %% | float | |
| %% | void | |
| show_type(bool) = "i32". | |
| show_type(int) = "i32". |
gabriel-fallen
/ insert_sort_loop_inv_preserv_why3.v
Created
October 6, 2019 17:08
Verifying insertion sort with Why3.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (* This file is generated by Why3's Coq driver *) | |
| (* Beware! Only edit allowed sections below *) | |
| Require Import BuiltIn. | |
| Require BuiltIn. | |
| Require HighOrd. | |
| Require int.Int. | |
| Require map.Map. | |
| (* Why3 assumption *) | |
| Inductive ref (a:Type) := |
gabriel-fallen
/ Fibonacci_Sums.thy
Created
August 18, 2019 12:42
Some theorems about Fibonacci numbers sums in Isabelle/HOL
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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" | |
gabriel-fallen
/ AliasingTests.fs
Last active
March 12, 2019 15:31
Trying to build an aliasing CFPQ.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ gallery.json
Created
September 26, 2018 16:17
Sample image gallery with thumbnails data.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| [ | |
| { | |
| "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
/ kickstarter.ows
Created
September 13, 2018 18:32
Orange example workspace with Kickstarter dataset.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <?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 & Score" position="(646.0, 444.0)" project_name="Orange3" qualified_name="Orange.widgets.evaluate.owtestlearners.OWTestLearners" title="Test & Score" version="" /> | |
| <node id="5" name="ROC Analysis" pos |
gabriel-fallen
/ Parser.hs
Last active
March 6, 2018 17:03
Pseudohaskell for continuation-based XML SAX-parser
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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
/ Radix.thy
Created
November 12, 2017 14:55
Equational proof that "treesort = radixsort" in Isabelle
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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" | |