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

Remove can now remove a logic symbol or a type symbol

parent 98ad883b
......@@ -209,6 +209,11 @@ let build_name_tables task : names_table =
(************* wrapper *************)
type symbol =
| Ttysymbol of Ty.tysymbol
| Tprsymbol of Decl.prsymbol
| Tlsymbol of Term.lsymbol
type (_, _) trans_typ =
| Ttrans : ((task trans), task) trans_typ
| Ttrans_l : ((task tlist), task list) trans_typ
......@@ -216,10 +221,8 @@ type (_, _) trans_typ =
| Tenvtrans_l : (Env.env -> (task tlist), task list) trans_typ
| Tint : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
| Tty : ('a, 'b) trans_typ -> ((ty -> 'a), 'b) trans_typ
| Ttysymbol : ('a, 'b) trans_typ -> ((tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tprlist : ('a, 'b) trans_typ -> ((Decl.prsymbol list -> 'a), 'b) trans_typ
| Tlsymbol : ('a, 'b) trans_typ -> ((Term.lsymbol -> 'a), 'b) trans_typ
| Tsymbol : ('a, 'b) trans_typ -> ((symbol -> 'a), 'b) trans_typ
| Tlist : ('a, 'b) trans_typ -> ((symbol list -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
| Tstring : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
......@@ -230,9 +233,21 @@ type (_, _) trans_typ =
let find_pr s tables =
Mstr.find s tables.namespace.ns_pr
let find_ts s tables =
Mstr.find s tables.namespace.ns_ts
let find_ls s tables =
Mstr.find s tables.namespace.ns_ls
let find_symbol s tables =
try Tprsymbol (find_pr s tables) with
| Not_found ->
try Tlsymbol (find_ls s tables) with
| Not_found ->
try Ttysymbol (find_ts s tables) with
| Not_found -> raise (Arg_hyp_not_found s)
let type_ptree ~as_fmla t tables =
(*let tables = build_name_tables task in*)
let km = tables.known_map in
......@@ -277,10 +292,8 @@ let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
match t with
| Tint t -> t
| Tty t -> t
| Ttysymbol t -> t
| Tprsymbol t -> t
| Tprlist t -> t
| Tlsymbol t -> t
| Tsymbol t -> t
| Tlist t -> t
| Tterm t -> t
| Tstring t -> t
| Tformula t -> t
......@@ -297,10 +310,8 @@ let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
| Ttrans_l -> Yes
| Tint t -> is_trans_typ_l t
| Tty t -> is_trans_typ_l t
| Ttysymbol t -> is_trans_typ_l t
| Tprsymbol t -> is_trans_typ_l t
| Tprlist t -> is_trans_typ_l t
| Tlsymbol t -> is_trans_typ_l t
| Tsymbol t -> is_trans_typ_l t
| Tlist t -> is_trans_typ_l t
| Tterm t -> is_trans_typ_l t
| Tstring t -> is_trans_typ_l t
| Tformula t -> is_trans_typ_l t
......@@ -317,10 +328,8 @@ let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
| Tenvtrans_l -> "env transl"
| Tint _ -> "integer"
| Tty _ -> "type"
| Ttysymbol _ -> "type symbol"
| Tprsymbol _ -> "prop symbol"
| Tprlist _ -> "list of prop symbol"
| Tlsymbol _ -> "logic symbol"
| Tsymbol _ -> "symbol"
| Tlist _ -> "list of prop symbol"
| Tterm _ -> "term"
| Tstring _ -> "string"
| Tformula _ -> "formula"
......@@ -337,10 +346,8 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
| Tenvtrans_l -> "()"
| Tint t -> "integer -> " ^ print_type t
| Tty t -> "type -> " ^ print_type t
| Ttysymbol t -> "type_symbol -> " ^ print_type t
| Tprsymbol t -> "prop_symbol -> " ^ print_type t
| Tprlist t -> "prop_symbol list -> " ^ print_type t
| Tlsymbol t -> "logic_symbol -> " ^ print_type t
| Tsymbol t -> "symbol -> " ^ print_type t
| Tlist t -> "prop_symbol list -> " ^ print_type t
| Tterm t -> "term -> " ^ print_type t
| Tstring t -> "string -> " ^ print_type t
| Tformula t -> "formula -> " ^ print_type t
......@@ -366,25 +373,14 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Tty t', _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f ty) tail env tables task
| Ttysymbol t', _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f tys) tail env tables task
| Tprsymbol t', s :: tail ->
let pr = try (find_pr s tables) with
| Not_found -> raise (Arg_hyp_not_found s) in
wrap_to_store t' (f pr) tail env tables task
| Tprlist t', s :: tail ->
| Tsymbol t', s :: tail ->
let symbol = find_symbol s tables in
wrap_to_store t' (f symbol) tail env tables task
| Tlist t', s :: tail ->
let pr_list = parse_list_ident s in
let pr_list =
List.map (fun id ->
try find_pr id.Ptree.id_str tables with
| Not_found -> raise (Arg_hyp_not_found s))
pr_list in
List.map (fun id -> find_symbol id.Ptree.id_str tables) pr_list in
wrap_to_store t' (f pr_list) tail env tables task
| Tlsymbol t', s :: tail ->
let pr = try (find_ls s tables) with
| Not_found -> raise (Arg_hyp_not_found s) in
wrap_to_store t' (f pr) tail env tables task
| Ttheory t', s :: tail ->
let th = parse_theory env s in
wrap_to_store t' (f th) tail env tables task
......@@ -395,9 +391,8 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Tint t' ->
let arg = Some (parse_int s') in
wrap_to_store t' (f arg) tail env tables task
| Tprsymbol t' ->
let arg = try Some (find_pr s' tables) with
| Not_found -> raise (Arg_hyp_not_found s') in
| Tsymbol t' ->
let arg = Some (find_symbol s' tables) in
wrap_to_store t' (f arg) tail env tables task
| Tformula t' ->
let arg = Some (parse_and_type ~as_fmla:true s' tables) in
......
......@@ -13,23 +13,26 @@ exception Arg_hyp_not_found of string
val build_name_tables : Task.task -> Task.names_table
type symbol =
| Ttysymbol of Ty.tysymbol
| Tprsymbol of Decl.prsymbol
| Tlsymbol of Term.lsymbol
type (_, _) trans_typ =
| Ttrans : (task Trans.trans, task) trans_typ
| Ttrans_l : (task Trans.tlist, task list) trans_typ
| Ttrans : ((task Trans.trans), task) trans_typ
| Ttrans_l : ((task Trans.tlist), task list) trans_typ
| Tenvtrans : (Env.env -> (task Trans.trans), task) trans_typ
| Tenvtrans_l : (Env.env -> (task Trans.tlist), task list) trans_typ
| Tint : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
| Tty : ('a, 'b) trans_typ -> ((Ty.ty -> 'a), 'b) trans_typ
| Ttysymbol : ('a, 'b) trans_typ -> ((Ty.tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tprlist : ('a, 'b) trans_typ -> ((Decl.prsymbol list -> 'a), 'b) trans_typ
| Tlsymbol : ('a, 'b) trans_typ -> ((Term.lsymbol -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Tstring : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
| Tint : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
| Tty : ('a, 'b) trans_typ -> ((Ty.ty -> 'a), 'b) trans_typ
| Tsymbol : ('a, 'b) trans_typ -> ((symbol -> 'a), 'b) trans_typ
| Tlist : ('a, 'b) trans_typ -> ((symbol list -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Tstring : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
(** wrap arguments of transformations, turning string arguments into
arguments of proper types. arguments of type term of formula are
......
......@@ -107,9 +107,64 @@ let remove_list name_list =
Trans.decl
(fun d ->
match d.d_node with
| Dprop (Paxiom, pr, _) when
(List.exists (fun x -> Ident.id_equal pr.pr_name x.pr_name) name_list) ->
| Dprop (k, pr, _) when
(k != Pgoal &&
List.exists
(fun x -> match x with
| Tprsymbol x -> Ident.id_equal pr.pr_name x.pr_name
| _ -> false
)
name_list) ->
[]
| Dparam ls when
(List.exists
(fun x -> match x with
| Tlsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list) ->
[]
| Dlogic dl when
(* also remove all dependant recursive declarations (as expected) *)
List.exists
(fun (ls, _) -> List.exists
(fun x -> match x with
| Tlsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list)
dl ->
[]
| Dind il when
(* also remove all dependant inductive declarations (as expected) *)
List.exists
(fun (ls, _) -> List.exists
(fun x -> match x with
| Tlsymbol x -> Ident.id_equal ls.ls_name x.ls_name
| _ -> false
)
name_list)
(snd il) ->
[]
| Dtype ty when
(List.exists
(fun x -> match x with
| Ttysymbol x -> Ident.id_equal ty.ts_name x.ts_name
| _ -> false
)
name_list) ->
[]
| Ddata tyl when
(* also remove all dependant recursive declarations (as expected) *)
List.exists
(fun (ty, _) -> List.exists
(fun x -> match x with
| Ttysymbol x -> Ident.id_equal ty.ts_name x.ts_name
| _ -> false
)
name_list)
tyl ->
[]
| _ -> [d])
None
......@@ -649,13 +704,30 @@ let subst to_subst =
in
Trans.bind found_eq subst
exception Invalid_trans_arg of symbol
let t_lsymbol x =
match x with
| Tlsymbol x -> x
| _ -> raise (Invalid_trans_arg x)
let t_tsymbol x =
match x with
| Ttysymbol x -> x
| _ -> raise (Invalid_trans_arg x)
let t_prsymbol x =
match x with
| Tprsymbol x -> x
| _ -> raise (Invalid_trans_arg x)
let () = wrap_and_register ~desc:"remove a literal using an equality on it"
"subst"
(Tlsymbol Ttrans) subst
(Tsymbol Ttrans) (fun x -> subst (t_lsymbol x))
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument"
"clear_but"
(Tprlist Ttrans) clear_but
(Tlist Ttrans) (fun l -> clear_but (List.map t_prsymbol l))
let () = wrap_and_register ~desc:"left transform a goal of the form A \\/ B into A"
......@@ -668,7 +740,7 @@ let () = wrap_and_register ~desc:"right transform a goal of the form A \\/ B int
let () = wrap_and_register ~desc:"unfold ls pr: unfold logic symbol ls in hypothesis pr. Experimental." (* TODO *)
"unfold"
(Tlsymbol (Tprsymbol Ttrans)) unfold
(Tsymbol (Tsymbol Ttrans)) (fun ls pr -> unfold (t_lsymbol ls) (t_prsymbol pr))
let () = wrap_and_register ~desc:"intros n"
"intros"
......@@ -700,16 +772,16 @@ let () = wrap_and_register
let () = wrap_and_register
~desc:"remove <prop list>: removes a list of hypothesis given by their names separated with ','. Example: remove_list a,b,c "
"remove"
(Tprlist Ttrans) remove_list
(Tlist Ttrans) (fun l -> remove_list l)
let () = wrap_and_register
~desc:"instantiate <prop> <term> generates a new hypothesis with first quantified variables of prop replaced with term "
"instantiate"
(Tprsymbol (Tterm Ttrans)) instantiate
(Tsymbol (Tterm Ttrans)) (fun x -> instantiate (t_prsymbol x))
let () = wrap_and_register
~desc:"apply <prop> applies prop to the goal" "apply"
(Tprsymbol Ttrans_l) apply
(Tsymbol Ttrans_l) (fun x -> apply (t_prsymbol x))
(* let () = wrap_and_register *)
(* ~desc:"duplicate <int> duplicates the goal int times" "duplicate" *)
......@@ -721,7 +793,8 @@ let () = wrap_and_register
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite
(Toptbool ("<-",(Tsymbol (Topt ("in", Tsymbol Ttrans_l)))))
(fun b p opt -> rewrite b (t_prsymbol p) (Opt.map t_prsymbol opt))
(* register_transform_with_args_l *)
(* ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
(* "rewrite" *)
......@@ -730,7 +803,7 @@ let _ = wrap_and_register
let () = wrap_and_register
~desc:"replace <term1> <term2> <name> replaces occcurences of term1 by term2 in prop name"
"replace"
(Tterm (Tterm (Tprsymbol Ttrans_l))) replace
(Tterm (Tterm (Tsymbol Ttrans_l))) (fun t1 t2 p -> replace t1 t2 (t_prsymbol p))
let () = wrap_and_register
~desc:"induction <term1> <term2> performs induction on int term1 from int term2"
......@@ -738,7 +811,7 @@ let () = wrap_and_register
(Tterm (Tterm Tenvtrans_l)) induction
let () = wrap_and_register ~desc:"destruct <name> destructs the head constructor of hypothesis name"
"destruct" (Tprsymbol Ttrans_l) destruct
"destruct" (Tsymbol Ttrans_l) (fun x -> destruct (t_prsymbol x))
let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type"
"destruct_alg" (Tterm Ttrans_l) destruct_alg
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