Tree editing scaffolds

Structures.agda

module Structures where

open import Data.Unit
open import Data.Product
open import Data.Empty
open import Data.Nat
open import Data.Fin
open import Data.Vec
open import Data.Maybe
open import Data.List
open import Data.String
open import Agda.Primitive
open import Agda.Builtin.Equality
open import Relation.Nullary.Decidable
open import Level hiding (zero;suc)

data Schema (n : ℕ) : Set where
  var : Fin n -> Schema n
  string : Schema n
  many : Schema n -> Schema n
  row : {m : ℕ} -> Vec (Schema n) m -> Schema n
  opt : {m : ℕ} -> Vec (Schema n) m -> Schema n

FullSchema : ℕ -> Set
FullSchema n = Vec (Schema n) n

⟦_⟧ : {n : ℕ} -> Schema n -> (Fin n -> Set) -> Set
Row : {n m : ℕ} -> Vec (Schema n) m -> (Fin n -> Set) -> Set
Opt : {n m : ℕ} -> Vec (Schema n) m -> (Fin n -> Set) -> Fin m -> Set

⟦ var i ⟧ K = K i
⟦ string ⟧ K = String
⟦ many x ⟧ K = List (⟦ x ⟧ K)
⟦ row xs ⟧ K = Row xs K
⟦ opt xs ⟧ K = Σ (Fin _) (Opt xs K)

Row [] K = ⊤
Row (x ∷ xs) K = ⟦ x ⟧ K × Row xs K

Opt (x ∷ xs) K zero = ⟦ x ⟧ K
Opt (x ∷ xs) K (suc i) = Opt xs K i

data µ {n : ℕ} (R : Vec (Schema n) n) (i : Fin n) : Set where
    con : (x : ⟦ Data.Vec.lookup R i ⟧ (µ R)) -> µ R i

data Scaffold {n : ℕ} (R : FullSchema n) : Schema n -> Set
Scaffolds : {n m : ℕ} (R : FullSchema n) -> Vec (Schema n) m -> Set

data Scaffold {n} R where
  sc-var : (i : Fin n) -> Scaffold R (Data.Vec.lookup R i) -> Scaffold R (var i)
  sc-string : (s : Schema n) -> String -> Scaffold R s
  sc-many : {s : Schema n} -> List (Scaffold R s) -> Scaffold R (many s)
  sc-row : {m : ℕ} -> {xs : Vec (Schema n) m} -> Scaffolds R xs -> Scaffold R (row xs)
  sc-opt : {m : ℕ} -> {xs : Vec (Schema n) m} -> (i : Fin m) -> Scaffold R (Data.Vec.lookup xs i) -> Scaffold R (opt xs)

data Context {n : ℕ} (R : FullSchema n) : Schema n -> Set

data Context {n} R where
  c-root : (s : Schema n) -> Context R s
  c-var : (i : Fin n) -> Context R (var i) -> Context R (Data.Vec.lookup R i)
  c-many : (s : Schema n) -> Context R (many s) -> Context R s -- missing prefix/suffix scaffolds.
  c-row : {m : ℕ} -> {xs : Vec (Schema n) m} -> (i : Fin m) -> Context R (row xs) -> Context R (Data.Vec.lookup xs i) -- missing other scaffolds
  c-opt : {m : ℕ} -> {xs : Vec (Schema n) m} -> (i : Fin m) -> Context R (opt xs) -> Context R (Data.Vec.lookup xs i)

Scaffolds R [] = ⊤
Scaffolds R (x ∷ xs) = Scaffold R x × Scaffolds R xs

minima : {n : ℕ} -> (R : FullSchema n) -> (s : Schema n) -> Scaffold R s
minima R (var x) = sc-string (var x) ""
minima R string = sc-string string ""
minima R (many s) = sc-many []
minima R (row x) = sc-row {!!}
minima R (opt x) = sc-string (opt x) ""

inject' : {n : ℕ} -> (R : FullSchema n) -> {s : Schema n} -> ⟦ s ⟧ (µ R) -> Scaffold R s
inject' R {var x₁} x = {!!}
inject' R {string} x = sc-string string x
inject' R {many s} x = {!!}
inject' R {row x₁} x = {!!}
inject' R {opt x₁} x = {!!}

complete : {n : ℕ} -> (R : FullSchema n) -> {s : Schema n} -> Scaffold R s -> Maybe (⟦ s ⟧ (µ R))
completeAll : {n : ℕ} -> (R : FullSchema n) -> {s : Schema n} -> List (Scaffold R s) -> Maybe (List (⟦ s ⟧ (µ R)))

complete R (sc-var i sc) = do y <- complete R sc
                              just (con y)
complete R (sc-string (var x₁) x) = nothing
complete R (sc-string string x) = just x
complete R (sc-string (many s) x) = nothing
complete R (sc-string (row x₁) x) = nothing
complete R (sc-string (opt x₁) x) = nothing
complete R (sc-many x) = completeAll R x
complete R (sc-row x) = {!completeRow R x!}
complete R (sc-opt i sc) = do y <- complete R sc
                              just (i , {!!})

Zipper : {n : ℕ} (R : FullSchema n) -> Set
Zipper {n} R = Σ (Schema n) (λ s -> Context R s × Scaffold R s)

up fir las prev next : {n : ℕ} {R : FullSchema n} -> Zipper R -> Maybe (Zipper R)

metaSchema : FullSchema 2
metaSchema = many (row (string ∷ var (suc zero) ∷ []))
           ∷ opt (string
                ∷ row []
                ∷ var (suc zero)
                ∷ many (var (suc zero))
                ∷ many (row (string ∷ var (suc zero) ∷ []))
                ∷ [])
           ∷ []