WIP: Add opaque command

[NotBad4U]

This PR add a new command to declare a symbol as opaque after it has been defined. It also fixes the function is_injective so that opaque symbols are considered as injective since they can never be unfolded.

TODO

• [x] update is_injective
• [x] update CHANGES.md
• [x] update doc

---

I was able to modify sym_opaq without making a pointer to it (sym_opaq : bool ref).

@fblanqui , setting the sym_opaq at true seems to be not enough. In the test that I added OK/opaque.lp, when I call the tactic simplify; in ∨ᶜᵢ₁' the symbol πᶜ is correctly Not unfold, but when I do apply ∨ᶜᵢ₁ (for testing purpose), it crashed with this error:

[/Users/alessiocoltellacci/Junk/lambdapi/tests/OK/opaque.lp:46:4-14] Missing subproofs (0 subproofs for 5 subgoals):
p: Prop
q: Prop
Hp: πᶜ p

--------------------------------------------------------------------------------
0. πᶜ (p ∨ᶜ q) ≡ π ⊥
1. ?10: Prop
2. ?11: Prop
3. ?12: πᶜ ?10.[p;q;Hp]
4. ?13: π (¬ (?10.[p;q;Hp] ∨ᶜ ?11.[p;q;Hp]))

I am mostly surprised by the two subgoals

• 0. πᶜ (p ∨ᶜ q) ≡ π ⊥
• 4. ?13: π (¬ (?10.[p;q;Hp] ∨ᶜ ?11.[p;q;Hp])) It keeps using the definition of the symbol made opaque. I tried to set sym_def at None when the opaque command is used but I got the same error. Any idea where I can have a look?

[fblanqui]

The absence of definition at a given moment is not sufficient to consider a symbol as injective: rules can be added later. You need to update the function is_injective as well: opaque symbols should be considered as constants and thus injective.

[NotBad4U]

The absence of definition at a given moment is not sufficient to consider a symbol as injective: rules can be added later. You need to update the function is_injective as well: opaque symbols should be considered as constants and thus injective.

It seems to not be enough because I have the same behavior.

p: Prop
q: Prop
Hp: πᶜ p
--------------------------------------------------------------------------------
0. πᶜ (p ∨ᶜ q) ≡ π ⊥
1. ?10: Prop
2. ?11: Prop
3. ?12: πᶜ ?10.[p;q;Hp]
4. ?13: π (¬ (?10.[p;q;Hp] ∨ᶜ ?11.[p;q;Hp]))

[fblanqui]

Other problems to fix:

File "src/parsing/pretty.ml", lines 310-344, characters 2-5:
310 | ..begin match elt with
311 |   | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid
312 |   | P_inductive (_, _, []) -> assert false (* not possible *)
313 |   | P_inductive (ms, xs, i :: il) ->
314 |     let with_ind ppf i = out ppf "@,%a" (inductive "with") i in
...
341 |     end
342 |   | P_unif_rule ur -> out ppf "unif_rule %a" unif_rule ur
343 |   | P_coercion c -> out ppf "%a" (rule "coerce_rule") c
344 |   end.
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
P_opaque _
File "src/parsing/pretty.ml", lines 310-344, characters 2-5:
310 | ..begin match elt with
311 |   | P_builtin (s, qid) -> out ppf "@[builtin \"%s\"@ ≔ %a@]" s qident qid
312 |   | P_inductive (_, _, []) -> assert false (* not possible *)
313 |   | P_inductive (ms, xs, i :: il) ->
314 |     let with_ind ppf i = out ppf "@,%a" (inductive "with") i in
...
341 |     end
342 |   | P_unif_rule ur -> out ppf "unif_rule %a" unif_rule ur
343 |   | P_coercion c -> out ppf "%a" (rule "coerce_rule") c
344 |   end.
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
P_opaque _
Warning: one state has shift/reduce conflicts.
Warning: 2 shift/reduce conflicts were arbitrarily resolved.

[fblanqui]

There is something wrong in your code. The type of the field sym_opaq of the record type sym must be changed to bool ref.

[NotBad4U]

The test passed now by changing the type of sym_opaq to bool ref! However, I am not sure to understand what is the necessity to have a pointer to make it work. I updated the doc, but it is you who will update CHANGES.md right?

[fblanqui]

No, please update CHANGES.md yourself. Why a ref is need, this is because sym's are shared: there is only one sym in memory for a given symbol.

[fblanqui]

CI currently fails because of a setup-ocaml failure.

[fblanqui]

Thanks Alessio. I propose you a few cosmetic changes before merging.

[NotBad4U]

If you agree with my last modification, then I think we can merge this PR.

[fblanqui]

Thanks Alessio!