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_______________________________________________________________ *)
22 module BE = BrgEnvironment
25 e: B.lenv; (* environment *)
26 s: (B.lenv * B.term) list; (* stack *)
28 d: int; (* inferred type iterations *)
29 n: int option; (* expected type iterations *)
32 type message = (rtm, B.term) L.message
34 (* Internal functions *******************************************************)
38 let sublevel = succ level
41 let s1, s2 = s ^ " in the environment", "the term" in
42 L.log st BO.specs level (L.et_items1 s1 c s2 t)
44 let log2 st s cu u ct t =
45 let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
46 L.log st BO.specs level (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
48 let rec list_and map = function
49 | hd1 :: tl1, hd2 :: tl2 ->
50 if map hd1 hd2 then list_and map (tl1, tl2) else false
56 let are_alpha_convertible err f t1 t2 =
57 let rec aux f = function
58 | B.Sort (_, p1), B.Sort (_, p2)
59 | B.LRef (_, p1), B.LRef (_, p2) ->
60 if p1 = p2 then f () else err ()
61 | B.GRef (_, u1), B.GRef (_, u2) ->
62 if U.eq u1 u2 then f () else err ()
63 | B.Cast (_, v1, t1), B.Cast (_, v2, t2)
64 | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
65 let f _ = aux f (t1, t2) in
67 | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
68 let f _ = aux f (t1, t2) in
71 and aux_bind f = function
72 | B.Abbr v1, B.Abbr v2 -> aux f (v1, v2)
73 | B.Abst (n1, v1), B.Abst (n2, v2) when n1 = n2 -> aux f (v1, v2)
74 | B.Void, B.Void -> f ()
77 if S.eq t1 t2 then f () else aux f (t1, t2)
79 let assert_tstep m vo = match m.n with
83 let tstep m = {m with d = succ m.d}
85 let tsteps m = match m.n with
86 | Some n when n > m.d -> n - m.d
90 let _, c, a, b = B.get m.e i in c, a, b
94 if !G.trace >= sublevel then
95 log1 st (Printf.sprintf "entering R.step: l:%u d:%i n:%s" m.l m.d (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e x;
98 if assert_tstep m false then
99 step st (tstep m) (B.Sort (a, H.apply h))
102 begin match BE.get_entity uri with
103 | _, _, _, E.Abbr v ->
104 if m.n = None || !G.expand then begin
105 if !G.summary then O.add ~gdelta:1 ();
109 | _, _, _, E.Abst w ->
110 if assert_tstep m true then begin
111 if !G.summary then O.add ~grt:1 ();
119 begin match get m i with
121 if !G.summary then O.add ~ldelta:1 ();
122 step st {m with e = c} v
123 | c, a, B.Abst (_, w) ->
124 if assert_tstep m true then begin
125 if !G.summary then O.add ~lrt:1 ();
126 step st {(tstep m) with e = c} w
128 m, B.LRef (a, i), None
132 | B.Cast (_, u, t) ->
133 if assert_tstep m false then begin
134 if !G.summary then O.add ~e:1 ();
137 if !G.summary then O.add ~epsilon:1 ();
140 | B.Appl (_, v, t) ->
141 step st {m with s = (m.e, v) :: m.s} t
142 | B.Bind (a, B.Abst (n, w), t) ->
143 if !G.si || N.is_not_zero st n then begin match m.s with
146 if i = 0 then m, x, None else
147 let n = N.minus st n i in
148 m, B.Bind (a, B.Abst (n, w), t), None
150 if !G.cc && not (N.assert_not_zero st n) then assert false;
151 if !G.summary then O.add ~beta:1 ~theta:(List.length s) ();
152 let v = if assert_tstep m false then B.Cast (E.empty_node, w, v) else v in
153 let e = B.push m.e c a (B.abbr v) in
154 step st {m with e = e; s = s} t
156 if !G.summary then O.add ~upsilon:1 ();
157 let e = B.push m.e m.e a B.Void in
158 step st {m with e = e} t
160 | B.Bind (a, b, t) ->
161 if !G.summary then O.add ~theta:(List.length m.s) ();
162 let e = B.push m.e m.e a b in
163 step st {m with e = e} t
165 let reset m ?(e=m.e) n =
166 {m with e = e; n = n; s = []; d = 0}
168 let assert_iterations m1 m2 = match m1.n, m2.n with
169 | Some n1, Some n2 -> n1 - m1.d = n2 - m2.d
173 let a, l = match b with
174 | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
177 let e = B.push m.e m.e a b in
178 {m with e = e; l = l}
180 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
181 if !G.trace >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2;
182 match t1, r1, t2, r2 with
183 | B.Sort (_, h1), _, B.Sort (_, h2), _ ->
185 | B.LRef ({E.n_apix = e1}, _), _,
186 B.LRef ({E.n_apix = e2}, _), _ ->
187 if e1 = e2 then ac_stacks st m1 m2 else false
188 | B.GRef (_, u1), None, B.GRef (_, u2), None ->
189 if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
190 | B.GRef ({E.n_apix = e1}, u1), Some v1,
191 B.GRef ({E.n_apix = e2}, u2), Some v2 ->
192 if e1 < e2 then begin
193 if !G.summary then O.add ~gdelta:1 ();
194 ac_nfs st (m1, t1, r1) (step st m2 v2)
195 end else if e2 < e1 then begin
196 if !G.summary then O.add ~gdelta:1 ();
197 ac_nfs st (step st m1 v1) (m2, t2, r2)
198 end else if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
200 if !G.summary then O.add ~gdelta:2 ();
203 | _, _, B.GRef _, Some v2 ->
204 if !G.summary then O.add ~gdelta:1 ();
205 ac_nfs st (m1, t1, r1) (step st m2 v2)
206 | B.GRef _, Some v1, _, _ ->
207 if !G.summary then O.add ~gdelta:1 ();
208 ac_nfs st (step st m1 v1) (m2, t2, r2)
209 | B.Bind (a1, (B.Abst (n1, w1) as b1), t1), _,
210 B.Bind (a2, (B.Abst (n2, w2) as b2), t2), _ ->
211 if !G.cc && not (N.assert_equal st n1 n2) then false else
212 if ac st (reset m1 zero) w1 (reset m2 zero) w2 then
213 ac st (push m1 a1 b1) t1 (push m2 a2 b2) t2
215 | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
217 if !G.cc && not (N.assert_zero st n) then false else begin
218 if !G.summary then O.add ~upsilon:1 ();
219 ac st (push m1 a B.Void) t1 (push m2 a B.Void) t end
223 and ac st m1 t1 m2 t2 =
224 (* L.warn "entering R.are_convertible"; *)
225 ac_nfs st (step st m1 t1) (step st m2 t2)
227 and ac_stacks st m1 m2 =
228 (* L.warn "entering R.are_convertible_stacks"; *)
229 if List.length m1.s <> List.length m2.s then false else
230 let map (c1, v1) (c2, v2) =
231 let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
234 list_and map (m1.s, m2.s)
236 (* Interface functions ******************************************************)
239 e = B.empty; s = []; l = 0; d = 0; n = None
244 let _, _, _, b = B.get m.e i in b
247 if !G.trace >= level then log1 st "Now scanning" m.e t;
248 let m, t, _ = step st (reset m n) t in
251 let are_convertible st m1 n1 t1 m2 n2 t2 =
252 if !G.trace >= level then log2 st "Now converting" m1.e t1 m2.e t2;
253 let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
256 if S.eq mu mw then are_alpha_convertible err f u w else err () *)
258 (* error reporting **********************************************************)
260 let pp_term st m och t = BO.specs.L.pp_term st m.e och t
262 let pp_lenv st och m = BO.specs.L.pp_lenv st och m.e
265 L.pp_term = pp_term; L.pp_lenv = pp_lenv