(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.              
     \ /   This software is distributed as is, NO WARRANTY.              
      V_______________________________________________________________ *)

module U  = NUri
module L  = Log
module Y  = Time
module G  = Options
module E  = Entity
module B  = Brg
module BE = BrgEnvironment
module BR = BrgReduction
module BT = BrgType
module BV = BrgValidity

(* Interface functions ******************************************************)

IFDEF TYPE THEN

(* to share *)
let type_check err f st = function
   | ra, na, uri, E.Abst (a, t) ->
      let err msg = err (L.Uri uri :: msg) in
      let f xt tt = 
         let e = BE.set_entity (ra, na, uri, E.abst a xt) in f tt e
      in
      BT.type_of err f st BR.empty_rtm t
   | ra, na, uri, E.Abbr (a, t) ->
      let err msg = err (L.Uri uri :: msg) in
      let f xt tt = 
         let xt = match xt with
	    | B.Cast _ -> xt
	    | _        -> B.Cast (tt, xt)
	 in
         let e = BE.set_entity (ra, na, uri, E.abbr a xt) in f tt e
      in
      BT.type_of err f st BR.empty_rtm t
   | _, _, _, E.Void            -> assert false

END

let validate err f st e =
IFDEF PROFV THEN
   Y.utime_lap ""
ELSE () END;
   let uri, t = match e with
      | _, _, uri, E.Abst (_, t) -> uri, t
      | _, _, uri, E.Abbr (_, t) -> uri, t
      | _, _, _,   E.Void        -> assert false
   in
   let err msg = err (L.Uri uri :: msg) in
   let f () =
       let _ = BE.set_entity e in
IFDEF PROFV THEN
       if !G.si then () else Y.utime_lap "validated"
ELSE () END;
       f ()
   in
   BV.validate err f st BR.empty_rtm t