diff --git a/Deduce.lark b/Deduce.lark index 10779e9..a256d31 100644 --- a/Deduce.lark +++ b/Deduce.lark @@ -146,21 +146,13 @@ 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 @@ -168,41 +160,54 @@ ident: IDENT -> ident | "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 diff --git a/abstract_syntax.py b/abstract_syntax.py index f8a8c3e..76c5e42 100644 --- a/abstract_syntax.py +++ b/abstract_syntax.py @@ -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): @@ -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): diff --git a/parser.py b/parser.py index ce46049..c10e393 100644 --- a/parser.py +++ b/parser.py @@ -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), @@ -337,14 +347,10 @@ 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': @@ -352,18 +358,18 @@ def parse_tree_to_ast(e, parent): 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), @@ -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), @@ -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 @@ -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) @@ -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) @@ -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) @@ -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]) @@ -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) diff --git a/proof_checker.py b/proof_checker.py index a961b0c..94ad391 100644 --- a/proof_checker.py +++ b/proof_checker.py @@ -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):