(* $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)
in
let content_sequent = Acic2content.map_sequent asequent in
let pres_sequent =
- (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
- in
+ Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
let xmlpres = mpres_document pres_sequent in
(Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
unsh_sequent,
(ids_to_terms, ids_to_father_ids, ids_to_conjectures, ids_to_hypotheses,
ids_to_inner_sorts,ids_to_inner_types)))
-let txt_of_cic_sequent ?map_unicode_to_tex size metasenv sequent =
+let txt_of_cic_sequent ~map_unicode_to_tex size metasenv sequent =
let unsh_sequent,(asequent,ids_to_terms,
ids_to_father_ids,ids_to_inner_sorts,ids_to_hypotheses)
=
CicNotationPres.mpres_of_box
(Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
in
- BoxPp.render_to_string ?map_unicode_to_tex
+ BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size pres_sequent
-let txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv sequent =
+let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
+ metasenv sequent =
let _,(asequent,_,_,ids_to_inner_sorts,_) =
Cic2acic.asequent_of_sequent metasenv sequent
in
let _,_,_,t = Acic2content.map_sequent asequent in
- let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
+ let t, ids_to_uris =
+ TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
let t = TermContentPres.pp_ast t in
let t = CicNotationPres.render ids_to_uris t in
- BoxPp.render_to_string ?map_unicode_to_tex
+ BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size t
-let txt_of_cic_term ?map_unicode_to_tex size metasenv context t =
- let fake_sequent = (-1,context,t) in
- txt_of_cic_sequent_conclusion ?map_unicode_to_tex size metasenv fake_sequent
+let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
+ let fake_sequent = (-1,context,t) in
+ txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
+ metasenv fake_sequent
;;
ignore (
let context' = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let term' = CicMetaSubst.apply_subst subst term in
- let res = txt_of_cic_term 30 metasenv context' term' in
+ let res =
+ txt_of_cic_term
+ ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ 30 metasenv context' term' in
if String.contains res '\n' then
"\n" ^ res ^ "\n"
else
let remove_closed_substs s =
Pcre.replace ~pat:"{...}" ~templ:"" s
-let term2pres ?map_unicode_to_tex n ids_to_inner_sorts annterm =
+let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm =
let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
- in
+ TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
let bobj =
CicNotationPres.box_of_mpres (
CicNotationPres.render ~prec:90 ids_to_uris
- (TermContentPres.pp_ast ast)
- )
- in
+ (TermContentPres.pp_ast ast)) in
let render = function _::x::_ -> x | _ -> assert false in
let mpres = CicNotationPres.mpres_of_box bobj in
- let s = BoxPp.render_to_string ?map_unicode_to_tex render n mpres in
+ let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
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 ->
?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_inner_sorts cobj
in
remove_closed_substs ("\n\n" ^
- BoxPp.render_to_string ?map_unicode_to_tex
+ BoxPp.render_to_string ~map_unicode_to_tex
(function _::x::_ -> x | _ -> assert false) n
(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 (n - 8) ids_to_inner_sorts 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 ~term_pp ~lazy_term_pp ~obj_pp in
+ let aux = GrafiteAstPp.pp_statement
+ ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp in
let script =
- Acic2Procedural.acic2procedural
- ~ids_to_inner_sorts ~ids_to_inner_types ?depth ?skip_thm_and_qed prefix aobj
+ Acic2Procedural.procedural_of_acic_object
+ ~ids_to_inner_sorts ~ids_to_inner_types
+ ?depth ?flavour prefix aobj
in
- String.concat "" (List.map aux script) ^ "\n\n"
+ "\n\n" ^ String.concat "" (List.map aux script)
+
+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_macro ?map_unicode_to_tex style suri prefix =
+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 ?flavour prefix name =
+ let suri =
+ if Librarian.is_uri name then name else
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+ in
+ let _, baseuri, _, _ =
+ Librarian.baseuri_of_script ~include_paths name
+ in
+ baseuri ^ "/"
+ in
+ 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