Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit 48b0fa2e authored by Sylvain Dailler's avatar Sylvain Dailler

Changing renaming of ident with printer.

Ident closer to the goal have lower disambiguation numbers.
We do that by first puting all declarations in a list and then iter on
it.
Also removing useless comments in test_argument and args_wrapper.
parent f55bbb8c
......@@ -133,43 +133,20 @@ let add (d: decl) (tables: name_tables): name_tables =
let build_name_tables task : name_tables =
(*
TODO:
- simply use [km = Task.task_known task] as the set of identifiers
to insert in the tables
- only one printer (do not attempt te rebuild qualified idents)
- use syntax_map from why3_itp driver
- to build the namespace, do a match on the decl associated with the id
in [km]
| Dtype -> tysymbol
| Ddata | Dparam | Dlogic | Dind -> lsymbol
| Dprop -> prsymbol
TODO: use the result of this function in
- a new variant of a printer in this file
- use the namespace to type the terms
(change the code in parser/typing.ml to use namespace
instead of theory_uc)
*)
let pr = fresh_printer () in
let km = Task.task_known task in
let tables = {
namespace = empty_ns;
known_map = km;
(*
unique_names = Mid.empty ;
*)
printer = pr;
} in
Mid.fold
(fun _id d tables ->
(* TODO optimization. We may check if id is already there to not explore twice the same
declaration ? *)
add d tables)
km
tables
(* We want conflicting names to be named as follows:
names closer to the goal should be named with lowest
disambiguation numbers.
This only works for things defined in .why/.mlw because things
added by the user are renamed on the fly. *)
let l = Mid.fold (fun _id d acc -> d :: acc) km [] in
List.fold_left (fun tables d -> add d tables) tables l
(************* wrapper *************)
......
......@@ -2,57 +2,9 @@
theory Test
use import int.Int
goal G: forall x "name:TOTO". forall y. x = y -> x = 2 * y
constant x "name:TOTO": int
(*
ng
b introduce_premises
>> print goal with premisses introduced
b cut "exists x: int. x = x"
>> print goal with h in context
b exists "5"
>> print new goal G1 with (x = (2 * 5))
p
>> print the proof tree with ** where we are
b case "exists x. exists y. x + y = y - x"
>> print the goal with the hypothesis in context
ng
g
>> print the goal with the contrary hypothesis
pg
>> return to context with positive exists
g
>> print it
b cut "exists x. exists y. x + y = 0"
ng
g
>> Have to prove h2 with 2 exists
b exists "4"
>> Instantiate x1
b cut "forall x. forall y. x + y = 0"
>> print with h2 in context
b instantiate "h2" "4"
>> create h21 which is correct
b exists "3"
>> instantiate y in the goal
b cut "forall y. true -> 4 + y = 0"
>> generate h3
b apply h3
>> apply h3 to the goal and generate the new goal
gu
g
>> go back to the 4 + 3 = 0 goal
b cut "forall y. y = 5 -> 4 + y = 0"
>> new hypothesis to apply
b apply h4
>> apply hypothesis and generate the goal 3 = 5 which is correct.
b remove h21
>> remove correct hypothesis h21
b remove x
>> Silently fails probably because not an axiom. Do we want to remove constant ? TODO
b remove CompatOrderMult
>> Success
goal G: forall x "name:TOTO". forall y. x = y -> x = 2 * y
*)
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment