helm/software/helena/src/basic_rg/brgReduction.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 S  = Share
  14 module L  = Log
  15 module G  = Options
  16 module H  = Hierarchy
  17 module N  = Layer
  18 module E  = Entity
  19 module O  = Output
  20 module B  = Brg
  21 module BO = BrgOutput
  22 module BE = BrgEnvironment
  23
  24 type rtm = {
  25    e: B.lenv;                 (* environment              *)
  26    s: (B.lenv * B.term) list; (* stack                    *)
  27    l: int;                    (* level                    *)
  28    n: int option;             (* expected type iterations *)
  29 }
  30
  31 type message = (rtm, B.term) L.message
  32
  33 (* Internal functions *******************************************************)
  34
  35 let level = 5
  36
  37 let sublevel = succ level
  38
  39 let log1 st s c t =
  40    let s1, s2 = s ^ " in the environment", "the term" in
  41    L.log st BO.specs (pred level) (L.et_items1 s1 c s2 t)
  42
  43 let log2 st s cu u ct t =
  44    let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in
  45    L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t)
  46
  47 let rec list_and map = function
  48    | hd1 :: tl1, hd2 :: tl2 ->
  49       if map hd1 hd2 then list_and map (tl1, tl2) else false
  50    | l1, l2                 -> l1 = l2
  51
  52 let zero = Some 0
  53
  54 (* check closure *)
  55 let are_alpha_convertible err f t1 t2 =
  56    let rec aux f = function
  57       | B.Sort p1, B.Sort p2
  58       | B.LRef (_, p1), B.LRef (_, p2)         ->
  59          if p1 = p2 then f () else err ()
  60       | B.GRef (_, u1), B.GRef (_, u2)         ->
  61          if U.eq u1 u2 then f () else err ()
  62       | B.Cast (v1, t1), B.Cast (v2, t2)
  63       | B.Appl (_, v1, t1), B.Appl (_, v2, t2) ->
  64          let f _ = aux f (t1, t2) in
  65          aux f (v1, v2)
  66       | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
  67          let f _ = aux f (t1, t2) in
  68          aux_bind f (b1, b2)
  69       | _                                      -> err ()
  70    and aux_bind f = function
  71       | B.Abbr v1, B.Abbr v2                                             -> aux f (v1, v2)
  72       | B.Abst (r1, n1, v1), B.Abst (r2, n2, v2) when r1 = r2 && n1 = n2 -> aux f (v1, v2)
  73       | B.Void, B.Void                                                   -> f ()
  74       | _                                                                -> err ()
  75    in
  76    if S.eq t1 t2 then f () else aux f (t1, t2)
  77
  78 let assert_tstep m vo = match m.n with
  79    | Some n -> n > 0
  80    | None   -> vo
  81
  82 let tstep m = match m.n with
  83    | Some n -> {m with n = Some (pred n)}
  84    | None   -> m
  85
  86 let tsteps m = match m.n with
  87    | Some n -> n
  88    | None   -> 0
  89
  90 let get m i =
  91    let _, c, a, _, b = B.get m.e i in c, a, b
  92
  93 (* to share *)
  94 let rec step st m r =
  95 IFDEF TRACE THEN
  96    if !G.ct >= sublevel then
  97    log1 st (Printf.sprintf "entering R.step: l=%u, n=%s," m.l (match m.n with Some n -> string_of_int n | None -> "infinite")) m.e r
  98 ELSE () END;
  99    match r with
 100    | B.Sort k                            ->
 101       if assert_tstep m false then
 102          step st (tstep m) (B.Sort (H.apply k))
 103       else m, r, None
 104    | B.GRef (_, u)                       ->
 105       begin match BE.get_entity u with
 106          | _, a, _, E.Abbr v ->
 107                m, B.gref a u, Some v
 108          | _, _, _, E.Abst w ->
 109             if assert_tstep m true then begin
 110 IFDEF SUMMARY THEN
 111                if !G.summary then O.add ~grt:1 ()
 112 ELSE () END;
 113                step st (tstep m) w
 114             end else
 115                m, r, None
 116          | _, _, _, E.Void   ->
 117             assert false
 118       end
 119    | B.LRef (_, i)                       ->
 120       begin match get m i with
 121          | c, _, B.Abbr v         ->
 122 IFDEF SUMMARY THEN
 123             if !G.summary then O.add ~ldelta:1 ()
 124 ELSE () END;
 125             step st {m with e = c} v
 126          | c, a, B.Abst (_, _, w) ->
 127             if assert_tstep m true then begin
 128 IFDEF SUMMARY THEN
 129                if !G.summary then O.add ~lrt:1 ()
 130 ELSE () END;
 131                step st {(tstep m) with e = c} w
 132             end else
 133                m, B.lref a i, None
 134          | _, _, B.Void           ->
 135             assert false
 136       end
 137    | B.Cast (u, t)                       ->
 138       if assert_tstep m false then begin
 139 IFDEF SUMMARY THEN
 140          if !G.summary then O.add ~e:1 ()
 141 ELSE () END;
 142          step st (tstep m) u
 143       end else begin
 144 IFDEF SUMMARY THEN
 145          if !G.summary then O.add ~epsilon:1 ()
 146 ELSE () END;
 147          step st m t
 148       end
 149    | B.Appl (_, v, t)                    ->
 150       step st {m with s = (m.e, v) :: m.s} t
 151    | B.Bind (y, B.Abst (false, n, w), t) ->
 152       let i = tsteps m in
 153 IFDEF SUMMARY THEN
 154       if !G.summary then O.add ~x:i ()
 155 ELSE () END;
 156       let n = if i = 0 then n else N.minus st n i in
 157       let r = B.Bind (y, B.Abst (true, n, w), t) in
 158       step st m r
 159    | B.Bind (y, B.Abst (true, n, w), t)  ->
 160       if !G.si || N.is_not_zero st n then begin match m.s with
 161          | []          ->
 162             m, B.Bind (y, B.Abst (true, n, w), t), None
 163          | (c, v) :: s ->
 164 IFDEF SUMMARY THEN
 165             if !G.summary then O.add ~beta:1 ~theta:(List.length s) ()
 166 ELSE () END;
 167             let v = B.Cast (w, v) in
 168             let e = B.push m.e c E.empty_node y (B.abbr v) in
 169             step st {m with e = e; s = s} t
 170       end else begin
 171 IFDEF SUMMARY THEN
 172          if !G.summary then O.add ~upsilon:1 ()
 173 ELSE () END;
 174          let e = B.push m.e m.e E.empty_node y B.Void in (**) (* this is wrong in general *)
 175          step st {m with e = e} t
 176       end
 177    | B.Bind (y, b, t)        ->
 178 IFDEF SUMMARY THEN
 179       if !G.summary then O.add ~theta:(List.length m.s) ()
 180 ELSE () END;
 181       let e = B.push m.e m.e E.empty_node y b in
 182       step st {m with e = e} t
 183
 184 let assert_iterations m1 m2 =
 185    m1.n = m2.n
 186
 187 let reset m ?(e=m.e) n =
 188    {m with e = e; n = n; s = []}
 189
 190 let push m y b =
 191    let a, l = match b with
 192       | B.Abst _ -> E.node_attrs ~apix:m.l (), succ m.l
 193       | _        -> E.empty_node, m.l
 194    in
 195    let e = B.push m.e m.e a y b in
 196    {m with e = e; l = l}
 197
 198 let rec ac_nfs st (m1, t1, r1) (m2, t2, r2) =
 199 IFDEF TRACE THEN
 200    if !G.ct >= level then log2 st "Now converting nfs" m1.e t1 m2.e t2
 201 ELSE () END;
 202    match t1, r1, t2, r2 with
 203       | B.Sort k1, _, B.Sort k2, _                         ->
 204          k1 = k2
 205       | B.LRef ({E.n_apix = e1}, _), _,
 206         B.LRef ({E.n_apix = e2}, _), _                     ->
 207          if e1 = e2 then ac_stacks st m1 m2 else false
 208       | B.GRef (_, u1), None, B.GRef (_, u2), None   ->
 209          if U.eq u1 u2 && assert_iterations m1 m2 then ac_stacks st m1 m2 else false
 210       | B.GRef ({E.n_apix = e1}, u1), Some v1,
 211         B.GRef ({E.n_apix = e2}, u2), Some v2              ->
 212          if U.eq u1 u2 && assert_iterations m1 m2 && ac_stacks st m1 m2 then true
 213          else if e1 < e2 then begin
 214 IFDEF SUMMARY THEN
 215             if !G.summary then O.add ~gdelta:1 ()
 216 ELSE () END;
 217             ac_nfs st (m1, t1, r1) (step st m2 v2)
 218          end else if e2 < e1 then begin
 219 IFDEF SUMMARY THEN
 220             if !G.summary then O.add ~gdelta:1 ()
 221 ELSE () END;
 222             ac_nfs st (step st m1 v1) (m2, t2, r2)
 223          end else begin
 224 IFDEF SUMMARY THEN
 225             if !G.summary then O.add ~gdelta:2 ()
 226 ELSE () END;
 227             ac st m1 v1 m2 v2
 228          end
 229       | _, _, B.GRef _, Some v2                            ->
 230 IFDEF SUMMARY THEN
 231          if !G.summary then O.add ~gdelta:1 ()
 232 ELSE () END;
 233          ac_nfs st (m1, t1, r1) (step st m2 v2)
 234       | B.GRef _, Some v1, _, _                            ->
 235 IFDEF SUMMARY THEN
 236          if !G.summary then O.add ~gdelta:1 ()
 237 ELSE () END;
 238          ac_nfs st (step st m1 v1) (m2, t2, r2)
 239       | B.Bind (y1, (B.Abst (true, n1, w1) as b1), t1), _,
 240         B.Bind (y2, (B.Abst (true, n2, w2) as b2), t2), _  ->
 241          if ((!G.cc && N.assert_equal st n1 n2) || N.are_equal st n1 n2) &&
 242             ac st (reset m1 zero) w1 (reset m2 zero) w2
 243          then ac st (push m1 y1 b1) t1 (push m2 y2 b2) t2
 244          else false
 245       | B.Sort _, _, B.Bind (y, B.Abst (true, n, _), t), _ ->
 246          if !G.si then
 247             if !G.cc && not (N.assert_zero st n) then false else begin
 248 IFDEF SUMMARY THEN
 249             if !G.summary then O.add ~upsilon:1 ()
 250 ELSE () END;
 251             ac st (push m1 y B.Void) t1 (push m2 y B.Void) t end
 252          else false
 253       | _                                                  -> false
 254
 255 and ac st m1 t1 m2 t2 =
 256 (*   L.warn "entering R.are_convertible"; *)
 257    ac_nfs st (step st m1 t1) (step st m2 t2)
 258
 259 and ac_stacks st m1 m2 =
 260 (*   L.warn "entering R.are_convertible_stacks"; *)
 261    if List.length m1.s <> List.length m2.s then false else
 262    let map (c1, v1) (c2, v2) =
 263       let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in
 264       ac st m1 v1 m2 v2
 265    in
 266    list_and map (m1.s, m2.s)
 267
 268 let rec ih_nfs st (m, t, r) =
 269    match t, r with
 270       | B.GRef _, Some v ->
 271 IFDEF SUMMARY THEN
 272          if !G.summary then O.add ~gdelta:1 ()
 273 ELSE () END;
 274          ih st m v
 275       | _                -> m, t
 276
 277 and ih st m t = ih_nfs st (step st m t)
 278
 279 (* Interface functions ******************************************************)
 280
 281 let empty_rtm = {
 282    e = B.empty; s = []; l = 0; n = None
 283 }
 284
 285 let get m i =
 286    assert (m.s = []);
 287    let _, _, _, _, b = B.get m.e i in b
 288
 289 let xwhd st m n t =
 290 IFDEF TRACE THEN
 291    if !G.ct >= level then log1 st "Now scanning" m.e t
 292 ELSE () END;
 293    ih st (reset m n) t
 294
 295 let are_convertible st m1 n1 t1 m2 n2 t2 =
 296 IFDEF TRACE THEN
 297    if !G.ct >= level then log2 st "Now converting" m1.e t1 m2.e t2
 298 ELSE () END;
 299    let r = ac st (reset m1 n1) t1 (reset m2 n2) t2 in
 300    r
 301 (*    let err _ = in
 302       if S.eq mu mw then are_alpha_convertible err f u w else err () *)
 303
 304 (* error reporting **********************************************************)
 305
 306 let pp_term st m och t = BO.specs.L.pp_term st m.e och t
 307
 308 let pp_lenv st och m = BO.specs.L.pp_lenv st och m.e
 309
 310 let specs = {
 311    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 312 }