Implement cbv tactic

Author: triviajon

examples/cbv_tactic.me

@@ -0,0 +1,12 @@
+(* cbv_tactic.me *)
+(* Using the cbv tactic. *)
+
+Inductive nat : Type := | O : nat | S : forall (_: nat), nat.
+
+Check nat.
+Check (S O).
+Check nat_ind.
+
+Fixpoint add (n : nat) (m : nat) {struct n} : nat := match n with | O => m | S n' => S (add n' m) end.
+
+Theorem test1 : eq nat (add (S O) (O)) (S O).

src/commandlanguage/command_exec.c

@@ -832,8 +832,10 @@ static int _handle_show_command(MEngineRuntime *rt, ShowCmd *show_cmd) {
             // Show proof term
             Expression *pending_theorem = proof_state_pending_theorem(rt->proof_state);
             Expression *pending_theorem_body = get_expression_body(pending_theorem);
-            MPRINT(rt->options->quiet, stdout, HEADER "Proof Term:" CRESET "\n%s\n",
-                   stringify_expression(pending_theorem_body));
+            Expression *pending_theorem_type = get_expression_type(pending_theorem);
+            MPRINT(rt->options->quiet, stdout, HEADER "Proof Term:" CRESET "\n%s : %s\n",
+                   stringify_expression(pending_theorem_body),
+                   stringify_expression(pending_theorem_type));
             return 0;
         }
         case SHOW_KW_GOAL: {

src/engine/tactics.c

@@ -1,11 +1,14 @@
 #include "src/engine/tactics.h"
 
 #include <stdlib.h>
+#include <string.h>
 
 #include "src/common/doubly_linked_list.h"
 #include "src/engine/rewrite_internal.h"
+#include "src/engine/tactic_api.h"
 #include "src/engine/unify.h"
 #include "src/kernel/expression.h"
+#include "src/kernel/normalize.h"
 #include "src/kernel/subst.h"
 #include "src/runtime/core.h"
 
@@ -326,4 +329,43 @@ TacticResult *erewrite_tactic(Expression *goal, Expression *lemma) {
     TacticResult *tac_result = init_tactic_result(true, new_goals, NULL);
     free_rewrite_result(rwr);
     return tac_result;
+}
+
+TacticResult *cbv_tactic(Expression *goal, char **rules, int rule_count) {
+    ReductionFlags flags = 0;
+    if (!rules || rule_count == 0) {
+        flags = REDUCE_ALL;
+    } else {
+        for (int i = 0; i < rule_count; i++) {
+            if (strcmp(rules[i], "beta")) {
+                flags |= REDUCE_BETA;
+            } else if (strcmp(rules[i], "delta")) {
+                flags |= REDUCE_DELTA;
+            } else if (strcmp(rules[i], "iota")) {
+                flags |= REDUCE_IOTA;
+            } else if (strcmp(rules[i], "fix")) {
+                flags |= REDUCE_FIX;
+            } else {
+                // unknown rule for now
+                return init_tactic_result(false, NULL, "Unknown converison rule in cbv.");
+            }
+        }
+    }
+
+    char *old_goal_name = get_hole_name(goal);
+    Expression *old_goal_ty = get_expression_type(goal);
+    Context *ctx = get_expression_context(goal);
+
+    Expression *new_goal_ty = normalize_cbv(old_goal_ty, flags);
+    Expression *new_goal = init_hole_expression(old_goal_name, new_goal_ty, ctx);
+
+    if (!can_fill(goal, new_goal)) {
+        return init_tactic_result(false, NULL, "Failed to fill the goal conversion");
+    }
+
+    fill_hole(goal, new_goal);
+
+    DoublyLinkedList *new_goals = dll_create();
+    dll_insert_at_tail(new_goals, dll_new_node(new_goal));
+    return init_tactic_result(true, new_goals, NULL);
 }

src/engine/tactics.h

@@ -40,4 +40,16 @@ TacticResult *rewrite_tactic(Expression *goal, Expression *lemma);
 // Same as rewrite_tactic, but allows unresolved binders to be added as goals to the proof state.
 TacticResult *erewrite_tactic(Expression *goal, Expression *lemma);
 
+// Given a goal, and optionally a list of conversion rules, attempt to normalize the goal by
+// applying the set of conversion rules given in `rules`.
+//
+// Supported rules:
+// - beta: (fun x => t) u ~> t[x := u]
+// - delta: unfold definitions
+// - iota: match on constructors
+// - fix: fixpoint to lambdas
+//
+// If `rules` is NULL, then all rules are applied
+TacticResult *cbv_tactic(Expression *goal, char **rules, int rule_count);
+
 #endif  // NEW_TACTICS

src/kernel/definitional_equal.c

@@ -0,0 +1,102 @@
+#include "src/kernel/definitional_equal.h"
+
+#include "src/common/linear_map.h"
+#include "src/kernel/normalize.h"
+
+static bool _defeq(Expression *a, Expression *b, LinearMap *mapping) {
+    // Reduce both sides to WHNF before inspecting structure
+    a = normalize_whnf(a);
+    b = normalize_whnf(b);
+
+    if (a == b) {
+        return true;
+    }
+
+    if (a->tag != b->tag) {
+        return false;
+    }
+
+    switch (a->tag) {
+        case TYPE_EXPRESSION:
+        case PROP_EXPRESSION:
+            return true;
+
+        case VAR_EXPRESSION:
+        case HOLE_EXPRESSION:
+            return (a == b) || (linear_map_get(mapping, a) == b);
+
+        case APP_EXPRESSION:
+            return _defeq(a->as.app.func, b->as.app.func, mapping) &&
+                   _defeq(a->as.app.arg, b->as.app.arg, mapping);
+
+        case FORALL_EXPRESSION:
+            linear_map_set(mapping, a->as.forall.bound_variable, b->as.forall.bound_variable);
+            return _defeq(a->as.forall.body, b->as.forall.body, mapping);
+
+        case LAMBDA_EXPRESSION:
+            linear_map_set(mapping, a->as.lambda.bound_variable, b->as.lambda.bound_variable);
+            return _defeq(a->as.lambda.body, b->as.lambda.body, mapping);
+
+        case MATCH_EXPRESSION: {
+            if (!_defeq(a->as.match.scrutinee, b->as.match.scrutinee, mapping)) {
+                return false;
+            }
+
+            if (a->as.match.branch_count != b->as.match.branch_count) {
+                return false;
+            }
+
+            for (int i = 0; i < a->as.match.branch_count; i++) {
+                MatchBranch *ba = a->as.match.branches[i];
+                MatchBranch *bb = b->as.match.branches[i];
+
+                if (!_defeq(ba->constructor, bb->constructor, mapping)) {
+                    return false;
+                }
+
+                if (ba->pattern_var_count != bb->pattern_var_count) {
+                    return false;
+                }
+
+                for (int j = 0; j < ba->pattern_var_count; j++) {
+                    linear_map_set(mapping, ba->pattern_variables[j], bb->pattern_variables[j]);
+                }
+
+                if (!_defeq(ba->body, bb->body, mapping)) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        case FIX_EXPRESSION:
+            linear_map_set(mapping, a->as.fix.recursive_var, b->as.fix.recursive_var);
+
+            if (a->as.fix.arg_count != b->as.fix.arg_count) {
+                return false;
+            }
+
+            if (a->as.fix.decreasing_arg_index != b->as.fix.decreasing_arg_index) {
+                return false;
+            }
+
+            for (int i = 0; i < a->as.fix.arg_count; i++) {
+                linear_map_set(mapping, a->as.fix.args[i], b->as.fix.args[i]);
+            }
+
+            return _defeq(a->as.fix.body, b->as.fix.body, mapping);
+    }
+
+    return false;
+}
+
+bool definitional_equal(Expression *a, Expression *b) {
+    if (a == b) {
+        return true;
+    }
+
+    LinearMap *mapping = linear_map_new();
+    bool result = _defeq(a, b, mapping);
+    linear_map_clear_free(mapping);
+    return result;
+}

src/kernel/definitional_equal.h

@@ -0,0 +1,8 @@
+#ifndef DEFINITIONAL_EQUAL_H
+#define DEFINITIONAL_EQUAL_H
+
+#include "src/kernel/expression.h"
+
+bool definitional_equal(Expression *a, Expression *b);
+
+#endif  // DEFINITIONAL_EQUAL_H

src/kernel/expression.c

@@ -8,6 +8,7 @@
 #include "src/common/linear_map.h"
 #include "src/kernel/beta_reduction.h"
 #include "src/kernel/context.h"
+#include "src/kernel/definitional_equal.h"
 #include "src/kernel/inductive.h"
 #include "src/kernel/structural.h"
 #include "src/kernel/subst.h"
@@ -1328,7 +1329,7 @@ bool is_hole(Expression *expr) { return expr->tag == HOLE_EXPRESSION; }
 //    3) Term does not itself contain the hole.
 // This does no modifications/creates no new objects.
 bool can_fill(Expression *hole, Expression *term) {
-    bool types_match = congruent_with_holes(get_expression_type(hole), get_expression_type(term));
+    bool types_match = definitional_equal(get_expression_type(hole), get_expression_type(term));
     if (get_maybe_hole_free(term)) {
         return types_match && valid_in_context(term, get_expression_context(hole));
     }
@@ -1412,71 +1413,57 @@ void fill_hole(Expression *hole, Expression *term) {
         return;
     }
 
-    // check if term satisfies hole type...
-    LinearMap *alpha_equivalences = linear_map_new();
-    LinearMap *required_holes = linear_map_new();
-    bool types_match = _congruent_with_holes(get_expression_type(hole), get_expression_type(term),
-                                             alpha_equivalences, required_holes);
+    bool types_match = definitional_equal(get_expression_type(hole), get_expression_type(term));
     if (!types_match) {
-        linear_map_clear_free(alpha_equivalences);
-        linear_map_clear_free(required_holes);
         return;  // Todo: signal that this has failed?
     }
-
-    int n = required_holes->size;
-    for (int i = 0; i < n; i++) {
-        Expression *hole = (required_holes->items + i)->key;
-        Expression *substitute = (required_holes->items + i)->val;
-        fill_hole(hole, substitute);
-    }
-
     DoublyLinkedList *holepars = hole->uplinks;
     for (int i = 0; i < dll_len(holepars); i++) {
         Uplink *uplink = dll_at(holepars, i)->data;
         switch (uplink->relation) {
             case (LAMBDA_BODY): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.lambda.body = term;
+                SET_LAMBDA_BODY(ptr, term);
                 break;
             }
             case (LAMBDA_BOUND_VAR): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.lambda.bound_variable = term;
+                SET_LAMBDA_BOUND_VAR(ptr, term);
                 break;
             }
             case (APP_FUNC): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.app.func = term;
+                SET_APP_FUNC(ptr, term);
                 break;
             }
             case (APP_ARG): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.app.arg = term;
+                SET_APP_ARG(ptr, term);
                 break;
             }
             case (FORALL_BODY): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.forall.body = term;
+                SET_FORALL_BODY(ptr, term);
                 break;
             }
             case (FORALL_BOUND_VAR): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.forall.bound_variable = term;
+                SET_FORALL_BOUND_VAR(ptr, term);
                 break;
             }
             case (VAR_BODY): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->as.var.body = term;
+                SET_VAR_BODY(ptr, term);
                 break;
             }
             case (EXPR_TYPE): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->type = term;
+                SET_EXPR_TYPE(ptr, term);
                 break;
             }
             case (EXPR_CONTEXT): {
                 Expression *ptr = (Expression *)uplink->ptr;
-                ptr->context = term;
+                SET_EXPR_CONTEXT(ptr, term);
                 break;
             }
             default:
@@ -1485,9 +1472,6 @@ void fill_hole(Expression *hole, Expression *term) {
                 break;
         }
     }
-
-    linear_map_clear_free(alpha_equivalences);
-    linear_map_clear_free(required_holes);
 }
 
 char c_counter = 'a';