Skip to content

Commit

Permalink
feat(eo-phi-normalizer): support "Φ̇ " instead of "Φ.org.eolang"
Browse files Browse the repository at this point in the history
  • Loading branch information
deemp committed Dec 17, 2024
1 parent a34269f commit b953999
Show file tree
Hide file tree
Showing 9 changed files with 47 additions and 26 deletions.
5 changes: 3 additions & 2 deletions eo-phi-normalizer/app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -556,9 +556,10 @@ wrapRawBytesIn = \case
]
ObjectDispatch obj a ->
ObjectDispatch (wrapRawBytesIn obj) a
GlobalObject -> GlobalObject
ThisObject -> ThisObject
Termination -> wrapTermination
obj@GlobalObject -> obj
obj@GlobalObjectPhiOrg -> obj
obj@ThisObject -> obj
obj@MetaSubstThis{} -> obj
obj@MetaContextualize{} -> obj
obj@MetaObject{} -> obj
Expand Down
29 changes: 15 additions & 14 deletions eo-phi-normalizer/grammar/EO/Phi/Syntax.cf
Original file line number Diff line number Diff line change
Expand Up @@ -48,20 +48,21 @@ MetaIdBindings. MetaId ::= BindingsMetaId ;
MetaIdObject. MetaId ::= ObjectMetaId ;
MetaIdBytes. MetaId ::= BytesMetaId ;

Formation. Object ::= "⟦" [Binding] "⟧" ;
Application. Object ::= Object "(" [Binding] ")" ;
ObjectDispatch. Object ::= Object "." Attribute ;
GlobalObject. Object ::= "Φ";
ThisObject. Object ::= "ξ";
Termination. Object ::= "⊥" ;
ConstString. Object ::= String ;
ConstInt. Object ::= Integer ;
ConstFloat. Object ::= Double ;
MetaSubstThis. Object ::= Object "[" "ξ" "↦" Object "]" ;
MetaContextualize. Object ::= "⌈" Object "," Object "⌉" ;
MetaObject. Object ::= ObjectMetaId ;
MetaTailContext. Object ::= Object "*" TailMetaId ;
MetaFunction. Object ::= MetaFunctionName "(" Object ")" ;
Formation. Object ::= "⟦" [Binding] "⟧" ;
Application. Object ::= Object "(" [Binding] ")" ;
ObjectDispatch. Object ::= Object "." Attribute ;
GlobalObject. Object ::= "Φ";
GlobalObjectPhiOrg. Object ::= "Φ̇";
ThisObject. Object ::= "ξ";
Termination. Object ::= "⊥" ;
ConstString. Object ::= String ;
ConstInt. Object ::= Integer ;
ConstFloat. Object ::= Double ;
MetaSubstThis. Object ::= Object "[" "ξ" "↦" Object "]" ;
MetaContextualize. Object ::= "⌈" Object "," Object "⌉" ;
MetaObject. Object ::= ObjectMetaId ;
MetaTailContext. Object ::= Object "*" TailMetaId ;
MetaFunction. Object ::= MetaFunctionName "(" Object ")" ;

AlphaBinding. Binding ::= Attribute "↦" Object ;
EmptyBinding. Binding ::= Attribute "↦" "∅" ;
Expand Down
1 change: 1 addition & 0 deletions eo-phi-normalizer/src/Language/EO/Phi/Normalize.hs
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@ peelObject = \case
Application object bindings -> peelObject object `followedBy` ActionApplication bindings
ObjectDispatch object attr -> peelObject object `followedBy` ActionDispatch attr
GlobalObject -> PeeledObject HeadGlobal []
obj@GlobalObjectPhiOrg -> peelObject (desugar obj)
ThisObject -> PeeledObject HeadThis []
Termination -> PeeledObject HeadTermination []
MetaObject _ -> PeeledObject HeadTermination []
Expand Down
21 changes: 14 additions & 7 deletions eo-phi-normalizer/src/Language/EO/Phi/Rules/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,7 @@ withSubObject f ctx root =
]
ObjectDispatch obj a -> propagateName2 ObjectDispatch <$> withSubObject f subctx obj <*> pure a
GlobalObject{} -> []
GlobalObjectPhiOrg{} -> []
ThisObject{} -> []
Termination -> []
MetaObject _ -> []
Expand Down Expand Up @@ -188,13 +189,19 @@ objectSize = \case
Application obj bindings -> 1 + objectSize obj + sum (map bindingSize bindings)
ObjectDispatch obj _attr -> 1 + objectSize obj
GlobalObject -> 1
-- TODO #617:30m
-- @fizruk, why desugar here and not assume the object is desugared?
-- Is it because we sometimes bounce between sugared and desugared versions?
--
-- Should we introduce a smart constructor with a desugared object inside?
obj@GlobalObjectPhiOrg -> objectSize (desugar obj)
ThisObject -> 1
Termination -> 1
MetaObject{} -> 1 -- should be impossible
MetaFunction{} -> 1 -- should be impossible
MetaSubstThis{} -> 1 -- should be impossible
MetaContextualize{} -> 1 -- should be impossible
MetaTailContext{} -> 1 -- should be impossible
obj@MetaObject{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@MetaFunction{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@MetaSubstThis{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@MetaContextualize{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@MetaTailContext{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@ConstString{} -> objectSize (desugar obj)
obj@ConstInt{} -> objectSize (desugar obj)
obj@ConstFloat{} -> objectSize (desugar obj)
Expand All @@ -206,8 +213,8 @@ bindingSize = \case
DeltaBinding _bytes -> 1
DeltaEmptyBinding -> 1
LambdaBinding _lam -> 1
MetaDeltaBinding{} -> 1 -- should be impossible
MetaBindings{} -> 1 -- should be impossible
obj@MetaDeltaBinding{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)
obj@MetaBindings{} -> error ("impossible: expected a desugared object, but got: " <> printTree obj)

-- | A variant of `applyRules` with a maximum application depth.
applyRulesWith :: ApplicationLimits -> Context -> Object -> [Object]
Expand Down
2 changes: 2 additions & 0 deletions eo-phi-normalizer/src/Language/EO/Phi/Rules/Fast.hs
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,8 @@ fastYegorInsideOut ctx = \case
AlphaBinding a (fastYegorInsideOut ctx' objA)
_ -> binding
]
-- TODO #617:30m Should this be error?
obj@GlobalObjectPhiOrg -> fastYegorInsideOut ctx (desugar obj)
Termination -> Termination
MetaSubstThis{} -> error "impossible MetaSubstThis!"
MetaContextualize{} -> error "impossible MetaContextualize!"
Expand Down
9 changes: 8 additions & 1 deletion eo-phi-normalizer/src/Language/EO/Phi/Rules/Yaml.hs
Original file line number Diff line number Diff line change
Expand Up @@ -228,6 +228,7 @@ usedLabelIds Context{..} = objectLabelIds globalObject
objectLabelIds :: Object -> Set LabelId
objectLabelIds = \case
GlobalObject -> mempty
obj@GlobalObjectPhiOrg -> objectLabelIds (desugar obj)
ThisObject -> mempty
Formation bindings -> foldMap bindingLabelIds bindings
ObjectDispatch obj a -> objectLabelIds obj <> attrLabelIds a
Expand Down Expand Up @@ -278,6 +279,7 @@ objectMetaIds (Formation bindings) = foldMap bindingMetaIds bindings
objectMetaIds (Application object bindings) = objectMetaIds object <> foldMap bindingMetaIds bindings
objectMetaIds (ObjectDispatch object attr) = objectMetaIds object <> attrMetaIds attr
objectMetaIds GlobalObject = mempty
objectMetaIds GlobalObjectPhiOrg = mempty
objectMetaIds ThisObject = mempty
objectMetaIds Termination = mempty
objectMetaIds (MetaObject x) = Set.singleton (MetaIdObject x)
Expand Down Expand Up @@ -310,6 +312,7 @@ objectHasMetavars (Formation bindings) = any bindingHasMetavars bindings
objectHasMetavars (Application object bindings) = objectHasMetavars object || any bindingHasMetavars bindings
objectHasMetavars (ObjectDispatch object attr) = objectHasMetavars object || attrHasMetavars attr
objectHasMetavars GlobalObject = False
objectHasMetavars GlobalObjectPhiOrg = False
objectHasMetavars ThisObject = False
objectHasMetavars Termination = False
objectHasMetavars (MetaObject _) = True
Expand Down Expand Up @@ -436,6 +439,7 @@ applySubst subst@Subst{..} = \case
ObjectDispatch obj a ->
ObjectDispatch (applySubst subst obj) (applySubstAttr subst a)
GlobalObject -> GlobalObject
obj@GlobalObjectPhiOrg -> applySubst subst (desugar obj)
ThisObject -> ThisObject
obj@(MetaObject x) -> fromMaybe obj $ lookup x objectMetas
Termination -> Termination
Expand Down Expand Up @@ -522,7 +526,8 @@ matchOneHoleContext ctxId pat obj = matchWhole <> matchPart
ConstString{} -> []
ConstInt{} -> []
ConstFloat{} -> []
-- should cases below be errors?
-- TODO #617:30m Should cases below be errors?
GlobalObjectPhiOrg -> []
MetaSubstThis{} -> []
MetaContextualize{} -> []
MetaObject{} -> []
Expand Down Expand Up @@ -629,6 +634,7 @@ substThis thisObj = go
Application obj bindings -> Application (go obj) (map (substThisBinding thisObj) bindings)
ObjectDispatch obj a -> ObjectDispatch (go obj) a
GlobalObject -> GlobalObject
obj@GlobalObjectPhiOrg -> go (desugar obj)
Termination -> Termination
obj@MetaTailContext{} -> error ("impossible: trying to substitute ξ in " <> printTree obj)
obj@MetaContextualize{} -> error ("impossible: trying to substitute ξ in " <> printTree obj)
Expand Down Expand Up @@ -662,6 +668,7 @@ contextualize thisObj = go
ObjectDispatch obj a -> ObjectDispatch (go obj) a
Application obj bindings -> Application (go obj) (map (contextualizeBinding thisObj) bindings)
GlobalObject -> GlobalObject -- TODO: Change to what GlobalObject is attached to
obj@GlobalObjectPhiOrg -> go (desugar obj) -- TODO: Change to what GlobalObject is attached to
Termination -> Termination
obj@MetaTailContext{} -> error ("impossible: trying to contextualize " <> printTree obj)
obj@MetaContextualize{} -> error ("impossible: trying to contextualize " <> printTree obj)
Expand Down
1 change: 1 addition & 0 deletions eo-phi-normalizer/src/Language/EO/Phi/Syntax.hs
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,7 @@ desugar = \case
Application obj bindings -> Application (desugar obj) (map desugarBinding bindings)
ObjectDispatch obj a -> ObjectDispatch (desugar obj) a
GlobalObject -> GlobalObject
GlobalObjectPhiOrg -> ObjectDispatch (ObjectDispatch GlobalObject (Label (LabelId "org"))) (Label (LabelId "eolang"))
ThisObject -> ThisObject
Termination -> Termination
MetaSubstThis obj this -> MetaSubstThis (desugar obj) (desugar this)
Expand Down
1 change: 1 addition & 0 deletions eo-phi-normalizer/src/Language/EO/Phi/ToLaTeX.hs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ instance ToLatex Object where
toLatex (ObjectDispatch obj attr) =
toLatex obj <> "." <> toLatex attr
toLatex GlobalObject = "Q"
toLatex GlobalObjectPhiOrg = "QQ"
toLatex ThisObject = "\\xi"
toLatex Termination = "\\dead"
toLatex (MetaObject (ObjectMetaId metaId)) = LaTeX metaId
Expand Down
4 changes: 2 additions & 2 deletions eo-phi-normalizer/test/eo/phi/dataization.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ tests:
input: |
{⟦
c ↦ Φ.org.eolang.number(
as-bytes ↦ Φ.org.eolang.bytes(Δ ⤍ 40-39-00-00-00-00-00-00)
as-bytes ↦ Φ̇.bytes(Δ ⤍ 40-39-00-00-00-00-00-00)
), // 25.0
φ ↦ ξ.c.times(x ↦ ⟦ Δ ⤍ 3F-FC-CC-CC-CC-CC-CC-CD ⟧) // 1.8
.plus(x ↦ ⟦ Δ ⤍ 40-40-00-00-00-00-00-00 ⟧), // 32.0
Expand All @@ -43,7 +43,7 @@ tests:
- ./data/0.41.2/org/eolang/true.phi
- ./data/0.41.2/org/eolang/false.phi
input: |
{⟦ φ ↦ Φ.org.eolang.true.eq(α0 ↦ Φ.org.eolang.true) ⟧}
{⟦ φ ↦ Φ.org.eolang.true.eq(α0 ↦ Φ̇.true) ⟧}
output:
bytes: "01-"

Expand Down

0 comments on commit b953999

Please sign in to comment.