regexp.syn

Require Import regexp.prelude.
Require Import regexp.expr.
Require regexp.lang.
Require Import regexp.concrete.universe.
Require Import regexp.concrete.function.
Require Import regexp.concrete.rule.

PHOAS based syntax for building regexps

Inductive t {B v : Type} : nat → Type :=
| Ret : expr.t v → t 0
| Bind : B → ∀ {n}, (expr.t v → t n ) → t (S n).

Arguments t : clear implicits.
Arguments Bind {B v} _ {n}.

The existentially quantified closed syntax tree

Definition T B n := ∀ v, t B v n.

Most syntactic operations on closed syntax trees begin with defining the corresponding operation with a suitably chosen variable type v. The internal module contains these functions and are meant to be used by the function of the same name defined at the top level.

Definition unret {B v}(bt : t B v 0) : expr.t v :=
  match bt with
  | Ret e ⇒ e
  end.

Definition unbind {B v m}(bt : t B v (S m)) : B × (v → t B v m ) :=
  match bt with
  | Bind b _ bfn ⇒ (b , fun v ⇒ bfn (single v))
  end.

Fixpoint sortOf (n : nat) : sort :=
  match n with
  | 0 ⇒ 𝟙
  | S m ⇒ (𝟙 ∐ sortOf m)
  end%con.

Definition vars v n := if n is m.+1 then (sortOf m ~> v)%con else option v.

Definition split {v n} : vars v (S n) → v × vars v n :=
  if n is m.+1 then fun vs : vars v (m.+2) ⇒ let (H,T) := unsum vs in (unconst H , T )
  else fun vs : vars v 1 ⇒ (unconst vs , None ).

Definition attach {v n} : (v × vars v n ) → vars v (S n) :=
  if n is m.+1 then fun vs ⇒ let (x,rest) := vs in (constant x ++ rest)%con
  else fun vs ⇒ constant vs .1.

Definition filled B v n := (vars B n × expr.t v)%type.

Fixpoint fill {B}{v : finType} {n} : vars v n → t B v n → filled B v n :=
  if n is m.+1 then fun vs bt ⇒ let (h,t) := split vs in
                              let (b,bfn) := unbind bt in
                              let (bs,e) := fill t (bfn h) in
                              (attach (b , bs ) , e )
  else fun _ bt ⇒ (None , unret bt ).

Definition alphabet := universe.typeOf \o sortOf.

Compiled expression that can be converted to hardware

Module internal.

  Fixpoint denote {B n}(re : t B B n) : expr.t B :=
    match re with
    | Ret r ⇒ r
    | Bind b _ bfn ⇒ denote (bfn (single b))
    end.

  Definition alloc m : vars (alphabet m) (m.+1) := function.from (fun x : sortOf m ⇒ x).

  Definition compile {B n}(re : t B (alphabet n) n.+1) : (sortOf n ~> B)%con × expr.t (alphabet n) :=
    fill (alloc n) re.

End internal.

Definition denote {B n}(re : T B n) : expr.t B := internal.denote (re B).

Definition compile {B n}(re : T B (n.+1)) : (sortOf n ~> B)%con × expr.t (alphabet n) := internal.compile (re (alphabet n)).

Custom syntax for regular expr

Declare Custom Entry rules.

Notation "'let' x ':=' b 'in' E"
  := (Bind b (fun x ⇒ E)) (in custom rules at level 70, right associativity, x ident, b constr,
          format "'let' x ':=' b 'in' '//' E"
        ).

Notation "'match' e"
  := (Ret e) (in custom rules at level 70, right associativity, e constr).

Definition makeRule {I n}(re : T (I → bool) (n.+1)) : Rule I :=
  let (bt, e) := compile re in
  {|
    letter := sortOf n;
    atomTable := bt;
    regexp := e
  |}.

Notation "[rule| e |]" := (makeRule (fun _ ⇒ e)) (e custom rules).

Example foo : Rule nat := [rule | let dgt := fun x ⇒ x < 10 in
                               let oct := fun x ⇒ x < 7 in
                               match many (dgt || oct)%re
                               |].