From 12167af880766c7e919378c9d4811200cbc90d4a Mon Sep 17 00:00:00 2001 From: pmbittner Date: Fri, 5 Apr 2024 22:42:55 +0200 Subject: [PATCH] repair FST-to-OC --- src/Translation/Lang/FST-to-OC.agda | 264 +++++++++++----------------- 1 file changed, 99 insertions(+), 165 deletions(-) diff --git a/src/Translation/Lang/FST-to-OC.agda b/src/Translation/Lang/FST-to-OC.agda index c3cfe406..0ed1cf40 100644 --- a/src/Translation/Lang/FST-to-OC.agda +++ b/src/Translation/Lang/FST-to-OC.agda @@ -5,7 +5,9 @@ module Translation.Lang.FST-to-OC (F : 𝔽) where open import Size using (Size; ↑_; _βŠ”Λ’_; ∞) +open import Data.Nat using (_β‰Ÿ_) open import Data.List using (List; []; _∷_; map) +open import Data.Product using (_,_) open import Relation.Nullary.Decidable using (yes; no; _because_; False) open import Relation.Binary using (Decidable; DecidableEquality; Rel) open import Relation.Binary.PropositionalEquality as Eq using (_≑_; refl) @@ -16,171 +18,103 @@ V = Rose ∞ mkArtifact = Artifactβˆˆβ‚›Rose Option = F +open import Framework.Relation.Expressiveness V + open import Framework.VariabilityLanguage open import Construct.Artifact as At using () import Lang.FST as FST --- open FST F using (FST; induction; fst-leaf) - -open import Framework.Relation.Expressiveness V - --- module _ {A : 𝔸} (_==_ : DecidableEquality A) where --- open FST.Impose F _==_ using (SPL; _β—€_; Feature; _::_; FSF; _⊚_) - --- -- translate-o : βˆ€ {i} β†’ A β†’ OC i A β†’ Feature --- -- translate-o a (b OC.-< cs >-) = {!!} --- -- translate-o a (O OC.❲ e ❳) = {!!} - --- -- left is base --- mutual --- embed : FST A β†’ OC ∞ A --- embed = induction OC._-<_>- - --- merge-trees : F β†’ List (OC ∞ A) β†’ F β†’ FST A β†’ List (OC ∞ A) --- merge-trees _ [] P t = P ❲ embed t ❳ ∷ [] --- merge-trees O (a OC.-< as >- ∷ inter) P (b FST.-< bs >-) with a == b --- ... | yes refl = a OC.-< merge O as P bs >- ∷ inter --- ... | no nope = O ❲ a OC.-< as >- ❳ ∷ merge-trees O inter P (b FST.-< bs >-) --- merge-trees O (Q ❲ e ❳ ∷ inter) P t = Q ❲ e ❳ ∷ merge-trees O inter P t - --- {-# TERMINATING #-} --- merge : F β†’ List (OC ∞ A) β†’ F β†’ List (FST A) β†’ List (OC ∞ A) --- merge _ ls _ [] = ls --- merge O ls P (t ∷ ts) = merge O (merge-trees O ls P t) P ts - --- record Intermediate : Set where --- constructor _:o:_ --- field --- name : F --- children : List (OC ∞ A) - --- translate' : List Intermediate β†’ List (OC ∞ A) --- translate' [] = [] --- translate' ((_ :o: cs) ∷ []) = cs --- translate' ((O :o: os) ∷ (P :o: ps) ∷ xs) = translate' ({!merge!} ∷ xs) - --- fromFeature : Feature β†’ Intermediate --- fromFeature (O :: (ts ⊚ _)) = O :o: map embed ts - --- start : List Feature β†’ List Intermediate --- start = map fromFeature - --- translate : SPL β†’ WFOC ∞ A --- translate (a β—€ fs) = Root a (translate' (start fs)) - -module _ (mkDec : (A : 𝔸) β†’ DecidableEquality A) where - data FeatureName : Set where - X : FeatureName - Y : FeatureName - - open import Data.Bool using (true; false; if_then_else_) - open import Data.Nat using (zero; suc; β„•) - open import Data.Fin using (Fin; zero; suc) - open import Data.List.Relation.Unary.All using (All; []; _∷_) - open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) - open import Framework.VariantMap V β„• - - import Lang.OC - open Lang.OC FeatureName using (OC; _❲_❳; WFOC; Root; opt; Configuration) - open Lang.OC.Sem FeatureName V mkArtifact - - open FST FeatureName using (_．_) - open FST.Impose FeatureName (mkDec β„•) using (SPL; _β—€_; _::_; _⊚_; unq) renaming (⟦_⟧ to FST⟦_⟧) - open FST.Framework FeatureName mkDec - - open import Data.EqIndexedSet - open import Data.Empty using (βŠ₯-elim) - - open import Data.Product using (_,_; βˆƒ-syntax) - open import Util.Existence using (¬Σ-syntax) - - counterexample : VMap 3 - counterexample zero = rose-leaf 0 - counterexample (suc zero) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ [] >-) ∷ [] >-) - counterexample (suc (suc zero)) = rose (0 At.-< rose (1 At.-< rose-leaf 3 ∷ [] >-) ∷ [] >-) - counterexample (suc (suc (suc zero))) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ rose-leaf 3 ∷ [] >-) ∷ [] >-) - - -- illegal' : βˆ€ {i : Size} β†’ βˆ„[ cs ∈ List (OC i β„•) ] (⟦ Root zero cs ⟧ β‰… counterexample) - -- illegal' ([] , fst , snd) with snd (suc zero) - -- ... | () - -- illegal' (x ∷ fst , snd) = {!!} - - -- illegal' : βˆ€ {i : Size} β†’ βˆ„[ e ∈ OC i β„• ] (βˆƒ[ O ] (βˆƒ[ xs ] (⟦ Root zero (opt O e ∷ xs) ⟧ β‰… counterexample))) - -- illegal' x = {!!} - open import Relation.Nullary.Negation using (Β¬_) - - nodup : βˆ€ {i : Size} {A : 𝔸} (a : A) (x y : OC i A) (zs : List (OC i A)) - β†’ Β¬ (βˆ€ (c : Configuration) β†’ (⟦ Root a (x ∷ y ∷ zs) ⟧ c ≑ rose-leaf a)) - nodup a x y zs sure with sure (Ξ» _ β†’ true) - nodup a (O ❲ e ❳) y zs sure | asd = {!!} - -- nodup a (b OC.-< bs >-) y zs sure with sure (Ξ» _ β†’ true) - -- ... | () - -- nodup a (O ❲ e ❳) (b OC.-< bs >-) zs sure with sure (Ξ» _ β†’ false) - -- ... | () - -- nodup a (O ❲ e ❳) (P ❲ f ❳) [] sure = {!!} - -- nodup a (O ❲ e ❳) (P ❲ f ❳) (z ∷ zs) sure = nodup a (P ❲ f ❳) z zs {!sure!} - -- nodup a (O ❲ e ❳) y zs (c , sure) with c O - -- nodup a (O ❲ e ❳) (P ❲ f ❳) [] (c , sure) | false with c P - -- nodup a (O ❲ e ❳) (P ❲ f ❳) [] (c , refl) | false | false = {!!} - -- nodup a (O ❲ e ❳) (P ❲ f ❳) [] (c , sure) | false | true = {!!} - -- nodup a (O ❲ e ❳) (P ❲ f ❳) (z ∷ zs) (c , sure) | false = nodup a (P ❲ f ❳) z zs (c , sure) - -- nodup a (O ❲ e ❳) y zs (c , sure) | true = {!!} - - illegal : βˆ€ {i : Size} β†’ βˆ„[ e ∈ WFOC i β„• ] (⟦ e ⟧ β‰… counterexample) - -- root must be zero because it is always zero in counterexample - illegal (Root (suc i) cs , _ , βŠ‡) with βŠ‡ zero - ... | () - -- there must be a child because there are variants in counterexample with children below the root (e.g., suc zero) - illegal (Root zero [] , _ , βŠ‡) with βŠ‡ (suc zero) -- illegal' (cs , eq) - ... | () - -- there must be an option at the front because there are variants with zero children (e.g., zero) - illegal (Root zero (a OC.-< cs >- ∷ _) , _ , βŠ‡) with βŠ‡ zero - ... | () - -- there can not be any other children - illegal (Root zero (O ❲ e ❳ ∷ a OC.-< as >- ∷ xs) , βŠ† , βŠ‡) = {!!} - illegal (Root zero (O ❲ e ❳ ∷ P OC.❲ e' ❳ ∷ xs) , βŠ† , βŠ‡) = {!!} - -- e can be a chain of options but somewhen, there must be an artifact - illegal (Root zero (O ❲ e ❳ ∷ []) , βŠ† , βŠ‡) = {!!} - --illegal' (e , (O , xs , (βŠ† , βŠ‡))) - - cef : SPL - cef = 0 β—€ ( - (X :: (1 ． 2 ． []) ⊚ ([] ∷ [] , unq ([] ∷ [] , unq ([] , []) ∷ []) ∷ [])) ∷ - (Y :: (1 ． 3 ． []) ⊚ ([] ∷ [] , unq ([] ∷ [] , unq ([] , []) ∷ []) ∷ [])) ∷ - []) - - cef-describes-counterexample : FST⟦ cef ⟧ β‰… counterexample - cef-describes-counterexample = βŠ†[]β†’βŠ† cef-βŠ†[] , βŠ†[]β†’βŠ† {f = fnoc} cef-βŠ‡[] - where - conf : FST.Conf FeatureName β†’ Fin 4 - conf c with c X | c Y - ... | false | false = zero - ... | false | true = suc (suc zero) - ... | true | false = suc zero - ... | true | true = suc (suc (suc zero)) - - cef-βŠ†[] : FST⟦ cef ⟧ βŠ†[ conf ] counterexample - cef-βŠ†[] c with c X | c Y - ... | false | false = refl - ... | false | true = refl - ... | true | false = refl - ... | true | true = {!!} - - fnoc : Fin 4 β†’ FST.Conf FeatureName - fnoc zero X = false - fnoc zero Y = false - fnoc (suc zero) X = true - fnoc (suc zero) Y = false - fnoc (suc (suc zero)) X = false - fnoc (suc (suc zero)) Y = true - fnoc (suc (suc (suc zero))) X = true - fnoc (suc (suc (suc zero))) Y = true - - cef-βŠ‡[] : counterexample βŠ†[ fnoc ] FST⟦ cef ⟧ - cef-βŠ‡[] zero = refl - cef-βŠ‡[] (suc zero) = refl - cef-βŠ‡[] (suc (suc zero)) = refl - cef-βŠ‡[] (suc (suc (suc zero))) = {!!} - - ouch : WFOCL β‹‘ FSTL - ouch sure with sure cef - ... | e , e≣cef = {!!} +open FST F using (FST; FSTL) + +data FeatureName : Set where + X : FeatureName + Y : FeatureName + +open import Data.Bool using (true; false; if_then_else_) +open import Data.Nat using (zero; suc; β„•) +open import Data.Fin using (Fin; zero; suc) +open import Data.List.Relation.Unary.All using (All; []; _∷_) +open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _∷_) +open import Framework.VariantMap V (β„• , _β‰Ÿ_) + +import Lang.All +open Lang.All.OC using (OC; _❲_❳; WFOC; Root; opt; Configuration; ⟦_⟧; WFOCL) + +AtomSet : 𝔸 +AtomSet = β„• , _β‰Ÿ_ + +open FST FeatureName using (_．_) +open FST.Impose FeatureName AtomSet using (SPL; _β—€_; _::_; _⊚_) renaming (⟦_⟧ to FST⟦_⟧) + +open import Data.EqIndexedSet +open import Data.Empty using (βŠ₯-elim) + +open import Data.Product using (_,_; βˆƒ-syntax) +open import Util.Existence using (¬Σ-syntax) + +counterexample : VMap 3 +counterexample zero = rose-leaf 0 +counterexample (suc zero) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ [] >-) ∷ [] >-) +counterexample (suc (suc zero)) = rose (0 At.-< rose (1 At.-< rose-leaf 3 ∷ [] >-) ∷ [] >-) +counterexample (suc (suc (suc zero))) = rose (0 At.-< rose (1 At.-< rose-leaf 2 ∷ rose-leaf 3 ∷ [] >-) ∷ [] >-) + +open import Relation.Nullary.Negation using (Β¬_) + + +illegal : βˆ€ {i : Size} β†’ βˆ„[ e ∈ WFOC FeatureName i AtomSet ] (⟦ e ⟧ β‰… counterexample) +-- root must be zero because it is always zero in counterexample +illegal (Root (suc i) cs , _ , βŠ‡) with βŠ‡ zero +... | () +-- there must be a child because there are variants in counterexample with children below the root (e.g., suc zero) +illegal (Root zero [] , _ , βŠ‡) with βŠ‡ (suc zero) -- illegal' (cs , eq) +... | () +-- there must be an option at the front because there are variants with zero children (e.g., zero) +illegal (Root zero (a OC.-< cs >- ∷ _) , _ , βŠ‡) with βŠ‡ zero +... | () +-- there can not be any other children +illegal (Root zero (O ❲ e ❳ ∷ a OC.-< as >- ∷ xs) , βŠ† , βŠ‡) = {!!} +illegal (Root zero (O ❲ e ❳ ∷ P OC.❲ e' ❳ ∷ xs) , βŠ† , βŠ‡) = {!!} +-- e can be a chain of options but somewhen, there must be an artifact +illegal (Root zero (O ❲ e ❳ ∷ []) , βŠ† , βŠ‡) = {!!} +--illegal' (e , (O , xs , (βŠ† , βŠ‡))) + +cef : SPL +cef = 0 β—€ ( + (X :: (1 ． 2 ． []) ⊚ ([] ∷ [] , ([] ∷ [] , ([] , []) ∷ []) ∷ [])) ∷ + (Y :: (1 ． 3 ． []) ⊚ ([] ∷ [] , ([] ∷ [] , ([] , []) ∷ []) ∷ [])) ∷ + []) + +cef-describes-counterexample : FST⟦ cef ⟧ β‰… counterexample +cef-describes-counterexample = βŠ†[]β†’βŠ† cef-βŠ†[] , βŠ†[]β†’βŠ† {f = fnoc} cef-βŠ‡[] + where + conf : FST.Conf FeatureName β†’ Fin 4 + conf c with c X | c Y + ... | false | false = zero + ... | false | true = suc (suc zero) + ... | true | false = suc zero + ... | true | true = suc (suc (suc zero)) + + cef-βŠ†[] : FST⟦ cef ⟧ βŠ†[ conf ] counterexample + cef-βŠ†[] c with c X | c Y + ... | false | false = refl + ... | false | true = refl + ... | true | false = refl + ... | true | true = {!!} + + fnoc : Fin 4 β†’ FST.Conf FeatureName + fnoc zero X = false + fnoc zero Y = false + fnoc (suc zero) X = true + fnoc (suc zero) Y = false + fnoc (suc (suc zero)) X = false + fnoc (suc (suc zero)) Y = true + fnoc (suc (suc (suc zero))) X = true + fnoc (suc (suc (suc zero))) Y = true + + cef-βŠ‡[] : counterexample βŠ†[ fnoc ] FST⟦ cef ⟧ + cef-βŠ‡[] zero = refl + cef-βŠ‡[] (suc zero) = refl + cef-βŠ‡[] (suc (suc zero)) = refl + cef-βŠ‡[] (suc (suc (suc zero))) = {!!} + +ouch : WFOCL FeatureName β‹‘ FSTL +ouch sure = {!!}