module Typed_ast: sig
.. end
Sets of Names
module NameSet: Set.S
with type elt = Name.t and type t = Set.Make(Name).t
Sets of Names
module Nfmap: Finite_map.Fmap
with type k = Name.t
Name keyed finite maps
val nfmap_domain : 'a Nfmap.t -> NameSet.t
type
name_l = Name.lskips_t * Ast.l
type
lskips = Ast.lex_skips
Whitespace, comments, and newlines
type 'a
lskips_seplist = ('a, lskips) Seplist.t
val no_lskips : lskips
The empty lskip
val space : lskips
A space lskip
: lskips list -> lskips
Get only the comments (and a trailing space)
: lskips list -> lskips
Get the first lskip of the list and only comments from the rest
type
env_tag =
| |
K_let |
| |
K_field |
| |
K_constr |
| |
K_relation |
| |
K_method |
| |
K_instance |
env_tag
is used by const_descr
to describe the type of constant. Constants can be defined in multiple ways:
the most common way is via a let
-statement. Record-type definitions introduce fields-accessor
functions and variant types introduce constructors. There are methods, instances and relations as well.
A let
definition can be made via a val
definition and multiple, target specific lets.
type
p_env = (Path.t * Ast.l) Nfmap.t
Maps a type name to the unique path representing that type and
the first location this type is defined
type
lit = (lit_aux, unit) Types.annot
type
lit_aux =
type
const_descr_ref = Types.const_descr_ref
type
name_kind =
type
pat = (pat_aux, pat_annot) Types.annot
type
pat_annot = {
}
type
pat_aux =
type
cr_special_fun =
| |
CR_special_uncurry of int |
| |
CR_special_rep of string list * exp list |
type
const_target_rep =
type
rel_io =
| |
Rel_mode_in |
| |
Rel_mode_out |
rel_io represents whether an argument of an inductive relation is considerred as an input or an output
type
rel_mode = rel_io list
rel_output_type specifies the type of the result
type
rel_output_type =
| |
Out_list |
| |
Out_pure |
| |
Out_option |
| |
Out_unique |
type
rel_info = {
}
rel_info represents information about functions and types genereated from this relation 0
type
const_descr = {
|
const_binding : Path.t ; |
|
const_tparams : Types.tnvar list ; |
|
const_class : (Path.t * Types.tnvar) list ; |
|
const_no_class : const_descr_ref Target.Targetmap.t ; |
|
const_ranges : Types.range list ; |
|
const_type : Types.t ; |
|
relation_info : rel_info option ; |
|
env_tag : env_tag ; |
|
const_targets : Target.Targetset.t ; |
|
spec_l : Ast.l ; |
|
target_rename : (Ast.l * Name.t) Target.Targetmap.t ; |
|
target_ascii_rep : (Ast.l * Name.t) Target.Targetmap.t ; |
|
target_rep : const_target_rep Target.Targetmap.t ; |
|
compile_message : string Target.Targetmap.t ; |
|
termination_setting : Ast.termination_setting Target.Targetmap.t ; |
}
The description of a top-level definition
type
v_env = const_descr_ref Nfmap.t
type
f_env = const_descr_ref Nfmap.t
type
m_env = Path.t Nfmap.t
type
e_env = mod_descr Types.Pfmap.t
type
c_env
local_env
represents local_environments, i.e. essentially maps from names to the entities they represent
type
local_env = {
}
type
env = {
}
type
mod_target_rep =
type
mod_descr = {
|
mod_binding : Path.t ; |
|
mod_env : local_env ; |
|
mod_target_rep : mod_target_rep Target.Targetmap.t ; |
|
mod_filename : string option ; |
|
mod_in_output : bool ; |
}
type
exp
type
exp_subst =
type
exp_aux = private
type
do_line =
type
bind_tyargs_order =
| |
BTO_input_output |
| |
BTO_output_input |
A bind constant of a monad M has type M 'a -> ('a -> M 'b) -> M 'b
.
Here, I call 'a
the input type and 'b
the output type. Depending on
how the bind constant is defined in detail its free type variable list
(stored in constant-description record, field const_tparams) might be either
of the form ['a, 'b]
or ['b, 'a]
. This type is used to distinguish the
two possibilities.
type
fexp = const_descr_ref Types.id * lskips * exp * Ast.l
type
name_lskips_annot = (Name.lskips_t, unit) Types.annot
type
quant_binding =
type
funcl_aux = name_lskips_annot * const_descr_ref *
pat list * (lskips * Types.src_t) option *
lskips * exp
type
letbind = letbind_aux * Ast.l
type
letbind_aux =
type
tyvar = lskips * Ulib.Text.t * Ast.l
type
nvar = lskips * Ulib.Text.t * Ast.l
type
tnvar =
type
texp =
Type exepressions for defining types
type
range =
type
constraints =
type
constraint_prefix =
type
typschm = constraint_prefix option * Types.src_t
type
instschm = constraint_prefix option * lskips * Ident.t * Path.t *
Types.src_t * lskips
Instance Scheme, constraint prefix, sk, class-ident as printed, resolved class-path the id points to, instantiation type, sk
val cr_special_fun_uses_name : cr_special_fun -> bool
cr_special_fun_uses_name f
checks, whether f
uses it's first argument,
i.e. whether it uses the formatted name of the constant. This information
is important to determine, whether the constant needs to be renamed.
type
targets_opt = (bool * lskips * Ast.target lskips_seplist *
lskips)
option
targets_opt is represents a set of targets. There are 3 types of values
- `None` represents the universal set, i.e. all targets
- `Some (false, sk_1, tl, sk_2)` (in source `{ t1; ...; tn }`) is the set of all targets in the list `tl`
- `Some (true, sk_1, tl, sk_2)` (in source `~{ t1; ...; tn }`) is the set of all targets not in the list `tl`
val in_targets_opt : Target.target -> targets_opt -> bool
in_targets_opt targ targets_opt
checks whether the target `targ` is in the set of targets represented by
`targets_opt`. If targ
is the a human readable target, true
is returned.
val in_target_set : Target.target -> Target.Targetset.t -> bool
in_target_set targ targetset
checks whether the target `targ` is in the set of targets
targetset
. It is intended for checking whether to output certain parts of the TAST.
Therefore, in_target_set
returns true for all human readable targets and only checks for others.
val targets_opt_to_list : targets_opt -> Target.non_ident_target list
target_opt_to_list targets_opt
returns a distinct list of all the targets in the option.
type
val_spec = lskips * name_l * const_descr_ref *
Ast.ascii_opt * lskips * typschm
type
class_val_spec = lskips * targets_opt * name_l *
const_descr_ref * Ast.ascii_opt * lskips * Types.src_t
type
fun_def_rec_flag =
| |
FR_non_rec |
| |
FR_rec of lskips |
fun_def_rec_flag
is used to encode, whether a Fun_def
is recursive. The recursive one carries some whitespace for
printing after the rec-keyword.
type
val_def =
type
name_sect =
type
indreln_rule_quant_name =
type
indreln_rule_aux =
A rule of the form Rule(clause_name_opt, sk1, sk2, bound_vars, sk3, left_hand_side_opt, sk4, rel_name, c, args)
encodes
a clause clause_name: forall bound_vars. (left_hand_side ==> rel_name args)
. c
is the reference of the relation rel_name
.
type
indreln_rule = indreln_rule_aux * Ast.l
type
indreln_witness =
Name of the witness type to be generated
type
indreln_indfn =
Name and mode of a function to be generated from an inductive relation
type
indreln_name =
Type annotation for the relation and information on what to generate from it.
RName(sk1, rel_name, rel_name_ref, sk2, rel_type, witness_opt, check_opt, indfns opt, sk3)
type
target_rep_rhs =
| |
Target_rep_rhs_infix of lskips * Ast.fixity_decl * lskips * Ident.t |
| |
Target_rep_rhs_term_replacement of exp |
| |
Target_rep_rhs_type_replacement of Types.src_t |
| |
Target_rep_rhs_special of lskips * lskips * string * exp list |
| |
Target_rep_rhs_undefined |
type
declare_def =
type
def_aux =
type
def = (def_aux * lskips option) * Ast.l * local_env
A definition consists of a the real definition represented as a def_aux
, followed by some white-space.
There is also the location of the definition and the local-environment present after the definition has been processed.
val tnvar_to_types_tnvar : tnvar -> Types.tnvar * Ast.l
val empty_local_env : local_env
val empty_env : env
val e_env_lookup : Ast.l -> e_env -> Path.t -> mod_descr
e_env_lookup l e_env p
looks up the module with path p
in
environment e_env
and returns the corresponding description. If this
lookup fails, a fatal error is thrown using location l
for the error message.
val c_env_lookup : Ast.l ->
c_env -> const_descr_ref -> const_descr
c_env_lookup l c_env c_ref
looks up the constant reference c_ref
in
environment c_env
and returns the corresponding description. If this
lookup fails, a fatal error is thrown using location l
for the error message.
val c_env_store_raw : c_env ->
const_descr -> c_env * const_descr_ref
c_env_store_raw c_env c_d
stores the description c_d
environment c_env
. Thereby, a new unique reference is generated and returned
along with the modified environment. It stores the real c_d
passed. The function
c_env_store
preprocesses c_d
to add common features like for example
capitalizing constructors for the Ocaml backend.
val c_env_update : c_env ->
const_descr_ref -> const_descr -> c_env
c_env_update c_env c_ref c_d
updates the description of constant c_ref
with
c_d
in environment c_env
.
val env_c_env_update : env ->
const_descr_ref -> const_descr -> env
env_c_env_update env c_ref c_d
updates the description of constant c_ref
with
c_d
in environment env
.
val c_env_all_consts : c_env -> const_descr_ref list
c_env_all_consts c_env
returns the constants defined in c_env
val exp_to_locn : exp -> Ast.l
val exp_to_typ : exp -> Types.t
val append_lskips : lskips -> exp -> exp
append_lskips adds new whitespace/newline/comments to the front of an
expression (before any existing whitespace/newline/comments in front of the
expression)
val pat_append_lskips : lskips -> pat -> pat
val alter_init_lskips : (lskips -> lskips * lskips) ->
exp -> exp * lskips
alter_init_lskips
finds all of the whitespace/newline/comments preceding an
expression and passes it to the supplied function in a single invocation.
The preceding whitespace/newline/comments are replaced with the fst of the
function's result, and the snd of the function's result is returned from
alter_init_lskips
val pat_alter_init_lskips : (lskips -> lskips * lskips) ->
pat -> pat * lskips
val def_aux_alter_init_lskips : (lskips -> lskips * lskips) ->
def_aux -> def_aux * lskips
val def_alter_init_lskips : (lskips -> lskips * lskips) ->
def -> def * lskips
val oi_alter_init_lskips : (lskips -> lskips * lskips) ->
Ast.open_import -> Ast.open_import * lskips
val pp_const_descr : Format.formatter -> const_descr -> unit
val pp_env : Format.formatter -> env -> unit
val pp_local_env : Format.formatter -> local_env -> unit
val pp_c_env : Format.formatter -> c_env -> unit
val pp_instances : Format.formatter -> Types.instance list Types.Pfmap.t -> unit
type
imported_modules =
type
checked_module = {
|
filename : string ; |
|
module_path : Path.t ; |
|
imported_modules : imported_modules list ; |
|
imported_modules_rec : imported_modules list ; |
|
untyped_ast : Ast.defs * Ast.lex_skips ; |
|
typed_ast : def list * Ast.lex_skips ; |
|
generate_output : bool ; |
}
type
var_avoid_f = bool * (Name.t -> bool) * (Ulib.Text.t -> (Name.t -> bool) -> Name.t)
var_avoid_f
is a type of a tuple (avoid_ty_vars, name_ok, do_rename)
.
The flag avoid_ty_vars
states, whether clashes with type variables should be avoided.
The name_ok n
checks whether the name n
is OK.
If it is not OK, the function do_rename n_text check
renames n
.
As input it takes the text of n
, a function check
that checks whether the new
name clashes with any names to be avoided or existing variable names in the context.
module type Exp_context = sig
.. end
module Exps_in_context:
val local_env_union : local_env -> local_env -> local_env
val funcl_aux_seplist_group : funcl_aux lskips_seplist ->
bool * lskips option *
(Name.t * funcl_aux lskips_seplist) list
Mutually recursive function definitions may contain multiple clauses for the
same function. These can however appear interleaved with clauses for other functions.
funcl_aux_seplist_group seplist
sorts the clauses according to the function names and
states, whether any resorting was necessary. Moreover, the initial lskip is returned, if present.
val class_path_to_dict_name : Path.t -> Types.tnvar -> Name.t
class_path_to_dict_name cp tv
creates a name for the class
cp
with type argument
tv
. This name is used during dictionary
passing. If a function has a type constraint that type-variable
tv
is of type-class
cp
, the function call
class_path_to_dict_name cp tv
is used to generate the name of a
new argument. This argument is a dictionary that is used to eliminate the use
of type classes.
This design is very fragile and should probably be changed in the future!
class_path_to_dict_name
needs to generate names that globally do not clash with
anything else, including names generated by class_path_to_dict_name
itself. The
generated name is independently used by both definition macros adding the
argument to the definition and expression macros that use the added argument.
The name used in both places has to coincide! Therefore, the name cannot be modified
depending on the context. Renaming to avoid clashes with other arguments /
local variables is not possible.
val ident_get_lskip : 'a Types.id -> Ast.lex_skips
val ident_replace_lskip : Types.ident_option -> Ast.lex_skips -> Types.ident_option
val oi_get_lskip : Ast.open_import -> Ast.lex_skips