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.
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_______________________________________________________________ *)
17 module E = BrgEnvironment
19 type environment = int * B.bind list
21 type stack = B.term list
29 exception LRefNotFound of (context, B.term) L.item list
33 | LRef_ of int * B.term option
34 | GRef_ of int * B.bind
35 | Bind_ of B.term * B.term
41 (* Internal functions *******************************************************)
43 let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
47 let push_e f b (l, e) =
51 let (gl, ge), (ll, le) = c.g, c.l in
52 if i >= gl + ll then error i;
54 if i < gl then List.nth ge (gl - (succ i))
55 else List.nth le (gl + ll - (succ i))
59 let rec lref_map_bind f map b = match b with
61 let f v' = f (S.sh1 v v' b B.abbr) in
64 let f w' = f (S.sh1 w w' b B.abst) in
68 and lref_map f map t = match t with
69 | B.LRef i -> f (B.LRef (map i))
73 let f w' u' = f (S.sh2 w w' u u' t B.cast) in
74 let f w' = lref_map (f w') map u in
77 let f w' u' = f (S.sh2 w w' u u' t B.appl) in
78 let f w' = lref_map (f w') map u in
80 | B.Bind (id, b, u) ->
81 let f b' u' = f (S.sh2 b b' u u' t (B.bind id)) in
82 let f b' = lref_map (f b') map u in
87 let (gl, _), (ll, le) = c.g, c.l in
88 let map i = if i >= gl then succ i else i in
90 | B.Abbr t -> let f t' = f (B.Abbr t') in lref_map f map t
93 let f le' = f {c with l = (ll, le')} in
97 let (gl, _), (ll, _) = c.g, c.l in
99 if i < gl || i > gl + ll then i else
100 if i >= gl && i < gl + ll then succ i else gl
105 let rec whd f c t = match t with
106 | B.Sort h -> f c (Sort_ h)
108 let f (i, _, b) = f c (GRef_ (i, b)) in
112 | B.Void -> f c (LRef_ (i, None))
113 | B.Abst t -> f c (LRef_ (i, Some t))
114 | B.Abbr t -> whd f c t
117 | B.Cast (_, t) -> whd f c t
118 | B.Appl (v, t) -> whd f {c with s = v :: c.s} t
119 | B.Bind (_, B.Abst w, t) ->
121 | [] -> f c (Bind_ (w, t))
123 let f tl l = whd f {c with l = l; s = tl} t in
124 push_e (f tl) (B.Abbr v) c.l
126 | B.Bind (_, b, t) ->
127 let f l = whd f {c with l = l} t in
132 let f c g = xchg f {c with g = g} t in
133 let f c = push_e (f c) B.Void c.g in
136 (* Interface functions ******************************************************)
138 let rec are_convertible f c1 t1 c2 t2 =
139 let rec aux c1' r1 c2' r2 = match r1, r2 with
140 | Sort_ h1, Sort_ h2 -> f (h1 = h2)
141 | LRef_ (i1, _), LRef_ (i2, _) ->
142 if i1 = i2 then are_convertible_stacks f c1' c2' else f false
143 | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) ->
144 if a1 = a2 then are_convertible_stacks f c1' c2' else f false
145 | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
146 if a1 = a2 then are_convertible_stacks f c1' c2' else
147 if a1 < a2 then whd (aux c1' r1) c2' v2 else
148 whd (aux_rev c2' r2) c1' v1
149 | _, GRef_ (_, B.Abbr v2) ->
150 whd (aux c1' r1) c2' v2
151 | GRef_ (_, B.Abbr v1), _ ->
152 whd (aux_rev c2' r2) c1' v1
153 | Bind_ (w1, t1), Bind_ (w2, t2) ->
156 let f c1'' t1' = push (are_convertible f c1'' t1') c2' t2 in
160 are_convertible f c1' w1 c2' w2
162 and aux_rev c2 r2 c1 r1 = aux c1 r1 c2 r2 in
163 let f c1' r1 = whd (aux c1' r1) c2 t2 in
166 and are_convertible_stacks f c1 c2 =
167 let map f v1 v2 = are_convertible f c1 v1 c2 v2 in
168 if List.length c1.s <> List.length c2.s then f false else
169 C.forall2 f map c1.s c2.s
171 let are_convertible f c t1 t2 = are_convertible f c t1 c t2
173 let rec ho_whd f c t =
174 let aux c' = function
175 | Sort_ h -> f c' (Sort h)
176 | Bind_ (w, t) -> f c' (Abst w)
177 | LRef_ (_, Some w) -> ho_whd f c w
178 | GRef_ (_, B.Abst u) -> ho_whd f c u
179 | GRef_ (_, B.Abbr u) -> ho_whd f c u
180 | LRef_ (_, None) -> assert false
181 | GRef_ (_, B.Void) -> assert false
186 assert (c.l = empty_e && c.s = []);
187 let f g = f {c with g = g} in
192 if i >= gl then error i;
193 f (List.nth ge (gl - (succ i)))
195 let empty_context = {
196 g = empty_e; l = empty_e; s = []