package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module ConstrSource

This file defines the most important datatype of Rocq, namely kernel terms, as well as a handful of generic manipulation functions.

Simply type aliases

Sourcetype metavariable = int

Existential variables

Sourcetype case_style =
  1. | LetStyle
  2. | IfStyle
  3. | LetPatternStyle
  4. | MatchStyle
  5. | RegularStyle
    (*

    infer printing form from number of constructor

    *)

Case annotation

Sourcetype case_printing = {
  1. style : case_style;
}
Sourcetype case_info = {
  1. ci_ind : Names.inductive;
  2. ci_npar : int;
  3. ci_cstr_ndecls : int array;
  4. ci_cstr_nargs : int array;
  5. ci_pp_info : case_printing;
}
The type of constructions
Sourcetype t
Sourcetype constr = t

types is the same as constr but is intended to be used for documentation to indicate that such or such function specifically works with types (i.e. terms of type a sort). (Rem:plurial form since type is a reserved ML keyword)

Sourcetype types = constr
Functions for dealing with constr terms.

The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones.

Term constructors.
Sourceval mkRel : int -> constr

Constructs a de Bruijn index (DB indices begin at 1)

Sourceval mkVar : Names.Id.t -> constr

Constructs a Variable

Sourceval mkInt : Uint63.t -> constr

Constructs a machine integer

Sourceval mkArray : (UVars.Instance.t * constr array * constr * types) -> constr

Constructs an array

Sourceval mkFloat : Float64.t -> constr

Constructs a machine float number

Sourceval mkString : Pstring.t -> constr

Constructs a machine string.

Sourceval mkMeta : metavariable -> constr

Constructs an patvar named "?n"

Sourcetype existential = Evar.t * constr SList.t

Constructs an existential variable

Sourceval mkEvar : existential -> constr
Sourceval mkSort : Sorts.t -> types

Construct a sort

Sourceval mkSProp : types
Sourceval mkProp : types
Sourceval mkSet : types
Sourcetype cast_kind =
  1. | VMcast
  2. | NATIVEcast
  3. | DEFAULTcast

This defines the strategy to use for verifiying a Cast

Sourceval mkCast : (constr * cast_kind * constr) -> constr

Constructs the term t1::t2, i.e. the term t1 casted with the type t2 (that means t2 is declared as the type of t1).

Sourcetype 'a binder_annot = ('a, Sorts.relevance) Context.pbinder_annot

Constructs the product (x:t1)t2

Constructs the abstraction [x:t1]t2

Constructs the product let x = t1 : t2 in t3

Sourceval mkApp : (constr * constr array) -> constr

mkApp (f, [|t1; ...; tN|] constructs the application (f t1 ... tn) .

Sourceval map_puniverses : ('a -> 'b) -> 'a UVars.puniverses -> 'b UVars.puniverses
Sourceval mkConstU : pconstant -> constr

Constructs a Constant.t

Constructs a projection application

Inductive types

Sourceval mkIndU : pinductive -> constr

Constructs the ith (co)inductive type of the block named kn

Sourceval mkConstructU : pconstructor -> constr

Constructs the jth constructor of the ith (co)inductive type of the block named kn.

Sourceval mkConstructUi : (pinductive * int) -> constr

Make a constant, inductive, constructor or variable.

Sourcemodule UnsafeMonomorphic : sig ... end

Constructs a destructor of inductive type.

mkCase ci params p c ac stand for match c as x in I args return p with ac presented as describe in ci.

p structure is args x |- "return clause"

acith element is ith constructor case presented as construct_args |- case_term

Sourcetype ('constr, 'r) pcase_branch = (Names.Name.t, 'r) Context.pbinder_annot array * 'constr

Names bound by matching the constructor for this branch.

Sourcetype ('types, 'r) pcase_return = ((Names.Name.t, 'r) Context.pbinder_annot array * 'types) * 'r

Names of the indices + name of self

Sourcetype 'constr pcase_invert =
  1. | NoInvert
    (*

    Normal reduction: match when the scrutinee is a constructor.

    *)
  2. | CaseInvert of {
    1. indices : 'constr array;
    }
    (*

    SProp to non SProp only: No constructors or reduce when the indices match those of the unique constructor.

    *)
Sourcetype ('constr, 'types, 'univs, 'r) pcase = case_info * 'univs * 'constr array * ('types, 'r) pcase_return * 'constr pcase_invert * 'constr * ('constr, 'r) pcase_branch array
Sourcetype case_invert = constr pcase_invert
Sourceval mkCase : case -> constr
Sourcetype ('constr, 'types, 'r) prec_declaration = (Names.Name.t, 'r) Context.pbinder_annot array * 'types array * 'constr array

If recindxs = [|i1,...in|] funnames = [|f1,.....fn|] typarray = [|t1,...tn|] bodies = [|b1,.....bn|] then mkFix ((recindxs,i), funnames, typarray, bodies) constructs the $ i $ th function of the block (counting from 0)

Fixpoint f1 [ctx1] = b1 with f2 [ctx2] = b2 ... with fn [ctxn] = bn.

where the length of the $ j $ th context is $ ij $ .

Sourcetype ('constr, 'types, 'r) pfixpoint = (int array * int) * ('constr, 'types, 'r) prec_declaration

The array of int's tells for each component of the array of mutual fixpoints the number of lambdas to skip before finding the recursive argument (e.g., value is 2 in "fix f (x:A) (y:=t) (z:B) (v:=u) (w:I) struct w"), telling to skip x and z and that w is the recursive argument); The second component int tells which component of the block is returned

Sourcetype ('constr, 'types, 'r) pcofixpoint = int * ('constr, 'types, 'r) prec_declaration

The component int tells which component of the block of cofixpoint is returned

Sourceval mkFix : fixpoint -> constr

If funnames = [|f1,.....fn|] typarray = [|t1,...tn|] bodies = [b1,.....bn] then mkCoFix (i, (funnames, typarray, bodies)) constructs the ith function of the block

CoFixpoint f1 = b1 with f2 = b2 ... with fn = bn.

Sourceval mkCoFix : cofixpoint -> constr
Concrete type for making pattern-matching.
Sourcetype 'constr pexistential = Evar.t * 'constr SList.t

constr list is an instance matching definitional named_context in the same order (i.e. last argument first)

Sourcetype ('constr, 'types, 'sort, 'univs, 'r) kind_of_term =
  1. | Rel of int
    (*

    Gallina-variable introduced by forall, fun, let-in, fix, or cofix.

    *)
  2. | Var of Names.Id.t
    (*

    Gallina-variable that was introduced by Vernacular-command that extends the local context of the currently open section (i.e. Variable or Let).

    *)
  3. | Meta of metavariable
  4. | Evar of 'constr pexistential
  5. | Sort of 'sort
  6. | Cast of 'constr * cast_kind * 'types
  7. | Prod of (Names.Name.t, 'r) Context.pbinder_annot * 'types * 'types
    (*

    Concrete syntax "forall A:B,C" is represented as Prod (A,B,C).

    *)
  8. | Lambda of (Names.Name.t, 'r) Context.pbinder_annot * 'types * 'constr
    (*

    Concrete syntax "fun A:B => C" is represented as Lambda (A,B,C).

    *)
  9. | LetIn of (Names.Name.t, 'r) Context.pbinder_annot * 'constr * 'types * 'constr
    (*

    Concrete syntax "let A:C := B in D" is represented as LetIn (A,B,C,D).

    *)
  10. | App of 'constr * 'constr array
    (*

    Concrete syntax "(F P1 P2 ... Pn)" is represented as App (F, [|P1; P2; ...; Pn|]). The mkApp constructor also enforces the following invariant:

    • F itself is not App
    • and [|P1;..;Pn|] is not empty.
    *)
  11. | Const of Names.Constant.t * 'univs
    (*

    Gallina-variable that was introduced by Vernacular-command that extends the global environment (i.e. Parameter, or Axiom, or Definition, or Theorem, or Symbol etc.)

    *)
  12. | Ind of Names.inductive * 'univs
    (*

    A name of an inductive type defined by Variant, Inductive or Record Vernacular-commands.

    *)
  13. | Construct of Names.constructor * 'univs
    (*

    A constructor of an inductive type defined by Variant, Inductive or Record Vernacular-commands.

    *)
  14. | Case of case_info * 'univs * 'constr array * ('types, 'r) pcase_return * 'constr pcase_invert * 'constr * ('constr, 'r) pcase_branch array
    (*

    Case (ci,u,params,p,iv,c,brs) is a match c return p with brs expression. c lives in inductive ci.ci_ind at universe instance u and parameters params. If this match has case inversion (ie match on a 1 constructor SProp inductive with proof relevant return type) the indices are in iv.

    The names in p are the names of the bound indices and inductive value (ie the in and as clauses).

    The names in the brs are the names of the variables bound in the respective branch.

    *)
  15. | Fix of ('constr, 'types, 'r) pfixpoint
  16. | CoFix of ('constr, 'types, 'r) pcofixpoint
  17. | Proj of Names.Projection.t * 'r * 'constr
    (*

    The relevance is the relevance of the whole term

    *)
  18. | Int of Uint63.t
  19. | Float of Float64.t
  20. | String of Pstring.t
  21. | Array of 'univs * 'constr array * 'constr * 'types
    (*

    Array (u,vals,def,t) is an array of vals in type t with default value def. u is a universe containing t.

    *)

User view of constr. For App, it is ensured there is at least one argument and the function is not itself an applicative term

Sourceval kind_nocast_gen : ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> 'v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term
Sourceval isRel : constr -> bool

Simple case analysis

Sourceval isRelN : int -> constr -> bool
Sourceval isVar : constr -> bool
Sourceval isVarId : Names.Id.t -> constr -> bool
Sourceval isRef : constr -> bool
Sourceval isRefX : Names.GlobRef.t -> constr -> bool
Sourceval isInd : constr -> bool
Sourceval isEvar : constr -> bool
Sourceval isMeta : constr -> bool
Sourceval isEvar_or_Meta : constr -> bool
Sourceval isSort : constr -> bool
Sourceval isCast : constr -> bool
Sourceval isApp : constr -> bool
Sourceval isLambda : constr -> bool
Sourceval isLetIn : constr -> bool
Sourceval isProd : constr -> bool
Sourceval isConst : constr -> bool
Sourceval isConstruct : constr -> bool
Sourceval isFix : constr -> bool
Sourceval isCoFix : constr -> bool
Sourceval isCase : constr -> bool
Sourceval isProj : constr -> bool
Sourceval is_Prop : constr -> bool
Sourceval is_Set : constr -> bool
Sourceval isprop : constr -> bool
Sourceval is_Type : constr -> bool
Sourceval iskind : constr -> bool
Sourceval is_small : Sorts.t -> bool
Term destructors

Destructor operations are partial functions and

  • raises DestKO

    if the term has not the expected form.

Sourceexception DestKO
Sourceval destRel : constr -> int

Destructs a de Bruijn index

Sourceval destMeta : constr -> metavariable

Destructs an existential variable

Sourceval destVar : constr -> Names.Id.t

Destructs a variable

Sourceval destSort : constr -> Sorts.t

Destructs a sort. is_Prop recognizes the sort Prop, whether isprop recognizes both Prop and Set.

Sourceval destCast : constr -> constr * cast_kind * constr

Destructs a casted term

Destructs the product $ (x:t_1)t_2 $

Destructs the abstraction $ x:t_1t_2 $

Destructs the let $ x:=b:t_1t_2 $

Sourceval destApp : constr -> constr * constr array

Destructs an application

Sourceval decompose_app_list : constr -> constr * constr list

Decompose any term as an applicative term; the list of args can be empty

Sourceval decompose_app : constr -> constr * constr array

Same as decompose_app, but returns an array.

Destructs a constant

Sourceval destEvar : constr -> existential

Destructs an existential variable

Destructs a (co)inductive type

Destructs a constructor

Sourceval destCase : constr -> case

Destructs a match c as x in I args return P with ... | Ci(...yij...) => ti | ... end (or let (..y1i..) := c as x in I args return P in t1, or if c then t1 else t2)

  • returns

    (info,c,fun args x => P,[|...|fun yij => ti| ...|]) where info is pretty-printing information

Destructs a projection

Sourceval destFix : constr -> fixpoint

Destructs the $ i $ th function of the block Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} with f{_ 2} ctx{_ 2} = b{_ 2} ... with f{_ n} ctx{_ n} = b{_ n}, where the length of the $ j $ th context is $ ij $ .

Sourceval destCoFix : constr -> cofixpoint
Equality
Sourceval equal : constr -> constr -> bool

equal a b is true if a equals b modulo alpha, casts, and application grouping

Sourceval eq_constr_univs : constr UGraph.check_function

eq_constr_univs u a b is true if a equals b modulo alpha, casts, application grouping and the universe equalities in u.

Sourceval leq_constr_univs : constr UGraph.check_function

leq_constr_univs u a b is true if a is convertible to b modulo alpha, casts, application grouping and the universe inequalities in u.

Sourceval eq_constr_nounivs : constr -> constr -> bool

eq_constr_univs a b true, c if a equals b modulo alpha, casts, application grouping and ignoring universe instances.

Sourceval compare : constr -> constr -> int

Total ordering compatible with equal

Extension of Context with declarations on constr
Sourcetype rel_context = rel_declaration list
Sourcetype named_context = named_declaration list
Sourcetype compacted_context = compacted_declaration list
Relocation and substitution
Sourceval exliftn : Esubst.lift -> constr -> constr

exliftn el c lifts c with lifting el

Sourceval liftn : int -> int -> constr -> constr

liftn n k c lifts by n indexes above or equal to k in c

Sourceval lift : int -> constr -> constr

lift n c lifts by n the positive indexes in c

Functionals working on expressions canonically abstracted over a local context (possibly with let-ins)

map_branches f br maps f on the immediate subterms of an array of "match" branches br in canonical eta-let-expanded form; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of each branch

Sourceval map_branches : (constr -> constr) -> case_branch array -> case_branch array

map_return_predicate f p maps f on the immediate subterms of a return predicate of a "match" in canonical eta-let-expanded form; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of the predicate

Sourceval map_return_predicate : (constr -> constr) -> case_return -> case_return

map_branches_with_binders f br maps f on the immediate subterms of an array of "match" branches br in canonical eta-let-expanded form; it carries an extra data n (typically a lift index) which is processed by g (which typically adds 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of the branch as well as the body of the branch

Sourceval map_branches_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_branch array -> case_branch array

map_return_predicate_with_binders f p maps f on the immediate subterms of a return predicate of a "match" in canonical eta-let-expanded form; it carries an extra data n (typically a lift index) which is processed by g (which typically adds 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified; it preserves sharing; the immediate subterms are the types and possibly terms occurring in the context of each branch as well as the body of the predicate

Sourceval map_return_predicate_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> case_return -> case_return
Functionals working on the immediate subterm of a construction

fold f acc c folds f on the immediate subterms of c starting from acc and proceeding from left to right according to the usual representation of the constructions; it is not recursive

Sourceval fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a
Sourceval fold_invert : ('a -> 'b -> 'a) -> 'a -> 'b pcase_invert -> 'a

map f c maps f on the immediate subterms of c; it is not recursive and the order with which subterms are processed is not specified

Sourceval map : (constr -> constr) -> constr -> constr
Sourceval map_invert : ('a -> 'a) -> 'a pcase_invert -> 'a pcase_invert

Like map, but also has an additional accumulator.

Sourceval fold_map : ('a -> constr -> 'a * constr) -> 'a -> constr -> 'a * constr
Sourceval fold_map_invert : ('a -> 'b -> 'a * 'b) -> 'a -> 'b pcase_invert -> 'a * 'b pcase_invert

map_with_binders g f n c maps f n on the immediate subterms of c; it carries an extra data n (typically a lift index) which is processed by g (which typically add 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified

Sourceval map_with_binders : ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr

iter f c iters f on the immediate subterms of c; it is not recursive and the order with which subterms are processed is not specified

Sourceval iter : (constr -> unit) -> constr -> unit
Sourceval iter_invert : ('a -> unit) -> 'a pcase_invert -> unit

iter_with_binders g f n c iters f n on the immediate subterms of c; it carries an extra data n (typically a lift index) which is processed by g (which typically add 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified

Sourceval iter_with_binders : ('a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit

iter_with_binders g f n c iters f n on the immediate subterms of c; it carries an extra data n (typically a lift index) which is processed by g (which typically add 1 to n) at each binder traversal; it is not recursive and the order with which subterms are processed is not specified

Sourceval fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
Sourcetype 'constr constr_compare_fn = int -> 'constr -> 'constr -> bool

compare_head f c1 c2 compare c1 and c2 using f to compare the immediate subterms of c1 of c2 if needed; Cast's, binders name and Cases annotations are not taken into account

Sourcetype 'univs instance_compare_fn = (Names.GlobRef.t * int) option -> 'univs -> 'univs -> bool

Convert a global reference applied to 2 instances. The int says how many arguments are given (as we can only use cumulativity for fully applied inductives/constructors) .

compare_head_gen u s f c1 c2 compare c1 and c2 using f to compare the immediate subterms of c1 of c2 if needed, u to compare universe instances, s to compare sorts; Cast's, binders name and Cases annotations are not taken into account

Sourceval compare_head_gen_leq_with : ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> ('v pexistential -> 'v pexistential -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn -> 'v constr_compare_fn
Sourceval compare_head_gen_with : ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> ('v -> ('v, 'v, 'sort, 'univs, 'r) kind_of_term) -> 'univs instance_compare_fn -> ('sort -> 'sort -> bool) -> ('v pexistential -> 'v pexistential -> bool) -> 'v constr_compare_fn -> 'v constr_compare_fn

compare_head_gen_with k1 k2 u s f c1 c2 compares c1 and c2 like compare_head_gen u s f c1 c2, except that k1 (resp. k2) is used,rather than kind, to expose the immediate subterms of c1 (resp. c2).

compare_head_gen_leq u s f fle c1 c2 compare c1 and c2 using f to compare the immediate subterms of c1 of c2 for conversion, fle for cumulativity, u to compare universe instances (the first boolean tells if they belong to a Constant.t), s to compare sorts for for subtyping; Cast's, binders name and Cases annotations are not taken into account

Sourceval eq_invert : ('a -> 'a -> bool) -> 'a pcase_invert -> 'a pcase_invert -> bool
Hashconsing
Sourceval hash : constr -> int
Sourceval case_info_hash : case_info -> int
Sourcemodule GenHCons (C : sig ... end) : sig ... end
Sourceval hcons : constr -> constr
Sourceval hasheq_kind : (_, _, _, _, _) kind_of_term as 'k -> 'k -> bool

Checks physical equality of every immediate element (goes inside tuples and arrays)

Sourceval debug_print : constr -> Pp.t
Sourceval debug_print_fix : ('a -> Pp.t) -> ('a, 'a, 'r) pfixpoint -> Pp.t
  • deprecated (8.18) Use [mkConstU] or if truly needed [UnsafeMonomorphic.mkConst]
  • deprecated (8.18) Use [mkIndU] or if truly needed [UnsafeMonomorphic.mkInd]
Sourceval mkConstruct : Names.constructor -> constr
  • deprecated (8.18) Use [mkConstructU] or if truly needed [UnsafeMonomorphic.mkConstruct]
Sourceval hcons_caseinfo : case_info -> case_info
Sourceval hash_cast_kind : cast_kind -> int
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct