package libzipperposition

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

Source file clauseContext.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

(* This file is free software, part of Zipperposition. See file "license" for more details. *)

(** {1 Clause context}

    A clause with a "hole" in it. Filling the whole with a term [t] is called
    "applying the context to [t]".

    The point is to relate different applications of the same context. *)

open Logtk

module T = Term
module Lits = Literals

type term = T.t
type subst = Subst.t

(** A context is represented as a regular array of literals, containing
    at least one specific variable [x], paired with this variable [x].
    Applying the context is a mere substitution *)
type t = {
  lits : Literals.t;
  var : T.var;
  mutable hash: int;
}
type ctx=t

let equal c1 c2 = HVar.equal Type.equal c1.var c2.var && Lits.equal c1.lits c2.lits

let raw_lits t = t.lits

(* TODO: compare types of extruded variables;
   if same type, instantiate with some specific "diamond" of that type
   and check for alpha-equiv *)
let compare c1 c2 =
  CCOrd.(HVar.compare Type.compare c1.var c2.var <?> (Lits.compare, c1.lits, c2.lits))

let hash_real c = Hash.combine3 42 (Literals.hash c.lits) (HVar.hash c.var)

let hash c =
  if c.hash = ~-1 then (
    let h = hash_real c in
    assert (h >= 0);
    c.hash <- h
  );
  c.hash

let make_ lits var =
  {lits; var; hash= ~-1}

let make lits ~var =
  assert (Lits.Seq.terms lits
          |> Iter.exists (T.var_occurs ~var));
  make_ lits var

let extract lits t =
  if Lits.Seq.terms lits |> Iter.exists (T.subterm ~sub:t)
  then
    (* create fresh var to replace [t], negative to avoid collisions later *)
    let var = HVar.make_unsafe ~ty:(T.ty t) ~-2 in
    let var_t = T.var var in
    (* replace [t] with [var] *)
    let lits =
      Array.map
        (Literal.map (fun root_t -> T.replace root_t ~old:t ~by:var_t))
        lits
    in
    Some (make_ lits var)
  else None

let extract_exn lits t = match extract lits t with
  | None -> invalid_arg "ClauseContext.extract_exn"
  | Some c -> c

let trivial lits t =
  (* create fresh var to replace [t], negative to avoid collisions later *)
  let var = HVar.make_unsafe ~ty:(T.ty t) ~-2 in
  assert (not (Literals.Seq.terms lits |> Iter.exists (T.subterm ~sub:t)));
  make_ lits var

let _apply_subst subst (lits, sc) =
  let renaming = Subst.Renaming.create () in
  Array.map (fun lit -> Literal.apply_subst renaming subst (lit, sc)) lits

let apply {lits; var; _} t =
  let var = (var : T.var :> InnerTerm.t HVar.t) in
  let subst = Subst.FO.bind Subst.empty (var, 0) (t, 1) in
  _apply_subst subst (lits, 0)

let apply_same_scope {lits; var; _} t =
  let var = (var : T.var :> InnerTerm.t HVar.t) in
  let subst = Subst.FO.bind Subst.empty (var, 0) (t, 0) in
  _apply_subst subst (lits, 0)

let _diamond = ID.make "◇"

let pp out c =
  let cst = T.const ~ty:(HVar.ty c.var) _diamond in
  let lits = apply_same_scope c cst in
  Format.fprintf out "[@[%a@]]" Lits.pp lits

module Set = CCSet.Make(struct
    type t = ctx
    let compare = compare
  end)
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