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    d: int;                    (* inferred type iterations *)
  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 map = function
  49    | hd1 :: tl1, hd2 :: tl2 ->
  50       if map hd1 hd2 then list_and map (tl1, tl2) else false
  51    | l1, l2                 -> l1 = l2
  52
  53 let zero = Some 0
  54
  55 (* check closure *)
  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
  66          aux f (v1, v2)
  67       | B.Bind (_, b1, t1), B.Bind (_, b2, t2) ->
  68          let f _ = aux f (t1, t2) in
  69          aux_bind f (b1, b2)
  70       | _                                      -> err ()
  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 ()
  75       | _                                             -> err ()
  76    in
  77    if S.eq t1 t2 then f () else aux f (t1, t2)
  78
  79 let assert_tstep m vo = match m.n with
  80    | Some n -> n > m.d
  81    | None   -> vo
  82
  83 let tstep m = {m with d = succ m.d}
  84
  85 let tsteps m = match m.n with
  86    | Some n when n > m.d -> n - m.d
  87    | _                   -> 0
  88
  89 let get m i =
  90    let _, c, a, b = B.get m.e i in c, a, b
  91
  92 (* to share *)
  93 let rec step st m x =
  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;
  96    match x with
  97    | B.Sort (a, h)                ->
  98       if assert_tstep m false then
  99          step st (tstep m) (B.Sort (a, H.apply h))
 100       else m, x, None
 101    | B.GRef (_, uri)              ->
 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 ();
 106                step st m v
 107             end else
 108                m, x, Some v
 109          | _, _, _, E.Abst w ->
 110             if assert_tstep m true then begin
 111                if !G.summary then O.add ~grt:1 ();
 112                step st (tstep m) w
 113             end else
 114              m, x, None
 115          | _, _, _, E.Void   ->
 116             assert false
 117       end
 118    | B.LRef (_, i)                ->
 119       begin match get m i with
 120          | c, _, B.Abbr v      ->
 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
 127             end else
 128                m, B.LRef (a, i), None
 129          | _, _, B.Void        ->
 130             assert false
 131       end
 132    | B.Cast (_, u, t)             ->
 133       if assert_tstep m false then begin
 134          if !G.summary then O.add ~e:1 ();
 135          step st (tstep m) u
 136       end else begin
 137          if !G.summary then O.add ~epsilon:1 ();
 138          step st m t
 139       end
 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       let i = tsteps m in
 144       let n = if i = 0 then n else N.minus st n i in
 145       if !G.si || N.is_not_zero st n then begin match m.s with
 146          | []          ->
 147             if i = 0 then m, x, None else
 148             m, B.Bind (a, B.Abst (n, w), t), None
 149          | (c, v) :: s ->
 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
 155       end else begin
 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
 159       end
 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
 164
 165 let reset m ?(e=m.e) n =
 166    {m with e = e; n = n; s = []; d = 0}
 167
 168 let assert_iterations m1 m2 = match m1.n, m2.n with
 169       | Some n1, Some n2 -> n1 - m1.d = n2 - m2.d
 170       | _                -> false
 171
 172 let push m a b =
 173    let a, l = match b with
 174       | B.Abst _ -> {a with E.n_apix = m.l}, succ m.l
 175       | _        -> a, m.l
 176    in
 177    let e = B.push m.e m.e a b in
 178    {m with e = e; l = l}
 179
 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), _         ->
 184          h1 = 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
 199          else begin
 200             if !G.summary then O.add ~gdelta:2 ();
 201             ac st m1 v1 m2 v2
 202          end
 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
 214          else false
 215       | B.Sort _, _, B.Bind (a, B.Abst (n, _), t), _ ->
 216          if !G.si then
 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
 220          else false
 221       | _                                            -> false
 222
 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)
 226
 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
 232       ac st m1 v1 m2 v2
 233    in
 234    list_and map (m1.s, m2.s)
 235
 236 (* Interface functions ******************************************************)
 237
 238 let empty_rtm = {
 239    e = B.empty; s = []; l = 0; d = 0; n = None
 240 }
 241
 242 let get m i =
 243    assert (m.s = []);
 244    let _, _, _, b = B.get m.e i in b
 245
 246 let xwhd st m n t =
 247    if !G.trace >= level then log1 st "Now scanning" m.e t;
 248    let m, t, _ = step st (reset m n) t in
 249    m, t
 250
 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
 254    r
 255 (*    let err _ = in
 256       if S.eq mu mw then are_alpha_convertible err f u w else err () *)
 257
 258 (* error reporting **********************************************************)
 259
 260 let pp_term st m och t = BO.specs.L.pp_term st m.e och t
 261
 262 let pp_lenv st och m = BO.specs.L.pp_lenv st och m.e
 263
 264 let specs = {
 265    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 266 }