Remove_list to remove list of hypotheses (prsymbol)

remove_list [H1,H2] works. Without spaces and with this exact syntax.
This is to be modified later. In particular, we should probably handle
parsing of arguments differently.

src/parser/lexer.mll

@@ -245,6 +245,8 @@ rule token = parse
 
   let parse_term lb = Parser.term_eof token lb
 
+  let parse_list_ident lb = Parser.ident_comma_list token lb
+
   let parse_logic_file env path lb =
     open_file token (Lexing.from_string "") (Typing.open_file env path);
     Loc.with_location (logic_file token) lb;

src/parser/parser.mly

@@ -220,6 +220,7 @@ end
 %start <Ptree.incremental -> unit> open_file
 %start <unit> logic_file program_file
 %start <Ptree.term> term_eof
+%start <Ptree.ident list> ident_comma_list
 %%
 
 (* parsing of a single term *)
@@ -1062,6 +1063,10 @@ sident:
 | ident   { $1 }
 | STRING  { mk_id $1 $startpos $endpos }
 
+(* Parsing of a list *)
+ident_comma_list:
+| LEFTSQ comma_list1(ident) RIGHTSQ EOF { $2 }
+
 (* Labels and position markers *)
 
 labels(X): X label* { add_lab $1 $2 }

src/transform/args_wrapper.ml

@@ -218,6 +218,7 @@ type (_, _) 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
   | Tterm       : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
   | Tstring     : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
@@ -250,6 +251,10 @@ let parse_and_type ~as_fmla s task =
   in
   t
 
+let parse_list_ident s =
+  let lb = Lexing.from_string s in
+  Lexer.parse_list_ident lb
+
 let parse_int s =
   try int_of_string s
   with Failure _ -> raise (Arg_parse_error (s,"int expected"))
@@ -274,6 +279,7 @@ let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
     | Tty t       -> t
     | Ttysymbol t -> t
     | Tprsymbol t -> t
+    | Tprlist t   -> t
     | Tlsymbol t  -> t
     | Tterm t     -> t
     | Tstring t   -> t
@@ -293,6 +299,7 @@ let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
     | 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
     | Tterm t        -> is_trans_typ_l t
     | Tstring t      -> is_trans_typ_l t
@@ -312,6 +319,7 @@ let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
     | Tty _          -> "type"
     | Ttysymbol _    -> "type symbol"
     | Tprsymbol _    -> "prop symbol"
+    | Tprlist _      -> "list of prop symbol"
     | Tlsymbol _     -> "logic symbol"
     | Tterm _        -> "term"
     | Tstring _      -> "string"
@@ -331,6 +339,7 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
     | 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
     | Tterm t        -> "term -> " ^ print_type t
     | Tstring t      -> "string -> " ^ print_type t
@@ -364,6 +373,11 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
       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 ->
+      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
+      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

src/transform/args_wrapper.mli

@@ -22,6 +22,7 @@ type (_, _) 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

src/transform/case.ml

@@ -114,6 +114,17 @@ let remove_task_decl (name: Ident.ident) : task trans =
 let remove name =
   remove_task_decl name.pr_name
 
+(* from task [delta, name1, name2, ... namen |- G] build the task [delta |- G] *)
+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) ->
+        []
+      | _ -> [d])
+    None
+
 (* from task [delta, name:forall x.A |- G,
      build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
 let instantiate (pr: Decl.prsymbol) t =
@@ -709,6 +720,11 @@ let () = wrap_and_register
     "remove"
     (Tprsymbol Ttrans) remove
 
+let () = wrap_and_register
+    ~desc:"remove_list <prop list>: removes a list of hypothesis when given their names. Example syntax: remove_list [a,b,c] ."
+     "remove_list"
+     (Tprlist Ttrans) remove_list
+
 let () = wrap_and_register
     ~desc:"instantiate <prop> <term> generates a new hypothesis with first quantified variables of prop replaced with term "
     "instantiate"