Skip to content

Commit

Permalink
reorganize grammar regarding sequences of proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@jsiek
jsiek committed Nov 18, 2024
1 parent 3ce8b17 commit 92a18a0
Show file tree
Hide file tree
Showing 4 changed files with 76 additions and 68 deletions.
67 changes: 36 additions & 31 deletions Deduce.lark
View file
Original file line number Diff line number Diff line change
Expand Up @@ -146,63 +146,68 @@ ident: IDENT -> ident
?proof_list: proof -> single
| proof "|" proof_list -> push

?proof: "conclude" term "by" proof -> annot
| "suffices" term "by" proof proof -> suffices
| "apply" proof "to" proof -> modus_ponens
?proof: tail_proof -> single_proof
| proof_stmt proof -> push_proof

?tail_proof: "conclude" term "by" proof -> annot
| proof "," proof -> tuple
| "apply" proof "to" proof -> modus_ponens
| "conjunct" INT "of" proof -> conjunct
| "suppose" IDENT proof -> imp_intro
| "suppose" IDENT ":" term proof -> imp_intro_explicit
| "suppose" ":" term proof -> imp_intro_anon
| "assume" IDENT proof -> imp_intro
| "assume" IDENT ":" term proof -> imp_intro_explicit
| "assume" ":" term proof -> imp_intro_anon
| "arbitrary" var_list proof -> all_intro
| "choose" term_list proof -> some_intro
| "obtain" ident_list "where" IDENT "from" proof proof -> some_elim
| "obtain" ident_list "where" IDENT ":" term "from" proof proof -> some_elim_explicit
| "cases" proof case_list -> cases
| "induction" type ind_case_list -> induction
| "definition" "{" ident_list "}" -> reason_definition
| "definition" ident -> reason_definition_one
| "rewrite" proof_list -> reason_rewrite
| "definition" "{" ident_list "}" "and" "rewrite" proof_list -> reason_def_rewrite
| "definition" ident "and" "rewrite" proof_list -> reason_def_one_rewrite
| "_definition" "{" ident_list "}" proof -> apply_defs_goal
| "_definition" ident proof -> apply_defs_goal_one
| "definition" "{" ident_list "}" "in" proof -> apply_defs_fact
| "definition" ident "in" proof -> apply_defs_fact_one
| "enable" "{" ident_list "}" proof -> enable_defs
| "enable" ident proof -> enable_def
| "_rewrite" proof_list proof -> rewrite_goal
| "rewrite" proof_list "in" proof -> rewrite_fact
| "evaluate" -> eval_goal
| "evaluate" "in" proof -> eval_fact
| "switch" term "{" switch_pf_case_list "}" -> switch_proof
| "switch" term "for" ident_list "{" switch_pf_case_list "}" -> switch_proof_for
| "equations" equation equation_list -> equations_proof
| "stop" "?" proof -> hole_in_middle_proof
| "recall" term_list -> recall_proof
| proof_hi

?proof_hi: IDENT -> proof_var
| "have" IDENT ":" term "by" proof proof -> let
| "have" ":" term "by" proof proof -> let_anon
| "define" IDENT "=" term proof -> define_term_proof
| "term" term "by" proof proof -> term_proof
| "." -> true_proof
| "reflexive" -> refl_proof
| "symmetric" proof -> sym_proof
| "transitive" proof proof -> trans_proof
| "injective" term proof -> injective_proof
| "extensionality" proof -> extensionality_proof
| "help" proof -> help_use_proof
| proof_hi

?proof_hi: IDENT -> proof_var
| "." -> true_proof
| "?" -> hole_proof
| "(" proof ")" -> paren
| proof_hi "[" term_list "]" -> all_elim
| proof_hi "<" type_list ">" -> all_elim_types
| "?" -> hole_proof
| "sorry" -> sorry_proof
| "help" proof -> help_use_proof
| "{" proof "}"

?proof_stmt:
| "suffices" term "by" proof -> suffices
| "suppose" IDENT -> imp_intro
| "suppose" IDENT ":" term -> imp_intro_explicit
| "suppose" ":" term -> imp_intro_anon
| "assume" IDENT -> imp_intro
| "assume" IDENT ":" term -> imp_intro_explicit
| "assume" ":" term -> imp_intro_anon
| "arbitrary" var_list -> all_intro
| "choose" term_list -> some_intro
| "obtain" ident_list "where" IDENT "from" proof -> some_elim
| "obtain" ident_list "where" IDENT ":" term "from" proof -> some_elim_explicit
| "_definition" "{" ident_list "}" -> apply_defs_goal
| "_definition" ident -> apply_defs_goal_one
| "enable" "{" ident_list "}" -> enable_defs
| "enable" ident -> enable_def
| "_rewrite" proof_list -> rewrite_goal
| "stop" "?" -> hole_in_middle_proof
| "have" IDENT ":" term "by" proof -> let
| "have" ":" term "by" proof -> let_anon
| "define" IDENT "=" term -> define_term_proof
| "term" term "by" proof -> term_proof
| "injective" term -> injective_proof
| "extensionality" -> extensionality_proof

?case: "case" IDENT "{" proof "}" -> case
| "case" IDENT ":" term "{" proof "}" -> case_annot
Expand Down
12 changes: 9 additions & 3 deletions abstract_syntax.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1701,6 +1701,12 @@ def uniquify(self, env):
body_env[x] = [new_x]
self.var = (new_x, new_t)
self.body.uniquify(body_env)

def set_body(self, new_body):
if self.body:
self.body.set_body(new_body)
else:
self.body = new_body

@dataclass
class AllElimTypes(Proof):
Expand Down Expand Up @@ -2052,16 +2058,16 @@ def uniquify(self, env):
@dataclass
class EnableDefs(Proof):
definitions: List[Term]
subject: Proof
body: Proof

def __str__(self):
return 'enable ' + ', '.join([str(d) for d in self.definitions]) \
+ ';\n' + str(self.subject)
+ ';\n' + str(self.body)

def uniquify(self, env):
for d in self.definitions:
d.uniquify(env)
self.subject.uniquify(env)
self.body.uniquify(env)

@dataclass
class Rewrite(Proof):
Expand Down
61 changes: 29 additions & 32 deletions parser.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -313,6 +313,16 @@ def parse_tree_to_ast(e, parent):
# proofs
if e.data == 'proof_var':
return PVar(e.meta, str(e.children[0].value))
elif e.data == 'single_proof':
return parse_tree_to_ast(e.children[0], e)
elif e.data == 'push_proof':
proof_stmt = parse_tree_to_ast(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
if isinstance(proof_stmt, AllIntro):
proof_stmt.set_body(body)
else:
proof_stmt.body = body
return proof_stmt
elif e.data == 'modus_ponens':
e1, e2 = e.children
return ModusPonens(e.meta, parse_tree_to_ast(e1, e),
Expand All @@ -337,33 +347,29 @@ def parse_tree_to_ast(e, parent):
eq2 = parse_tree_to_ast(e2, e)
return PTransitive(e.meta, eq1, eq2)
elif e.data == 'injective_proof':
e1, e2 = e.children
constr = parse_tree_to_ast(e1, e)
eq = parse_tree_to_ast(e2, e)
return PInjective(e.meta, constr, eq)
constr = parse_tree_to_ast(e.children[0], e)
return PInjective(e.meta, constr, None)
elif e.data == 'extensionality_proof':
e1 = e.children[0]
eq1 = parse_tree_to_ast(e1, e)
return PExtensionality(e.meta, eq1)
return PExtensionality(e.meta, None)
elif e.data == 'paren':
return parse_tree_to_ast(e.children[0], e)
elif e.data == 'let':
return PLet(e.meta,
str(e.children[0].value),
parse_tree_to_ast(e.children[1], e),
parse_tree_to_ast(e.children[2], e),
parse_tree_to_ast(e.children[3], e))
None)
elif e.data == 'let_anon':
return PLet(e.meta,
'_',
parse_tree_to_ast(e.children[0], e),
parse_tree_to_ast(e.children[1], e),
parse_tree_to_ast(e.children[2], e))
None)
elif e.data == 'define_term_proof':
return PTLetNew(e.meta,
str(e.children[0].value),
parse_tree_to_ast(e.children[1], e),
parse_tree_to_ast(e.children[2], e))
None)
elif e.data == 'annot':
return PAnnot(e.meta,
parse_tree_to_ast(e.children[0], e),
Expand All @@ -376,7 +382,7 @@ def parse_tree_to_ast(e, parent):
return Suffices(e.meta,
parse_tree_to_ast(e.children[0], e),
parse_tree_to_ast(e.children[1], e),
parse_tree_to_ast(e.children[2], e))
None)
elif e.data == 'term_proof':
return PTerm(e.meta,
parse_tree_to_ast(e.children[0], e),
Expand All @@ -391,21 +397,17 @@ def parse_tree_to_ast(e, parent):
return PAndElim(e.meta, int(e.children[0].value), subject)
elif e.data == 'imp_intro':
label = str(e.children[0].value)
body = parse_tree_to_ast(e.children[1], e)
return ImpIntro(e.meta, label, None, body)
return ImpIntro(e.meta, label, None, None)
elif e.data == 'imp_intro_explicit':
label = str(e.children[0].value)
premise = parse_tree_to_ast(e.children[1], e)
body = parse_tree_to_ast(e.children[2], e)
return ImpIntro(e.meta, label, premise, body)
return ImpIntro(e.meta, label, premise, None)
elif e.data == 'imp_intro_anon':
premise = parse_tree_to_ast(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
return ImpIntro(e.meta, '_', premise, body)
return ImpIntro(e.meta, '_', premise, None)
elif e.data == 'all_intro':
vars = parse_tree_to_list(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
result = body
result = None
for i, var in enumerate(reversed(vars)):
result = AllIntro(e.meta, var, (i, len(vars)), result)
return result
Expand All @@ -425,21 +427,18 @@ def parse_tree_to_ast(e, parent):
return result
elif e.data == 'some_intro':
witnesses = parse_tree_to_list(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
return SomeIntro(e.meta, witnesses, body)
return SomeIntro(e.meta, witnesses, None)
elif e.data == 'some_elim':
witnesses = parse_tree_to_list(e.children[0], e)
label = parse_tree_to_ast(e.children[1], e)
some = parse_tree_to_ast(e.children[2], e)
body = parse_tree_to_ast(e.children[3], e)
return SomeElim(e.meta, witnesses, label, None, some, body)
return SomeElim(e.meta, witnesses, label, None, some, None)
elif e.data == 'some_elim_explicit':
witnesses = parse_tree_to_list(e.children[0], e)
label = parse_tree_to_ast(e.children[1], e)
prop = parse_tree_to_ast(e.children[2], e)
some = parse_tree_to_ast(e.children[3], e)
body = parse_tree_to_ast(e.children[4], e)
return SomeElim(e.meta, witnesses, label, prop, some, body)
return SomeElim(e.meta, witnesses, label, prop, some, None)
elif e.data == 'case':
tag = str(e.children[0].value)
body = parse_tree_to_ast(e.children[1], e)
Expand Down Expand Up @@ -478,7 +477,8 @@ def parse_tree_to_ast(e, parent):
subject = parse_tree_to_ast(e.children[0], e)
definitions = parse_tree_to_list(e.children[1], e)
cases = parse_tree_to_list(e.children[2], e)
return ApplyDefsGoal(e.meta, [Var(e.meta, None, t, []) for t in definitions],
return ApplyDefsGoal(e.meta, [Var(e.meta, None, t, []) \
for t in definitions],
SwitchProof(e.meta, subject, cases))
elif e.data == 'ind_case':
pat = parse_tree_to_ast(e.children[0], e)
Expand All @@ -501,8 +501,7 @@ def parse_tree_to_ast(e, parent):
return EvaluateFact(e.meta, subject)
elif e.data == 'apply_defs_goal_one':
definition = parse_tree_to_ast(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
return ApplyDefsGoal(e.meta, [Var(e.meta, None, definition, [])], body)
return ApplyDefsGoal(e.meta, [Var(e.meta, None, definition, [])], None)
elif e.data == 'apply_defs_fact':
definitions = parse_tree_to_list(e.children[0], e)
subject = parse_tree_to_ast(e.children[1], e)
Expand All @@ -517,10 +516,9 @@ def parse_tree_to_ast(e, parent):
subject)
elif e.data == 'enable_defs':
definitions = parse_tree_to_list(e.children[0], e)
subject = parse_tree_to_ast(e.children[1], e)
return EnableDefs(e.meta,
[Var(e.meta, None, x, []) for x in definitions],
subject)
None)
elif e.data == 'reason_definition':
definitions = parse_tree_to_list(e.children[0], e)
return ApplyDefs(e.meta, [Var(e.meta, None, t, []) for t in definitions])
Expand Down Expand Up @@ -549,8 +547,7 @@ def parse_tree_to_ast(e, parent):
subject)
elif e.data == 'rewrite_goal':
eqns = parse_tree_to_list(e.children[0], e)
body = parse_tree_to_ast(e.children[1], e)
return RewriteGoal(e.meta, eqns, body)
return RewriteGoal(e.meta, eqns, None)
elif e.data == 'rewrite_fact':
eqns = parse_tree_to_list(e.children[0], e)
subject = parse_tree_to_ast(e.children[1], e)
Expand Down
4 changes: 2 additions & 2 deletions proof_checker.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -386,12 +386,12 @@ def check_proof(proof, env):
new_formula = apply_definitions(loc, formula, defs, env)
ret = new_formula

case EnableDefs(loc, definitions, subject):
case EnableDefs(loc, definitions, body):
defs = [type_synth_term(d, env, None, []) for d in definitions]
defs = [d.reduce(env) for d in defs]
old_defs = get_reduce_only()
set_reduce_only(defs + old_defs)
ret = check_proof(subject, env)
ret = check_proof(body, env)
set_reduce_only(old_defs)

case RewriteFact(loc, subject, equation_proofs):
Expand Down

0 comments on commit 92a18a0

Please sign in to comment.