HERMIT to HERMIT Shell

Symbols

	Meaning
🎤	implemented in server
🔈	implemented in client
↔️	tested by hand, front to back, implies 🎤 & 🔈
✅	In a unit test. The test may or may not run

Types

HERMIT Type	HERMIT-shell Type	Notes
RhsOfName	Name
TransformH :: * -> * -> *	Transform
LCoreTC
LocalPathH	LocalPath
RewriteH	Rewrite

All shell functions

HERMIT.Dictionary.AlphaConversion

Name	Type	Done
alpha	RewriteH LCore	🎤 🔈
alpha-lam	String -> RewriteH LCore
alpha-lam	RewriteH LCore
alpha-case-binder	String -> RewriteH LCore
alpha-case-binder	RewriteH LCore
alpha-alt	RewriteH LCore
alpha-alt	[String] -> RewriteH LCore
alpha-case	RewriteH LCore	🎤 🔈
alpha-let	[String] -> RewriteH LCore
alpha-let	RewriteH LCore
alpha-top	[String] -> RewriteH LCore
alpha-top	RewriteH LCore
alpha-prog	RewriteH LCore	🎤 🔈
unshadow	RewriteH LCore	🎤 🔈

HERMIT.Dictionary.Composite

Name	Type	Done
unfold-basic-combinator	RewriteH LCore	🎤 🔈
simplify	RewriteH LCore	🎤 🔈
bash	RewriteH LCore	🎤 🔈
smash	RewriteH LCore	🎤 🔈
bash-extended-with	[RewriteH LCore] -> RewriteH LCore
smash-extended-with	[RewriteH LCore] -> RewriteH LCore
bash-debug	RewriteH LCore	🎤 🔈

HERMIT.Dictionary.Debug

Name	Type	Done
trace	String -> RewriteH LCoreTC	🎤 🔈
observe	String -> RewriteH LCoreTC	🎤 🔈
observe-failure	String -> RewriteH LCoreTC -> RewriteH LCoreTC	🎤 🔈
bracket	String -> RewriteH LCoreTC -> RewriteH LCoreTC	🎤 🔈

HERMIT.Dictionary.FixPoint

Name	Type	Done
fix-intro	RewriteH LCore	🎤 🔈
fix-computation-rule	BiRewriteH LCore	🎤 🔈
fix-rolling-rule	BiRewriteH LCore	🎤 🔈
fix-fusion-rule	String -> String -> String -> RewriteH LCore -> RewriteH LCore -> RewriteH LCore -> BiRewriteH LCore	🎤 🔈
fix-fusion-rule-unsafe	String -> String -> String -> RewriteH LCore -> BiRewriteH LCore
fix-fusion-rule-unsafe	String -> String -> String -> BiRewriteH LCore

HERMIT.Dictionary.Fold

Name	Type	Done
fold	HermitName -> RewriteH LCore	🎤 🔈

HERMIT.Dictionary.Function

Name	Type	Done
static-arg	RewriteH LCore
static-arg-types	RewriteH LCore
static-arg-pos	[Int] -> RewriteH LCore

HERMIT.Dictionary.GHC

Name	Type	Done
deshadow-prog	RewriteH LCore
dezombify	RewriteH LCore
occurrence-analysis	RewriteH LCore
lint-expr	TransformH LCoreTC String
lint-module	TransformH LCoreTC String
lint	TransformH LCoreTC String
load-lemma-library	HermitName -> TransformH LCore String
load-lemma-library	HermitName -> LemmaName -> TransformH LCore String
inject-dependency	String -> TransformH LCore ()

HERMIT.Dictionary.Induction

Name	Type	Done
induction	HermitName -> RewriteH LCore
prove-by-cases	HermitName -> RewriteH LCore

HERMIT.Dictionary.Inline

Name	Type	Done
inline	RewriteH LCore
inline	OccurrenceName -> RewriteH LCore
inline	[String] -> RewriteH LCore
inline-case-scrutinee	RewriteH LCore
inline-case-alternative	RewriteH LCore

HERMIT.Dictionary.Kure

Name	Type	Done
id	RewriteH LCore
id	RewriteH LCoreTC
success	TransformH LCore ()
fail	String -> RewriteH LCore
<+	RewriteH LCore -> RewriteH LCore -> RewriteH LCore
<+	TransformH LCore () -> TransformH LCore () -> TransformH LCore ()
>>>	RewriteH LCore -> RewriteH LCore -> RewriteH LCore
>>>	BiRewriteH LCore -> BiRewriteH LCore -> BiRewriteH LCore
>>>	RewriteH LCoreTC -> RewriteH LCoreTC -> RewriteH LCoreTC
>+>	RewriteH LCore -> RewriteH LCore -> RewriteH LCore
try	RewriteH LCore -> RewriteH LCore
repeat	RewriteH LCore -> RewriteH LCore
replicate	Int -> RewriteH LCore -> RewriteH LCore
all	RewriteH LCore -> RewriteH LCore
any	RewriteH LCore -> RewriteH LCore
one	RewriteH LCore -> RewriteH LCore
all-bu	RewriteH LCore -> RewriteH LCore
all-td	RewriteH LCore -> RewriteH LCore
all-du	RewriteH LCore -> RewriteH LCore
any-bu	RewriteH LCore -> RewriteH LCore
any-td	RewriteH LCore -> RewriteH LCore
any-du	RewriteH LCore -> RewriteH LCore
one-td	RewriteH LCore -> RewriteH LCore
one-bu	RewriteH LCore -> RewriteH LCore
prune-td	RewriteH LCore -> RewriteH LCore
innermost	RewriteH LCore -> RewriteH LCore
focus	TransformH LCoreTC LocalPathH -> RewriteH LCoreTC -> RewriteH LCoreTC
focus	TransformH LCoreTC LocalPathH -> TransformH LCoreTC String -> TransformH LCoreTC String
focus	LocalPathH -> RewriteH LCoreTC -> RewriteH LCoreTC
focus	LocalPathH -> TransformH LCoreTC String -> TransformH LCoreTC String
focus	TransformH LCore LocalPathH -> RewriteH LCore -> RewriteH LCore
focus	TransformH LCore LocalPathH -> TransformH LCore String -> TransformH LCore String
focus	LocalPathH -> RewriteH LCore -> RewriteH LCore
focus	LocalPathH -> TransformH LCore String -> TransformH LCore String
when	TransformH LCore () -> RewriteH LCore -> RewriteH LCore
not	TransformH LCore () -> TransformH LCore ()
invert	BiRewriteH LCore -> BiRewriteH LCore
forward	BiRewriteH LCore -> RewriteH LCore
backward	BiRewriteH LCore -> RewriteH LCore
test	RewriteH LCore -> TransformH LCore String
any-call	RewriteH LCore -> RewriteH LCore
promote	RewriteH LCore -> RewriteH LCoreTC
extract	RewriteH LCoreTC -> RewriteH LCore
extract	TransformH LCoreTC String -> TransformH LCore String
between	Int -> Int -> RewriteH LCoreTC -> RewriteH LCoreTC
atPath	TransformH LCore LocalPathH -> TransformH LCore LCore
atPath	TransformH LCoreTC LocalPathH -> TransformH LCoreTC LCoreTC
atPath	TransformH LCoreTC LocalPathH -> TransformH LCore LCore

HERMIT.Dictionary.Local.Bind

Name	Type	Done
nonrec-to-rec	RewriteH LCore
rec-to-nonrec	RewriteH LCore

HERMIT.Dictionary.Local.Case

Name	Type	Done
case-float-app	RewriteH LCore
case-float-arg	RewriteH LCore -> RewriteH LCore
case-float-arg	CoreString -> RewriteH LCore -> RewriteH LCore
case-float-arg-unsafe	CoreString -> RewriteH LCore
case-float-arg-unsafe	LemmaName -> RewriteH LCore
case-float-arg-lemma	LemmaName -> RewriteH LCore
case-float-case	RewriteH LCore
case-float-cast	RewriteH LCore
case-float-let	RewriteH LCore
case-float	RewriteH LCore
case-float-in	RewriteH LCore
case-float-in-args	RewriteH LCore
case-float-in-app	RewriteH LCore
case-reduce	RewriteH LCore
case-reduce-datacon	RewriteH LCore
case-reduce-literal	RewriteH LCore
case-reduce-unfold	RewriteH LCore
case-split	OccurrenceName -> RewriteH LCore
case-split	CoreString -> RewriteH LCore
case-split-inline	OccurrenceName -> RewriteH LCore
case-split-inline	CoreString -> RewriteH LCore
case-intro-seq	String -> RewriteH LCore
case-elim-seq	RewriteH LCore
case-inline-alternative	RewriteH LCore
case-inline-scrutinee	RewriteH LCore
case-merge-alts	RewriteH LCore
case-merge-alts-with-binder	RewriteH LCore
case-elim	RewriteH LCore
case-elim-inline-scrutinee	RewriteH LCore
case-elim-merge-alts	RewriteH LCore
case-fold-binder	RewriteH LCore
cast-elim	RewriteH LCore
cast-elim-refl	RewriteH LCore
cast-elim-sym	RewriteH LCore
cast-elim-sym-plus	RewriteH LCore
cast-float-app	RewriteH LCore
cast-float-lam	RewriteH LCore
cast-elim-unsafe	RewriteH LCore

HERMIT.Dictionary.Local.Let

Name	Type	Done
let-subst	RewriteH LCore
let-subst-safe	RewriteH LCore
let-nonrec-subst-safe	RewriteH LCore
safe-let-subst-plus	RewriteH LCore
let-intro	String -> RewriteH LCore
let-intro-unfolding	HermitName -> RewriteH LCore
let-elim	RewriteH LCore
let-constructor-reuse	RewriteH LCore
let-float-app	RewriteH LCore
let-float-arg	RewriteH LCore
let-float-lam	RewriteH LCore
let-float-let	RewriteH LCore
let-float-case	RewriteH LCore
let-float-case-alt	RewriteH LCore
let-float-case-alt	Int -> RewriteH LCore
let-float-cast	RewriteH LCore
let-float-top	RewriteH LCore
let-float	RewriteH LCore
let-to-case	RewriteH LCore
let-to-case-unbox	RewriteH LCore
let-float-in	RewriteH LCore
let-float-in-app	RewriteH LCore
let-float-in-case	RewriteH LCore
let-float-in-lam	RewriteH LCore
reorder-lets	[String] -> RewriteH LCore
let-tuple	String -> RewriteH LCore
prog-bind-elim	RewriteH LCore
prog-bind-nonrec-elim	RewriteH LCore
prog-bind-rec-elim	RewriteH LCore

HERMIT.Dictionary.Local

Name	Type	Done
beta-reduce	RewriteH LCore
beta-expand	RewriteH LCore
eta-reduce	RewriteH LCore
eta-expand	String -> RewriteH LCore
flatten-module	RewriteH LCore
flatten-program	RewriteH LCore
abstract	OccurrenceName -> RewriteH LCore
push	String -> RewriteH LCore -> RewriteH LCore
push-unsafe	String -> RewriteH LCore

HERMIT.Dictionary.Navigation/Crumbs

Name	Type	Done
prog
prog-head
prog-tail
nonrec-rhs
rec-def
def-rhs
app-fun
app-arg
lam-body
let-bind
let-body
case-expr
case-type
case-alt
cast-expr
cast-co
tick-expr
alt-rhs
type
coercion
appTy-fun
appTy-arg
tyCon-arg
fun-dom
fun-cod
forall-body
refl-type
coCon-arg
appCo-fun
appCo-arg
coForall-body
axiom-inst
unsafe-left
unsafe-right
sym-co
trans-left
trans-right
nth-co
inst-co
inst-type
lr-co
forall-body
conj-lhs
conj-rhs
disj-lhs
disj-rhs
antecedent
consequent
eq-lhs
eq-rhs

HERMIT.Dictionary.Navigation

Name	Type	Done
rhs-of	RhsOfName -> TransformH LCoreTC LocalPathH
binding-group-of	String -> TransformH LCoreTC LocalPathH
binding-of	BindingName -> TransformH LCoreTC LocalPathH	✅
occurrence-of	OccurrenceName -> TransformH LCoreTC LocalPathH
application-of	OccurrenceName -> TransformH LCoreTC LocalPathH
consider	Considerable -> TransformH LCore LocalPathH
arg	Int -> TransformH LCore LocalPathH
lams-body	TransformH LCore LocalPathH
lets-body	TransformH LCore LocalPathH
prog-end	TransformH LCore LocalPathH
parent-of	TransformH LCore LocalPathH -> TransformH LCore LocalPathH
parent-of	TransformH LCoreTC LocalPathH -> TransformH LCoreTC LocalPathH

HERMIT.Dictionary.New

Name	Type	Done
var	String -> TransformH LCore ()
nonrec-intro	String -> CoreString -> RewriteH LCore

HERMIT.Dictionary.Query

Name	Type	Done
info	TransformH LCoreTC String
compare-bound-ids	HermitName -> HermitName -> TransformH LCoreTC ()
compare-core-at	TransformH LCoreTC LocalPathH -> TransformH LCoreTC LocalPathH -> TransformH LCoreTC ()

HERMIT.Dictionary.Reasoning

Name	Type	Done
retraction	CoreString -> CoreString -> RewriteH LCore -> BiRewriteH LCore
retraction-unsafe	CoreString -> CoreString -> BiRewriteH LCore
unshadow-quantified	RewriteH LCoreTC
merge-quantifiers	RewriteH LCore
float-left	RewriteH LCore
float-right	RewriteH LCore
conjunct	TransformH LCore ()
disjunct	TransformH LCore ()
imply	TransformH LCore ()
lemma-birewrite	LemmaName -> BiRewriteH LCore
lemma-forward	LemmaName -> RewriteH LCore
lemma-backward	LemmaName -> RewriteH LCore
lemma-consequent	LemmaName -> RewriteH LCore
lemma-consequent-birewrite	LemmaName -> BiRewriteH LCore
lemma-lhs-intro	LemmaName -> RewriteH LCore
lemma-rhs-intro	LemmaName -> RewriteH LCore
inst-lemma	TransformH LCore ()
inst-dictionaries	RewriteH LCore
abstract-forall	String -> CoreString -> RewriteH LCore
abstract-forall	String -> RewriteH LCore -> RewriteH LCore
copy-lemma	TransformH LCore ()
modify-lemma	LemmaName -> RewriteH LCore -> TransformH LCore ()
query-lemma	LemmaName -> TransformH LCore String -> TransformH LCore String
show-lemma	PrettyPrinter -> LemmaName -> PrettyH LCore
show-lemmas	PrettyPrinter -> LemmaName -> PrettyH LCore
show-lemmas	PrettyPrinter -> PrettyH LCore
extensionality	String -> RewriteH LCore
extensionality	RewriteH LCore
lhs	TransformH LCore String -> TransformH LCore String
lhs	RewriteH LCore -> RewriteH LCore
rhs	TransformH LCore String -> TransformH LCore String
rhs	RewriteH LCore -> RewriteH LCore
both	RewriteH LCore -> RewriteH LCore
both	TransformH LCore String -> TransformH LCore String
reflexivity	RewriteH LCore
simplify-proof	RewriteH LCore
split-antecedent	RewriteH LCore
lemma	LemmaName -> RewriteH LCore
lemma-unsafe	LemmaName -> RewriteH LCore

HERMIT.Dictionary.Remembered

Name	Type	Done
remember	LemmaName -> TransformH LCore ()
unfold-remembered	LemmaName -> RewriteH LCore
fold-remembered	LemmaName -> RewriteH LCore
fold-any-remembered	RewriteH LCore
show-remembered	PrettyPrinter -> PrettyH LCore

HERMIT.Dictionary.Rules

Name	Type	Done
show-rules	TransformH LCoreTC String
show-rule	PrettyPrinter -> RuleName -> TransformH LCoreTC DocH
fold-rule	RuleName -> RewriteH LCore
fold-rules	[RuleName] -> RewriteH LCore
unfold-rule	RuleName -> RewriteH LCore
unfold-rule-unsafe	RuleName -> RewriteH LCore
unfold-rules	[RuleName] -> RewriteH LCore
unfold-rules-unsafe	[RuleName] -> RewriteH LCore
rule-to-lemma	PrettyPrinter -> RuleName -> TransformH LCore DocH
spec-constr	RewriteH LCore
specialise	RewriteH LCore

HERMIT.Dictionary.Undefined

Name	Type	Done
replace-current-expr-with-undefined	RewriteH LCore
replace-id-with-undefined	HermitName -> RewriteH LCore
error-to-undefined	RewriteH LCore
is-undefined-val	TransformH LCore ()
undefined-expr	RewriteH LCore
undefined-app	RewriteH LCore
undefined-lam	RewriteH LCore
undefined-let	RewriteH LCore
undefined-case	RewriteH LCore
undefined-cast	RewriteH LCore
undefined-tick	RewriteH LCore

HERMIT.Dictionary.Unfold

Name	Type	Done
beta-reduce-plus	RewriteH LCore
unfold	RewriteH LCore
unfold	OccurrenceName -> RewriteH LCore
unfold	[OccurrenceName] -> RewriteH LCore
unfold-saturated	RewriteH LCore
specialize	RewriteH LCore
unsafe-replace	CoreString -> RewriteH LCore

HERMIT.Dictionary.WorkerWrapper/Common

Name	Type	Done
intro-ww-assumption-A
intro-ww-assumption-B
intro-ww-assumption-C
split-1-beta	CoreString -> RewriteH LCore
split-2-beta	CoreString -> RewriteH LCore

HERMIT.Dictionary.WorkerWrapper/Fix

Name	Type	Done
ww-factorisation-unsafe
ww-split-unsafe
ww-split-static-arg-unsafe
ww-assumption-B
ww-assumption-A-unsafe
ww-assumption-C-unsafe
ww-AssA-to-AssB	RewriteH LCore -> RewriteH LCore
ww-AssB-to-AssC	RewriteH LCore -> RewriteH LCore
ww-AssA-to-AssC	RewriteH LCore -> RewriteH LCore
ww-generate-fusion	RewriteH LCore -> TransformH LCore ()
ww-generate-fusion-unsafe	TransformH LCore ()
ww-fusion	BiRewriteH LCore

HERMIT.Dictionary.WorkerWrapper/FixResult

Name	Type	Done
ww-result-factorisation-unsafe
ww-result-split-unsafe
ww-result-split-static-arg-unsafe
ww-result-assumption-B
ww-result-assumption-A-unsafe
ww-result-assumption-C-unsafe
ww-result-AssA-to-AssB	RewriteH LCore -> RewriteH LCore
ww-result-AssB-to-AssC	RewriteH LCore -> RewriteH LCore
ww-result-AssA-to-AssC	RewriteH LCore -> RewriteH LCore
ww-result-generate-fusion	RewriteH LCore -> TransformH LCore ()
ww-result-generate-fusion-unsafe	TransformH LCore ()
ww-result-fusion	BiRewriteH LCore

HERMIT/PrettyPrinter/AST

Name	Type	Done
ast

HERMIT/PrettyPrinter/Clean

Name	Type	Done
clean

HERMIT/PrettyPrinter/GHC

Name	Type	Done
ghc

HERMIT/Shell/Dictionary

Name	Type	Done
help
help

HERMIT/Shell/Externals

Name	Type	Done
resume
abort
continue
gc
gc
display
up	KernelEffect	🎤 🔈
navigate
command-line
set-window	ShellEffect	🎤 🔈
top	KernelEffect	🎤 🔈
log	QueryFun	🎤 🔈
back	ShellEffect	🎤 🔈
step	ShellEffect	🎤 🔈
goto
goto
tag	String -> ShellEffect	🎤 🔈
diff	AST -> AST -> ShellEffect	🎤 🔈
set-pp-diffonly
set-fail-hard
set-auto-corelint
set-pp
set-pp-renderer
set-pp-renderer
dump
dump
dump-lemma	LemmaName -> FilePath -> PrettyPrinter -> String -> Int -> TransformH LCoreTC ()
dump-lemma	PrettyPrinter -> LemmaName -> FilePath -> String -> Int -> TransformH LCoreTC ()
set-pp-width
set-pp-type
set-pp-coercion
set-pp-uniques
{
}
load
load-and-run
save
save-verbose
save-script
load-as-rewrite
script-to-rewrite
define-script
define-rewrite
run-script
display-scripts
stop-script
possible-rewrites	CommandLineState -> TransformH LCore String

HERMIT/Shell/Proof

Name	Type	Done
prove-lemma
end-proof
end-case
assume