]> matita.cs.unibo.it Git - helm.git/blob - helm/software/lambda-delta/basic_rg/brgType.ml
0afb9c70b23296968ef722dccb265483d04a89ab
[helm.git] / 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 Y = Entity
18 module B = Brg
19 module O = BrgOutput
20 module E = BrgEnvironment
21 module S = BrgSubstitution
22 module R = BrgReduction
23
24 type message = (R.kam, B.term) Log.message
25
26 (* Internal functions *******************************************************)
27
28 let level = 4
29
30 let message1 st1 m t1 =
31    L.et_items1 "In the environment" m st1 t1
32
33 let log1 s m t =
34    let s =  s ^ " the term" in
35    L.log R.specs level (message1 s m t) 
36
37 let error1 err s m t =
38    err (message1 s m t)
39
40 let message3 m t1 t2 ?mu t3 =    
41    let sm, st1, st2 = "In the environment", "the term", "is of type" in
42    match mu with
43       | Some mu ->
44          let smu, st3 = "but in the environment", "it must be of type" in
45          L.et_items3 sm m st1 t1 st2 t2 ~sc3:smu ~c3:mu st3 t3
46       | None    ->
47          let st3 = "but it must be of type" in
48          L.et_items3 sm m st1 t1 st2 t2 st3 t3
49    
50 let error3 err m t1 t2 ?mu t3 =
51    err (message3 m t1 t2 ?mu t3)
52
53 let assert_convertibility err f st m u w v =
54    if R.are_convertible st m u m w then f () else
55    error3 err m v w u
56
57 let assert_applicability err f st m u w v =
58    match R.xwhd st m u with 
59       | _, B.Sort _                   -> error1 err "not a function type" m u
60       | mu, B.Bind (B.Abst (_, u), _) -> 
61          if R.are_convertible st mu u m w then f () else
62          error3 err m v w ~mu u
63       | _                         -> assert false (**)
64
65 let rec b_type_of err f st g m x =
66    log1 "Now checking" m x;
67    match x with
68    | B.Sort (a, h)             ->
69       let f h = f x (B.Sort (a, h)) in H.apply f g h
70    | B.LRef (_, i)             ->
71       let f = function
72          | B.Abst (_, w)                ->
73             f x (S.lift (succ i) (0) w)
74          | B.Abbr (_, B.Cast (_, w, _)) -> 
75             f x (S.lift (succ i) (0) w)
76          | B.Abbr _                     -> assert false
77          | B.Void _                     -> 
78             error1 err "reference to excluded variable" m x
79       in
80       let err _ = error1 err "reference to unknown variable" m x in
81       R.get err f m i
82    | B.GRef (_, uri)           ->
83       begin match E.get_entity uri with
84          | _, _, Y.Abst w                  -> f x w
85          | _, _, Y.Abbr (B.Cast (_, w, _)) -> f x w
86          | _, _, Y.Abbr _                  -> assert false
87          | _, _, Y.Void                    ->
88             error1 err "reference to unknown entry" m x
89       end
90    | B.Bind (B.Abbr (a, v), t) ->
91       let f xv xt tt =
92          f (A.sh2 v xv t xt x (B.bind_abbr a)) (B.bind_abbr a xv tt)
93       in
94       let f xv m = b_type_of err (f xv) st g m t in
95       let f xv = f xv (R.push m (B.abbr a xv)) in
96       let f xv vv = match xv with 
97          | B.Cast _ -> f xv
98          | _        -> f (B.Cast ([], vv, xv))
99       in
100       type_of err f st g m v
101    | B.Bind (B.Abst (a, u), t) ->
102       let f xu xt tt =
103          f (A.sh2 u xu t xt x (B.bind_abst a)) (B.bind_abst a xu tt)
104       in
105       let f xu m = b_type_of err (f xu) st g m t in
106       let f xu _ = f xu (R.push m (B.abst a xu)) in
107       type_of err f st g m u
108    | B.Bind (B.Void a as b, t) ->
109       let f xt tt = 
110          f (A.sh1 t xt x (B.bind b)) (B.bind b tt)
111       in
112       b_type_of err f st g (R.push m b) t
113          
114    | B.Appl (a, v, t)          ->
115       let f xv vv xt tt = 
116          let f _ = f (A.sh2 v xv t xt x (B.appl a)) (B.appl a xv tt) in
117          assert_applicability err f st m tt vv xv
118       in
119       let f xv vv = b_type_of err (f xv vv) st g m t in
120       type_of err f st g m v
121    | B.Cast (a, u, t)          ->
122       let f xu xt tt =  
123          let f _ = f (A.sh2 u xu t xt x (B.cast a)) xu in
124          assert_convertibility err f st m xu tt xt
125       in
126       let f xu _ = b_type_of err (f xu) st g m t in
127       type_of err f st g m u
128
129 (* Interface functions ******************************************************)
130
131 and type_of err f st g m x =
132    let f t u = L.unbox level; f t u in
133    L.box level; b_type_of err f st g m x