engine/univops.ml

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Univ
open Constr

let universes_of_constr c =
  let rec aux s c = 
    match kind c with
    | Const (_, u) | Ind (_, u) | Construct (_, u) ->
      LSet.fold LSet.add (Instance.levels u) s
    | Sort u when not (Sorts.is_small u) -> 
      let u = Sorts.univ_of_sort u in
      LSet.fold LSet.add (Universe.levels u) s
    | _ -> Constr.fold aux s c
  in aux LSet.empty c

type graphnode = {
  mutable up : constraint_type LMap.t;
  mutable visited : bool
}

let merge_types d d0 =
  match d, d0 with
  | _, Lt | Lt, _ -> Lt
  | Le, _ | _, Le -> Le
  | Eq, Eq -> Eq

let merge_up d b up =
  let find = try Some (LMap.find b up) with Not_found -> None in
  match find with
  | Some d0 ->
    let d = merge_types d d0 in
    if d == d0 then up else LMap.add b d up
  | None -> LMap.add b d up

let add_up a d b graph =
  let node, graph =
    try LMap.find a graph, graph
    with Not_found ->
      let node = { up = LMap.empty; visited = false } in
      node, LMap.add a node graph
  in
  node.up <- merge_up d b node.up;
  graph

(* for each node transitive close until you find a non removable, discard the rest *)
let transitive_close removable graph =
  let rec do_node a node =
    if not node.visited
    then
      let keepup =
        LMap.fold (fun b d keepup ->
            if not (LSet.mem b removable)
            then merge_up d b keepup
            else
              begin
                match LMap.find b graph with
                | bnode ->
                  do_node b bnode;
                  LMap.fold (fun k d' keepup ->
                    merge_up (merge_types d d') k keepup)
                    bnode.up keepup
                | exception Not_found -> keepup
              end
          )
          node.up LMap.empty
      in
      node.up <- keepup;
      node.visited <- true
  in
  LMap.iter do_node graph

let restrict_universe_context (univs,csts) keep =
  let removable = LSet.diff univs keep in
  let (csts, rem) =
    Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
        if LSet.mem a removable || LSet.mem b removable
        then (csts, add_up a d b rem)
        else (Constraint.add cst csts, rem))
      csts (Constraint.empty, LMap.empty)
  in
  transitive_close removable rem;
  let csts =
    LMap.fold (fun a node csts ->
        if LSet.mem a removable
        then csts
        else
          LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
            node.up csts)
      rem csts
  in
  (LSet.inter univs keep, csts)