2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
13 module E = BrgEnvironment
14 module R = BrgReduction
16 exception TypeError of string Lazy.t
18 (* Internal functions *******************************************************)
20 let error msg = raise (TypeError (lazy msg))
22 (* Interface functions ******************************************************)
24 let rec type_of f g c = function
25 | B.Sort h -> f (B.Sort (g h))
29 | B.Abbr, B.Cast (w, v) -> f w
30 | B.Abbr, _ -> error "lref"
35 | _, _, B.Abst, w -> f w
36 | _, _, B.Abbr, B.Cast (w, v) -> f w
37 | _, _, B.Abbr, _ -> error "gref"
40 | B.Bind (id, b, u, t) ->
41 let f uu tt = match b, t with
43 | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
44 | _ -> f (B.Bind (id, b, B.Cast (uu, u), tt))
46 let f uu cc = type_of (f uu) g cc t in
47 let f uu = R.push (f uu) c b u in
50 let f tt cc = function
51 | R.Sort _ -> error "appl"
53 let f b = if b then f (B.Appl (v, tt)) else error "appl_cast" in
54 type_of (R.are_convertible f cc w) g c v
56 let f tt = R.ho_whd (f tt) c t in
59 let f b = if b then f u else error "cast" in
60 let f _ = type_of (R.are_convertible f c u) g c t in