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 U = NUri
  13 module C = Cps
  14 module A = Share
  15 module L = Log
  16 module H = Hierarchy
  17 module B = Brg
  18 module O = BrgOutput
  19 module E = BrgEnvironment
  20 module S = BrgSubstitution
  21 module R = BrgReduction
  22
  23 (* Internal functions *******************************************************)
  24
  25 let level = 4
  26
  27 let log1 s c t =
  28    let sc, st = s ^ " in the context", "the term" in
  29    L.log O.specs level (L.ct_items1 sc c st t)
  30
  31 let error1 st c t =
  32    let sc = "In the context" in
  33    raise (R.TypeError (L.ct_items1 sc c st t))
  34
  35 (* Interface functions ******************************************************)
  36
  37 let rec b_type_of f ~si g c x =
  38    log1 "Now checking" c x;
  39    match x with
  40    | B.Sort (a, h)           ->
  41       let f h = f x (B.Sort (a, h)) in H.apply f g h
  42    | B.LRef (_, i)           ->
  43       let f _ = function
  44          | Some (_, B.Abst w)                  ->
  45             S.lift (f x) (succ i) (0) w
  46          | Some (_, B.Abbr (B.Cast (_, w, _))) ->
  47             S.lift (f x) (succ i) (0) w
  48          | Some (_, B.Abbr _)                  -> assert false
  49          | Some (_, B.Void)                    ->
  50             error1 "reference to excluded variable" c x
  51          | None                             ->
  52             error1 "variable not found" c x
  53       in
  54       B.get f c i
  55    | B.GRef (_, uri)         ->
  56       let f = function
  57          | _, _, B.Abst w                  -> f x w
  58          | _, _, B.Abbr (B.Cast (_, w, _)) -> f x w
  59          | _, _, B.Abbr _                  -> assert false
  60          | _, _, B.Void                    ->
  61             error1 "reference to excluded object" c x
  62       in
  63       E.get_obj f uri
  64    | B.Bind (a, B.Abbr v, t) ->
  65       let f xv xt tt =
  66          f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
  67       in
  68       let f xv cc = b_type_of (f xv) ~si g cc t in
  69       let f xv = B.push (f xv) c a (B.Abbr xv) in
  70       let f xv vv = match xv with
  71          | B.Cast _ -> f xv
  72          | _        -> assert false (* f (B.Cast ([], vv, xv)) *)
  73       in
  74       type_of f ~si g c v
  75    | B.Bind (a, B.Abst u, t) ->
  76       let f xu xt tt =
  77          f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
  78       in
  79       let f xu cc = b_type_of (f xu) ~si g cc t in
  80       let f xu _ = B.push (f xu) c a (B.Abst xu) in
  81       type_of f ~si g c u
  82    | B.Bind (a, B.Void, t)   ->
  83       let f xt tt =
  84          f (A.sh1 t xt x (B.bind a B.Void)) (B.bind a B.Void tt)
  85       in
  86       let f cc = b_type_of f ~si g cc t in
  87       B.push f c a B.Void
  88    | B.Appl (a, v, t)        ->
  89       let f xv vv xt tt =
  90          let f () = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
  91          R.assert_conversion f ~si ~rt:true c tt vv xv
  92       in
  93       let f xv vv = b_type_of (f xv vv) ~si g c t in
  94       type_of f ~si g c v
  95    | B.Cast (a, u, t)        ->
  96       let f xu xt tt =
  97          let f () = f (A.sh2 u xu t xt x (B.cast a)) xu in
  98          R.assert_conversion f ~si c xu tt xt
  99       in
 100       let f xu _ = b_type_of (f xu) ~si g c t in
 101       type_of f ~si g c u
 102
 103 and type_of f ?(si=false) g c x =
 104    let f t u = L.unbox level; f t u in
 105    L.box level; b_type_of f ~si g c x