+ let stm_pp =
+ GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp
+ in
+ let aux = function
+ | G.Executable (_, G.Command (_, G.Obj (_, N.Inductive _))) as stm
+ ->
+ enable_notations false;
+ let str = stm_pp stm in enable_notations true; str
+(* FG: we disable notation for Inductive to avoid recursive notation *)
+ | stm -> stm_pp stm
+ in
+ let script =
+ Acic2Procedural.procedural_of_acic_object
+ ~ids_to_inner_sorts ~ids_to_inner_types ~info
+ ?depth ?flavour prefix aobj
+ in
+ String.concat "" (List.map aux script) ^ "\n\n"
+
+let cic_prefix = Str.regexp_string "cic:/"
+let matita_prefix = Str.regexp_string "cic:/matita/"
+let suffixes = [".ind"; "_rec.con"; "_rect.con"; "_ind.con"; ".con"]
+
+let replacements =
+ let map s = String.length s, s, Str.regexp_string s, "_discharged" ^ s in
+ List.map map suffixes
+
+let replacement (ok, u) (l, s, x, t) =
+ if ok then ok, u else
+ if Str.last_chars u l = s then true, Str.replace_first x t u else ok, u
+
+let discharge_uri style uri =
+ let template = match style with
+ | G.Declarative -> "cic:/matita/declarative/"
+ | G.Procedural _ -> "cic:/matita/procedural/"
+ in
+ let s = UM.string_of_uri uri in
+ if Str.string_match matita_prefix s 0 then uri else
+ let s = Str.replace_first cic_prefix template s in
+ let _, s = List.fold_left replacement (false, s) replacements in
+ UM.uri_of_string s
+
+let discharge_name s = s ^ "_discharged"