LE: implement is the number of x such that

lib/haskell/natural4/src/LS/XPile/LogicalEnglish/GenLEHCs.hs

@@ -3,9 +3,8 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE DuplicateRecordFields, RecordWildCards #-}
 -- {-# LANGUAGE OverloadedRecordDot #-}
--- {-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE QuasiQuotes #-}
+-- {-# LANGUAGE QuasiQuotes #-}
 -- {-# LANGUAGE DerivingStrategies #-}
 
 module LS.XPile.LogicalEnglish.GenLEHCs (leHCFromVarsHC) where
@@ -14,13 +13,12 @@ import Data.Text qualified as T
 import Data.HashSet qualified as HS
 -- import Data.Foldable (toList)
 import Data.Coerce (coerce)
-import Data.String.Interpolate ( i )
 import Data.Traversable
 
 import LS.XPile.LogicalEnglish.Types
   ( -- L4-related types
       AtomicBPropn(..)
-    
+
     -- Intermediate representation types, prisms, and consts
     , TemplateVar(..)
     , aposSuffix
@@ -30,7 +28,7 @@ import LS.XPile.LogicalEnglish.Types
     , VarsRule
     , AtomicPWithVars
     , VCell(..)
-  
+
     -- LE-related types
     , LEhcCell(..)
     , LEVar(..)
@@ -41,7 +39,7 @@ import LS.XPile.LogicalEnglish.Types
     , UnivStatus(..)
     , RuleWithUnivsMarked
     , LERuleForPrint
-    , LEhcPrint(..) 
+    , LEhcPrint(..)
   )
 
 leHCFromVarsHC :: VarsHC -> LEhcPrint
@@ -52,7 +50,7 @@ leHCFromVarsHC = \case
     LEHcR . textifyUnivMarkedRule . markUnivVarsInRule $ vrule
 
 -- type LEFactForPrint = AtomicBPropn LETemplateTxt 
-leFactPrintFromVFact :: VarsFact ->  AtomicBPropn LETemplateTxt 
+leFactPrintFromVFact :: VarsFact ->  AtomicBPropn LETemplateTxt
 leFactPrintFromVFact = fmap univst2tmpltetxt . markUnivVarsInFact
 
 markUnivVarsInFact :: VarsFact -> AtomicBPropn UnivStatus
@@ -108,7 +106,7 @@ In more detail:
       (nvars -> leap -> (nvars, uvsp)  )                   
       -> nvars -> br leap -> (nvars, br uvsp)
 
-  It's also worth studying `markUnivVarsInAtomicPacc` and `markUnivVarsInLeCells`
+  It's also worth studying `markUnivVarsInAtomicPacc` and `markUnivVarsInTravable`
   since those functions are what implement the lower-level mechanics of threading 
   the accumulator argument through
 -}
@@ -122,37 +120,36 @@ just not sure if streamlining the plumbing is worth the potential increased comp
 markUnivVarsInAtomicPacc :: NormdVars -> LEhcAtomicP -> (NormdVars, AtomicBPropn UnivStatus)
 markUnivVarsInAtomicPacc nvars = \case
   ABPatomic lecells ->
-    let (nvars', univStatuses) = markUnivVarsInLeCells nvars lecells
+    let (nvars', univStatuses) = markUnivVarsInTravable nvars lecells
     in (nvars', ABPatomic univStatuses)
 
-  ABPBaseIs lefts rights -> 
-    let (nvars', leftsWithUnivStats) = markUnivVarsInLeCells nvars lefts
-        (nvars'', rightsWithUnivStats) = markUnivVarsInLeCells nvars' rights
+  ABPBaseIs lefts rights ->
+    let (nvars', leftsWithUnivStats) = markUnivVarsInTravable nvars lefts
+        (nvars'', rightsWithUnivStats) = markUnivVarsInTravable nvars' rights
     in (nvars'', ABPBaseIs leftsWithUnivStats rightsWithUnivStats)
 
   ABPIsIn t1 t2     -> isSmtg ABPIsIn t1 t2
   ABPIsDiffFr t1 t2 -> isSmtg ABPIsDiffFr t1 t2
 
   ABPIsOpOf term opof termlst ->
     let (nvars', term') = identifyUnivVar nvars term
-        (nvars'', univStatuses) = markUnivVarsInLeCells nvars' termlst
+        (nvars'', univStatuses) = markUnivVarsInTravable nvars' termlst
     in (nvars'', ABPIsOpOf term' opof univStatuses)
 
-  ABPIsOpSuchTt term ostt lecells ->
+  ABPIsOpSuchTt term ostt lecsφx ->
     let (nvars', term') = identifyUnivVar nvars term
-        (nvars'', univStatuses) = markUnivVarsInLeCells nvars' lecells
-    in (nvars'', ABPIsOpSuchTt term' ostt univStatuses)
-
+        (nvars'', ostt') = markUnivVarsInTravable nvars' ostt
+        (nvars''', univStatuses) = markUnivVarsInTravable nvars'' lecsφx
+    in (nvars''', ABPIsOpSuchTt term' ostt' univStatuses)
   where
-    isSmtg op t1 t2 = 
+    isSmtg op t1 t2 =
       let (nvars', t1') = identifyUnivVar nvars t1
           (nvars'', t2') = identifyUnivVar nvars' t2
       in (nvars'', op t1' t2')
 
---- start by doing it the EASIEST possible way 
-markUnivVarsInLeCells :: NormdVars -> [LEhcCell] -> (NormdVars, [UnivStatus])
-markUnivVarsInLeCells init lecells =
-  mapAccumL identifyUnivVar init lecells
+
+markUnivVarsInTravable :: Traversable t => NormdVars -> t LEhcCell -> (NormdVars, t UnivStatus)
+markUnivVarsInTravable = mapAccumL identifyUnivVar
 
 identifyUnivVar :: NormdVars -> LEhcCell -> (NormdVars, UnivStatus)
 identifyUnivVar normdvars = \case
@@ -191,7 +188,7 @@ tvar2lecell = \case
     MatchGVar vtxt    -> VarCell $ VarNonApos vtxt
     EndsInApos prefix -> VarCell $ VarApos prefix
     Num numtxt        -> NotVar numtxt
-    
+
 -- | Prints the intended text for a LEVar
 printlev :: LEVar -> T.Text
 printlev = \case

lib/haskell/natural4/src/LS/XPile/LogicalEnglish/Pretty.hs

@@ -79,7 +79,7 @@ indentLE :: Doc ann -> Doc ann
 indentLE = indent printcfg.numIndentSpcs
 
 nestVsepSeq :: [Doc ann] -> Doc ann
-nestVsepSeq seq =  nestLE (vsep seq)
+nestVsepSeq seq = nestLE (vsep seq)
 
 instance Pretty OpOf where
   pretty :: OpOf -> Doc ann
@@ -89,13 +89,13 @@ instance Pretty OpOf where
     SumOf -> "is the sum of"
     ProductOf -> "is the product of"
 
-instance Pretty OpSuchTt where
-  pretty :: OpSuchTt -> Doc ann
+instance Pretty a => Pretty (OpSuchTt a) where
+  pretty :: Pretty a => OpSuchTt a -> Doc ann
   pretty = \case
     MaxXSuchThat -> "is the max x such that"
     MinXSuchThat -> "is the min x such that"
     SumEachXSuchThat -> "is the sum of each x such that"
-
+    NumOfSuchThat x -> [__di|is the number of #{pretty x} such that|]
 
 instance Pretty LEhcPrint where
   pretty :: LEhcPrint -> Doc ann

lib/haskell/natural4/src/LS/XPile/LogicalEnglish/SimplifyL4.hs

@@ -207,14 +207,34 @@ pattern TermIsOpSuchThat op term φx <- RPnary RPis
 pattern TermIsMaxXWhere :: MTExpr -> [MTExpr] -> RelationalPredicate
 pattern TermIsMinXWhere :: MTExpr -> [MTExpr] -> RelationalPredicate
 pattern TermIsSumXWhere :: MTExpr -> [MTExpr] -> RelationalPredicate
+pattern TermIsNumberOfXWhere :: MTExpr -> MTExpr -> [MTExpr] -> [MTExpr]
 
 pattern TermIsMaxXWhere term φx = TermIsOpSuchThat RPmax term φx
 pattern TermIsMinXWhere term φx = TermIsOpSuchThat RPmin term φx
 pattern TermIsSumXWhere term φx = TermIsOpSuchThat RPsum term φx
+pattern TermIsNumberOfXWhere term x φx <- (term :
+                                            (MTT "is the number of" : (x :
+                                            (MTT "where" : φx))))
 
 {- ^ 
 Examples of the L4 patterns
 
+```
+        [ Leaf
+            ( RPMT
+                [ MTT "n"
+                , MTT "is the number of"
+                , MTT "friend"
+                , MTT "where"
+                , MTT "person"
+                , MTT "met"
+                , MTT "friend"
+                , MTT "on"
+                , MTT "date"
+                ]
+            )
+```
+
 TermIsMaxXWhere:
 ```
       ( RPnary RPis
@@ -267,20 +287,19 @@ t1 IS IN t2:
                     [ MTT "set of things" ]
                 ] ] )
 -}
-
 simplifybodyRP :: forall m. MonadValidate (HS.HashSet SimL4Error) m =>
                     RelationalPredicate -> m (BoolPropn L4AtomicP)
 simplifybodyRP = \case
-  RPMT exprs                         -> pure $ MkTrueAtomicBP (mtes2cells exprs)
-                                        -- ^ this is the same for both the body and head
+  RPMT exprs                         -> simplifyRPMT exprs
+                                        -- ^ TermIsNumberOfXWhere gets handled here
   RPConstraint exprsl rel exprsr     -> simpbodRPC exprsl exprsr rel
 
-  -- max / min / sum x where φ(x)
+  -- max / min / sum x where φ(x), corresponding to RPnary RPis ...
   TermIsMaxXWhere term φx            -> pure $ MkIsOpSuchTtBP (mte2cell term) MaxXSuchThat (mtes2cells φx)
   TermIsMinXWhere term φx            -> pure $ MkIsOpSuchTtBP (mte2cell term) MinXSuchThat (mtes2cells φx)
   TermIsSumXWhere total φx           -> pure $ MkIsOpSuchTtBP (mte2cell total) SumEachXSuchThat (mtes2cells φx)
 
-  -- max / min / sum of terms
+  -- max / min / sum of terms; another RPnary RPis ...
   TermIsMax term maxargRPs           -> termIsNaryOpOf MaxOf term maxargRPs
   TermIsMin term minargRPs           -> termIsNaryOpOf MinOf term minargRPs
   TotalIsSumTerms total summandRPs   -> termIsNaryOpOf SumOf total summandRPs
@@ -295,6 +314,12 @@ simplifybodyRP = \case
   RPParamText _                      -> refute [MkErr "should not be seeing RPParamText in body"]
 
 
+simplifyRPMT :: forall m. MonadValidate (HS.HashSet SimL4Error) m =>
+                    [MTExpr] -> m (BoolPropn L4AtomicP)
+simplifyRPMT = \case
+  TermIsNumberOfXWhere term x φx -> pure $ MkIsOpSuchTtBP (mte2cell term) (NumOfSuchThat $ mte2cell x) (mtes2cells φx)
+  otherExprs                     -> pure $ MkTrueAtomicBP (mtes2cells otherExprs)
+
 termIsNaryOpOf ::
   (Foldable seq, Traversable seq, MonadValidate (HS.HashSet SimL4Error) m) =>
     OpOf -> MTExpr -> seq RelationalPredicate -> m (BoolPropn L4AtomicP)
@@ -406,7 +431,7 @@ mte2cell = \case
 
   mte@(MTI _) -> numify mte
   mte@(MTF _) -> numify mte
-  where 
+  where
     textify = textifyMTE MkCellT
     numify  = textifyMTE MkCellNum
   -- could use prisms and guards instead to get less 'repetition of code', but that would also increase the risk of incomplete case matching in the future

lib/haskell/natural4/src/LS/XPile/LogicalEnglish/Types.hs

@@ -123,7 +123,7 @@ data AtomicBPropn term =
     -- ^ Note: the encoding has a few rules that use an atom in the rightmost term
   | ABPIsOpOf term OpOf [term]
     -- ^ 't IS MAX / MIN / SUM / PROD t_1, ..., t_n'  
-  | ABPIsOpSuchTt term OpSuchTt [term]
+  | ABPIsOpSuchTt term (OpSuchTt term) [term]
     {- |  t IS MAX / MIN / SUM / PROD x where φ(x) -- these require special indentation
         * the first L4Term would be, e.g., the "total savings" in "total savings is the max x such that"
         * the second propn would be the indented φ(x) condition
@@ -138,10 +138,11 @@ data OpOf = MaxOf
           | ProductOf
   deriving stock (Show, Eq, Ord)
 
-data OpSuchTt = MaxXSuchThat
-              | MinXSuchThat
-              | SumEachXSuchThat
-  deriving stock (Show, Eq, Ord)
+data OpSuchTt a = MaxXSuchThat
+                | MinXSuchThat
+                | SumEachXSuchThat
+                | NumOfSuchThat a
+  deriving stock (Show, Eq, Ord, Functor, Foldable, Traversable)
 
 
 {-------------------------------------------------------------------------------
@@ -180,6 +181,7 @@ type GVarSet = HS.HashSet GVar
 data Cell = MkCellT !T.Text
           | MkCellNum !T.Text
   deriving stock (Show, Eq)
+makePrisms ''Cell
 
 type L4Term = Cell
 type L4AtomicP = AtomicBPropn Cell
@@ -188,7 +190,7 @@ type L4AtomicP = AtomicBPropn Cell
 pattern MkTrueAtomicBP :: [Cell] -> BoolPropn L4AtomicP
 pattern MkTrueAtomicBP cells = AtomicBP (ABPatomic cells)
 
-pattern MkIsOpSuchTtBP :: L4Term -> OpSuchTt -> [Cell] -> BoolPropn L4AtomicP
+pattern MkIsOpSuchTtBP :: L4Term -> OpSuchTt L4Term -> [L4Term] -> BoolPropn L4AtomicP
 pattern MkIsOpSuchTtBP var ost bprop = AtomicBP (ABPIsOpSuchTt var ost bprop)
 
 pattern MkIsIn :: L4Term -> L4Term -> BoolPropn L4AtomicP

lib/haskell/natural4/test/Testcases/LogicalEnglish/is-number-of-x-where/actual.le

@@ -0,0 +1,118 @@
+the target language is: prolog.
+
+the templates are:
+  *a person* made friends at the event,
+  *a person* met friend on *a date*,
+  *a number* <= *a number*,
+  *a date* is before *a date*,
+  *a date* is after *a date*,
+  *a date* is strictly before *a date*,
+  *a date* is strictly after *a date*,
+  *a class*'s *a field* is *a value*,
+  *a class*'s nested *a list of fields* is *a value*,
+  *a class*'s *a field0*'s *a field1* is *a value*,
+  *a class*'s *a field0*'s *a field1*'s *a field2* is *a value*,
+  *a class*'s *a field0*'s *a field1*'s *a field2*'s *a field3* is *a value*,
+  *a class*'s *a field0*'s *a field1*'s *a field2*'s *a field3*'s *a field4* is *a value*,
+  *a number* is a lower bound of *a list*,
+  *a number* is an upper bound of *a list*,
+  *a number* is the minimum of *a number* and the maximum of *a number* and *a number*,
+  the sum of *a list* does not exceed the minimum of *a list*,
+  *a number* does not exceed the minimum of *a list*.
+
+
+% Predefined stdlib for translating natural4 -> LE.
+the knowledge base lib includes:
+  a number <= an other number
+  if number =< other number.
+
+  % Note: LE's parsing of [H | T] is broken atm because it transforms that
+  % into [H, T] rather than the Prolog term [H | T].
+
+  % a class's nested [] is a value.
+
+  % a class's nested [a field | a fields] is a value
+  % if the class's the field is an other class
+  % and the other class's nested the fields is the value.
+
+  a d0 is before a d1
+  if d0 is a n days before d1
+  and n >= 0.
+
+  a d0 is strictly before a d1
+  if d0 is a n days before d1
+  and n > 0.
+
+  a d0 is after a d1
+  if d1 is before d0.
+
+  a d0 is strictly after a d1
+  if d1 is strictly before d0.
+
+  % Nested accessor predicates.
+  % a class's a field is a value
+  % if field is different from name
+  % and field is different from id
+  % and a class0's name is class
+  %   or class0's id is class
+  % and class0's field is value.
+
+  a class's a field0's a field1 is a value
+  if class's field0 is a class0
+  and class0's field1 is value.
+
+  a class's a field0's a field1's a field2 is a value
+  if class's field0 is a class0
+  and class0's field1 is a class1
+  and class1's field2 is value.
+
+  a class's a field0's a field1's a field2's a field3 is a value
+  if class's field0 is a class0
+  and class0's field1 is a class1
+  and class1's field2 is a class2
+  and class2's field3 is value.
+
+  a class's a field0's a field1's a field2's a field3's a field4 is a value
+  if the class's field0 is a class0
+  and class0's field1 is a class1
+  and class1's field2 is a class2
+  and class2's field3 is a class3
+  and class3's field4 is value.
+
+  % Arithmetic predicates.
+  a number is an upper bound of a list
+  if for all cases in which
+     a X is in list
+     it is the case that
+      X is [a class, a field]
+          and class's field is a value
+          and number >= value
+        or number >= X.
+
+  a number is a lower bound of a list
+  if for all cases in which
+     a X is in list
+     it is the case that
+      X is [a class, a field]
+          and class's field is a value
+          and number =< value
+        or number =< X.
+
+  % number = min(x, max(y, z))
+  a number is the minimum of a x and the maximum of a y and a z
+  if a m is the maximum of [y, z]
+  and number is the minimum of [x, m].
+
+  a number does not exceed the minimum of a list of numbers
+  if a min is the minimum of list of numbers
+  and number =< min.
+
+  the sum of a list does not exceed the minimum of a other list
+  if a x is the sum of list 
+  and x does not exceed the minimum of other list.
+
+the knowledge base rules includes:
+  a person made friends at the event
+  if a n is the number of friend such that
+    person met friend on a date
+  and n > 1.

lib/haskell/natural4/test/Testcases/LogicalEnglish/is-number-of-x-where/config.yml

@@ -0,0 +1,2 @@
+description: "is the number of x where"
+enabled: true