components/content_pres/cicClassify.ml

   1 (* Copyright (C) 2003-2005, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 module C = Cic
  27 module CS = CicSubstitution
  28 module D = Deannotate
  29 module Int = struct
  30    type t = int
  31    let compare = compare
  32 end
  33 module S = Set.Make (Int)
  34
  35 type conclusion = (int * int) option
  36
  37 (* debugging ****************************************************************)
  38
  39 let string_of_entry inverse =
  40    if S.mem 0 inverse then "C" else
  41    if S.is_empty inverse then "I" else "P"
  42
  43 let to_string (classes, rc) =
  44    let linearize = String.concat " " (List.map string_of_entry classes) in
  45    match rc with
  46       | None        -> linearize
  47       | Some (i, j) -> Printf.sprintf "%s %u %u" linearize i j
  48
  49 let out_table b =
  50    let map i (_, inverse) =
  51       let map i tl = Printf.sprintf "%2u" i :: tl in
  52       let iset = String.concat " " (S.fold map inverse []) in
  53       Printf.eprintf "%2u|%s\n" i iset
  54    in
  55    Array.iteri map b;
  56    prerr_newline ()
  57
  58 (****************************************************************************)
  59
  60 let rec list_fold_left g map = function
  61   | []       -> g
  62   | hd :: tl -> map (list_fold_left g map tl) hd
  63
  64 let get_rels h t =
  65    let rec aux d g = function
  66       | C.Sort _
  67       | C.Implicit _       -> g
  68       | C.Rel i            ->
  69          if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
  70       | C.Appl ss          -> list_fold_left g (aux d) ss
  71       | C.Const (_, ss)
  72       | C.MutInd (_, _, ss)
  73       | C.MutConstruct (_, _, _, ss)
  74       | C.Var (_, ss)      ->
  75          let map g (_, t) = aux d g t in
  76          list_fold_left g map ss
  77       | C.Meta (_, ss)     ->
  78          let map g = function
  79             | None   -> g
  80             | Some t -> aux d g t
  81          in
  82          list_fold_left g map ss
  83       | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
  84       | C.LetIn (_, t1, t2)
  85       | C.Lambda (_, t1, t2)
  86       | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
  87       | C.MutCase (_, _, t1, t2, ss) ->
  88          aux d (aux d (list_fold_left g (aux d) ss) t2) t1
  89       | C.Fix (_, ss) ->
  90          let k = List.length ss in
  91          let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
  92          list_fold_left g map ss
  93       | C.CoFix (_, ss) ->
  94          let k = List.length ss in
  95          let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
  96          list_fold_left g map ss
  97    in
  98    let g a = a in
  99    aux 1 g t S.empty
 100
 101 let split t =
 102    let rec aux a n = function
 103       | C.Prod (_, v, t)  -> aux (v :: a) (succ n) t
 104       | C.Cast (t, v)     -> aux a n t
 105       | C.LetIn (_, v, t) -> aux a n (CS.subst v t)
 106       | v                 -> v :: a, n
 107     in
 108     aux [] 0 t
 109
 110 let classify_conclusion = function
 111    | C.Rel i                -> Some (i, 0)
 112    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
 113    | _                      -> None
 114
 115 let classify t =
 116    let vs, h = split t in
 117    let rc = classify_conclusion (List.hd vs) in
 118    let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
 119    let l, h = List.fold_left map ([], 0) vs in
 120    let b = Array.of_list (List.rev l) in
 121    let mk_closure b h =
 122       let map j = S.union (fst b.(j)) in
 123       for i = pred h downto 0 do
 124          let direct, unused = b.(i) in
 125          b.(i) <- S.fold map direct direct, unused
 126       done; b
 127    in
 128    let b = mk_closure b h in
 129    let rec mk_inverse i direct =
 130       if S.is_empty direct then () else
 131       let j = S.choose direct in
 132       let unused, inverse = b.(j) in
 133       b.(j) <- unused, S.add i inverse;
 134       mk_inverse i (S.remove j direct)
 135    in
 136    let map i (direct, _) = mk_inverse i direct in
 137    Array.iteri map b;
 138    out_table b;
 139    List.rev_map snd (List.tl (Array.to_list b)), rc
 140
 141 let aclassify t = classify (D.deannotate_term t)
 142
 143 let overlaps s1 s2 =
 144    let predicate x = S.mem x s1 in
 145    S.exists predicate s2