X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FapplyTransformation.ml;h=f58f4dae2e1cba819e7eb1795df1d74d136b8a5b;hb=e053aaf3085a079c3125ed4666ba648a48fbb2af;hp=150ec8de07c5d454ff7781e800ba1e9cb53ac89b;hpb=7782637e13656ec7d1d0ccc84e0d8cf894431187;p=helm.git diff --git a/helm/software/matita/applyTransformation.ml b/helm/software/matita/applyTransformation.ml index 150ec8de0..f58f4dae2 100644 --- a/helm/software/matita/applyTransformation.ml +++ b/helm/software/matita/applyTransformation.ml @@ -35,7 +35,12 @@ (* $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) @@ -161,7 +166,8 @@ let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm = 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 @@ -169,9 +175,13 @@ let txt_of_cic_object 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 -> @@ -190,7 +200,7 @@ let txt_of_cic_object (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 @@ -198,13 +208,27 @@ let txt_of_cic_object 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 @@ -213,18 +237,30 @@ let txt_of_inline_uri ~map_unicode_to_tex style suri prefix = 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 = @@ -233,8 +269,27 @@ let txt_of_inline_macro ~map_unicode_to_tex style name prefix = 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)