Index of values

o1 ^ o2 appends to outputs to each other

absolute_dir dir tries to get the absolute path name of directory dir.

The distinction between cur_env, new_defs and export_env is interesting.

add_def_aux_entities targ only_new ue def adds all the modules, types, constants ...

add_def_entities is called add_def_aux_entities after extracting the appropriate def_aux.

Add a list of values to an existing set.

add_lskip converts a name into a name with skips by adding empty whitespace

add_pre_lskip sk n adds additional whitespace in front of n

add_used_entities_to_avoid_names env targ ue ns adds the used entities in ue to the name-set ns.

The set of all the targets.

A list of all the targets.

The set of targets used when negating or no mentioning explicit targets.

alter_init_lskips finds all of the whitespace/newline/comments preceding an expression and passes it to the supplied function in a single invocation.

always_replace_files determines whether Lem only updates modified files.

append d sl1 sl2 appends the seplists sl1 and sl2.

append_lskips adds new whitespace/newline/comments to the front of an expression (before any existing whitespace/newline/comments in front of the expression)

apply_target m targ looks up the targ in map m.

assert_equal l m d t1 t2 performs the same check as check_equal d t1 t2.

ast_target_compare is a comparison function for ast-targets.

ast_target_to_target t converts an ast-target to a target.

Avoiding certain names for local variables.

The boolean type

break_hint add_space ind is a general hint for a line-break.

break_hint_cut is short for break_hint false 0.

break_hint_space ind is short for break_hint true ind.

c_env_all_consts c_env returns the constants defined in c_env

c_env_lookup l c_env c_ref looks up the constant reference c_ref in environment c_env and returns the corresponding description.

c_env_save c_env c_ref_opt c_d is a combination of c_env_update and c_env_store.

c_env_store c_env c_d stores the description c_d environment c_env.

c_env_store_raw c_env c_d stores the description c_d environment 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.

capitalize n tries to capitalize the first letter of n.

cdmap_domain m returns the list of all const description references in the map

Constructs an empty cdmap

cdmap_insert m v inserts value v into m.

cdmap_lookup m r looks up the reference r in map m

cdmap_update m r v updates map m at reference r with value v.

changed2 f g x h y applies g to x and h to y.

check_constr_family is similar to constr_family_to_id.

check_defs backend_targets mod_name filename mod_in_output env ast typescheck the parsed module ast from file filename in environment env.

check_equal d t1 t2 checks whether t1 and t2 are equal in type environment d.

check_for_inline_cycles targ env checks whether any constant in env would be inlined (possible over several steps) onto itself.

check_match_def env d checks a definition using pattern matching d in environment env.

check_match_def_warn env d checks a definition and prints appropriate warning messages.

check_match_exp env e checks the pattern match expression e in environment env.

check_match_exp_warn env e internally calls check_match_exp env e.

checked_number_patterns env p checks that all number patterns which are part of p are of type nat or natural.

check_pat_list env pl checks the pattern list pL in environment env.

Some targets may choose to not use type-classes to implement certain functions.

Given a class-description cd and an argument type arg, the function class_descr_get_dict_type cd arg generates the type of the dictionary for the class and argument type.

class_path_to_dict_name cp tv creates a name for the class cp with type argument tv.

Type classes are not supported by all backends.

cleanup_match_exp env add_missing e tries to cleanup the match-expression e by removing redunanant rows.

cleanup_set_quant moves restricted and unrestricted quantification in set comprehensions to the condition part, if the bound variables are only used by the condition.

collapse_nested_matches tries to eliminate nested matches by collapsing them.

A comment

comment_block min_width_opt content comment a whole list of lines in a block.

Removes inline instances for backends that employ typeclasses.

Structural comparison of types, without expanding type abbreviations.

basic functions on plain names

compare_expand d t1 t2 is similar check_equal d t1 t2.

compile_match_exp target_opt pat_OK env e compiles match-expressions.

component_to_output c formats component c as an output

concat sep [o0; ...; on] appends all the outputs in the list using the separator sep, i.e.

cons_sep_alt doesn't add the separator if the list is empty

const_descr_has_target_rep targ d checks whether the description d contains a target-representation for target targ.

const_descr_ref_to_ascii_name env c tries to find a simple identifier for constant c.

const_descr_to_kind r d assumes that d is the description associated with reference r.

const_exists env label checks, whether the constant with label label is available in the environment env.

const_id_to_ident c_id use_ascii tries to format a constant, constructor or field c_id as an identifier for target A.target using the rules stored in environment A.env.

const_ref_to_name n use_ascii c tries to format a constant c for target A.target using the rules stored in environment A.env.

const_target_rep_allow_override rep returns whether this representation can be redefined.

const_target_rep_to_loc rep returns the location, at which rep is defined.

const_descr_rename targ n' l' cd looks up the representation for target targ in the constant description cd.

constant_descr_to_name targ cd looks up the representation for target targ in the constant description cd.

constr_family_to_id l env ty cf tries to instantiate the constructor family cf to be used on a match statement where the matched type is ty.

copy_file src dst copies file src to file dst.

Add type annotations to pattern variables whose type contains a type variable (only add for arguments to top-level functions)

core out is a marker for marking the most important part of some output.

cr_special_fun_uses_name f checks, whether f uses it's first argument, i.e.

ctxt_all_tdefs_set_target_rep l ctxt ty targ new_rep updates the target-representation of type ty for target targ in context ctxt to new_rep.

ctxt_start_submodule ctxt is used when a new submodule is processed.

ctxt_c_env_set_target_rep l ctxt c targ new_rep updates the target-representation of constant c for target targ in context ctxt to new_rep.

ctxt_end_submodule l ctxt_before mod_path mod_name ctxt_submodule is used when a new submodule is no longer processed.

Should debug be printed

If def_add_location_comment_flag is set, def_add_location_comment d adds a comment with location information before definition d.

def_add_location_comment_flag controls whether def_add_location_comment.

A definition context contains amoung other things an environment split up over several fields.

If a target representation for a constant is given, the original definition is not needed.

dest_app_exp e tries to destruct an function application expression e.

dest_cons_pat p destructs list-cons patterns.

Destructor for constants expressions

dest_contr_pat p destructs constructor patterns.

dest_ext_var_pat p is an extended version of det_var_pat p.

dest_field_types l env f looks up the types of the field f in environment env.

dest_fn_type d_opt t tries to destruct a function type t.

dest_human_target targ destructs targ to get the non-identity target.

dest_infix_exp e tries to destruct an infix expression e.

dest_list_pat p destructs list patterns.

dest_num_add_pat p destructs number addition literal patterns

dest_num_exp e destructs a number literal expression.

dest_num_pat p destructs number literal patterns

dest_record_pat p destructs record patterns.

dest_string_pat p destructs number literal patterns

dest_tf_exp destructs true and false expressions.

dest_tf_pat p destructs boolean literal patterns, i.e.

Destructor for tuple expressions.

dest_tup_pat lo p destructs a tuple pattern.

Destructor for variable expressions

dest_var_pat p destructs variable patterns and returs their name.

dir_eq d1 d2 uses absolute_dir to check whether the two directories are equal.

direct_subpats p returns a list of all the direct subpatterns of p.

If sl starts with a seperator, it is dropped and returned, otherwise nothing happens.

drop_init_ws should be used with function like Typed_ast.alter_init_lskips.

drop_path i drops the path of an identier.

e_env_lookup l e_env p looks up the module with path p in environment e_env and returns the corresponding description.

Empty output

an empty instance environment

An empty collection of entities

Make sure there is a newline starting here.

env_apply env comp_opt n looks up the name n in the environment env.

env_c_env_update env c_ref c_d updates the description of constant c_ref with c_d in environment env.

The environment the expressions are considered in

env_tag_to_string tag formats tag as a string.

err message is an error output.

err_general b l m is an abreviatiation for Fatal_error (Err_general (b, l, m))

err_todo b l m is an abreviatiation for Fatal_error (Err_todo (b, l, m))

err_type l msg is an abreviatiation for Fatal_error (Err_type (l, m), i.e.

err_type l msg pp n is similar to err_type.

err_unreachable l m is an abreviatiation for Fatal_error (Err_unreachable (l, m))

exists_pat cf p checks whether p has a subpattern p' such that cf p' holds.

extract_core o extracts all top-level cores from output o.

flat [o0; ...; on] appends all the outputs in the list, i.e.

flatten d sll flattens a list of seplists by applying append repeatedly

fold left implemented via map_acc_left

fold right implemented via map_acc_right

for_all_subpat cf p checks whether all subpatterns p' of p satisfy cf p'.

fresh n OK generates a name m, such that OK m holds.

fresh_list OK ns builds variants of the names in list ns such that all elements of the resulting list ns' satisfy OK and are distinct to each other.

fresh_num_list i n OK generates a list of i fresh names.

fresh_string forbidden generates a stateful function gen_fresh that generates fresh strings.

creates a name from Ast.ix_l, used during typechecking

Construct a set from a list.

The from list functions ignore the last separator in the input list

from_list_default d l constructs a seplist form a list of entries l using the separator d as default separator between all entries.

constructs a seplist from a list of pairs.

from_pair_list_sym first_val_opt sep_val_list last_sep_opt constructs a seplist from a list of pairs sep_val_list.

creates a name from Ast.x_l, used during typechecking

Mutually recursive function definitions may contain multiple clauses for the same function.

function_application_to_output l exp inf full_exp c_id args tries to format a function application as output.

The level of extra information to generate

get_avoid_f targ returns the target specific variable avoid function.

get_checked_module_entities targ only_new ml gets all the modules, types, constants ...

get_const env label is a wrapper around string_get_const that maps a label to an actual constant description.

get_const_id env l label inst uses strings_get_const_id with an indirection to look up a constant for a given label.

get_duplicates l returns the elements that appear multiple times in the list l.

get_duplicates_gen p l returns the elements that appear multiple times in the list l.

get_field_all_fields l env f uses get_field_type_descr l env f to look up the type description of the record type of the field f.

get_field_type_descr l env f uses dest_field_types l env f to get the base type of the field f.

get_imported_modules ast returns a list of the modules imported by the given definitions.

get_imported_target_modules env targ defs extracts a list of module that should be imported.

get_lskip n gets the preceeding whitespace of n

get_matching_instance type_env (class, ty) i_env searches for an instantiation of type class class instantianted with type ty in the type invironment i_env.

get_module_name env targ mod_path mod_name looks up the name of module mod_path.mod_name in environment env for target targ.

get_module_open_string l env targ dir mod_path looks up how to represent this module in import / open statements.

get_module_path p returns the module path of path p.

Return the last name in the ident, e.g., M.Y.x gives x

get_prec target env c looks up the precedence of constant c in environment env for the target target.

get_prec target env e looks up the precedence of expression e in environment env for the target target.

get_toplevel_name p gets the outmost name of a path.

get_transformation targ returns the (pre-backend) transformation function for target targ

has_empty_path_prefix i check whether the identifier i consists of just a single name without any prefix describing its module path

gets the first entry, if there is one

gets the first seperator, if there is one

i_env_add i_env i adds an additional instance i to the instance environment.

i_env_lookup l i_env ref looks up the reference in environment i_env.

An identifier

This flag enables dictionary passing transfromations for the identity backend.

This flag enables pattern compilation for the identity backend.

Turn off pattern compilation warnings, used by main

imported_modules_to_strings env targ dir imported_mods is used together with get_imported_target_modules.

in_target_set targ targetset checks whether the target `targ` is in the set of targets targetset.

in_targets_opt targ targets_opt checks whether the target `targ` is in the set of targets represented by `targets_opt`.

inline_exp_macro target env does the inlining of target specific constant definitions

inline_pat_macro target env does the inlining of target specific constant definitions

insert_target m (targ, v) inserts value v for targ in map m.

instance_to_dict do_inline targ turns instance declarations into a definition of a dictionary record.

intercalate sep as inserts sep between the elements of as, i.e.

interleave l1 l2 interleaves lists l1 and l2, by alternatingly taking an element of l1 and l2 till one of the lists is empty.

is_buildin_constructor l env targ c checks whether c is a build-in constructor for target targ in environment env.

is_const_exp e checks whether e is a constant expression

is_constructor l env targ c checks whether c is a constructor for target targ in environment env.

is_empty_backend_exp checks whether the expression is ``

is_ext_var_pat p checks whether the pattern p is a variable pattern in the broadest sense.

if_f_pat p checks whether p is the false pattern.

is_human_target targ checks whether targ is a target intended to be read by humans and therefore needs preserving the original structure very closely.

is_infix_exp e checks whether e is an infix operation

is the type ok to be used in an non-default type-class instantiation?

is_nil_const_descr_ref r checks whether r is the nil reference.

is_not_buildin_constructor l env targ c checks whether c is a constructor for target targ in environment env, but not a build-in one.

is_num_add_pat p checks whether p is a number addition pattern.

is_num_exp checks whether e is a number literal expression.

is_num_pat p checks whether p is a number pattern.

is_pp_loc l checks whether l is of the form Ast.Trans (true, _, _).

is_recursive_def d checks whether d is recursive.

is_simple_ident_string s checks whether s is a "simple" identifier.

is_string_pat p checks whether p is a number pattern.

if_t_pat p checks whether p is the true pattern.

is_tf_exp v e checks whether e is a true or false expression.

if_tf_pat p checks whether p is the true or false pattern.

is_tup_exp s_opt e checks whether e is a tuple of size s_opt.

is_tup_pat lo p checks whether p is a tuple pattern of the given length.

is_type_def_abbrev d checks whether the definition d is a type-abbreviation definition.

is_type_def_abbrev d checks whether the definition d is a definition of a record_type.

is_var_exp e checks whether e is a variable expression

is_var_pat p checks whether the pattern p is a variable pattern.

is_var_tup_exp e checks, whether e is an expression consisting only of variables and tuples.

is_var_tup_pat p checks whether the pattern p consists only of variable and tuple patterns.

is_var_wild_pat p checks whether the pattern p is a wildcard or a variable pattern.

is_var_wild_tup_pat p checks whether the pattern p consists only of variable, wildcard and tuple patterns.

is_wild_pat p checks whether the pattern p is a wildcard pattern.

kwd s constructs the output for keyword s

list_dest_snoc l splits the last entry off a list.

list_diff l1 l2 removes all elements from l1 that occur in l2.

list_dropn n l drops the first n elemenst from list l, i.e.

list_fristn n l gets the first n elemenst from list l, i.e.

list_index p l returns the first index i such that the predicate p (l!i) holds.

Builds the intersection of a list of sets.

list_iter_sep sf f [a1; ...; an] applies function f in turn to a1; ...; an and calls sf () in between.

list_longer n l checks whether the list l has more than n elements.

list_mapi f l maps f over l.

list_null l checks whether the list l is empty, i.e.

list_pick p l tries to pick the first element from l that satisfies predicate p.

list_quant_to_set_quant turns forall (x MEM L). P x into forall (x IN Set.from_list L). P x

list_subset l1 l2 tests whether all elements of l1 also occur in l2.

list_to_front i l resorts the list l by bringing the element at index i to the front.

list_to_mac macro_list collapses a list of def_macros into a single one.

Builds the union of a list of sets

loc_to_string short l formats l as a string.

lookup_class_descr l env c_path looks up the description of type-class c_path in environment env.

lookup_env is similar to lookup_env_opt, but reports an internal error instead of returning None, if no environment can be found.

lookup_env_opt env path is used to navigate inside a environment env.

lookup_field_for_class_method l cd method_ref looks up the field reference corresponding to the method identified by method_ref in the description cd of a type class.

lookup_inst_method_for_class_method l i method_ref looks up the instance method reference corresponding to the method identified by method_ref in the instance i.

lookup_mod_descr env path mod_name is used to navigate inside an environment env.

lookup_mod_descr_opt env path mod_name is used to navigate inside an environment env.

lskip_rename r_fun n is a version of rename that can handle lskips.

Get only the comments (and a trailing space)

Get the first lskip of the list and only comments from the rest

Maps with an accumulating parameter.

map_all f l maps f over l.

map_changed f l maps f over l.

Returns None if the function returns None on all of the elements, otherwise returns a list that uses the original element where the function returns None

map_changed_default d f l maps f over l.

map_filter f l maps f over l and removes all entries x of l with f x = None.

match_types t_pat t tries to match type t_pat against type t.

may_need_paren e checks, whether e might need parenthesis.

message_singular_plural (sing_message, multiple_message) l is used to determine whether the singular or plural form should be used in messages.

meta s creates a string directly as output such that the formatting can't interfere with string s any more

mk_and_exp env e1 e2 constructs the expression e1 && e2.

mk_and_exps env es constructs the conjunction of all expressions in es.

mk_app_exp d e1 e2 constructs the expression e1 e2.

mk_case_exp final l e rows ty constructs a case (match) expression.

mk_const_exp uses strings_mk_const_exp with an indirection through a label.

mk_cross_exp env e1 e2 constructs the expression cross e1 e2.

mk_dummy_exp ty constructs a dummy expression of type ty.

mk_eq_exp env e1 e2 constructs the expression e1 = e2.

mk_eta_expansion_exp d vars e for variables vars = [x1, ..., xn] tries to build the expression fun x1 ... xn -> (e x1 ... xn).

mk_from_list_exp env e constructs the expression Set.from_list e.

mk_fun_exp [p1, ..., pn] e constructs the expression fun p1 ... pn -> e.

mk_ident sk ms n creates an identifier n with module prefix ms and leading whitespace sk.

mk_ident_ast nsl ns l generates a new identifiers during type-checking.

mk_ident_strings is a version of mk_ident that uses strings as input and uses empty whitespace.

mk_if_exp l c e_t e_f constructs the expression if c then e_t else e_f using default spacing.

mk_le_exp env e1 e2 constructs the expression e1 <= e2.

mk_let_exp l (n, e1) e2 constructs the expression let n = e1 in e2 using default spacing.

mk_list_app_exp d f [a1 ... an] constructs the expression f a1 ... an by repeatedly calling mk_app_exp.

mk_name_lskips_annot creates an annoted name

mk_num_add_pat num_ty i makes a number addition pattern.

mk_num_exp creates a number literal expression.

mk_num_pat num_ty i makes a number pattern.

mk_opt_fun_exp pL e returns mk_fun_exp pL e if pL is not empty and e otherwise.

mk_opt_paren_exp e adds parenthesis around expression e if it seems sensible.

adds parenthesis around a pattern, when needed

mk_paren_exp e adds parenthesis around expression e.

adds parenthesis around a pattern

mk_path_list names splits names into ns @ [n] and calls mk_path ns n.

mk_set_filter_exp env e_P e_s constructs the expression Set.filter e_P e_s.

mk_set_image_exp env e_f e_s constructs the expression Set.image e_f e_s.

mk_set_sigma_exp env e1 e2 constructs the expression set_sigma e1 e2.

mk_sub_exp env e1 e2 constructs the expression e1 - e2.

mk_tc_type vars reg_exp_opt generates a simple description of a type, which uses the type arguments vars and the reg_exp_opt for restricting the names of variables of this type.

Generates a type abbreviation

mk_tf_exp creates true and false expressions.

mk_tf_pat b creates true or false pattern.

mk_tup_pat [p1, ..., pn] creates the pattern (p1, ..., pn).

mk_undefined_exp l m ty constructs an undefined expression of type ty with message m.

ml_comment_to_rope com formats an ML-comment as a text by putting (* and *) around it.

mod_descr_rename targ mod_name n' l' md updates the representation for target targ in the module description md by renaming to the new name n' and new location l'.

module_id_to_ident m_id tries to format a module m_id as an identifier for target A.target using the rules stored in environment A.env.

move_file src dst moves file src to file dst.

names_get_const env path n looks up the constant with name n reachable via path path in the environment env

The natural number type

a new line

nil_const_descr_ref is a nil reference, i.e.

The empty lskip

non_ident_target_to_mname t returns a name for a target.

non_ident_target_to_string t returns a string description of a target t.

num i constructs the output for number i

num_ty_pat_cases f_v f_i f_a f_w f_else p performs case analysis for patterns of type num.

only_auxiliary determines whether Lem generates only auxiliary files

option_bind f None returns None, whereas option_bind f (Some x) returns f x.

option_cases None f_s f_n returns f_n, whereas option_cases (Some x) f_s f_n returns f_s x.

option_default d None returns the default value d, whereas option_default d (Some x) returns x.

option_default_map v d f is short for option_default d (option_map f v).

option_first f l searches for the first element x of l such that the f x is not None.

option_get_exn exn None throws the exception exn, whereas option_get_exn exn (Some x) returns x.

option_map f None returns None, whereas option_map f (Some x) returns Some (f x).

output_alltexdoc produces the latex output for all modules in a single file

pat_extract_lskips p extracts all whitespace from a pattern

pat_to_exp env p tries to convert p into a corresponding expression.

pat_to_ext_name p is very similar to dest_ext_var_pat p.

pat_vars_src p returns a list of all the variable names occuring in the pattern.

pattern_application_to_output l pat c_id args tries to format a function application in a pattern as output.

Pretty print

prefix_if_not_emp o1 o2 returns o1 ^ o2 if o2 is not empty and emp otherwise

print_debug s prints the string s with some debug prefix to the standard error output.

print_debug_typ_raw s [ty0, ..., tn] prints a debug message s t0, ..., tn using Reporting_basic.print_debug.

print_err fatal print_loc_source print_only_first_loc l head mes prints an error / warning message to std-err.

process_defs rev_path def_mac mod_name env ds is intended to run the macro def_mac over all definitions in module mod_name.

process_files allow_reorder lib_dirs files parses the files in list files.

read_target_constants lib_path target reads the list of contants that should be avoided for target target.

remove_class_const remove constants that have class constraints by adding explicit dictionary parameters.

remove_core o removes all occurences of core form t by replacing core o' with just o'.

remove_duplicates l removes duplicate elements from the list l.

remove_duplicates_gen p l removes duplicate elements from the list l.

remove_fun env case_f e replaces the fun-expression e.

remove_fun_pats keep_tup removes patterns from expressions of the from fun p1 ... pn -> e by introducing function expressions.

remove_function turns function | pat1 -> exp1 ... | patn -> expn end into fun x -> match x with | pat1 -> exp1 ... | patn -> expn end.

remove_function env case_f e replaces the function expression e with with fun x -> match x with ....

remove_import removes all import statements.

remove_import_include removes all import and include statements.

remove_init_ws should be used with function like Typed_ast.alter_init_lskips.

removes intial whitespace (including comments) from output

Removes a list of values to an existing set.

remove_list_comprehension removes list comprehensions by turning them into fold and insert operations.

remove_method target add_dict is used to remove occurrences of class methods.

remove_method_pat is used to remove occurrences of class methods.

remove_module_renames removes all module rename statements.

remove_multiple_record_updates replaces record updates simultaneously updating multiple fields with a nested record update, each affecting only one field, that achieves the same effect.

remove_num_lit replaces L_num (sk, i) with fromNumeral (L_numeral (sk, i)).

remove_opens removes all open / include and import statements

remove_quant turns quantifiers into iteration.

remove_quant_coq the same as above but does not apply in the body of lemma or theorem statements.

remove_restr_quant pat_OK turns restricted quantification into unrestricted quantification, if then pattern does not satisfy pat_OK.

remove_set_comp_binding tries to turn Comb_binding expressions into Set_comb ones.

remove_set_comprehension removes set comprehensions by turning them into fold and insert operations.

remove_set_comprehension allow_sigma removes set comprehensions by turning them into set-image, set-filter and set-product operations.

remove_set_restr_quant turns restricted quantification in set comprehensions into unrestricted quantification.

remove_setcomp removes set comprehensions with implicit bound variable to ones with explicitly bound onces.

Warning: OCaml specific! remove_sets transforms set expressions like {e1, ..., en} into Ocaml.Pset.from_list (type_specific compare) [e1, ..., en]

remove_singleton_record_updates replaces updates of records that have only one field with the construction of a completely new record.

remove_toplevel_match tries to introduce matching directly in the function definition by eliminating match-expressions in the body.

If a target representation for a type is given, the original type definition is commented out.

remove_underscore n tries to remove a leading underscore from name n.

remove_unit_pats replaces unit-patterns () with wildcard ones _.

rename r_fun n renames n using the function r_fun.

rename i n' renames the last name component of identifier i to n'.

Rename the arguments to definitions, if they clash with constants in a given set of constants.

rename_target topt ue consts e processes the entities (constants, constructors, types, modules ...) stored in ue and renames them for target topt.

replace_lskip sk n replaces the whitespace in front of n with sk.

replicate n e creates a list that contains n times the element e.

Report error should only be used by main to print the error in the end.

report_warning env w reports a warning.

report_warning_no_env w reports a warning, when no-environment is available.

resolve_const_ref l env target io c_ref tries to find the constant c_ref in environment env.

resolve_module_path l env sk m tries to find the module-path m in environment env.

resolve_type_path l env sk p tries to find the type of (absolute) path p in environment env.

same_content_files file1 file2 checks, whether the files file1 and file2 have the same content.

Infer the comprehension variables for a set comprehension without explicitly listed comprehension variables.

sing a constructs a seplist with entry a.

single_pat_exhaustive p checks whether the pattern p is exhaustive.

sort_record_fields sorts the fields of a record expression into the same order as in the definition of the record type.

A space lskip

a single space

space_com_init_ws should be used with function like Typed_ast.alter_init_lskips.

space_init_ws should be used with function like Typed_ast.alter_init_lskips.

split_after n l splits the first n elemenst from list l, i.e.

split_var_annot_pat p splits annotated variable patterns in variable patterns + type annotation.

start_with_lower_letter n checks, whether the name n starts with a character in the range a-z.

start_with_underscore n checks, whether the name n starts with an underscore character.

start_with_upper_letter n checks, whether the name n starts with a character in the range A-Z.

str s constructs the output for string constant s

string_for_all p s checks whether all characters of s satisfy p.

string_lits_isa translates non-representable string literals into list of characters for Isabelle

string_map f s maps f over all characters of a copy of s.

string_of_const_descr_ref formats a reference in a human readable form.

string_of_instance_ref formats a reference in a human readable form.

string_split c string splits the string into a list of strings on occurences of the char c.

string_to_list l translates the string l to the list of its characters.

strings_get_const is a wrapper around names_get_const that uses strings instead of names.

strings_get_const_id env l path n inst uses get_const env path n to construct a const_descr and then wraps it in an id using location l and instantiations inst.

strings_mk_const_exp uses get_const_id to construct a constant expression.

strip_app_exp e tries to destruct multiple function applications.

strip_app_infix_exp e is a combination of strip_infix_exp and strip_app_exp.

strip_fn_type d t tries to destruct a function type t by applying dest_fn repeatedly.

strip_infix_exp e is similar to dest_infix_exp, but returns the result in the same way as strip_app_exp.

strip_lskip converts a name with whitespace into a name by dropping the preceeding whitespace

strip_paren_typ_exp e strips parenthesis and type-annotations form expression e.

Remove the name from the identifier if it occurs at the first

subpats p returns a list of all the subpatterns of p.

target_compare is a comparison function for targets.

target_to_ast_target t converts a target t to an ast_target.

target_to_output t returns output for a target t.

target_to_string t_opt returns a string description of a target.

target_opt_to_list targets_opt returns a distinct list of all the targets in the option.

??? Unsure what it is.

Removes the first entry, fails is there is none, or if a separator is first

Removes the first entry, fails is there is none, removes any separator that precedes the first entry

Removes the first separator, fails is there is none, or if an entry is first

Makes a normal list, ignoring separators

to_output is the same as to_output_format Output.id

to_output_format format_fun id_annot n formats the name n as output.

to_output_quoted qs_begin qs_end id_annot n formats n with the quoting strings qs_begin and qs_end added before and after respectively.

Makes a normal list of pairs.

to_rope quote_char lex_skips_to_rope need_space t formats the output t as an unicode text.

to_rope_option_tex t is similar to to_rope_tex t.

to_rope_tex t corresponds to to_rope for the Latex backend.

to_rope_tex a n formats n as a for the tex-backend as a string.

Flattens into a normal list with separators and elements intermixed

Flattens into a normal list with separators and elements intermixed, with special control over the first separator.

As to_sep_list_first, but for the last separator

to_string i formats i using pp.

try_termination_proof targ c_env d calls is_recursive_def d.

type_defs_get_constr_families l d targ t c gets all constructor family descriptions for type t for target targ in type environment d, which contain the constant c.

type_defs_lookup l d p looks up the description of type with path p in defs d.

type_defs_lookup_typ l d t looks up the description of type t in defs d.

type_def_rename_type l d p t n renames the type with path p in the defs d to the name n for target t.

type_defs_update d p td updates the description of type with path p in defs d with td.

type_defs_update_fields l d p fl updates the fields of type p in d.

type_defs_update_tc_class l d p up updates the description of type p in d using the function up.

type_defs_update_tc_type l d p up updates the description of type p in d using the function up.

type_descr_rename targ n' l' td looks up the representation for target targ in the type description td.

type_descr_to_name targ ty td looks up the representation for target targ in the type description td.

type_id_to_ident ty_id tries to format a type ty_id as an identifier for target A.target using the rules stored in environment A.env.

type_id_to_ident_no_modify ty_id formats ty_id as an identifier.

type_id_to_output ty_id tries to format a type ty_id as an identifier for target A.target using the rules stored in environment A.env.

type_path_to_name n p tries to format a type-path p for target A.target using the rules stored in environment A.env.

type_target_rep_allow_override rep returns whether this representation can be redefined.

type_target_rep_to_loc rep returns the location, at which rep is defined.

uncapitalize n tries to uncapitalize the first letter of n.

uncapitalize_prefix n tries to uncapitalize the first few letters of n.

undo_list_to_front i l resorts the list l by moving the head element to index index i It's the inverse of list_to_front i l.

update_const_descr l up c env updates the description of the constant c in environment env using the function up.

val_def_get_class_constraints env vd collects the class constraints of all top-level function definitions in vd.

val_def_get_class_constraints_no_target_rep env targ vd collects the class constraints of all top-level function definitions in vd, which don't have a target-specific representation for target targ.

val_def_get_free_tnvars env vd returns the set of all free type-variables used by vd.

val_def_get_name d tries to extract the name of the defined function.

Command line options for warnings

if the flag warnings_active is set, warning messages are printed, otherwise they are thrown away.

Whitespace