Source file LLProof_conv.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
161
162
163
164
165
166
167
168
169
170
171
172
173
174

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

open Logtk

module T = TypedSTerm

type ll_subst = (T.t,T.t) Var.Subst.t

let section = LLProof.section
let errorf msg = Util.errorf ~where:"llproof_conv" msg

let conv_subst ~ctx (p:Subst.Projection.t) : ll_subst =
  List.fold_left
    (fun lsubst (v,t) ->
       let v = Type.cast_var_unsafe v in
       let prefix = if Type.is_tType (HVar.ty v) then "A" else "X" in
       let v = Term.Conv.var_to_simple_var ~prefix ctx v in
       let t = Term.Conv.to_simple_term ctx (Term.of_term_unsafe t) in
       assert (not (Var.Subst.mem lsubst v));
       Var.Subst.add lsubst v t)
    Var.Subst.empty
    (Subst.Projection.bindings p)

type state = {
  ctx: Term.Conv.ctx;
  tbl: LLProof.t Proof.S.Tbl.t;
}

let open_forall = T.unfold_binder Binder.Forall

let rec conv_proof st p: LLProof.t =
  begin match Proof.S.Tbl.get st.tbl p with
    | Some r -> r
    | None ->
      let res = conv_step st p in
      Proof.S.Tbl.add st.tbl p res;
      res
  end

and conv_step st p =
  Util.debugf ~section 5 "(@[llproof.conv.step@ %a@])"
    (fun k->k Proof.S.pp_notrec1 p);
  let res = Proof.Result.to_form ~ctx:st.ctx (Proof.S.result p) in
  let vars, _ = open_forall res in
  (* introduce local symbols for making proof checking locally ground.
     Some variables are typed using other variables, so we
     need to substitute eagerly *)
  let intros =
    let l =
      List.mapi (fun i v -> v, T.const ~ty:(Var.ty v) (ID.makef "sk_%d" i)) vars
    in
    let subst = Var.Subst.of_list l in
    List.map (fun (_,c) -> T.Subst.eval subst c) l
  in
  (* convert result *)
  let res = match Proof.Step.kind @@ Proof.S.step p with
    | Proof.Inference (rule,tags)
    | Proof.Simplification (rule,tags) ->
      let local_intros = ref Var.Subst.empty in
      let parents =
        List.map (conv_parent st res intros local_intros tags)
          (Proof.Step.parents @@ Proof.S.step p)
      in
      let local_intros = Var.Subst.to_list !local_intros |> List.rev_map snd in
      LLProof.inference ~intros ~local_intros ~tags
        (T.rename_all_vars res) (Proof.Rule.name rule) parents
    | Proof.Esa rule ->
      let l =
        List.map
          (function
            | Proof.P_of p -> conv_proof st p
            | Proof.P_subst _ -> assert false)
          (Proof.Step.parents @@ Proof.S.step p)
      in
      LLProof.esa (T.rename_all_vars res) (Proof.Rule.name rule) l
    | Proof.Trivial -> LLProof.trivial res
    | Proof.By_def id -> LLProof.by_def id res
    | Proof.Define (id,_) -> LLProof.define id res
    | Proof.Intro (_,Proof.R_assert) -> LLProof.assert_ res
    | Proof.Intro (_,(Proof.R_goal|Proof.R_lemma)) -> LLProof.goal res
    | Proof.Intro (_,(Proof.R_def|Proof.R_decl)) ->
      LLProof.trivial res
  in
  Util.debugf ~section 4 "(@[llproof.conv.step.->@ :from %a@ :to %a@])"
    (fun k->k Proof.S.pp_notrec1 p LLProof.pp res);
  res

(* convert parent of the given result formula. Also make instantiations
   explicit. *)
and conv_parent
    st step_res intros local_intros tags
    (parent:Proof.Parent.t) : LLProof.parent =
  Util.debugf ~section 5 "(@[llproof.conv_parent@ %a@])"
    (fun k->k Proof.pp_parent parent);
  (* rename variables of result of inference *)
  let vars_step_res, _ = open_forall step_res in
  if List.length intros <> List.length vars_step_res then (
    errorf "length mismatch, cannot do intros@ :res %a@ :with [@[%a@]]"
      T.pp step_res (Util.pp_list ~sep:"," T.pp) intros
  );
  let intro_subst =
    Var.Subst.of_list (List.combine vars_step_res intros)
  in
  (* build an instantiation step, if needed *)
  let prev_proof, p_instantiated_res = match parent with
    | Proof.P_of p ->
      let p_res = Proof.Result.to_form ~ctx:st.ctx (Proof.S.result p) in
      let p = conv_proof st p in
      p, p_res
    | Proof.P_subst (p,subst) ->
      (* perform instantiation *)
      assert (not (Subst.Projection.is_empty subst));
      (* instantiated result of [p] *)
      let p_instantiated_res, inst_subst =
        Proof.Result.to_form_subst ~ctx:st.ctx subst (Proof.S.result p)
      in
      let p_res = Proof.Result.to_form ~ctx:st.ctx (Proof.S.result p) in
      (* convert [p] itself *)
      let p = conv_proof st p in
      (* find instantiation for [p] by looking at variables of [p_res] *)
      let inst : LLProof.inst =
        let vars_p, _ = open_forall p_res in
        List.map
          (fun v ->
             begin match Var.Subst.find inst_subst v with
               | Some t -> t
               | None ->
                 errorf "cannot find variable `%a`@ \
                         in inst-subst {%a}@ :inst-res %a@ :res %a@ \
                         :parent %a@ :intros [@[%a@]]"
                   Var.pp_fullc v (Var.Subst.pp T.pp) inst_subst
                   T.pp p_instantiated_res T.pp step_res Proof.pp_parent parent
                   (Util.pp_list ~sep:"," T.pp) intros
             end)
          vars_p
      in
      LLProof.instantiate ~tags p_instantiated_res p inst, p_instantiated_res
  in
  (* now open foralls in [p_instantiated_res]
     and find which variable of [intros] they rename into *)
  let inst_intros : LLProof.inst =
    let vars_instantiated, _ = T.unfold_binder Binder.forall p_instantiated_res in
    List.map
      (fun v ->
         begin match Var.Subst.find intro_subst v with
           | Some t -> t
           | None ->
             begin match Var.Subst.find !local_intros v with
               | Some t -> t
               | None ->
                 (* introduce local_intro *)
                 let c =
                   ID.makef "sk_%d"
                     (List.length intros + Var.Subst.size !local_intros)
                   |> T.const ~ty:(Var.ty v |> T.Subst.eval intro_subst)
                 in
                 local_intros := Var.Subst.add !local_intros v c;
                 Util.debugf ~section 5
                   "(@[llproof.conv.add_local_intro@ %a := %a@ :p-instantiated `%a`@])"
                   (fun k->k Var.pp_fullc v T.pp c T.pp p_instantiated_res);
                 c
             end
         end)
      vars_instantiated
  in
  LLProof.p_inst prev_proof inst_intros

let conv (p:Proof.t) : LLProof.t =
  let st = {
    ctx = Term.Conv.create();
    tbl = Proof.S.Tbl.create 32;
  } in
  conv_proof st p