links

The Links Programming Language
IN THIS PACKAGE
val show_pattern_compilation : bool Settings.setting
module ConstSet : sig ... end
module ConstMap : sig ... end
module Pattern : sig ... end
module NEnv = Env.String
module TEnv = Env.Int
module PEnv = Env.Int
type nenv = Var.var NEnv.t
type env = nenv * tenv * Types.row * penv
type raw_env = nenv * tenv * Types.row
val bind_context : PEnv.name -> 'a -> ('b * 'c * 'd * 'e PEnv.t) -> 'f * 'g * 'h * 'e PEnv.t
val bind_type : TEnv.name -> 'a -> ('b * 'c TEnv.t * 'd * 'e) -> 'f * 'c TEnv.t * 'g * 'h
val mem_context : PEnv.name -> ('a * 'b * 'c * 'd PEnv.t) -> bool
val mem_type : TEnv.name -> ('a * 'b TEnv.t * 'c * 'd) -> bool
val lookup_context : PEnv.name -> ('a * 'b * 'c * 'd PEnv.t) -> 'e
val lookup_type : TEnv.name -> ('a * 'b TEnv.t * 'c * 'd) -> 'e
val lookup_name : NEnv.name -> ('a NEnv.t * 'b * 'c * 'd) -> 'e
val lookup_effects : ('a * 'b * 'c * 'd) -> 'e
type raw_bound_computation = raw_env -> Ir.computation
type bound_computation = env -> Ir.computation
module CompileLists : sig ... end
module CompileEq : sig ... end
type annotation = Pattern.annotation_element list
type annotated_pattern = annotation * Pattern.t
type raw_clause = Pattern.t list * raw_bound_computation
type annotated_clause = annotation * clause
val get_pattern_sort : Pattern.t -> Pattern.sort
val get_clause_pattern_sort : clause -> Pattern.sort
val get_clauses_pattern_sort : clause list -> Pattern.sort
val reduce_pattern : Pattern.t -> annotated_pattern
val reduce_clause : raw_clause -> clause
val partition_clauses : clause list -> clause list list
val arrange_list_clauses : clause list -> annotated_clause list * annotated_clause list
val arrange_variant_clauses : clause list -> annotated_clause list Utility.StringMap.t
val arrange_constant_clauses : clause list -> annotated_clause list ConstMap.t
val arrange_record_clauses : clause list -> (annotated_pattern Utility.StringMap.t * annotated_pattern option * annotated_clause) list
val apply_annotation : Ir.value -> (annotation * bound_computation) -> bound_computation
val apply_annotations : Ir.value -> annotated_clause list -> clause list
val match_cases : Var.var list -> clause list -> bound_computation -> bound_computation
val match_var : Var.var list -> clause list -> bound_computation -> Var.var -> bound_computation
val match_negative : Var.var list -> clause -> bound_computation -> Var.var -> bound_computation
val compile_cases : raw_env -> (Types.datatype * Var.var * raw_clause list) -> Ir.computation
val handle_parameter_pattern : raw_env -> (Pattern.t * Types.datatype) -> Ir.computation -> (Ir.binder * Ir.value) * (( Ir.computation -> Ir.computation ) * Ir.binding list)
val compile_handle_parameters : raw_env -> (Pattern.t * Ir.computation * Types.datatype) list -> (Ir.binder * Ir.value) list * (( Ir.computation -> Ir.computation ) * Ir.binding list)
val match_choices : Var.var -> clause list -> bound_computation
val compile_choices : raw_env -> (Types.datatype * Var.var * raw_clause list) -> Ir.computation