helm/software/components/acic_procedural/proceduralClassify.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 R = CicReduction
  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 id x = x
  61
  62 let rec list_fold_left g map = function
  63   | []       -> g
  64   | hd :: tl -> map (list_fold_left g map tl) hd
  65
  66 let get_rels h t =
  67    let rec aux d g = function
  68       | C.Sort _
  69       | C.Implicit _       -> g
  70       | C.Rel i            ->
  71          if i < d then g else fun a -> g (S.add (i - d + h + 1) a)
  72       | C.Appl ss          -> list_fold_left g (aux d) ss
  73       | C.Const (_, ss)
  74       | C.MutInd (_, _, ss)
  75       | C.MutConstruct (_, _, _, ss)
  76       | C.Var (_, ss)      ->
  77          let map g (_, t) = aux d g t in
  78          list_fold_left g map ss
  79       | C.Meta (_, ss)     ->
  80          let map g = function
  81             | None   -> g
  82             | Some t -> aux d g t
  83          in
  84          list_fold_left g map ss
  85       | C.Cast (t1, t2)    -> aux d (aux d g t2) t1
  86       | C.LetIn (_, t1, t2)
  87       | C.Lambda (_, t1, t2)
  88       | C.Prod (_, t1, t2) -> aux d (aux (succ d) g t2) t1
  89       | C.MutCase (_, _, t1, t2, ss) ->
  90          aux d (aux d (list_fold_left g (aux d) ss) t2) t1
  91       | C.Fix (_, ss) ->
  92          let k = List.length ss in
  93          let map g (_, _, t1, t2) = aux d (aux (d + k) g t2) t1 in
  94          list_fold_left g map ss
  95       | C.CoFix (_, ss) ->
  96          let k = List.length ss in
  97          let map g (_, t1, t2) = aux d (aux (d + k) g t2) t1 in
  98          list_fold_left g map ss
  99    in
 100    let g a = a in
 101    aux 1 g t S.empty
 102
 103 let split c t =
 104    let add s v c = Some (s, C.Decl v) :: c in
 105    let rec aux whd a n c = function
 106       | C.Prod (s, v, t)  -> aux false (v :: a) (succ n) (add s v c) t
 107       | v when whd        -> v :: a, n
 108       | v                 -> aux true a n c (R.whd ~delta:true c v)
 109     in
 110     aux false [] 0 c t
 111
 112 let classify_conclusion = function
 113    | C.Rel i                -> Some (i, 0)
 114    | C.Appl (C.Rel i :: tl) -> Some (i, List.length tl)
 115    | _                      -> None
 116
 117 let classify c t =
 118 try
 119    let vs, h = split c t in
 120    let rc = classify_conclusion (List.hd vs) in
 121    let map (b, h) v = (get_rels h v, S.empty) :: b, succ h in
 122    let l, h = List.fold_left map ([], 0) vs in
 123    let b = Array.of_list (List.rev l) in
 124    let mk_closure b h =
 125       let map j = if j < h then S.union (fst b.(j)) else id in
 126       for i = pred h downto 0 do
 127          let direct, unused = b.(i) in
 128          b.(i) <- S.fold map direct direct, unused
 129       done; b
 130    in
 131    let b = mk_closure b h in
 132    let rec mk_inverse i direct =
 133       if S.is_empty direct then () else
 134       let j = S.choose direct in
 135       if j < h then
 136          let unused, inverse = b.(j) in
 137          b.(j) <- unused, S.add i inverse
 138        else ();
 139        mk_inverse i (S.remove j direct)
 140    in
 141    let map i (direct, _) = mk_inverse i direct in
 142    Array.iteri map b;
 143 (*   out_table b; *)
 144    List.rev_map snd (List.tl (Array.to_list b)), rc
 145 with Invalid_argument _ -> failwith "Classify.classify"
 146
 147 let overlaps s1 s2 =
 148    let predicate x = S.mem x s1 in
 149    S.exists predicate s2