package alba
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 ())
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>