View Source cure_dependent_parser (cure v0.7.0)

Dependent Type Parser Support

This module provides parser helper functions for dependent type syntax introduced in Phase 6. It extends the main parser with support for:

Type-level parameters (both type and value parameters)
Type-level expressions (arithmetic, comparisons)
Dependent function types
Value parameter constraints

Examples

Parsing Type-Level Parameters

type Vector(T, n: Nat) = List(T) when length(this) == n
%        ^  ^^^^^^^^^ value parameter
%        | type parameter

Parsing Dependent Function Types

def concat<T, m: Nat, n: Nat>(
    v1: Vector(T, m),
    v2: Vector(T, n)
): Vector(T, m + n) = ...
%         ^^^^^^^ type-level expression

Usage

These functions are called by the main parser (cure_parser.erl) when encountering dependent type syntax.

Summary

Types

location()

Functions

is_type_level_op/1

is_value_param/1

make_dependent_function_type(TypeParams, Params, ReturnType, Constraints, Location)

make_dependent_type(Name, TypeParams, ValueParams, Location)

make_type_level_expr(Op, Left, Right, Location)

parse_type_level_expr/1

parse_type_params(Params)

parse_value_param/1

Types

location()

-type location() :: #location{line :: term(), column :: term(), file :: term()}.

Functions

is_type_level_op/1

-spec is_type_level_op(atom()) -> boolean().

is_value_param/1

-spec is_value_param(term()) -> boolean().

make_dependent_function_type(TypeParams, Params, ReturnType, Constraints, Location)

-spec make_dependent_function_type([#type_param{name :: term(),
                                                kind :: term(),
                                                type :: term(),
                                                constraint :: term(),
                                                location :: term()}],
                                   [#param{name :: term(), type :: term(), location :: term()}],
                                   term(),
                                   [term()],
                                   location()) ->
                                      #dependent_function_type{type_params :: term(),
                                                               params :: term(),
                                                               return_type :: term(),
                                                               constraints :: term(),
                                                               location :: term()}.

make_dependent_type(Name, TypeParams, ValueParams, Location)

-spec make_dependent_type(atom(), [term()], [{atom(), term()}], location()) ->
                             #dependent_type{name :: term(),
                                             type_params :: term(),
                                             value_params :: term(),
                                             location :: term()}.

make_type_level_expr(Op, Left, Right, Location)

-spec make_type_level_expr(atom(), term(), term(), location()) ->
                              #type_level_expr{op :: term(),
                                               left :: term(),
                                               right :: term(),
                                               location :: term()}.

parse_type_level_expr/1

-spec parse_type_level_expr(term()) ->
                               #type_level_expr{op :: term(),
                                                left :: term(),
                                                right :: term(),
                                                location :: term()}.

parse_type_params(Params)

-spec parse_type_params([term()]) ->
                           [#type_param{name :: term(),
                                        kind :: term(),
                                        type :: term(),
                                        constraint :: term(),
                                        location :: term()}].

parse_value_param/1

-spec parse_value_param(term()) ->
                           #value_param{name :: term(),
                                        type :: term(),
                                        constraint :: term(),
                                        location :: term()}.