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