helm/software/lambda-delta/basic_rg/brgType.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 B = Brg
  13 module E = BrgEnvironment
  14 module R = BrgReduction
  15
  16 exception TypeError of string Lazy.t
  17
  18 (* Internal functions *******************************************************)
  19
  20 let error msg = raise (TypeError (lazy msg))
  21
  22 (* Interface functions ******************************************************)
  23
  24 let rec type_of f g c = function
  25    | B.Sort h             -> f (B.Sort (g h))
  26    | B.LRef i             ->
  27       let f = function
  28          | B.Abst, w             -> f w
  29          | B.Abbr, B.Cast (w, v) -> f w
  30          | B.Abbr, _             -> error "lref"
  31       in
  32       R.get f c i
  33    | B.GRef uri           ->
  34       let f = function
  35          | _, _, B.Abst, w             -> f w
  36          | _, _, B.Abbr, B.Cast (w, v) -> f w
  37          | _, _, B.Abbr, _             -> error "gref"
  38       in
  39       E.get_obj f uri
  40    | B.Bind (id, b, u, t) ->
  41       let f uu tt = match b, t with
  42          | B.Abst, _
  43          | B.Abbr, B.Cast _ -> f (B.Bind (id, b, u, tt))
  44          | _                -> f (B.Bind (id, b, B.Cast (uu, u), tt))
  45       in
  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
  48       type_of f g c u
  49    | B.Appl (v, t)        ->
  50       let f tt cc = function
  51          | R.Sort _ -> error "appl"
  52          | R.Abst w ->
  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
  55       in
  56       let f tt = R.ho_whd (f tt) c t in
  57       type_of f g c t
  58    | B.Cast (u, t)        ->
  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
  61       type_of f g c u