(* $Id$ *)
-module G = GrafiteAst
+module UM = UriManager
+module C = Cic
+module Un = CicUniv
+module E = CicEnvironment
+module TC = CicTypeChecker
+module G = GrafiteAst
let mpres_document pres_box =
Xml.add_xml_declaration (CicNotationPres.print_box pres_box)
remove_closed_substs s
let txt_of_cic_object
- ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas n style prefix obj
+ ~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
+ n style ?flavour prefix obj
=
let get_aobj obj =
try
Cic2acic.acic_object_of_cic_object obj
in
aobj, ids_to_inner_sorts, ids_to_inner_types
- with e ->
- let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
- failwith msg
+ with
+ | E.Object_not_found uri ->
+ let msg = "txt_of_cic_object: object not found: " ^ UM.string_of_uri uri in
+ failwith msg
+ | e ->
+ let msg = "txt_of_cic_object: " ^ Printexc.to_string e in
+ failwith msg
in
match style with
| G.Declarative ->
(CicNotationPres.mpres_of_box bobj)
)
| G.Procedural depth ->
- let obj = ProceduralOptimizer.optimize_obj obj in
+ let obj = ProceduralOptimizer.optimize_obj obj in
let aobj, ids_to_inner_sorts, ids_to_inner_types = get_aobj obj in
let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
let lazy_term_pp = term_pp in
let aux = GrafiteAstPp.pp_statement
~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
let script =
- Acic2Procedural.acic2procedural
+ Acic2Procedural.procedural_of_acic_object
~ids_to_inner_sorts ~ids_to_inner_types
- ?depth ?skip_thm_and_qed prefix aobj
+ ?depth ?flavour prefix aobj
in
"\n\n" ^ String.concat "" (List.map aux script)
-let txt_of_inline_uri ~map_unicode_to_tex style suri prefix =
+let cic_prefix = Str.regexp_string "cic:/"
+
+let matita_prefix = Str.regexp_string "cic:/matita/"
+
+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
+ UM.uri_of_string s
+
+let txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri =
let print_exc = function
| ProofEngineHelpers.Bad_pattern s as e ->
Printexc.to_string e ^ " " ^ Lazy.force s
let dbd = LibraryDb.instance () in
let sorted_uris = MetadataDeps.sorted_uris_of_baseuri ~dbd suri in
let map uri =
- try
- txt_of_cic_object
- ~map_unicode_to_tex 78 style prefix
- (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+ try
+(* FG: for now the explicit variables must be discharged *)
+ let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
+ match CicDischarge.discharge_uri (discharge_uri style) uri with
+ | C.InductiveDefinition _ as obj', false ->
+ let uri' = discharge_uri style uri in
+ TC.typecheck_obj uri' obj';
+ (* we loose the sharing in this case *)
+ let obj'', _ = E.get_obj Un.default_ugraph uri' in
+ let s = do_it obj'' in begin E.remove_obj uri'; s end
+ | obj, _ -> do_it obj
with
| e ->
- Printf.sprintf "\n(* ERRORE IN STAMPA DI %s\nEXCEPTION: %s *)\n"
- (UriManager.string_of_uri uri) (print_exc e)
+ let msg =
+ Printf.sprintf
+ "ERROR IN THE GENERATION OF %s\nEXCEPTION: %s"
+ (UM.string_of_uri uri) (print_exc e)
+ in
+ Printf.eprintf "%s\n" msg;
+ GrafiteTypes.command_error msg
in
String.concat "" (List.map map sorted_uris)
-let txt_of_inline_macro ~map_unicode_to_tex style name prefix =
+let txt_of_inline_macro ~map_unicode_to_tex style ?flavour prefix name =
let suri =
if Librarian.is_uri name then name else
let include_paths =
let _, baseuri, _, _ =
Librarian.baseuri_of_script ~include_paths name
in
- baseuri
+ baseuri ^ "/"
in
- txt_of_inline_uri ~map_unicode_to_tex style suri prefix
-
-
+ txt_of_inline_uri ~map_unicode_to_tex style ?flavour prefix suri
+
+(****************************************************************************)
+(* procedural_txt_of_cic_term *)
+
+let procedural_txt_of_cic_term ~map_unicode_to_tex n ?depth context term =
+ let annterm, ids_to_inner_sorts, ids_to_inner_types =
+ try Cic2acic.acic_term_of_cic_term context term
+ with e ->
+ let msg = "procedural_txt_of_cic_term: " ^ Printexc.to_string e in
+ failwith msg
+ in
+ let term_pp = term2pres ~map_unicode_to_tex (n - 8) ids_to_inner_sorts in
+ let lazy_term_pp = term_pp in
+ let obj_pp = CicNotationPp.pp_obj term_pp in
+ let aux = GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
+ let script =
+ Acic2Procedural.procedural_of_acic_term
+ ~ids_to_inner_sorts ~ids_to_inner_types ?depth "" context annterm
+ in
+ String.concat "" (List.map aux script)
projects / helm.git / blobdiff