Library zoo.common.format

Require Import Stdlib.Strings.Ascii.

Require Import stdpp.gmap.

Require Import zoo.prelude.
Require Import zoo.common.string.
Require Import zoo.options.

Implicit Type str pref suff var val : string.

Definition format۰env :=
  gmap string string.
Implicit Type env : format۰env.

Module parse.
  Notation assign :=
    "="%char.
  Notation sep :=
    ";"%char.
  Notation hole_beg :=
    "{"%char.
  Notation hole_end :=
    "}"%char.

  Definition binding str :=
    let '(var, val) := split_on assign str in
    let val := default var val in
    (var, val).

  Variant insideness :=
    | Inside
    | Outside.

  Fixpoint go env str res :=
    match str with
    | "" ⇒
        Some (String.rev res)
    | String hole_beg str ⇒
        hole env str res ""
    | String chr str ⇒
        go env str (String chr res)
    end
  with hole env str res acc :=
    match str with
    | "" ⇒
        None
    | String hole_beg str ⇒
        hole_variable env str res acc ""
    | String hole_end str ⇒
        match env !! String.rev acc with
        | None ⇒
            go env str (acc +:+ res)
        | Some val ⇒
            go env str (String.rev val +:+ res)
        end
    | String sep str ⇒
        match env !! String.rev acc with
        | None ⇒
            hole' env str res ""
        | Some val ⇒
            hole_finish env str (String.rev val +:+ res) Outside
        end
    | String chr str ⇒
        hole env str res (String chr acc)
    end
  with hole' env str res acc :=
    match str with
    | "" ⇒
        None
    | String hole_beg str ⇒
        hole_variable env str res acc ""
    | String hole_end str ⇒
        go env str (acc +:+ res)
    | String sep str ⇒
        hole_finish env str (acc +:+ res) Outside
    | String chr str ⇒
        hole' env str res (String chr acc)
    end
  with hole_variable env str res acc var :=
    match str with
    | "" ⇒
        None
    | String hole_end str ⇒
        match env !! String.rev var with
        | None ⇒
            hole_next env str res Outside
        | Some val ⇒
            hole' env str res (String.rev val +:+ acc)
        end
    | String chr str ⇒
        hole_variable env str res acc (String chr var)
    end
  with hole_finish env str res state :=
    match str with
    | "" ⇒
        None
    | String hole_beg str ⇒
        hole_finish env str res Inside
    | String hole_end str ⇒
        if state is Inside then
          hole_finish env str res Outside
        else
          go env str res
    | String _ str ⇒
        hole_finish env str res state
    end
  with hole_next env str res state :=
    match str with
    | "" ⇒
        None
    | String hole_beg str ⇒
        hole_next env str res Inside
    | String hole_end str ⇒
        if state is Inside then
          hole_next env str res Outside
        else
          go env str res
    | String sep str ⇒
        hole' env str res ""
    | String _ str ⇒
        hole_next env str res state
    end.
  Definition format env str :=
    go env str "".
End parse.

Definition format۰env۰of_bindings bdgs env :=
  foldr (λ p, <[p.1 := p.2]>) env bdgs.
Definition format۰env۰of_strings strs :=
  format۰env۰of_bindings (parse.binding <$> strs).
Definition format۰env۰of_string str :=
  format۰env۰of_strings (String.words str).

Definition format fmt env :=
  parse.format env fmt.

Goal format "{}" ∅ = Some "".
Goal format "{}" {["":="!"]} = Some "!".

Goal format "{1}" {["1":="one"]} = Some "one".
Goal format "{1}" ∅ = Some "1".

Goal format "{1} {2}" {["1":="one";"2":="two"]} = Some "one two".

Goal format "{1;∅}" ∅ = Some "∅".
Goal format "{1;∅}" {["1":="one"]} = Some "one".

Goal format "{1;}" ∅ = Some "".
Goal format "{1;}" {["1":="one"]} = Some "one".

Goal format "{({1});∅}" ∅ = Some "∅".
Goal format "{({1});∅}" {["1":="one"]} = Some "(one)".

Goal format "{({1});({2})}" ∅ = Some "".
Goal format "{({1});({2})}" {["1":="one"]} = Some "(one)".
Goal format "{({1});({2})}" {["2":="two"]} = Some "(two)".

Goal format "{({1});({2});∅}" ∅ = Some "∅".
Goal format "{({1});({2});∅}" {["1":="one"]} = Some "(one)".
Goal format "{({1});({2});∅}" {["2":="two"]} = Some "(two)".

Goal format "{{1}-{2}}" ∅ = Some "".
Goal format "{{1}-{2}}" {["1":="one"]} = Some "".
Goal format "{{1}-{2}}" {["2":="two"]} = Some "".
Goal format "{{1}-{2}}" {["1":="one";"2":="two"]} = Some "one-two".

Goal format "{{1}-{2};∅}" ∅ = Some "∅".
Goal format "{{1}-{2};∅}" {["1":="one"]} = Some "∅".
Goal format "{{1}-{2};∅}" {["2":="two"]} = Some "∅".
Goal format "{{1}-{2};∅}" {["1":="one";"2":="two"]} = Some "one-two".