support for "syntax cloned"

src/core/printer.ml

@@ -30,11 +30,10 @@ open Task
 
 type prelude = string list
 type prelude_map = prelude Mid.t
-type syntax_map = string Mid.t
 
 type 'a pp = formatter -> 'a -> unit
 
-type printer = prelude -> prelude_map -> syntax_map -> task pp
+type printer = prelude -> prelude_map -> task pp
 
 let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
 
@@ -125,34 +124,46 @@ let print_th_prelude task fmt pm =
 exception KnownTypeSyntax of tysymbol
 exception KnownLogicSyntax of lsymbol
 
-let add_ts_syntax ts s sm =
+let meta_syntax_type  = register_meta "syntax_type" [MTtysymbol; MTstring]
+let meta_syntax_logic = register_meta "syntax_logic" [MTlsymbol; MTstring]
+let meta_remove_prop  = register_meta "remove_prop" [MTprsymbol]
+
+let syntax_type ts s =
   check_syntax s (List.length ts.ts_args);
-  if Mid.mem ts.ts_name sm then raise (KnownTypeSyntax ts);
-  Mid.add ts.ts_name s sm
+  create_meta meta_syntax_type [MAts ts; MAstr s]
 
-let add_ls_syntax ls s sm =
+let syntax_logic ls s =
   check_syntax s (List.length ls.ls_args);
-  if Mid.mem ls.ls_name sm then raise (KnownLogicSyntax ls);
-  Mid.add ls.ls_name s sm
+  create_meta meta_syntax_logic [MAls ls; MAstr s]
 
-let query_syntax sm id =
-  try Some (Mid.find id sm) with Not_found -> None
+let remove_prop pr =
+  create_meta meta_remove_prop [MApr pr]
 
-let meta_remove_type  = register_meta "remove_type" [MTtysymbol]
-let meta_remove_logic = register_meta "remove_logic" [MTlsymbol]
-let meta_remove_prop  = register_meta "remove_prop" [MTprsymbol]
-
-let remove_type  ts = create_meta meta_remove_type  [MAts ts]
-let remove_logic ls = create_meta meta_remove_logic [MAls ls]
-let remove_prop  pr = create_meta meta_remove_prop  [MApr pr]
+let get_syntax_map task =
+  let add_ts td m = match td.td_node with
+    | Meta (_,[MAts ts; MAstr s]) ->
+        if Mid.mem ts.ts_name m then raise (KnownTypeSyntax ts);
+        Mid.add ts.ts_name s m
+    | _ -> assert false
+  in
+  let add_ls td m = match td.td_node with
+    | Meta (_,[MAls ls; MAstr s]) ->
+        if Mid.mem ls.ls_name m then raise (KnownLogicSyntax ls);
+        Mid.add ls.ls_name s m
+    | _ -> assert false
+  in
+  let m = Mid.empty in
+  let m = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set m in
+  let m = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set m in
+  m
 
 let get_remove_set task =
   let add_ts td s = match td.td_node with
-    | Meta (_,[MAts ts]) -> Sid.add ts.ts_name s
+    | Meta (_,[MAts ts; _]) -> Sid.add ts.ts_name s
     | _ -> assert false
   in
   let add_ls td s = match td.td_node with
-    | Meta (_,[MAls ls]) -> Sid.add ls.ls_name s
+    | Meta (_,[MAls ls; _]) -> Sid.add ls.ls_name s
     | _ -> assert false
   in
   let add_pr td s = match td.td_node with
@@ -160,11 +171,14 @@ let get_remove_set task =
     | _ -> assert false
   in
   let s = Sid.empty in
-  let s = Stdecl.fold add_ts (find_meta task meta_remove_type).tds_set s in
-  let s = Stdecl.fold add_ls (find_meta task meta_remove_logic).tds_set s in
+  let s = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set s in
+  let s = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set s in
   let s = Stdecl.fold add_pr (find_meta task meta_remove_prop).tds_set s in
   s
 
+let query_syntax sm id =
+  try Some (Mid.find id sm) with Not_found -> None
+
 (** {2 exceptions to use in transformations and printers} *)
 
 exception UnsupportedType of ty   * string

src/core/printer.mli

@@ -29,11 +29,9 @@ open Task
 type prelude = string list
 type prelude_map = prelude Mid.t
 
-type syntax_map = string Mid.t
-
 type 'a pp = Format.formatter -> 'a -> unit
 
-type printer = prelude -> prelude_map -> syntax_map -> task pp
+type printer = prelude -> prelude_map -> task pp
 
 val register_printer : string -> printer -> unit
 
@@ -46,20 +44,18 @@ val list_printers : unit -> string list
 val print_prelude : prelude pp
 val print_th_prelude : task -> prelude_map pp
 
-val meta_remove_type : meta
-val meta_remove_logic : meta
+val meta_syntax_type : meta
+val meta_syntax_logic : meta
 val meta_remove_prop : meta
 
-val remove_type : tysymbol -> tdecl
-val remove_logic : lsymbol -> tdecl
+val syntax_type : tysymbol -> string -> tdecl
+val syntax_logic : lsymbol -> string -> tdecl
 val remove_prop : prsymbol -> tdecl
 
+val get_syntax_map : task -> string Mid.t
 val get_remove_set : task -> Sid.t
 
-val add_ts_syntax : tysymbol -> string -> syntax_map -> syntax_map
-val add_ls_syntax : lsymbol  -> string -> syntax_map -> syntax_map
-
-val query_syntax : syntax_map -> ident -> string option
+val query_syntax : string Mid.t -> ident -> string option
 
 val syntax_arguments : string -> 'a pp -> 'a list pp
 (** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt

src/core/task.ml

@@ -220,29 +220,29 @@ exception NotTaggingMeta of meta
 
 let find_tagged_ts t tds acc =
   begin match t.meta_type with
-    | [MTtysymbol] -> ()
+    | MTtysymbol :: _ -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MAts ts]) when meta_equal s t -> Sts.add ts acc
+    | Meta (s, MAts ts :: _) when meta_equal s t -> Sts.add ts acc
     | _ -> assert false) tds.tds_set acc
 
 let find_tagged_ls t tds acc =
   begin match t.meta_type with
-    | [MTlsymbol] -> ()
+    | MTlsymbol :: _ -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MAls ls]) when meta_equal s t -> Sls.add ls acc
+    | Meta (s, MAls ls :: _) when meta_equal s t -> Sls.add ls acc
     | _ -> assert false) tds.tds_set acc
 
 let find_tagged_pr t tds acc =
   begin match t.meta_type with
-    | [MTprsymbol] -> ()
+    | MTprsymbol :: _ -> ()
     | _ -> raise (NotTaggingMeta t)
   end;
   Stdecl.fold (fun td acc -> match td.td_node with
-    | Meta (s, [MApr pr]) when meta_equal s t -> Spr.add pr acc
+    | Meta (s, MApr pr :: _) when meta_equal s t -> Spr.add pr acc
     | _ -> assert false) tds.tds_set acc
 
 exception NotExclusiveMeta of meta

src/driver/driver.ml

@@ -39,7 +39,6 @@ type driver = {
   drv_transform : string list;
   drv_prelude   : prelude;
   drv_thprelude : prelude_map;
-  drv_syntax    : syntax_map;
   drv_meta      : (theory * Stdecl.t) Mid.t;
   drv_meta_cl   : (theory * Stdecl.t) Mid.t;
   drv_regexps   : (Str.regexp * prover_answer) list;
@@ -103,7 +102,6 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
   List.iter add_global f.f_global;
 
   let thprelude = ref Mid.empty in
-  let syntax    = ref Mid.empty in
   let meta      = ref Mid.empty in
   let meta_cl   = ref Mid.empty in
   let qualid    = ref [] in
@@ -125,14 +123,12 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
     | Rprelude s ->
         let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
         thprelude := Mid.add th.th_name (l @ [s]) !thprelude
-    | Rsyntaxls (q,s) ->
-        let ls = find_ls th q in
-        add_meta th (remove_logic ls) meta;
-        syntax := add_ls_syntax ls s !syntax
-    | Rsyntaxts (q,s) ->
-        let ts = find_ts th q in
-        add_meta th (remove_type ts) meta;
-        syntax := add_ts_syntax ts s !syntax
+    | Rsyntaxts (c,q,s) ->
+        let td = syntax_type (find_ts th q) s in
+        add_meta th td (if c then meta_cl else meta)
+    | Rsyntaxls (c,q,s) ->
+        let td = syntax_logic (find_ls th q) s in
+        add_meta th td (if c then meta_cl else meta)
     | Rremovepr (c,q) ->
         let td = remove_prop (find_pr th q) in
         add_meta th td (if c then meta_cl else meta)
@@ -169,7 +165,6 @@ let load_driver = let driver_tag = ref (-1) in fun env file ->
     drv_filename  = !filename;
     drv_transform = !transform;
     drv_thprelude = !thprelude;
-    drv_syntax    = !syntax;
     drv_meta      = !meta;
     drv_meta_cl   = !meta_cl;
     drv_regexps   = !regexps;
@@ -243,9 +238,7 @@ let print_task drv fmt task =
     | None -> raise NoPrinter
     | Some p -> p
   in
-  let printer =
-    lookup_printer p drv.drv_prelude drv.drv_thprelude drv.drv_syntax
-  in
+  let printer = lookup_printer p drv.drv_prelude drv.drv_thprelude in
   let lookup_transform t = t, lookup_transform t drv.drv_env in
   let transl = List.map lookup_transform drv.drv_transform in
   let apply task (t, tr) =

src/driver/driver_ast.ml

@@ -32,8 +32,8 @@ type metarg =
 
 type th_rule =
   | Rprelude  of string
-  | Rsyntaxts of qualid * string
-  | Rsyntaxls of qualid * string
+  | Rsyntaxts of cloned * qualid * string
+  | Rsyntaxls of cloned * qualid * string
   | Rremovepr of cloned * qualid
   | Rmeta     of cloned * string * metarg list
 

src/driver/driver_parser.mly

@@ -86,8 +86,8 @@ list0_trule:
 
 trule:
 | PRELUDE STRING                      { Rprelude  ($2) }
-| SYNTAX TYPE qualid STRING           { Rsyntaxts ($3, $4) }
-| SYNTAX LOGIC qualid STRING          { Rsyntaxls ($3, $4) }
+| SYNTAX cloned TYPE qualid STRING    { Rsyntaxts ($2, $4, $5) }
+| SYNTAX cloned LOGIC qualid STRING   { Rsyntaxls ($2, $4, $5) }
 | REMOVE cloned PROP qualid           { Rremovepr ($2, $4) }
 | META cloned ident meta_args         { Rmeta     ($2, $3, $4) }
 | META cloned STRING meta_args        { Rmeta     ($2, $3, $4) }

src/printer/alt_ergo.ml

@@ -51,7 +51,7 @@ let print_tvsymbols fmt tv =
 let forget_var v = forget_id ident_printer v.vs_name
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
   info_ac  : Sls.t;
 }
@@ -214,11 +214,11 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr syn fmt task =
+let print_task pr thpr fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
-    info_syn = syn;
+    info_syn = get_syntax_map task;
     info_rem = get_remove_set task;
     info_ac  = 
       Task.find_tagged_ls meta_ac (find_meta task meta_ac) Sls.empty }
@@ -227,9 +227,9 @@ let print_task pr thpr syn fmt task =
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "alt-ergo" 
-  (fun pr thpr syn fmt task -> 
+  (fun pr thpr fmt task ->
      forget_all ident_printer;
-     print_task pr thpr syn fmt task)
+     print_task pr thpr fmt task)
 
 (*
 let print_goal info fmt (id, f, task) =

src/printer/coq.ml

@@ -75,7 +75,7 @@ let print_pr fmt pr =
 (* info *)
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 
@@ -337,11 +337,13 @@ let print_decl info fmt d = match d.d_node with
 let print_decls info fmt dl =
   fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl info)) dl
 
-let print_task pr thpr syn fmt task =
+let print_task pr thpr fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
-  let info = { info_syn = syn; info_rem = get_remove_set task } in
+  let info = {
+    info_syn = get_syntax_map task;
+    info_rem = get_remove_set task } in
   print_decls info fmt (Task.task_decls task)
 
 let () = register_printer "coq" print_task

src/printer/gappa.ml

@@ -401,7 +401,7 @@ let print_tvsymbols fmt tv =
 let forget_var v = forget_id ident_printer v.vs_name
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 

src/printer/simplify.ml

@@ -54,7 +54,7 @@ let print_real fmt = function
       fprintf fmt "0x%s_%sp%a" i f pp_exp e
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 
@@ -178,18 +178,18 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr syn fmt task =
+let print_task pr thpr fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
-    info_syn = syn;
+    info_syn = get_syntax_map task;
     info_rem = get_remove_set task }
   in
   let decls = Task.task_decls task in
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "simplify" 
-  (fun pr thpr syn fmt task -> 
+  (fun pr thpr fmt task ->
      forget_all ident_printer;
-     print_task pr thpr syn fmt task)
+     print_task pr thpr fmt task)
 

src/printer/smt.ml

@@ -48,7 +48,7 @@ let print_var fmt {vs_name = id} =
   fprintf fmt "%s" n
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 
@@ -203,14 +203,14 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr syn fmt task = 
+let print_task pr thpr fmt task =
   fprintf fmt "(benchmark why3@\n" 
     (*print_ident (Task.task_goal task).pr_name*);
   fprintf fmt "  :status unknown@\n";
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
-    info_syn = syn;
+    info_syn = get_syntax_map task;
     info_rem = get_remove_set task }
   in
   let decls = Task.task_decls task in
@@ -218,6 +218,6 @@ let print_task pr thpr syn fmt task =
   fprintf fmt "@\n)@."
 
 let () = register_printer "smtv1" 
-  (fun pr thpr syn fmt task -> 
+  (fun pr thpr fmt task ->
      forget_all ident_printer;
-     print_task pr thpr syn fmt task)
+     print_task pr thpr fmt task)

src/printer/tptp.ml

@@ -50,7 +50,7 @@ let print_var fmt {vs_name = id} =
 let forget_var v = forget_id ident_printer v.vs_name
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 
@@ -151,18 +151,18 @@ let print_decl info fmt d = match d.d_node with
 
 let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
 
-let print_task pr thpr syn fmt task =
+let print_task pr thpr fmt task =
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
   let info = {
-    info_syn = syn;
+    info_syn = get_syntax_map task;
     info_rem = get_remove_set task }
   in
   let decls = Task.task_decls task in
   ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
 
 let () = register_printer "tptp" 
-  (fun pr thpr syn fmt task -> 
+  (fun pr thpr fmt task ->
      forget_all ident_printer;
-     print_task pr thpr syn fmt task)
+     print_task pr thpr fmt task)
 

src/printer/why3.ml

@@ -89,7 +89,7 @@ let print_pr fmt pr =
 (* info *)
 
 type info = {
-  info_syn : syntax_map;
+  info_syn : string Mid.t;
   info_rem : Sid.t;
 }
 
@@ -391,11 +391,13 @@ let print_tdecl fmt td = match td.td_node with
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
         m.meta_name (print_list comma print_meta_arg) al
 
-let print_task pr thpr syn fmt task =
+let print_task pr thpr fmt task =
   forget_all ();
   print_prelude fmt pr;
   print_th_prelude task fmt thpr;
-  info := { info_syn = syn; info_rem = get_remove_set task };
+  info := {
+    info_syn = get_syntax_map task;
+    info_rem = get_remove_set task };
   fprintf fmt "@[<hov 2>theory Task@\n%a@]@\nend@."
     (print_list nothing print_tdecl) (Task.task_tdecls task)
 

src/transform/eliminate_definition.ml

@@ -42,8 +42,8 @@ let elim q d = match d.d_node with
       ld @ id
   | _ -> [d]
 
-let eliminate_builtin = Trans.on_meta Printer.meta_remove_logic (fun tds ->
-  let rem_ls = Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty in
+let eliminate_builtin = Trans.on_meta Printer.meta_syntax_logic (fun tds ->
+  let rem_ls = Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty in
   Trans.decl (elim rem_ls) None)
 
 let () = Trans.register_transform "eliminate_builtin" eliminate_builtin

src/transform/encoding_decorate_mono.ml

@@ -267,8 +267,8 @@ let decl tenv d =
   res
 *)
 
-let t env = Trans.on_meta Printer.meta_remove_logic (fun tds ->
-  let rem_ls = Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty in
+let t env = Trans.on_meta Printer.meta_syntax_logic (fun tds ->
+  let rem_ls = Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty in
   let init_task,tenv = load_prelude rem_ls env in
   Trans.tdecl (decl tenv) init_task)
 

src/transform/filter_trigger.ml

@@ -79,9 +79,9 @@ let keep_no_builtin rem_ls = function
 
   
 let filter_trigger_builtin =
-  Trans.on_meta Printer.meta_remove_logic (fun tds ->
+  Trans.on_meta Printer.meta_syntax_logic (fun tds ->
     let rem_ls = 
-       Task.find_tagged_ls Printer.meta_remove_logic tds Sls.empty
+       Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty
     in
     let rt,rf = make_rt_rf (keep_no_builtin rem_ls) in
     Trans.rewrite rt rf None)