Module Synint.Comp

type unbox_modifier = [
  1. | `Strengthened
]
type case_pragma =
  1. | PragmaCase
  2. | PragmaNotCase
type context_case =
  1. | EmptyContext of Syncom.Location.t
  2. | ExtendedBy of Syncom.Location.t * int
type case_label =
  1. | Lf_constant of Syncom.Location.t * Syncom.Name.t * Syncom.Id.cid_term
  2. | Comp_constant of Syncom.Location.t * Syncom.Name.t * Syncom.Id.cid_comp_const
  3. | BVarCase of Syncom.Location.t
  4. | ContextCase of context_case
  5. | PVarCase of Syncom.Location.t * int * int option
type 'a generic_order =
  1. | Arg of 'a
  2. | Lex of 'a generic_order list
  3. | Simul of 'a generic_order list
type 'a generic_suffices_typ = [
  1. | `exact of 'a
  2. | `infer of Syncom.Location.t
]

Type specified in an interactive use of `suffices`

val map_suffices_typ : ('a -> 'b) -> 'a generic_suffices_typ -> 'b generic_suffices_typ
val map_order : ('a -> 'b) -> 'a generic_order -> 'b generic_order
type kind =
  1. | Ctype of Syncom.Location.t
  2. | PiKind of Syncom.Location.t * LF.ctyp_decl * kind
type meta_typ = LF.ctyp
type meta_obj = Syncom.Location.t * LF.mfront
type meta_spine =
  1. | MetaNil
  2. | MetaApp of meta_obj * meta_typ * meta_spine * Syncom.Plicity.t
type suffices_typ = typ generic_suffices_typ
val loc_of_typ : typ -> Syncom.Location.t
val loc_of_suffices_typ : suffices_typ -> Syncom.Location.t
type ih_arg =
  1. | M of meta_obj * meta_typ
  2. | V of Syncom.Id.offset
  3. | E
  4. | DC
type wf_tag = bool
type ctyp_decl =
  1. | CTypDecl of Syncom.Name.t * typ * wf_tag
  2. | CTypDeclOpt of Syncom.Name.t
type ih_decl =
  1. | WfRec of Syncom.Name.t * ih_arg list * typ
val rename_ctyp_decl : (Syncom.Name.t -> Syncom.Name.t) -> ctyp_decl -> ctyp_decl
type gctx = ctyp_decl LF.ctx
type ihctx = ih_decl LF.ctx

Normal computational terms

and pattern_spine =
  1. | PatNil
  2. | PatApp of Syncom.Location.t * pattern * pattern_spine
  3. | PatObs of Syncom.Location.t * Syncom.Id.cid_comp_dest * LF.msub * pattern_spine
and branch =
  1. | Branch of Syncom.Location.t * LF.mctx * LF.mctx * gctx * pattern * LF.msub * exp
and fun_branches =
  1. | NilFBranch of Syncom.Location.t
  2. | ConsFBranch of Syncom.Location.t * LF.mctx * gctx * pattern_spine * exp * fun_branches
type tclo = typ * LF.msub
type order = int generic_order
type 'order total_dec_kind = [
  1. | `inductive of 'order
  2. | `not_recursive
  3. | `trust
  4. | `partial
]
val map_total_dec_kind : ('o2 -> 'o2) -> 'o2 total_dec_kind -> 'o2 total_dec_kind
val option_of_total_dec_kind : [> `inductive of 'a ] -> 'a option
val apply_many : exp -> exp list -> exp

Applies a spine of checkable terms to a synthesizable term, from left to right.

val loc_of_exp : exp -> Syncom.Location.t
type total_dec = {
  1. name : Syncom.Name.t;
  2. tau : typ;
  3. order : order total_dec_kind;
}
val make_total_dec : Syncom.Name.t -> typ -> order total_dec_kind -> total_dec
val is_meta_obj : exp -> meta_obj option

Decides whether this synthesizable expression is actually an annotated box.

val head_of_meta_obj : meta_obj -> (LF.dctx_hat * LF.head) option
val itermToClObj : LF.iterm -> LF.clobj
val metaObjToMFront : ('a * 'b) -> 'b
val head_of_application : exp -> exp

Finds the head of an application. Chases meta-applications and computation applications.

val strip_pattern : pattern -> pattern

Removes all type annotations from a pattern.

val strip_pattern_spine : pattern_spine -> pattern_spine
type defer_kind = [
  1. | `subgoal
  2. | `theorem
]
type invoke_kind = [
  1. | `ih
  2. | `lemma
]
type split_kind = [
  1. | `split
  2. | `invert
  3. | `impossible
]
type level = [
  1. | `meta
  2. | `comp
]
type hypotheses = {
  1. cD : LF.mctx;
  2. cG : gctx;
  3. cIH : ihctx;
}
val no_hypotheses : hypotheses
type meta_branch_label = [
  1. | `ctor of Syncom.Id.cid_term
  2. | `pvar of int option
  3. | `bvar
]
module SubgoalPath : sig ... end
type proof =
  1. | Incomplete of Syncom.Location.t * proof_state
  2. | Command of command * proof
  3. | Directive of directive
and command =
  1. | By of exp * Syncom.Name.t * typ
  2. | Unbox of exp * Syncom.Name.t * LF.ctyp * unbox_modifier option
and proof_state = {
  1. context : hypotheses;
  2. label : SubgoalPath.builder;
  3. goal : tclo;
  4. solution : proof option Stdlib.ref;
}
and directive =
  1. | Intros of hypothetical
  2. | Solve of exp
  3. | ImpossibleSplit of exp
  4. | Suffices of exp * suffices_arg list
  5. | MetaSplit of exp * typ * meta_branch list
  6. | CompSplit of exp * typ * comp_branch list
  7. | ContextSplit of exp * typ * context_branch list
and suffices_arg = Syncom.Location.t * typ * proof
and context_branch = context_case split_branch
and 'b split_branch =
  1. | SplitBranch of 'b * gctx * pattern * LF.msub * hypothetical

A general branch of a case analysis.

and hypothetical =
  1. | Hypothetical of Syncom.Location.t * hypotheses * proof

A hypothetical derivation lists meta-hypotheses and hypotheses, then proceeds with a proof.

An open subgoal is a proof state together with a reference ot the theorem in which it occurs.

val make_proof_state : SubgoalPath.builder -> tclo -> proof_state

Generates a unsolved subgoal with the given goal in an empty context, with no label.

val incomplete_proof : Syncom.Location.t -> proof_state -> proof

Smart constructor for an unfinished proof ending.

val intros : hypotheses -> proof -> proof

Smart constructor for the intros directive.

val suffices : exp -> suffices_arg list -> proof
val proof_cons : command -> proof -> proof
val solve : exp -> proof
val context_split : exp -> typ -> context_branch list -> proof
val context_branch : context_case -> (gctx * pattern) -> LF.msub -> hypotheses -> proof -> context_branch
val meta_split : exp -> typ -> meta_branch list -> proof
val impossible_split : exp -> proof
val meta_branch : meta_branch_label -> (gctx * pattern) -> LF.msub -> hypotheses -> proof -> meta_branch
val comp_split : exp -> typ -> comp_branch list -> proof
val prepend_commands : command list -> proof -> proof

Gives a more convenient way of writing complex proofs by using list syntax.

val name_of_ctyp_decl : ctyp_decl -> Syncom.Name.t
val metavariable_of_exp : exp -> (Syncom.Id.offset * Syncom.Id.offset option) option

Decides whether the computational term is actually a variable index object. See `LF.variable_of_mfront`.

val variable_of_exp : exp -> Syncom.Id.offset option
type thm =
  1. | Proof of proof
  2. | Program of exp
type env =
  1. | Empty
  2. | Cons of value * env
and value =
  1. | FnValue of Syncom.Name.t * exp * LF.msub * env
  2. | FunValue of fun_branches_value
  3. | ThmValue of Syncom.Id.cid_prog * thm * LF.msub * env
  4. | MLamValue of Syncom.Name.t * exp * LF.msub * env
  5. | CtxValue of Syncom.Name.t * exp * LF.msub * env
  6. | BoxValue of meta_obj
  7. | ConstValue of Syncom.Id.cid_prog
  8. | DataValue of Syncom.Id.cid_comp_const * data_spine
  9. | TupleValue of value Support.List2.t
and data_spine =
  1. | DataNil
  2. | DataApp of value * data_spine
and fun_branches_value =
  1. | NilValBranch
  2. | ConsValBranch of pattern_spine * exp * LF.msub * env * fun_branches_value