Agnishom

Require Export Setoid.
Require Export Relation_Definitions.

Section ASet.

Declare Scope aset_scope.
Delimit Scope aset_scope with aset. (* so that we can write term%aset *)

Open Scope aset_scope.

Agnishom

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.
Require Import Coq.Wellfounded.Lexicographic_Product.
Require Import Coq.Arith.Wf_nat.
Require Import Arith. 

Import ListNotations.

Require Import Coq.Init.Nat.
Require Import Lia.

Agnishom

// g++ -o boostregex-test boostregex-test.cpp -lboost_regex

#include <fstream>
#include <vector>
#include <string>
#include <iostream>
#include <sstream>
#include <iomanip>
#include <chrono>
#include <boost/regex.hpp> 

Agnishom

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.

Agnishom

Require Import Coq.Lists.List.
Require Import Coq.Relations.Relation_Operators.

Import ListNotations.

Require Import Coq.Init.Nat.

Require Import Recdef.
Require Import FunInd.
Require Import Coq.Program.Wf.

Agnishom

Require Import Coq.Lists.List.

Declare Scope regex_scope.
Open Scope regex_scope.

Section Regex.

Variable (A : Type).

Inductive Regex : Type :=

Agnishom

(* 
  
  Some lemmas that can be used in conjunction with those in Coq.Lists.List
  
  See https://coq.inria.fr/library/Coq.Lists.List.html
 
 *)

 Require Import Lia.
 Require Import Coq.Lists.List.

Agnishom

#include <iostream>
#include <string>
#include <pcre.h>
#include <chrono>

using namespace std;

int main() {
    string pattern;
    string input;

Agnishom

use std::collections::VecDeque;
use std::cell::RefCell;
use std::rc::Rc;
use std::cell::Ref;

pub mod vllsimple;
use vllsimple::*;

struct part_man{
    // pools

Agnishom

use std::collections::VecDeque;

// compute the inverse relation given a function
fn inverse_fn(n: usize, f: &Vec<usize>) -> Vec<Vec<usize>> {
    let mut inverse_f = vec![vec![]; n];
    for i in 0..n {
        inverse_f[f[i]].push(i);
    }
    inverse_f
}