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_______________________________________________________________ *)
18 module BE = BrgEnvironment
19 module BR = BrgReduction
21 module BV = BrgValidity
23 (* Interface functions ******************************************************)
28 let type_check err f st = function
29 | ra, na, uri, E.Abst t ->
30 let err msg = err (L.Uri uri :: msg) in
32 let e = BE.set_entity (ra, na, uri, E.Abst xt) in f tt e
34 BT.type_of err f st BR.empty_rtm t
35 | ra, na, uri, E.Abbr t ->
36 let err msg = err (L.Uri uri :: msg) in
38 let xt = match xt with
40 | _ -> B.Cast (tt, xt)
42 let e = BE.set_entity (ra, na, uri, E.Abbr xt) in f tt e
44 BT.type_of err f st BR.empty_rtm t
45 | _, _, _, E.Void -> assert false
49 let validate err f st e =
53 let uri, t = match e with
54 | _, _, uri, E.Abst t -> uri, t
55 | _, _, uri, E.Abbr t -> uri, t
56 | _, _, _, E.Void -> assert false
58 let err msg = err (L.Uri uri :: msg) in
60 let _ = BE.set_entity e in
62 if !G.si then () else Y.utime_lap "validated"
66 BV.validate err f st BR.empty_rtm t