Comp (beluga.Synapx.Comp)

type unbox_modifier = [

| `Strengthened

]

type case_pragma = Synint.Comp.case_pragma =

| PragmaCase
| PragmaNotCase

type context_case = Synint.Comp.context_case =

| EmptyContext of Syncom.Location.t
| ExtendedBy of Syncom.Location.t * int

type case_label = Synint.Comp.case_label =

| Lf_constant of Syncom.Location.t * Syncom.Name.t * Syncom.Id.cid_term
| Comp_constant of Syncom.Location.t * Syncom.Name.t * Syncom.Id.cid_comp_const
| BVarCase of Syncom.Location.t
| ContextCase of context_case
| PVarCase of Syncom.Location.t * int * int option

type 'a generic_order = 'a Synint.Comp.generic_order =

| Arg of 'a
| Lex of 'a generic_order list
| Simul of 'a generic_order list

type 'a generic_suffices_typ = [

| `exact of 'a
| `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 =

| Ctype of Syncom.Location.t
| PiKind of Syncom.Location.t * LF.ctyp_decl * kind

type meta_typ = Syncom.Location.t * LF.ctyp

type meta_obj = Syncom.Location.t * LF.mfront

type meta_spine =

| MetaNil
| MetaApp of meta_obj * meta_spine

type typ =

| TypBase of Syncom.Location.t * Syncom.Id.cid_comp_typ * meta_spine
| TypCobase of Syncom.Location.t * Syncom.Id.cid_comp_cotyp * meta_spine
| TypDef of Syncom.Location.t * Syncom.Id.cid_comp_typdef * meta_spine
| TypBox of Syncom.Location.t * meta_typ
| TypArr of Syncom.Location.t * typ * typ
| TypCross of Syncom.Location.t * typ Support.List2.t
| TypPiBox of Syncom.Location.t * LF.ctyp_decl * typ
| TypInd of typ

and exp =

| Fn of Syncom.Location.t * Syncom.Name.t * exp
| Fun of Syncom.Location.t * fun_branches
| MLam of Syncom.Location.t * Syncom.Name.t * exp
| Tuple of Syncom.Location.t * exp Support.List2.t
| LetTuple of Syncom.Location.t * exp * Syncom.Name.t Support.List2.t * exp
| Let of Syncom.Location.t * exp * Syncom.Name.t * exp
| Box of Syncom.Location.t * meta_obj
| Case of Syncom.Location.t * case_pragma * exp * branch list
| Impossible of Syncom.Location.t * exp
| Hole of Syncom.Location.t * string option
| BoxHole of Syncom.Location.t
| Var of Syncom.Location.t * Syncom.Id.offset
| DataConst of Syncom.Location.t * Syncom.Id.cid_comp_const
| Obs of Syncom.Location.t * exp * Syncom.Id.cid_comp_dest
| Const of Syncom.Location.t * Syncom.Id.cid_prog
| Apply of Syncom.Location.t * exp * exp
| Ann of Syncom.Location.t * exp * typ

Computation-level terms

and pattern =

| PatMetaObj of Syncom.Location.t * meta_obj
| PatConst of Syncom.Location.t * Syncom.Id.cid_comp_const * pattern_spine
| PatFVar of Syncom.Location.t * Syncom.Name.t
| PatVar of Syncom.Location.t * Syncom.Name.t * Syncom.Id.offset
| PatTuple of Syncom.Location.t * pattern Support.List2.t
| PatAnn of Syncom.Location.t * pattern * typ

and pattern_spine =

| PatNil of Syncom.Location.t
| PatApp of Syncom.Location.t * pattern * pattern_spine
| PatObs of Syncom.Location.t * Syncom.Id.cid_comp_dest * pattern_spine

and branch =

| Branch of Syncom.Location.t * LF.ctyp_decl LF.ctx * pattern * exp

and fun_branches =

| NilFBranch of Syncom.Location.t
| ConsFBranch of Syncom.Location.t * pattern_spine * exp * fun_branches

type ctyp_decl =

| CTypDecl of Syncom.Name.t * typ

type gctx = ctyp_decl LF.ctx

type hypotheses = {

cD : LF.mctx;
cG : gctx;

}

type proof =

| Incomplete of Syncom.Location.t * string option
| Command of Syncom.Location.t * command * proof
| Directive of Syncom.Location.t * directive

and command =

| By of Syncom.Location.t * exp * Syncom.Name.t
| Unbox of Syncom.Location.t * exp * Syncom.Name.t * unbox_modifier option

and directive =

| Intros of Syncom.Location.t * hypothetical
| Solve of Syncom.Location.t * exp
| Split of Syncom.Location.t * exp * split_branch list
| Suffices of Syncom.Location.t * exp * suffices_arg list

and suffices_arg = Syncom.Location.t * typ * proof

and split_branch = {

case_label : case_label;
branch_body : hypothetical;
split_branch_loc : Syncom.Location.t;

}

and hypothetical = {

hypotheses : hypotheses;
proof : proof;
hypothetical_loc : Syncom.Location.t;

}

type thm =

| Program of exp
| Proof of proof

val loc_of_exp : exp -> Syncom.Location.t