package libzipperposition

  1. Overview
  2. Docs
package libzipperposition
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file Ind_cst.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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160

(** {1 Inductive Constants and Cases}

    Skolem constants of an inductive type, coversets, etc. required for
    inductive reasoning. *)

open Logtk

module T = Term

exception InvalidDecl of string
exception NotAnInductiveConstant of ID.t

let () =
  let spf = CCFormat.sprintf in
  Printexc.register_printer
    (function
      | InvalidDecl msg ->
        Some (spf "@[<2>invalid declaration:@ %s@]" msg)
      | NotAnInductiveConstant id ->
        Some (spf "%a is not an inductive constant" ID.pp id)
      | _ -> None)

let invalid_decl m = raise (InvalidDecl m)
let invalid_declf m = CCFormat.ksprintf m ~f:invalid_decl

type t = {
  cst_id: ID.t;
  cst_args: Type.t list;
  cst_ty: Type.t; (* [cst_ty = cst_id cst_args] *)
  cst_ity: Ind_ty.t; (* the corresponding inductive type *)
  cst_is_sub: bool; (* sub-constant? *)
  cst_depth: int; (* how many induction lead to this one? *)
}

exception Payload_cst of t

(** {6 Inductive Constants} *)

let to_term c = Term.const ~ty:c.cst_ty c.cst_id
let id c = c.cst_id
let ty c = c.cst_ty

let equal a b = ID.equal a.cst_id b.cst_id
let compare a b = ID.compare a.cst_id b.cst_id
let hash a = ID.hash a.cst_id

module Cst_set = CCSet.Make(struct
    type t_ = t
    type t = t_
    let compare = compare
  end)

let depth c = c.cst_depth

let same_type c1 c2 = Type.equal c1.cst_ty c2.cst_ty

let pp out c = ID.pp out c.cst_id

let on_new_cst = Signal.create()

let id_as_cst id =
  ID.payload_find id
    ~f:(function
        | Payload_cst c -> Some c
        | _ -> None)

let id_as_cst_exn id = match id_as_cst id with
  | None -> raise (NotAnInductiveConstant id)
  | Some c -> c

let id_is_cst id = match id_as_cst id with Some _ -> true | _ -> false

let is_sub c = c.cst_is_sub

let id_is_sub id = id_as_cst id |> CCOpt.map_or ~default:false is_sub

(** {6 Creation of Coverset and Cst} *)

let n_ = ref 0

let make_skolem ty : ID.t =
  let c = ID.makef "#%s_%d" (Type.mangle ty) !n_ in
  incr n_;
  (* declare as a skolem *)
  let k = if Ind_ty.is_inductive_type ty then ID.K_ind else ID.K_normal in
  ID.set_payload c (ID.Attr_skolem k);
  c

(* declare new constant *)
let declare ~depth ~is_sub id ty =
  Util.debugf ~section:Ind_ty.section 2
    "@[<2>declare new inductive symbol@ `@[%a : %a@]`@ :depth %d :is_sub %B@]"
    (fun k->k ID.pp id Type.pp ty depth is_sub);
  assert (not (id_is_cst id));
  assert (Type.is_ground ty); (* constant --> not polymorphic *)
  let ity, args = match Ind_ty.as_inductive_type ty with
    | Some (t,l) -> t,l
    | None -> invalid_declf "cannot declare a constant of type %a" Type.pp ty
  in
  (* build coverset and constant, mutually recursive *)
  let cst = {
    cst_id=id;
    cst_ty=ty;
    cst_depth=depth;
    cst_ity=ity;
    cst_args=args;
    cst_is_sub=is_sub;
  }
  in
  ID.set_payload id (Payload_cst cst)
    ~can_erase:(function
        | ID.Attr_skolem ID.K_ind ->
          true (* special case: promotion from skolem to inductive const *)
        | _ -> false);
  (* return *)
  Signal.send on_new_cst cst;
  cst

let make ?(depth=0) ~is_sub (ty:Type.t): t =
  let id = make_skolem ty in
  declare ~depth ~is_sub id ty

let dominates (c1:t)(c2:t): bool =
  c1.cst_depth < c2.cst_depth

(** {2 Inductive Skolems} *)

type ind_skolem = ID.t * Type.t

let ind_skolem_compare = CCOrd.pair ID.compare Type.compare
let ind_skolem_equal a b = ind_skolem_compare a b = 0

let id_is_ind_skolem (id:ID.t) (ty:Type.t): bool =
  let n_tyvars, ty_args, ty_ret = Type.open_poly_fun ty in
  n_tyvars=0
  && ty_args=[] (* constant *)
  && Ind_ty.is_inductive_type ty_ret
  && Ind_ty.is_recursive (Ind_ty.as_inductive_type_exn ty_ret |> fst)
  && Type.is_ground ty
  && (id_is_cst id || (not (Ind_ty.is_constructor id) && not (Rewrite.is_defined_cst id)))

let ind_skolem_depth (id:ID.t): int = match id_as_cst id with
  | None -> 0
  | Some c -> depth c

(* find inductive constant candidates in terms *)
let find_ind_skolems t : ind_skolem Iter.t =
  T.Seq.subterms t
  |> Iter.filter_map
    (fun t -> match T.view t with
       | T.Const id ->
         let ty = T.ty t in
         if id_is_ind_skolem id ty
         then (
           let n_tyvars, ty_args, _ = Type.open_poly_fun ty in
           assert (n_tyvars=0 && ty_args=[]);
           Some (id, ty)
         ) else None
       | _ -> None)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct