Theory Rhombus_HOL_Code_Export

(* SPDX-License-Identifier: 0BSD *)
(* Original code-export equations and Rhombus target configuration. *)

theory Rhombus_HOL_Code_Export
  imports Rhombus_HOL_Code_API "HOL-Library.Code_Target_Numeral"
begin

ML_file "Rhombus_HOL_Code_Target.ML"

section ‹Executable natural-fuel matcher›

definition empty_type_subst :: "hname ⇒ htype option" where
  "empty_type_subst _ = None"

lemma empty_type_subst_eq [simp]: "empty_type_subst = (λ_. None)"
  by (rule ext) (simp add: empty_type_subst_def)

section ‹Single-pass checking with type computation›

text ‹The specification checks both children of every application and then traverses
  the same subtree again through @{const type_of}. Fuse validation and type
  computation for executable code while leaving the trusted specification unchanged.›

fun check_term_type :: "htheory ⇒ htype list ⇒ hterm ⇒ htype option" where
  "check_term_type thy env (FVar _ ty) =
     (if check_type thy ty then Some ty else None)"
| "check_term_type thy env (BVar i ty) =
     (if i < length env ∧ env ! i = ty ∧ check_type thy ty then Some ty else None)"
| "check_term_type thy env (Const n ty) =
     (if check_type thy ty ∧
         (case const_tab thy n of None ⇒ False
          | Some generic ⇒ type_match generic ty empty_type_subst ≠ None)
      then Some ty else None)"
| "check_term_type thy env (NatLit _) =
     (if check_type thy nat_aty ∧ check_type thy nat_sty ∧
         const_tab thy nat_zero_name = Some nat_aty ∧
         const_tab thy nat_succ_name = Some nat_sty
      then Some nat_aty else None)"
| "check_term_type thy env (Comb f x) =
     (case (check_term_type thy env f, check_term_type thy env x) of
        (Some (TyApp NFun [dty, rty]), Some aty) ⇒
          (if dty = aty then Some rty else None)
      | _ ⇒ None)"
| "check_term_type thy env (Abs aty body) =
     (if check_type thy aty
      then map_option (mk_fun aty) (check_term_type thy (aty # env) body)
      else None)"

lemma check_open_term_type_of:
  "check_open_term thy env t ⟹ type_of t ≠ None"
  by (induction t arbitrary: env) auto

lemma check_term_type_eq:
  "check_term_type thy env t = (if check_open_term thy env t then type_of t else None)"
proof (induction t arbitrary: env)
  case (Comb f x)
  show ?case
    using Comb.IH(1)[of env] Comb.IH(2)[of env] check_open_term_type_of
    by (auto split: option.splits htype.splits list.splits hname.splits)
next
  case (Abs aty body)
  show ?case
    using Abs.IH[of "aty # env"] by auto
next
  case (Const n ty)
  show ?case
    by (simp add: empty_type_subst_def split: option.splits)
qed simp_all

definition type_match_uncached ::
  "htype ⇒ htype ⇒ (hname ⇒ htype option) ⇒ (hname ⇒ htype option) option" where
  "type_match_uncached pat ty acc =
    (case type_match_fuel (size pat + 1) pat ty acc of
       None ⇒ None
     | Some θ ⇒ if type_subst θ pat = ty then Some θ else None)"

lemma type_match_uncached_eq: "type_match_uncached = type_match"
  by (simp add: fun_eq_iff type_match_uncached_def type_match_def)

definition memoize_ternary ::
  "('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ 'a ⇒ 'b ⇒ 'c ⇒ 'd" where
  "memoize_ternary f a b c = f a b c"

text ‹One memo table on the fused checker lets shared subterms retain the
  single-pass checker while making every public check a cached projection.
  Recursive calls deliberately go through the memoized constant.›

definition check_term_type_uncached ::
  "htheory ⇒ hterm ⇒ htype list ⇒ htype option" where
  "check_term_type_uncached thy t env =
    (case t of
       FVar _ ty ⇒ (if check_type thy ty then Some ty else None)
     | BVar i ty ⇒
         (if i < length env ∧ env ! i = ty ∧ check_type thy ty then Some ty else None)
     | Const n ty ⇒
         (if check_type thy ty ∧
             (case const_tab thy n of None ⇒ False
              | Some generic ⇒ type_match generic ty empty_type_subst ≠ None)
          then Some ty else None)
     | NatLit _ ⇒
         (if check_type thy nat_aty ∧ check_type thy nat_sty ∧
             const_tab thy nat_zero_name = Some nat_aty ∧
             const_tab thy nat_succ_name = Some nat_sty
          then Some nat_aty else None)
     | Comb f x ⇒
         (case (check_term_type thy env f, check_term_type thy env x) of
            (Some (TyApp NFun [dty, rty]), Some aty) ⇒
              (if dty = aty then Some rty else None)
          | _ ⇒ None)
     | Abs aty body ⇒
         (if check_type thy aty
          then map_option (mk_fun aty) (check_term_type thy (aty # env) body)
          else None))"

lemma check_term_type_uncached_eq:
  "check_term_type_uncached thy t env = check_term_type thy env t"
  by (cases t) (simp_all add: check_term_type_uncached_def)

declare [[code drop: check_term_type]]
declare [[code drop: check_open_term]]
declare [[code drop: type_match]]
declare [[code drop: check_term]]
declare [[code drop: check_prop]]

lemma check_term_type_memo_code [code]:
  "check_term_type thy env t =
    memoize_ternary check_term_type_uncached thy t env"
  by (simp add: memoize_ternary_def check_term_type_uncached_eq)

lemma check_open_term_code [code]:
  "check_open_term thy env t ⟷ check_term_type thy env t ≠ None"
  by (auto simp: check_term_type_eq dest: check_open_term_type_of)

lemma check_term_code [code]:
  "check_term thy t ⟷ check_term_type thy [] t ≠ None"
  by (auto simp: check_term_def check_term_type_eq dest: check_open_term_type_of)

lemma check_prop_code [code]:
  "check_prop thy p ⟷ check_term_type thy [] p = Some bool_ty"
  by (auto simp: check_prop_def check_term_def is_bool_def check_term_type_eq)

lemma type_match_memo_code [code]:
  "type_match pat ty acc =
    memoize_ternary type_match_uncached pat ty acc"
  by (simp add: memoize_ternary_def type_match_uncached_eq)

declare [[code drop: type_match_fuel]]

lemma type_match_fuel_code [code]:
  "type_match_fuel fuel pat ty acc =
    (if fuel = 0 then None
     else case pat of
       TyVar n ⇒
         (case acc n of None ⇒ Some (acc(n := Some ty))
          | Some old ⇒ if old = ty then Some acc else None)
     | TyApp n ps ⇒
         (case ty of TyVar _ ⇒ None
          | TyApp m ts ⇒
              if n = m ∧ length ps = length ts then
                fold (λ(p, t) result.
                  case result of None ⇒ None
                  | Some current ⇒ type_match_fuel (fuel - 1) p t current)
                  (zip ps ts) (Some acc)
              else None))"
  by (cases fuel; cases pat; cases ty) auto

definition nat_value :: "integer ⇒ nat" where
  "nat_value k = nat_of_integer k"

definition integer_value :: "nat ⇒ integer" where
  "integer_value n = integer_of_nat n"
section ‹Rhombus integer primitives›

code_printing
  type_constructor integer ⇀ (Rhombus) "Int"
| constant "0 :: integer" ⇀ (Rhombus) "0"
| constant "plus :: integer ⇒ integer ⇒ integer" ⇀ (Rhombus) infixl 6 "+"
| constant "uminus :: integer ⇒ integer" ⇀ (Rhombus) "(- _)"
| constant "minus :: integer ⇒ integer ⇒ integer" ⇀ (Rhombus) infixl 6 "-"
| constant "times :: integer ⇒ integer ⇒ integer" ⇀ (Rhombus) infixl 7 "*"
| constant "HOL.equal :: integer ⇒ integer ⇒ bool" ⇀ (Rhombus) infix 4 "=="
| constant "less_eq :: integer ⇒ integer ⇒ bool" ⇀ (Rhombus) infix 4 "<="
| constant "less :: integer ⇒ integer ⇒ bool" ⇀ (Rhombus) infix 4 "<"
| constant "abs :: integer ⇒ integer" ⇀ (Rhombus) "abs(_)"

setup ‹
  Numeral.add_code @{const_name Code_Numeral.Pos} I
    Code_Printer.literal_numeral "Rhombus"
  #> Numeral.add_code @{const_name Code_Numeral.Neg} (~)
    Code_Printer.literal_numeral "Rhombus"
›

section ‹Native mapped equality›

code_printing
  constant "HOL.equal :: hname ⇒ hname ⇒ bool" ⇀ (Rhombus) "abi.structural'_equal"
| constant "HOL.equal :: htype ⇒ htype ⇒ bool" ⇀ (Rhombus) "abi.structural'_equal"
| constant "HOL.equal :: hterm ⇒ hterm ⇒ bool" ⇀ (Rhombus) "abi.structural'_equal"
| constant "HOL.equal :: nat ⇒ nat ⇒ bool" ⇀ (Rhombus) "abi.structural'_equal"

section ‹Weak memoization for generated checkers›

text ‹The generated checker revisits immutable theories, terms, types, and small
  environments across inference results. Weak identity tables partition caches by
  the live computation roots; the innermost table uses structural keys. Since
  @{const memoize_ternary} is the identity in HOL, this changes only executable
  sharing, not logical meaning.›

code_printing
  code_module Rhombus_Memo ⇀ (Rhombus) ‹
class RhombusMemoValue(value)

def rhombus_ternary_memos = WeakMutableMap.by(===)()

fun rhombus_memoized_ternary(run):
  fun (first):
    fun (second):
      fun (third):
        let firsts:
          match rhombus_ternary_memos.maybe[run]
          | #false:
              let table = WeakMutableMap.by(===)()
              rhombus_ternary_memos[run] := table
              table
          | table: table
        let seconds:
          match firsts.maybe[first]
          | #false:
              let table = WeakMutableMap.by(===)()
              firsts[first] := table
              table
          | table: table
        let thirds:
          match seconds.maybe[second]
          | #false:
              let table = MutableMap()
              seconds[second] := table
              table
          | table: table
        match thirds.maybe[third]
        | #false:
            let result = (((run)(first))(second))(third)
            thirds[third] := RhombusMemoValue(result)
            result
        | RhombusMemoValue(result): result
› for constant memoize_ternary
| constant memoize_ternary ⇀ (Rhombus) "rhombus'_memoized'_ternary"

section ‹Stable Rhombus API names›

code_identifier
  type_constructor stamp_ext ⇀ (Rhombus) "Rhombus_HOL_Generated.Stamp"
| type_constructor hthm_ext ⇀ (Rhombus) "Rhombus_HOL_Generated.HThm"
| type_constructor htheory_ext ⇀ (Rhombus) "Rhombus_HOL_Generated.HTheory"
| type_constructor code_failure ⇀ (Rhombus) "Rhombus_HOL_Generated.FailureCode"
| type_constructor code_result ⇀ (Rhombus) "Rhombus_HOL_Generated.Result"
| constant check_term_type_uncached ⇀ (Rhombus) "Rhombus_HOL_Generated.check_term_type_uncached"
| constant type_match_uncached ⇀ (Rhombus) "Rhombus_HOL_Generated.type_match_uncached"
| constant CodeUndeclaredType ⇀ (Rhombus) "Rhombus_HOL_Generated.UndeclaredType"
| constant CodeTypeArity ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeArity"
| constant CodeInvalidType ⇀ (Rhombus) "Rhombus_HOL_Generated.InvalidType"
| constant CodeUnboundIndex ⇀ (Rhombus) "Rhombus_HOL_Generated.UnboundIndex"
| constant CodeBinderTypeMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.BinderTypeMismatch"
| constant CodeUndeclaredConstant ⇀ (Rhombus) "Rhombus_HOL_Generated.UndeclaredConstant"
| constant CodeConstantTypeMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.ConstantTypeMismatch"
| constant CodeOperatorNotFunction ⇀ (Rhombus) "Rhombus_HOL_Generated.OperatorNotFunction"
| constant CodeIllTypedApplication ⇀ (Rhombus) "Rhombus_HOL_Generated.IllTypedApplication"
| constant CodeNotProposition ⇀ (Rhombus) "Rhombus_HOL_Generated.NotProposition"
| constant CodeNotEquation ⇀ (Rhombus) "Rhombus_HOL_Generated.NotEquation"
| constant CodeMiddleTermsDiffer ⇀ (Rhombus) "Rhombus_HOL_Generated.MiddleTermsDiffer"
| constant CodeCombinationTypeMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.CombinationTypeMismatch"
| constant CodeVariableFreeInHypotheses ⇀ (Rhombus) "Rhombus_HOL_Generated.VariableFreeInHypotheses"
| constant CodeNotBetaRedex ⇀ (Rhombus) "Rhombus_HOL_Generated.NotBetaRedex"
| constant CodeAntecedentMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.AntecedentMismatch"
| constant CodeInvalidInstantiationTarget ⇀ (Rhombus) "Rhombus_HOL_Generated.InvalidInstantiationTarget"
| constant CodeInstantiationTypeMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.InstantiationTypeMismatch"
| constant CodeInvalidTypeSubstitution ⇀ (Rhombus) "Rhombus_HOL_Generated.InvalidTypeSubstitution"
| constant CodeDuplicateType ⇀ (Rhombus) "Rhombus_HOL_Generated.DuplicateType"
| constant CodeDuplicateConstant ⇀ (Rhombus) "Rhombus_HOL_Generated.DuplicateConstant"
| constant CodeDefinitionNotEquation ⇀ (Rhombus) "Rhombus_HOL_Generated.DefinitionNotEquation"
| constant CodeDefinitionLeftNotVariable ⇀ (Rhombus) "Rhombus_HOL_Generated.DefinitionLeftNotVariable"
| constant CodeDefinitionOpen ⇀ (Rhombus) "Rhombus_HOL_Generated.DefinitionOpen"
| constant CodeDefinitionTypeMismatch ⇀ (Rhombus) "Rhombus_HOL_Generated.DefinitionTypeMismatch"
| constant CodeDefinitionExtraTypeVariables ⇀ (Rhombus) "Rhombus_HOL_Generated.DefinitionExtraTypeVariables"
| constant CodeTypeDefinitionSameConstants ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeDefinitionSameConstants"
| constant CodeTypeDefinitionHasHypotheses ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeDefinitionHasHypotheses"
| constant CodeTypeDefinitionOpenPredicate ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeDefinitionOpenPredicate"
| constant CodeTypeDefinitionExtraTypeVariables ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeDefinitionExtraTypeVariables"
| constant CodeTypeDefinitionBadWitness ⇀ (Rhombus) "Rhombus_HOL_Generated.TypeDefinitionBadWitness"
| constant CodeRuleRejected ⇀ (Rhombus) "Rhombus_HOL_Generated.RuleRejected"
| constant CodeExtensionRejected ⇀ (Rhombus) "Rhombus_HOL_Generated.ExtensionRejected"
| constant CodeSuccess ⇀ (Rhombus) "Rhombus_HOL_Generated.Success"
| constant CodeFailure ⇀ (Rhombus) "Rhombus_HOL_Generated.Failure"
| constant code_check_type ⇀ (Rhombus) "Rhombus_HOL_Generated.check_type_result"
| constant code_check_term ⇀ (Rhombus) "Rhombus_HOL_Generated.check_term_result"
| constant code_refl ⇀ (Rhombus) "Rhombus_HOL_Generated.refl"
| constant code_trans ⇀ (Rhombus) "Rhombus_HOL_Generated.trans"
| constant code_mk_comb ⇀ (Rhombus) "Rhombus_HOL_Generated.mk_comb"
| constant code_abs ⇀ (Rhombus) "Rhombus_HOL_Generated.abs"
| constant code_beta ⇀ (Rhombus) "Rhombus_HOL_Generated.beta"
| constant code_assume ⇀ (Rhombus) "Rhombus_HOL_Generated.assume"
| constant code_eq_mp ⇀ (Rhombus) "Rhombus_HOL_Generated.eq_mp"
| constant code_deduct_antisym ⇀ (Rhombus) "Rhombus_HOL_Generated.deduct_antisym"
| constant code_inst ⇀ (Rhombus) "Rhombus_HOL_Generated.inst"
| constant code_inst_type ⇀ (Rhombus) "Rhombus_HOL_Generated.inst_type"
| constant code_nat_lit_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_conv"
| constant code_nat_lit_eq_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_eq_conv"
| constant code_nat_lit_add_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_add_conv"
| constant code_nat_lit_mul_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_mul_conv"
| constant code_nat_lit_le_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_le_conv"
| constant code_nat_lit_sub_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_sub_conv"
| constant code_nat_lit_pow_conv ⇀ (Rhombus) "Rhombus_HOL_Generated.nat_lit_pow_conv"
| constant code_new_type ⇀ (Rhombus) "Rhombus_HOL_Generated.new_type"
| constant code_new_nat_type ⇀ (Rhombus) "Rhombus_HOL_Generated.new_nat_type"
| constant code_new_constant ⇀ (Rhombus) "Rhombus_HOL_Generated.new_constant"
| constant code_new_axiom ⇀ (Rhombus) "Rhombus_HOL_Generated.new_axiom"
| constant code_new_basic_definition ⇀ (Rhombus) "Rhombus_HOL_Generated.new_basic_definition"
| constant code_new_basic_type_definition ⇀ (Rhombus) "Rhombus_HOL_Generated.new_basic_type_definition"
| constant Pair ⇀ (Rhombus) "Rhombus_HOL_Generated.PairValue"
section ‹Generated Rhombus module›

export_code CodeUndeclaredType CodeTypeArity CodeInvalidType CodeUnboundIndex
  CodeBinderTypeMismatch CodeUndeclaredConstant CodeConstantTypeMismatch
  CodeOperatorNotFunction CodeIllTypedApplication CodeNotProposition CodeNotEquation
  CodeMiddleTermsDiffer CodeCombinationTypeMismatch CodeVariableFreeInHypotheses
  CodeNotBetaRedex CodeAntecedentMismatch CodeInvalidInstantiationTarget
  CodeInstantiationTypeMismatch CodeInvalidTypeSubstitution CodeDuplicateType
  CodeDuplicateConstant CodeDefinitionNotEquation CodeDefinitionLeftNotVariable
  CodeDefinitionOpen CodeDefinitionTypeMismatch CodeDefinitionExtraTypeVariables
  CodeTypeDefinitionSameConstants CodeTypeDefinitionHasHypotheses
  CodeTypeDefinitionOpenPredicate CodeTypeDefinitionExtraTypeVariables
  CodeTypeDefinitionBadWitness CodeRuleRejected CodeExtensionRejected
  CodeSuccess CodeFailure Pair None Some
  code_check_type code_check_term
  code_refl code_trans code_mk_comb code_abs code_beta code_assume code_eq_mp
  code_deduct_antisym code_inst code_inst_type
  code_nat_lit_conv code_nat_lit_eq_conv code_nat_lit_add_conv code_nat_lit_mul_conv
  code_nat_lit_le_conv code_nat_lit_sub_conv code_nat_lit_pow_conv code_new_nat_type code_new_type code_new_constant code_new_axiom
  code_new_basic_definition code_new_basic_type_definition
  initial_theory check_type check_open_term check_term is_bool mk_eq dest_eq
  sid gen ancestors hyps concl thm_stamp tyops const_tab axiom_list def_tab thy_stamp
  in Rhombus module_name Rhombus_HOL_Generated file_prefix rhombus_hol_kernel

export_code CodeUndeclaredType CodeTypeArity CodeInvalidType CodeUnboundIndex
  CodeBinderTypeMismatch CodeUndeclaredConstant CodeConstantTypeMismatch
  CodeOperatorNotFunction CodeIllTypedApplication CodeNotProposition CodeNotEquation
  CodeMiddleTermsDiffer CodeCombinationTypeMismatch CodeVariableFreeInHypotheses
  CodeNotBetaRedex CodeAntecedentMismatch CodeInvalidInstantiationTarget
  CodeInstantiationTypeMismatch CodeInvalidTypeSubstitution CodeDuplicateType
  CodeDuplicateConstant CodeDefinitionNotEquation CodeDefinitionLeftNotVariable
  CodeDefinitionOpen CodeDefinitionTypeMismatch CodeDefinitionExtraTypeVariables
  CodeTypeDefinitionSameConstants CodeTypeDefinitionHasHypotheses
  CodeTypeDefinitionOpenPredicate CodeTypeDefinitionExtraTypeVariables
  CodeTypeDefinitionBadWitness CodeRuleRejected CodeExtensionRejected
  CodeSuccess CodeFailure Pair None Some
  code_check_type code_check_term
  code_refl code_trans code_mk_comb code_abs code_beta code_assume code_eq_mp
  code_nat_lit_conv code_nat_lit_eq_conv code_nat_lit_add_conv code_nat_lit_mul_conv
  code_nat_lit_le_conv code_nat_lit_sub_conv code_nat_lit_pow_conv code_new_nat_type code_new_type code_new_constant code_new_axiom
  code_new_basic_definition code_new_basic_type_definition
  initial_theory check_type check_open_term check_term is_bool mk_eq dest_eq
  sid gen ancestors hyps concl thm_stamp tyops const_tab axiom_list def_tab thy_stamp
  checking Rhombus

end