-let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
- let module MQ = MetadataQuery in
- let module CTC = CicTypeChecker in
- (* no idea why ocaml wants this *)
- let parsed_text_length = String.length parsed_text in
- let dbd = LibraryDb.instance () in
- let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:true in
- match mac with
- (* WHELP's stuff *)
- | TA.WMatch (loc, term) ->
- let l = Whelp.match_term ~dbd term in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WInstance (loc, term) ->
- let l = Whelp.instance ~dbd term in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WLocate (loc, s) ->
- let l = Whelp.locate ~dbd s in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WElim (loc, term) ->
- let uri =
- match term with
- | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None
- | _ -> failwith "Not a MutInd"
- in
- let l = Whelp.elim ~dbd uri in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- | TA.WHint (loc, term) ->
- let _subst = [] in
- let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
- let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let entry = `Whelp (pp_macro [] [] mac, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], "", parsed_text_length
- (* REAL macro *)
- | TA.Hint (loc, rewrite) ->
- 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
- 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
- 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.Eval (_, kind, term) ->
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context =
- match user_goal with
- None -> []
- | Some n -> GrafiteTypes.get_proof_context grafite_status n in
- let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let term =
- match kind with
- | `Normalize ->
- CicReduction.normalize ~delta:true ~subst:[] context term
- | `Simpl ->
- ProofEngineReduction.simpl context term
- | `Unfold None ->
- ProofEngineReduction.unfold ?what:None context term
- | `Unfold (Some lazy_term) ->
- let what, _, _ =
- lazy_term context metasenv CicUniv.empty_ugraph in
- ProofEngineReduction.unfold ~what context term
- | `Whd ->
- CicReduction.whd ~delta:true ~subst:[] context term
- in
- let t_and_ty = Cic.Cast (term,ty) in
- guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [(grafite_status#set_proof_status No_proof), parsed_text ],"",
- parsed_text_length
- | TA.Check (_,term) ->
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context =
- match user_goal with
- None -> []
- | Some n -> GrafiteTypes.get_proof_context grafite_status n in
- let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let t_and_ty = Cic.Cast (term,ty) in
- guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [], "", 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
- ~automation_cache:grafite_status#automation_cache)
- 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'
- [] [] proof_term CicUniv.empty_ugraph
- in
- prerr_endline (CicPp.ppterm proof_term ^ " n lambda= " ^ string_of_int how_many_lambdas);
- (* use declarative output *)
- let obj =
- (* il proof_term vive in cc, devo metterci i lambda no? *)
- (Cic.CurrentProof ("xxx",[],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 [] obj
- else
- if true then
- (* use cic2grafite *)
- cic2grafite cc menv proof_term
- else
- (* alternative using FG stuff *)
- let map_unicode_to_tex =
- Helm_registry.get_bool "matita.paste_unicode_as_tex"
- in
- ApplyTransformation.procedural_txt_of_cic_term
- ~map_unicode_to_tex 78 [] cc proof_term
- 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 (_, suri, params) ->
- let str = "\n\n" ^
- ApplyTransformation.txt_of_inline_macro
- ~map_unicode_to_tex:(Helm_registry.get_bool
- "matita.paste_unicode_as_tex")
- params suri
- in
- [], str, String.length parsed_text
-
-and eval_executable include_paths (buffer : GText.buffer) guistuff
-grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
-script ex loc