Conjure Vertical Set Rules: Occurrence Representation

• In progress

• Some examples of horizontal rules, with vertical comprehension rules applied - Occurrence representation:

• solving problem C = A intersect B

>     Answer 1: set-eq: Horizontal rule for set equality
>               C = A intersect B
>               ~~>
>               C subsetEq A intersect B /\ A intersect B subsetEq C

> Picking the first option: Question 1: C subsetEq A intersect B
>                               Context #1: [C subsetEq A intersect B, A intersect B subsetEq C; int(1..2)]
>     Answer 1: set-subsetEq: Horizontal rule for set subsetEq
>               C subsetEq A intersect B ~~> and([q4 in A intersect B | q4 <- C])

> Picking the first option: Question 1: [q4 in A intersect B | q4 <- C]
>                               Context #1: and([q4 in A intersect B | q4 <- C])
>                               Context #3: and([q4 in A intersect B | q4 <- C]) /\ A intersect B subsetEq C
>     Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
>               [q4 in A intersect B | q4 <- C]
>               ~~>
>               [q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]] 

> Picking the first option: Question 1: [q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]
>                               Context #1: and([q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]])
>                               Context #3: and([q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]) /\ A intersect B subsetEq C
>     Answer 1: choose-repr-for-comprehension: Choosing representation for quantified variable q4:
>                                                  int(0..6)

> Picking the first option: Question 1: q4 in A intersect B
>                               Context #1: [q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]
>                               Context #3: [and([q4 in A intersect B | q4 : int(0..6), C_Occurrence[q4]]), A intersect B subsetEq C; int(1..2)]
>     Answer 1: set-in: Horizontal rule for set-in.
>               q4 in A intersect B ~~> or([q5 = q4 | q5 <- A intersect B])

> Picking the first option: Question 1: [q5 = q4 | q5 <- A intersect B]
>                               Context #1: or([q5 = q4 | q5 <- A intersect B])
>                               Context #3: and([or([q5 = q4 | q5 <- A intersect B]) | q4 : int(0..6), C_Occurrence[q4]])
>                               Context #5: and([or([q5 = q4 | q5 <- A intersect B]) | q4 : int(0..6), C_Occurrence[q4]]) /\ A intersect B subsetEq C
>     Answer 1: set-intersect: Horizontal rule for set intersection
>               [q5 = q4 | q5 <- A intersect B] ~~> [q5 = q4 | q5 <- A, q5 in B]

> Picking the first option: Question 1: [q5 = q4 | q5 <- A, q5 in B]
>                               Context #1: or([q5 = q4 | q5 <- A, q5 in B])
>                               Context #3: and([or([q5 = q4 | q5 <- A, q5 in B]) | q4 : int(0..6), C_Occurrence[q4]])
>                               Context #5: and([or([q5 = q4 | q5 <- A, q5 in B]) | q4 : int(0..6), C_Occurrence[q4]]) /\ A intersect B subsetEq C
>     Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
>               [q5 = q4 | q5 <- A, q5 in B]
>               ~~>
>               [q5 = q4 | q5 : int(0..6), A_Occurrence[q5], q5 in B]

• comprehension rule for occurrence - Code:

> rule_Comprehension :: Rule
> rule_Comprehension = "set-comprehension{Occurrence}" `namedRule` theRule where
>     theRule (Comprehension body gensOrConds) = do
>         (gocBefore, (pat, iPat, s), gocAfter) <- matchFirst gensOrConds $ \ goc -> case goc of
>             Generator (GenInExpr pat@(Single iPat) s) -> return (pat, iPat, matchDefs [opToSet,opToMSet] s)
>             _ -> na "rule_Comprehension"
>         TypeSet{}            <- typeOf s
>         Set_Occurrence       <- representationOf s
>         [m]                  <- downX1 s
>         DomainMatrix index _ <- domainOf m
>         let i = Reference iPat Nothing
>         return
>             ( "Vertical rule for set-comprehension, Occurrence representation"
>             , return $
>                 Comprehension body
>                     $  gocBefore
>                     ++ [ Generator (GenDomainNoRepr pat index)
>                        , Condition [essence| &m[&i] |]
>                        ]
>                     ++ gocAfter
>             )
>     theRule _ = na "rule_Comprehension"

• Example:

> Picking the first option: Question 1: [q3 in B | q3 <- A]
>                               Context #1: and([q3 in B | q3 <- A])
>     Answer 1: set-comprehension{Occurrence}: Vertical rule for set-comprehension, Occurrence representation
>               [q3 in B | q3 <- A]
>               ~~>
>               [q3 in B | q3 : int(0..6), A_Occurrence[q3]]

• set-in rule for occurrence - Code:

> rule_In :: Rule
> rule_In = "set-in{Occurrence}" `namedRule` theRule where
>     theRule p = do
>         (x, s)         <- match opIn p
>         TypeSet{}      <- typeOf s
>         Set_Occurrence <- representationOf s
>         [m]            <- downX1 s
>         return
>             ( "Vertical rule for set-in, Occurrence representation"
>             , return $ make opIndexing m x
>             )

• Example:

> Picking the first option: Question 1: q3 in B
>                               Context #1: [q3 in B | q3 : int(0..6), A_Occurrence[q3]]
>     Answer 1: set-in{Occurrence}: Vertical rule for set-in, Occurrence representation
>               q3 in B ~~> B_Occurrence[q3]