mo_types/productive.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

open Type

(*
  Maintain a map from con to info = {Nonproductive, Productive, Param n}`.
  After the analysis, this map says, for all type constructors, whether they are  really unproductive, productive, or if their unfolding is equal to one of their parameters.
* Maintain a set of type definitions under scrutiny
* For each type definition:
  * If it is already in the memo map, use that result. Else analyze it as follows, updating the memo map afterwards.
  * If it is already in the set, we have found a loop. Mark it as `unproductive`. Else add to the setduring the next step.
  * Consider its RHS:
    * If it is a concrete type, return `Productive`.
    * If it is the nth type parameter, return `Param n`
    * If it is a type application `T<t1,…,tn>`, recurse.
      * If recursion returns `Productive` or `Nonproductive`, return that.
      * If recursion returns `Param n`, loop to “Consider its RHS”, as if `tn`
        is the RHS.
*)

type info =
  | Nonproductive
  | Productive
  | Param of int

let non_productive cs =
  let map = ref ConEnv.empty in
  let rec rhs cs = function
    | Pre
    | Mut _ | Typ _ ->
      assert false (* body of a Def shouldn't be 2nd class *)
    | Var (s, j) ->
      Param j
    | Con (d, ts) ->
      begin
        visit_con cs d;
        match ConEnv.find d (!map) with
        | Param n ->
          begin
          match Cons.kind d with
          | Def (tbs, t) ->
            assert (n < List.length tbs); (* assume types are arity-correct *)
            rhs cs (List.nth ts n)
          | Abs (tbs, t) ->
            (* we could assert here since Defs should be closed *)
            Productive
          end
        | info -> info
      end
    | _ ->  (* anything else is productive *)
      Productive

  and visit_con cs c =
    match ConEnv.find_opt c (!map) with
    | Some info -> ()
    | None ->
      let info =
        if ConSet.mem c cs then
          Nonproductive
        else
          let t = match Cons.kind c with
            | Def (_, t) -> t
            | _ -> assert false
          in
          rhs (ConSet.add c cs) t
      in
      map := ConEnv.add c info !map
  in
  ConSet.iter (visit_con ConSet.empty) cs;
  ConSet.filter (fun c -> ConEnv.find c !map = Nonproductive) cs