helm/software/helena/src/basic_ag/bagType.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 S  = Share
  15 module L  = Log
  16 module G  = Options
  17 module H  = Hierarchy
  18 module E  = Entity
  19 module Z  = Bag
  20 module ZO = BagOutput
  21 module ZE = BagEnvironment
  22 module ZR = BagReduction
  23
  24 (* Internal functions *******************************************************)
  25
  26 let level = 4
  27
  28 let log1 st s c t =
  29    let s1, s2 = s ^ " in the envireonment", "the term" in
  30    L.log st ZO.specs (pred level) (L.et_items1 s1 c s2 t)
  31
  32 let error1 err st c t =
  33    let sc = "In the envireonment" in
  34    err (L.et_items1 sc c st t)
  35
  36 let error3 err c t1 t2 t3 =
  37    let sc, st1, st2, st3 =
  38       "In the envireonment", "the term", "is of type", "but must be of type"
  39    in
  40    err (L.et_items3 sc c st1 t1 st2 t2 st3 t3)
  41
  42 let mk_gref u l =
  43    let map t v = Z.Appl (v, t) in
  44    List.fold_left map (Z.GRef u) l
  45
  46 let rec b_type_of err f st c x =
  47 (*   L.warn "Entering T.b_type_of"; *)
  48    if !G.ct >= level then log1 st "Now checking" c x;
  49    match x with
  50    | Z.Sort h                   ->
  51       let h = H.apply h in f x (Z.Sort h)
  52    | Z.LRef i                   ->
  53       let err0 () = error1 err "variable not found" c x in
  54       let f _ = function
  55          | Z.Abst w               -> f x w
  56          | Z.Abbr (Z.Cast (w, v)) -> f x w
  57          | Z.Abbr _               -> assert false
  58          | Z.Void                 -> error1 err "reference to excluded variable" c x
  59       in
  60       Z.get err0 f c i
  61    | Z.GRef uri                 ->
  62       let f = function
  63          | _, _, _, E.Abst w               -> f x w
  64          | _, _, _, E.Abbr (Z.Cast (w, v)) -> f x w
  65          | _, _, _, E.Abbr _               -> assert false
  66          | _, _, _, E.Void                 -> assert false
  67       in
  68       ZE.get_entity f uri
  69    | Z.Bind (y, l, Z.Abbr v, t) ->
  70       let f xv xt tt =
  71          f (S.sh2 v xv t xt x (Z.bind_abbr y l)) (Z.bind_abbr y l xv tt)
  72       in
  73       let f xv cc = b_type_of err (f xv) st cc t in
  74       let f xv = Z.push "type abbr" (f xv) c y l (Z.Abbr xv) in
  75       let f xv vv = match xv with
  76          | Z.Cast _ -> f xv
  77          | _        -> f (Z.Cast (vv, xv))
  78       in
  79       type_of err f st c v
  80    | Z.Bind (y, l, Z.Abst u, t) ->
  81       let f xu xt tt =
  82          f (S.sh2 u xu t xt x (Z.bind_abst y l)) (Z.bind_abst y l xu tt)
  83       in
  84       let f xu cc = b_type_of err (f xu) st cc t in
  85       let f xu _ = Z.push "type abst" (f xu) c y l (Z.Abst xu) in
  86       type_of err f st c u
  87    | Z.Bind (y, l, Z.Void, t)   ->
  88       let f xt tt =
  89          f (S.sh1 t xt x (Z.bind y l Z.Void)) (Z.bind y l Z.Void tt)
  90       in
  91       let f cc = b_type_of err f st cc t in
  92       Z.push "type void" f c y l Z.Void
  93    | Z.Appl (v, t)              ->
  94       let f xv vv xt tt = function
  95          | ZR.Abst w ->
  96             if !G.ct > level then L.log st ZO.specs level (L.t_items1 "Just scanned" c w);
  97             let f a =
  98 (*             L.warn (Printf.sprintf "Convertible: %b" a); *)
  99                if a then f (S.sh2 v xv t xt x Z.appl) (Z.appl xv tt)
 100                else error3 err c xv vv w
 101             in
 102             ZR.are_convertible f st c w vv
 103          | _         ->
 104             error1 err "not a function" c xt
 105       in
 106       let f xv vv xt tt = ZR.ho_whd (f xv vv xt tt) st c tt in
 107       let f xv vv = b_type_of err (f xv vv) st c t in
 108       type_of err f st c v
 109    | Z.Cast (u, t)              ->
 110       let f xu xt tt a =
 111          (* L.warn (Printf.sprintf "Convertible: %b" a); *)
 112          if a then f (S.sh2 u xu t xt x Z.cast) xu else error3 err c xt tt xu
 113       in
 114       let f xu xt tt = ZR.are_convertible (f xu xt tt) st c xu tt in
 115       let f xu _ = b_type_of err (f xu) st c t in
 116       type_of err f st c u
 117
 118 (* Interface functions ******************************************************)
 119
 120 and type_of err f st c x = b_type_of err f st c x