diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 07:42:16 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 23:26:19 +0100 |
commit | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (patch) | |
tree | 73ce61804aae0e16b1a30994affd75a59ed08efe /pretyping/geninterp.mli | |
parent | eb91ccaf236bc9a60a1e216b76a0a42980c072a7 (diff) |
[api] Miscellaneous consolidation + moves to engine.
We deprecate a few functions that were deprecated in the comments plus
we place `Nameops` and `Univops` in engine where they do seem to
belong in the large picture of code organization.
Diffstat (limited to 'pretyping/geninterp.mli')
-rw-r--r-- | pretyping/geninterp.mli | 72 |
1 files changed, 72 insertions, 0 deletions
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli new file mode 100644 index 000000000..ae0b26e59 --- /dev/null +++ b/pretyping/geninterp.mli @@ -0,0 +1,72 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Interpretation functions for generic arguments and interpreted Ltac + values. *) + +open Names +open Genarg + +(** {6 Dynamic toplevel values} *) + +module Val : +sig + type 'a typ + + val create : string -> 'a typ + + type _ tag = + | Base : 'a typ -> 'a tag + | List : 'a tag -> 'a list tag + | Opt : 'a tag -> 'a option tag + | Pair : 'a tag * 'b tag -> ('a * 'b) tag + + type t = Dyn : 'a typ * 'a -> t + + val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option + val repr : 'a typ -> string + val pr : 'a typ -> Pp.t + + val typ_list : t list typ + val typ_opt : t option typ + val typ_pair : (t * t) typ + + val inject : 'a tag -> 'a -> t + +end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + +(** Dynamic types for toplevel values. While the generic types permit to relate + objects at various levels of interpretation, toplevel values are wearing + their own type regardless of where they came from. This allows to use the + same runtime representation for several generic types. *) + +val val_tag : 'a typed_abstract_argument_type -> 'a Val.tag +(** Retrieve the dynamic type associated to a toplevel genarg. *) + +val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> unit +(** Register the representation of a generic argument. If no tag is given as + argument, a new fresh tag with the same name as the argument is associated + to the generic type. *) + +(** {6 Interpretation functions} *) + +module TacStore : Store.S + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, Val.t) interp_fun -> unit |