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 c47db2e2 authored by Sylvain Dailler's avatar Sylvain Dailler

Adding transformation apply. Probably not the one we want.

Only works with hypothesis of the form forall x. A -> B.
Also cleaning the code a little.
parent 0f771e2b
......@@ -75,6 +75,7 @@ let string_pr pr =
Pretty.print_pr Format.str_formatter pr;
Format.flush_str_formatter()
(* Return a new task with hypothesis name removed *)
let rec remove_task_decl task (name: string) : task_hd option =
match task with
| Some {task_decl = {td_node = Decl {d_node = Dprop (Paxiom, pr, _)}};
......@@ -107,6 +108,15 @@ let pr_prsymbol pr =
| Decl {d_node = Dprop (_pk, pr, _t)} -> Some pr
| _ -> None
(* Looks for the hypothesis name and return it. If not found return None *)
let find_hypothesis name task =
let ndecl = ref None in
let _ = task_iter (fun x -> if (
match (pr_prsymbol x.td_node) with
| None -> false
| Some pr -> string_pr pr = name) then ndecl := Some x) task in
!ndecl
(* from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let simple_apply name t task =
......@@ -114,12 +124,8 @@ let simple_apply name t task =
let _ = Pretty.print_task Format.str_formatter task in
let _ = ignore (Format.flush_str_formatter ()) in
let g, task = Task.task_separate_goal task in
let ndecl = ref None in
let _ = task_iter (fun x -> if (
match (pr_prsymbol x.td_node) with
| None -> false
| Some pr -> string_pr pr = name) then ndecl := Some x) task in
match !ndecl with
let ndecl = find_hypothesis name task in
match ndecl with
| None -> Format.printf "Hypothesis %s not found@." name; [Task.add_tdecl task g]
| Some decl -> (match decl.td_node with
| Decl {d_node = Dprop (pk, _pr, ht)} ->
......@@ -130,10 +136,97 @@ let simple_apply name t task =
[Task.add_tdecl task g]
| _ -> Format.printf "Not an hypothesis@."; [Task.add_tdecl task g])
let apply _name task = (* ? *)
[task;task]
(* TODO : from task [delta, name:forall x.A->B |- G,
build the task [delta,name:forall x.A->B] |- A[x -> t]] ou t est tel que B[x->t] = G *)
(* TODO find correct librrary *)
let choose_option a b =
match a, b with
| Some x, _ -> Some x
| None, Some x -> Some x
| None, None -> None
(* TODO stupid This function return the term we need to use in place of
the variable so that the 2 terms can be equal.
This function is NOT used to check that the 2 terms are equal as we want
library function from Term to do that.
TODO cases are probably forgotten. To be completed *)
let rec is_unify t x v =
match t.t_node, x.t_node with
| Tvar v', _ when v == v' -> Some x
| Tapp(ls, tl), Tapp(ls', tl') when ls == ls' ->
is_unify_list tl tl' v
| Tif (f, t, e), Tif(f', t', e') ->
is_unify_list [f;t;e] [f';t';e'] v
| Tlet (t, tb), Tlet (t', tb') ->
let (_v', e) = t_open_bound tb in
let (_v'', e') = t_open_bound tb' in
is_unify_list [t; e] [t'; e'] v
| Tcase (t, bl), Tcase (t', bl') ->
choose_option
(List.fold_left2 (fun acc b b' ->
let (_, t1) = t_open_branch b in
let (_, t2) = t_open_branch b' in
choose_option acc (is_unify t1 t2 v)) None bl bl')
(is_unify t t' v)
| Teps tb, Teps tb' ->
let (_v', e) = t_open_bound tb in
let (_v'', e') = t_open_bound tb' in
is_unify e e' v
| Tquant (_q, tq), Tquant (_q', tq') ->
let (_vl, _tr, t) = t_open_quant tq in
let (_vl', _tr', t') = t_open_quant tq' in
is_unify t t' v
| Tbinop (_b, t1, t2), Tbinop (_b', t1', t2') ->
is_unify_list [t1;t2] [t1';t2'] v
| Tnot t, Tnot t' ->
is_unify t t' v
| _, _ -> None
and is_unify_list tl xl v =
List.fold_left2 (fun acc t1 t2 ->
choose_option acc (is_unify t1 t2 v)) None tl xl
let term_decl d =
match d.td_node with
| Decl ({d_node = Dprop (_pk, _pr, t)}) -> t
| _ -> failwith "Not a correct prop"
(* from task [delta, name:forall x.A->B |- G,
build the task [delta,name:forall x.A->B] |- A[x -> t]] ou t est tel que B[x->t] = G *)
let apply name task =
(* Force setting of pprinter *)
let _ = Pretty.print_task Format.str_formatter task in
let _ = ignore (Format.flush_str_formatter ()) in
let g, task = Task.task_separate_goal task in
let tg = term_decl g in
let d = find_hypothesis name task in
if d = None then failwith "Hypothesis not found" else
let d = Opt.get d in
let t = term_decl d in
match t.t_node with
| Tquant (Tforall, tb) ->
let (vl, tr, t) = t_open_quant tb in
let v = List.hd vl in
begin
match t.t_node with
| Tbinop (Timplies, ta, tb) ->
let candidate_unifier = is_unify tb tg v in
begin
match candidate_unifier with
| None -> failwith "Unable to unify the hypothesis with the goal"
| Some x ->
let new_goal = t_forall_close (List.tl vl) tr (t_subst_single v x ta) in
let new_tb = t_subst_single v x tb in
(* TODO t_equal is probably too strong *)
if (Term.t_equal new_tb tg) then
[Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (Ident.id_fresh "G")) new_goal)]
else
(Format.printf "Term substituted was %a. Should be goal was %a. Goal was %a @." Pretty.print_term x Pretty.print_term new_tb Pretty.print_term tg;
failwith "After substitution, terms are not exactly identical")
end
| _ -> failwith "Not of the form forall immediately followed by implies"
end
| Tbinop (Timplies, _ta, _tb) -> failwith "Not implemented yet" (* TODO to be done later *)
| _ -> failwith "Not of the form forall x. A -> B"
let case' args task =
match args with
......@@ -160,9 +253,15 @@ let simple_apply' args task =
| [TAstring name; TAterm t] -> simple_apply name t task
| _ -> failwith "wrong arguments of simple_apply"
let apply' args task =
match args with
| [TAstring name] -> apply name task
| _ -> failwith "wrong arguments of simple_apply"
let () = register_transform_with_args ~desc:"test case" "case" case'
let () = register_transform_with_args ~desc:"test cut" "cut" cut'
let () = register_transform_with_args ~desc:"test exists" "exists" exists'
let () = register_transform_with_args ~desc:"test remove" "remove" remove'
let () = register_transform_with_args ~desc:"test simple_apply" "simple_apply" simple_apply'
let () = register_transform_with_args ~desc:"test apply" "apply" apply'
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" duplicate
......@@ -479,6 +479,17 @@ let test_simple_apply fmt args =
end
| _ -> let _ = printf "term argument expected@." in ()
let test_apply_with_string_args fmt args =
match (parse_transformation_string args) with
| None -> ()
| Some s ->
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "apply" [Trans.TAstring s] ~callback
let test_remove_with_string_args fmt args =
match (parse_transformation_string args) with
| None -> ()
......@@ -561,6 +572,7 @@ let commands =
"g", "prints the first goal", test_print_goal;
"r", "reload the session (test only)", test_reload;
"rem", "test remove transformation. Take one string argument", test_remove_with_string_args;
"app", "test apply transformation. Take one string argument", test_apply_with_string_args;
"s", "[s my_session] save the current session in my_session.xml", test_save_session;
"tr", "test schedule_transformation with split_goal on the current or next right goal (or on the top goal if there is none", test_transformation;
"ttr", "takes 2 arguments. Name of the transformation (with one term argument) and a term" , test_transformation_one_arg_term;
......
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