helm/software/helena/src/basic_rg/brgUntrusted.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 module U  = NUri
  13 module L  = Log
  14 module Y  = Time
  15 module G  = Options
  16 module E  = Entity
  17 module B  = Brg
  18 module BE = BrgEnvironment
  19 module BR = BrgReduction
  20 module BT = BrgType
  21 module BV = BrgValidity
  22
  23 (* Interface functions ******************************************************)
  24
  25 IFDEF TYPE THEN
  26
  27 (* to share *)
  28 let type_check err f st = function
  29    | ra, na, uri, E.Abst (a, t) ->
  30       let err msg = err (L.Uri uri :: msg) in
  31       let f xt tt =
  32          let e = BE.set_entity (ra, na, uri, E.abst a xt) in f tt e
  33       in
  34       BT.type_of err f st BR.empty_rtm t
  35    | ra, na, uri, E.Abbr (a, t) ->
  36       let err msg = err (L.Uri uri :: msg) in
  37       let f xt tt =
  38          let xt = match xt with
  39             | B.Cast _ -> xt
  40             | _        -> B.Cast (tt, xt)
  41          in
  42          let e = BE.set_entity (ra, na, uri, E.abbr a xt) in f tt e
  43       in
  44       BT.type_of err f st BR.empty_rtm t
  45    | _, _, _, E.Void            -> assert false
  46
  47 END
  48
  49 let validate err f st e =
  50 IFDEF PROFV THEN
  51    Y.utime_lap ""
  52 ELSE () END;
  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
  57    in
  58    let err msg = err (L.Uri uri :: msg) in
  59    let f () =
  60        let _ = BE.set_entity e in
  61 IFDEF PROFV THEN
  62        if !G.si then () else Y.utime_lap "validated"
  63 ELSE () END;
  64        f ()
  65    in
  66    BV.validate err f st BR.empty_rtm t