| Some d -> handle_with_devel d
;;
-let disambiguate_macro_term term lexicon_status grafite_status user_goal =
- let module MD = GrafiteDisambiguator in
- let dbd = LibraryDb.instance () in
- let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
- let context = GrafiteTypes.get_proof_context grafite_status user_goal in
- let interps =
- MD.disambiguate_term ~dbd ~context ~metasenv
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in
- match interps with
- | [_,_,x,_], _ -> x
- | _ -> assert false
-
let pp_eager_statement_ast =
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-let eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
+let rec eval_macro (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
let module TAPp = GrafiteAstPp in
let module MQ = MetadataQuery in
let module MDB = LibraryDb in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
- let term =
- disambiguate_macro_term term lexicon_status grafite_status user_goal in
- let l = Whelp.match_term ~dbd term in
- let query_url =
- MatitaMisc.strip_suffix ~suffix:"."
- (HExtlib.trim_blanks unparsed_text)
- in
- let entry = `Whelp (query_url, l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], parsed_text_length
+ let l = Whelp.match_term ~dbd term in
+ let query_url =
+ MatitaMisc.strip_suffix ~suffix:"."
+ (HExtlib.trim_blanks unparsed_text)
+ in
+ let entry = `Whelp (query_url, l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
| TA.WInstance (loc, term) ->
- let term =
- disambiguate_macro_term term lexicon_status grafite_status user_goal in
- let l = Whelp.instance ~dbd term in
- let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], parsed_text_length
+ let l = Whelp.instance ~dbd term in
+ let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), 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 (TA.WLocate (loc, s)), l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], parsed_text_length
+ let l = Whelp.locate ~dbd s in
+ let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
| TA.WElim (loc, term) ->
- let term =
- disambiguate_macro_term term lexicon_status grafite_status user_goal in
- 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 (TA.WElim (loc, term)), l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], parsed_text_length
+ 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 (TA.WElim (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
| TA.WHint (loc, term) ->
- let term =
- disambiguate_macro_term term lexicon_status grafite_status user_goal in
- let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
- let l = List.map fst (MQ.experimental_hint ~dbd s) in
- let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
- guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
- [], parsed_text_length
+ let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
+ let l = List.map fst (MQ.experimental_hint ~dbd s) in
+ let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
+ guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
+ [], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
let proof = GrafiteTypes.get_current_proof grafite_status in
- let proof_status = proof, user_goal 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 =
+ let ast loc =
TA.Executable (loc, (TA.Tactical (loc,
TA.Tactic (loc,
TA.Apply (loc, CicNotationPt.Uri (suri, None))),
- Some (TA.Dot loc))))
+ Some (TA.Dot loc)))) in
+ let text =
+ comment parsed_text ^ "\n" ^
+ pp_eager_statement_ast (ast HExtlib.dummy_floc) in
+ let text_len = 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 buffer guistuff lexicon_status grafite_status
+ user_goal script statement
in
-(*
- let new_lexicon_status,new_grafite_status =
- MatitaEngine.eval_ast lexicon_status grafite_status ast in
- let extra_text =
- comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
- [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
- parsed_text_length
-*) assert false (* implementarla con una ricorsione *)
+ (* 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";
| TA.Check (_,term) ->
let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
let context = GrafiteTypes.get_proof_context grafite_status user_goal in
- let interps =
- GrafiteDisambiguator.disambiguate_term ~dbd ~context ~metasenv
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) term in
- let _, metasenv , term, ugraph =
- match interps with
- | [x], _ -> x
- | _ -> assert false
- in
- let ty,_ = CTC.type_of_aux' metasenv context term ugraph 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.Abort _ ->
- let rec go_back () =
- let grafite_status = script#grafite_status.proof_status in
- match status with
- | No_proof -> ()
- | _ -> script#retract ();go_back()
- in
- [], parsed_text_length, Some go_back
- | TA.Redo (_, Some i) -> [], parsed_text_length,
- Some (fun () -> for j = 1 to i do advance () done)
- | TA.Redo (_, None) -> [], parsed_text_length,
- Some (fun () -> advance ())
- | TA.Undo (_, Some i) -> [], parsed_text_length,
- Some (fun () -> for j = 1 to i do script#retract () done)
- | TA.Undo (_, None) -> [], parsed_text_length,
- Some (fun () -> script#retract ()) *)
(* TODO *)
| TA.Quit _ -> failwith "not implemented"
| TA.Print (_,kind) -> failwith "not implemented"
| TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
| TA.Search_term (_, search_kind, term) -> failwith "not implemented"
-let eval_executable guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script ex
+and eval_executable (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script loc ex
=
- let module TAPp = GrafiteAstPp in
- let module MD = GrafiteDisambiguator in
- let module ML = MatitaMisc in
- match ex with
- TA.Tactical (loc, _, _) ->
- eval_with_engine
- guistuff lexicon_status grafite_status user_goal parsed_text
- (TA.Executable (loc, ex))
- | TA.Command (loc, cmd) ->
- (try
- begin
- match cmd with
- | TA.Set (loc',"baseuri",u) ->
- if not (GrafiteMisc.is_empty u) then
- (match
- guistuff.ask_confirmation
- ~title:"Baseuri redefinition"
- ~message:(
- "Baseuri " ^ u ^ " already exists.\n" ^
- "Do you want to redefine the corresponding "^
- "part of the library?")
- with
- | `YES ->
- let basedir = Helm_registry.get "matita.basedir" in
- LibraryClean.clean_baseuris ~basedir [u]
- | `NO -> ()
- | `CANCEL -> raise MatitaTypes.Cancel)
- | _ -> ()
- end;
- eval_with_engine
- guistuff lexicon_status grafite_status user_goal parsed_text
- (TA.Executable (loc, ex))
- with MatitaTypes.Cancel -> [], 0)
- | TA.Macro (_,mac) ->
- eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text
- parsed_text script mac
-
-let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
+ let module TAPp = GrafiteAstPp in
+ let module MD = GrafiteDisambiguator in
+ let module ML = MatitaMisc in
+ try
+ begin
+ match ex with
+ | TA.Command (_,TA.Set (_,"baseuri",u)) ->
+ if not (GrafiteMisc.is_empty u) then
+ (match
+ guistuff.ask_confirmation
+ ~title:"Baseuri redefinition"
+ ~message:(
+ "Baseuri " ^ u ^ " already exists.\n" ^
+ "Do you want to redefine the corresponding "^
+ "part of the library?")
+ with
+ | `YES ->
+ let basedir = Helm_registry.get "matita.basedir" in
+ LibraryClean.clean_baseuris ~basedir [u]
+ | `NO -> ()
+ | `CANCEL -> raise MatitaTypes.Cancel)
+ | _ -> ()
+ end;
+ eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text
+ (TA.Executable (loc, ex))
+ with
+ MatitaTypes.Cancel -> [], 0
+ | GrafiteEngine.Macro (_loc,lazy_macro) ->
+ let grafite_status,macro = lazy_macro user_goal in
+ eval_macro buffer guistuff lexicon_status grafite_status user_goal
+ unparsed_text parsed_text script macro
+
+and eval_statement (buffer : GText.buffer) guistuff lexicon_status
grafite_status user_goal script statement
=
let (lexicon_status,st), unparsed_text =
(statuses,parsed_text ^ text)::tl,parsed_text_length + len
| [] -> [], 0)
| GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
- let parsed_text, parsed_text_length = text_of_loc loc in
- eval_executable guistuff lexicon_status grafite_status user_goal
- unparsed_text parsed_text script ex
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ eval_executable buffer guistuff lexicon_status grafite_status user_goal
+ unparsed_text parsed_text script loc ex
let fresh_script_id =
let i = ref 0 in
exception Drop
exception IncludedFileNotCompiled of string (* file name *)
+(* the integer is expected to be the goal the user is currently seeing *)
+exception Macro of
+ GrafiteAst.loc * (int -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
type options = {
do_heavy_checks: bool ;
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
?do_heavy_checks:bool ->
?clean_baseuri:bool ->
GrafiteTypes.status ->
'obj GrafiteAst.command ->
GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ disambiguate_macro:
+ (GrafiteTypes.status ->
+ 'term GrafiteAst.macro ->
+ int -> GrafiteTypes.status * Cic.term GrafiteAst.macro) ->
+
options ->
GrafiteTypes.status ->
('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code ->
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},uris
| _ -> status,uris
-} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status ex ->
match ex with
| GrafiteAst.Tactical (_, tac, None) ->
eval_tactical ~disambiguate_tactic status tac,[]
eval_tactical ~disambiguate_tactic status punct,[]
| GrafiteAst.Command (_, cmd) ->
eval_command.ec_go ~disambiguate_command opts status cmd
- | GrafiteAst.Macro (_, mac) ->
-(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
- raise (Command_error
- (Printf.sprintf "The macro %s can't be in a script"
- (GrafiteAstPp.pp_macro_ast mac)))
-*) assert false
+ | GrafiteAst.Macro (loc, macro) ->
+ raise (Macro (loc,disambiguate_macro status macro))
} and eval_from_moo = {efm_go = fun status fname ->
let ast_of_cmd cmd =
eval_ast.ea_go
~disambiguate_tactic:(fun status _ tactic -> status,tactic)
~disambiguate_command:(fun status cmd -> status,cmd)
+ ~disambiguate_macro:(fun _ _ -> assert false)
status ast
in
assert (lemmas=[]);
status)
status moo
-} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
- st
+} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status st
->
let opts = {
do_heavy_checks = do_heavy_checks ;
in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~disambiguate_tactic
- ~disambiguate_command opts status ex
+ eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
+ ~disambiguate_macro opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c,[]
}
projects / helm.git / commitdiff