Struct Runtime 

pub struct Runtime {
    pub module_manager: ModuleManager,
    pub environment_stack: Vec<Box<Environment>>,
    pub parsing_free_param_collection: FreeParamCollection,
}

Fields

module_manager: ModuleManager

environment_stack: Vec<Box<Environment>>

parsing_free_param_collection: FreeParamCollection

Implementations

impl Runtime

pub fn exec_by_fn_stmt( &mut self, stmt: &ByFnAsSetStmt, ) -> Result<StmtResult, RuntimeError>

pub fn exec_by_fn_set_stmt( &mut self, stmt: &ByFnSetAsSetStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_cases_stmt( &mut self, stmt: &ByCasesStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_closed_range_as_cases_stmt( &mut self, stmt: &ByClosedRangeAsCasesStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_commutative_prop_stmt( &mut self, stmt: &ByCommutativePropStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_contra_stmt( &mut self, stmt: &ByContraStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_enumerate_finite_set_stmt( &mut self, stmt: &ByEnumerateFiniteSetStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_extension_stmt( &mut self, stmt: &ByExtensionStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_family_stmt( &mut self, stmt: &ByFamilyAsSetStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_for_stmt( &mut self, stmt: &ByForStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_induc_stmt( &mut self, stmt: &ByInducStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_transitive_prop_stmt( &mut self, stmt: &ByTransitivePropStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_by_tuple_stmt( &mut self, stmt: &ByTupleAsSetStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_claim_stmt( &mut self, stmt: &ClaimStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_def_abstract_prop_stmt( &mut self, def_abstract_prop_stmt: &DefAbstractPropStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_def_algo_stmt( &mut self, def_algo_stmt: &DefAlgoStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_def_prop_stmt( &mut self, def_prop_stmt: &DefPropStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_def_struct_stmt( &mut self, def_struct_stmt: &DefStructStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn define_params_with_set( &mut self, param_def: &ParamGroupWithSet, ) -> Result<InferResult, RuntimeError>

pub fn define_params_with_set_in_scope( &mut self, param_def: &ParamGroupWithSet, binding_scope: ParamObjType, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn exec_eval_stmt( &mut self, stmt: &EvalStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_fact(&mut self, fact: &Fact) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_def_family_stmt( &mut self, def_family_stmt: &DefFamilyStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_exist_obj_stmt( &mut self, have_exist_obj_stmt: &HaveByExistStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_fn_by_forall_exist_unique_stmt( &mut self, stmt: &HaveFnByForallExistUniqueStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_fn_by_induc( &mut self, stmt: &HaveFnByInducStmt, ) -> Result<StmtResult, RuntimeError>

pub fn exec_have_fn_by_induc_stmt( &mut self, stmt: &HaveFnByInducStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_fn_equal_case_by_case_stmt( &mut self, have_fn_equal_case_by_case_stmt: &HaveFnEqualCaseByCaseStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_fn_equal_stmt( &mut self, have_fn_equal_stmt: &HaveFnEqualStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_obj_equal_stmt( &mut self, have_obj_equal_stmt: &HaveObjEqualStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_have_obj_in_nonempty_set_or_param_type_stmt( &mut self, stmt: &HaveObjInNonemptySetOrParamTypeStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_know_stmt( &mut self, know_stmt: &KnowStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_let_stmt( &mut self, def_let_stmt: &DefLetStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_prove_stmt( &mut self, stmt: &ProveStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn exec_stmt(&mut self, stmt: &Stmt) -> Result<StmtResult, RuntimeError>

pub fn stmt_unsupported(stmt: Stmt) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn store_def_prop( &mut self, def_prop_stmt: &DefPropStmt, ) -> Result<(), RuntimeError>

pub fn store_def_abstract_prop( &mut self, def_abstract_prop_stmt: &DefAbstractPropStmt, ) -> Result<(), RuntimeError>

pub fn store_def_algo( &mut self, def_algo_stmt: &DefAlgoStmt, ) -> Result<(), RuntimeError>

pub fn store_def_struct( &mut self, def_struct_stmt: &DefStructStmt, ) -> Result<(), RuntimeError>

pub fn store_free_param_or_identifier_name( &mut self, name: &str, kind: ParamObjType, ) -> Result<(), RuntimeError>

pub fn store_def_family( &mut self, def_family_stmt: &DefFamilyStmt, ) -> Result<(), RuntimeError>

impl Runtime

pub fn exec_import_stmt( &mut self, stmt: &ImportStmt, ) -> Result<StmtResult, RuntimeError>

pub fn exec_do_nothing_stmt( &mut self, stmt: &DoNothingStmt, ) -> Result<StmtResult, RuntimeError>

pub fn exec_clear_stmt( &mut self, stmt: &ClearStmt, ) -> Result<StmtResult, RuntimeError>

pub fn exec_run_file_stmt( &mut self, stmt: &RunFileStmt, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_exist_or_and_chain_atomic_fact_well_defined_and_store_and_infer( &mut self, fact: &ExistOrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<InferResult, RuntimeError>

pub fn verify_or_and_chain_atomic_fact_well_defined_and_store_and_infer( &mut self, fact: &OrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<InferResult, RuntimeError>

pub fn verify_fact_well_defined_and_store_and_infer( &mut self, fact: Fact, verify_state: &VerifyState, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn exec_witness_exist_fact( &mut self, stmt: &WitnessExistFact, ) -> Result<StmtResult, RuntimeError>

pub fn exec_witness_nonempty_set( &mut self, stmt: &WitnessNonemptySet, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn infer_atomic_fact( &mut self, atomic_fact: &AtomicFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn infer(&mut self, fact: &Fact) -> Result<InferResult, RuntimeError>

Dispatch infer by fact kind. Example: a $subset b enters atomic infer branch.

pub fn infer_exist_or_and_chain_atomic_fact( &mut self, fact: &ExistOrAndChainAtomicFact, ) -> Result<InferResult, RuntimeError>

pub fn infer_or_and_chain_atomic_fact( &mut self, fact: &OrAndChainAtomicFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn infer_equal_fact( &mut self, equal_fact: &EqualFact, ) -> Result<InferResult, RuntimeError>

pub fn infer_normal_atomic_fact( &mut self, normal_atomic_fact: &NormalAtomicFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn infer_restrict_fact( &mut self, rf: &RestrictFact, ) -> Result<InferResult, RuntimeError>

$restrict_fn_in(f, narrower_fn_set) after the fact is stored: remember the narrowed FnSetBody.

pub fn instantiate_family_member_set( &mut self, family_ty: &FamilyObj, ) -> Result<Obj, RuntimeError>

pub fn infer_membership_in_family_for_param_binding( &mut self, name: &str, family_ty: &FamilyObj, binding_kind: ParamObjType, ) -> Result<InferResult, RuntimeError>

pub fn infer_membership_in_family_from_in_fact( &mut self, in_fact: &InFact, family_obj: &FamilyObj, ) -> Result<InferResult, RuntimeError>

pub fn infer_membership_in_fn_set_from_in_fact( &mut self, in_fact: &InFact, fn_set_with_dom: &FnSet, ) -> Result<InferResult, RuntimeError>

pub fn infer_membership_in_set_builder_from_in_fact( &mut self, in_fact: &InFact, set_builder: &SetBuilder, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn infer_numeric_order_sign_from_order_atomic( &mut self, atomic_fact: &AtomicFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn infer_subset_fact( &mut self, subset_fact: &SubsetFact, ) -> Result<InferResult, RuntimeError>

pub fn infer_superset_fact( &mut self, superset_fact: &SupersetFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn parse_by_cases_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_closed_range_as_cases_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_commutative_prop_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_contra_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

by contra: then prove: block with exactly one atomic fact, optional proof statements, then impossible atomic fact.

Shorthand: by contra atomic_goal: embeds the goal on the header line; body is optional proof statement blocks followed by impossible ... as the last block.

impl Runtime

pub fn parse_by_enumerate_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_extension_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_family_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_fn_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_by_fn_set_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_by_tuple_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_for_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_induc_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_strong_induc_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_transitive_prop_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_by_prefixed_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_claim_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_def_struct_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_def_prop_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_def_abstract_prop_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_def_let_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_have_obj_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_have_fn_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_have_exist( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_def_family_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_def_algorithm_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn register_collected_param_names_for_def_parse( &mut self, names: &Vec<String>, line_file: LineFile, ) -> Result<(), RuntimeError>

pub fn insert_parsed_name_into_top_parsing_time_name_scope( &mut self, name: &str, line_file: LineFile, ) -> Result<(), RuntimeError>

pub fn parse_name_and_insert_into_top_parsing_time_name_scope( &mut self, tb: &mut TokenBlock, ) -> Result<String, RuntimeError>

impl Runtime

pub fn parse_eval_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_fact(&mut self, tb: &mut TokenBlock) -> Result<Fact, RuntimeError>

pub fn parse_and_chain_atomic_fact( &mut self, tb: &mut TokenBlock, ) -> Result<AndChainAtomicFact, RuntimeError>

pub fn parse_exist_fact( &mut self, tb: &mut TokenBlock, ) -> Result<ExistFactEnum, RuntimeError>

pub fn parse_facts_in_body( &mut self, tb: &mut TokenBlock, ) -> Result<Vec<Fact>, RuntimeError>

pub fn parse_exist_or_and_chain_atomic_fact( &mut self, tb: &mut TokenBlock, ) -> Result<ExistOrAndChainAtomicFact, RuntimeError>

pub fn parse_atomic_fact( &mut self, tb: &mut TokenBlock, is_true: bool, ) -> Result<AtomicFact, RuntimeError>

Parse a single atomic fact only: $prop(args) or obj op obj. Does not parse chain (obj op obj op obj).

pub fn parse_and_chain_atomic_fact_allow_leading_not( &mut self, tb: &mut TokenBlock, ) -> Result<AndChainAtomicFact, RuntimeError>

Normal and/chain atomic fact, or a single leading not on an atomic.

Self::parse_and_chain_atomic_fact alone is wrong for not $p(): it uses Self::parse_chain_atomic, which treats $p() as an infix $ between objs and parses () as grouping (empty-() / EOT issues). Used for or-disjuncts and case not ....

pub fn parse_or_and_chain_atomic_fact( &mut self, tb: &mut TokenBlock, ) -> Result<OrAndChainAtomicFact, RuntimeError>

pub fn parse_chain_atomic( &mut self, tb: &mut TokenBlock, is_true: bool, ) -> Result<ChainAtomicFact, RuntimeError>

Parse chain (obj op obj op …) or single atomic ($prop(args) or obj op obj). When is_true is false, only single atomic is allowed (negated).

impl Runtime

pub fn parse_know_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_obj(&mut self, tb: &mut TokenBlock) -> Result<Obj, RuntimeError>

pub fn parse_anonymous_fn( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

' + (param sets [: dom]) + return set + { body }, or ' + set + (names) + { body }.

After a comma-separated name list, if the next token is : (domain facts) rather than a set expression, parameters are taken to be in R (same as writing x, y R : ...).

pub fn parse_fn_set( &mut self, tb: &mut TokenBlock, ) -> Result<FnSet, RuntimeError>

pub fn parse_fn_set_clause( &mut self, tb: &mut TokenBlock, ) -> Result<FnSetClause, RuntimeError>

pub fn parse_number_or_primary_obj_or_fn_obj_with_minus_prefix( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

pub fn parse_braced_objs( &mut self, tb: &mut TokenBlock, ) -> Result<Vec<Obj>, RuntimeError>

pub fn parse_braced_obj( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

pub fn parse_obj_list( &mut self, tb: &mut TokenBlock, ) -> Result<Vec<Obj>, RuntimeError>

解析逗号分隔的 obj 列表，直到遇到非 COMMA 的 token（如 COLON）。

pub fn parse_list_set_obj( &mut self, tb: &mut TokenBlock, ) -> Result<ListSet, RuntimeError>

pub fn parse_identifier( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

pub fn parse_identifier_or_identifier_with_mod( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

Unqualified or ::-qualified name / field name; returns a name-shaped Obj.

pub fn parse_predicate( &mut self, tb: &mut TokenBlock, ) -> Result<AtomicName, RuntimeError>

pub fn parse_family_obj( &mut self, tb: &mut TokenBlock, ) -> Result<FamilyObj, RuntimeError>

pub fn parse_struct_view_obj( &mut self, tb: &mut TokenBlock, ) -> Result<Obj, RuntimeError>

pub fn parse_atomic_name( &mut self, tb: &mut TokenBlock, ) -> Result<AtomicName, RuntimeError>

ident or mod::ident as a predicate/atomic name in parse position.

impl Runtime

pub fn parse_param_def_with_param_type_and_skip_comma( &mut self, tb: &mut TokenBlock, free_param_kind: ParamObjType, ) -> Result<ParamGroupWithParamType, RuntimeError>

Each parameter name is pushed to Runtime::parsing_free_param_collection with free_param_kind before its shared type is parsed, so later parameter types in the same group (or later groups) can resolve earlier parameters. Use ParamObjType::DefHeader for prop { ... } and family headers, ParamObjType::Forall for forall, ParamObjType::Exist for exist, ParamObjType::Identifier for let / have, etc.

pub fn parse_param_type( &mut self, tb: &mut TokenBlock, ) -> Result<ParamType, RuntimeError>

pub fn parse_param_type_nonempty_set( &self, tb: &mut TokenBlock, ) -> Result<ParamType, RuntimeError>

pub fn parse_param_type_finite_set( &self, tb: &mut TokenBlock, ) -> Result<ParamType, RuntimeError>

pub fn parse_param_type_set( &self, tb: &mut TokenBlock, ) -> Result<ParamType, RuntimeError>

pub fn parse_param_type_obj( &mut self, tb: &mut TokenBlock, ) -> Result<ParamType, RuntimeError>

impl Runtime

pub fn parse_prove_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_stmt(&mut self, tb: &mut TokenBlock) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_import_stmt( &self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_do_nothing_stmt( &self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_clear_stmt( &self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_run_file_stmt( &self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn parse_witness_stmt( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_witness_exist_fact( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

pub fn parse_witness_nonempty_set( &mut self, tb: &mut TokenBlock, ) -> Result<Stmt, RuntimeError>

impl Runtime

pub fn new() -> Self

pub fn new_with_builtin_code() -> Self

impl Runtime

pub fn validate_name( &mut self, name: &str, _current_line_file: LineFile, ) -> Result<(), RuntimeError>

pub fn validate_user_fn_param_names_for_parse( &mut self, names: &[String], line_file: LineFile, ) -> Result<(), RuntimeError>

pub fn validate_names_and_insert_into_top_parsing_time_name_scope( &mut self, names: &Vec<String>, line_file: LineFile, ) -> Result<(), RuntimeError>

pub fn validate_name_and_insert_into_top_parsing_time_name_scope( &mut self, name: &str, line_file: LineFile, ) -> Result<(), RuntimeError>

Validates identifier syntax only; does not record bindings (see run_in_local_parsing_time_name_scope).

impl Runtime

pub fn new_file_path_new_env_new_name_scope(&mut self, path: &str)

pub fn set_current_user_lit_file_path(&mut self, path: &str)

After new_file_path_new_env_new_name_scope, point the current user entry slot at another path without pushing more layers (pair with clear_current_env_and_parse_name_scope).

impl Runtime

pub fn top_level_env(&mut self) -> &mut Environment

impl Runtime

pub fn clear_current_env_and_parse_name_scope(&mut self)

Replace the top environment with an empty one and clear parse-time free-param scopes. If there is only one environment layer (builtin), does nothing so builtins stay intact.

pub fn run_in_local_env<T, E, F>(&mut self, f: F) -> Result<T, E>

where F: FnOnce(&mut Self) -> Result<T, E>,

在临时子环境中执行闭包：push_env → f → pop_env；Ok/Err 都会弹出。 与手写 push/pop 等价；若闭包 panic，栈不会恢复（与手写相同）。

pub fn run_in_local_parsing_time_name_scope<T, E, F>( &mut self, f: F, ) -> Result<T, E>

where F: FnOnce(&mut Self) -> Result<T, E>,

Restores Runtime::parsing_free_param_collection after f so parse-time bindings (e.g. have x … without =) do not leak across sibling prove: blocks or out of nested parses that use this wrapper (forall, exist, prove, prop bodies, etc.).

pub fn parse_in_local_free_param_scope<T, F>( &mut self, kind: ParamObjType, names: &[String], line_file: LineFile, f: F, ) -> Result<T, RuntimeError>

where F: FnOnce(&mut Self) -> Result<T, RuntimeError>,

begin_scope → f → end_scope; runs end_scope on both Ok and Err (not on begin_scope failure).

pub fn with_optional_free_param_scope<T, F>( &mut self, kind: ParamObjType, names: &[String], line_file: LineFile, f: F, ) -> Result<T, RuntimeError>

where F: FnOnce(&mut Self) -> Result<T, RuntimeError>,

If names is empty, runs f with no extra scope; otherwise wraps it in parse_in_local_free_param_scope.

pub fn parse_stmts_with_optional_free_param_scope<F>( &mut self, kind: ParamObjType, names: &[String], line_file: LineFile, parse_body: F, ) -> Result<Vec<Stmt>, RuntimeError>

where F: FnOnce(&mut Self) -> Result<Vec<Stmt>, RuntimeError>,

impl Runtime

pub fn is_name_used_for_identifier(&self, name: &str) -> bool

pub fn is_name_used_for_prop(&self, name: &str) -> bool

pub fn is_name_used_for_abstract_prop(&self, name: &str) -> bool

pub fn is_name_used_for_family(&self, name: &str) -> bool

pub fn is_name_used_for_algo(&self, name: &str) -> bool

impl Runtime

pub fn new_file_and_update_runtime_with_file_content(&mut self, path: &str)

pub fn change_file_index_to(&mut self, file_index: usize)

impl Runtime

pub fn store_tuple_obj_and_cart( &mut self, name: &str, tuple: Option<Tuple>, cart: Option<Cart>, line_file: LineFile, )

pub fn store_known_cart_obj( &mut self, name: &str, cart: Cart, line_file: LineFile, )

pub fn store_known_finite_seq_list_obj( &mut self, name: &str, list: FiniteSeqListObj, member_of_finite_seq_set: Option<FiniteSeqSet>, line_file: LineFile, )

pub fn store_known_matrix_list_obj( &mut self, name: &str, matrix: MatrixListObj, member_of_matrix_set: Option<MatrixSet>, line_file: LineFile, )

pub fn matrix_set_to_fn_set(&self, ms: &MatrixSet, line_file: LineFile) -> FnSet

pub fn finite_seq_set_to_fn_set( &self, fs: &FiniteSeqSet, line_file: LineFile, ) -> FnSet

pub fn seq_set_to_fn_set(&self, ss: &SeqSet, _line_file: LineFile) -> FnSet

pub fn finite_seq_set_to_fn_set_from_surface_dom_param( &self, fs: &FiniteSeqSet, line_file: LineFile, surface_dom_param: &str, ) -> Result<FnSet, RuntimeError>

pub fn store_well_defined_obj_cache(&mut self, obj: &Obj)

impl Runtime

pub fn new_fn_set( &self, params_and_their_sets: Vec<ParamGroupWithSet>, dom_facts: Vec<OrAndChainAtomicFact>, ret_set: Obj, ) -> Result<FnSet, RuntimeError>

pub fn new_anonymous_fn( &self, params_and_their_sets: Vec<ParamGroupWithSet>, dom_facts: Vec<OrAndChainAtomicFact>, ret_set: Obj, equal_to: Obj, ) -> Result<AnonymousFn, RuntimeError>

pub fn fn_set_from_fn_set_clause( &self, clause: &FnSetClause, ) -> Result<FnSet, RuntimeError>

impl Runtime

pub fn params_to_arg_map( &self, param_defs: &ParamDefWithType, args: &[Obj], ) -> Result<HashMap<String, Obj>, RuntimeError>

impl Runtime

pub fn define_parameter_by_binding_param_type( &mut self, name: &str, param_type: &ParamType, binding_kind: ParamObjType, ) -> Result<InferResult, RuntimeError>

After store_identifier_obj, run param-type-specific work (type facts, storage, and later hooks).

pub fn define_params_with_type( &mut self, param_defs: &ParamDefWithType, check_type_nonempty: bool, binding_kind: ParamObjType, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn generate_one_unused_name_with_reserved( &self, reserved_names: &HashSet<String>, ) -> String

pub fn generate_random_unused_names(&self, count: usize) -> Vec<String>

pub fn generate_random_unused_name(&self) -> String

impl Runtime

pub fn get_prop_definition_by_name( &self, predicate_name: &str, ) -> Option<&DefPropStmt>

pub fn get_abstract_prop_definition_by_name( &self, predicate_name: &str, ) -> Option<&DefAbstractPropStmt>

Look up abstract prop (abstract_prop keyword) definition by name from current env or builtin.

pub fn get_algo_definition_by_name( &self, algo_name: &str, ) -> Option<&DefAlgoStmt>

pub fn get_struct_definition_by_name( &self, struct_name: &str, ) -> Option<&DefStructStmt>

pub fn get_family_definition_by_name( &self, family_name: &str, ) -> Option<&DefFamilyStmt>

pub fn get_cloned_family_definition_by_name( &self, family_name: &str, ) -> Option<DefFamilyStmt>

impl Runtime

pub fn inst_fact( &self, fact: &Fact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_to_line_file: Option<LineFile>, ) -> Result<Fact, RuntimeError>

inst_to_line_file: None keeps each node’s original line file (verify, exec, parsing). Some(lf) assigns lf throughout the instance (infer: tie the new fact to the use site).

pub fn inst_exist_or_and_chain_atomic_fact( &self, fact: &ExistOrAndChainAtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ExistOrAndChainAtomicFact, RuntimeError>

pub fn inst_exist_body_fact( &self, fact: &ExistBodyFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ExistBodyFact, RuntimeError>

pub fn inst_or_and_chain_atomic_fact( &self, fact: &OrAndChainAtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<OrAndChainAtomicFact, RuntimeError>

pub fn inst_and_chain_atomic_fact( &self, fact: &AndChainAtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<AndChainAtomicFact, RuntimeError>

pub fn inst_atomic_fact( &self, atomic_fact: &AtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<AtomicFact, RuntimeError>

pub fn inst_normal_atomic_fact( &self, normal_atomic_fact: &NormalAtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NormalAtomicFact, RuntimeError>

pub fn inst_equal_fact( &self, equal_fact: &EqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<EqualFact, RuntimeError>

pub fn inst_less_fact( &self, less_fact: &LessFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<LessFact, RuntimeError>

pub fn inst_greater_fact( &self, greater_fact: &GreaterFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<GreaterFact, RuntimeError>

pub fn inst_less_equal_fact( &self, less_equal_fact: &LessEqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<LessEqualFact, RuntimeError>

pub fn inst_greater_equal_fact( &self, greater_equal_fact: &GreaterEqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<GreaterEqualFact, RuntimeError>

pub fn inst_is_set_fact( &self, is_set_fact: &IsSetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<IsSetFact, RuntimeError>

pub fn inst_is_nonempty_set_fact( &self, is_nonempty_set_fact: &IsNonemptySetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<IsNonemptySetFact, RuntimeError>

pub fn inst_is_finite_set_fact( &self, is_finite_set_fact: &IsFiniteSetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<IsFiniteSetFact, RuntimeError>

pub fn inst_in_fact( &self, in_fact: &InFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<InFact, RuntimeError>

pub fn inst_is_cart_fact( &self, is_cart_fact: &IsCartFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<IsCartFact, RuntimeError>

pub fn inst_is_tuple_fact( &self, is_tuple_fact: &IsTupleFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<IsTupleFact, RuntimeError>

pub fn inst_subset_fact( &self, subset_fact: &SubsetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<SubsetFact, RuntimeError>

pub fn inst_superset_fact( &self, superset_fact: &SupersetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<SupersetFact, RuntimeError>

pub fn inst_not_normal_atomic_fact( &self, not_normal_atomic_fact: &NotNormalAtomicFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotNormalAtomicFact, RuntimeError>

pub fn inst_not_equal_fact( &self, not_equal_fact: &NotEqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotEqualFact, RuntimeError>

pub fn inst_not_less_fact( &self, not_less_fact: &NotLessFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotLessFact, RuntimeError>

pub fn inst_not_greater_fact( &self, not_greater_fact: &NotGreaterFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotGreaterFact, RuntimeError>

pub fn inst_not_less_equal_fact( &self, not_less_equal_fact: &NotLessEqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotLessEqualFact, RuntimeError>

pub fn inst_not_greater_equal_fact( &self, not_greater_equal_fact: &NotGreaterEqualFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotGreaterEqualFact, RuntimeError>

pub fn inst_not_is_set_fact( &self, not_is_set_fact: &NotIsSetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotIsSetFact, RuntimeError>

pub fn inst_not_is_nonempty_set_fact( &self, not_is_nonempty_set_fact: &NotIsNonemptySetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotIsNonemptySetFact, RuntimeError>

pub fn inst_not_is_finite_set_fact( &self, not_is_finite_set_fact: &NotIsFiniteSetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotIsFiniteSetFact, RuntimeError>

pub fn inst_not_in_fact( &self, not_in_fact: &NotInFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotInFact, RuntimeError>

pub fn inst_not_is_cart_fact( &self, not_is_cart_fact: &NotIsCartFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotIsCartFact, RuntimeError>

pub fn inst_not_is_tuple_fact( &self, not_is_tuple_fact: &NotIsTupleFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotIsTupleFact, RuntimeError>

pub fn inst_not_subset_fact( &self, not_subset_fact: &NotSubsetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotSubsetFact, RuntimeError>

pub fn inst_not_superset_fact( &self, not_superset_fact: &NotSupersetFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotSupersetFact, RuntimeError>

pub fn inst_exist_fact( &self, exist_fact: &ExistFactEnum, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ExistFactEnum, RuntimeError>

pub fn inst_or_fact( &self, or_fact: &OrFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<OrFact, RuntimeError>

pub fn inst_and_fact( &self, and_fact: &AndFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<AndFact, RuntimeError>

pub fn inst_chain_fact( &self, chain_fact: &ChainFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ChainFact, RuntimeError>

pub fn inst_forall_fact( &self, forall_fact: &ForallFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ForallFact, RuntimeError>

pub fn inst_forall_fact_with_iff( &self, forall_fact_with_iff: &ForallFactWithIff, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<ForallFactWithIff, RuntimeError>

pub fn inst_restrict_fact( &self, restrict_fact: &RestrictFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<RestrictFact, RuntimeError>

pub fn inst_not_restrict_fact( &self, not_restrict_fact: &NotRestrictFact, param_to_arg_map: &HashMap<String, Obj>, to_inst_param_type: ParamObjType, inst_lf: Option<&LineFile>, ) -> Result<NotRestrictFact, RuntimeError>

impl Runtime

pub fn inst_have_fn_forall_fact_for_store( &self, forall_fact: ForallFact, ) -> Result<Fact, RuntimeError>

impl Runtime

pub fn inst_obj( &self, obj: &Obj, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_identifier( &self, identifier: &Identifier, param_to_arg_map: &HashMap<String, Obj>, ) -> Result<Obj, RuntimeError>

pub fn inst_identifier_with_mod( &self, identifier_with_mod: &IdentifierWithMod, param_to_arg_map: &HashMap<String, Obj>, ) -> Result<Obj, RuntimeError>

pub fn inst_fn_obj( &self, fn_obj: &FnObj, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_number( &self, number: &Number, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_add( &self, add: &Add, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_add( &self, ma: &MatrixAdd, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_sub( &self, ms: &MatrixSub, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_mul( &self, mm: &MatrixMul, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_scalar_mul( &self, m: &MatrixScalarMul, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_pow( &self, m: &MatrixPow, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_sub( &self, sub: &Sub, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_mul( &self, mul: &Mul, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_div( &self, div: &Div, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_mod( &self, mod_obj: &Mod, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_pow( &self, pow: &Pow, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_abs( &self, abs: &Abs, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_log( &self, log: &Log, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_max( &self, max: &Max, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_min( &self, min: &Min, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_union( &self, union: &Union, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_intersect( &self, intersect: &Intersect, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_set_minus( &self, set_minus: &SetMinus, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_set_diff( &self, set_diff: &SetDiff, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_cup( &self, cup: &Cup, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_cap( &self, cap: &Cap, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_power_set( &self, power_set: &PowerSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_list_set( &self, list_set: &ListSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_set_builder( &self, set_builder: &SetBuilder, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_fn_set_with_params( &self, fn_set_with_params: &FnSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_anonymous_fn_with_params( &self, af: &AnonymousFn, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_cart( &self, cart: &Cart, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_cart_dim( &self, cart_dim: &CartDim, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_proj( &self, proj: &Proj, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_tuple_dim( &self, tuple_dim: &TupleDim, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_tuple( &self, tuple: &Tuple, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_count( &self, count: &Count, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_sum( &self, sum: &Sum, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_product( &self, product: &Product, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_range( &self, range: &Range, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_closed_range( &self, closed_range: &ClosedRange, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_finite_seq_set( &self, fs: &FiniteSeqSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_seq_set( &self, ss: &SeqSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_finite_seq_list_obj( &self, v: &FiniteSeqListObj, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_set( &self, ms: &MatrixSet, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_matrix_list_obj( &self, m: &MatrixListObj, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_choose( &self, choose: &Choose, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_obj_at_index( &self, obj_at_index: &ObjAtIndex, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<Obj, RuntimeError>

pub fn inst_standard_set( &self, standard_set: &StandardSet, ) -> Result<Obj, RuntimeError>

pub fn inst_param_type( &self, param_type: &ParamType, param_to_arg_map: &HashMap<String, Obj>, param_obj_type: ParamObjType, ) -> Result<ParamType, RuntimeError>

pub fn inst_param_def_with_set_one_by_one( &self, param_defs: &Vec<ParamGroupWithSet>, args: &Vec<Obj>, param_obj_type: ParamObjType, ) -> Result<Vec<Obj>, RuntimeError>

pub fn inst_param_def_with_type_one_by_one( &self, param_defs: &ParamDefWithType, args: &Vec<Obj>, param_obj_type: ParamObjType, ) -> Result<Vec<ParamType>, RuntimeError>

impl Runtime

pub fn iter_environments_from_top(&self) -> impl Iterator<Item = &Environment>

pub fn is_commutative_prop_name_known(&self, prop_name: &str) -> bool

pub fn get_object_in_fn_set(&self, obj: &Obj) -> Option<&FnSetBody>

Declared function space (KnownFnInfo.fn_set) only — not $restrict_fn_in targets.

pub fn get_object_in_fn_set_or_restrict(&self, obj: &Obj) -> Option<&FnSetBody>

Like get_object_in_fn_set but falls back to KnownFnInfo.restrict_to (e.g. after $restrict_fn_in) for well-defined/calls.

pub fn get_cloned_object_in_fn_set(&self, obj: &Obj) -> Option<FnSetBody>

pub fn get_cloned_object_in_fn_set_or_restrict( &self, obj: &Obj, ) -> Option<FnSetBody>

pub fn get_known_fn_body_and_equal_to_for_key( &self, key: &str, ) -> Option<(FnSetBody, Obj, LineFile)>

User have fn f … = …: FnSetBody and defining RHS when both are stored in crate::environment::KnownFnInfo (inner scopes override outer).

pub fn cache_well_defined_obj_contains(&self, key: &str) -> bool

pub fn cache_known_facts_contains(&self, key: &str) -> (bool, LineFile)

pub fn get_object_equal_to_cart(&self, name: &str) -> Option<Cart>

pub fn get_obj_equal_to_tuple(&self, name: &str) -> Option<Tuple>

pub fn get_obj_equal_to_finite_seq_list( &self, name: &str, ) -> Option<FiniteSeqListObj>

pub fn get_finite_seq_set_for_obj_equal_to_seq_list( &self, name: &str, ) -> Option<FiniteSeqSet>

pub fn get_obj_equal_to_matrix_list(&self, name: &str) -> Option<MatrixListObj>

pub fn get_matrix_set_for_obj_equal_to_matrix_list( &self, name: &str, ) -> Option<MatrixSet>

pub fn get_object_equal_to_tuple(&self, name: &str) -> Option<Cart>

pub fn get_object_equal_to_normalized_decimal_number( &self, obj_str: &str, ) -> Option<Number>

pub fn get_all_objs_equal_to_given(&self, given: &str) -> Vec<String>

impl Runtime

pub fn resolve_obj_to_number(&self, obj: &Obj) -> Option<Number>

pub fn resolve_obj_to_number_resolved(&self, obj: &Obj) -> Option<Number>

pub fn resolve_obj(&self, obj: &Obj) -> Obj

impl Runtime

pub fn store_args_satisfy_param_type_when_not_defining_new_identifiers( &mut self, param_defs: &ParamDefWithType, args: &Vec<Obj>, _line_file: LineFile, param_obj_type: ParamObjType, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn verify_well_defined_and_store_and_infer( &mut self, fact: Fact, verify_state: &VerifyState, ) -> Result<InferResult, RuntimeError>

pub fn verify_well_defined_and_store_and_infer_with_default_verify_state( &mut self, fact: Fact, ) -> Result<InferResult, RuntimeError>

pub fn store_fact_without_forall_coverage_check_and_infer( &mut self, fact: Fact, ) -> Result<InferResult, RuntimeError>

pub fn store_and_chain_atomic_fact_without_well_defined_verified_and_infer( &mut self, fact: AndChainAtomicFact, ) -> Result<InferResult, RuntimeError>

pub fn store_atomic_fact_without_well_defined_verified_and_infer( &mut self, fact: AtomicFact, ) -> Result<InferResult, RuntimeError>

pub fn store_exist_or_and_chain_atomic_fact_without_well_defined_verified_and_infer( &mut self, fact: ExistOrAndChainAtomicFact, ) -> Result<InferResult, RuntimeError>

pub fn store_or_and_chain_atomic_fact_without_well_defined_verified_and_infer( &mut self, fact: OrAndChainAtomicFact, ) -> Result<InferResult, RuntimeError>

impl Runtime

pub fn verify_and_fact( &mut self, and_fact: &AndFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_chain_fact( &mut self, chain_fact: &ChainFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_atomic_fact( &mut self, fact: &AtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_atomic_fact_with_known_forall( &mut self, atomic_fact: &AtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn match_args_in_fact_in_known_forall_fact_with_given_args( &mut self, fact_args_in_known_forall: &Vec<Obj>, given_fact_args: &Vec<Obj>, ) -> Result<Option<HashMap<String, Obj>>, RuntimeError>

impl Runtime

pub fn verify_equality_by_builtin_rules( &mut self, left: &Obj, right: &Obj, line_file: LineFile, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn try_verify_equality_with_known_equalities_by_builtin_rules_only( &mut self, left: &Obj, right: &Obj, line_file: LineFile, verify_state: &VerifyState, known_objs_equal_to_left: Option<&Rc<Vec<Obj>>>, known_objs_equal_to_right: Option<&Rc<Vec<Obj>>>, ) -> Result<Option<StmtResult>, RuntimeError>

pub fn objs_have_same_known_equality_rc_in_some_env( &self, left: &Obj, right: &Obj, ) -> bool

pub fn try_verify_equal_by_same_shape_and_known_equality_args( &self, left: &Obj, right: &Obj, line_file: LineFile, ) -> Option<StmtResult>

pub fn verify_equality_by_they_are_the_same_and_calculation( &mut self, left: &Obj, right: &Obj, line_file: LineFile, _verify_state: &VerifyState, ) -> Result<(StmtResult, Obj, Obj), RuntimeError>

impl Runtime

pub fn verify_not_in_fact_with_builtin_rules( &mut self, not_in_fact: &NotInFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_in_fact_with_builtin_rules( &mut self, in_fact: &InFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_non_equational_atomic_fact_with_builtin_rules( &mut self, atomic_fact: &AtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn non_equational_atomic_fact_holds_by_full_verify_pipeline( &mut self, atomic_fact: &AtomicFact, verify_state: &VerifyState, ) -> Result<bool, RuntimeError>

impl Runtime

pub fn _verify_not_equal_fact_with_builtin_rules( &mut self, not_equal_fact: &NotEqualFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn mul_product_negative_when_factors_have_strict_opposite_sign_by_non_equational_verify( &mut self, left_factor: &Obj, right_factor: &Obj, line_file: LineFile, verify_state: &VerifyState, ) -> Result<bool, RuntimeError>

impl Runtime

pub fn verify_order_atomic_fact_numeric_builtin_only( &mut self, atomic_fact: &AtomicFact, ) -> Result<StmtResult, RuntimeError>

pub fn verify_number_comparison_builtin_rule( &self, atomic_fact: &AtomicFact, ) -> Option<bool>

impl Runtime

pub fn try_verify_numeric_order_via_div_elimination( &self, left_obj: &Obj, right_obj: &Obj, allow_equal: bool, ) -> Option<bool>

impl Runtime

pub fn verify_subset_fact_with_builtin_rules( &mut self, subset_fact: &SubsetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

Verify subset by duality: a subset b iff b superset a.

pub fn verify_superset_fact_with_builtin_rules( &mut self, superset_fact: &SupersetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

Verify superset by duality: a superset b iff b subset a.

pub fn verify_not_subset_fact_with_builtin_rules( &mut self, not_subset_fact: &NotSubsetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

Verify not subset by converting to the dual not superset.

pub fn verify_not_superset_fact_with_builtin_rules( &mut self, not_superset_fact: &NotSupersetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

Verify not superset by converting to the dual not subset.

impl Runtime

pub fn _verify_is_nonempty_set_fact_with_builtin_rules( &mut self, is_nonempty_set_fact: &IsNonemptySetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn _verify_is_finite_set_fact_with_builtin_rules( &mut self, is_finite_set_fact: &IsFiniteSetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn _verify_is_cart_fact_with_builtin_rules( &mut self, is_cart_fact: &IsCartFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn _verify_is_tuple_fact_with_builtin_rules( &mut self, is_tuple_fact: &IsTupleFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn _verify_not_is_nonempty_set_fact_with_builtin_rules( &mut self, not_is_nonempty_set_fact: &NotIsNonemptySetFact, _verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn equal_literally(&self, left: &Obj, right: &Obj) -> bool

impl Runtime

pub fn verify_equal_fact( &mut self, equal_fact: &EqualFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_objs_are_equal( &mut self, left: &Obj, right: &Obj, line_file: LineFile, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_exist_fact( &mut self, exist_fact: &ExistFactEnum, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_exist_fact_with_known_exist_fact( &mut self, exist_fact: &ExistFactEnum, known_exist_fact: &ExistFactEnum, ) -> Result<StmtResult, RuntimeError>

pub fn verify_exist_fact_with_known_exist_fact_with_facts_in_environment( runtime: &Runtime, environment: &Environment, exist_fact: &ExistFactEnum, known_exist_fact: &ExistFactEnum, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_exist_fact_with_known_forall( &mut self, exist_fact: &ExistFactEnum, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_fact_return_err_if_not_true( &mut self, fact: &Fact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_exist_or_and_chain_atomic_fact( &mut self, exist_or_and_chain_atomic_fact: &ExistOrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_or_and_chain_atomic_fact( &mut self, or_and_chain_atomic_fact: &OrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_and_chain_atomic_fact( &mut self, and_chain_atomic_fact: &AndChainAtomicFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_fact_well_defined( &mut self, fact: &Fact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_atomic_fact_well_defined( &mut self, atomic_fact: &AtomicFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_and_fact_well_defined( &mut self, and_fact: &AndFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_chain_fact_well_defined( &mut self, chain_fact: &ChainFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_or_fact_well_defined( &mut self, or_fact: &OrFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_exist_fact_well_defined( &mut self, exist_fact: &ExistFactEnum, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_forall_fact_well_defined( &mut self, forall_fact: &ForallFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_forall_fact_params_and_dom_well_defined( &mut self, forall_fact: &ForallFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_or_and_chain_atomic_fact_well_defined( &mut self, fact: &OrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_exist_or_and_chain_atomic_fact_well_defined( &mut self, fact: &ExistOrAndChainAtomicFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_forall_fact_with_iff_well_defined( &mut self, forall_fact_with_iff: &ForallFactWithIff, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

pub fn verify_not_forall_fact_well_defined( &mut self, not_forall: &NotForallFact, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

impl Runtime

pub fn _verify_or_and_chain_atomic_facts_the_same_type_and_return_matched_args( fact: &OrAndChainAtomicFact, other: &OrAndChainAtomicFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_and_chain_atomic_facts_the_same_type_and_return_matched_args( fact: &AndChainAtomicFact, other: &AndChainAtomicFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_chain_fact_the_same_type_and_return_matched_args( fact: &ChainFact, other: &ChainFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_or_fact_the_same_type_and_return_matched_args( fact: &OrFact, other: &OrFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_and_fact_the_same_type_and_return_matched_args( fact: &AndFact, other: &AndFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_exist_fact_the_same_type_and_return_matched_args( fact: &ExistFactEnum, other: &ExistFactEnum, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

pub fn _verify_atomic_fact_the_same_type_and_return_matched_args( _fact: &AtomicFact, _other: &AtomicFact, ) -> Result<Option<Vec<(Obj, Obj)>>, RuntimeError>

impl Runtime

pub fn verify_fn_equal_in_fact_with_builtin_rules( &mut self, f: &FnEqualInFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_fn_equal_fact_with_builtin_rules( &mut self, f: &FnEqualFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_fn_set_with_params_equality_by_builtin_rules( &mut self, left: &FnSet, right: &FnSet, line_file: LineFile, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_forall_fact( &mut self, forall_fact: &ForallFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

Declare params, assume dom facts hold, then verify each then_fact.

impl Runtime

pub fn verify_forall_fact_with_iff( &mut self, forall_iff: &ForallFactWithIff, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_fact_from_cache_using_display_string( &self, fact: &Fact, ) -> Option<StmtResult>

If the fact string is in the known-facts cache, return the cached verification result.

pub fn verify_param_type_nonempty_if_required( &mut self, param_type: &ParamType, check_type_nonempty: bool, ) -> Result<(), RuntimeError>

If check_type_nonempty is true and param_type is Obj(set), verifies that the set is nonempty and stores the fact.

impl Runtime

pub fn verify_non_equational_atomic_fact_with_known_atomic_facts( &mut self, atomic_fact: &AtomicFact, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_non_equational_atomic_fact( &mut self, atomic_fact: &AtomicFact, verify_state: &VerifyState, post_process: bool, ) -> Result<StmtResult, RuntimeError>

pub fn verify_fact( &mut self, fact: &Fact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_not_forall_fact( &mut self, not_forall: &NotForallFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_obj_satisfies_param_type( &mut self, obj: Obj, param_type: &ParamType, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_args_satisfy_param_def_flat_types( &mut self, param_defs: &ParamDefWithType, args: &Vec<Obj>, verify_state: &VerifyState, to_inst_param_type: ParamObjType, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_obj_satisfies_family( &mut self, obj: Obj, family_ty: &FamilyObj, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_obj_well_defined_and_store_cache( &mut self, obj: &Obj, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

impl Runtime

pub fn verify_param_type_well_defined( &mut self, param_type: &ParamType, verify_state: &VerifyState, ) -> Result<(), RuntimeError>

impl Runtime

pub fn verify_or_fact( &mut self, or_fact: &OrFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

pub fn verify_or_fact_with_known_or_facts( &mut self, or_fact: &OrFact, ) -> Result<StmtResult, RuntimeError>

pub fn verify_or_fact_with_known_or_facts_with_facts_in_environment( environment: &Environment, or_fact: &OrFact, all_objs_equal_to_each_arg: &Vec<Vec<String>>, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_or_fact_with_known_forall( &mut self, or_fact: &OrFact, verify_state: &VerifyState, ) -> Result<StmtResult, RuntimeError>

impl Runtime

pub fn verify_restrict_fact_using_its_definition( &mut self, restrict_fact: &RestrictFact, verify_state: &VerifyState, ) -> Result<Option<StmtResult>, RuntimeError>

impl Runtime

pub fn verify_obj_well_defined_with_its_local_def( &mut self, params_def: Vec<ParamGroupWithSet>, define_params_to_be_param_obj_type: ParamObjType, obj: Obj, ) -> Result<(), RuntimeError>