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;
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 *)
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
(* REAL macro *)
- | TA.Hint loc ->
+ | TA.Hint (loc, rewrite) ->
let user_goal' =
match user_goal with
Some n -> n
in
let proof = GrafiteTypes.get_current_proof grafite_status in
let proof_status = proof,user_goal' in
- let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
- let selected = guistuff.urichooser l in
- (match selected with
- | [] -> [], "", parsed_text_length
- | [uri] ->
- let suri = UriManager.string_of_uri uri in
- let ast loc =
- TA.Executable (loc, (TA.Tactic (loc,
- Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
- TA.Dot loc))) in
- let text =
- comment parsed_text ^ "\n" ^
- pp_eager_statement_ast (ast HExtlib.dummy_floc) 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
- let res,_,_parsed_text_len =
- eval_statement include_paths buffer guistuff lexicon_status
- grafite_status user_goal script statement
- in
- (* we need to replace all the parsed_text *)
- res,"",String.length parsed_text
- | _ ->
- HLog.error
- "The result of the urichooser should be only 1 uri, not:\n";
- List.iter (
- fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
- ) selected;
- assert false)
+ if rewrite then
+ let l = MQ.equations_for_goal ~dbd proof_status in
+ let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
+ let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], "", parsed_text_length
+ else
+ let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
+ let selected = guistuff.urichooser l in
+ (match selected with
+ | [] -> [], "", parsed_text_length
+ | [uri] ->
+ let suri = UriManager.string_of_uri uri in
+ let ast loc =
+ TA.Executable (loc, (TA.Tactic (loc,
+ Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+ TA.Dot loc))) in
+ let text =
+ comment parsed_text ^ "\n" ^
+ 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
+ let res,_,_parsed_text_len =
+ eval_statement include_paths buffer guistuff lexicon_status
+ grafite_status user_goal script statement
+ in
+ (* we need to replace all the parsed_text *)
+ res,"",String.length parsed_text
+ | _ ->
+ HLog.error
+ "The result of the urichooser should be only 1 uri, not:\n";
+ List.iter (
+ fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
+ ) selected;
+ assert false)
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let context =
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)
+ 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
- (* alternative using FG stuff
- let proof_term =
- Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc
+ 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 ty,_ =
- CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph
- 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
| 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"