simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

more docs

Browse source
This commit is contained in:
Simon Cruanes 2021-06-11 19:01:31 -04:00
parent dcbc4d4a59
commit fbc3ec7ed6
1 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/th-data/Sidekick_th_data.mli
View file

@ -1,14 +1,19 @@
(** Theory for datatypes. *)
(** Datatype-oriented view of terms.
['c] is the representation of constructors
['t] is the representation of terms
- ['c] is the representation of constructors
- ['t] is the representation of terms
*)
type ('c,'t) data_view =
| T_cstor of 'c * 't IArray.t
| T_cstor of 'c * 't IArray.t (** [T_cstor (c,args)] is the term [c(args)] *)
| T_select of 'c * int * 't
| T_is_a of 'c * 't
| T_other of 't
(** [T_select (c,i,u)] means the [i]-th argument of [u], which should
start with constructor [c] *)
| T_is_a of 'c * 't (** [T_is_a (c,u)] means [u] starts with constructor [c] *)
| T_other of 't (** non-datatype term *)
(* TODO: use ['ts] rather than IArray? *)
(** View of types in a way that is directly useful for the theory of datatypes *)
type ('c, 'ty) data_ty_view =