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_______________________________________________________________ *)
16 module E = BagEnvironment
17 module S = BagSubstitution
19 exception LRefNotFound of B.message
28 | LRef_ of int * B.term option
29 | GRef_ of int * B.bind
30 | Bind_ of int * B.id * B.term * B.term
36 (* Internal functions *******************************************************)
40 let error i = raise (LRefNotFound (L.items1 (string_of_int i)))
42 let empty_machine = {c = B.empty_context; s = []}
45 let f gl ges = B.contents (f gl ges) m.c in
48 let unwind_to_context f c m = B.append f c m.c
50 let unwind_to_term f m t =
51 let map f t (l, id, b) = f (B.Bind (l, id, b, t)) in
52 let f mc = C.list_fold_left f map t mc in
60 let f c = B.get f c i in
61 unwind_to_context f c m
63 let push f c m l id w =
65 let f w = B.push f c l id (B.Abst w) in
69 let rec whd f c m x = match x with
70 | B.Sort h -> f m (Sort_ h)
72 let f (i, _, b) = f m (GRef_ (i, b)) in
76 | B.Void -> f m (LRef_ (i, None))
77 | B.Abst t -> f m (LRef_ (i, Some t))
78 | B.Abbr t -> whd f c m t
81 | B.Cast (_, t) -> whd f c m t
82 | B.Appl (v, t) -> whd f c {m with s = v :: m.s} t
83 | B.Bind (l, id, B.Abst w, t) ->
85 | [] -> f m (Bind_ (l, id, w, t))
87 let f mc = whd f c {c = mc; s = tl} t in
88 B.push f m.c l id (B.Abbr (B.Cast (w, v)))
90 | B.Bind (l, id, b, t) ->
91 let f mc = whd f c {m with c = mc} t in
94 (* Interface functions ******************************************************)
96 let rec ho_whd f c m x =
98 | Sort_ h -> f c (Sort h)
99 | Bind_ (_, _, w, _) ->
100 let f c = f c (Abst w) in unwind_to_context f c m
101 | LRef_ (_, Some w) -> ho_whd f c m w
102 | GRef_ (_, B.Abst u) -> ho_whd f c m u
103 | GRef_ (_, B.Abbr t) -> ho_whd f c m t
104 | LRef_ (_, None) -> assert false
105 | GRef_ (_, B.Void) -> assert false
110 let f c r = L.unbox (); f c r in
111 L.box (); L.log O.specs level (L.ct_items1 "Now scanning" c t);
112 ho_whd f c empty_machine t
114 let rec are_convertible f c m1 t1 m2 t2 =
115 let rec aux m1 r1 m2 r2 = match r1, r2 with
116 | Sort_ h1, Sort_ h2 -> f (h1 = h2)
117 | LRef_ (i1, _), LRef_ (i2, _) ->
118 if i1 = i2 then are_convertible_stacks f c m1 m2 else f false
119 | GRef_ (a1, B.Abst _), GRef_ (a2, B.Abst _) ->
120 if a1 = a2 then are_convertible_stacks f c m1 m2 else f false
121 | GRef_ (a1, B.Abbr v1), GRef_ (a2, B.Abbr v2) ->
122 if a1 = a2 then are_convertible_stacks f c m1 m2 else
123 if a1 < a2 then whd (aux m1 r1) c m2 v2 else
124 whd (aux_rev m2 r2) c m1 v1
125 | _, GRef_ (_, B.Abbr v2) ->
126 whd (aux m1 r1) c m2 v2
127 | GRef_ (_, B.Abbr v1), _ ->
128 whd (aux_rev m2 r2) c m1 v1
129 | Bind_ (l1, id1, w1, t1), Bind_ (l2, id2, w2, t2) ->
133 S.subst (are_convertible f c m1 t1 m2) l1 l2 t2
135 push f c m1 l1 id1 w1
138 are_convertible f c m1 w1 m2 w2
140 and aux_rev m2 r2 m1 r1 = aux m1 r1 m2 r2 in
141 let f m1 r1 = whd (aux m1 r1) c m2 t2 in
144 and are_convertible_stacks f c m1 m2 =
145 let mm1, mm2 = {m1 with s = []}, {m2 with s = []} in
146 let map f v1 v2 = are_convertible f c mm1 v1 mm2 v2 in
147 if List.length m1.s <> List.length m2.s then f false else
148 C.forall2 f map m1.s m2.s
150 let are_convertible f c t1 t2 =
151 let f b = L.unbox (); f b in
153 L.log O.specs level (L.ct_items2 "Now converting" c t1 "and" c t2);
154 are_convertible f c empty_machine t1 empty_machine t2