package alba

  1. Overview
  2. Docs
Alba compiler

Install

Dune Dependency

Authors

Maintainers

Sources

0.4.1.tar.gz
sha256=439b1dce07c86e914d1ebf1712c5581418314b0c8d13594f27a698b1d25fe272
md5=5cf58d4ed4eacbe6f330e9d2378ef5c6

doc/src/alba.albalib/typecheck.ml.html

Source file typecheck.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
open Fmlib

module Algo = Gamma_algo.Make (Gamma_holes)

module Uni = Unifier.Make (Gamma_holes)


include Gamma_holes

let string_of_term term gh =
    Term_printer.string_of_term term (Gamma_holes.context gh)
let _ = string_of_term


let is_subtype (sub: Term.typ) (typ: Term.typ) (gh: t) : bool
    =
    Option.has (Uni.unify sub typ true gh)





let rec check (term: Term.t) (c: t): Term.typ option =
    let open Term in
    let open Option in
    match term with
    | Sort s ->
        Some (type_of_sort s)

    | Value v ->
        Some (type_of_literal v c)

    | Variable i ->
        if i < count c then
            Some (type_of_variable i c)
        else
            None

    | Appl (f, arg, _ ) ->
        check f c >>= fun f_type ->
        check arg c >>= fun arg_type ->
        (
            match Algo.key_normal f_type c with
            | Pi (tp, rt, _ ) when is_subtype arg_type tp c ->
                Some (apply rt arg)
            | _ ->
              None
        )

    | Typed (exp, tp) ->
        check exp c >>=
        fun exp_type ->
        check tp c >>=
        fun tp_tp ->
        (   match tp_tp with
            | Sort _  when is_subtype exp_type tp c ->
                Some tp
            | _ ->
                None
        )

    | Lambda (arg, exp, info ) ->
        check arg c >>= fun sort ->
        if Term.is_sort sort then
            let name = Lambda_info.name info in
            check exp (push_local name arg c)
            >>= fun res ->
            Some (
                Pi (arg, res, Pi_info.typed name)
            )
        else
            None

    | Pi (arg, res, info) ->
        check arg c >>=
        (
            function
            | Sort arg_sort ->
                check res (push_local (Pi_info.name info) arg c)
                >>=
                (
                    function
                    | Sort res_sort ->
                        Some (Sort (Sort.pi_sort arg_sort res_sort))
                    | _ ->
                        None
                )
            | _ ->
                None
        )




let check (term: Term.t) (gamma: Gamma.t): Term.typ option =
    check term (make gamma)



let is_valid_context (gamma: Gamma.t): bool =
    let cnt = Gamma.count gamma in
    let rec check_entry i =
        if i = cnt then
            true
        else
            let typ = Gamma.type_at_level i gamma in
            match Term.down (cnt - i) typ with
            | None ->
                false
            | Some _ ->
                match check typ gamma with
                | None ->
                    false
                | Some _ ->
                    let idx = Gamma.index_of_level i gamma in
                    match Gamma.definition_term idx gamma with
                    | None ->
                        check_entry (i + 1)
                    | Some def ->
                        match Term.down (cnt - i) def with
                        | None ->
                            false
                        | Some _ ->
                            match check def gamma with
                            | None ->
                                false
                            | Some def_typ ->
                                let gh = Gamma_holes.make gamma in
                                is_subtype def_typ typ gh
                                && check_entry (i + 1)
    in
    check_entry 0


let%test _ =
    is_valid_context (Gamma.standard ())
OCaml

Innovation. Community. Security.