args_wrapper.ml 21.2 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15
open Task
open Ty
open Term
open Trans
16 17 18 19
open Ident
open Theory
open Decl

20
exception Parse_error of string
21
exception Arg_expected of string * string
22
exception Arg_theory_not_found of string
23
exception Arg_expected_none of string
24
exception Arg_qid_not_found of Ptree.qualid
25
exception Arg_pr_not_found of prsymbol
26
exception Arg_error of string
27 28 29 30

let () = Exn_printer.register
    (fun fmt e ->
      match e with
31 32
      | Parse_error s ->
          Format.fprintf fmt "Parsing error: %s" s
33 34 35 36 37 38 39
      | Arg_expected (ty, s) ->
          Format.fprintf fmt "Argument expected of type: %s\n Argument given: %s" ty s
      | Arg_theory_not_found s ->
          Format.fprintf fmt "Theory not found %s" s
      | Arg_expected_none s ->
          Format.fprintf fmt "Argument expected of type %s. None were given." s
      | _ -> raise e)
40

41
open Wstdlib
42 43 44 45 46 47 48 49

(* Use symb to encapsulate ids into correct categories of symbols *)
type symb =
  | Ts of tysymbol
  | Ls of lsymbol
  | Pr of prsymbol

(* [add_unsafe s id tables] Add (s, id) to tables without any checking. *)
50
let add_unsafe (s: string) (id: symb) (tables: naming_table) : naming_table =
51 52 53 54 55 56 57 58
  match id with
  | Ts ty ->
      {tables with
        namespace = {tables.namespace with ns_ts = Mstr.add s ty tables.namespace.ns_ts};
      }
  | Ls ls ->
      {tables with
        namespace = {tables.namespace with ns_ls = Mstr.add s ls tables.namespace.ns_ls};
59
      }
60 61 62
  | Pr pr ->
      {tables with
        namespace = {tables.namespace with ns_pr = Mstr.add s pr tables.namespace.ns_pr};
63
}
64

Andrei Paskevich's avatar
Andrei Paskevich committed
65
let id_unique tables id = id_unique_attr tables.printer id
66

67
(* Adds symbols that are introduced to a constructor *)
68
let constructor_add (cl: constructor list) tables : naming_table =
69
  List.fold_left
70 71 72 73 74 75
    (fun tables ((ls, cl): constructor) ->
      let tables = List.fold_left
          (fun tables (cs: lsymbol option) ->
            match cs with
            | Some cs ->
                let id = cs.ls_name in
76
                let s = id_unique tables id in
77 78 79
                add_unsafe s (Ls cs) tables
            | None -> tables) tables cl in
      let id = ls.ls_name in
80
      let s = id_unique tables id in
81
      add_unsafe s (Ls ls) tables)
82 83 84 85 86 87 88 89
    tables
    cl

(* Add symbols that are introduced by an inductive *)
let ind_decl_add il tables =
  List.fold_left
    (fun tables ((pr, _): prsymbol * term) ->
      let id = pr.pr_name in
90
      let s = id_unique tables id in
91 92 93 94
      add_unsafe s (Pr pr) tables)
    il
    tables

95 96


97 98
(* [add d printer tables] Adds all new declaration of symbol inside d to tables.
  It uses printer to give them a unique name and also register these new names in printer *)
99
let add (d: decl) (tables: naming_table): naming_table =
100 101 102 103
  match d.d_node with
  | Dtype ty ->
      (* only current symbol is new in the declaration (see create_ty_decl) *)
      let id = ty.ts_name in
104
      let s = id_unique tables id in
105 106 107 108 109 110 111
      add_unsafe s (Ts ty) tables
  | Ddata dl ->
      (* first part is new. Also only first part of each constructor seem new
         (see create_data_decl) *)
      List.fold_left
        (fun tables (dd: data_decl) ->
          let id = (fst dd).ts_name in
112
          let s = id_unique tables id in
113 114 115 116 117 118 119
          let tables = add_unsafe s (Ts (fst dd)) tables in
          constructor_add (snd dd) tables)
        tables
        dl
  | Dparam ls ->
      (* Only one lsymbol which is new *)
      let id = ls.ls_name in
120
      let s = id_unique tables id in
121 122 123 124 125 126
      add_unsafe s (Ls ls) tables
  | Dlogic lsd ->
      (* Only first part of logic_decl is new (see create_logic) *)
      List.fold_left
        (fun tables ((ls,_): logic_decl) ->
          let id = ls.ls_name in
127
          let s = id_unique tables id in
128 129 130 131 132 133 134 135
          add_unsafe s (Ls ls) tables)
        tables
        lsd
  | Dind (_is, il) ->
      (* Every symbol is new except symbol inside terms (see create_ind_decl) *)
      List.fold_left
        (fun tables ((ls,ind): ind_decl) ->
          let id = ls.ls_name in
136
          let s = id_unique tables id in
137 138 139 140
          let tables = add_unsafe s (Ls ls) tables in
          ind_decl_add tables ind)
        tables
        il
141
  | Dprop (_, pr, _) ->
142 143
      (* Only pr is new in Dprop (see create_prop_decl) *)
      let id = pr.pr_name in
144
      let s = id_unique tables id in
145
      add_unsafe s (Pr pr) tables
146

147 148 149 150 151
(* Adds meta arguments of type ident to tables *)
let add_meta_id_args (al: meta_arg list) (tables: naming_table): naming_table =
  List.fold_left
    (fun t a ->
      match a with
Raphael Rieu-Helft's avatar
Raphael Rieu-Helft committed
152
      | MAid id ->
153 154 155 156 157
         let s = id_unique tables id in
         { tables with meta_id_args = Mstr.add s id tables.meta_id_args }
      | _ -> t)
    tables al

Sylvain Dailler's avatar
Sylvain Dailler committed
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
(* Takes the set of meta defined in the tasks and build the coercions from it.
   TODO we could have a set of coercions in the task ? Same problem for naming
   table ?
*)
let build_coercion_map km_meta =
  try
    let crc_set = Theory.Mmeta.find Theory.meta_coercion km_meta in
    let crc_map = Stdecl.fold (fun elem crc_map ->
      match elem.Theory.td_node with
      | Meta (m,([MAls ls] as _al)) when meta_equal m Theory.meta_coercion ->
        Coercion.add crc_map ls
      | _ -> crc_map) crc_set.tds_set Coercion.empty in
    crc_map
  with
  | Not_found -> Coercion.empty

174
let build_naming_tables task : naming_table =
175
  let isanitizer = None (* sanitizer do not seem to be necessary *) in
176
  let lsanitize = sanitizer char_to_lalpha char_to_alnumus in
177 178
  let pr = create_ident_printer Pretty.why3_keywords ?sanitizer:isanitizer in
  let apr = create_ident_printer Pretty.why3_keywords ~sanitizer:lsanitize in
179
  let km = Task.task_known task in
Sylvain Dailler's avatar
Sylvain Dailler committed
180
  let km_meta = Task.task_meta task in
181 182 183
  let tables = {
      namespace = empty_ns;
      known_map = km;
Sylvain Dailler's avatar
Sylvain Dailler committed
184
      coercion = Coercion.empty;
185
      printer = pr;
186
      aprinter = apr;
187
      meta_id_args = Mstr.empty;
188
  } in
189 190 191 192 193
(*  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. *)
194
  (* TODO:imported theories should be added in the namespace too *)
MARCHE Claude's avatar
MARCHE Claude committed
195
  let tables = Task.task_fold
196
    (fun t d ->
197 198 199 200
      match d.td_node with
      | Decl d -> add d t
      | Meta (_,al) -> add_meta_id_args al t
      | _ -> t) tables task
MARCHE Claude's avatar
MARCHE Claude committed
201
  in
Sylvain Dailler's avatar
Sylvain Dailler committed
202 203 204
  let crc_map = build_coercion_map km_meta in
  {tables with coercion = crc_map}

205
(************* wrapper  *************)
206

207
type symbol =
208 209 210
  | Tstysymbol of Ty.tysymbol
  | Tsprsymbol of Decl.prsymbol
  | Tslsymbol of Term.lsymbol
211

212
type (_, _) trans_typ =
213 214 215 216
  | Ttrans      : ((task trans), task) trans_typ
  | Ttrans_l    : ((task tlist), task list) trans_typ
  | Tenvtrans   : (Env.env -> (task trans), task) trans_typ
  | Tenvtrans_l : (Env.env -> (task tlist), task list) trans_typ
217
  | Tstring     : ('a, 'b) trans_typ -> ((string -> 'a), 'b) trans_typ
218 219
  | Tint        : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
  | Tty         : ('a, 'b) trans_typ -> ((ty -> 'a), 'b) trans_typ
220 221 222 223
  | 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
224 225
  | Tsymbol     : ('a, 'b) trans_typ -> ((symbol -> 'a), 'b) trans_typ
  | Tlist       : ('a, 'b) trans_typ -> ((symbol list -> 'a), 'b) trans_typ
226 227
  | Tidentlist  : ('a, 'b) trans_typ -> ((string list -> 'a), 'b) trans_typ
  | Ttermlist   : ('a, 'b) trans_typ -> ((term list -> 'a), 'b) trans_typ
228 229 230 231 232
  | Tterm       : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
  | Tformula    : ('a, 'b) trans_typ -> ((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
233

234 235
let find_pr q tables =
  Theory.ns_find_pr tables.namespace (Typing.string_list_of_qualid q)
236

237 238
let find_ts q tables =
  Theory.ns_find_ts tables.namespace (Typing.string_list_of_qualid q)
239

240 241
let find_ls q tables =
  Theory.ns_find_ls tables.namespace (Typing.string_list_of_qualid q)
242

243 244
let find_symbol q tables =
  try Tsprsymbol (find_pr q tables) with
245
        | Not_found ->
246
          try Tslsymbol (find_ls q tables) with
247
          | Not_found ->
248 249
            try Tstysymbol (find_ts q tables) with
            | Not_found -> raise (Arg_qid_not_found q)
250 251


252
let type_ptree ~as_fmla t tables =
253 254
  let km = tables.known_map in
  let ns = tables.namespace in
Sylvain Dailler's avatar
Sylvain Dailler committed
255
  let crc = tables.coercion in
256
  if as_fmla
257 258
  then Typing.type_fmla_in_namespace ns km crc t
  else Typing.type_term_in_namespace ns km crc t
259

260 261
exception Arg_parse_type_error of Loc.position * string * exn

262
let parse_and_type ~as_fmla s task =
263 264 265
  try
    let lb = Lexing.from_string s in
    let t =
266
      Lexer.parse_term lb
267 268
    in
    let t =
269
      type_ptree ~as_fmla:as_fmla t task
270 271 272 273
    in
    t
  with
  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
274

275 276 277 278 279 280 281 282 283 284 285 286 287
let parse_and_type_list ~as_fmla s task =
  try
    let lb = Lexing.from_string s in
    let t_list =
      Lexer.parse_term_list lb
    in
    let t_list =
      List.map (fun t -> type_ptree ~as_fmla:as_fmla t task) t_list
    in
    t_list
  with
  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))

288 289 290 291 292 293 294 295 296 297 298 299 300 301
let parse_qualid s =
  try
    let lb = Lexing.from_string s in
    Lexer.parse_qualid lb
  with
  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))

let parse_list_qualid s =
  try
    let lb = Lexing.from_string s in
    Lexer.parse_list_qualid lb
  with
  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))

302
let parse_list_ident s =
303 304 305 306 307
  try
    let lb = Lexing.from_string s in
    Lexer.parse_list_ident lb
  with
  | Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
308

309 310 311 312
let build_error s e =
  let loc = Loc.user_position "" 0 0 (String.length s - 1) in
  raise (Arg_parse_type_error (loc, s, e))

313 314
let parse_int s =
  try int_of_string s
315 316
  with Failure _ ->
    build_error s (Parse_error "int expected")
317 318 319 320 321 322 323 324

let parse_theory env s =
  try
    let path, name = match Strings.split '.' s with
      | [name] -> [],name
      | path::[name] ->
        let path = Strings.split '/' path in
        path, name
325 326
      | _ ->
          build_error s (Parse_error "Ill-formed theory name")
327 328 329
    in
    Env.read_theory env path name
  with
330 331
    _ ->
      build_error s (Parse_error "Theory not found")
332

333
let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
334
  fun t ->
Clément Fumex's avatar
Clément Fumex committed
335
    match t with
DAILLER Sylvain's avatar
DAILLER Sylvain committed
336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
    | 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
    | Ttheory t    -> t
    | Ttermlist t  -> t
    | Tidentlist t -> t
    | _            -> assert false
351 352 353 354 355

type _ trans_typ_is_l = Yes : (task list) trans_typ_is_l | No : task trans_typ_is_l

let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
  fun t -> match t with
356
    | Tenvtrans      -> No
357
    | Ttrans         -> No
358
    | Tenvtrans_l    -> Yes
359 360
    | Ttrans_l       -> Yes
    | Tint t         -> is_trans_typ_l t
361
    | Tstring t      -> is_trans_typ_l t
362
    | Tty t          -> is_trans_typ_l t
363 364 365 366
    | 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
367 368
    | Tsymbol t      -> is_trans_typ_l t
    | Tlist t        -> is_trans_typ_l t
369
    | Tterm t        -> is_trans_typ_l t
370
    | Tidentlist t   -> is_trans_typ_l t
371
    | Ttermlist t    -> is_trans_typ_l t
372 373 374 375
    | Tformula t     -> is_trans_typ_l t
    | Ttheory t      -> is_trans_typ_l t
    | Topt (_,t)     -> is_trans_typ_l t
    | Toptbool (_,t) -> is_trans_typ_l t
Clément Fumex's avatar
Clément Fumex committed
376

377
let rec string_of_trans_typ : type a b. (a, b) trans_typ -> string =
Clément Fumex's avatar
Clément Fumex committed
378 379
  fun t ->
    match t with
380 381 382 383 384 385
    | Ttrans         -> "task"
    | Ttrans_l       -> "list task"
    | Tenvtrans      -> "env -> task"
    | Tenvtrans_l    -> "env -> list task"
    | Tint _         -> "int"
    | Tstring _      -> "string"
Clément Fumex's avatar
Clément Fumex committed
386
    | Tty _          -> "type"
387 388 389 390
    | Ttysymbol _    -> "tysymbol"
    | Tprsymbol _    -> "prsymbol"
    | Tprlist _      -> "list prsymbol"
    | Tlsymbol _     -> "lsymbol"
391
    | Tsymbol _      -> "symbol"
392
    | Tlist _        -> "list symbol"
Clément Fumex's avatar
Clément Fumex committed
393 394
    | Tterm _        -> "term"
    | Tformula _     -> "formula"
395
    | Tidentlist _   -> "list ident"
396
    | Ttermlist _    -> "list term"
Clément Fumex's avatar
Clément Fumex committed
397
    | Ttheory _      -> "theory"
398 399
    | Topt (s,t)     -> "?" ^ s ^ (string_of_trans_typ t)
    | Toptbool (s,_) -> "?" ^ s ^ ":bool"
400

401 402
let rec print_type : type a b. Format.formatter -> (a, b) trans_typ -> unit =
  fun fmt t ->
403
    match t with
404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
    | Ttrans         -> Format.fprintf fmt "task"
    | Ttrans_l       -> Format.fprintf fmt "list task"
    | Tenvtrans      -> Format.fprintf fmt "env -> task"
    | Tenvtrans_l    -> Format.fprintf fmt "env -> list task"
    | Tint t         -> Format.fprintf fmt "integer -> %a" print_type t
    | Tstring t      -> Format.fprintf fmt "string -> %a" print_type t
    | Tty t          -> Format.fprintf fmt "type -> %a" print_type t
    | Ttysymbol t    -> Format.fprintf fmt "type_symbol -> %a" print_type t
    | Tprsymbol t    -> Format.fprintf fmt "prsymbol -> %a" print_type t
    | Tprlist t      -> Format.fprintf fmt "list prsymbol -> %a" print_type t
    | Tlsymbol t     -> Format.fprintf fmt "lsymbol -> %a" print_type t
    | Tsymbol t      -> Format.fprintf fmt "symbol -> %a" print_type t
    | Tlist t        -> Format.fprintf fmt "list symbol -> %a" print_type t
    | Tterm t        -> Format.fprintf fmt "term -> %a" print_type t
    | Tformula t     -> Format.fprintf fmt "formula -> %a" print_type t
    | Tidentlist t   -> Format.fprintf fmt "list ident -> %a" print_type t
    | Ttermlist t    -> Format.fprintf fmt "list term -> %a" print_type t
    | Ttheory t      -> Format.fprintf fmt "theory -> %a" print_type t
    | Topt (s,t)     -> Format.fprintf fmt "?%s -> %a" s print_type t
    | Toptbool (s,t) -> Format.fprintf fmt "?%s:bool -> %a" s print_type t
424

425
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> naming_table -> task -> b =
426
  fun t f l env tables task ->
427
    match t, l with
428 429 430 431 432 433 434 435
    | Ttrans, []-> apply f task
    | Ttrans_l, [] -> apply f task
    | Tenvtrans, [] -> apply (f env) task
    | Tenvtrans_l, [] -> apply (f env) task
    | Ttrans, _ -> raise (Unnecessary_arguments l)
    | Ttrans_l, _ -> raise (Unnecessary_arguments l)
    | Tenvtrans, _ -> raise (Unnecessary_arguments l)
    | Tenvtrans_l, _ -> raise (Unnecessary_arguments l)
436
    | Tint t', s :: tail ->
437
      let arg = parse_int s in wrap_to_store t' (f arg) tail env tables task
438 439
    | Tstring t', s :: tail ->
       wrap_to_store t' (f s) tail env tables task
440
    | Tformula t', s :: tail ->
441 442
      let te = parse_and_type ~as_fmla:true s tables in
      wrap_to_store t' (f te) tail env tables task
443
    | Tterm t', s :: tail ->
444 445
      let te = parse_and_type ~as_fmla:false s tables in
      wrap_to_store t' (f te) tail env tables task
446 447
    | Tty t', _s :: tail ->
      let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
448
      wrap_to_store t' (f ty) tail env tables task
449 450 451 452
    | 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 ->
453 454 455
       let q = parse_qualid s in
       let pr = try (find_pr q tables) with
                | Not_found -> raise (Arg_qid_not_found q) in
456 457
      wrap_to_store t' (f pr) tail env tables task
    | Tprlist t', s :: tail ->
458
        let pr_list = parse_list_qualid s in
459 460
        let pr_list =
        List.map (fun id ->
461 462
                    try find_pr id tables with
                    | Not_found -> raise (Arg_qid_not_found id))
463 464 465
                 pr_list in
        wrap_to_store t' (f pr_list) tail env tables task
    | Tlsymbol t', s :: tail ->
466 467 468
       let q = parse_qualid s in
       let pr = try (find_ls q tables) with
               | Not_found -> raise (Arg_qid_not_found q) in
469
      wrap_to_store t' (f pr) tail env tables task
470
    | Tsymbol t', s :: tail ->
471 472 473
       let q = parse_qualid s in
       let symbol = find_symbol q tables in
       wrap_to_store t' (f symbol) tail env tables task
474
    | Tlist t', s :: tail ->
475 476 477 478
       let pr_list = parse_list_qualid s in
       let pr_list =
         List.map (fun id -> find_symbol id tables) pr_list in
       wrap_to_store t' (f pr_list) tail env tables task
479
    | Ttheory t', s :: tail ->
480 481
       let th = parse_theory env s in
       wrap_to_store t' (f th) tail env tables task
482
    | Tidentlist t', s :: tail ->
483 484
       let list = List.map (fun id -> id.Ptree.id_str) (parse_list_ident s) in
       wrap_to_store t' (f list) tail env tables task
485 486 487
    | Ttermlist t', s :: tail ->
       let term_list = parse_and_type_list ~as_fmla:false s tables in
       wrap_to_store t' (f term_list) tail env tables task
488
    | Topt (optname, t'), s :: s' :: tail when s = optname ->
489
       begin match t' with
490 491
        | Tint t' ->
          let arg = Some (parse_int s') in
492
          wrap_to_store t' (f arg) tail env tables task
493
        | Tprsymbol t' ->
494 495 496
           let q = parse_qualid s' in
           let arg = try Some (find_pr q tables) with
                    | Not_found -> raise (Arg_qid_not_found q) in
497
          wrap_to_store t' (f arg) tail env tables task
498
        | Tsymbol t' ->
499 500 501
           let q = parse_qualid s' in
           let arg = Some (find_symbol q tables) in
           wrap_to_store t' (f arg) tail env tables task
502
        | Tformula t' ->
503 504
           let arg = Some (parse_and_type ~as_fmla:true s' tables) in
           wrap_to_store t' (f arg) tail env tables task
505
        | Tterm t' ->
506 507
           let arg = Some (parse_and_type ~as_fmla:false s' tables) in
           wrap_to_store t' (f arg) tail env tables task
508
        | Ttheory t' ->
509 510
           let arg = Some (parse_theory env s') in
           wrap_to_store t' (f arg) tail env tables task
511
        | Tstring t' ->
512 513
           let arg = Some s' in
           wrap_to_store t' (f arg) tail env tables task
514 515 516 517 518 519 520 521 522
        | Tprlist t' ->
            let pr_list = parse_list_qualid s' in
            let pr_list =
              List.map (fun id ->
                try find_pr id tables with
                | Not_found -> raise (Arg_qid_not_found id))
                pr_list in
            let arg = Some pr_list in
            wrap_to_store t' (f arg) tail env tables task
Sylvain Dailler's avatar
Sylvain Dailler committed
523 524 525
        | Ttermlist t' ->
            let term_list = parse_and_type_list ~as_fmla:false s' tables in
            wrap_to_store t' (f (Some term_list)) tail env tables task
DAILLER Sylvain's avatar
DAILLER Sylvain committed
526 527 528 529
        | Tidentlist t' ->
            let list =
              List.map (fun id -> id.Ptree.id_str) (parse_list_ident s') in
            wrap_to_store t' (f (Some list)) tail env tables task
530 531 532 533 534
        | Tlist t' ->
            let pr_list = parse_list_qualid s' in
            let pr_list =
              List.map (fun id -> find_symbol id tables) pr_list in
            wrap_to_store t' (f (Some pr_list)) tail env tables task
535
        | _ -> raise (Arg_expected (string_of_trans_typ t', s'))
536
       end
537
    | Topt (_, t'), _ ->
538
       wrap_to_store (trans_typ_tail t') (f None) l env tables task
539
    | Toptbool (optname, t'), s :: tail when s = optname ->
540
      wrap_to_store t' (f true) tail env tables task
541
    | Toptbool (_, t'), _ ->
542
      wrap_to_store t' (f false) l env tables task
543
    | _, [] -> raise (Arg_expected_none (string_of_trans_typ t))
544

545
let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
546
  fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
547 548

let wrap   : type a. (a, task) trans_typ -> a -> trans_with_args =
549
  fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
550

551 552
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env ->
                    Trans.naming_table -> b trans =
553
  fun t f l env tables -> Trans.store (wrap_to_store t f l env tables)
554

555 556 557 558
(* the one in Scanf is awfully broken with respect to backslashes *)
let format_from_string s fmt =
  Scanf.sscanf_format (Printf.sprintf "%S" s) fmt (fun s -> s)

559 560
let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_typ -> a -> unit =
  fun ~desc name t f  ->
561 562 563 564
    (* "%@\n" is escaped on purpose *)
    let type_desc = Format.asprintf "type: %a%@\n" print_type t in
    let type_desc = format_from_string type_desc Pp.empty_formatted in
    let desc = type_desc ^^ desc in
565 566
    let trans = wrap_any t f in
    match is_trans_typ_l t with
567 568
    | Yes -> Trans.register_transform_with_args_l ~desc name trans
    | No  -> Trans.register_transform_with_args   ~desc name trans
569 570 571


let find_symbol s tables = find_symbol (parse_qualid s) tables