X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2FmatitaScript.ml;h=fca45c02628132a700ef92bcf3fd913da19e40f1;hb=f0cfb75e23d0c1c403c8a67b47be931980f5419f;hp=f6610911f5ac2ebcb450bde106c46a616ef2fa0b;hpb=8e24e39aed25a2c31fb7073308ee3f0b80c206e6;p=helm.git diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml index f6610911f..fca45c026 100644 --- a/matita/matitaScript.ml +++ b/matita/matitaScript.ml @@ -402,14 +402,20 @@ let cic2grafite context menv t = let pres_term = TermContentPres.pp_ast content_term in let dummy_tbl = Hashtbl.create 1 in let markup = CicNotationPres.render dummy_tbl pres_term in - let s = "(" ^ BoxPp.render_to_string List.hd width markup ^ ")" in + let s = "(" ^ BoxPp.render_to_string + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + List.hd width markup ^ ")" in Pcre.substitute ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s in CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in - GrafiteAstPp.pp_statement ~term_pp ~lazy_term_pp ~obj_pp t + GrafiteAstPp.pp_statement + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~term_pp ~lazy_term_pp ~obj_pp t in let script = String.concat "" (List.map pp ast) in prerr_endline script; @@ -433,7 +439,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in TAPp.pp_macro ~term_pp:(fun x -> - ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)) + ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex")) in match mac with (* WHELP's stuff *) @@ -490,7 +498,10 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status TA.Dot loc))) in let text = comment parsed_text ^ "\n" ^ - pp_eager_statement_ast (ast HExtlib.dummy_floc) in + pp_eager_statement_ast (ast HExtlib.dummy_floc) + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + in let text_len = MatitaGtkMisc.utf8_string_length text in let loc = HExtlib.floc_of_loc (0,text_len) in let statement = `Ast (GrafiteParser.LSome (ast loc),text) in @@ -541,38 +552,73 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status CicMetaSubst.apply_subst subst (Cic.Meta (i,irl)) in let time = Unix.gettimeofday () -. timestamp in - let text = - comment parsed_text ^ "\n" ^ - cic2grafite cc menv proof_term ^ - (Printf.sprintf "\n(* end auto proof: %4.2f *)" time) - in - (* alternative using FG stuff - let proof_term = - Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc + let size, depth = Auto.size_and_depth cc menv proof_term in + let trailer = + Printf.sprintf + "\n(* end auto(%s) proof: TIME=%4.2f SIZE=%d DEPTH=%d *)" + Auto.revision time size depth in - let ty,_ = - CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph + let proof_script = + if List.exists (fun (s,_) -> s = "paramodulation") params then + let proof_term, how_many_lambdas = + Auto.lambda_close ~prefix_name:"orrible_hack_" + proof_term menv cc + in + let ty,_ = + CicTypeChecker.type_of_aux' + menv [] proof_term CicUniv.empty_ugraph + in + prerr_endline (CicPp.ppterm proof_term); + (* use declarative output *) + let obj = + (* il proof_term vive in cc, devo metterci i lambda no? *) + (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[])) + in + ApplyTransformation.txt_of_cic_object + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~skip_thm_and_qed:true + ~skip_initial_lambdas:how_many_lambdas + 80 GrafiteAst.Declarative "" obj + else + if true then + (* use cic2grafite *) + cic2grafite cc menv proof_term + else + (* alternative using FG stuff *) + let proof_term, how_many_lambdas = + Auto.lambda_close ~prefix_name:"orrible_hack_" + proof_term menv cc + in + let ty,_ = + CicTypeChecker.type_of_aux' + menv [] proof_term CicUniv.empty_ugraph + in + let obj = + Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) + in + Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" + (strip_comments + (ApplyTransformation.txt_of_cic_object + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + ~skip_thm_and_qed:true + ~skip_initial_lambdas:how_many_lambdas + 80 (GrafiteAst.Procedural None) "" obj)) in - let obj = - Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) - in - let text = - comment parsed_text ^ - Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" - (strip_comments - (ApplyTransformation.txt_of_cic_object - ~map_unicode_to_tex:false - ~skip_thm_and_qed:true - ~skip_initial_lambdas:true - 80 (GrafiteAst.Procedural None) "" obj)) ^ - "(* end auto proof *)" - in - *) + let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in [],text,parsed_text_length with - ProofEngineTypes.Fail _ -> [], comment parsed_text, parsed_text_length) + ProofEngineTypes.Fail _ as exn -> + raise exn + (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *)) | TA.Inline (_,style,suri,prefix) -> - let str = ApplyTransformation.txt_of_inline_macro style suri prefix in + let str = + ApplyTransformation.txt_of_inline_macro + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") + style suri prefix + in [], str, String.length parsed_text and eval_executable include_paths (buffer : GText.buffer) guistuff @@ -588,7 +634,7 @@ script ex loc | TA.Command (_,TA.Set (_,"baseuri",u)) -> if Http_getter_storage.is_read_only u then raise (ActionCancelled ("baseuri " ^ u ^ " is readonly")); - if not (Http_getter_storage.is_empty u) then + if not (Http_getter_storage.is_empty ~local:true u) then (match guistuff.ask_confirmation ~title:"Baseuri redefinition"