Apply clang-format to all files

Author: triviajon

src/commandlanguage/command_exec.h

@@ -1,9 +1,8 @@
 #ifndef COMMAND_EXEC_H
 #define COMMAND_EXEC_H
 
-#include "src/runtime/runtime.h"
-
 #include "src/commandlanguage/command_parser.h"
+#include "src/runtime/runtime.h"
 
 /**
  * Execute a single top-level command in the given runtime.

src/commandlanguage/command_parser.c

@@ -292,8 +292,7 @@ ShowKeyword command_parse_show_type(Parser *p) {
         return SHOW_KW_STATE;
     }
 
-    parser_error(
-        p, "expected 'Context', 'Proof', 'Goal', or 'State' after 'Show'");
+    parser_error(p, "expected 'Context', 'Proof', 'Goal', or 'State' after 'Show'");
 
     // Unreachable, but avoids compiler warning.
     return SHOW_KW_STATE;
@@ -348,8 +347,8 @@ Command *command_parse_inductive(Parser *p) {
     while (parser_expect_no_consume(p, TOK_PIPE)) {
         InductiveConstructor *ctor = command_parse_constructor(p);
 
-        constructors = realloc(constructors, sizeof(InductiveConstructor *) *
-                                                 (constructor_count + 1));
+        constructors =
+            realloc(constructors, sizeof(InductiveConstructor *) * (constructor_count + 1));
         constructors[constructor_count] = ctor;
         constructor_count++;
     }

src/commandlanguage/command_parser.h

@@ -30,12 +30,7 @@ typedef struct {
 
 char *stmt_keyword_to_string(StmtKeyword kw);
 
-typedef enum {
-    SHOW_KW_CONTEXT,
-    SHOW_KW_PROOF,
-    SHOW_KW_GOAL,
-    SHOW_KW_STATE
-} ShowKeyword;
+typedef enum { SHOW_KW_CONTEXT, SHOW_KW_PROOF, SHOW_KW_GOAL, SHOW_KW_STATE } ShowKeyword;
 
 typedef struct {
     ShowKeyword kw;
@@ -211,20 +206,18 @@ typedef struct {
     CommandParseFunc parse_func;
 } CommandDispatchEntry;
 
-static CommandDispatchEntry command_dispatch_table[] = {
-    {TOK_AXIOM, command_parse_declaration},
-    {TOK_VARIABLE, command_parse_declaration},
-    {TOK_DEFINITION, command_parse_definition},
-    {TOK_THEOREM, command_parse_statement},
-    {TOK_LEMMA, command_parse_statement},
-    {TOK_CHECK, command_parse_check},
-    {TOK_PRINT, command_parse_print},
-    {TOK_INDUCTIVE, command_parse_inductive},
-    {TOK_SHOW, command_parse_show}};
+static CommandDispatchEntry command_dispatch_table[] = {{TOK_AXIOM, command_parse_declaration},
+                                                        {TOK_VARIABLE, command_parse_declaration},
+                                                        {TOK_DEFINITION, command_parse_definition},
+                                                        {TOK_THEOREM, command_parse_statement},
+                                                        {TOK_LEMMA, command_parse_statement},
+                                                        {TOK_CHECK, command_parse_check},
+                                                        {TOK_PRINT, command_parse_print},
+                                                        {TOK_INDUCTIVE, command_parse_inductive},
+                                                        {TOK_SHOW, command_parse_show}};
 
 #define CMD_DISPATCH_TABLE (command_dispatch_table)
-#define CMD_DISPATCH_TABLE_SIZE \
-    (sizeof(command_dispatch_table) / sizeof(command_dispatch_table[0]))
+#define CMD_DISPATCH_TABLE_SIZE (sizeof(command_dispatch_table) / sizeof(command_dispatch_table[0]))
 
 /**
  * Macro to iterate over all entries in the command dispatch table.

src/common/lexer.c

@@ -9,8 +9,7 @@
 static inline char peek_char(Lexer *lx) { return lx->src[lx->pos]; }
 
 static void debug_print_token(Lexer *lx, Token *t) {
-    if (!lx->options || !lx->options->debug ||
-        !lx->options->debug__print_tokens) {
+    if (!lx->options || !lx->options->debug || !lx->options->debug__print_tokens) {
         return;
     }
 
@@ -157,13 +156,13 @@ static void debug_print_token(Lexer *lx, Token *t) {
             name = "UNKNOWN";
     }
 
-    fprintf(stderr, YEL "[LEX]" DIM " %-12s at %-4d  %s" CRESET "\n", name,
-            t->pos, t->lexeme ? t->lexeme : "");
+    fprintf(stderr, YEL "[LEX]" DIM " %-12s at %-4d  %s" CRESET "\n", name, t->pos,
+            t->lexeme ? t->lexeme : "");
 }
 
 void skip_whitespace(Lexer *lx) {
-    while (lx->src[lx->pos] == ' ' || lx->src[lx->pos] == '\t' ||
-           lx->src[lx->pos] == '\n' || lx->src[lx->pos] == '\r') {
+    while (lx->src[lx->pos] == ' ' || lx->src[lx->pos] == '\t' || lx->src[lx->pos] == '\n' ||
+           lx->src[lx->pos] == '\r') {
         lx->pos++;
     }
 }
@@ -201,9 +200,7 @@ char *skip_comment(Lexer *lx) {
 
 char next_char(Lexer *lx) { return lx->src[lx->pos++]; }
 
-bool is_alpha(char c) {
-    return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z');
-}
+bool is_alpha(char c) { return (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z'); }
 
 bool is_digit(char c) { return (c >= '0' && c <= '9'); }
 

src/common/options.h

@@ -7,8 +7,8 @@ typedef struct {
     bool debug;                // Gate all debug options
     bool debug__print_tokens;  // Print tokens during lexing
     bool debug__print_ast;     // Print AST after parsing
-    bool debug__print_mode;  // Print the current runtime mode and relevant info
-                             // after each update to the mode.
+    bool debug__print_mode;    // Print the current runtime mode and relevant info
+                               // after each update to the mode.
 } MEngineOptions;
 
 #endif  // OPTIONS_H

src/common/parser_base.c

@@ -32,9 +32,7 @@ Token *parser_next(Parser *p) {
     return old_current;
 }
 
-bool parser_eof(Parser *p) {
-    return p->current == NULL || p->current->type == TOK_EOF;
-}
+bool parser_eof(Parser *p) { return p->current == NULL || p->current->type == TOK_EOF; }
 
 Token *parser_peek(Parser *p) { return p->current; }
 

src/engine/rewrite_proof.c

@@ -3,8 +3,7 @@
 #include <stdlib.h>
 
 RewriteProof *init_rewrite_proof(Expression *expr, Expression *rewritten_expr,
-                                 Expression *equality_proof,
-                                 DoublyLinkedList *remaining_goals) {
+                                 Expression *equality_proof, DoublyLinkedList *remaining_goals) {
     RewriteProof *proof = malloc(sizeof(RewriteProof));
     proof->expr = expr;
     proof->rewritten_expr = rewritten_expr;
@@ -19,8 +18,7 @@ void free_rewrite_proof(RewriteProof *proof) {
     }
 }
 
-RewrittenGoal *init_rewritten_goal(Expression *new_goal,
-                                   DoublyLinkedList *remaining_open) {
+RewrittenGoal *init_rewritten_goal(Expression *new_goal, DoublyLinkedList *remaining_open) {
     RewrittenGoal *rewritten_goal = malloc(sizeof(RewrittenGoal));
     rewritten_goal->new_goal = new_goal;
     rewritten_goal->remaining_open = remaining_open;

src/engine/rewrite_proof.h

@@ -13,17 +13,15 @@ typedef struct RewriteProof {
 } RewriteProof;
 
 RewriteProof *init_rewrite_proof(Expression *expr, Expression *rewritten_expr,
-                                 Expression *equality_proof,
-                                 DoublyLinkedList *remaining_goals);
+                                 Expression *equality_proof, DoublyLinkedList *remaining_goals);
 void free_rewrite_proof(RewriteProof *proof);
 
 typedef struct {
     Expression *new_goal;
     DoublyLinkedList *remaining_open;
 } RewrittenGoal;
 
-RewrittenGoal *init_rewritten_goal(Expression *new_goal,
-                                   DoublyLinkedList *remaining_open);
+RewrittenGoal *init_rewritten_goal(Expression *new_goal, DoublyLinkedList *remaining_open);
 void free_rewritten_goal(RewrittenGoal *rewritten_goal);
 
 typedef struct {

src/engine/tactics.h

@@ -1,11 +1,11 @@
 #ifndef NEW_TACTICS_H
 #define NEW_TACTICS_H
 
-#include "src/kernel/expression.h"
 #include "src/kernel/context.h"
+#include "src/kernel/expression.h"
 
 typedef struct {
-    bool success; // true if the tactic was successful, false otherwise
+    bool success;                 // true if the tactic was successful, false otherwise
     DoublyLinkedList *new_goals;  // If success, the new goals, otherwise NULL
     char *error_message;          // If success, NULL, otherwise the error message
 } TacticResult;
@@ -17,27 +17,28 @@ void free_tactic_result(TacticResult *result);
 // DoublyLinkedList *eapply(Expression *goal, Expression *lemma);
 // Expression *eexists(Expression *goal);
 
-// Given a hole with expected type "forall (x : A), B" and a name, 
+// Given a hole with expected type "forall (x : A), B" and a name,
 // fill the hole with the term "λ x : A, ?B" and the result of the tactic is returned.
 TacticResult *intro_tactic(Expression *goal, char *name);
 
 // Given a hole with expected type "forall (x : A), B" and a list of names,
 // fill the hole with the term "λ x : A, ?B" and the result of the tactic is returned.
 TacticResult *intros_tactic(Expression *goal, char **names, size_t name_count);
 
-// Given a hole and a lemma, use unification to match the expected type of the hole with the type of the lemma,
-// and instantiate the lemma with the variables in the hole.
+// Given a hole and a lemma, use unification to match the expected type of the hole with the type of
+// the lemma, and instantiate the lemma with the variables in the hole.
 TacticResult *apply_tactic(Expression *goal, Expression *lemma);
 
-// Given a hole and a lemma, use unification to match the expected type of the hole with the type of the lemma,
-// and instantiate the lemma with the variables in the hole. For any binders in the lemma, 
-// this will create existential variables if necessary to match the goal.
+// Given a hole and a lemma, use unification to match the expected type of the hole with the type of
+// the lemma, and instantiate the lemma with the variables in the hole. For any binders in the
+// lemma, this will create existential variables if necessary to match the goal.
 TacticResult *eapply_tactic(Expression *goal, Expression *lemma);
 
 // Search the context for a variable whose type matches the goal, and fill the hole with it.
 TacticResult *assumption_tactic(Expression *goal);
 
-// Given a hole and a proof term, check if the term's type matches the goal, and fill the hole with it.
+// Given a hole and a proof term, check if the term's type matches the goal, and fill the hole with
+// it.
 TacticResult *exact_tactic(Expression *goal, Expression *proof_term);
 
 typedef struct {
@@ -47,8 +48,9 @@ typedef struct {
     Expression *original_to_rewritten_proof;
 } RewriteResult;
 
-// Given a hole and a lemma, where the hole's expected type has the form eq A x y. The eventual goal is to
-// generalize this to any equivalence relation. See: https://sozeau.gitlabpages.inria.fr/www/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory.pdf
+// Given a hole and a lemma, where the hole's expected type has the form eq A x y. The eventual goal
+// is to generalize this to any equivalence relation. See:
+// https://sozeau.gitlabpages.inria.fr/www/research/publications/A_New_Look_at_Generalized_Rewriting_in_Type_Theory.pdf
 TacticResult *rewrite_tactic(Expression *goal, Expression *lemma);
 
 #endif  // NEW_TACTICS

src/engine/unify.c

@@ -8,8 +8,7 @@ Expression *instantiate_lemma_type(Context *context, Expression *lemma_ty) {
         case (FORALL_EXPRESSION): {
             Expression *bound_var = lemma_ty->as.forall.bound_variable;
             Expression *bound_var_ty = get_expression_type(bound_var);
-            Expression *hole = init_hole_expression(get_var_name(bound_var),
-                                                    bound_var_ty, context);
+            Expression *hole = init_hole_expression(get_var_name(bound_var), bound_var_ty, context);
             Expression *lemma_ty_body = lemma_ty->as.forall.body;
             // lemma_ty_body is closed under context(bound_var), which contains bound_var
             Expression *new_body = new_subst(bound_var, lemma_ty_body, bound_var, hole);
@@ -31,14 +30,12 @@ Expression *instantiate_lemma(Context *context, Expression *lemma) {
 DoublyLinkedList *_list_holes(Expression *expr, DoublyLinkedList *curr) {
     switch (expr->tag) {
         case (LAMBDA_EXPRESSION): {
-            curr = _list_holes(
-                get_expression_type(expr->as.lambda.bound_variable), curr);
+            curr = _list_holes(get_expression_type(expr->as.lambda.bound_variable), curr);
             curr = _list_holes(expr->as.lambda.body, curr);
             return curr;
         }
         case (FORALL_EXPRESSION): {
-            curr = _list_holes(
-                get_expression_type(expr->as.forall.bound_variable), curr);
+            curr = _list_holes(get_expression_type(expr->as.forall.bound_variable), curr);
             curr = _list_holes(expr->as.forall.body, curr);
             return curr;
         }
@@ -71,8 +68,7 @@ int num_holes(Expression *expr) {
     return num_holes;
 }
 
-Expression *_unify2(Expression *exprA, Expression *exprB,
-                    Expression *var_to_fill) {
+Expression *_unify2(Expression *exprA, Expression *exprB, Expression *var_to_fill) {
     if (exprA == exprB) {
         return NULL;
     }
@@ -96,14 +92,12 @@ Expression *_unify2(Expression *exprA, Expression *exprB,
                 return NULL;
             }
 
-            Expression *new_func =
-                _unify2(exprA->as.app.func, exprB->as.app.func, var_to_fill);
+            Expression *new_func = _unify2(exprA->as.app.func, exprB->as.app.func, var_to_fill);
             if (new_func != NULL && new_func->tag != HOLE_EXPRESSION) {
                 return new_func;
             }
 
-            Expression *new_arg =
-                _unify2(exprA->as.app.arg, exprB->as.app.arg, var_to_fill);
+            Expression *new_arg = _unify2(exprA->as.app.arg, exprB->as.app.arg, var_to_fill);
             if (new_arg != NULL) {
                 return new_arg;
             }
@@ -115,9 +109,7 @@ Expression *_unify2(Expression *exprA, Expression *exprB,
     }
 }
 
-Expression *instantiate_lemma_with_bindings(Expression *lemma,
-                                            Expression *lemma_ty,
-                                            Map *binders) {
+Expression *instantiate_lemma_with_bindings(Expression *lemma, Expression *lemma_ty, Map *binders) {
     Expression *final_expr = lemma;
     Expression *curr_forall = lemma_ty;
     while (curr_forall->tag == FORALL_EXPRESSION) {
@@ -128,8 +120,7 @@ Expression *instantiate_lemma_with_bindings(Expression *lemma,
         Context *app_ctx = (final_expr_ctx->ctx_size >= binding_result_ctx->ctx_size)
                                ? final_expr_ctx
                                : binding_result_ctx;
-        final_expr =
-            init_app_expression_wc(final_expr, binding_result, app_ctx);
+        final_expr = init_app_expression_wc(final_expr, binding_result, app_ctx);
         Expression *curr_forall_body = curr_forall->as.forall.body;
         // curr_forall_body is closed under context(binding_var), which contains binding_var
         curr_forall = new_subst(binding_var, curr_forall_body, binding_var, binding_result);
@@ -139,8 +130,7 @@ Expression *instantiate_lemma_with_bindings(Expression *lemma,
 
 UnificationResult *init_unification_result(Expression *lemma_instantiation,
                                            DoublyLinkedList *new_goals) {
-    UnificationResult *unification_result =
-        (UnificationResult *)malloc(sizeof(UnificationResult));
+    UnificationResult *unification_result = (UnificationResult *)malloc(sizeof(UnificationResult));
     unification_result->lemma_instantiation = lemma_instantiation;
     unification_result->new_goals = new_goals;
     return unification_result;
@@ -166,50 +156,41 @@ UnificationResult *eunify2(Expression *lemma, Expression *goal) {
     Expression *current_lemma_app_ty = get_expression_type(current_lemma_app);
     DoublyLinkedList *remaining_open = dll_create();
     while (current_lemma_app_ty->tag == FORALL_EXPRESSION) {
-        Expression *bound_variable =
-            current_lemma_app_ty->as.forall.bound_variable;
-        Expression *hole_subst = _unify2(
-            get_innermost_body(current_lemma_app_ty), expr, bound_variable);
+        Expression *bound_variable = current_lemma_app_ty->as.forall.bound_variable;
+        Expression *hole_subst =
+            _unify2(get_innermost_body(current_lemma_app_ty), expr, bound_variable);
 
         if (hole_subst == NULL) {
             Expression *hole_to_fill = init_hole_expression(
-                get_var_name(bound_variable),
-                get_expression_type(bound_variable), goal_context);
-            current_lemma_app = init_app_expression_wc(
-                current_lemma_app, hole_to_fill, goal_context);
+                get_var_name(bound_variable), get_expression_type(bound_variable), goal_context);
+            current_lemma_app =
+                init_app_expression_wc(current_lemma_app, hole_to_fill, goal_context);
             dll_insert_at_tail(remaining_open, dll_new_node(hole_to_fill));
         } else {
-            current_lemma_app = init_app_expression_wc(
-                current_lemma_app, hole_subst, goal_context);
+            current_lemma_app = init_app_expression_wc(current_lemma_app, hole_subst, goal_context);
         }
         current_lemma_app_ty = get_expression_type(current_lemma_app);
     }
     return init_unification_result(current_lemma_app, remaining_open);
 }
 
-UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma,
-                                    Expression *expr) {
+UnificationResult *bad_unify_for_eq(Context *goal_context, Expression *lemma, Expression *expr) {
     Expression *current_lemma_app = lemma;
     Expression *current_lemma_app_ty = get_expression_type(current_lemma_app);
     DoublyLinkedList *remaining_open = dll_create();
     while (current_lemma_app_ty->tag == FORALL_EXPRESSION) {
-        Expression *current_lemma_ty_lhs =
-            _get_lhs_eq(get_innermost_body(current_lemma_app_ty));
-        Expression *bound_variable =
-            current_lemma_app_ty->as.forall.bound_variable;
-        Expression *hole_subst =
-            _unify2(current_lemma_ty_lhs, expr, bound_variable);
+        Expression *current_lemma_ty_lhs = _get_lhs_eq(get_innermost_body(current_lemma_app_ty));
+        Expression *bound_variable = current_lemma_app_ty->as.forall.bound_variable;
+        Expression *hole_subst = _unify2(current_lemma_ty_lhs, expr, bound_variable);
 
         if (hole_subst == NULL) {
             Expression *hole_to_fill = init_hole_expression(
-                get_var_name(bound_variable),
-                get_expression_type(bound_variable), goal_context);
-            current_lemma_app = init_app_expression_wc(
-                current_lemma_app, hole_to_fill, goal_context);
+                get_var_name(bound_variable), get_expression_type(bound_variable), goal_context);
+            current_lemma_app =
+                init_app_expression_wc(current_lemma_app, hole_to_fill, goal_context);
             dll_insert_at_tail(remaining_open, dll_new_node(hole_to_fill));
         } else {
-            current_lemma_app = init_app_expression_wc(
-                current_lemma_app, hole_subst, goal_context);
+            current_lemma_app = init_app_expression_wc(current_lemma_app, hole_subst, goal_context);
         }
         current_lemma_app_ty = get_expression_type(current_lemma_app);
     }