package dolmen_type

  1. Overview
  2. Docs

Source file tff.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

(* This file is free software, part of dolmen. See file "LICENSE" for more information *)

module type S = Tff_intf.S

(* Typechecking functor *)
(* ************************************************************************ *)

module Make
    (Tag: Dolmen.Intf.Tag.S)
    (Ty: Dolmen.Intf.Ty.Tff
     with type 'a tag := 'a Tag.t
      and type path := Dolmen.Std.Path.t)
    (T: Dolmen.Intf.Term.Tff
     with type ty := Ty.t
      and type ty_var := Ty.Var.t
      and type ty_const := Ty.Const.t
      and type 'a tag := 'a Tag.t
      and type path := Dolmen.Std.Path.t)
= struct

  include Thf.Make(Tag)
      (struct
        include Ty
        let arrow _ _ = assert false
        let pi _ _ = assert false
      end)
      (struct
        include T
        let apply _ _ _ = assert false
      end)

  let empty_env
      ?st ?expect ?var_infer ?sym_infer
      ?(order=First_order) ?poly ?quants
      ?free_wildcards ~warnings ~file builtin_symbols =
    let env =
      empty_env ?st
        ?expect ?var_infer ?sym_infer
        ~order ?poly ?quants ?free_wildcards
        ~warnings ~file builtin_symbols
    in
    match order with
    | First_order -> env
    | Higher_order ->
      _error env (Located Dolmen.Std.Loc.no_loc) Higher_order_env_in_tff_typechecker

end