Module Frontend.ConcreteSyntax

include module type of ConcreteSyntaxData
type info = Basis.LexingUtil.span option
val pp_info : Stdlib.Format.formatter -> Basis.LexingUtil.span option -> unit
type 'a node = {
  1. node : 'a;
  2. info : info;
}
val pp_node : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'a node -> Ppx_deriving_runtime.unit
val show_node : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> 'a node -> Ppx_deriving_runtime.string
type hole = {
  1. name : string option;
  2. silent : bool;
}
val pp_hole : Ppx_deriving_runtime.Format.formatter -> hole -> Ppx_deriving_runtime.unit
val show_hole : hole -> Ppx_deriving_runtime.string
val map_node : f:('a -> 'b) -> 'c node -> 'd node
val get_info : 'a node -> info
type cell =
  1. | Cell of {
    1. names : Core.Ident.t list;
    2. tp : con;
    }
and con = con_ node
and con_ =
  1. | Var of Core.Ident.t
  2. | DeBruijnLevel of int
  3. | Let of con * Core.Ident.t * con
  4. | Ann of {
    1. term : con;
    2. tp : con;
    }
  5. | Nat
  6. | Suc of con
  7. | Lit of int
  8. | Circle
  9. | Base
  10. | Loop of con
  11. | Pi of cell list * con
  12. | Lam of Core.Ident.t list * con
  13. | Ap of con * con list
  14. | Sg of cell list * con
  15. | Signature of field list
  16. | Struct of field list
  17. | Proj of con * Core.Ident.t
  18. | Patch of con * patch_field list
  19. | Open of con * (Core.Ident.user * Core.Ident.user) list * con
  20. | Sub of con * con * con
  21. | Pair of con * con
  22. | Fst of con
  23. | Snd of con
  24. | Type
  25. | Hole of hole * con option
  26. | BoundaryHole of con option
  27. | Visualize
  28. | Underscore
  29. | Generalize of Core.Ident.t * con
  30. | Unfold of Core.Ident.t list * con
  31. | Abstract of Core.Ident.t option * con
  32. | Elim of {
    1. mot : con;
    2. cases : case list;
    3. scrut : con;
    }
  33. | Rec of {
    1. mot : con;
    2. cases : case list;
    3. scrut : con;
    }
  34. | LamElim of case list
  35. | Equations of {
    1. code : con;
    2. eqns : eqns step;
    }
  36. | Dim
  37. | Cof
  38. | CofEq of con * con
  39. | CofLe of con * con
  40. | Join of con list
  41. | Meet of con list
  42. | CofBoundary of con
  43. | Prf of con
  44. | CofSplit of (con * con) list
  45. | Ext of Core.Ident.t list * con * (con * con) list
  46. | Coe of con * con * con * con
  47. | TopC
  48. | BotC
  49. | HCom of con * con * con * con * con
  50. | HComChk of con * con * con
  51. | HFill of con * con * con * con
  52. | HFillChk of con * con
  53. | Com of con * con * con * con * con
  54. | V of con * con * con * con
  55. | VProj of con
  56. | Cap of con
  57. | ModAll
  58. | ModOnly of string list
  59. | ModRename of string list * string list
  60. | ModNone
  61. | ModExcept of string list
  62. | ModSeq of con list
  63. | ModUnion of con list
  64. | ModInSubtree of string list * con
  65. | ModPrint of hole
and case = pat * con
and field = [
  1. | `Field of Core.Ident.user * con
  2. | `Include of con * (Core.Ident.user * Core.Ident.user) list
]
and patch_field = [
  1. | `Patch of Core.Ident.user * con
  2. | `Subst of Core.Ident.user * con
]
and pat =
  1. | Pat of {
    1. lbl : string list;
    2. args : pat_arg list;
    }
and pat_arg = [
  1. | `Simple of Core.Ident.t
  2. | `Inductive of Core.Ident.t * Core.Ident.t
]
and 'a step =
  1. | Equals of con * con * 'a
  2. | Trivial of con * 'a
and eqns =
  1. | Step of eqns step
  2. | Qed of con
val pp_cell : Ppx_deriving_runtime.Format.formatter -> cell -> Ppx_deriving_runtime.unit
val show_cell : cell -> Ppx_deriving_runtime.string
val pp_con_ : Ppx_deriving_runtime.Format.formatter -> con_ -> Ppx_deriving_runtime.unit
val show_con_ : con_ -> Ppx_deriving_runtime.string
val pp_case : Ppx_deriving_runtime.Format.formatter -> case -> Ppx_deriving_runtime.unit
val show_case : case -> Ppx_deriving_runtime.string
val pp_field : Ppx_deriving_runtime.Format.formatter -> field -> Ppx_deriving_runtime.unit
val show_field : field -> Ppx_deriving_runtime.string
val pp_patch_field : Ppx_deriving_runtime.Format.formatter -> patch_field -> Ppx_deriving_runtime.unit
val show_patch_field : patch_field -> Ppx_deriving_runtime.string
val pp_pat : Ppx_deriving_runtime.Format.formatter -> pat -> Ppx_deriving_runtime.unit
val show_pat : pat -> Ppx_deriving_runtime.string
val pp_pat_arg : Ppx_deriving_runtime.Format.formatter -> pat_arg -> Ppx_deriving_runtime.unit
val show_pat_arg : pat_arg -> Ppx_deriving_runtime.string
val pp_step : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> Ppx_deriving_runtime.Format.formatter -> 'a step -> Ppx_deriving_runtime.unit
val show_step : 'a. (Ppx_deriving_runtime.Format.formatter -> 'a -> Ppx_deriving_runtime.unit) -> 'a step -> Ppx_deriving_runtime.string
val pp_eqns : Ppx_deriving_runtime.Format.formatter -> eqns -> Ppx_deriving_runtime.unit
val show_eqns : eqns -> Ppx_deriving_runtime.string
type decl = decl_ node
and decl_ =
  1. | Def of {
    1. abstract : bool;
    2. shadowing : bool;
    3. name : Core.Ident.t;
    4. args : cell list;
    5. def : con;
    6. tp : con;
    7. unfolding : Core.Ident.t list;
    }
  2. | Axiom of {
    1. shadowing : bool;
    2. name : Core.Ident.t;
    3. args : cell list;
    4. tp : con;
    }
  3. | Print of {
    1. unfolding : Core.Ident.t list;
    2. name : Core.Ident.t node;
    }
  4. | Import of {
    1. shadowing : bool;
    2. unitpath : string list;
    3. modifier : con option;
    }
  5. | NormalizeTerm of {
    1. unfolding : Core.Ident.t list;
    2. con : con;
    }
  6. | Fail of decl
  7. | Debug of bool
  8. | Quit
  9. | View of {
    1. shadowing : bool;
    2. modifier : con;
    }
  10. | Export of {
    1. shadowing : bool;
    2. modifier : con;
    }
  11. | Repack of {
    1. shadowing : bool;
    2. modifier : con;
    }
  12. | Section of {
    1. shadowing : bool;
    2. prefix : string list option;
    3. decls : signature;
    4. modifier : con option;
    }
and signature = decl list
val pp_decl : Ppx_deriving_runtime.Format.formatter -> decl -> Ppx_deriving_runtime.unit
val show_decl : decl -> Ppx_deriving_runtime.string
val pp_decl_ : Ppx_deriving_runtime.Format.formatter -> decl_ -> Ppx_deriving_runtime.unit
val show_decl_ : decl_ -> Ppx_deriving_runtime.string
val pp_signature : Ppx_deriving_runtime.Format.formatter -> signature -> Ppx_deriving_runtime.unit
val show_signature : signature -> Ppx_deriving_runtime.string
type repl_command = repl_command_ node
and repl_command_ =
  1. | NoOp
  2. | EndOfFile
  3. | Decl of decl
val show_con : con -> string
val pp_con : Stdlib.Format.formatter -> con -> unit