Skip to content

Instantly share code, notes, and snippets.

@Janiczek

Janiczek/Pred.elm

Last active December 4, 2022 21:34
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save Janiczek/cb84e49baf62f9b488b901eb6e0d9530 to your computer and use it in GitHub Desktop.
Save Janiczek/cb84e49baf62f9b488b901eb6e0d9530 to your computer and use it in GitHub Desktop.
Download ZIP
Advent of Code 2022-04 - code synthesis
Raw
Pred.elm
module Pred exposing (..)
import List.Cartesian
import Transform
type alias Example =
( Range, Range )
type alias Range =
( Int, Int )
type Pred
= Cmp What Op What
| And Pred Pred
| Or Pred Pred
| Literal Bool
type Op
= LT_
| LTE
| EQ_
| NEQ
| GTE
| GT_
type What
= L1
| R1
| L2
| R2
-- Eval
eval : Pred -> Example -> Bool
eval pred example =
case pred of
Cmp w1 op w2 ->
opFn op
(whatFn example w1)
(whatFn example w2)
And p1 p2 ->
eval p1 example && eval p2 example
Or p1 p2 ->
eval p1 example || eval p2 example
Literal bool ->
bool
opFn : Op -> (Int -> Int -> Bool)
opFn op =
case op of
LT_ ->
(<)
LTE ->
(<=)
EQ_ ->
(==)
NEQ ->
(/=)
GTE ->
(>=)
GT_ ->
(>)
whatFn : Example -> What -> Int
whatFn ( ( l1, r1 ), ( l2, r2 ) ) what =
case what of
L1 ->
l1
R1 ->
r1
L2 ->
l2
R2 ->
r2
-- Size
size : Pred -> Int
size pred =
case pred of
Cmp _ _ _ ->
1
And p1 p2 ->
1 + size p1 + size p2
Or p1 p2 ->
1 + size p1 + size p2
Literal _ ->
1
-- Pretty printer
toString : Pred -> String
toString p =
case p of
Cmp w1 op w2 ->
String.join " "
[ wToString w1
, opToString op
, wToString w2
]
And p1 p2 ->
String.concat
[ "("
, toString p1
, " && "
, toString p2
, ")"
]
Or p1 p2 ->
String.concat
[ "("
, toString p1
, " || "
, toString p2
, ")"
]
Literal bool ->
if bool then
"True"
else
"False"
opToString : Op -> String
opToString op =
case op of
LT_ ->
"<"
LTE ->
"<="
EQ_ ->
"=="
NEQ ->
"!="
GTE ->
">="
GT_ ->
">"
wToString : What -> String
wToString what =
case what of
L1 ->
"L1"
R1 ->
"R1"
L2 ->
"L2"
R2 ->
"R2"
oracleP1 : Example -> Bool
oracleP1 ( r1, r2 ) =
oracleContainsFully r1 r2 || oracleContainsFully r2 r1
oracleContainsFully : Range -> Range -> Bool
oracleContainsFully ( bigLeft, bigRight ) ( smallLeft, smallRight ) =
bigLeft <= smallLeft && bigRight >= smallRight
oracleP2 : Example -> Bool
oracleP2 ( r1, r2 ) =
oracleContains r1 r2 || oracleContains r2 r1
oracleContains : Range -> Range -> Bool
oracleContains ( bigLeft, bigRight ) ( smallLeft, smallRight ) =
bigLeft <= smallLeft && bigRight >= smallLeft
examples : List Example
examples =
-- Should be all interesting cases
let
range =
List.range 1 4
in
List.Cartesian.map4 (\a b c d -> ( ( a, b ), ( c, d ) ))
range
range
range
range
|> List.filter (\( ( a, b ), ( c, d ) ) -> a <= b && c <= d)
-- SIMPLIFY
simplify : Pred -> Pred
simplify =
Transform.transformAll
recurse
simplifyAll
recurse : (Pred -> Pred) -> Pred -> Pred
recurse fn pred =
case pred of
Cmp _ _ _ ->
pred
And p1 p2 ->
And (fn p1) (fn p2)
Or p1 p2 ->
Or (fn p1) (fn p2)
Literal _ ->
pred
simplifyAll : Pred -> Maybe Pred
simplifyAll =
Transform.orList
[ simplifyObvious
]
simplifyObvious : Pred -> Maybe Pred
simplifyObvious pred =
let
false =
Just (Literal False)
true =
Just (Literal True)
in
case pred of
Cmp w1 op w2 ->
case op of
LT_ ->
if w1 == w2 then
false
else if w1 == R1 && w2 == L1 then
false
else if w1 == R2 && w2 == L2 then
false
else
Nothing
LTE ->
if w1 == w2 then
true
else if w1 == L1 && w2 == R1 then
true
else if w1 == L2 && w2 == R2 then
true
else
Nothing
EQ_ ->
if w1 == w2 then
true
else
Nothing
NEQ ->
if w1 == w2 then
false
else
Nothing
GTE ->
if w1 == w2 then
true
else if w1 == R1 && w2 == L1 then
true
else if w1 == R2 && w2 == L2 then
true
else
Nothing
GT_ ->
if w1 == w2 then
false
else if w1 == L1 && w2 == R1 then
false
else if w1 == L2 && w2 == R2 then
false
else
Nothing
And p1 p2 ->
if p1 == Literal False || p2 == Literal False then
false
else if p1 == Literal True then
Just p2
else if p2 == Literal True then
Just p1
else
Nothing
Or p1 p2 ->
if p1 == Literal True || p2 == Literal True then
true
else if p1 == Literal False then
Just p2
else if p2 == Literal False then
Just p1
else
Nothing
Literal _ ->
Nothing
bestFoundP1 : Pred
bestFoundP1 =
Or
(And (Cmp L1 LTE L2) (Cmp R1 GTE R2))
(And (Cmp L2 LTE L1) (Cmp R2 GTE R1))
bestFoundP2 : Pred
bestFoundP2 =
Or
(And (Cmp L1 LTE L2) (Cmp R1 GTE L2))
(And (Cmp L2 LTE L1) (Cmp R2 GTE L1))
Raw
Tests.elm
module Tests exposing (suite)
import Expect exposing (Expectation)
import Fuzz exposing (Fuzzer)
import Pred exposing (..)
import Test exposing (Test)
-- Fuzzers
predFuzzer : Fuzzer Pred
predFuzzer =
exprFuzzer
{ baseCases = [ cmpFuzzer ]
, recursiveCases = [ andFuzzer, orFuzzer ]
, maxDepth = 4
}
andFuzzer : Fuzzer Pred -> Fuzzer Pred
andFuzzer e =
Fuzz.map2 And e e
orFuzzer : Fuzzer Pred -> Fuzzer Pred
orFuzzer e =
Fuzz.map2 Or e e
cmpFuzzer : Fuzzer Pred
cmpFuzzer =
Fuzz.map3 Cmp whatFuzzer opFuzzer whatFuzzer
opFuzzer : Fuzzer Op
opFuzzer =
Fuzz.oneOfValues [ LT_, LTE, EQ_, NEQ, GTE, GT_ ]
whatFuzzer : Fuzzer What
whatFuzzer =
Fuzz.oneOfValues [ L1, R1, L2, R2 ]
exprFuzzer :
{ baseCases : List (Fuzzer a)
, recursiveCases : List (Fuzzer a -> Fuzzer a)
, maxDepth : Int
}
-> Fuzzer a
exprFuzzer config =
Fuzz.oneOf <|
if config.maxDepth <= 0 then
config.baseCases
else
config.baseCases
++ List.map
(\f -> f (exprFuzzer { config | maxDepth = config.maxDepth - 1 }))
config.recursiveCases
-- Tests! aka, "I bet you can't find a function that does the same thing as my function!"
suite : Test
suite =
Test.concat
[ Test.fuzz predFuzzer "P1" <|
\pred ->
let
simple =
simplify pred
in
(List.all (\example -> eval simple example == oracleP1 example) examples
&& (size simple < size bestFoundP1)
)
|> Expect.equal False
|> Expect.onFail (Debug.toString simple ++ "\n\n" ++ toString simple)
, Test.fuzz predFuzzer "P2" <|
\pred ->
let
simple =
simplify pred
in
(List.all (\example -> eval simple example == oracleP2 example) examples
&& (size simple < size bestFoundP2)
)
|> Expect.equal False
|> Expect.onFail (Debug.toString simple ++ "\n\n" ++ toString simple)
, Test.fuzzWith
{ runs = 100
, distribution = Test.noDistribution
}
predFuzzer
"simplify preserves meaning"
<|
\pred ->
examples
|> List.all (\example -> eval (simplify pred) example == eval pred example)
|> Expect.equal True
]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment