module Generic.PrimAtom.WebEditor where
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Char using (Char; primCharEquality)
open import Agda.Builtin.List using (List; []; _∷_)
open import Agda.Builtin.Nat using (Nat; zero; suc)
open import Agda.Builtin.Sigma using (_,_)
open import Agda.Builtin.String
using
( String
; primShowNat
; primShowString
; primStringAppend
; primStringFromList
; primStringToList
)
open import Cubical.Data.Maybe.Base using (Maybe; just; nothing)
import Cubical.Data.Maybe.Properties as MaybeProperties
import Cubical.Data.Empty as Empty
open import Generic.Core hiding (natAtom; stringAtom; boolAtom)
open import Generic.Certified
open import Generic.Default
open import Generic.NativeJson
open import Generic.PrimAtom
import FF.Json as Json
import FF.Json.Native as Native
import Cubical.Data.FinData.Base as FinData
import Generic.Json as GenericJson
infixr 5 _++_
_++_ : String → String → String
_++_ = primStringAppend
maybeMap : ∀ {A B : Type₀} → (A → B) → Maybe A → Maybe B
maybeMap f (just x) = just (f x)
maybeMap f nothing = nothing
maybeBind : ∀ {A B : Type₀} → Maybe A → (A → Maybe B) → Maybe B
maybeBind (just x) f = f x
maybeBind nothing f = nothing
primAtomJsonString : String → JsonValue
primAtomJsonString = Native.jstring
primAtomJsonNumber : Nat → JsonValue
primAtomJsonNumber = Native.jnumber
primAtomJsonTrue : JsonValue
primAtomJsonTrue = Native.jbool true
primAtomJsonFalse : JsonValue
primAtomJsonFalse = Native.jbool false
primAtomJsonNull : JsonValue
primAtomJsonNull = Native.jnull
primAtomJsonArrayNil : JsonValue
primAtomJsonArrayNil = Native.jarray []
primAtomJsonArrayCons : JsonValue → JsonValue → JsonValue
primAtomJsonArrayCons value (Json.array values) =
Native.jarray (value ∷ values)
primAtomJsonArrayCons value _ =
Native.jarray (value ∷ [])
lookupNat : ∀ {A : Type₀} → List A → Nat → Maybe A
lookupNat [] n = nothing
lookupNat (x ∷ xs) zero = just x
lookupNat (x ∷ xs) (suc n) = lookupNat xs n
parens : String → String
parens s = "(" ++ s ++ ")"
prependArg : String → String → String
prependArg arg rest = " " ++ arg ++ rest
showInt : Int → String
showInt (pos n) =
"(pos " ++ primShowNat n ++ ")"
showInt (negsuc n) =
"(negsuc " ++ primShowNat n ++ ")"
snoc : List Char → Char → List Char
snoc [] c = c ∷ []
snoc (x ∷ xs) c = x ∷ snoc xs c
lastSegmentChars : List Char → List Char → List Char
lastSegmentChars [] current = current
lastSegmentChars (c ∷ cs) current with primCharEquality c '.'
... | true = lastSegmentChars cs []
... | false = lastSegmentChars cs (snoc current c)
sourceConstructorName : String → String
sourceConstructorName name =
primStringFromList (lastSegmentChars (primStringToList name) [])
data PrimSourceExpr : Type₀ where
constructorExpr : String → List PrimSourceExpr → PrimSourceExpr
stringExpr : String → PrimSourceExpr
natExpr : Nat → PrimSourceExpr
intExpr : Int → PrimSourceExpr
boolExpr : Bool → PrimSourceExpr
mutual
renderSourceArgs : List PrimSourceExpr → String
renderSourceArgs [] = ""
renderSourceArgs (x ∷ xs) =
prependArg (renderSourceExpr x) (renderSourceArgs xs)
renderSourceExpr : PrimSourceExpr → String
renderSourceExpr (constructorExpr name args) =
parens (sourceConstructorName name ++ renderSourceArgs args)
renderSourceExpr (stringExpr s) = primShowString s
renderSourceExpr (natExpr n) = primShowNat n
renderSourceExpr (intExpr n) = showInt n
renderSourceExpr (boolExpr true) = "true"
renderSourceExpr (boolExpr false) = "false"
data AtomSourceIx : (a : PrimAtomCode) → PrimAtom a → Type₀ where
stringSourceIx : ∀ {s} → AtomSourceIx stringAtom s
natSourceIx : ∀ {n} → AtomSourceIx natAtom n
intSourceIx : ∀ {n} → AtomSourceIx intAtom n
boolSourceIx : ∀ {b} → AtomSourceIx boolAtom b
mutual
data CodeSourceIx {A : Type₀} (certified : CertifiedGeneric PrimAtoms A) :
∀ {d : TyDesc PrimAtoms (Generic.typeCount (base certified))} →
CodeIx PrimAtoms (Generic.desc (base certified)) d → Type₀ where
nodeSourceIx : ∀ {cs} {c : ListIx cs} {args} →
String →
ArgsSourceIx certified args →
CodeSourceIx certified {d = dataD cs} (nodeIx c args)
data FieldSourceIx {A : Type₀} (certified : CertifiedGeneric PrimAtoms A) :
∀ {f} →
FieldCodeIx PrimAtoms (Generic.desc (base certified)) f → Type₀ where
recSourceIx : ∀ {i} {x : CodeIx PrimAtoms (Generic.desc (base certified))
(Generic.desc (base certified) i)} →
CodeSourceIx certified x →
FieldSourceIx certified (recIx x)
atomSourceIx : ∀ {a} {x : PrimAtom a} →
AtomSourceIx a x →
FieldSourceIx certified (atomIx x)
data ArgsSourceIx {A : Type₀} (certified : CertifiedGeneric PrimAtoms A) :
∀ {c} →
ArgsCodeIx PrimAtoms (Generic.desc (base certified)) c → Type₀ where
[]SourceIx : ArgsSourceIx certified []ⁱ
_∷SourceIx_ : ∀ {f fs} {x : FieldCodeIx PrimAtoms (Generic.desc (base certified)) f}
{xs : ArgsCodeIx PrimAtoms (Generic.desc (base certified)) (con fs)} →
FieldSourceIx certified x →
ArgsSourceIx certified xs →
ArgsSourceIx certified (x ∷ⁱ xs)
data RootSourceIx {A : Type₀} (certified : CertifiedGeneric PrimAtoms A) :
∀ {r} →
RootCodeIx PrimAtoms (Generic.desc (base certified)) r → Type₀ where
rootDataSourceIx : ∀ {i} {x : CodeIx PrimAtoms (Generic.desc (base certified))
(Generic.desc (base certified) i)} →
CodeSourceIx certified x →
RootSourceIx certified (rootDataIx x)
rootAtomSourceIx : ∀ {a} {x : PrimAtom a} →
AtomSourceIx a x →
RootSourceIx certified (rootAtomIx x)
atomSourceExpr : ∀ {a x} → AtomSourceIx a x → PrimSourceExpr
atomSourceExpr {x = s} stringSourceIx = stringExpr s
atomSourceExpr {x = n} natSourceIx = natExpr n
atomSourceExpr {x = n} intSourceIx = intExpr n
atomSourceExpr {x = b} boolSourceIx = boolExpr b
mutual
codeSourceExpr : ∀ {A} {certified : CertifiedGeneric PrimAtoms A}
{d : TyDesc PrimAtoms (Generic.typeCount (base certified))}
{x : CodeIx PrimAtoms (Generic.desc (base certified)) d} →
CodeSourceIx certified x → PrimSourceExpr
codeSourceExpr (nodeSourceIx name args) =
constructorExpr name (argsSourceExpr args)
fieldSourceExpr : ∀ {A} {certified : CertifiedGeneric PrimAtoms A}
{f : FieldDesc PrimAtoms (Generic.typeCount (base certified))}
{x : FieldCodeIx PrimAtoms (Generic.desc (base certified)) f} →
FieldSourceIx certified x → PrimSourceExpr
fieldSourceExpr (recSourceIx source) = codeSourceExpr source
fieldSourceExpr (atomSourceIx source) = atomSourceExpr source
argsSourceExpr : ∀ {A} {certified : CertifiedGeneric PrimAtoms A}
{c : ConDesc PrimAtoms (Generic.typeCount (base certified))}
{xs : ArgsCodeIx PrimAtoms (Generic.desc (base certified)) c} →
ArgsSourceIx certified xs → List PrimSourceExpr
argsSourceExpr []SourceIx = []
argsSourceExpr (x ∷SourceIx xs) =
fieldSourceExpr x ∷ argsSourceExpr xs
rootSourceExpr : ∀ {A} {certified : CertifiedGeneric PrimAtoms A}
{r : RootDesc PrimAtoms (Generic.typeCount (base certified))}
{x : RootCodeIx PrimAtoms (Generic.desc (base certified)) r} →
RootSourceIx certified x → PrimSourceExpr
rootSourceExpr (rootDataSourceIx source) = codeSourceExpr source
rootSourceExpr (rootAtomSourceIx source) = atomSourceExpr source
atomSourceWitness : (a : PrimAtomCode) → (x : PrimAtom a) → AtomSourceIx a x
atomSourceWitness stringAtom x = stringSourceIx
atomSourceWitness natAtom x = natSourceIx
atomSourceWitness intAtom x = intSourceIx
atomSourceWitness boolAtom x = boolSourceIx
mutual
codeSourceWitnessForDesc : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(d : TyDesc PrimAtoms (Generic.typeCount (base certified))) →
(ListIx (constructorsOf d) → String) →
(x : CodeIx PrimAtoms (Generic.desc (base certified)) d) →
CodeSourceIx certified x
codeSourceWitnessForDesc certified (dataD cs) nameAt (nodeIx c args) =
nodeSourceIx (nameAt c)
(argsSourceWitness certified (lookup c) args)
codeSourceWitness : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(i : Fin (Generic.typeCount (base certified))) →
(x : CodeIx PrimAtoms (Generic.desc (base certified))
(Generic.desc (base certified) i)) →
CodeSourceIx certified x
codeSourceWitness certified i x =
codeSourceWitnessForDesc certified
(Generic.desc (base certified) i)
(CertifiedGeneric.constructorName certified i)
x
fieldSourceWitness : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(f : FieldDesc PrimAtoms (Generic.typeCount (base certified))) →
(x : FieldCodeIx PrimAtoms (Generic.desc (base certified)) f) →
FieldSourceIx certified x
fieldSourceWitness certified (fieldRec i) (recIx x) =
recSourceIx (codeSourceWitness certified i x)
fieldSourceWitness certified (fieldAtom a) (atomIx x) =
atomSourceIx (atomSourceWitness a x)
argsSourceWitness : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(c : ConDesc PrimAtoms (Generic.typeCount (base certified))) →
(xs : ArgsCodeIx PrimAtoms (Generic.desc (base certified)) c) →
ArgsSourceIx certified xs
argsSourceWitness certified (con []) []ⁱ = []SourceIx
argsSourceWitness certified (con (f ∷ fs)) (x ∷ⁱ xs) =
fieldSourceWitness certified f x ∷SourceIx
argsSourceWitness certified (con fs) xs
rootSourceWitnessForDesc : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(r : RootDesc PrimAtoms (Generic.typeCount (base certified))) →
(x : RootCodeIx PrimAtoms
(Generic.desc (base certified)) r) →
RootSourceIx certified x
rootSourceWitnessForDesc certified (rootData i) (rootDataIx code) =
rootDataSourceIx (codeSourceWitness certified i code)
rootSourceWitnessForDesc certified (rootAtom a) (rootAtomIx atom) =
rootAtomSourceIx (atomSourceWitness a atom)
rootSourceWitness : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(x : RootCodeIx PrimAtoms
(Generic.desc (base certified))
(Generic.root (base certified))) →
RootSourceIx certified x
rootSourceWitness certified x =
rootSourceWitnessForDesc certified (Generic.root (base certified)) x
RootSourceDenotes : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(code : RootCodeIx PrimAtoms
(Generic.desc (base certified))
(Generic.root (base certified))) →
PrimSourceExpr → Type₀
RootSourceDenotes certified code expr =
Σ[ witness ∈ RootSourceIx certified code ] rootSourceExpr witness ≡ expr
sourceExprOfRootCode : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
RootCodeIx PrimAtoms
(Generic.desc (base certified))
(Generic.root (base certified)) →
PrimSourceExpr
sourceExprOfRootCode certified code =
rootSourceExpr (rootSourceWitness certified code)
sourceExprOfRootCode-correct : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(code : RootCodeIx PrimAtoms
(Generic.desc (base certified))
(Generic.root (base certified))) →
RootSourceDenotes certified code
(sourceExprOfRootCode certified code)
sourceExprOfRootCode-correct certified code =
rootSourceWitness certified code , refl
sourceExprOfValue : ∀ {A} → CertifiedGeneric PrimAtoms A → A → PrimSourceExpr
sourceExprOfValue certified x =
sourceExprOfRootCode certified (Generic.encode (base certified) x)
sourceExprOfValue-correct : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(x : A) →
RootSourceDenotes certified
(Generic.encode (base certified) x)
(sourceExprOfValue certified x)
sourceExprOfValue-correct certified x =
sourceExprOfRootCode-correct certified (Generic.encode (base certified) x)
sourceExprOfValue-decodes : ∀ {A} (certified : CertifiedGeneric PrimAtoms A) →
(x : A) →
Generic.decode (base certified)
(Generic.encode (base certified) x) ≡ x
sourceExprOfValue-decodes certified = Generic.decode-encode (base certified)
atomSource : PrimAtomCode → Json.JsonValue → Maybe String
atomSource stringAtom (Json.atom Native.string s) =
just (primShowString s)
atomSource natAtom value =
maybeMap primShowNat (fromNativeJSON Native.numberFromJson value)
atomSource intAtom value =
maybeMap showInt (fromNativeJSON intFromNativeJSON value)
atomSource boolAtom (Json.atom Native.boolean true) =
just "true"
atomSource boolAtom (Json.atom Native.boolean false) =
just "false"
atomSource _ _ =
nothing
mutual
fieldSource : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
FieldDesc PrimAtoms (Generic.typeCount g) →
Json.JsonValue → Maybe String
fieldSource g (fieldRec i) value =
codeSource g i value
fieldSource g (fieldAtom a) value =
atomSource a value
argsSource : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
List (FieldDesc PrimAtoms (Generic.typeCount g)) →
List Json.JsonValue → Maybe String
argsSource g [] [] = just ""
argsSource g [] (_ ∷ _) = nothing
argsSource g (_ ∷ _) [] = nothing
argsSource g (f ∷ fs) (j ∷ js) =
maybeBind (fieldSource g f j) λ arg →
maybeMap (prependArg arg) (argsSource g fs js)
codeSource : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
Fin (Generic.typeCount g) →
Json.JsonValue → Maybe String
codeSource g i (Json.array (jc ∷ Json.array args ∷ [])) with Generic.desc g i
... | dataD cs =
maybeBind (GenericJson.fromNatJSON jc) λ cIx →
maybeBind (lookupNat cs cIx) λ where
(con fs) →
maybeBind (lookupNat (Generic.constructorNames g i) cIx) λ cName →
maybeMap (λ argText → parens (sourceConstructorName cName ++ argText))
(argsSource g fs args)
codeSource g i _ = nothing
rootSource : ∀ {A : Type₀} →
Generic PrimAtoms A → Json.JsonValue → Maybe String
rootSource g value with Generic.root g
... | rootData i = codeSource g i value
... | rootAtom a = atomSource a value
editorSpecificationJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue
editorSpecificationJsonValue g =
toSpecificationNativeJSON
primAtomCodeFromToNativeJSON
(specificationOf g)
editorSpecificationJsonValueRoundtrip : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
fromSpecificationNativeJSON
primAtomCodeFromToNativeJSON
(editorSpecificationJsonValue g)
≡ just (specificationOf g)
editorSpecificationJsonValueRoundtrip g =
Json.FromToJSON'.roundtrip
(genericSpecificationFromToNativeJSON primAtomCodeFromToNativeJSON)
(specificationOf g)
editorSpecificationJSON : ∀ {A : Type₀} → Generic PrimAtoms A → String
editorSpecificationJSON g =
Json.renderCompact (editorSpecificationJsonValue g)
editorValueJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → A → JsonValue
editorValueJsonValue g x =
toNativeJSON
(Json.FromToJSON'.to (genericFromToNativeJSON primAtomValueCodecs g))
x
editorValueJSON : ∀ {A : Type₀} → Generic PrimAtoms A → A → String
editorValueJSON g x =
Json.renderCompact (editorValueJsonValue g x)
tabulateListFrom : ∀ {A : Type₀} →
(count len : Nat) →
(Fin len → Fin count) →
(Fin count → A) →
List A
tabulateListFrom count zero shift f = []
tabulateListFrom count (suc len) shift f =
f (shift FinData.zero) ∷
tabulateListFrom count len (λ i → shift (FinData.suc i)) f
tabulateList : ∀ {A : Type₀} →
(count : Nat) → (Fin count → A) → List A
tabulateList count = tabulateListFrom count count (λ i → i)
editorDefaultCodeJsonValue : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
Fin (Generic.typeCount g) → JsonValue
editorDefaultCodeJsonValue g i with
defaultCodes primAtomDefaults (Generic.desc g) i
... | nothing = Native.jnull
... | just code =
GenericJson.toCodeJSON primAtomValueCodecs (Generic.desc g) code
editorDefaultCodeJsonValueRoundtrip : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
(i : Fin (Generic.typeCount g)) →
(code : CodeIx PrimAtoms (Generic.desc g) (Generic.desc g i)) →
defaultCodes primAtomDefaults (Generic.desc g) i ≡ just code →
GenericJson.fromCodeJSON
primAtomValueCodecs
(Generic.desc g)
(Generic.desc g i)
(editorDefaultCodeJsonValue g i)
≡ just code
editorDefaultCodeJsonValueRoundtrip g i code eq with
defaultCodes primAtomDefaults (Generic.desc g) i
... | nothing = Empty.rec (MaybeProperties.¬nothing≡just eq)
... | just found =
GenericJson.codeJSONRoundtrip primAtomValueCodecs (Generic.desc g) found
∙ cong just (MaybeProperties.just-inj found code eq)
editorDefaultsJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue
editorDefaultsJsonValue g =
Native.jarray
(tabulateList
(Generic.typeCount g)
(editorDefaultCodeJsonValue g))
editorProtocolJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue
editorProtocolJsonValue g =
Native.jobject
( ("version" , Native.jnumber (suc (suc zero)))
∷ ("specification" , editorSpecificationJsonValue g)
∷ ("defaults" , editorDefaultsJsonValue g)
∷ []
)
editorProtocolJSON : ∀ {A : Type₀} → Generic PrimAtoms A → String
editorProtocolJSON g =
Json.renderCompact (editorProtocolJsonValue g)
editorPayloadJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue
editorPayloadJsonValue g =
Native.jobject
( ("specification" , editorSpecificationJsonValue g)
∷ ("defaults" , editorDefaultsJsonValue g)
∷ []
)
editorPayloadJSON : ∀ {A : Type₀} → Generic PrimAtoms A → String
editorPayloadJSON g =
Json.renderCompact (editorPayloadJsonValue g)
editorPayloadWithValueJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → A → JsonValue
editorPayloadWithValueJsonValue g x =
Native.jobject
( ("specification" , editorSpecificationJsonValue g)
∷ ("defaults" , editorDefaultsJsonValue g)
∷ ("value" , editorValueJsonValue g x)
∷ []
)
editorPayloadWithValueJSON : ∀ {A : Type₀} →
Generic PrimAtoms A → A → String
editorPayloadWithValueJSON g x =
Json.renderCompact (editorPayloadWithValueJsonValue g x)
editorValueFromJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue → Maybe A
editorValueFromJsonValue g value =
fromNativeJSON
(Json.FromToJSON'.from (genericFromToNativeJSON primAtomValueCodecs g))
value
editorValueJsonValueRoundtrip : ∀ {A : Type₀} →
(g : Generic PrimAtoms A) →
(x : A) →
editorValueFromJsonValue g (editorValueJsonValue g x) ≡ just x
editorValueJsonValueRoundtrip g =
Json.FromToJSON'.roundtrip (genericFromToNativeJSON primAtomValueCodecs g)
certifiedEditorSourceFromValue : ∀ {A : Type₀} →
CertifiedGeneric PrimAtoms A →
JsonValue → Maybe String
certifiedEditorSourceFromValue certified value =
maybeMap
(λ x → renderSourceExpr (sourceExprOfValue certified x))
(editorValueFromJsonValue (base certified) value)
certifiedEditorSourceFromEncodedValue : ∀ {A : Type₀} →
(certified : CertifiedGeneric PrimAtoms A) →
(x : A) →
certifiedEditorSourceFromValue certified
(editorValueJsonValue (base certified) x)
≡ just (renderSourceExpr (sourceExprOfValue certified x))
certifiedEditorSourceFromEncodedValue certified x =
cong
(maybeMap (λ y → renderSourceExpr (sourceExprOfValue certified y)))
(editorValueJsonValueRoundtrip (base certified) x)
editorValueFromJsonValueOr : ∀ {A : Type₀} →
A → Generic PrimAtoms A → JsonValue → A
editorValueFromJsonValueOr fallback g value with editorValueFromJsonValue g value
... | just x = x
... | nothing = fallback
editorSourceFromValue : ∀ {A : Type₀} →
Generic PrimAtoms A → Json.JsonValue → Maybe String
editorSourceFromValue g value with editorValueFromJsonValue g value
... | nothing = nothing
... | just _ = rootSource g value
editorSourceFromJsonValue : ∀ {A : Type₀} →
Generic PrimAtoms A → JsonValue → Maybe String
editorSourceFromJsonValue = editorSourceFromValue
editorSourceFromValueOr : ∀ {A : Type₀} →
String → Generic PrimAtoms A → Json.JsonValue → String
editorSourceFromValueOr fallback g value with editorSourceFromValue g value
... | just source = source
... | nothing = fallback
editorSourceFromJsonValueOr : ∀ {A : Type₀} →
String → Generic PrimAtoms A → JsonValue → String
editorSourceFromJsonValueOr = editorSourceFromValueOr