Skip to content

Instantly share code, notes, and snippets.

@MonoidMusician

MonoidMusician/0 metalanguage-grammar.bnf

Last active December 20, 2021 07:20
Show Gist options
  • Save MonoidMusician/edaf572a1dac7f44635f36e4b1b46ef6 to your computer and use it in GitHub Desktop.
Save MonoidMusician/edaf572a1dac7f44635f36e4b1b46ef6 to your computer and use it in GitHub Desktop.
Download ZIP
Sketches for Dhall-standard-as-data in Python using a type system à la PureScript
Raw
0 metalanguage-grammar.bnf
# Syntax for a metalanguage for writing programming language standards/specifications with an eye towards codegen
# The data format is very simple: data is either a string or a tuple of data.
# The idea is that we'll impose some simple types on top of this:
# Obviously strings, and arrays, possibly associative lists, and then mixed ADTs/enums, which are either plain strings or arrays where the first item is the tag denoting the constructor.
# I don't have the types figured out yet.
# Variable names
variable-name = [_A-Za-z][-_A-Za-z0-9]*
# A variable can have periods, but they don't mean anything
variable = variable-name ("." variable-name)*
# String literal
# this needs escaping and stuff obviously
string-literal = '"' character '"' | "'" character "'"
character = [.]
# A pattern can match a variable name and/or a semi-literal
pattern = variable | semi-literal | variable "@" semi-literal
# A semi-literal is a string literal or a list of patterns (separated by space, since a pattern has well-defined extent)
semi-literal = string-literal | "[" patterns "]"
patterns = pattern+
# A simple expression is an expression that has well-defined extent: we know when it ends, so a list of them can be separated by whitespace
simple-expression
= pattern
| variable
| "%" lambda-body "!"
| "(" expression ")"
simple-expressions = simple-expression+
# An expression can be a simple expression or a lambda with no ending … idk
expression
= simple-expression
| "%" lambda-body
# A lambda consists of many cases separated by vertical bars, see below
lambda-body = "|"? case ("|" case)* "|"?
# A switch expression is just syntactic sugar for calling a lambda with arguments
switch = "?" calling lambda-body "!"
# Top-level functions are defined using slash-separated paths for each case, and the trailing slash is required so we know it is a definition
path = variable-name ("/" variable-name)* "/"
top-case = path case
# Match means specifying patterns and then the return expression
matching = patterns "=>" simple-expression
# A case consists of matching followed by conditions, which are the body of the function, the commands to execute to reach the result (which was already specified in matching)
case = matching (";" | ":"? conditions)
# A condition consists of calling a function with arguments and matching on the result
condition = simple-expression calling
conditions = condition*
# Each time we call a function we get to match on its result
calling = simple-expressions "=>" pattern
# Notes
# Typechecking lambdas is tricky, but it works out because we want main functions (which have type information) to be at head: if a lambda is being applied immediately that is a case expression, if it is being returned then also know its type again
# Oh wait, I guess polymorphism jinxes that: identity function will not work to determine the type of its argument and result
# If we only case-match on variables (partial evaluate to get there) then we have a simpler time with type inference: we can't guess the type of literals, but every variable should have a type
# We can have an untyped local macro thingy too, but it shouldn't be necessary
# We can elaborate to desugar typeclasses during typechecking
# Not sure how matching is going to work: ideally I want nested matches to use the specified equality
# Need to think about effects … hmm how do languages with first-class effects make functions functors? functions aren't traversable so it seems like they couldn't even support `map` in a language where all functions come with effects
# Main use for first-class effects: want to write a meta-function `ensure` that acts to force unification, it will take basically a raw pattern match and then be elaborated to unify with that constructor (it must be a single constructor) … `ensure :: (Expr -[Maybe, …]> o) -> (Expr -[…]> o)`
# are there languages with first-class patterns? what does that look like? I have a function that basically wants to take a pattern, thinking about how to make unification appear ergonomic
Raw
1 syntax.txt
reference-equality :: m.a -> m.a -> m.a
reference-equality/ o o => o
syntactic-equality :: Expr -> Expr -> Expr
syntactic-equality/reference-equality/ l r => o
reference-equality l r => o
syntactic-equality/ l r => o
traverseRTogether % [x y] => z
syntactic-equality x y => z ! l r => ['Some' o]
judgmental-equality :: Expr -> Expr -> Expr
judgmental-equality/reference-equality/ l r => o
reference-equality l r => o
judgmental-equality/ l r => o
alpha-beta-normalize l => x
alpha-beta-normalize r => y
syntactic-equality x y => o
constant :: Text -> Expr -> Expr
constant/ v e => r
shift '-1' v '0' e => r
shift-nat :: Integer -> Natural -> Natural
le :: Natural -> Natural -> Bool
if-eq-suc :: Text -> Text -> Natural -> Natural
if-eq-suc/eq/ v v m => m1
suc m => m1
if-eq-suc/neq/ _ _ m => m
shift :: Integer -> Text -> Natural -> Expr -> Expr
shift/Variable/ d v m e@['Variable' v n] => ['Variable' v nd]
le m n => 'True'
ensure-shift-nat d n => nd
shift/Lambda/ d v m e@['Lambda' u A0 b0] => ['Lambda' u A1 b1]
if-eq-suc v u m => m1
shift d v m A0 => A1
shift d v m1 b0 => b1
shift/Forall/ d v m e@['Forall' u A0 B0] => ['Forall' u A1 B1]
if-eq-suc v u m => m1
shift d v m A0 => A1
shift d v m1 B0 => B1
shift/Let/ d v m e@['Let' u mA0 a0 b0] => ['Let' u mA1 a0 b1]
if-eq-suc v u m => m1
traverse mA0 % A0 => A1
shift d v m A0 => A1 ! => mA1
shift d v m a0 => a1
shift d v m1 b0 => b1
shift/Application/ d v m ['Application' f0 a0] => ['Application' f1 a1]
shift d v m f0 => f1
shift d v m a0 => a1
shift/Type/ d v m 'Type' => 'Type'
shift/Variable/ _ _ _ v@['Variable' _ _] => v
shift/ d v m e1 => e2
traverseR e1 % se1 => se2
shift d v m se1 => se2 ! => e2
substitute :: Text -> Natural -> Expr -> Expr -> Expr
substitute/Variable-match/ v m r ['Variable' v m] => r
substitute/Lambda/ v m r ['Lambda' u A0 b0] => ['Lambda' u A1 b1]
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' u '0' r => r1
substitute v m1 r1 b0 => b1
substitute/Forall/ v m r ['Forall' u A0 B0] => ['Forall' u A1 B1]
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' u '0' r => r1
substitute v m r1 B0 => B1
substitute/Let/ v m r ['Let' v mA0 a0 b0] => ['Lambda' v A1 b1]
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' v '0' r => r1
substitute v m1 r1 b0 => b1
substitute/ v m r e1 => e2
traverseR e1 % se1 => se2
substitute v m r se1 => se2 ! => e2
shift-substitute-shift :: Text -> Expr -> Expr -> Expr
shift-substitute-shift/ v r0 e0 => e2
shift '1' v '0' r0 => r1
substitute v '0' r1 e0 => e1
shift '-1' v '0' e1 => e2
rename-immediate :: Text -> Text -> Expr -> Expr
rename-immediate/noop/ v v e => e
rename-immediate/ v u e0 => e1
shift-substitute-shift v ['Variable' u '0'] e0 => e1
alpha-normalize :: Expr -> Expr
alpha-normalize/Lambda/ ['Lambda' v A0 b0] => ['Lambda' '_' A1 b2]
alpha-normalize A0 => A1
rename-immediate v '_' b0 => b1
alpha-normalize b1 => b2
alpha-normalize/Forall/ ['Forall' v A0 B0] => ['Forall' '_' A1 B2]
alpha-normalize A0 => A1
rename-immediate v '_' B0 => B1
alpha-normalize B1 => B2
alpha-normalize/Let/ ['Let' v mA0 a0 b0] => ['Let' '_' mA1 a1 b2]
traverse mA0 % A0 => A1
alpha-normalize A0 => A1 ! => mA1
alpha-normalize a0 => a1
rename-immediate v '_' b0 => b1
alpha-normalize b1 => b2
alpha-normalize/ e0 => e1
traverseR e0 % se0 => se1
alpha-normalize se0 => se1 ! => e1
beta-normalize :: Expr -> Expr
beta-normalize/Bool/if_then_else_/ ['if_then_else_' ['BoolLit' b] l r] => o
builtin/if_then_else_ b l r => o
beta-normalize/Bool/if_then_else_/identity/ ['if_then_else_' b ['BoolLit' 'true'] ['BoolLit' 'false']] => b
beta-normalize/Bool/if_then_else_/constant/ ['if_then_else_' _ e e] => e
beta-normalize/Bool/||/L-absorb/ ['||' l@['BoolLit' 'True'] _] => l
beta-normalize/Bool/||/L-identity/ ['||' _@['BoolLit' 'False'] r] => r
beta-normalize/Bool/||/ ['||' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/|| l r => o
beta-normalize/Bool/||/R-absorb/ ['||' _ r@['BoolLit' 'True']] => r
beta-normalize/Bool/||/R-identity/ ['||' l _@['BoolLit' 'False']] => l
beta-normalize/Bool/||/idempotence/ ['||' e e] => e
beta-normalize/Bool/&&/L-absorb/ ['&&' l@['BoolLit' 'False'] _] => l
beta-normalize/Bool/&&/L-identity/ ['&&' _@['BoolLit' 'True'] r] => r
beta-normalize/Bool/&&/ ['&&' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/&& l r => o
beta-normalize/Bool/&&/R-absorb/ ['&&' _ r@['BoolLit' 'False']] => r
beta-normalize/Bool/&&/R-identity/ ['&&' l _@['BoolLit' 'True']] => l
beta-normalize/Bool/&&/idempotence/ ['&&' e e] => e
beta-normalize/Bool/==/L-identity/ ['==' _@['BoolLit' 'True'] r] => r
beta-normalize/Bool/==/ ['==' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/== l r => o
beta-normalize/Bool/==/R-identity/ ['==' l _@['BoolLit' 'True']] => l
beta-normalize/Bool/==/idempotence/ ['==' e e] => e
beta-normalize/Bool/!=/L-identity/ ['!=' _@['BoolLit' 'False'] r] => r
beta-normalize/Bool/!=/ ['!=' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/!= l r => o
beta-normalize/Bool/!=/R-identity/ ['!=' l _@['BoolLit' 'False']] => l
beta-normalize/Bool/!=/idempotence/ ['!=' e e] => e
beta-normalize/Natural/build/ ['Application' 'Natural/build' g] => b
identity ['Lambda' 'x' 'Natural' ['+' ['Variable' 'x' '0'] ['NaturalLit' '1']]] => succ
identity ['NaturalLit' '0'] => zero
beta-normalize ['Application' g 'Natural' succ zero] => b
beta-normalize/Natural/fold/ ['Application' 'Natural/fold' ['NaturalLit' n] B g b] => r
fold-natural n b % r0 => ['Application' g r0] ! => r
beta-normalize/Natural/*/L-absorb/ ['*' l@['NaturalLit' '0'] _] => l
beta-normalize/Natural/*/L-identity/ ['*' _@['NaturalLit' '1'] r] => r
beta-normalize/Natural/*/ ['*' ['NaturalLit' l] ['NaturalLit' r]] => ['NaturalLit' o]
builtin/* l r => o
beta-normalize/Natural/*/R-absorb/ ['*' r@['NaturalLit' '0'] _] => r
beta-normalize/Natural/*/R-identity/ ['*' l _@['NaturalLit' '1']] => l
beta-normalize/Natural/+/L-identity/ ['+' _@['NaturalLit' '0'] r] => r
beta-normalize/Natural/+/ ['+' ['NaturalLit' l] ['NaturalLit' r]] => ['NaturalLit' o]
builtin/+ l r => o
beta-normalize/Natural/+/R-identity/ ['+' l _@['NaturalLit' '0']] => l
beta-normalize/Natural/isZero/ ['Application' 'Natural/isZero' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/isZero n => o
beta-normalize/Natural/even/ ['Application' 'Natural/even' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/even n => o
beta-normalize/Natural/odd/ ['Application' 'Natural/odd' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/odd n => o
beta-normalize/Natural/toInteger/ ['Application' 'Natural/toInteger' ['NaturalLit' n]] => ['IntegerLit' o]
builtin/Natural/toInteger n => o
beta-normalize/Natural/show/ ['Application' 'Natural/show' ['NaturalLit' n]] => ['TextLit' o]
builtin/Natural/show n => o
beta-normalize/Natural/subtract/L-zero/ ['Application' 'Natural/subtract' ['NaturalLit' '0'] n] => n
beta-normalize/Natural/subtract/R-zero/ ['Application' 'Natural/subtract' _ l@['NaturalLit' '0']] => l
beta-normalize/Natural/subtract/equal/ ['Application' 'Natural/subtract' n n] => ['NaturalLit' '0']
beta-normalize/Natural/subtract/ ['Application' 'Natural/subtract' ['NaturalLit' m] ['NaturalLit' n]] => ['NaturalLit' o]
builtin/Natural/subtract m n => o
beta-normalize/List/build/ ['Application' 'List/build' A0 g] => b
shift '1' 'a' '0' A0 => A1
identity ['Lambda' 'a' A0 ['Lambda' 'as' ['Application' 'List' A1] ['#' ['ListLit' [['Variable' 'a' '0']] 'None'] ['Variable' 'as' '0']]]] => succ
identity ['ListLit' [] ['Some' ['Application' 'List' A0]]] => zero
beta-normalize ['Application' g ['Application' 'List' A0] succ zero] => b
beta-normalize/List/fold/ ['Application' 'List/fold' A0 ['ListLit' l _] B g b] => r
fold-list l b % a0 r0 => ['Application' g a0 r0] ! => r
beta-normalize/List/#/L-identity/ ['#' ['ListLit' [] _] r] => r
beta-normalize/List/#/R-identity/ ['#' l ['ListLit' [] _]] => l
beta-normalize/List/#/ ['#' ['ListLit' ls 'None'] ['ListLit' rs 'None']] => ['ListLit' lrs []]
builtin/List/# ls rs => lrs
beta-normalize/Record/Field/ ['Field' ['RecordLit' kvs] k] => v
find kvs k => v
beta-normalize/Record/Field/Project/ ['Field' ['Project' rec ks] k] => ['Field' rec k]
beta-normalize/Record/Field/Prefer/L-yes/ ['Field' ['Prefer' ['RecordLit' kvs] r] k] => v
find kvs k => v
beta-normalize/Record/Field/Prefer/L-no/ ['Field' ['Prefer' ['RecordLit' kvs] r] k] => ['Field' r k]
beta-normalize/Record/Field/Prefer/R-yes/ ['Field' ['Prefer' l ['RecordLit' kvs]] k] => v
find kvs k => v
beta-normalize/Record/Field/Prefer/R-no/ ['Field' ['Prefer' l ['RecordLit' kvs]] k] => ['Field' l k]
beta-normalize/Record/Field/Combine/L-yes/ ['Field' ['Combine' ['RecordLit' kvs] r] k] => ['Field' ['Combine' ['RecordLit' [[k v]]] r] k]
find kvs k => v
beta-normalize/Record/Field/Combine/L-no/ ['Field' ['Combine' ['RecordLit' kvs] r] k] => ['Field' r k]
beta-normalize/Record/Field/Combine/R-yes/ ['Field' ['Combine' l ['RecordLit' kvs]] k] => ['Field' ['Combine' l ['RecordLit' [[k v]]]] k]
find kvs k => v
beta-normalize/Record/Field/Combine/R-no/ ['Field' ['Combine' l ['RecordLit' kvs]] k] => ['Field' l k]
beta-normalize/Record/Project/empty/ ['Project' rec ['ByLabels' []]] => ['RecordLit' []]
beta-normalize/Record/Project/ ['Project' ['RecordLit' kvs0] ['ByLabels' ks]] => ['RecordLit' kvs1]
select kvs0 ks => kvs1
beta-normalize/Record/Project/Project/ ['Project' ['Project' rec _] ['ByLabels' ks]] => ['Project' rec ['ByLabels' ks]]
beta-normalize/Record/Project/Prefer/ ['Project' ['Prefer' l ['RecordLit' kvs]] ['ByLabels' ks]] => ['Prefer' ['Project' l ['ByFields' lks]] ['Project' r ['ByFields' rks]]]
separate kvs ks lks => rks
beta-normalize/Record/Project/Record/ ['Project' rec ['ByType' ['RecordType' kvs]]] => ['Project' rec ['ByFields' ks]]
void kvs => ks
beta-normalize/Application/ ['Application' ['Lambda' v _ b] a] => r
shift-substitute-shift v a b => r
beta-normalize/Let/ ['Let' v _ a b] => r
shift-substitute-shift v a b => r
beta-normalize/Annotation/ ['Annotation' v _] => v
eta-normalize :: Expr -> Expr
eta-normalize/ ['Lambda' v t ['Application' f ['Variable' v '0']]] => o
constant v f => o
typecheck :: Context Expr -> Expr -> Expr
typecheck/Variable/ ctx ['Variable' x n] => T
find-ctx ctx x n => T
typecheck/Bool/ ctx 'Bool' => 'Type'
typecheck/BoolLit/ ctx ['BoolLit' _] => 'Bool'
typecheck/if_then_else_/ ctx ['if_then_else_' b l r] => T
typecheck ctx b => 'Bool'
typecheck ctx l => T
typecheck ctx r => T
typecheck/||/ ctx ['||' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/&&/ ctx ['&&' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/==/ ctx ['==' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/!=/ ctx ['!=' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/Natural/ ctx 'Natural' => 'Type'
typecheck/NaturalLit/ ctx ['NaturalLit' _] => 'Natural'
typecheck/+/ ctx ['+' l r] => 'Natural'
typecheck ctx l => 'Natural'
typecheck ctx r => 'Natural'
typecheck/*/ ctx ['*' l r] => 'Natural'
typecheck ctx l => 'Natural'
typecheck ctx r => 'Natural'
typecheck/Natural/build/ ctx 'Natural/build' => ['Forall' '_' ['Forall' 'natural' 'Type' ['Forall' 'succ' ['Forall' '_' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']] ['Forall' 'zero' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']]]] 'Natural']
typecheck/Natural/fold/ ctx 'Natural/fold' => ['Forall' '_' 'Natural' ['Forall' 'natural' 'Type' ['Forall' 'succ' ['Forall' '_' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']] ['Forall' 'zero' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']]]]]
typecheck/Natural/isZero/ ctx 'Natural/isZero' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/even/ ctx 'Natural/even' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/odd/ ctx 'Natural/odd' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/toInteger/ ctx 'Natural/toInteger' => ['Forall' '_' 'Natural' 'Integer']
typecheck/Natural/show/ ctx 'Natural/show' => ['Forall' '_' 'Natural' 'Text']
typecheck/Natural/subtract/ ctx 'Natural/subtract' => ['Forall' '_' 'Natural' ['Forall' '_' 'Natural' 'Natural']]
typecheck/Text/ ctx 'Text' => 'Type'
typecheck/TextLiteral/ ctx ['TextLiteral' txt] => 'Text'
traverse_ % t => []
typecheck ctx t => 'Text' ! txt => []
typecheck/Text/show/ ctx 'Text/show' => ['Forall' '_' 'Text' 'Text']
typecheck/Text/replace/ ctx 'Text/replace' => ['Forall' 'needle' 'Text' ['Forall' 'replacement' 'Text' ['Forall' 'haystack' 'Text' 'Text']]]
typecheck/Text/++/ ctx ['++' l r] => 'Text'
typecheck ctx l => 'Text'
typecheck ctx r => 'Text'
typecheck/Date/ ctx 'Date' => 'Type'
typecheck/Time/ ctx 'Time' => 'Type'
typecheck/TimeZone/ ctx 'TimeZone' => 'Type'
typecheck/Date/ ctx ['DateLiteral' _] => 'Date'
typecheck/Time/ ctx ['TimeLiteral' _] => 'Time'
typecheck/TimeZone/ ctx ['TimeZoneLiteral' _] => 'TimeZone'
typecheck/List/ ctx 'List' => ['Forall' '_' 'Type' 'Type']
typecheck/List/#/ ctx ['#' l r] => ['Application' 'List' T]
typecheck ctx l => ['Application' 'List' T]
typecheck ctx r => ['Application' 'List' T]
typecheck/RecordLit/ ctx ['RecordLit' kvs] => kts
ensureNodupes kvs => []
traverse typecheck kvs => kts
typecheck/Field/ ctx ['Field' expr field] => fieldType
typecheck expr => ty
? ty => fieldType
| ['Record' kts] => fieldType
find kts field => fieldType
| ['Const' c] => fieldType
? expr => fieldType
| ['Union' kts] => fieldType
find kts field => mt
? mt => fieldType
| ['Some' ty] => ['Pi' field ty result]
shift field '1' expr => result
| 'None' => expr
!
!
!
typecheck/Integer/ ctx 'Integer' => 'Type'
typecheck/IntegerLit/ ctx ['IntegerLit' _] => 'Integer'
typecheck/Integer/show/ ctx 'Integer/show' => ['Forall' '_' 'Integer' 'Text']
typecheck/Integer/toDouble/ ctx 'Integer/toDouble' => ['Forall' '_' 'Integer' 'Double']
typecheck/Integer/negate/ ctx 'Integer/negate' => ['Forall' '_' 'Integer' 'Integer']
typecheck/Integer/clamp/ ctx 'Integer/clamp' => ['Forall' '_' 'Integer' 'Natural']
typecheck/Double/ ctx 'Double' => 'Type'
typecheck/DoubleLit/ ctx ['DoubleLit' _] => 'Double'
typecheck/Double/show/ ctx 'Double/show' => ['Forall' '_' 'Double' 'Text']
typecheck/Forall/ ctx ['Forall' x A B] => ['Const' c]
typecheck ctx A => ['Const' i]
add-ctx x A ctx => ctx1
typecheck ctx1 B => ['Const' o]
imax i o => c
typecheck/Lambda/ ctx ['Lambda' x A b] => ['Forall' x A B]
typecheck ctx A => ['Const' _]
add-ctx x A ctx => ctx1
typecheck ctx1 b => B
typecheck/Application/ ctx ['Application' f a] => ['Application' ['Lambda' x A B] a]
typecheck ctx f => ['Forall' x A B]
typecheck ctx a => A
typecheck/Let/ ctx ['Let' x mA a b] => B
typecheck ctx a => A
traverse_ % A => [] ! mA => []
shift-substitute-shift x a b => b1
typecheck ctx b1 => B
typecheck/Annot/ ctx ['Annot' a A] => A
typecheck ctx a => A
typecheck/Assert/ ctx ['Assert' T] => ['Equivalent' x x]
typecheck ctx T => 'Type'
beta-normalize T => ['Equivalent' x x]
typecheck/Equivalent/ ctx ['Equivalent' x y] => 'Type'
typecheck ctx x => A
typecheck ctx y => A
typecheck ctx A => 'Type'
Raw
2 desugared.txt
reference-equality :: m.a -> m.a -> m.a
reference-equality/ o.0 o.1 => o
eq o.0 o.1 => o.2
identity o.2 => o
syntactic-equality :: Expr -> Expr -> Expr
syntactic-equality/reference-equality/ l r => o
reference-equality l r => o
syntactic-equality/ l r => o
traverseRTogether % [x y] => z
syntactic-equality x y => z ! l r => ['Some' o]
judgmental-equality :: Expr -> Expr -> Expr
judgmental-equality/reference-equality/ l r => o
reference-equality l r => o
judgmental-equality/ l r => o
alpha-beta-normalize l => x
alpha-beta-normalize r => y
syntactic-equality x y => o
constant :: Text -> Expr -> Expr
constant/ v e => r
shift '-1' v '0' e => r
shift-nat :: Integer -> Natural -> Natural
le :: Natural -> Natural -> Bool
if-eq-suc :: Text -> Text -> Natural -> Natural
if-eq-suc/eq/ v.0 v.1 m => m1
eq v.0 v.1 => v.2
identity v.2 => v
suc m => m1
if-eq-suc/neq/ _ _ m => m
shift :: Integer -> Text -> Natural -> Expr -> Expr
shift/Variable/ d v.0 m e@['Variable' v.1 n] => ['Variable' v nd]
eq v.0 v.1 => v.2
identity v.2 => v
le m n => 'True'
ensure-shift-nat d n => nd
shift/Lambda/ d v m e@['Lambda' u A0 b0] => ['Lambda' u A1 b1]
if-eq-suc v u m => m1
shift d v m A0 => A1
shift d v m1 b0 => b1
shift/Forall/ d v m e@['Forall' u A0 B0] => ['Forall' u A1 B1]
if-eq-suc v u m => m1
shift d v m A0 => A1
shift d v m1 B0 => B1
shift/Let/ d v m e@['Let' u mA0 a0 b0] => ['Let' u mA1 a0 b1]
if-eq-suc v u m => m1
traverse mA0 % A0 => A1
shift d v m A0 => A1 ! => mA1
shift d v m a0 => a1
shift d v m1 b0 => b1
shift/Application/ d v m ['Application' f0 a0] => ['Application' f1 a1]
shift d v m f0 => f1
shift d v m a0 => a1
shift/Type/ d v m 'Type' => 'Type'
shift/Variable/ _ _ _ v@['Variable' _ _] => v
shift/ d v m e1 => e2
traverseR e1 % se1 => se2
shift d v m se1 => se2 ! => e2
substitute :: Text -> Natural -> Expr -> Expr -> Expr
substitute/Variable-match/ v.0 m.0 r ['Variable' v.1 m.1] => r
eq v.0 v.1 => v.2
eq m.0 m.1 => m.2
identity v.2 => v
identity m.2 => m
substitute/Lambda/ v m r ['Lambda' u A0 b0] => ['Lambda' u A1 b1]
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' u '0' r => r1
substitute v m1 r1 b0 => b1
substitute/Forall/ v m r ['Forall' u A0 B0] => ['Forall' u A1 B1]
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' u '0' r => r1
substitute v m r1 B0 => B1
substitute/Let/ v.0 m r ['Let' v.1 mA0 a0 b0] => ['Lambda' v A1 b1]
eq v.0 v.1 => v.2
identity v.2 => v
if-eq-suc v u m => m1
substitute v m r A0 => A1
shift '1' v '0' r => r1
substitute v m1 r1 b0 => b1
substitute/ v m r e1 => e2
traverseR e1 % se1 => se2
substitute v m r se1 => se2 ! => e2
shift-substitute-shift :: Text -> Expr -> Expr -> Expr
shift-substitute-shift/ v r0 e0 => e2
shift '1' v '0' r0 => r1
substitute v '0' r1 e0 => e1
shift '-1' v '0' e1 => e2
rename-immediate :: Text -> Text -> Expr -> Expr
rename-immediate/noop/ v.0 v.1 e => e
eq v.0 v.1 => v.2
identity v.2 => v
rename-immediate/ v u e0 => e1
shift-substitute-shift v ['Variable' u '0'] e0 => e1
alpha-normalize :: Expr -> Expr
alpha-normalize/Lambda/ ['Lambda' v A0 b0] => ['Lambda' '_' A1 b2]
alpha-normalize A0 => A1
rename-immediate v '_' b0 => b1
alpha-normalize b1 => b2
alpha-normalize/Forall/ ['Forall' v A0 B0] => ['Forall' '_' A1 B2]
alpha-normalize A0 => A1
rename-immediate v '_' B0 => B1
alpha-normalize B1 => B2
alpha-normalize/Let/ ['Let' v mA0 a0 b0] => ['Let' '_' mA1 a1 b2]
traverse mA0 % A0 => A1
alpha-normalize A0 => A1 ! => mA1
alpha-normalize a0 => a1
rename-immediate v '_' b0 => b1
alpha-normalize b1 => b2
alpha-normalize/ e0 => e1
traverseR e0 % se0 => se1
alpha-normalize se0 => se1 ! => e1
beta-normalize :: Expr -> Expr
beta-normalize/Bool/if_then_else_/ ['if_then_else_' ['BoolLit' b] l r] => o
builtin/if_then_else_ b l r => o
beta-normalize/Bool/if_then_else_/identity/ ['if_then_else_' b ['BoolLit' 'true'] ['BoolLit' 'false']] => b
beta-normalize/Bool/if_then_else_/constant/ ['if_then_else_' _ e.0 e.1] => e
judgmental-equality e.0 e.1 => e.2
identity e.2 => e
beta-normalize/Bool/||/L-absorb/ ['||' l@['BoolLit' 'True'] _] => l
beta-normalize/Bool/||/L-identity/ ['||' _@['BoolLit' 'False'] r] => r
beta-normalize/Bool/||/ ['||' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/|| l r => o
beta-normalize/Bool/||/R-absorb/ ['||' _ r@['BoolLit' 'True']] => r
beta-normalize/Bool/||/R-identity/ ['||' l _@['BoolLit' 'False']] => l
beta-normalize/Bool/||/idempotence/ ['||' e.0 e.1] => e
judgmental-equality e.0 e.1 => e.2
identity e.2 => e
beta-normalize/Bool/&&/L-absorb/ ['&&' l@['BoolLit' 'False'] _] => l
beta-normalize/Bool/&&/L-identity/ ['&&' _@['BoolLit' 'True'] r] => r
beta-normalize/Bool/&&/ ['&&' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/&& l r => o
beta-normalize/Bool/&&/R-absorb/ ['&&' _ r@['BoolLit' 'False']] => r
beta-normalize/Bool/&&/R-identity/ ['&&' l _@['BoolLit' 'True']] => l
beta-normalize/Bool/&&/idempotence/ ['&&' e.0 e.1] => e
judgmental-equality e.0 e.1 => e.2
identity e.2 => e
beta-normalize/Bool/==/L-identity/ ['==' _@['BoolLit' 'True'] r] => r
beta-normalize/Bool/==/ ['==' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/== l r => o
beta-normalize/Bool/==/R-identity/ ['==' l _@['BoolLit' 'True']] => l
beta-normalize/Bool/==/idempotence/ ['==' e.0 e.1] => e
judgmental-equality e.0 e.1 => e.2
identity e.2 => e
beta-normalize/Bool/!=/L-identity/ ['!=' _@['BoolLit' 'False'] r] => r
beta-normalize/Bool/!=/ ['!=' ['BoolLit' l] ['BoolLit' r]] => ['BoolLit' o]
builtin/!= l r => o
beta-normalize/Bool/!=/R-identity/ ['!=' l _@['BoolLit' 'False']] => l
beta-normalize/Bool/!=/idempotence/ ['!=' e.0 e.1] => e
judgmental-equality e.0 e.1 => e.2
identity e.2 => e
beta-normalize/Natural/build/ ['Application' 'Natural/build' g] => b
identity ['Lambda' 'x' 'Natural' ['+' ['Variable' 'x' '0'] ['NaturalLit' '1']]] => succ
identity ['NaturalLit' '0'] => zero
beta-normalize ['Application' g 'Natural' succ zero] => b
beta-normalize/Natural/fold/ ['Application' 'Natural/fold' ['NaturalLit' n] B g b] => r
fold-natural n b % r0 => ['Application' g r0] ! => r
beta-normalize/Natural/*/L-absorb/ ['*' l@['NaturalLit' '0'] _] => l
beta-normalize/Natural/*/L-identity/ ['*' _@['NaturalLit' '1'] r] => r
beta-normalize/Natural/*/ ['*' ['NaturalLit' l] ['NaturalLit' r]] => ['NaturalLit' o]
builtin/* l r => o
beta-normalize/Natural/*/R-absorb/ ['*' r@['NaturalLit' '0'] _] => r
beta-normalize/Natural/*/R-identity/ ['*' l _@['NaturalLit' '1']] => l
beta-normalize/Natural/+/L-identity/ ['+' _@['NaturalLit' '0'] r] => r
beta-normalize/Natural/+/ ['+' ['NaturalLit' l] ['NaturalLit' r]] => ['NaturalLit' o]
builtin/+ l r => o
beta-normalize/Natural/+/R-identity/ ['+' l _@['NaturalLit' '0']] => l
beta-normalize/Natural/isZero/ ['Application' 'Natural/isZero' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/isZero n => o
beta-normalize/Natural/even/ ['Application' 'Natural/even' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/even n => o
beta-normalize/Natural/odd/ ['Application' 'Natural/odd' ['NaturalLit' n]] => ['BoolLit' o]
builtin/Natural/odd n => o
beta-normalize/Natural/toInteger/ ['Application' 'Natural/toInteger' ['NaturalLit' n]] => ['IntegerLit' o]
builtin/Natural/toInteger n => o
beta-normalize/Natural/show/ ['Application' 'Natural/show' ['NaturalLit' n]] => ['TextLit' o]
builtin/Natural/show n => o
beta-normalize/Natural/subtract/L-zero/ ['Application' 'Natural/subtract' ['NaturalLit' '0'] n] => n
beta-normalize/Natural/subtract/R-zero/ ['Application' 'Natural/subtract' _ l@['NaturalLit' '0']] => l
beta-normalize/Natural/subtract/equal/ ['Application' 'Natural/subtract' n.0 n.1] => ['NaturalLit' '0']
judgmental-equality n.0 n.1 => n.2
identity n.2 => n
beta-normalize/Natural/subtract/ ['Application' 'Natural/subtract' ['NaturalLit' m] ['NaturalLit' n]] => ['NaturalLit' o]
builtin/Natural/subtract m n => o
beta-normalize/List/build/ ['Application' 'List/build' A0 g] => b
shift '1' 'a' '0' A0 => A1
identity ['Lambda' 'a' A0 ['Lambda' 'as' ['Application' 'List' A1] ['#' ['ListLit' [['Variable' 'a' '0']] 'None'] ['Variable' 'as' '0']]]] => succ
identity ['ListLit' [] ['Some' ['Application' 'List' A0]]] => zero
beta-normalize ['Application' g ['Application' 'List' A0] succ zero] => b
beta-normalize/List/fold/ ['Application' 'List/fold' A0 ['ListLit' l _] B g b] => r
fold-list l b % a0 r0 => ['Application' g a0 r0] ! => r
beta-normalize/List/#/L-identity/ ['#' ['ListLit' [] _] r] => r
beta-normalize/List/#/R-identity/ ['#' l ['ListLit' [] _]] => l
beta-normalize/List/#/ ['#' ['ListLit' ls 'None'] ['ListLit' rs 'None']] => ['ListLit' lrs []]
builtin/List/# ls rs => lrs
beta-normalize/Record/Field/ ['Field' ['RecordLit' kvs] k] => v
find kvs k => v
beta-normalize/Record/Field/Project/ ['Field' ['Project' rec ks] k] => ['Field' rec k]
beta-normalize/Record/Field/Prefer/L-yes/ ['Field' ['Prefer' ['RecordLit' kvs] r] k] => v
find kvs k => v
beta-normalize/Record/Field/Prefer/L-no/ ['Field' ['Prefer' ['RecordLit' kvs] r] k] => ['Field' r k]
beta-normalize/Record/Field/Prefer/R-yes/ ['Field' ['Prefer' l ['RecordLit' kvs]] k] => v
find kvs k => v
beta-normalize/Record/Field/Prefer/R-no/ ['Field' ['Prefer' l ['RecordLit' kvs]] k] => ['Field' l k]
beta-normalize/Record/Field/Combine/L-yes/ ['Field' ['Combine' ['RecordLit' kvs] r] k] => ['Field' ['Combine' ['RecordLit' [[k v]]] r] k]
find kvs k => v
beta-normalize/Record/Field/Combine/L-no/ ['Field' ['Combine' ['RecordLit' kvs] r] k] => ['Field' r k]
beta-normalize/Record/Field/Combine/R-yes/ ['Field' ['Combine' l ['RecordLit' kvs]] k] => ['Field' ['Combine' l ['RecordLit' [[k v]]]] k]
find kvs k => v
beta-normalize/Record/Field/Combine/R-no/ ['Field' ['Combine' l ['RecordLit' kvs]] k] => ['Field' l k]
beta-normalize/Record/Project/empty/ ['Project' rec ['ByLabels' []]] => ['RecordLit' []]
beta-normalize/Record/Project/ ['Project' ['RecordLit' kvs0] ['ByLabels' ks]] => ['RecordLit' kvs1]
select kvs0 ks => kvs1
beta-normalize/Record/Project/Project/ ['Project' ['Project' rec _] ['ByLabels' ks]] => ['Project' rec ['ByLabels' ks]]
beta-normalize/Record/Project/Prefer/ ['Project' ['Prefer' l ['RecordLit' kvs]] ['ByLabels' ks]] => ['Prefer' ['Project' l ['ByFields' lks]] ['Project' r ['ByFields' rks]]]
separate kvs ks lks => rks
beta-normalize/Record/Project/Record/ ['Project' rec ['ByType' ['RecordType' kvs]]] => ['Project' rec ['ByFields' ks]]
void kvs => ks
beta-normalize/Application/ ['Application' ['Lambda' v _ b] a] => r
shift-substitute-shift v a b => r
beta-normalize/Let/ ['Let' v _ a b] => r
shift-substitute-shift v a b => r
beta-normalize/Annotation/ ['Annotation' v _] => v
eta-normalize :: Expr -> Expr
eta-normalize/ ['Lambda' v.0 t ['Application' f ['Variable' v.1 '0']]] => o
judgmental-equality v.0 v.1 => v.2
identity v.2 => v
constant v f => o
typecheck :: Context Expr -> Expr -> Expr
typecheck/Variable/ ctx ['Variable' x n] => T
find-ctx ctx x n => T
typecheck/Bool/ ctx 'Bool' => 'Type'
typecheck/BoolLit/ ctx ['BoolLit' _] => 'Bool'
typecheck/if_then_else_/ ctx ['if_then_else_' b l r] => T
judgmental-equality T.0 T.1 => T.2
identity T.2 => T
typecheck ctx b => 'Bool'
typecheck ctx l => T.0
typecheck ctx r => T.1
typecheck/||/ ctx ['||' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/&&/ ctx ['&&' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/==/ ctx ['==' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/!=/ ctx ['!=' l r] => 'Bool'
typecheck ctx l => 'Bool'
typecheck ctx r => 'Bool'
typecheck/Natural/ ctx 'Natural' => 'Type'
typecheck/NaturalLit/ ctx ['NaturalLit' _] => 'Natural'
typecheck/+/ ctx ['+' l r] => 'Natural'
typecheck ctx l => 'Natural'
typecheck ctx r => 'Natural'
typecheck/*/ ctx ['*' l r] => 'Natural'
typecheck ctx l => 'Natural'
typecheck ctx r => 'Natural'
typecheck/Natural/build/ ctx 'Natural/build' => ['Forall' '_' ['Forall' 'natural' 'Type' ['Forall' 'succ' ['Forall' '_' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']] ['Forall' 'zero' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']]]] 'Natural']
typecheck/Natural/fold/ ctx 'Natural/fold' => ['Forall' '_' 'Natural' ['Forall' 'natural' 'Type' ['Forall' 'succ' ['Forall' '_' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']] ['Forall' 'zero' ['Variable' 'natural' '0'] ['Variable' 'natural' '0']]]]]
typecheck/Natural/isZero/ ctx 'Natural/isZero' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/even/ ctx 'Natural/even' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/odd/ ctx 'Natural/odd' => ['Forall' '_' 'Natural' 'Bool']
typecheck/Natural/toInteger/ ctx 'Natural/toInteger' => ['Forall' '_' 'Natural' 'Integer']
typecheck/Natural/show/ ctx 'Natural/show' => ['Forall' '_' 'Natural' 'Text']
typecheck/Natural/subtract/ ctx 'Natural/subtract' => ['Forall' '_' 'Natural' ['Forall' '_' 'Natural' 'Natural']]
typecheck/Text/ ctx 'Text' => 'Type'
typecheck/TextLiteral/ ctx ['TextLiteral' txt] => 'Text'
traverse_ % t => []
typecheck ctx t => 'Text' ! txt => []
typecheck/Text/show/ ctx 'Text/show' => ['Forall' '_' 'Text' 'Text']
typecheck/Text/replace/ ctx 'Text/replace' => ['Forall' 'needle' 'Text' ['Forall' 'replacement' 'Text' ['Forall' 'haystack' 'Text' 'Text']]]
typecheck/Text/++/ ctx ['++' l r] => 'Text'
typecheck ctx l => 'Text'
typecheck ctx r => 'Text'
typecheck/Date/ ctx 'Date' => 'Type'
typecheck/Time/ ctx 'Time' => 'Type'
typecheck/TimeZone/ ctx 'TimeZone' => 'Type'
typecheck/Date/ ctx ['DateLiteral' _] => 'Date'
typecheck/Time/ ctx ['TimeLiteral' _] => 'Time'
typecheck/TimeZone/ ctx ['TimeZoneLiteral' _] => 'TimeZone'
typecheck/List/ ctx 'List' => ['Forall' '_' 'Type' 'Type']
typecheck/List/#/ ctx ['#' l r] => ['Application' 'List' T]
judgmental-equality T.0 T.1 => T.2
identity T.2 => T
typecheck ctx l => ['Application' 'List' T.0]
typecheck ctx r => ['Application' 'List' T.1]
typecheck/RecordLit/ ctx ['RecordLit' kvs] => kts
ensureNodupes kvs => []
traverse typecheck kvs => kts
typecheck/Field/ ctx ['Field' expr field] => fieldType
typecheck expr => ty
? ty => fieldType
| ['Record' kts] => fieldType
find kts field => fieldType
| ['Const' c] => fieldType
? expr => fieldType
| ['Union' kts] => fieldType
find kts field => mt
? mt => fieldType
| ['Some' ty] => ['Pi' field ty result]
shift field '1' expr => result
| 'None' => expr
!
!
!
typecheck/Integer/ ctx 'Integer' => 'Type'
typecheck/IntegerLit/ ctx ['IntegerLit' _] => 'Integer'
typecheck/Integer/show/ ctx 'Integer/show' => ['Forall' '_' 'Integer' 'Text']
typecheck/Integer/toDouble/ ctx 'Integer/toDouble' => ['Forall' '_' 'Integer' 'Double']
typecheck/Integer/negate/ ctx 'Integer/negate' => ['Forall' '_' 'Integer' 'Integer']
typecheck/Integer/clamp/ ctx 'Integer/clamp' => ['Forall' '_' 'Integer' 'Natural']
typecheck/Double/ ctx 'Double' => 'Type'
typecheck/DoubleLit/ ctx ['DoubleLit' _] => 'Double'
typecheck/Double/show/ ctx 'Double/show' => ['Forall' '_' 'Double' 'Text']
typecheck/Forall/ ctx ['Forall' x A B] => ['Const' c]
typecheck ctx A => ['Const' i]
add-ctx x A ctx => ctx1
typecheck ctx1 B => ['Const' o]
imax i o => c
typecheck/Lambda/ ctx ['Lambda' x A b] => ['Forall' x A B]
typecheck ctx A => ['Const' _]
add-ctx x A ctx => ctx1
typecheck ctx1 b => B
typecheck/Application/ ctx ['Application' f a] => ['Application' ['Lambda' x A B] a]
judgmental-equality A.0 A.1 => A.2
identity A.2 => A
typecheck ctx f => ['Forall' x A.0 B]
typecheck ctx a => A.1
typecheck/Let/ ctx ['Let' x mA a b] => B
typecheck ctx a => A
traverse_ % A => [] ! mA => []
shift-substitute-shift x a b => b1
typecheck ctx b1 => B
typecheck/Annot/ ctx ['Annot' a A.0] => A
judgmental-equality A.0 A.1 => A.2
identity A.2 => A
typecheck ctx a => A.1
typecheck/Assert/ ctx ['Assert' T] => ['Equivalent' x x]
judgmental-equality x.0 x.1 => x.2
identity x.2 => x
typecheck ctx T => 'Type'
beta-normalize T => ['Equivalent' x.0 x.1]
typecheck/Equivalent/ ctx ['Equivalent' x y] => 'Type'
judgmental-equality A.0 A.1 => A.2
identity A.2 => A
typecheck ctx x => A.0
typecheck ctx y => A.1
typecheck ctx A => 'Type'
Raw
3 metalanguage.py
#!/usr/bin/env python3
import inspect
# Defer f(*a)(*b) so the first application is only computed after the second
# is being applied. Memoized so it the first is only computed once.
def defer(f, *arg):
saved = False
value = None
def deferred(*arg2):
nonlocal saved, value
if not saved:
value = f(*arg)
saved = True
return value(*arg2)
return deferred
# Parse a basic syntax of parentheses and spaces into a tree of tuples
def parse(s):
z = iter(s)
def go():
r = ()
o = True
for c in z:
if c == " ":
o = True
elif c == "(":
if r == ():
r = go()
else:
r = (r, go())
o = True
elif c == ")":
return r
elif o:
o = False
if r == ():
r = c
else:
r = (r, c)
else:
if isinstance(r, str):
r += c
else:
r = tuple([*r[:-1], r[-1]+c])
return r
return go()
# Print a tree of tuples into space-delimited applications,
# adding parentheses as needed
def pretty(r):
if isinstance(r, str):
return r
if isinstance(r, Taker) or isinstance(r, Matcher):
return repr(r)
s = ""
s += pretty(r[0])
s += " "
if isinstance(r[1], str):
s += r[1]
else:
s += "("
s += pretty(r[1])
s += ")"
return s
# Forall type, takes a lambda, like Void = Forall(lambda a: a)
class Forall:
def __init__(self, value, name=None):
if name is None:
name = list(inspect.signature(value).parameters.keys())[0]
self.name = name
self.value = value
self.tester = Tester(self.name)
self.tested = self.value(self.tester)
#print(f"kind {tester.kind!r}")
self.kind = ()
def __repr__(self):
return f"Forall(lambda {self.name}: {repr(self.tested)})"
def __call__(self, param):
return self.value(param)
# Type in the meta language:
# - `name` is a string for primitive types, or a tuple-tree of names
# as applied to each other.
# - `kind` is a tuple of input kinds, which are themselves tuples of input kinds
# (the output is always Type). Thus a type has kind `()`, a functor has kind
# `((),)`, a bifunctor has kind `((),())`, etc.
# - `pred` is the predicate used to verify data; for types that take parameters
# it is first passed the predicate for the parameter, then later it gets
# the actual data to verify.
class MetaType:
registry = dict()
# __init__ registers all named types immediately
def __init__(self, name, pred, kind=()):
self.name = name
self.pred = pred
self.kind = kind
if isinstance(self.name, str):
if self.name in MetaType.registry:
raise KeyError(f"Duplicate type with name {self.name}")
MetaType.registry[self.name] = self
# Note: __repr__ does not use `parse` because it could include type
# variables which cannot be parsed, so we use `get` instead.
def __repr__(self):
# Shortcut to eliminate one layer of parentheses
if isinstance(self.name, tuple):
return f"MetaType.get{self.name!r}"
return f"MetaType.get({self.name!r})"
def __eq__(self, other):
return self.name == other.name
def __hash__(self):
return hash(self.name)
@classmethod
def parse(cls, name):
return cls.get(parse(name))
@classmethod
def get(cls, *name):
if len(name) == 1:
name = name[0]
if isinstance(name, str):
return cls.registry[name]
if isinstance(name, MetaType):
return name
return MetaType.__call__(*(cls.get(n) for n in name))
# __call__ either instantiates type parameters or checks data across the
# predicate. These are exclusive: it doesn't make sense to check data on
# a functor.
def __call__(self, *params):
if len(params) == 1 and not isinstance(params[0], MetaType):
return self.pred(params[0])
if self.kind.__len__() < len(params):
raise TypeError(f"Cannot instantiate type with {len(params)} more parameters")
kind = self.kind
for i,p in enumerate(params):
if kind[i] != p.kind:
raise TypeError(f"Mismatched kind while applying parameter {i}")
self = MetaType((self.name, p.name), defer(self.pred, p), kind[i+1:])
return self
# Create the wrapped data for this type.
def mk(self, data):
return MetaData(self, data)
# Deconstruct an application of this type, returning the parameters passed
# to it. Returns None if it is not an application of this type, or if
# the passed `arity` does not match the number of arguments.
def de(self, other, arity=None):
args = []
head = other.name
while head != self.name:
if not isinstance(head, tuple):
return None
args.insert(0, *head[1:])
head = head[0]
if arity is not None:
args = args[:arity]
if len(args) != arity:
return None
return tuple(MetaType.get(a) for a in args)
# Construct the predicate for an algebraic data type.
@staticmethod
def adt(spec):
def validate(data):
if not isinstance(data, tuple) or len(data) < 1:
return False
if data[0] not in spec:
return False
tag = spec[data[0]]
if len(data)-1 != len(tag):
return False
return all(tag[i](data[i+1]) for i in range(len(tag)))
return validate
# Construct the predicate that only matches the specified values.
@staticmethod
def enum(*values):
values = set(values)
def validate(data):
return data in values
return validate
# More abstract specification, subsumes but enum and adt.
@staticmethod
def abstractSpec(spec):
discr = dict()
for i,rule in enumerate(spec):
if isinstance(rule, str):
if rule in discr:
raise KeyError(f"Duplicate rule matching on {rule} at indices {discr[rule]}, {i}")
discr[rule] = i
elif isinstance(rule, tuple):
if len(rule) == 0:
if () in discr:
raise KeyError(f"Duplicate empty tuple at index {i}")
discr[()] = i
elif isinstance(rule[0], str):
if not all(isinstance(r, MetaType) for r in rule[1:]):
raise TypeError(f"Bad tuple item at index {i}")
k = (len(rule), rule[0])
discr[k] = i
else:
raise TypeError(f"Bad tuple rule at index {i}")
else:
raise TypeError(f"Bad rule at index {i}")
def validate(data):
if isinstance(data, str):
return data in discr
if isinstance(data, tuple):
if len(data) == 0:
return () in discr
if not isinstance(data[0], str):
return False
k = (len(data), data[0])
if k not in discr:
return False
rule = spec[discr[k]]
return all(r.pred(d) for r,d in zip(rule[1:], data[1:]))
return False
return validate
# Kinds
MetaType.Type = ()
MetaType.Functor = (MetaType.Type,)
MetaType.Bifunctor = (MetaType.Type, MetaType.Type)
# Data tagged with a MetaType.
class MetaData:
def __init__(self, typ, data):
if isinstance(data, MetaData):
if data.typ != typ:
raise TypeError(f"Data had existing type {data.typ!r}, expected {typ!r}")
self.typ = data.typ
self.data = data.data
elif isinstance(typ, Forall):
if not callable(data):
raise TypeError(f"Forall expects function")
self.typ = typ
self.data = data
else:
if typ.kind != ():
raise TypeError(f"Cannot construct data for non-fully-applied types")
else:
if not typ.pred(data):
print(data)
raise TypeError(f"Data does not satisfy type predicate for {typ!r}")
self.typ = typ
self.data = data
def __repr__(self):
return f"MetaData({self.typ!r}, {self.data!r})"
def __call__(self, *args):
for arg in args:
if isinstance(self.typ, Forall):
if not isinstance(arg, MetaType):
raise TypeError(f"Expected type for forall")
self = MetaData(self.typ(arg), self.data(arg))
else:
try:
(ti, to) = mtFunction.de(self.typ, 2)
except TypeError:
raise TypeError(f"Was not function type {self.typ!r}")
arg = MetaData(ti, arg)
self = MetaData(to, self.data(arg.data))
return self
# Very basic TypeClass support
# Multi-parameter (no fundeps, no flexible contexts/instances)
class TypeClass:
registry = dict()
def __init__(self, name, kinds, methods):
self.name = name
self.kinds = kinds
self.methods = methods
self.instances = dict()
if self.name in TypeClass.registry:
raise KeyError(f"Duplicate typeclass with name {self.name}")
TypeClass.registry[self.name] = self
def __repr__(self):
return f"TypeClass.get({self.name!r})"
def __getitem__(self, typs):
return self.instances[typs]
@classmethod
def parse(cls, name):
return cls.get(parse(name))
@classmethod
def get(cls, name):
return cls.registry[name]
# Instance of TypeClass for specified types
class ClassData:
def __init__(self, cls, typs, methods):
if tuple(t.kind for t in typs) != tuple(cls.kinds):
raise TypeError(f"Types do not match kinds from class")
if methods.keys() != cls.methods.keys():
raise TypeError(f"Methods mismatch")
self.cls = cls
self.typs = typs
self.methods = {m: MetaData(cls.methods[m](*typs),methods[m]) for m in cls.methods}
if typs in cls.instances:
raise KeyError(f"Duplicate typeclass instance")
cls.instances[typs] = self
def __repr__(self):
return f"{self.cls!r}[{self.typs!r}]"
def __getitem__(self, m):
return self.methods[m]
# Hacks to do HOAS
class AlwaysTrue:
def __bool__(self):
return True
def __call__(self, *args):
return self
class Tester(MetaType):
def __init__(self, name, kind=None):
self.secret = name
self.name = self
self.kind = Taker() if kind is None else kind
self.pred = AlwaysTrue()
def __repr__(self):
return self.secret
def __call__(self, *params):
kind = TupleTaker(tuple(p.kind for p in params))
print(f"Guessing {kind!r}")
if not (self.kind == kind):
pass
for i,p in enumerate(params):
self = MetaType((self.name, p.name), AlwaysTrue(), kind[i+1:])
print(f"Guessed {kind!r}")
return self
class ManyTaker:
def __init__(self):
self.values = dict()
def __get__(self, i):
if i not in self.values:
self.values[i] = Taker()
return self.values[i]
class Taker:
def __init__(self):
self.hasValue = False
def __eq__(self, other):
if not self.hasValue:
#print(f"Taking {other!r} for {id(self):02X}")
self.value = other
self.hasValue = True
return True
return self.value == other
def __len__(self):
if not self.hasValue:
self.value = TupleTaker()
self.hasValue = True
return self.value.__len__()
def __getitem__(self, i):
if not self.hasValue:
self.value = TupleTaker()
self.hasValue = True
return self.value[i]
def __repr__(self):
if self.hasValue:
return repr(self.value)
else:
return f"Taker({id(self):02X})"
class TakeLen:
def __init__(self, len=0):
self.finalized = False
self.len = len
def __lt__(self, other):
if self.finalized:
return self.len < other
if self.len < other:
self.len = other
return False
class TakeLenView:
def __init__(self, parent, offset):
self.parent = parent
self.offset = offset
def __lt__(self, other):
return self.parent < other+self.offset
class TupleTaker:
def __init__(self, data=()):
self.len = TakeLen(len(data))
self.data = list(data)
def __repr__(self):
if self.len.finalized:
return repr(self.data)
while len(self.data) < self.len.len:
self.data.append(Taker())
return f"TupleTaker({self.data!r})"
def __len__(self):
return self.len
def __eq__(self, other):
if self.len.finalized:
return self.data == other
if other.len < self.len.len:
return False
self.len.len = other.len
self.len.finalized = True
self.data = tuple(other)
return True
def __getitem__(self, i):
if isinstance(i, slice):
if self.len.finalized:
return self.data[i]
if i.step is not None or i.stop is not None:
raise IndexError()
return TupleTakerView(self, i.start)
else:
if self.len < i:
raise IndexError()
while len(self.data) < self.len.len:
self.data.append(Taker())
return self.data[i]
class TupleTakerView:
def __init__(self, parent, offset):
if parent.len < offset:
raise IndexError()
self.parent = parent
self.offset = offset
def __repr__(self):
return f"TupleTakerView({self.parent!r}, {self.offset!r})"
def __len__(self):
return TakeLenView(self.parent.len, self.offset)
def __eq__(self, other):
if self.parent.len < self.offset+len(other):
return False
self.parent.len.finalized = True
self.parent.data = tuple(self.parent.data[:self.offset]) + tuple(other)
return True
def __getitem__(self, i):
if isinstance(i, slice):
s = slice(
i.start + self.offset,
None if i.stop is None else i.stop + self.offset,
i.step,
)
return self.parent[s]
else:
return self.parent[i+self.offset]
# End hacks, begin examples
# Note: I used PureScript names for these types
mtFunction = MetaType("Function", lambda a: lambda b: callable, MetaType.Bifunctor)
mtString = MetaType("String", lambda x: isinstance(x, str), MetaType.Type)
mtArray = MetaType("Array", lambda a: lambda x: isinstance(x, tuple) and all(a(y) for y in x), MetaType.Functor)
mtStrMap = MetaType("StrMap", lambda a: lambda x: isinstance(x, tuple) and all(isinstance(k, str) and a(y) for k,y in x), MetaType.Functor)
mtOrdering = MetaType("Ordering", MetaType.enum("LT","GT","EQ"))
mtNatural = MetaType("Natural", lambda x: isinstance(x, str) and int(x) >= 0)
mtTuple = MetaType("Tuple", lambda a: lambda b: lambda x: isinstance(x, tuple) and len(x) == 2 and a(x[0]) and b(x[1]), MetaType.Bifunctor)
mtJoin = MetaType("Join", lambda f: lambda a: f(a)(a), (MetaType.Bifunctor, MetaType.Type))
mtBoolean = MetaType("Boolean", MetaType.enum("true", "false"))
mtUnit = MetaType("Unit", MetaType.enum(""))
mtIdentity = MetaType("Identity", lambda a: a, MetaType.Functor)
mkIdentity = MetaData(Forall(lambda a: mtFunction(a, mtIdentity(a))), lambda a: lambda fa: MetaData(mtIdentity(a), fa))
unIdentity = MetaData(Forall(lambda a: mtFunction(mtIdentity(a), a)), lambda a: lambda fa: MetaData(a, fa))
mtPair = mtJoin(mtTuple)
def mu(f):
return f(mtMu(f))
mtMu = MetaType("Mu", mu, (MetaType.Functor,))
mtString.mk("hello")
mtArray(mtString).mk(("a","b"))
mtStrMap(mtString).mk((("k","v"),("k1","v1")))
repr(Forall(lambda x: MetaType.get(('Function', x, x))))
repr(Forall(lambda x: MetaType.get(('Function', (x, 'StrMap'), (x, 'Array')))))
comparePrim = lambda x: lambda y: ["LT","EQ","GT"][1 + (x > y) - (x < y)]
tcOrd = TypeClass("Ord", (MetaType.Type,), {
"compare": lambda a: mtFunction(a, mtFunction(a, mtOrdering))
})
tcOrdString = ClassData(tcOrd, (mtString,), { "compare": comparePrim })
tcOrdString["compare"]("a", "b")
tcFunctor = TypeClass("Functor", (MetaType.Functor,), {
"map": lambda f: Forall(lambda a: Forall(lambda b: mtFunction(mtFunction(a, b), mtFunction(f(a), f(b)))))
})
tcFunctorArray = ClassData(tcFunctor, (mtArray,), {"map": lambda a: lambda b: lambda ab: lambda aa: tuple(ab(a) for a in aa)})
tcFunctorIdentity = ClassData(tcFunctor, (mtIdentity,), {"map": lambda a: lambda b: lambda ab: lambda aa: ab(aa)})
tcApplicative = TypeClass("Applicative", (MetaType.Functor,), {
"pure": lambda m: Forall(lambda a: MetaType.get(('Function', a, (m, a)))),
"apply": lambda m: Forall(lambda a: Forall(lambda b: MetaType.get(('Function', (m, ('Function', a, b)), ('Function', (m, a), (m, b)))))),
})
tcApplicativeIdentity = ClassData(tcApplicative, (mtIdentity,), {
"pure": lambda a: lambda fa: fa,
"apply": lambda a: lambda b: lambda fab: lambda fa: mkIdentity(b, unIdentity(mtFunction(a, b), fab, unIdentity(a, fa))),
})
tcApplicativeArray = ClassData(tcApplicative, (mtArray,), {
"pure": lambda a: lambda fa: (fa,),
"apply": lambda a: lambda b: lambda fab: lambda fa: tuple(ab(a) for ab in fab for a in fa),
})
tcContainer = TypeClass("Container", (MetaType.Type,MetaType.Functor,), {
"mapWithIndex": lambda i, f: Forall(lambda a: Forall(lambda b: MetaType.get(('Function', ('Function', i, ('Function', a, b)), ('Function', (f, a), (f, b)))))),
})
tcTraversable = TypeClass("Traversable", (MetaType.Functor,), {
"sequence": lambda f: Forall(lambda m: Forall(lambda a: MetaType.get(('Function', (f, (m, a)), (m, (f, a)))))),
})
mapWithIndexPrim = lambda a: lambda b: lambda mapper: lambda aa: tuple(mapper(str(i))(aa[i]) for i in range(len(aa)))
tcContainerArray = ClassData(tcContainer, (mtNatural,mtArray), {
"mapWithIndex": mapWithIndexPrim
})
tcContainerPair = ClassData(tcContainer, (mtBoolean,mtJoin(mtTuple)), {
"mapWithIndex": lambda a: lambda b: lambda mapper: lambda aa: (mapper("false")(aa[0]), mapper("true")(aa[1]))
})
# sequence (Pair fa0 fa1) = (\a0 a1 -> Pair a0 a1) <$> fa0 <*> fa1
tcTraversablePair = ClassData(tcTraversable, (mtPair,), {
"sequence": lambda m: lambda a: lambda aa: tcApplicative[(m,)]["apply"](a, mtPair(a), tcFunctor[(m,)]["map"](a, mtFunction(a, mtPair(a)), lambda a0: lambda a1: (a0, a1), aa[0]), aa[1]),
})
def sequenceArrayPrim(m, a, aa):
apM = tcApplicative[(m,)]
fnM = tcFunctor[(m,)]
r = apM["pure"](mtArray(a), tuple())
for mai in aa:
r = apM["apply"](a, mtArray(a), fnM["map"](mtArray(a), mtFunction(a, mtArray(a)), lambda ar: lambda ai: (*ar, ai), r), mai)
return r
tcTraversableArray = ClassData(tcTraversable, (mtArray,), {
"sequence": lambda m: lambda a: lambda aa: sequenceArrayPrim(m, a, aa),
})
tcFunctorIdentity["map"](mtNatural, mtString, lambda s: s + s, "34")
tcContainerArray["mapWithIndex"](mtString, mtTuple(mtNatural, mtString), lambda i: lambda v: (i, v), ("a","b"))
tcContainerPair["mapWithIndex"](mtNatural, mtNatural, lambda d: lambda n: str(int(n) * 2 + (d == "true")), ("6", "10"))
tcTraversablePair["sequence"](mtIdentity, mtString, ("",""))
tcTraversablePair["sequence"](mtArray, mtString, (("a","c"),("b","d")))
tcTraversableArray["sequence"](mtArray, mtString, (("a","1"),("b","2"),("c","3")))
# Okay, now we're getting to the Dhall language sketches
# Suggested format for syntax types
# Define a functor for one layer of syntax
mtBoolExprF = MetaType("BoolExprF", lambda e: MetaType.abstractSpec(
( "Bool"
, ("if_then_else_", e, e, e)
, ("BoolLit", mtBoolean)
)
), MetaType.Functor)
# And make it recursive
mtBoolExpr = mtMu(mtBoolExprF)
mtBoolExpr.mk("Bool")
mtBoolExpr.mk(("BoolLit", "true"))
mtBoolExpr.mk(("if_then_else_", ("BoolLit", "true"), ("BoolLit", "false"), ("BoolLit", "true")))
# Rule form:
# - S-exp style (prefix) for rules and data
# - Rules specify name/aliases, attributes, arity, and input/output types
# - Name of n-ary rule, n arguments, sideconditions, and finally the result
# - Each rule can be thought of as specifying an algorithm in an appropriate
# monadic context
#
# Matching forms:
# - String literals and S-exp constructor literals
# - `m.var` matcher matches and binds `var`
# - Repeated matchers and nested matches match up to specified equality
# (short for a side-condition of specified equality)
# - `m._` matches anything and binds nothing
# - `m.var("c", a, b)` matches a constructor literal as well as binding `var`,
# like at-patterns in Haskell/Purescript
# - `m.var["l"]` matches a string literal as well as binding `var`
# - `m(func, i1, i2, ..., im, o)` is a sidecondition
# - `m[i1, i2, ..., im, m(c1), m(c2), ..., m(cn), o][...]...` is a m-ary
# multicase lambda that matches m inputs and returns an output based on those
# matches, depending on the side-conditions c1, c2, ..., cn. Note: inherits
# matching semantics from parent rule.
#
# Meta-judgments?
# - "traverse"
# - "ensure": converts a pattern match failure to the given error
#
# Attributes:
# - "external": Has separate external implementation
# - "inline": Inline this rule wherever it occurs
# - "match:judgmental-equality": Use jugmental equality (syntactic is default)
#
# Desugaring:
# - Repeated matchers `m.v, m.v` get desugared to separate matchers
# `m.v1, m.v2` with sidecondition `m("equality", m.v1, m.v2, m.v)`
# (with the type of equality specified in the rule)
# - Nested matches `("constr", m.vs...)` get desugared to a matcher `m.v`
# with sidecondition `m("match", m.v, ("constr", m.vs...))`
# (with the type of match normalization specified in the rule)
# - Case analysis optimizations, totality checking?
# - Parallel applicative vs sequential monad optimization?
# - Optimization, e.g. optimized alpha-beta normalization generated from mix?
# - "ensure" with a single pattern match will be compiled to unification,
# a multipattern match is not possible, so first one will have to match on the
# specified cases, and then the fallback will be to "ensure" the combined
# constructor (e.g. `m(m[a, x][b, y][m._, m("ensure", m.v, a_or_b), z], m.v)`)
#
# Open problems:
# - Provenance ……… for efficiency, we don't want to represent it in the tree,
# but then we have to deal with passing it down? meh
"""
itraverseRTogether :: forall i m t f.
Recursive t f =>
Corecursive t f =>
TraversableWithIndex i f =>
Merge f =>
Applicative m =>
(i -> Pair t -> m t) -> t -> t -> Maybe (m t)
itraverseRTogether f l r =
(map embed <<< traverseWithIndex f) <$>
(mergeWith Pair `on` project) l r
"""
# Class for my weird matching syntax as explained above
#
# Matches can be variables and values, where the values are string literals or
# tuples with nested matches.
#
# There are also lambda-cases, which take some inputs and case on them
# and return some output after computation.
#
# Statements are for computation, so you can reference either lambdas
# (for casing on a known result) or globally defined functions, with some
# arguments provided and then matching on the result.
#
# All matches are partial, all functions are partial.
class Matcher:
def OrLambda(v):
if isinstance(v, Matcher.Lambda):
return v
return Matcher(v)
class Statement:
def __init__(self, fn, inputs, output):
self.fn = fn
self.inputs = tuple(Matcher.OrLambda(i) for i in inputs)
self.output = Matcher(output)
def copy(self):
return Statement(self.fn, tuple(i.copy() for i in self.inputs), self.output.copy())
def __repr__(self):
return "m"+repr(tuple([self.fn, *self.inputs, self.output]))
def unparse(self):
r = ""
calling = " " + " ".join(v.unparse() for v in self.inputs) + " => " + self.output.unparse()
if isinstance(self.fn, Matcher.Lambda):
r += "?" + calling + "\n"
for c in self.fn.cases:
r += "|" + c.unparse()
r += "!"
elif isinstance(self.fn, Builtin):
r += "builtin" + "/" + self.fn.key + calling
else:
r += self.fn + calling
return r
class Lambda:
class Case:
def __init__(self, inputs, stmts, output, name=None):
self.name = name
self.inputs = tuple(Matcher(i) for i in inputs)
self.stmts = stmts
self.output = Matcher.OrLambda(output)
def copy(self):
other = Lambda.Case(self.inputs, tuple(s.copy for s in self.stmts), self.output.copy())
def __repr__(self):
return repr([*self.inputs, *self.stmts, self.output])
def unparse(self):
r = ""
for i in self.inputs:
r += " " + i.unparse()
r += " => " + self.output.unparse() + "\n"
for s in self.stmts:
r += " " + s.unparse().replace("\n", "\n ") + "\n"
return r
def __init__(self, cases=()):
self.cases = cases
def copy(self):
return Lambda(tuple(c.copy() for c in self.cases))
def __repr__(self):
if not len(self.cases):
return "m.Lambda()"
return "m" + "".join(repr(c) for c in self.cases)
def unparse(self):
r = "%"
for i,c in enumerate(self.cases):
r += (" |" if i else "") + c.unparse()
if i == 0:
r = r[:-1] + " "
return r + "!"
def __getitem__(self, args):
assert isinstance(args, tuple)
assert len(args) > 1
name = None
if isinstance(args[0], slice):
if slice.step is not None:
raise TypeError(f"Triple colon not supported for lambda case")
name = args[0].start
args[0] = args[0].stop
inputs, statements = [], []
for a in args[:-1]:
(inputs, statements)[isinstance(a, Matcher.Statement)].append(a)
output = args[-1]
case = Matcher.Lambda.Case(tuple(inputs), tuple(statements), output, name)
return Matcher.Lambda(tuple([*self.cases, case]))
def __init__(self, value=None, name=()):
while isinstance(value, Matcher):
name = value.name
value = value.value
self.name = name
if value is None:
self.value = value
else:
def validate(arg):
if isinstance(arg, tuple):
return tuple(validate(a) for a in arg)
else:
assert isinstance(arg, str) or isinstance(arg, Matcher) or arg is Ellipsis
return arg
try:
self.value = validate(value)
except AssertionError:
raise TypeError(f"Invalid Matcher value: {value!r}")
def copy(self):
return Matcher(self)
def __repr__(self):
if self.name == ():
if self.value is None:
return "m"
elif isinstance(self.value, tuple):
return "m"+repr(self.value)
elif isinstance(self.value, str):
return repr(self.value)
elif self.value is Ellipsis:
return "m[...]"
else:
return "m??"
else:
if self.name is None:
pre = "m._"
else:
pre = "m." + ".".join(self.name)
if self.value is None:
return pre
else:
if isinstance(self.value, str):
return f"{pre}[{self.value!r}]"
elif self.value is Ellipsis:
return f"{pre}[...]"
return f"{pre}{self.value!r}"
def unparse(self):
if self.name is None:
pre = "_"
else:
pre = ".".join(self.name)
if self.value is None:
return pre
elif pre:
pre += "@"
if isinstance(self.value, tuple):
return pre+"[" + " ".join(Matcher(v).unparse() for v in self.value) + "]"
elif isinstance(self.value, str):
return f"{pre}{self.value!r}"
elif self.value is Ellipsis:
return f"{pre}..."
return f"{pre}{self.value.unparse()}"
def __getattr__(self, name):
if self.value is not None:
raise TypeError(f"Put variable before value")
if self.name != ():
raise TypeError(f"Cannot bind two names at once")
if name == "_": return Matcher(None, None)
return Matcher(None, tuple([*self.name, name]))
def __call__(self, *args):
if self.name == ():
return Matcher.Statement(args[0], args[1:-1], args[-1])
if self.value is not None:
raise TypeError(f"Multimatch is not supported")
return Matcher(args, self.name)
def __getitem__(self, i):
if self.name == ():
return Matcher.Lambda()[i]
if self.value is not None:
raise TypeError(f"Multimatch is not supported")
return Matcher(i, self.name)
class MatchError(Exception):
__module__ = Exception.__module__
pass
@staticmethod
def record(name, value, vars):
if name in vars:
if value != vars[name]:
raise Matcher.MatchError(Matcher(value, name), vars[name])
else:
vars[name] = value
def verify_pattern_pair(left, right):
def verify(m):
if isinstance(m, str):
return
if isinstance(m, tuple):
ell = False
for mm in m:
if isinstance(mm, Matcher) and mm.value is Ellipsis:
if ell:
raise ValueError(f"Can only match against one ellipsis at once")
ell = True
if mm.name is None or mm.name == ():
raise ValueError(f"Ellipsis must be named in pattern pair")
else:
verify(mm)
return
if isinstance(m, Matcher):
if m.name is not None and m.name != ():
vars.add(m.name)
if m.value is not None:
verify(m.value)
return
raise ValueError(f"Unknown data in pattern: {m!r}")
vars = set()
verify(left)
lvars = set(vars)
vars = set()
verify(right)
rvars = set(vars)
if lvars != rvars:
raise ValueError(f"Pattern pair must use same variables")
def match(m, v, vars=None):
if vars is None: vars = dict()
if isinstance(m, str):
if m != v:
raise Matcher.MatchError(m, v)
return vars
if isinstance(m, tuple):
if not isinstance(v, tuple):
raise Matcher.MatchError(m, v)
i = None
for j,mm in enumerate(m):
if isinstance(mm, Matcher) and mm.value is Ellipsis:
if i is None:
i = j
else:
raise ValueError(f"Can only match against one ellipsis at once")
if i is not None:
e = m[i]
if len(m)-1 > len(v):
raise Matcher.MatchError(m, v)
j = (i+1)-len(m)+len(v)
Matcher.match(m[:i], v[:i], vars)
if e.name is not None and e.name != ():
Matcher.record(e.name, v[i:j], vars)
Matcher.match(m[i+1:], v[j:], vars)
else:
if len(m) != len(v):
raise Matcher.MatchError(m, v)
for i in range(len(m)):
Matcher.match(m[i], v[i], vars)
return vars
if isinstance(m, Matcher):
if m.value is not None:
Matcher.match(m.value, v, vars)
if m.name is not None and m.name != ():
Matcher.record(m.name, v, vars)
return vars
raise ValueError(f"Invalid value in Matcher: {m!r}")
def instantiate(m, vars=None):
if vars is None:
vars = dict()
if isinstance(m, str):
return m
if isinstance(m, tuple):
i = None
for j,mm in enumerate(m):
if isinstance(mm, Matcher) and mm.value is Ellipsis:
if i is None:
i = j
else:
raise ValueError(f"Can only match against one ellipsis at once")
if i is not None:
e = m[i]
j = (i+1)-len(m)
r0 = Matcher.instantiate(m[:i], vars)
if e.name is not None and e.name != ():
r1 = vars[e.name]
else:
raise ValueError(f"Unnamed ellipsis cannot be instantiated")
r2 = Matcher.instantiate(m[j:], vars)
return r0 + r1 + r2
else:
return tuple(Matcher.instantiate(mm, vars) for mm in m)
if isinstance(m, Matcher):
if m.value is not None:
v = Matcher.instantiate(m.value, vars)
if m.name is not None and m.name != ():
Matcher.record(m.name, v, vars)
return v
else:
if m.name is not None and m.name != ():
return vars[m.name]
else:
raise ValueError(f"Cannot instantiate matcher without value and without name")
# Class for reifying it into actual data and processing it
class Description:
Types = "# Types"
Patterns = "# Patterns"
Rules = "# Rules"
Laws = "# Laws"
modes = set([Types, Patterns, Rules])
# Parse the data from a list of rules into a slightly more structured
# representation
def __init__(self, *data):
# by name
type_aliases = dict()
self.types = dict()
# by type
ptrn_aliases = dict()
self.ptrns = dict()
# by name
func_aliases = dict()
self.funcs = dict()
mode = None
for (linenum, line) in enumerate(data):
try:
if line in Description.modes:
mode = line
continue
if mode == Description.Types:
if isinstance(line, str):
continue
assert isinstance(line, tuple) and len(line)
if line[0] == "alias":
assert len(line) == 3
alias = line[1]
alibi = line[2]
if alias in type_aliases:
raise KeyError(f"Duplicate type alias")
type_aliases[alias] = alibi
continue
if mode == Description.Patterns:
if isinstance(line, str):
continue
assert isinstance(line, tuple)
assert len(line) == 3
ty = line[0]
left = line[1]
right = line[2]
Matcher.verify_pattern_pair(left, right)
if ty not in self.ptrns:
self.ptrns[ty] = []
self.ptrns[ty].append((Matcher(left), Matcher(right)))
continue
if mode == Description.Rules:
if isinstance(line, str):
continue
assert isinstance(line, tuple)
if isinstance(line[0], tuple):
name = line[0][0]
assert isinstance(name, str)
aliases = line[0][1:]
section = None
else:
assert isinstance(line[0], str)
parts = line[0].split("/")
name = parts[0]
section = tuple(parts[1:])
aliases = None
if name not in self.funcs:
if section:
raise TypeError(f"Missing definition of {name}")
for alias in aliases or []:
assert isinstance(alias, str)
func_aliases[alias] = name
attrs = line[1]
assert isinstance(attrs, tuple)
signature = line[2:]
self.funcs[name] = Description.Function(attrs, signature)
else:
if aliases:
raise TypeError(f"Duplicate definition or malformed syntax")
self.funcs[name].add_case(*line[1:], name=section)
pass
continue
except Exception as e:
if len(e.args) == 1:
raise type(e)(e.args[0] + f" at line {linenum+1}: {line}")
raise Exception(e, f"at line {linenum+1}: {line}")
raise TypeError(f"Missing mode (start with Description.Types or Description.Rules)")
def copy(self):
other = Description()
other.types = {k:v.copy() for k,v in self.types.items()}
other.ptrns = {k:v.copy() for k,v in self.ptrns.items()}
other.funcs = {k:v.copy() for k,v in self.funcs.items()}
return other
class Function:
def __init__(self, attrs, signature):
self.attrs = attrs
self.inputs = signature[:-1]
self.output = signature[-1]
self.spec = Matcher.Lambda()
def copy(self):
other = Function(self.attrs, self.inputs + (self.output,))
other.spec = self.spec.copy()
return other
def add_case(self, *args, **kwargs):
self.spec = self.spec[args]
case = self.spec.cases[-1]
case.name = kwargs['name']
if len(case.inputs) != len(self.inputs):
raise TypeError(f"Wrong number of inputs, {len(case.inputs)} vs {len(self.inputs)}")
def unparse(self, name):
r = name + " :: " + " -> ".join(pretty(v) for v in [*self.inputs, self.output]) + "\n"
for case in self.spec.cases:
r += name + "/" + ("/".join(case.name) + "/" if len(case.name) and case.name != ("",) else "")
r += case.unparse()
return r
def unparse(self):
r = ""
for name in self.funcs:
r += self.funcs[name].unparse(name)
r += "\n"
return r
def inline(self):
pass
def add_method(cls):
def decorator(func):
setattr(cls, func.__name__, func)
return None
return decorator
# Compilation methods
# - helpers:
def nextFree(used, name):
try:
i = int(name[-1])
name = name[:-1]
except:
i = 0
while (ret := tuple((*name, str(i)))) in used:
i += 1
used.add(ret)
return ret
# - linearization:
# - v1 =[v]= v2 -- just need to rename input occurrences and add
# side-conditions, output stays the same
# - first calculate which variables need to change
# - then for each, keep track of { [original_name]: latest_name }
# - first occurrence: instantiate original_name and latest_name with new name
# - next occurrences: rename, join this name with lastest name to another new
# name in statement, update map
# - at end, tie latest_name back to original_name via identity function
@add_method(Description)
def linearize(self):
for f in self.funcs:
self.funcs[f].linearize()
@add_method(Description.Function)
def linearize(self):
matcher = "eq"
tag = "match:"
for attr in self.attrs:
if attr[:len(tag)] == tag:
matcher = attr[len(tag):]
self.spec.linearize(matcher, dict())
@add_method(Matcher.Lambda)
def linearize(self, matcher, vars):
for c in self.cases:
c.linearize(matcher, vars)
@add_method(Matcher.Lambda.Case)
def linearize(self, matcher, vars):
M = m
# This visits all the matchers used in inputs positions.
# It only recurses into lambdas if stacker is not None, though.
# (In particular, for gathering used variables, cases operate
# independently, with their results merged together.)
def visitinputs(visitor, m, stacker=None):
if isinstance(m, tuple):
for v in m:
visitinputs(visitor, v)
# If we are visiting a Matcher:
if type(m) == Matcher:
# Visit it if it has a name
if m.name is not None and m.name != ():
visitor(m)
# And visit its children:
visitinputs(visitor, m.value)
# If we are visiting a Lambda, descend only if we have a stacker:
if type(m) == Matcher.Lambda and stacker is not None:
# Push the stack
stacker[0]()
for v in m.cases:
# Prep the stack
stacker[1]()
visitinputs(visitor, v)
# Get the result off the stack
stacker[2]()
# Pop the stack
stacker[3]()
# If we are visiting a Case:
if type(m) == Matcher.Lambda.Case:
# Visit the inputs:
for v in m.inputs:
visitinputs(visitor, v, stacker)
# Visit the outputs of each statement:
for s in m.stmts:
visitinputs(visitor, s.output, stacker)
# And descend into the output, if it is a Lambda:
if isinstance(m.output, Matcher.Lambda):
visitinputs(visitor, m.output, stacker)
# We prep the used variables from the keys of vars
used = set(vars)
# And start by assuming 0 duplicates:
dups = set()
# Stack for recursion in Lambdas:
stack = []
def push_stack():
# running total (used,dups) then reset state (used,dups)
stack.append((used, dups, used, dups))
def stack_start():
# reset state from latter half of last item on stack
used = set(stack[-1][2])
dups = set(stack[-1][3])
def stack_end():
# accumulate the running total back into the stack
stack[-1][0].update(used)
stack[-1][1].update(dups)
def pop_stack():
# pop the result off of the stack
(used, dups) = stack.pop()[:2]
def collect(m):
if m.name in used:
dups.add(m.name)
else:
used.add(m.name)
visitinputs(collect, self, (push_stack, stack_start, stack_end, pop_stack))
#print((used, dups))
if len(dups) and matcher is None:
offenses = tuple(Matcher(name=d) for d in dups)
if len(offenses) == 1: offenses = offenses[0]
raise ValueError(f"No matching semantics specified for duplicate variables {offenses!r}")
preused = set(used)
# Okay, now we maintain a map of original_name to latest_name
# as we start renaming variables:
vars = dict(vars)
# And a list of sideconditions:
pre = []
def renamer(m):
# If we see a name we've seen before:
if m.name in vars:
# Remember the latest name
lst = vars[m.name]
# Generate two new names
# (note: automatically added to used)
new = nextFree(used, lst)
dst = nextFree(used, new)
# Update the latest name
vars[m.name] = dst
# Rename to bind the new name instead
m.name = new
# And add side condition (lst =[dst]= new)
pre.append(M(matcher, Matcher(name=lst), Matcher(name=new), Matcher(name=dst)))
# If it is a new name:
elif m.name in dups:
# Simply rename freshly and record the new name:
vars[m.name] = nextFree(used, m.name)
m.name = vars[m.name]
# Now run it! over all the inputs of self and outputs of statements of self
visitinputs(renamer, self)
# Descend into the tail:
if isinstance(self.output, Matcher.Lambda):
# We need to keep track of the variables we generated,
# so we pass it down as part of vars
for k in used.difference(preused):
if k not in vars:
vars[k] = None
self.output.linearize(matcher, vars)
# Or, if there is no tail, do bookkeeping:
else:
# We could really just rename all variables in output, but it seems nice
# to use the intended name in the output, so we add assignments from the
# new name to the intended name:
post = []
for (old,new) in vars.items():
if new is not None:
post.append(M("identity", Matcher(name=new), Matcher(name=old)))
self.stmts = tuple(post) + self.stmts
# Add the preconditions to the list of statements
self.stmts = tuple(pre) + self.stmts
del linearize
m = Matcher()
def test(h):
return
print(h)
h.linearize("eq", dict())
print(h)
print("---")
test(m[m.v, m.v][m.v, m.v])
test(m[m.v, m.v, m.v])
test(m[m.v, m[m.v, m.v]])
test(m[m.v, m["", m.v][m.v, m.v]])
class getter:
def __init__(self, wrapper=None):
if wrapper is None:
wrapper = lambda x: x
self.wrapper = wrapper
def __getitem__(self, x):
return self.wrapper(x)
class Builtin:
def __init__(self, key):
self.key = key
builtins = getter(Builtin)
Builtins =\
( "Natural/build"
, "Natural/fold"
, "Natural/isZero"
, "Natural/even"
, "Natural/odd"
, "Natural/toInteger"
, "Natural/show"
, "Natural/subtract"
, "Integer/toDouble"
, "Integer/show"
, "Integer/negate"
, "Integer/clamp"
, "Double/show"
, "List/build"
, "List/fold"
, "List/length"
, "List/head"
, "List/last"
, "List/indexed"
, "List/reverse"
, "Text/show"
, "Text/replace"
, "Bool"
, "Optional"
, "Natural"
, "Integer"
, "Double"
, "Text"
, "List"
, "True"
, "False"
, "None"
, "Date"
, "Time"
, "TimeZone"
)
rules = Description\
( Description.Types
# Just a sketch for now
# but the idea is that Text and List are the only primitives
, ("primitive", "Text")
, ("primitive", "List")
# and everything else is derived as like subtypes satisfying predicates
# FIXME
, ("subtype", "Natural", "[0-9]+")
, ("subtype", "Integer", "[-+][0-9]+")
, ("subtype", "Double", "[-+][0-9]+(.[0-9]+)?")
, ("enum", "Bool", "True", "False")
, ("enum", "Constant", "Type", "Kind", "Sort")
, ("alias", "VariableName", "Text")
, ("alias", "VariableIndex", "Natural")
# note to self: m.a() kind annotation, takes 0 arguments
, ("adt", m.a(), "Optional", "None", ("Some", m.a))
, ("adt", m.a(), m.b(), "These", ("This", m.a), ("That", m.b), ("These", m.a, m.b))
, ("adt", m.a(), "Projection", ("Labels", ("ByList", "Text")), ("ByType", m.a))
, ("adt", m.a(), "TextLitF", ("TextLit", "Text"), ("TextInterp", "Text", m.a, ("TextLitF", m.a)))
, ("adt", m.a(), "ExprF",
("Variable", "VariableName", "VariableIndex"),
("Lambda", "Text", m.a, m.a),
("Forall", "Text", m.a, m.a),
("Let", "Text", ("Optional", m.a), m.a, m.a),
("If", m.a, m.a, m.a),
("Merge", m.a, m.a, ("Optional", m.a)),
("ToMap", m.a, ("Optional", m.a)),
("ListLit", ("List", m.a), ("Optional", m.a)),
("Annotation", m.a, m.a),
("||", m.a, m.a),
("+", m.a, m.a),
("++", m.a, m.a),
("#", m.a, m.a),
("&&", m.a, m.a),
("/\\", m.a, m.a),
("//", m.a, m.a),
("//\\\\", m.a, m.a),
("*", m.a, m.a),
("==", m.a, m.a),
("!=", m.a, m.a),
("===", m.a, m.a),
("?", m.a, m.a),
("Application", m.a, m.a),
("Field", m.a, "Text"),
("Project", m.a, ("Projection", m.a)),
("Completion", m.a, m.a),
("Assert", m.a),
("With", m.a, ("NonEmpty", "Text"), (m.a)),
("DoubleLit", "Double"),
("NaturalLit", "Natural"),
("IntegerLit", "Integer"),
("TextLit", ("TextLitF", m.a)),
("DateLit", "Date"),
("TimeLit", "Time"),
("TimeZoneLit", "TimeZone"),
("RecordType", ("Map", "Text", m.a)),
("RecordLiteral", ("Map", "Text", m.a)),
("UnionType", ("Map", "Text", ("Optional", m.a))),
("Import", "Import"),
("Some", m.a),
*Builtins,
("Constant", "Constant"),
)
, Description.Patterns
# Desugar ("Application", f, a, b, c) to ("Application", ("Application", ("Application", f, a), b), c)
, ("Expr", ("Application", m.a[...], m.a1, m.a2, m.a3), ("Application", ("Application", m.a[...], m.a1, m.a2), m.a3))
# Desugar ("List", a) to ("Application", "List", a)
, ("Expr", ("List", m.a), ("Application", "List", m.a))
, Description.Rules
# Potential for optimization to add unsafeRefEq for comparing expressions
# Note: these equality operators take two arguments and return the "merged"
# expression (important for metadata later)
, (("reference-equality", "refeq"), ("external",), m.a, m.a, m.a)
, ("reference-equality/", m.o, m.o, m.o)
# Syntactic equality
, (("syntactic-equality", "eq"), (), "Expr", "Expr", "Expr")
, ("syntactic-equality/reference-equality", m.l, m.r, m("reference-equality", m.l, m.r, m.o), m.o) # optimization
, ("syntactic-equality/", m.l, m.r,
m("traverseRTogether", m[(m.x, m.y), m("syntactic-equality", m.x, m.y, m.z), m.z], m.l, m.r, ("Some", m.o)),
m.o
)
# Judgmental equality via alpha-beta-normalization
, (("judgmental-equality", "judgeq"), (), "Expr", "Expr", "Expr")
, ("judgmental-equality/reference-equality", m.l, m.r, m("reference-equality", m.l, m.r, m.o), m.o) # optimization
, ("judgmental-equality/", m.l, m.r,
m("alpha-beta-normalize", m.l, m.x),
m("alpha-beta-normalize", m.r, m.y),
m("syntactic-equality", m.x, m.y, m.o),
m.o
)
# If the Expr is constant on a variable (considered at index 0)
# then return the constant (i.e. shift out the variable)
, ("constant", (), "Text", "Expr", "Expr")
, ("constant/", m.v, m.e,
m("shift", "-1", m.v, "0", m.e, m.r),
m.r
)
# ("shift-nat", d, n, n - d) if n-d>=0
, ("shift-nat", ("external",), "Integer", "Natural", "Natural")
, ("le", ("external",), "Natural", "Natural", "Bool")
# Increment the last argument if the first two are equal
, ("if-eq-suc", (), "Text", "Text", "Natural", "Natural")
, ("if-eq-suc/eq", m.v, m.v, m.m, m("suc", m.m, m.m1), m.m1)
, ("if-eq-suc/neq", m._, m._, m.m, m.m)
, ("shift", (), "Integer", "Text", "Natural", "Expr", "Expr")
, ("shift/Variable", m.d, m.v, m.m, m.e("Variable", m.v, m.n),
m("le", m.m, m.n, "True"),
m("ensure-shift-nat", m.d, m.n, m.nd),
("Variable", m.v, m.nd),
)
, ("shift/Lambda", m.d, m.v, m.m, m.e("Lambda", m.u, m.A0, m.b0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("shift", m.d, m.v, m.m, m.A0, m.A1),
m("shift", m.d, m.v, m.m1, m.b0, m.b1),
("Lambda", m.u, m.A1, m.b1)
)
, ("shift/Forall", m.d, m.v, m.m, m.e("Forall", m.u, m.A0, m.B0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("shift", m.d, m.v, m.m, m.A0, m.A1),
m("shift", m.d, m.v, m.m1, m.B0, m.B1),
("Forall", m.u, m.A1, m.B1)
)
, ("shift/Let", m.d, m.v, m.m, m.e("Let", m.u, m.mA0, m.a0, m.b0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("traverse", m.mA0, m[m.A0, m("shift", m.d, m.v, m.m, m.A0, m.A1), m.A1], m.mA1),
m("shift", m.d, m.v, m.m, m.a0, m.a1),
m("shift", m.d, m.v, m.m1, m.b0, m.b1),
("Let", m.u, m.mA1, m.a0, m.b1)
)
, ("shift/Application", m.d, m.v, m.m, ("Application", m.f0, m.a0),
m("shift", m.d, m.v, m.m, m.f0, m.f1),
m("shift", m.d, m.v, m.m, m.a0, m.a1),
("Application", m.f1, m.a1)
)
, ("shift/Type", m.d, m.v, m.m, "Type", "Type")
, ("shift/Variable", m._, m._, m._, m.v("Variable", m._, m._), m.v)
, ("shift/", m.d, m.v, m.m, m.e1,
m("traverseR", m.e1, m[m.se1, m("shift", m.d, m.v, m.m, m.se1, m.se2), m.se2], m.e2),
m.e2
)
, (("substitute", "subst"), (), "Text", "Natural", "Expr", "Expr", "Expr")
, ("substitute/Variable-match", m.v, m.m, m.r, ("Variable", m.v, m.m), m.r)
, ("substitute/Lambda", m.v, m.m, m.r, ("Lambda", m.u, m.A0, m.b0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("substitute", m.v, m.m, m.r, m.A0, m.A1),
m("shift", "1", m.u, "0", m.r, m.r1),
m("substitute", m.v, m.m1, m.r1, m.b0, m.b1),
("Lambda", m.u, m.A1, m.b1)
)
, ("substitute/Forall", m.v, m.m, m.r, ("Forall", m.u, m.A0, m.B0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("substitute", m.v, m.m, m.r, m.A0, m.A1),
m("shift", "1", m.u, "0", m.r, m.r1),
m("substitute", m.v, m.m, m.r1, m.B0, m.B1),
("Forall", m.u, m.A1, m.B1)
)
, ("substitute/Let", m.v, m.m, m.r, ("Let", m.v, m.mA0, m.a0, m.b0),
m("if-eq-suc", m.v, m.u, m.m, m.m1),
m("substitute", m.v, m.m, m.r, m.A0, m.A1),
m("shift", "1", m.v, "0", m.r, m.r1),
m("substitute", m.v, m.m1, m.r1, m.b0, m.b1),
("Lambda", m.v, m.A1, m.b1)
)
, ("substitute/", m.v, m.m, m.r, m.e1,
m("traverseR", m.e1, m[m.se1, m("substitute", m.v, m.m, m.r, m.se1, m.se2), m.se2], m.e2),
m.e2
)
, ("shift-substitute-shift", ("inline",), "Text", "Expr", "Expr", "Expr")
, ("shift-substitute-shift/", m.v, m.r0, m.e0,
m("shift", "1", m.v, "0", m.r0, m.r1),
m("substitute", m.v, "0", m.r1, m.e0, m.e1),
m("shift", "-1", m.v, "0", m.e1, m.e2),
m.e2
)
, ("rename-immediate", (), "Text", "Text", "Expr", "Expr")
, "Interestingly, this case is needed for correctness, not efficiency."
, ("rename-immediate/noop", m.v, m.v, m.e, m.e)
, ("rename-immediate/", m.v, m.u, m.e0,
m("shift-substitute-shift", m.v, ("Variable", m.u, "0"), m.e0, m.e1),
m.e1
)
, (("alpha-normalize", "alpha"), (), "Expr", "Expr")
, ("alpha-normalize/Lambda", ("Lambda", m.v, m.A0, m.b0),
m("alpha-normalize", m.A0, m.A1),
m("rename-immediate", m.v, "_", m.b0, m.b1),
m("alpha-normalize", m.b1, m.b2),
("Lambda", "_", m.A1, m.b2)
)
, ("alpha-normalize/Forall", ("Forall", m.v, m.A0, m.B0),
m("alpha-normalize", m.A0, m.A1),
m("rename-immediate", m.v, "_", m.B0, m.B1),
m("alpha-normalize", m.B1, m.B2),
("Forall", "_", m.A1, m.B2)
)
, ("alpha-normalize/Let", ("Let", m.v, m.mA0, m.a0, m.b0),
m("traverse", m.mA0, m[m.A0, m("alpha-normalize", m.A0, m.A1), m.A1], m.mA1),
m("alpha-normalize", m.a0, m.a1),
m("rename-immediate", m.v, "_", m.b0, m.b1),
m("alpha-normalize", m.b1, m.b2),
("Let", "_", m.mA1, m.a1, m.b2)
)
, ("alpha-normalize/", m.e0,
m("traverseR", m.e0, m[m.se0, m("alpha-normalize", m.se0, m.se1), m.se1], m.e1),
m.e1
)
, (("beta-normalize", "beta"), ("match:judgmental-equality",), "Expr", "Expr")
, ("beta-normalize/Bool/if_then_else_", ("if_then_else_", ("BoolLit", m.b), m.l, m.r), m(builtins["if_then_else_"], m.b, m.l, m.r, m.o), m.o)
, ("beta-normalize/Bool/if_then_else_/identity", ("if_then_else_", m.b, ("BoolLit", "true"), ("BoolLit", "false")), m.b)
, ("beta-normalize/Bool/if_then_else_/constant", ("if_then_else_", m._, m.e, m.e), m.e)
# It would be cool if we could automatically check confluence
# (unify patterns and check equality)
# Maybe generate runtime assertions that builtins["||"]("True", "True") == "True"
, ("beta-normalize/Bool/||/L-absorb", ("||", m.l("BoolLit", "True"), m._), m.l)
, ("beta-normalize/Bool/||/L-identity", ("||", m._("BoolLit", "False"), m.r), m.r)
, ("beta-normalize/Bool/||", ("||", ("BoolLit", m.l), ("BoolLit", m.r)), m(builtins["||"], m.l, m.r, m.o), ("BoolLit", m.o))
, ("beta-normalize/Bool/||/R-absorb", ("||", m._, m.r("BoolLit", "True")), m.r)
, ("beta-normalize/Bool/||/R-identity", ("||", m.l, m._("BoolLit", "False")), m.l)
, ("beta-normalize/Bool/||/idempotence", ("||", m.e, m.e), m.e)
, ("beta-normalize/Bool/&&/L-absorb", ("&&", m.l("BoolLit", "False"), m._), m.l)
, ("beta-normalize/Bool/&&/L-identity", ("&&", m._("BoolLit", "True"), m.r), m.r)
, ("beta-normalize/Bool/&&", ("&&", ("BoolLit", m.l), ("BoolLit", m.r)), m(builtins["&&"], m.l, m.r, m.o), ("BoolLit", m.o))
, ("beta-normalize/Bool/&&/R-absorb", ("&&", m._, m.r("BoolLit", "False")), m.r)
, ("beta-normalize/Bool/&&/R-identity", ("&&", m.l, m._("BoolLit", "True")), m.l)
, ("beta-normalize/Bool/&&/idempotence", ("&&", m.e, m.e), m.e)
, ("beta-normalize/Bool/==/L-identity", ("==", m._("BoolLit", "True"), m.r), m.r)
, ("beta-normalize/Bool/==", ("==", ("BoolLit", m.l), ("BoolLit", m.r)), m(builtins["=="], m.l, m.r, m.o), ("BoolLit", m.o))
, ("beta-normalize/Bool/==/R-identity", ("==", m.l, m._("BoolLit", "True")), m.l)
, ("beta-normalize/Bool/==/idempotence", ("==", m.e, m.e), m.e)
, ("beta-normalize/Bool/!=/L-identity", ("!=", m._("BoolLit", "False"), m.r), m.r)
, ("beta-normalize/Bool/!=", ("!=", ("BoolLit", m.l), ("BoolLit", m.r)), m(builtins["!="], m.l, m.r, m.o), ("BoolLit", m.o))
, ("beta-normalize/Bool/!=/R-identity", ("!=", m.l, m._("BoolLit", "False")), m.l)
, ("beta-normalize/Bool/!=/idempotence", ("!=", m.e, m.e), m.e)
, ("beta-normalize/Natural/build", ("Application", "Natural/build", m.g),
m("identity", ("Lambda", "x", "Natural", ("+", ("Variable", "x", "0"), ("NaturalLit", "1"))), m.succ),
m("identity", ("NaturalLit", "0"), m.zero),
m("beta-normalize",
("Application", m.g, "Natural", m.succ, m.zero),
m.b
),
m.b
)
, ("beta-normalize/Natural/fold", ("Application", "Natural/fold", ("NaturalLit", m.n), m.B, m.g, m.b),
m("fold-natural", m.n, m.b, m[m.r0, ("Application", m.g, m.r0)], m.r),
m.r
)
, ("beta-normalize/Natural/*/L-absorb", ("*", m.l("NaturalLit", "0"), m._), m.l)
, ("beta-normalize/Natural/*/L-identity", ("*", m._("NaturalLit", "1"), m.r), m.r)
, ("beta-normalize/Natural/*", ("*", ("NaturalLit", m.l), ("NaturalLit", m.r)), m(builtins["*"], m.l, m.r, m.o), ("NaturalLit", m.o))
, ("beta-normalize/Natural/*/R-absorb", ("*", m.r("NaturalLit", "0"), m._), m.r)
, ("beta-normalize/Natural/*/R-identity", ("*", m.l, m._("NaturalLit", "1")), m.l)
, ("beta-normalize/Natural/+/L-identity", ("+", m._("NaturalLit", "0"), m.r), m.r)
, ("beta-normalize/Natural/+", ("+", ("NaturalLit", m.l), ("NaturalLit", m.r)), m(builtins["+"], m.l, m.r, m.o), ("NaturalLit", m.o))
, ("beta-normalize/Natural/+/R-identity", ("+", m.l, m._("NaturalLit", "0")), m.l)
, ("beta-normalize/Natural/isZero", ("Application", "Natural/isZero", ("NaturalLit", m.n)), m(builtins["Natural/isZero"], m.n, m.o), ("BoolLit", m.o))
, ("beta-normalize/Natural/even", ("Application", "Natural/even", ("NaturalLit", m.n)), m(builtins["Natural/even"], m.n, m.o), ("BoolLit", m.o))
, ("beta-normalize/Natural/odd", ("Application", "Natural/odd", ("NaturalLit", m.n)), m(builtins["Natural/odd"], m.n, m.o), ("BoolLit", m.o))
, ("beta-normalize/Natural/toInteger", ("Application", "Natural/toInteger", ("NaturalLit", m.n)), m(builtins["Natural/toInteger"], m.n, m.o), ("IntegerLit", m.o))
, ("beta-normalize/Natural/show", ("Application", "Natural/show", ("NaturalLit", m.n)), m(builtins["Natural/show"], m.n, m.o), ("TextLit", m.o))
, ("beta-normalize/Natural/subtract/L-zero", ("Application", "Natural/subtract", ("NaturalLit", "0"), m.n), m.n)
, ("beta-normalize/Natural/subtract/R-zero", ("Application", "Natural/subtract", m._, m.l("NaturalLit", "0")), m.l)
, ("beta-normalize/Natural/subtract/equal", ("Application", "Natural/subtract", m.n, m.n), ("NaturalLit", "0"))
, ("beta-normalize/Natural/subtract", ("Application", "Natural/subtract", ("NaturalLit", m.m), ("NaturalLit", m.n)), m(builtins["Natural/subtract"], m.m, m.n, m.o), ("NaturalLit", m.o))
, ("beta-normalize/List/build", ("Application", "List/build", m.A0, m.g),
m("shift", "1", "a", "0", m.A0, m.A1),
m("identity", ("Lambda", "a", m.A0, ("Lambda", "as", ("Application", "List", m.A1), ("#", ("ListLit", (("Variable", "a", "0"),), "None"), ("Variable", "as", "0")))), m.succ),
m("identity", ("ListLit", (), ("Some", ("Application", "List", m.A0))), m.zero),
m("beta-normalize",
("Application", m.g, ("Application", "List", m.A0), m.succ, m.zero),
m.b
),
m.b
)
, ("beta-normalize/List/fold", ("Application", "List/fold", m.A0, ("ListLit", m.l, m._), m.B, m.g, m.b),
m("fold-list", m.l, m.b, m[m.a0, m.r0, ("Application", m.g, m.a0, m.r0)], m.r),
m.r
)
, ("beta-normalize/List/#/L-identity", ("#", ("ListLit", (), m._), m.r), m.r)
, ("beta-normalize/List/#/R-identity", ("#", m.l, ("ListLit", (), m._)), m.l)
, ("beta-normalize/List/#", ("#", ("ListLit", m.ls, "None"), ("ListLit", m.rs, "None")),
m(builtins["List/#"], m.ls, m.rs, m.lrs),
("ListLit", m.lrs, ())
)
, """builtins…"""
, ("beta-normalize/Record/Field", ("Field", ("RecordLit", m.kvs), m.k),
m("find", m.kvs, m.k, m.v),
m.v
)
, ("beta-normalize/Record/Field/Project", ("Field", ("Project", m.rec, m.ks), m.k),
("Field", m.rec, m.k)
)
, ("beta-normalize/Record/Field/Prefer/L-yes", ("Field", ("Prefer", ("RecordLit", m.kvs), m.r), m.k),
m("find", m.kvs, m.k, m.v),
m.v
)
, ("beta-normalize/Record/Field/Prefer/L-no", ("Field", ("Prefer", ("RecordLit", m.kvs), m.r), m.k),
#m("not-found", m.kvs, m.k, ()),
("Field", m.r, m.k)
)
, ("beta-normalize/Record/Field/Prefer/R-yes", ("Field", ("Prefer", m.l, ("RecordLit", m.kvs)), m.k),
m("find", m.kvs, m.k, m.v),
m.v
)
, ("beta-normalize/Record/Field/Prefer/R-no", ("Field", ("Prefer", m.l, ("RecordLit", m.kvs)), m.k),
#m("not-found", m.kvs, m.k, ()),
("Field", m.l, m.k)
)
, ("beta-normalize/Record/Field/Combine/L-yes", ("Field", ("Combine", ("RecordLit", m.kvs), m.r), m.k),
m("find", m.kvs, m.k, m.v),
("Field", ("Combine", ("RecordLit", ((m.k, m.v),)), m.r), m.k)
)
, ("beta-normalize/Record/Field/Combine/L-no", ("Field", ("Combine", ("RecordLit", m.kvs), m.r), m.k),
#m("not-found", m.kvs, m.k, ()),
("Field", m.r, m.k)
)
, ("beta-normalize/Record/Field/Combine/R-yes", ("Field", ("Combine", m.l, ("RecordLit", m.kvs)), m.k),
m("find", m.kvs, m.k, m.v),
("Field", ("Combine", m.l, ("RecordLit", ((m.k, m.v),))), m.k)
)
, ("beta-normalize/Record/Field/Combine/R-no", ("Field", ("Combine", m.l, ("RecordLit", m.kvs)), m.k),
#m("not-found", m.kvs, m.k, ()),
("Field", m.l, m.k)
)
, ("beta-normalize/Record/Project/empty", ("Project", m.rec, ("ByLabels", ())),
("RecordLit", ())
)
, ("beta-normalize/Record/Project", ("Project", ("RecordLit", m.kvs0), ("ByLabels", m.ks)),
# TODO
m("select", m.kvs0, m.ks, m.kvs1),
("RecordLit", m.kvs1)
)
, ("beta-normalize/Record/Project/Project", ("Project", ("Project", m.rec, m._), ("ByLabels", m.ks)),
("Project", m.rec, ("ByLabels", m.ks))
)
, ("beta-normalize/Record/Project/Prefer", ("Project", ("Prefer", m.l, ("RecordLit", m.kvs)), ("ByLabels", m.ks)),
# TODO
m("separate", m.kvs, m.ks, m.lks, m.rks),
("Prefer", ("Project", m.l, ("ByFields", m.lks)), ("Project", m.r, ("ByFields", m.rks)))
)
, ("beta-normalize/Record/Project/Record", ("Project", m.rec, ("ByType", ("RecordType", m.kvs))),
m("void", m.kvs, m.ks),
("Project", m.rec, ("ByFields", m.ks))
)
, """TODO"""
, ("beta-normalize/Application", ("Application", ("Lambda", m.v, m._, m.b), m.a),
m("shift-substitute-shift", m.v, m.a, m.b, m.r),
m.r
)
, ("beta-normalize/Let", ("Let", m.v, m._, m.a, m.b),
m("shift-substitute-shift", m.v, m.a, m.b, m.r),
m.r
)
, ("beta-normalize/Annotation", ("Annotation", m.v, m._), m.v)
, (("eta-normalize", "eta"), ("match:judgmental-equality",), "Expr", "Expr")
, ("eta-normalize/",
("Lambda", m.v, m.t, ("Application", m.f, ("Variable", m.v, "0"))),
m("constant", m.v, m.f, m.o),
m.o
)
, (("typecheck", "type"), ("match:judgmental-equality",), ("Context", "Expr"), "Expr", "Expr")
, ("typecheck/Variable",
m.ctx,
("Variable", m.x, m.n),
m("find-ctx", m.ctx, m.x, m.n, m.T),
m.T
)
, ("typecheck/Bool", m.ctx, "Bool", "Type")
, ("typecheck/BoolLit", m.ctx, ("BoolLit", m._), "Bool")
, ("typecheck/if_then_else_", m.ctx, ("if_then_else_", m.b, m.l, m.r),
m("typecheck", m.ctx, m.b, "Bool"),
m("typecheck", m.ctx, m.l, m.T),
m("typecheck", m.ctx, m.r, m.T),
m.T
)
, ("typecheck/||", m.ctx, ("||", m.l, m.r),
m("typecheck", m.ctx, m.l, "Bool"),
m("typecheck", m.ctx, m.r, "Bool"),
"Bool"
)
, ("typecheck/&&", m.ctx, ("&&", m.l, m.r),
m("typecheck", m.ctx, m.l, "Bool"),
m("typecheck", m.ctx, m.r, "Bool"),
"Bool"
)
, ("typecheck/==", m.ctx, ("==", m.l, m.r),
m("typecheck", m.ctx, m.l, "Bool"),
m("typecheck", m.ctx, m.r, "Bool"),
"Bool"
)
, ("typecheck/!=", m.ctx, ("!=", m.l, m.r),
m("typecheck", m.ctx, m.l, "Bool"),
m("typecheck", m.ctx, m.r, "Bool"),
"Bool"
)
, ("typecheck/Natural", m.ctx, "Natural", "Type")
, ("typecheck/NaturalLit", m.ctx, ("NaturalLit", m._), "Natural")
, ("typecheck/+", m.ctx, ("+", m.l, m.r),
m("typecheck", m.ctx, m.l, "Natural"),
m("typecheck", m.ctx, m.r, "Natural"),
"Natural"
)
, ("typecheck/*", m.ctx, ("*", m.l, m.r),
m("typecheck", m.ctx, m.l, "Natural"),
m("typecheck", m.ctx, m.r, "Natural"),
"Natural"
)
, ("typecheck/Natural/build", m.ctx, "Natural/build",
("Forall", "_",
("Forall", "natural", "Type",
("Forall", "succ", ("Forall", "_", ("Variable", "natural", "0"), ("Variable", "natural", "0")),
("Forall", "zero", ("Variable", "natural", "0"),
("Variable", "natural", "0")
))),
"Natural"
)
)
, ("typecheck/Natural/fold", m.ctx, "Natural/fold",
("Forall", "_",
"Natural",
("Forall", "natural", "Type",
("Forall", "succ", ("Forall", "_", ("Variable", "natural", "0"), ("Variable", "natural", "0")),
("Forall", "zero", ("Variable", "natural", "0"),
("Variable", "natural", "0")
)))
)
)
, ("typecheck/Natural/isZero", m.ctx, "Natural/isZero",
("Forall", "_", "Natural", "Bool")
)
, ("typecheck/Natural/even", m.ctx, "Natural/even",
("Forall", "_", "Natural", "Bool")
)
, ("typecheck/Natural/odd", m.ctx, "Natural/odd",
("Forall", "_", "Natural", "Bool")
)
, ("typecheck/Natural/toInteger", m.ctx, "Natural/toInteger",
("Forall", "_", "Natural", "Integer")
)
, ("typecheck/Natural/show", m.ctx, "Natural/show",
("Forall", "_", "Natural", "Text")
)
, ("typecheck/Natural/subtract", m.ctx, "Natural/subtract",
("Forall", "_", "Natural", ("Forall", "_", "Natural", "Natural"))
)
, ("typecheck/Text", m.ctx, "Text", "Type")
, ("typecheck/TextLiteral", m.ctx, ("TextLiteral", m.txt),
m("traverse_", m[m.t, m("typecheck", m.ctx, m.t, "Text"), ()], m.txt, ()),
"Text"
)
, ("typecheck/Text/show", m.ctx, "Text/show",
("Forall", "_", "Text", "Text")
)
, ("typecheck/Text/replace", m.ctx, "Text/replace",
("Forall", "needle", "Text",
("Forall", "replacement", "Text",
("Forall", "haystack", "Text",
"Text")))
)
, ("typecheck/Text/++", m.ctx, ("++", m.l, m.r),
m("typecheck", m.ctx, m.l, "Text"),
m("typecheck", m.ctx, m.r, "Text"),
"Text",
)
, ("typecheck/Date", m.ctx, "Date", "Type")
, ("typecheck/Time", m.ctx, "Time", "Type")
, ("typecheck/TimeZone", m.ctx, "TimeZone", "Type")
, ("typecheck/Date", m.ctx, ("DateLiteral", m._), "Date")
, ("typecheck/Time", m.ctx, ("TimeLiteral", m._), "Time")
, ("typecheck/TimeZone", m.ctx, ("TimeZoneLiteral", m._), "TimeZone")
, ("typecheck/List", m.ctx, "List", ("Forall", "_", "Type", "Type"))
, ("typecheck/List/#", m.ctx, ("#", m.l, m.r),
m("typecheck", m.ctx, m.l, ("Application", "List", m.T)),
m("typecheck", m.ctx, m.r, ("Application", "List", m.T)),
("Application", "List", m.T)
)
, ("typecheck/RecordLit",
m.ctx,
("RecordLit", m.kvs),
m("ensureNodupes", m.kvs, ()),
m("traverse", m.typecheck, m.kvs, m.kts),
m.kts
)
, ("typecheck/Field",
m.ctx,
("Field", m.expr, m.field),
m("typecheck", m.expr, m.ty),
m(m
[("Record", m.kts), m("find", m.kts, m.field, m.fieldType), m.fieldType]
[("Const", m.c), m(m
[("Union", m.kts),
m("find", m.kts, m.field, m.mt),
m(m
[("Some", m.ty),
m("shift", m.field, "1", m.expr, m.result),
("Pi", m.field, m.ty, m.result)
]
["None", m.expr],
m.mt,
m.fieldType
),
m.fieldType
],
m.expr,
m.fieldType,
), m.fieldType],
m.ty,
m.fieldType
),
m.fieldType
)
, ("typecheck/Integer", m.ctx, "Integer", "Type")
, ("typecheck/IntegerLit", m.ctx, ("IntegerLit", m._), "Integer")
, ("typecheck/Integer/show", m.ctx, "Integer/show",
("Forall", "_", "Integer", "Text")
)
, ("typecheck/Integer/toDouble", m.ctx, "Integer/toDouble",
("Forall", "_", "Integer", "Double")
)
, ("typecheck/Integer/negate", m.ctx, "Integer/negate",
("Forall", "_", "Integer", "Integer")
)
, ("typecheck/Integer/clamp", m.ctx, "Integer/clamp",
("Forall", "_", "Integer", "Natural")
)
, ("typecheck/Double", m.ctx, "Double", "Type")
, ("typecheck/DoubleLit", m.ctx, ("DoubleLit", m._), "Double")
, ("typecheck/Double/show", m.ctx, "Double/show",
("Forall", "_", "Double", "Text")
)
, ("typecheck/Forall", m.ctx,
("Forall", m.x, m.A, m.B),
m("typecheck", m.ctx, m.A, ("Const", m.i)),
m("add-ctx", m.x, m.A, m.ctx, m.ctx1),
m("typecheck", m.ctx1, m.B, ("Const", m.o)),
m("imax", m.i, m.o, m.c),
("Const", m.c)
)
, ("typecheck/Lambda", m.ctx,
("Lambda", m.x, m.A, m.b),
m("typecheck", m.ctx, m.A, ("Const", m._)),
m("add-ctx", m.x, m.A, m.ctx, m.ctx1),
m("typecheck", m.ctx1, m.b, m.B),
("Forall", m.x, m.A, m.B)
)
, ("typecheck/Application", m.ctx,
("Application", m.f, m.a),
m("typecheck", m.ctx, m.f, ("Forall", m.x, m.A, m.B)),
m("typecheck", m.ctx, m.a, m.A),
("Application", ("Lambda", m.x, m.A, m.B), m.a),
)
, ("typecheck/Let", m.ctx,
("Let", m.x, m.mA, m.a, m.b),
m("typecheck", m.ctx, m.a, m.A),
m("traverse_", m[m.A, ()], m.mA, ()),
m("shift-substitute-shift", m.x, m.a, m.b, m.b1),
m("typecheck", m.ctx, m.b1, m.B),
m.B
)
, ("typecheck/Annot", m.ctx, ("Annot", m.a, m.A),
m("typecheck", m.ctx, m.a, m.A),
m.A
)
, ("typecheck/Assert", m.ctx, ("Assert", m.T),
m("typecheck", m.ctx, m.T, "Type"),
m("beta-normalize", m.T, ("Equivalent", m.x, m.x)), ("Equivalent", m.x, m.x)
)
, ("typecheck/Equivalent", m.ctx, ("Equivalent", m.x, m.y),
m("typecheck", m.ctx, m.x, m.A),
m("typecheck", m.ctx, m.y, m.A),
m("typecheck", m.ctx, m.A, "Type"),
"Type",
)
, Description.Laws
)
# Basic codegen for JS, including pattern matching and stuff
def genJS(d):
import json
r = ""
def mangle(name):
return name.replace("-", "_")
r += "const matchError = new Error(\"Match failure\");\n"
r += "const check = (c) => {if (!c) {throw matchError;}};\n"
r += "function $or(...fns) {\n"
r += " return function(...args) {\n"
r += " for (let fn of fns) {\n"
r += " try {\n"
r += " return fn(...args);\n"
r += " } catch(e) {\n"
r += " if (e !== matchError) throw e;\n"
r += " }\n"
r += " }\n"
r += " throw matchError;\n"
r += " }\n"
r += "}\n"
r += "function are_eq(a, b) {\n"
r += " if (a === b) return true;\n"
r += " if (typeof a !== typeof b) return false;\n"
r += " return (({\n"
r += " 'array': function() {\n"
r += " if (a.length !== b.length) return false;\n"
r += " return a.every((x, i) => are_eq(x, b[i]));\n"
r += " },\n"
r += " 'object': function() {\n"
r += " var ks = Object.keys(a);\n"
r += " if (!are_eq(ks, Object.keys(b))) return false;\n"
r += " return ks.every(k => are_eq(a[k], b[k]));\n"
r += " },\n"
r += " })[typeof a] || (() => false))();\n"
r += "}\n"
r += "function eq(a, b) {\n"
r += " if (are_eq(a,b)) {\n"
r += " return a;\n"
r += " } else {\n"
r += " throw matchError;\n"
r += " }\n"
r += "}\n"
r += "function identity(a) {\n"
r += " return a;\n"
r += "}\n"
def genFn(fn):
if len(fn.cases) == 1:
return "("+genCase(fn.cases[0])+")"
return "$or(\n" + ",\n".join(genCase(case) for case in fn.cases) + "\n)"
def genCase(case):
inputs = {"$i"+str(k):v for k,v in enumerate(case.inputs)}
r2 = "function ("+", ".join(inputs)+") {\n"
for k,i in inputs.items():
r2 += genInput(k, i)
for k,i in enumerate(case.stmts):
r2 += genStatement(k, i)
r2 += "return " + genOutput(case.output) + ";\n"
r2 += "}"
return r2
def check(cond):
return "if(!("+cond+")) {throw matchError;}\n"
def genInput(var, m):
if m is None:
return ""
if isinstance(m, str):
return check(f"{var} === {json.dumps(m)}")
if isinstance(m, tuple):
r2 = ""
r2 += check(f"{var}.length === {str(len(m))}")
for i,v in enumerate(m):
r2 += genInput(var+f"[{str(i)}]", v)
return r2
if isinstance(m, Matcher):
r2 = genInput(var, m.value)
if m.name is not None and m.name != ():
r2 += "const " + "$".join(m.name) + " = " + var + ";\n"
return r2
raise ValueError(f"Unhandled input matcher? {m!r}")
def genOutput(m):
if isinstance(m, str):
return json.dumps(m)
if isinstance(m, tuple):
return "[" + ", ".join(genOutput(o) for o in m) + "]"
if isinstance(m, Matcher.Lambda):
return genFn(m)
if not isinstance(m, Matcher):
raise TypeError(f"Not a valid output? {m!r}")
if m.name is not None and m.name != ():
if m.value is not None:
raise ValueError(f"Cannot have both name and value as output {m!r}")
return "$".join(m.name)
if m.value is None:
raise ValueError(f"Empty output match? {m!r}")
return genOutput(m.value)
def genStatement(i, m):
r2 = "const $s"+str(i) + " = "
if isinstance(m.fn, str):
r2 += mangle(m.fn)
elif isinstance(m.fn, Builtin):
r2 += "builtins["+json.dumps(m.fn.key)+"]"
else:
r2 += genFn(m.fn)
if len(m.inputs):
r2 += "("
r2 += ", ".join(genOutput(v) for v in m.inputs)
r2 += ")"
r2 += ";\n"
r2 += genInput("$s"+str(i), m.output)
return r2
for name in d.funcs:
r += "function " + mangle(name) + "(...$args) {\n"
r += " return " + genFn(d.funcs[name].spec) + "(...$args);\n"
r += "}\n"
try:
import jsbeautifier
return jsbeautifier.beautify(r)+"\n"
except Exception:
return r
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment