Discriminate: provide direct get_syntax_map

src/transform/discriminate.ml

@@ -367,21 +367,30 @@ let () =
     discriminate_if_poly
     ~desc:"Same@ as@ discriminate@ but@ only@ if@ polymorphism@ appear."
 
-let on_lsinst fn =
-  let add_ls acc = function
+let li_add_ls acc = function
   | [MAls ls; MAls nls] -> Mls.add nls ls acc
-    | _ -> assert false in
+  | _ -> assert false
+
+let get_lsinst task =
+  Task.on_meta meta_lsinst li_add_ls Mls.empty task
+
+let on_lsinst fn =
   Trans.on_meta meta_lsinst (fun dls ->
-    fn (List.fold_left add_ls Mls.empty dls))
+    fn (List.fold_left li_add_ls Mls.empty dls))
 
-let on_syntax_map fn =
-  let add_ls sm0 sm = function
+let sm_add_ls sm0 sm = function
   | [MAls ls; MAls nls] ->
       begin match Mid.find_opt ls.ls_name sm0 with
         | Some s -> Mid.add nls.ls_name s sm
         | None -> sm
       end
-    | _ -> assert false in
+  | _ -> assert false
+
+let get_syntax_map task =
+  let sm0 = Printer.get_syntax_map task in
+  Task.on_meta meta_lsinst (sm_add_ls sm0) sm0 task
+
+let on_syntax_map fn =
   Printer.on_syntax_map (fun sm0 ->
   Trans.on_meta meta_lsinst (fun dls ->
-    fn (List.fold_left (fun sm dl -> add_ls sm0 sm dl) sm0 dls)))
+    fn (List.fold_left (sm_add_ls sm0) sm0 dls)))

src/transform/discriminate.mli

@@ -23,5 +23,8 @@ val ft_select_inst   : (Env.env,Ty.Sty.t) Trans.flag_trans
 val ft_select_lskept : (Env.env,Term.Sls.t) Trans.flag_trans
 val ft_select_lsinst : (Env.env,Lsmap.t) Trans.flag_trans
 
+val get_lsinst : Task.task -> Term.lsymbol Term.Mls.t
+val get_syntax_map : Task.task -> Printer.syntax_map
+
 val on_lsinst : (Term.lsymbol Term.Mls.t -> 'a Trans.trans) -> 'a Trans.trans
 val on_syntax_map : (Printer.syntax_map -> 'a Trans.trans) -> 'a Trans.trans