+ [], "", parsed_text_length
+ | TA.AutoInteractive (_, params) ->
+ let user_goal' =
+ match user_goal with
+ Some n -> n
+ | None -> raise NoUnfinishedProof
+ in
+ let proof = GrafiteTypes.get_current_proof grafite_status in
+ let proof_status = proof,user_goal' in
+ (try
+ let _,menv,_,_,_,_ = proof in
+ let i,cc,ty = CicUtil.lookup_meta user_goal' menv in
+ let timestamp = Unix.gettimeofday () in
+ let (_,menv,subst,_,_,_), _ =
+ ProofEngineTypes.apply_tactic
+ (Auto.auto_tac ~dbd ~params
+ ~universe:grafite_status.GrafiteTypes.universe) proof_status
+ in
+ let proof_term =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable cc
+ in
+ CicMetaSubst.apply_subst subst (Cic.Meta (i,irl))
+ in
+ let time = Unix.gettimeofday () -. timestamp in
+ 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 proof_script =
+ if List.exists (fun (s,_) -> s = "paramodulation") (snd 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 text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
+ [],text,parsed_text_length
+ with
+ 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
+ ~map_unicode_to_tex:(Helm_registry.get_bool
+ "matita.paste_unicode_as_tex")
+ style suri prefix
+ in
+ [], str, String.length parsed_text