pred absurd();

// ## Identifiers
//
// The `Ident` type corresponds to actual strings that occur in the source
// file. The `VirtIdent` type represent ids that do not occur verbatim in
// source code, but semantically correspond to identifiers. For example, each
// occurence of a wildcard token _ corresponds to a separate `VirtIdent` which
// does not arise from an `Ident`.
type Ident;
type VirtIdent;

func real_virt_ident(Ident) -> VirtIdent;
func virt_real_ident(VirtIdent) -> Ident;

rule real_virt_ident_total {
    if ident: Ident;
    then real_virt_ident(ident)!;
}
rule virt_real_ident_retraction {
    if virt_ident = real_virt_ident(ident);
    then virt_real_ident(virt_ident) = ident;
}

// ## Abstract syntax tree (AST) nodes

type TypeDeclNode;
pred type_decl(TypeDeclNode, name: Ident);

type ArgDeclNode;
// arg_decl_node_name is optional (but must be unique), arg_decl_node_type is
// mandatory and must be unique.
pred arg_decl_node_name(ArgDeclNode, name: Ident);
pred arg_decl_node_type(ArgDeclNode, typ: Ident);

type ArgDeclListNode;
pred nil_arg_decl_list_node(ArgDeclListNode);
pred cons_arg_decl_list_node(ArgDeclListNode, head: ArgDeclNode, tail: ArgDeclListNode);

type PredDeclNode;
pred pred_decl(PredDeclNode, name: Ident, args: ArgDeclListNode);

type FuncDeclNode;
pred func_decl(FuncDeclNode, name: Ident, args: ArgDeclListNode, result_type: Ident);

type CtorDeclNode;
pred ctor_decl(CtorDeclNode, name: Ident, args: ArgDeclListNode);

type CtorDeclListNode;
pred nil_ctor_decl_list_node(CtorDeclListNode);
pred cons_ctor_decl_list_node(CtorDeclListNode, head: CtorDeclNode, tail: CtorDeclListNode);

type EnumDeclNode;
pred enum_decl(EnumDeclNode, name: Ident, ctors: CtorDeclListNode);

type TermNode;

type TermListNode;
pred nil_term_list_node(nil: TermListNode);
pred cons_term_list_node(node: TermListNode, head: TermNode, tail: TermListNode);

type OptTermNode;
pred none_term_node(OptTermNode);
pred some_term_node(OptTermNode, value: TermNode);

pred var_term_node(TermNode, VirtIdent);
pred wildcard_term_node(TermNode);
pred app_term_node(TermNode, function: Ident, args: TermListNode);

type MatchCaseNode;
pred match_case(node: MatchCaseNode, pattern: TermNode, body: StmtListNode);

type MatchCaseListNode;
pred nil_match_case_list_node(nil: MatchCaseListNode);
pred cons_match_case_list_node(node: MatchCaseListNode, head: MatchCaseNode, tail: MatchCaseListNode);

type IfAtomNode;
pred equal_if_atom_node(IfAtomNode, lhs: TermNode, rhs: TermNode);
pred defined_if_atom_node(IfAtomNode, term: TermNode);
pred pred_if_atom_node(IfAtomNode, predicate: Ident, args: TermListNode);
pred var_if_atom_node(IfAtomNode, var: TermNode, typ: Ident);

type ThenAtomNode;
pred equal_then_atom_node(ThenAtomNode, lhs: TermNode, rhs: TermNode);
pred defined_then_atom_node(ThenAtomNode, var: OptTermNode, tm: TermNode);
pred pred_then_atom_node(ThenAtomNode, predicate: Ident, args: TermListNode);

type StmtNode;
pred if_stmt_node(StmtNode, IfAtomNode);
pred then_stmt_node(StmtNode, ThenAtomNode);
pred branch_stmt_node(StmtNode, blocks: StmtBlockListNode);
pred match_stmt_node(StmtNode, term: TermNode, cases: MatchCaseListNode);

type StmtListNode;
pred nil_stmt_list_node(nil: StmtListNode);
pred cons_stmt_list_node(node: StmtListNode, head: StmtNode, tail: StmtListNode);

type StmtBlockListNode;
pred nil_stmt_block_list_node(node: StmtBlockListNode);
pred cons_stmt_block_list_node(node: StmtBlockListNode, head: StmtListNode, tail: StmtBlockListNode);

type RuleDeclNode;
pred rule_decl(node: RuleDeclNode, stmts: StmtListNode);
// This is defined for non-anonymous RuleDeclNode elements only.
func rule_name(RuleDeclNode) -> Ident;

type DeclNode;
pred decl_node_type(DeclNode, TypeDeclNode);
pred decl_node_pred(DeclNode, PredDeclNode);
pred decl_node_func(DeclNode, FuncDeclNode);
pred decl_node_rule(DeclNode, RuleDeclNode);
pred decl_node_enum(DeclNode, EnumDeclNode);

type DeclListNode;
pred nil_decl_list_node(DeclListNode);
pred cons_decl_list_node(DeclListNode, head: DeclNode, tail: DeclListNode);

type ModuleNode;
pred decls_module_node(ModuleNode, DeclListNode);

// ### Locations
type Loc;

func type_decl_node_loc(TypeDeclNode) -> Loc;
func arg_decl_node_loc(ArgDeclNode) -> Loc;
func arg_decl_list_node_loc(ArgDeclListNode) -> Loc;
func pred_decl_node_loc(PredDeclNode) -> Loc;
func func_decl_node_loc(FuncDeclNode) -> Loc;
func ctor_decl_node_loc(CtorDeclNode) -> Loc;
func enum_decl_node_loc(EnumDeclNode) -> Loc;
func term_node_loc(TermNode) -> Loc;
func term_list_node_loc(TermListNode) -> Loc;
func match_case_node_loc(MatchCaseNode) -> Loc;
func opt_term_node_loc(OptTermNode) -> Loc;
func if_atom_node_loc(IfAtomNode) -> Loc;
func then_atom_node_loc(ThenAtomNode) -> Loc;
func stmt_node_loc(StmtNode) -> Loc;
func stmt_list_node_loc(StmtListNode) -> Loc;
func rule_decl_node_loc(RuleDeclNode) -> Loc;
func decl_node_loc(DeclNode) -> Loc;
func decl_list_node_loc(DeclListNode) -> Loc;
func module_node_loc(ModuleNode) -> Loc;

// ### Descendant nodes of rules
//
// Every node that can appear as a descendant of a `RuleDeclNode` can be
// coerced into a `RuleDescendantNode`.
type RuleDescendantNode;

func rule_descendant_rule(RuleDeclNode) -> RuleDescendantNode;
func rule_descendant_term(TermNode) -> RuleDescendantNode;
func rule_descendant_term_list(TermListNode) -> RuleDescendantNode;
func rule_descendant_opt_term(OptTermNode) -> RuleDescendantNode;
func rule_descendant_if_atom(IfAtomNode) -> RuleDescendantNode;
func rule_descendant_then_atom(ThenAtomNode) -> RuleDescendantNode;
func rule_descendant_match_case(MatchCaseNode) -> RuleDescendantNode;
func rule_descendant_match_case_list(MatchCaseListNode) -> RuleDescendantNode;
func rule_descendant_stmt(StmtNode) -> RuleDescendantNode;
func rule_descendant_stmt_list(StmtListNode) -> RuleDescendantNode;
func rule_descendant_stmt_block_list(StmtBlockListNode) -> RuleDescendantNode;

rule rule_descendant_rule_total {
    if rul: RuleDeclNode;
    then rule_descendant_rule(rul)!;
}
rule rule_descendant_term_total {
    if tm: TermNode;
    then rule_descendant_term(tm)!;
}
rule rule_descendant_term_list_total {
    if tms: TermListNode;
    then rule_descendant_term_list(tms)!;
}
rule rule_descendant_opt_term_total {
    if opt_tm: OptTermNode;
    then rule_descendant_opt_term(opt_tm)!;
}
rule rule_descendant_if_atom_total {
    if atom: IfAtomNode;
    then rule_descendant_if_atom(atom)!;
}
rule rule_descendant_then_atom_total {
    if atom: ThenAtomNode;
    then rule_descendant_then_atom(atom)!;
}
rule rule_descendant_match_case_total {
    if case: MatchCaseNode;
    then rule_descendant_match_case(case)!;
}
rule rule_descendant_match_case_list_total {
    if cases: MatchCaseListNode;
    then rule_descendant_match_case_list(cases)!;
}
rule rule_descendant_stmt_total {
    if stmt: StmtNode;
    then rule_descendant_stmt(stmt)!;
}
rule rule_descendant_stmt_list_total {
    if stmts: StmtListNode;
    then rule_descendant_stmt_list(stmts)!;
}
rule rule_descendant_stmt_block_list_total {
    if blocks: StmtBlockListNode;
    then rule_descendant_stmt_block_list(blocks)!;
}

/// ### Scopes

type Scope;

pred var_in_scope(VirtIdent, Scope);
pred scope_extension(smaller: Scope, larger: Scope);

rule scope_extension_vars {
    if var_in_scope(ident, scope);
    if scope_extension(scope, extension);
    then var_in_scope(ident, extension);
}

func entry_scope(RuleDescendantNode) -> Scope;
func exit_scope(RuleDescendantNode) -> Scope;

rule entry_exit_scope_total {
    if descendant: RuleDescendantNode;
    then entry_scope(descendant)!;
    then exit_scope(descendant)!;
}
rule exit_scope_extends_entry_scope {
    if node: RuleDescendantNode;
    if entry = entry_scope(node);
    if exit = exit_scope(node);
    then scope_extension(entry, exit);
}

pred scope_single_child(child: RuleDescendantNode, parent: RuleDescendantNode);
pred scope_extension_siblings(first_child: RuleDescendantNode, second_child: RuleDescendantNode, parent: RuleDescendantNode);

rule scope_single_child_scopes {
    if scope_single_child(child, parent);
    if parent_entry = entry_scope(parent);
    if parent_exit = exit_scope(parent);
    then entry_scope(child) = parent_entry;
    then exit_scope(child) = parent_exit;
}

rule scope_extension_siblings_parent_first {
    if scope_extension_siblings(first_child, _, parent);
    if parent_entry = entry_scope(parent);
    then entry_scope(first_child) = parent_entry;
}

rule scope_extension_siblings_first_second {
    if scope_extension_siblings(first_child, second_child, _);
    if first_exit = exit_scope(first_child);
    then entry_scope(second_child) = first_exit;
}

rule scope_extension_siblings_second_parent {
    if scope_extension_siblings(_, second_child, parent);
    if second_exit = exit_scope(second_child);
    then exit_scope(parent) = second_exit;
}

rule scopes_rule {
    if rule_decl(rul, stmts);

    if descendant_rule = rule_descendant_rule(rul);
    if descendant_stmts = rule_descendant_stmt_list(stmts);

    then scope_single_child(descendant_stmts, descendant_rule);
}

rule scopes_stmt_list_cons {
    if cons_stmt_list_node(stmts, head, tail);

    if descendant_stmts = rule_descendant_stmt_list(stmts);
    if descendant_head = rule_descendant_stmt(head);
    if descendant_tail = rule_descendant_stmt_list(tail);

    then scope_extension_siblings(descendant_head, descendant_tail, descendant_stmts);
}

rule scopes_stmt_block_list_cons {
    if cons_stmt_block_list_node(blocks, head, tail);
    if descendant_blocks = rule_descendant_stmt_block_list(blocks);
    if descendant_head = rule_descendant_stmt_list(head);
    if descendant_tail = rule_descendant_stmt_block_list(tail);

    if blocks_entry = entry_scope(descendant_blocks);

    then blocks_entry = entry_scope(descendant_head);
    then blocks_entry = entry_scope(descendant_tail);
}

rule scopes_stmt_if {
    if if_stmt_node(stmt, atom);
    if descendant_stmt = rule_descendant_stmt(stmt);
    if descendant_atom = rule_descendant_if_atom(atom);

    then scope_single_child(descendant_atom, descendant_stmt);
}
rule scopes_stmt_then {
    if then_stmt_node(stmt, atom);
    if descendant_stmt = rule_descendant_stmt(stmt);
    if descendant_atom = rule_descendant_then_atom(atom);

    then scope_single_child(descendant_atom, descendant_stmt);
}
rule scopes_stmt_branch {
    if branch_stmt_node(stmt, blocks);
    if descendant_stmt = rule_descendant_stmt(stmt);
    if descendant_block_list = rule_descendant_stmt_block_list(blocks);

    then scope_single_child(descendant_block_list, descendant_stmt);
}
rule scopes_stmt_match {
    if match_stmt_node(stmt, term, cases);
    if stmt_descendant = rule_descendant_stmt(stmt);
    if descendant_term = rule_descendant_term(term);
    if descendant_cases = rule_descendant_match_case_list(cases);

    then scope_extension_siblings(descendant_term, descendant_cases, stmt_descendant);
}

rule scopes_if_atom_equal {
    if equal_if_atom_node(atom, lhs, rhs);
    if atom_descendant = rule_descendant_if_atom(atom);
    if descendant_lhs = rule_descendant_term(lhs);
    if descendant_rhs = rule_descendant_term(rhs);

    then scope_extension_siblings(descendant_lhs, descendant_rhs, atom_descendant);
}
rule scopes_if_atom_defined {
    if defined_if_atom_node(atom, tm);
    if atom_descendant = rule_descendant_if_atom(atom);
    if descendant_tm = rule_descendant_term(tm);

    then scope_single_child(descendant_tm, atom_descendant);
}
rule scopes_if_atom_pred {
    if pred_if_atom_node(atom, _, tms);
    if atom_descendant = rule_descendant_if_atom(atom);
    if tms_descendant = rule_descendant_term_list(tms);

    then scope_single_child(tms_descendant, atom_descendant);
}
rule scopes_if_atom_var {
    if var_if_atom_node(atom, tm, _);
    if atom_descendant = rule_descendant_if_atom(atom);
    if tm_descendant = rule_descendant_term(tm);

    then scope_single_child(tm_descendant, atom_descendant);
}

rule scopes_then_atom_equal {
    if equal_then_atom_node(atom, lhs, rhs);

    if atom_descendant = rule_descendant_then_atom(atom);
    if lhs_descendant = rule_descendant_term(lhs);
    if rhs_descendant = rule_descendant_term(rhs);

    then scope_extension_siblings(lhs_descendant, rhs_descendant, atom_descendant);
}
rule scopes_then_atom_defined {
    if defined_then_atom_node(atom, var_tm, tm);
    if atom_descendant = rule_descendant_then_atom(atom);
    if var_tm_descendant = rule_descendant_opt_term(var_tm);
    if tm_descendant = rule_descendant_term(tm);

    then scope_extension_siblings(var_tm_descendant, tm_descendant, atom_descendant);
}
rule scopes_then_atom_pred {
    if pred_then_atom_node(atom, _, tms);
    if atom_descendant = rule_descendant_then_atom(atom);
    if tms_descendant = rule_descendant_term_list(tms);

    then scope_extension_siblings(atom_descendant, tms_descendant, atom_descendant);
}

// No rules for match case nodes -- they're taken care of by desugaring to BlockListNodes.

rule scopes_term_list_cons {
    if cons_term_list_node(tms, head, tail);
    if tms_descendant = rule_descendant_term_list(tms);
    if head_descendant = rule_descendant_term(head);
    if tail_descendant = rule_descendant_term_list(tail);

    then scope_extension_siblings(head_descendant, tail_descendant, tms_descendant);
}
rule scopes_opt_term_some {
    if some_term_node(opt_tm, tm);
    if opt_tm_descendant = rule_descendant_opt_term(opt_tm);
    if tm_descendant = rule_descendant_term(tm);

    then scope_single_child(tm_descendant, opt_tm_descendant);
}
rule scopes_term_app {
    if app_term_node(tm, _, args);
    if tm_descendant = rule_descendant_term(tm);
    if args_descendant = rule_descendant_term_list(args);

    then scope_single_child(args_descendant, tm_descendant);
}
rule scopes_term_var {
    if var_term_node(tm, virt_ident);
    if tm_descendant = rule_descendant_term(tm);
    if tm_exit = exit_scope(tm_descendant);

    then var_in_scope(virt_ident, tm_exit);
}

// ### The enum constructor belong to

func ctor_enum(CtorDeclNode) -> EnumDeclNode;
func ctors_enum(CtorDeclListNode) -> EnumDeclNode;

rule enum_ctors {
    if enum_decl(enum_node, _, ctors);
    then ctors_enum(ctors) = enum_node;
}
rule enum_ctors_cons {
    if ctors_enum(ctors) = enum_node;
    if cons_ctor_decl_list_node(ctors, head_ctor, tail_ctors);
    then ctor_enum(head_ctor) = enum_node;
    then ctors_enum(tail_ctors) = enum_node;
}

// ## Desugaring MatchCase nodes

// ### The discriminee of a match case (list) node.
//
// I.e., the term that is being matched on in the match statement that a match
// case node belongs to.
func cases_discriminee(MatchCaseListNode) -> TermNode;
func case_discriminee(MatchCaseNode) -> TermNode;

rule match_stmt_cases_discriminee {
    if match_stmt_node(_, discriminee, cases);
    then cases_discriminee(cases) = discriminee;
}
rule cases_match_stmt_cons {
    if cases_discriminee(cases) = discriminee;
    if cons_match_case_list_node(cases, head_case, tail_cases);
    then case_discriminee(head_case) = discriminee;
    then cases_discriminee(tail_cases) = discriminee;
}

// ### Desugared AST nodes
func desugared_case_equality_atom(MatchCaseNode) -> IfAtomNode;
func desugared_case_equality_stmt(MatchCaseNode) -> StmtNode;
func desugared_case_block(MatchCaseNode) -> StmtListNode;
func desugared_case_block_list(MatchCaseListNode) -> StmtBlockListNode;

rule desugared_case_equality_stmt_loc {
    if match_case(case_node, pattern, _);
    if pattern_loc = term_node_loc(pattern);
    if stmt_node = desugared_case_equality_stmt(case_node);
    then stmt_node_loc(stmt_node) = pattern_loc;
}

rule desugared_case_defined {
    if match_case(case_node, _, _);

    then desugared_case_equality_atom(case_node)!;
    then desugared_case_equality_stmt(case_node)!;
    then desugared_case_block(case_node)!;
}
rule desugared_case_block_list_defined {
    if cases: MatchCaseListNode;
    then desugared_case_block_list(cases)!;
}

rule desugared_case_equality_atom_stmt {
    if discriminee = case_discriminee(case_node);
    if match_case(case_node, pattern, _);
    if atom = desugared_case_equality_atom(case_node);
    if stmt = desugared_case_equality_stmt(case_node);

    then equal_if_atom_node(atom, discriminee, pattern);
    then if_stmt_node(stmt, atom);
}
rule desugared_case_block_structure {
    if match_case(case_node, _, block);
    if desugared_stmt = desugared_case_equality_stmt(case_node);
    if desugared_block = desugared_case_block(case_node);

    then cons_stmt_list_node(desugared_block, desugared_stmt, block);
}
rule desugared_case_blocks {
    if cons_match_case_list_node(cases, head_case, tail_cases);

    if desugared_blocks = desugared_case_block_list(cases);
    if desugared_head_block = desugared_case_block(head_case);
    if desugared_tail_blocks = desugared_case_block_list(tail_cases);

    then cons_stmt_block_list_node(desugared_blocks, desugared_head_block, desugared_tail_blocks);
}

rule scopes_desugared_case {
    if block = desugared_case_block(case);

    if descendant_block = rule_descendant_stmt_list(block);
    if descendant_case = rule_descendant_match_case(case);

    if entry = entry_scope(descendant_case);
    if exit = exit_scope(descendant_case);

    then entry_scope(descendant_block) = entry;
    then exit_scope(descendant_block) = exit;
}

rule scopes_desugared_case_list {
    if blocks = desugared_case_block_list(cases);

    if descendant_blocks = rule_descendant_stmt_block_list(blocks);
    if descendant_cases = rule_descendant_match_case_list(cases);

    if entry = entry_scope(descendant_cases);
    if exit = exit_scope(descendant_cases);

    then entry_scope(descendant_blocks) = entry;
    then exit_scope(descendant_blocks) = exit;
}

// ## Semantic types, predicates and functions

type Type;
enum TypeList {
    NilTypeList(),
    ConsTypeList(head: Type, tail: TypeList),
    SnocTypeList(init: TypeList, last: Type)
}

rule type_list_nil_not_cons {
    if NilTypeList() = ConsTypeList(_, _);
    then absurd();
}
rule type_list_cons_injective {
    if ConsTypeList(head_0, tail_0) = ConsTypeList(head_1, tail_1);
    then head_0 = head_1;
    then tail_0 = tail_1;
}

func semantic_type(Ident) -> Type;
rule semantic_decl_type {
    if type_decl(_, ident);
    then semantic_type(ident)!;
}
rule semantic_decl_enum {
    if enum_decl(_, ident, _);
    then semantic_type(ident)!;
}

func semantic_arg_types(ArgDeclListNode) -> TypeList;
rule semantic_arg_types_nil {
    if nil_arg_decl_list_node(n);
    then NilTypeList()!;
    then semantic_arg_types(n) = NilTypeList();
}
rule semantic_arg_types_cons {
    if cons_arg_decl_list_node(arg_decls, head, tail);
    if arg_decl_node_type(head, head_type_name);
    if head_type = semantic_type(head_type_name);
    if tail_types = semantic_arg_types(tail);
    then ConsTypeList(head_type, tail_types)!;
    then semantic_arg_types(arg_decls) = ConsTypeList(head_type, tail_types);
}

type Pred;
func semantic_pred(Ident) -> Pred;
rule semantic_decl_pred {
    if pred_decl(_, name, _);
    then semantic_pred(name)!;
}


func pred_arity(Pred) -> TypeList;
rule pred_arity_decl {
    if pred_decl(_, pred_name, arg_decls);
    if predicate = semantic_pred(pred_name);
    if arg_types = semantic_arg_types(arg_decls);
    then pred_arity(predicate) = arg_types;
}

type Func;
func semantic_func(Ident) -> Func;
rule semantic_decl_func {
    if func_decl(_, name, _, _);
    then semantic_func(name)!;
}
rule semantic_decl_func_ctor {
    if ctor_decl(_, name, _);
    then semantic_func(name)!;
}

func domain(Func) -> TypeList;
func codomain(Func) -> Type;
rule func_decl_domain_codomain {
    if func_decl(_, func_name, arg_decls, result_type_name);
    if function = semantic_func(func_name);
    if domain_types = semantic_arg_types(arg_decls);
    if result_type = semantic_type(result_type_name);
    then domain(function) = domain_types;
    then codomain(function) = result_type;
}
rule ctor_decl_domain {
    if ctor_decl(_, ctor_name, arg_decls);
    if function = semantic_func(ctor_name);
    if domain_types = semantic_arg_types(arg_decls);
    then domain(function) = domain_types;
}
rule ctor_decl_codomain {
    if ctor_decl(ctor, ctor_name, _);
    if function = semantic_func(ctor_name);
    if enum_decl(ctor_enum(ctor), enum_name, _);
    if semantic_enum_type = semantic_type(enum_name);
    then codomain(function) = semantic_enum_type;
}

enum Rel {
    PredRel(Pred),
    FuncRel(Func)
    //NegatedPredRel(Pred),
    //UndefinedFuncRel(Func)
}

rule rel_constructors_pred_total {
    if predicate: Pred;
    then PredRel(predicate)!;
    //then NegatedPredRel(predicate)!;
}
rule rel_constructors_func_total {
    if function: Func;
    then FuncRel(function)!;
    //then UndefinedFuncRel(function)!;
}

func arity(Rel) -> TypeList;
//rule pred_rel_arity {
//    if rel = PredRel(predicate);
//    if tys = pred_arity(predicate);
//    then arity(rel) = tys;
//}
//rule func_rel_arity {
//    if rel = FuncRel(function);
//    if dom = domain(function);
//    if cod = codomain(function);
//    then tys := ConsTypeList(cod, dom)!;
//    then arity(rel) = tys;
//}
rule arity_laws {
    if rel: Rel;
    match rel {
        PredRel(predicate) => {
            if tys = pred_arity(predicate);
            then arity(rel) = tys;
        }
        FuncRel(function) => {
            if dom = domain(function);
            if cod = codomain(function);
            then tys := SnocTypeList(dom, cod)!;
            then arity(rel) = tys;
        }
        //NegatedPredRel(predicate) => {
        //    if tys = pred_arity(predicate);
        //    then arity(rel) = tys;
        //}
        //UndefinedFuncRel(function) => {
        //    if tys = domain(function);
        //    then arity(rel) = tys;
        //}
    }
}

// ## Structures

type Structure;

type El;

enum ElList {
    NilElList(Structure),
    ConsElList(head: El, tail: ElList),
    SnocElList(init: ElList, last: El)
}

rule el_list_cons_injective {
    if ConsElList(head_0, tail_0) = ConsElList(head_1, tail_1);
    then head_0 = head_1;
    then tail_0 = tail_1;
}
rule el_list_snoc_injective {
    if SnocElList(init_0, last_0) = SnocElList(init_1, last_1);
    then init_0 = init_1;
    then last_0 = last_1;
}
rule el_list_cons_nil {
    if ConsElList(_, _) = NilElList(_);
    then absurd();
}
rule el_list_snoc_nil {
    if SnocElList(_, _) = NilElList(_);
    then absurd();
}

pred rel_app(Rel, ElList);

type ElName;
func var(Structure, ElName) -> El;

// ### The structure that elements belong to
func el_structure(El) -> Structure;
func els_structure(ElList) -> Structure;
rule nil_els_structure {
    if els = NilElList(structure);
    then els_structure(els) = structure;
}
rule cons_els_structure {
    if els = ConsElList(head, tail);
    if head_structure = el_structure(head);
    then head_structure = els_structure(els);
    then head_structure = els_structure(tail);
}
rule snoc_els_structure {
    if els = SnocElList(init, last);
    if last_structure = el_structure(last);
    then last_structure = els_structure(els);
    then last_structure = els_structure(init);
}

rule var_structure {
    if el = var(structure, _);
    then el_structure(el) = structure;
}

// ### The types of elements
pred el_type(El, Type);
pred el_types(ElList, TypeList);

rule nil_el_types {
    if els = NilElList(_);
    then NilTypeList()!;
    then el_types(els, NilTypeList());
}
rule cons_el_types {
    if els = ConsElList(head, tail);
    if el_type(head, head_type);
    if el_types(tail, tail_types);
    then ConsTypeList(head_type, tail_types)!;
    then el_types(els, ConsTypeList(head_type, tail_types));
}
rule cons_el_types_reverse {
    if els = ConsElList(head, tail);
    if el_types(els, ConsTypeList(head_type, tail_types));
    then el_type(head, head_type);
    then el_types(tail, tail_types);
}

rule snoc_el_types {
    if els = SnocElList(init, last);
    if el_types(init, init_types);
    if el_type(last, last_type);
    then SnocTypeList(init_types, last_type)!;
    then el_types(els, SnocTypeList(init_types, last_type));
}
rule snoc_el_types_reverse {
    if els = SnocElList(init, last);
    if el_types(els, SnocTypeList(init_types, last_type));
    then el_types(init, init_types);
    then el_type(last, last_type);
}

rule rel_app_types {
    if rel_app(rel, els);
    if arity(rel) = ar;
    then el_types(els, ar);
}

// This is only used from Rust. If it's removed we need to
// add an explicit functionality law for rel_app of
// FuncRel relations though.
func func_app(function: Func, args: ElList) -> El;
rule rel_app_func_app {
    if rel_app(FuncRel(function), SnocElList(args, result));
    then result = func_app(function, args);
}

// ### Constrained elements
//
// An element is constrained if it appears in a function
// application (including the result) or in the
// application of a predicate.
pred constrained_el(El);
pred constrained_els(ElList);
rule rel_app_constrained {
    if rel_app(_, args);
    then constrained_els(args);
}
rule constrained_head_tail {
    if constrained_els(ConsElList(head, tail));
    then constrained_el(head);
    then constrained_els(tail);
}
rule constrained_init_snoc {
    if constrained_els(SnocElList(init, last));
    then constrained_els(init);
    then constrained_el(last);
}

// ## Morphisms

type Morphism;
func dom(Morphism) -> Structure;
func cod(Morphism) -> Structure;

rule dom_total {
    if morph: Morphism;
    then dom(morph)!;
}
rule cod_total {
    if morph: Morphism;
    then cod(morph)!;
}

func map_el(Morphism, El) -> El;
func map_els(Morphism, ElList) -> ElList;

// Mapped elements live in the codomain structure.
rule map_el_structure {
    if mapped = map_el(mor, _);
    if cod = cod(mor);
    then el_structure(mapped) = cod;
}

// The operations map_el(mor, -) and map_els(mor, -) are total.
rule map_el_defined {
    if dom(mor) = struct;
    if el_structure(el) = struct;
    then map_el(mor, el)!;
}
// Morphisms commute with nil, cons and snoc.
rule map_els_defined {
    if els_structure(els) = dom(mor);
    match els {
        NilElList(_) => {
            if c = cod(mor);
            then cod_nil := NilElList(c)!;
            then map_els(mor, els) = cod_nil;
        }
        ConsElList(head, tail) => {
            if cod_head = map_el(mor, head);
            if cod_tail = map_els(mor, tail);
            then cod_cons := ConsElList(cod_head, cod_tail)!;
            then map_els(mor, els) = cod_cons;
        }
        SnocElList(init, last) => {
            if cod_init = map_els(mor, init);
            if cod_last = map_el(mor, last);
            then cod_snoc := SnocElList(cod_init, cod_last)!;
            then map_els(mor, els) = cod_snoc;
        }
    }
}

// Morphisms commute with relations and variables.
rule map_var {
    if el = var(_, name);
    if mapped_el = map_el(morph, el);
    if cod(morph) = cod_structure;
    then mapped_el = var(cod_structure, name);
}
rule map_rel_app {
    if rel_app(rel, args);
    if mapped_args = map_els(_, args);
    then rel_app(rel, mapped_args);
}

// Morphisms preserve and reflect types.
rule map_preserves_el_type {
    if el_type(el, typ);
    if mapped_el = map_el(_, el);
    then el_type(mapped_el, typ);
}
rule map_reflects_el_type {
    if el_type(map_el(_, el), typ);
    then el_type(el, typ);
}

// ### Kernel pairs of morphisms.

pred in_ker(Morphism, El, El);
rule in_ker_rule {
    if map_el(morph, el_0) = map_el(morph, el_1);
    then in_ker(morph, el_0, el_1);
}

// ### Images of morphisms.

pred el_in_img(Morphism, El);
rule el_in_img_rule {
    if map_el(morph, _) = el;
    then el_in_img(morph, el);
}

pred rel_tuple_in_img(Morphism, Rel, ElList);
rule rel_tuple_in_img_law {
    if rel_app(rel, dom_els);
    if cod_els = map_els(morphism, dom_els);
    then rel_tuple_in_img(morphism, rel, cod_els);
}

// ## Symbol checks
//
// This is for facilitating checks for duplicated symbols, wrong symbol types,
// and wrong argument numbers.

type SymbolKind;
func type_symbol() -> SymbolKind;
func pred_symbol() -> SymbolKind;
func func_symbol() -> SymbolKind;
func rule_symbol() -> SymbolKind;
func enum_symbol() -> SymbolKind;
func ctor_symbol() -> SymbolKind;
rule {
    then type_symbol()!;
    then pred_symbol()!;
    then func_symbol()!;
    then rule_symbol()!;
    then enum_symbol()!;
    then ctor_symbol()!;
}

pred defined_symbol(Ident, SymbolKind, Loc);

rule type_decl_defines_symbol {
    if type_decl(decl, name);
    if kind = type_symbol();
    if loc = type_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}
rule enum_decl_defines_symbol {
    if enum_decl(decl, name, _);
    if kind = enum_symbol();
    if loc = enum_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}
rule pred_decl_defines_symbol {
    if pred_decl(decl, name, _);
    if kind = pred_symbol();
    if loc = pred_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}
rule func_decl_defines_symbol {
    if func_decl(decl, name, _, _);
    if kind = func_symbol();
    if loc = func_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}
rule ctor_decl_defines_symbol {
    if ctor_decl(decl, name, _);
    if kind  = ctor_symbol();
    if loc = ctor_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}
rule rule_decl_defines_symbol {
    if rule_decl(decl, _);
    if name = rule_name(decl);
    if kind = rule_symbol();
    if loc = rule_decl_node_loc(decl);
    then defined_symbol(name, kind, loc);
}

// ### Symbol lookup checks

// Only one kind of symbol is allowed.
pred should_be_symbol(name: Ident, kind: SymbolKind, loc: Loc);
// Two kinds of symbols are allowed, with `kind_1` being the typical one.
pred should_be_symbol_2(name: Ident, kind_1: SymbolKind, kind_2: SymbolKind, loc: Loc);

rule arg_decl_should_be_type {
    if arg_decl_node_type(arg_decl, name);
    if type_kind = type_symbol();
    if enum_kind = enum_symbol();
    if loc = arg_decl_node_loc(arg_decl);
    then should_be_symbol_2(name, type_kind, enum_kind, loc);
}
rule result_should_be_type {
    if func_decl(func_decl, _, _, result_type);
    if type_kind = type_symbol();
    if enum_kind = enum_symbol();
    if loc = func_decl_node_loc(func_decl);
    then should_be_symbol_2(result_type, type_kind, enum_kind, loc);
}
rule var_atom_should_be_type {
    if var_if_atom_node(atom, _, name);
    if type_kind = type_symbol();
    if enum_kind = enum_symbol();
    if loc = if_atom_node_loc(atom);
    then should_be_symbol_2(name, type_kind, enum_kind, loc);
}
rule pred_if_atom_should_be_pred {
    if pred_if_atom_node(atom, pred_name, _);
    if kind = pred_symbol();
    if loc = if_atom_node_loc(atom);
    then should_be_symbol(pred_name, kind, loc);
}
rule pred_then_atom_should_be_pred {
    if pred_then_atom_node(atom, pred_name, _);
    if kind = pred_symbol();
    if loc = then_atom_node_loc(atom);
    then should_be_symbol(pred_name, kind, loc);
}
rule app_atom_should_be_func {
    if app_term_node(term, name, _);
    if func_kind = func_symbol();
    if ctor_kind = ctor_symbol();
    if loc = term_node_loc(term);
    then should_be_symbol_2(name, func_kind, ctor_kind, loc);
}

// ### Natural numbers and argument numbers

type Nat;
func zero() -> Nat;
func succ(Nat) -> Nat;

func type_list_len(TypeList) -> Nat;
rule type_list_len_total {
    if tys: TypeList;
    then type_list_len(tys)!;
}
rule type_list_len_nil {
    if tys = NilTypeList();
    if len = type_list_len(tys);
    then len = zero();
}
rule type_list_len_cons {
    if tys = ConsTypeList(_, tail);
    if len = type_list_len(tys);
    if tail_len = type_list_len(tail);
    then len = succ(tail_len);
}
rule type_list_len_snoc {
    if tys = SnocTypeList(init, _);
    if len = type_list_len(tys);
    if init_len = type_list_len(init);
    then len = succ(init_len);
}

func term_list_len(TermListNode) -> Nat;
rule term_list_len_total {
    if terms: TermListNode;
    then term_list_len(terms)!;
}
rule term_list_len_nil {
    if nil_term_list_node(terms);
    if len = term_list_len(terms);
    then len = zero();
}
rule term_list_len_cons {
    if cons_term_list_node(terms, _, tail);
    if len = term_list_len(terms);
    if tail_len = term_list_len(tail);
    then len = succ(tail_len);
}

pred pred_arg_num_should_match(
    got: Nat,
    expected: Nat,
    usage: Loc
);
pred func_arg_num_should_match(
    got: Nat,
    expected: Nat,
    usage: Loc
);

rule pred_if_atom_arg_num_should_match {
    if pred_if_atom_node(atom, name, args);
    if got_len = term_list_len(args);
    if expected_len = type_list_len(pred_arity(semantic_pred(name)));
    if loc = if_atom_node_loc(atom);
    then pred_arg_num_should_match(got_len, expected_len, loc);
}
rule pred_then_atom_arg_num_should_match {
    if pred_then_atom_node(atom, name, args);
    if got_len = term_list_len(args);
    if expected_len = type_list_len(pred_arity(semantic_pred(name)));
    if loc = then_atom_node_loc(atom);
    then pred_arg_num_should_match(got_len, expected_len, loc);
}

rule app_term_arg_num_should_match {
    if app_term_node(tm, name, args);
    if got_len = term_list_len(args);
    if expected_len = type_list_len(domain(semantic_func(name)));
    if loc = term_node_loc(tm);
    then func_arg_num_should_match(got_len, expected_len, loc);
}

// ## Control flow graph
pred cfg_edge(from: StmtNode, to: StmtNode);

// ### Control flow from and into StmtListNodes
// 
// If control flows into a list of statements, then it flows into the first statement in that list.
// If control flows out of a statement list, then it flows out of every suffix of the statement list, and from the last statement in the list.
// In case of an empty statement list, there's an ordinary cfg edge between every before-statement to every after-statement.
pred cfg_edge_stmts_stmt(from: StmtListNode, to: StmtNode);
pred cfg_edge_stmt_stmts(from: StmtNode, to: StmtListNode);

rule cfg_edge_stmts_stmt_cons {
    if cfg_edge_stmts_stmt(stmts, stmt);
    if cons_stmt_list_node(stmts, _, tail);
    then cfg_edge_stmts_stmt(tail, stmt);
}
rule cfg_edge_stmts_stmt_singleton {
    if cfg_edge_stmts_stmt(stmts, stmt);
    if cons_stmt_list_node(stmts, head, tail);
    if nil_stmt_list_node(tail);
    then cfg_edge(head, stmt);
}

rule cfg_edge_stmt_stmts_cons {
    if cfg_edge_stmt_stmts(stmt, stmts);
    if cons_stmt_list_node(stmts, head, _);
    then cfg_edge(stmt, head);
}
rule cfg_edge_stmt_stmts_nil {
    if cfg_edge_stmt_stmts(stmt, stmts);
    if nil_stmt_list_node(stmts);
    if cfg_edge_stmts_stmt(stmts, next_stmt);
    then cfg_edge(stmt, next_stmt);
}

// ### Control flow from and into branches
//
// This is for branch and match statements.

pred cfg_edge_fork(from: StmtNode, to: StmtBlockListNode);
pred cfg_edge_join(from: StmtBlockListNode, to: StmtNode);

rule cfg_edge_fork_cons {
    if cfg_edge_fork(stmt, blocks);
    if cons_stmt_block_list_node(blocks, head_block, tail_blocks);
    then cfg_edge_fork(stmt, tail_blocks);
    then cfg_edge_stmt_stmts(stmt, head_block);
}
rule cfg_edge_join_cons {
    if cfg_edge_join(blocks, stmt);
    if cons_stmt_block_list_node(blocks, head_block, tail_blocks);
    then cfg_edge_join(tail_blocks, stmt);
    then cfg_edge_stmts_stmt(head_block, stmt);
}

// ## Populating the cfg edge based on the AST

rule cfg_edge_if {
    if cons_stmt_list_node(_, first , tail);
    if if_stmt_node(first, _);
    if cons_stmt_list_node(tail, second , _);
    then cfg_edge(first, second);
}

rule cfg_edge_then {
    if cons_stmt_list_node(_, first , tail);
    if then_stmt_node(first, _);
    if cons_stmt_list_node(tail, second , _);
    then cfg_edge(first, second);
}

rule cfg_edge_branch_fork_blocks {
    if branch_stmt_node(branch_stmt, branch_blocks);
    then cfg_edge_fork(branch_stmt, branch_blocks);
}
rule cfg_edge_match_fork_blocks {
    if match_stmt_node(match_stmt, _, cases);
    if branch_blocks = desugared_case_block_list(cases);
    then cfg_edge_fork(match_stmt, branch_blocks);
}

rule cfg_edge_branch_join_blocks {
    if branch_stmt_node(branch_stmt, branch_blocks);
    if cons_stmt_list_node(_, branch_stmt , tail);
    if cons_stmt_list_node(tail, after_branch_stmt , _);
    then cfg_edge_join(branch_blocks, after_branch_stmt);
}
rule cfg_edge_match_join_blocks {
    if match_stmt_node(match_stmt, _, cases);
    if cons_stmt_list_node(_, match_stmt , tail);
    if cons_stmt_list_node(tail, after_match_stmt , _);
    if branch_blocks = desugared_case_block_list(cases);
    then cfg_edge_join(branch_blocks, after_match_stmt);
}

// ## The morphisms associated to statements.
//
// Each statement in a rule corresponds to a morphism of structures. The domain
// of this morphism corresponds to the data that has been queries or asserted
// earlier in the rule, and the codomain to the result of adjoining the data in
// that statement. Codomain and domain of subsequent statements match, so their
// morphisms are composable.

pred before_stmt_structure(StmtNode, Structure);
pred stmt_morphism(StmtNode, Morphism);

func before_rule_structure(RuleDeclNode) -> Structure;
rule before_rule_structure_total {
    if rn: RuleDeclNode;
    then before_rule_structure(rn)!;
}
rule before_first_rule_stmt {
    if rule_decl(rul, stmts);
    if cons_stmt_list_node(stmts, first, _);
    if structure = before_rule_structure(rul);
    then before_stmt_structure(first, structure);
}

rule cfg_edge_stmt_structure {
    if cfg_edge(from_stmt, to_stmt);
    if stmt_morphism(from_stmt, from_morphism);
    if from_cod = cod(from_morphism);
    then before_stmt_structure(to_stmt, from_cod);
}

func if_atom_morphism(IfAtomNode, before_structure: Structure) -> Morphism;
func then_atom_morphism(ThenAtomNode, before_structure: Structure) -> Morphism;
// This should only be defined for branch statements.
func branch_stmt_morphism(StmtNode, before_structure: Structure) -> Morphism;
// This should only be defined for match statements.
func match_stmt_morphism(StmtNode, before_structure: Structure) -> Morphism;

rule if_atom_morphism_dom {
    if morph_dom = dom(if_atom_morphism(_, before_structure));
    then morph_dom = before_structure;
}
rule then_atom_morphism_dom {
    if morph_dom = dom(then_atom_morphism(_, before_structure));
    then morph_dom = before_structure;
}
rule branch_stmt_morphism_dom {
    if morph_dom = dom(branch_stmt_morphism(_, before_structure));
    then morph_dom = before_structure;
}
rule match_stmt_morphism_dom {
    if morph_dom = dom(match_stmt_morphism(_, before_structure));
    then morph_dom = before_structure;
}

rule if_stmt_morphism_defined {
    if if_stmt_node(stmt, atom);
    if before_stmt_structure(stmt, before_structure);
    then morph := if_atom_morphism(atom, before_structure)!;
    then stmt_morphism(stmt, morph);
}
rule then_stmt_morphism_defined {
    if then_stmt_node(stmt, atom);
    if before_stmt_structure(stmt, before_structure);
    then morph := then_atom_morphism(atom, before_structure)!;
    then stmt_morphism(stmt, morph);
}
rule branch_stmt_morphism_defined {
    if branch_stmt_node(stmt, _);
    if before_stmt_structure(stmt, before_structure);
    then morph := branch_stmt_morphism(stmt, before_structure)!;
    then stmt_morphism(stmt, morph);
}
rule match_stmt_morphism_defined {
    if match_stmt_node(stmt, _, _);
    if before_stmt_structure(stmt, before_structure);
    then morph := match_stmt_morphism(stmt, before_structure)!;
    then stmt_morphism(stmt, morph);
}

pred if_morphism(Morphism);
pred surj_then_morphism(Morphism);
pred non_surj_then_morphism(Morphism);
pred noop_morphism(Morphism);

rule if_stmt_morphism_is_if {
    if if_stmt_node(stmt, _);
    if stmt_morphism(stmt, morph);
    then if_morphism(morph);
}
rule then_equal_stmt_morphism_is_surj {
    if then_stmt_node(stmt, atom);
    if equal_then_atom_node(atom, _, _);
    if stmt_morphism(stmt, morph);
    then surj_then_morphism(morph);
}
rule then_pred_stmt_morphism_is_surj {
    if then_stmt_node(stmt, atom);
    if pred_then_atom_node(atom, _, _);
    if stmt_morphism(stmt, morph);
    then surj_then_morphism(morph);
}
rule then_defined_stmt_morphism_is_non_surj {
    if then_stmt_node(stmt, atom);
    if defined_then_atom_node(atom, _, _);
    if stmt_morphism(stmt, morph);
    then non_surj_then_morphism(morph);
}
rule branch_stmt_morphism_is_noop {
    if branch_stmt_node(stmt, _);
    if stmt_morphism(stmt, morph);
    then noop_morphism(morph);
}
rule match_stmt_morphism_is_if {
    if match_stmt_node(stmt, _, _);
    if stmt_morphism(stmt, morph);
    then if_morphism(morph);
}

// ### Propagation of associated structures through the AST
//
// Even though a statement corresponds to a morphism, inside the statement we
// only need access to the codomain of that morphism. That's the
// stmt_structure, and similarly for subnodes of statements.
//
// #### Propagate stmt structure through if and then stmts.
pred stmt_structure(StmtNode, Structure);
pred if_atom_structure(IfAtomNode, Structure);
pred then_atom_structure(ThenAtomNode, Structure);
pred term_structure(TermNode, Structure);
pred terms_structure(TermListNode, Structure);
pred opt_term_structure(OptTermNode, Structure);

rule stmt_structure_morphism {
    if stmt_morphism(stmt, morph);
    if s = cod(morph);
    then stmt_structure(stmt, s);
}

rule if_stmt_structure {
    if if_stmt_node(stmt, atom);
    if stmt_structure(stmt, structure);
    then if_atom_structure(atom, structure);
}
rule then_stmt_structure {
    if then_stmt_node(stmt, atom);
    if stmt_structure(stmt, structure);
    then then_atom_structure(atom, structure);
}
rule match_stmt_structure {
    if match_stmt_node(stmt, term, _);
    if stmt_structure(stmt, structure);
    then term_structure(term, structure);
}

// #### Propagate associated structures through if atoms.
rule equal_if_atom_structure {
    if equal_if_atom_node(atom, lhs, rhs);
    if if_atom_structure(atom, structure);
    then term_structure(lhs, structure);
    then term_structure(rhs, structure);
}
rule defined_if_atom_structure {
    if defined_if_atom_node(atom, term);
    if if_atom_structure(atom, structure);
    then term_structure(term, structure);
}
rule pred_if_atom_structure {
    if pred_if_atom_node(atom, _, arg_terms);
    if if_atom_structure(atom, structure);
    then terms_structure(arg_terms, structure);
}
rule var_if_atom_structure {
    if var_if_atom_node(atom, var_term, _);
    if if_atom_structure(atom, structure);
    then term_structure(var_term, structure);
}

// #### Propagate associated structures through then atoms.
rule equal_then_atom_structure {
    if equal_then_atom_node(atom, lhs, rhs);
    if then_atom_structure(atom, structure);
    then term_structure(lhs, structure);
    then term_structure(rhs, structure);
}
rule defined_then_atom_structure {
    if defined_then_atom_node(atom, var_term, term);
    if then_atom_structure(atom, structure);
    then opt_term_structure(var_term, structure);
    then term_structure(term, structure);
}
rule pred_then_atom_structure {
    if pred_then_atom_node(atom, _, arg_terms);
    if then_atom_structure(atom, structure);
    then terms_structure(arg_terms, structure);
}

// #### Propagate associated structures through terms.
rule cons_term_list_structure {
    if cons_term_list_node(terms, head, tail);
    if terms_structure(terms, structure);
    then term_structure(head, structure);
    then terms_structure(tail, structure);
}

rule some_opt_term_structure {
    if some_term_node(opt_term, term);
    if opt_term_structure(opt_term, structure);
    then term_structure(term, structure);
}

rule app_term_structure {
    if app_term_node(term, _, args);
    if term_structure(term, structure);
    then terms_structure(args, structure);
}

// ### Populate associated structures

// #### Variables, scopes and named elements

func semantic_name(VirtIdent, Scope) -> ElName;

rule semantic_name_defined {
    if var_in_scope(ident, scope);
    then semantic_name(ident, scope)!;
}
rule semantic_name_extension_scope {
    if scope_extension(smaller_scope, larger_scope);
    if name_smaller = semantic_name(ident, smaller_scope);
    if name_larger = semantic_name(ident, larger_scope);
    then name_smaller = name_larger;
}

func semantic_el(TermNode, Structure) -> El;
func semantic_els(TermListNode, Structure) -> ElList;
rule semantic_el_defined {
    if el: TermNode;
    if term_structure(el, structure);
    then semantic_el(el, structure)!;
}

rule semantic_els_nil {
    if nil_term_list_node(terms);
    if terms_structure(terms, structure);
    then nil_els := NilElList(structure)!;
    then semantic_els(terms, structure) = nil_els;
}
rule semantic_els_cons {
    if cons_term_list_node(terms, head, tail);
    if head_el = semantic_el(head, structure);
    if tail_els = semantic_els(tail, structure);
    then cons_els := ConsElList(head_el, tail_els)!;
    then semantic_els(terms, structure) = cons_els;
}

// #### The structures of semantic elements
rule semantic_el_struct {
    if el = semantic_el(_, structure);
    then el_structure(el) = structure;
}
rule semantic_els_struct {
    if els = semantic_els(_, structure);
    then els_structure(els) = structure;
}

// #### Semantics of terms
rule app_term_semantics {
    if app_term_node(result_term, func_name, arg_terms);
    if result_el = semantic_el(result_term, structure);
    if func_arg_els = semantic_els(arg_terms, structure);
    if func_rel = FuncRel(semantic_func(func_name));
    then rel_arg_els := SnocElList(func_arg_els, result_el)!;
    then rel_app(func_rel, rel_arg_els);
}

rule var_term_semantics {
    if var_term_node(term, ident);
    if scope = exit_scope(rule_descendant_term(term));
    if name = semantic_name(ident, scope);
    if el = semantic_el(term, structure);
    then el = var(structure, name);
}

func wildcard_name(TermNode) -> ElName;
rule wildcard_name_defined {
    if wildcard_term_node(term);
    then wildcard_name(term)!;
}
rule wildcard_term_semantics {
    if wildcard_term_node(term);
    if name = wildcard_name(term);
    if el = semantic_el(term, structure);
    then el = var(structure, name);
}

// #### Semantics of if atoms
rule equal_if_atom_semantics {
    if equal_if_atom_node(_, lhs_term, rhs_term);
    if lhs_el = semantic_el(lhs_term, structure);
    if rhs_el = semantic_el(rhs_term, structure);
    then lhs_el = rhs_el;
}
// No rule for `defined_if_atom` -- this is already taken care of because `semantic_el` is total.
rule pred_if_atom_semantics {
    if pred_if_atom_node(_, predicate_name, arg_terms);
    if rel = PredRel(semantic_pred(predicate_name));
    if arg_els = semantic_els(arg_terms, _);
    then rel_app(rel, arg_els);
}
rule var_if_atom_semantics {
    if var_if_atom_node(_, var_term, type_name);
    if typ = semantic_type(type_name);
    if var_el = semantic_el(var_term, _);
    then el_type(var_el, typ);
}

// #### Semantics of then atoms
rule equal_then_atom_semantics {
    if equal_then_atom_node(_, lhs_term, rhs_term);
    if lhs_el = semantic_el(lhs_term, structure);
    if rhs_el = semantic_el(rhs_term, structure);
    then lhs_el = rhs_el;
}
rule defined_then_atom_semantics {
    if defined_then_atom_node(_, opt_var_term, term);
    if some_term_node(opt_var_term, var_term);
    if var_el = semantic_el(var_term, structure);
    if el = semantic_el(term, structure);
    then var_el = el;
}
rule pred_then_atom_semantics {
    if pred_then_atom_node(_, predicate_name, arg_terms);
    if rel = PredRel(semantic_pred(predicate_name));
    if arg_els = semantic_els(arg_terms, _);
    then rel_app(rel, arg_els);
}

// ## Epic check

// ### Terms that should need epic checking
//
// These are terms that appear in then statements.

pred term_should_be_epic_ok(TermNode);
pred terms_should_be_epic_ok(TermListNode);

// #### Propagate should_be_epic_ok downwards.
rule terms_should_be_epic_ok_cons {
    if terms_should_be_epic_ok(terms);
    if cons_term_list_node(terms, head, tail);
    then term_should_be_epic_ok(head);
    then terms_should_be_epic_ok(tail);
}

rule terms_should_be_epic_ok_app {
    if term_should_be_epic_ok(tm);
    if app_term_node(tm, _, args);
    then terms_should_be_epic_ok(args);
}

rule then_atom_epic_ok_equal {
    if equal_then_atom_node(_, lhs, rhs);
    then term_should_be_epic_ok(lhs);
    then term_should_be_epic_ok(rhs);
}
rule then_atom_epic_ok_defined {
    if defined_then_atom_node(_, _, tm);
    then term_should_be_epic_ok(tm);
}
rule then_atom_epic_ok_pred {
    if pred_then_atom_node(_, _, args);
    then terms_should_be_epic_ok(args);
}

// ## Surjectivity check
//
// Since the morphisms we derive from statements are such that no two morphisms
// share a codomain, we don't need to reference a morphism in the surjectivity
// check.

pred el_should_be_surjective_ok(El);
pred el_is_surjective_ok(El);

rule surjective_codomain_should_be_ok {
    if surj_then_morphism(morph);
    if el_structure(el) = cod(morph);
    then el_should_be_surjective_ok(el);
}
rule non_surjective_codomain_should_be_ok {
    if non_surj_then_morphism(morph);
    if el_structure(el) = cod(morph);
    then el_should_be_surjective_ok(el);
}

rule surjective_img_el_is_ok {
    if el_should_be_surjective_ok(el);
    if el_in_img(_, el);
    then el_is_surjective_ok(el);
}
rule surjective_exempted_then_defined_term {
    if defined_then_atom_node(_, _, tm);
    if el = semantic_el(tm, _);
    then el_is_surjective_ok(el);
}


// ## Enum constructor surjectivity check
pred should_be_obtained_by_ctor(TermNode, EnumDeclNode);
rule defined_then_should_be_given_by_ctor {
    if defined_then_atom_node(_, _, tm);
    if el = semantic_el(tm, _);
    if el_type(el, semantic_type(ty_name));
    if enum_decl(enum_decl_node, ty_name, _);
    then should_be_obtained_by_ctor(tm, enum_decl_node);
}

pred is_given_by_ctor(TermNode, EnumDeclNode);

rule ctor_app_is_given_by_ctor {
    if app_term_node(tm, func_ident, _);
    if ctor_decl(ctor, func_ident, _);
    if ctor_enum(ctor) = enum_decl_node;
    then is_given_by_ctor(tm, enum_decl_node);
}

// ### Function definedness
//
// This predicate holds if an Eqlog function can be made defined via the Rust API.
pred function_can_be_made_defined(Func);

rule function_can_be_made_defined_if_codomain_normal_type {
    if type_decl(_, ident);
    if ty = semantic_type(ident);
    if codomain(function) = ty;
    then function_can_be_made_defined(function);
}
rule function_can_be_defined_if_constructor {
    if ctor_decl(_, ident, _);
    if function = semantic_func(ident);
    then function_can_be_made_defined(function);
}

// ## Match statement exhaustiveness check
//
// ### Checking that the pattern of every match case is a valid enum constructor.

pred case_pattern_is_variable(Loc);
pred case_pattern_is_wildcard(Loc);
rule case_pattern_is_variable_defined {
    if match_case(_, pattern, _);
    if var_term_node(pattern, _);
    if pattern_loc = term_node_loc(pattern);
    then case_pattern_is_variable(pattern_loc);
}
rule case_pattern_is_wildcard_defined {
    if match_case(_, pattern, _);
    if wildcard_term_node(pattern);
    if pattern_loc = term_node_loc(pattern);
    then case_pattern_is_wildcard(pattern_loc);
}

// The constructor of the pattern of a match case, if any, i.e. if the pattern
// term is a valid enum constructor.
func match_case_pattern_ctor(MatchCaseNode) -> CtorDeclNode;
rule case_pattern_app_should_be_constructor {
    if match_case(_, pattern, _);
    if app_term_node(pattern, func_name, _);
    if pattern_loc = term_node_loc(pattern);
    if ctor_sym = ctor_symbol();
    then should_be_symbol(func_name, ctor_sym, pattern_loc);
}
rule match_case_pattern_ctor_defined {
    if match_case(case_node, pattern, _);
    if app_term_node(pattern, func_name, _);
    if ctor_decl(ctor, func_name, _);
    then match_case_pattern_ctor(case_node) = ctor;
}

// ### Checking of constructor arguments in patterns
pred is_pattern_ctor_arg(TermNode);
pred are_pattern_ctor_args(TermListNode);
rule is_pattern_ctor_arg_cons {
    if are_pattern_ctor_args(tms);
    if cons_term_list_node(tms, head, tail);
    then is_pattern_ctor_arg(head);
    then are_pattern_ctor_args(tail);
}

rule are_pattern_ctor_args_defined {
    if match_case(_, pattern, _);
    if app_term_node(pattern, _, args);
    then are_pattern_ctor_args(args);
}

pred pattern_ctor_arg_is_app(Loc);
rule pattern_ctor_arg_is_app_defined {
    if is_pattern_ctor_arg(arg);
    if app_term_node(arg, _, _);
    if loc = term_node_loc(arg);
    then pattern_ctor_arg_is_app(loc);
}

pred pattern_ctor_arg_var_is_not_fresh(Loc);
rule pattern_ctor_arg_var_is_not_fresh_defined {
    if is_pattern_ctor_arg(arg);
    if var_term_node(arg, ident);
    if scope = entry_scope(rule_descendant_term(arg));
    if var_in_scope(ident, scope);
    if loc = term_node_loc(arg);
    then pattern_ctor_arg_var_is_not_fresh(loc);
}

// ### Which constructors occur in a case list, and if they determine the enum type uniquely

pred cases_contain_ctor(MatchCaseListNode, CtorDeclNode);
rule contains_ctor_case_head {
    if cons_match_case_list_node(cases, head_case, _);
    if ctor = match_case_pattern_ctor(head_case);
    then cases_contain_ctor(cases, ctor);
}
rule contains_ctor_case_tail {
    if cons_match_case_list_node(cases, _, tail_cases);
    if cases_contain_ctor(tail_cases, ctor);
    then cases_contain_ctor(cases, ctor);
}

pred match_stmt_contains_ctor_of_enum(StmtNode, CtorDeclNode, EnumDeclNode);
rule match_stmt_contains_ctor_of_enum_defined {
    if match_stmt_node(stmt, _, cases);
    if cases_contain_ctor(cases, ctor);
    if ctor_enum(ctor) = enum_decl_node;
    then match_stmt_contains_ctor_of_enum(stmt, ctor, enum_decl_node);
}

func cases_determined_enum(MatchCaseListNode) -> EnumDeclNode;
rule ctor_cases_determine_enum_singleton {
    if cons_match_case_list_node(cases, head_case, tail_cases);
    if nil_match_case_list_node(tail_cases);
    if enum_type = ctor_enum(match_case_pattern_ctor(head_case));
    then cases_determined_enum(cases) = enum_type;
}
rule ctor_cases_determine_enum_cons {
    if cons_match_case_list_node(cases, head_case, tail_cases);
    if enum_type = cases_determined_enum(tail_cases);
    if enum_type = ctor_enum(match_case_pattern_ctor(head_case));
    then cases_determined_enum(cases) = enum_type;
}

rule match_term_type_if_cases_determine_enum {
    if match_stmt_node(_, match_term, cases);
    if enum_decl_node = cases_determined_enum(cases);
    if enum_decl(enum_decl_node, ident, _);
    if enum_type = semantic_type(ident);
    if match_el = semantic_el(match_term, _);
    then el_type(match_el, enum_type);
}

// ## Exhaustiveness of case lists in match statement

pred match_stmt_should_contain_ctor(StmtNode, CtorDeclNode);
rule match_stmt_should_contain_ctor_defined {
    if match_stmt_node(stmt, match_term, _);
    if el_type(semantic_el(match_term, _), enum_type);
    if semantic_type(enum_ident) = enum_type;
    if enum_decl(enum_decl_node, enum_ident, _);
    if ctor_enum(ctor) = enum_decl_node;
    then match_stmt_should_contain_ctor(stmt, ctor);
}

pred match_stmt_contains_ctor(StmtNode, CtorDeclNode);
rule match_stmt_contains_ctor_defined {
    if match_stmt_node(stmt, _, cases);
    if cases_contain_ctor(cases, ctor);
    then match_stmt_contains_ctor(stmt, ctor);
}