* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
open GrafiteTypes
(** raised when one of the script margins (top or bottom) is reached *)
exception Margin
+exception NoUnfinishedProof
+exception ActionCancelled
let safe_substring s i j =
try String.sub s i j with Invalid_argument _ -> assert false
parsed_text st
=
let module TAPp = GrafiteAstPp in
- let include_ =
- match guistuff.filenamedata with
- | None,None -> []
- | None,Some devel -> [MatitamakeLib.root_for_development devel ]
- | Some f,_ ->
- match MatitamakeLib.development_for_dir (Filename.dirname f) with
- | None -> []
- | Some devel -> [MatitamakeLib.root_for_development devel ]
- in
- let include_ =
- include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
- in
let parsed_text_length = String.length parsed_text in
- let loc, ex =
- match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
let initial_space,parsed_text =
try
let pieces = Pcre.extract ~rex:heading_nl_RE' parsed_text in
let inital_space,new_grafite_status,new_lexicon_status,new_status_and_text_list' =
(* the code commented out adds the "select" command if needed *)
initial_space,grafite_status,lexicon_status,[] in
-(* match grafite_status.proof_status with
+(* let loc, ex =
+ match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in
+ match grafite_status.proof_status with
| Incomplete_proof { stack = stack }
when not (List.mem user_goal (Continuationals.head_goals stack)) ->
let grafite_status =
in
res,parsed_text_length
-let eval_with_engine
- guistuff lexicon_status grafite_status user_goal parsed_text st
-=
- try
- eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text
- st
+let wrap_with_developments guistuff f arg =
+ try
+ f arg
with
| DependenciesParser.UnableToInclude what
+ | LexiconEngine.IncludedFileNotCompiled what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
- let target = what in
+ let target = Pcre.replace ~pat:"lexicon$" ~templ:"moo" what in
let refresh_cb () =
while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
in
if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
raise exc
else
- eval_with_engine guistuff lexicon_status grafite_status user_goal
- parsed_text st
+ f arg
in
- let do_nothing () = [], 0 in
+ let do_nothing () = raise ActionCancelled in
let handle_with_devel d =
let name = MatitamakeLib.name_for_development d in
let title = "Unable to include " ^ what in
| None -> handle_without_devel (Some f)
| 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 eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text st
+=
+ wrap_with_developments guistuff
+ (eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text) st
+;;
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 include_paths (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 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
+ 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 include_paths 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";
assert false)
| 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 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.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 include_paths (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 context =
+ match user_goal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context grafite_status n in
+ let grafite_status,macro = lazy_macro context in
+ eval_macro include_paths buffer guistuff lexicon_status grafite_status
+ user_goal unparsed_text parsed_text script macro
+
+and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
grafite_status user_goal script statement
=
let (lexicon_status,st), unparsed_text =
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
- GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
- ~include_paths:(Helm_registry.get_list
- Helm_registry.string "matita.includes")
- lexicon_status, text
+ let ast =
+ wrap_with_developments guistuff
+ (GrafiteParser.parse_statement
+ (Ulexing.from_utf8_string text) ~include_paths) lexicon_status
+ in
+ ast, text
| `Ast (st, text) -> (lexicon_status, st), text
in
let text_of_loc loc =
let s = String.sub unparsed_text parsed_text_length remain_len in
let s,len =
try
- eval_statement buffer guistuff lexicon_status grafite_status user_goal
- script (`Raw s)
+ eval_statement include_paths buffer guistuff lexicon_status
+ grafite_status user_goal script (`Raw s)
with
HExtlib.Localized (floc, exn) ->
HExtlib.raise_localized_exception ~offset:parsed_text_length floc exn
(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 include_paths buffer guistuff lexicon_status
+ grafite_status user_goal unparsed_text parsed_text script loc ex
let fresh_script_id =
let i = ref 0 in
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
let initial_statuses =
+ (* these include_paths are used only to load the initial notation *)
let include_paths =
Helm_registry.get_list Helm_registry.string "matita.includes" in
let lexicon_status =
grafite_status,lexicon_status
in
object (self)
+ val mutable include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes"
+
val scriptId = fresh_script_id ()
val guistuff = {
* Invariant: this list length is 1 + length of statements *)
(** goal as seen by the user (i.e. metano corresponding to current tab) *)
- val mutable userGoal = ~-1
+ val mutable userGoal = None
(** text mark and tag representing locked part of a script *)
val locked_mark =
method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false
method private _advance ?statement () =
- let rec aux st =
- let (entries, parsed_len) =
- eval_statement buffer guistuff self#lexicon_status self#grafite_status
- userGoal self st
- in
- let new_statuses, new_statements =
- let statuses, texts = List.split entries in
- statuses, texts
- in
- history <- new_statuses @ history;
- statements <- new_statements @ statements;
- let start = buffer#get_iter_at_mark (`MARK locked_mark) in
- let new_text = String.concat "" (List.rev new_statements) in
- if statement <> None then
- buffer#insert ~iter:start new_text
- else begin
- let s = match st with `Raw s | `Ast (_, s) -> s in
- if new_text <> String.sub s 0 parsed_len then begin
- buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
- buffer#insert ~iter:start new_text;
- end;
- end;
- self#moveMark (String.length new_text)
- in
- let s = match statement with Some s -> s | None -> self#getFuture in
- HLog.debug ("evaluating: " ^ first_line s ^ " ...");
- (try aux (`Raw s) with End_of_file -> raise Margin)
+ let s = match statement with Some s -> s | None -> self#getFuture in
+ HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let (entries, parsed_len) =
+ try
+ eval_statement include_paths buffer guistuff self#lexicon_status
+ self#grafite_status userGoal self (`Raw s)
+ with End_of_file -> raise Margin
+ in
+ let new_statuses, new_statements =
+ let statuses, texts = List.split entries in
+ statuses, texts
+ in
+ history <- new_statuses @ history;
+ statements <- new_statements @ statements;
+ let start = buffer#get_iter_at_mark (`MARK locked_mark) in
+ let new_text = String.concat "" (List.rev new_statements) in
+ if statement <> None then
+ buffer#insert ~iter:start new_text
+ else begin
+ if new_text <> String.sub s 0 parsed_len then begin
+ buffer#delete ~start ~stop:(start#copy#forward_chars parsed_len);
+ buffer#insert ~iter:start new_text;
+ end;
+ end;
+ self#moveMark (String.length new_text);
+ (* here we need to set the Goal in case we are going to cursor (or to
+ bottom) and we will face a macro *)
+ match self#grafite_status.proof_status with
+ Incomplete_proof p ->
+ userGoal <-
+ (try Some (Continuationals.Stack.find_goal p.stack)
+ with Failure _ -> None)
+ | _ -> userGoal <- None
method private _retract offset lexicon_status grafite_status new_statements
new_history
method assignFileName file =
let abspath = MatitaMisc.absolute_path file in
- let devel = MatitamakeLib.development_for_dir (Filename.dirname abspath) in
- guistuff.filenamedata <- Some abspath, devel
+ let dirname = Filename.dirname abspath in
+ let devel = MatitamakeLib.development_for_dir dirname in
+ guistuff.filenamedata <- Some abspath, devel;
+ let include_ =
+ match MatitamakeLib.development_for_dir dirname with
+ None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel] in
+ let include_ =
+ include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+ in
+ include_paths <- include_
method saveToFile () =
let oc = open_out self#getFilename in
method private reset_buffer =
statements <- [];
history <- [ initial_statuses ];
- userGoal <- ~-1;
+ userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
method template () =
let template = HExtlib.input_file BuildTimeConf.script_template in
buffer#insert ~iter:(buffer#get_iter `START) template;
- guistuff.filenamedata <-
- (None,MatitamakeLib.development_for_dir (Unix.getcwd ()));
- buffer#set_modified false;
- set_star (Filename.basename self#ppFilename) false
+ let development = MatitamakeLib.development_for_dir (Unix.getcwd ()) in
+ guistuff.filenamedata <- (None,development);
+ let include_ =
+ match development with
+ None -> []
+ | Some devel -> [MatitamakeLib.root_for_development devel ]
+ in
+ let include_ =
+ include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+ in
+ include_paths <- include_ ;
+ buffer#set_modified false;
+ set_star (Filename.basename self#ppFilename) false
method goto (pos: [`Top | `Bottom | `Cursor]) () =
let old_locked_mark =
(* method proofStatus = MatitaTypes.get_proof_status self#status *)
method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status
+
method proofContext =
- GrafiteTypes.get_proof_context self#grafite_status userGoal
+ match userGoal with
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
+
method proofConclusion =
- GrafiteTypes.get_proof_conclusion self#grafite_status userGoal
+ match userGoal with
+ None -> assert false
+ | Some n ->
+ GrafiteTypes.get_proof_conclusion self#grafite_status n
+
method stack = GrafiteTypes.get_stack self#grafite_status
method setGoal n = userGoal <- n
method goal = userGoal
method eos =
let s = self#getFuture in
- let rec is_there_and_executable lexicon_status s =
+ let rec is_there_only_comments lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
let lexicon_status,st =
GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
- ~include_paths:(Helm_registry.get_list
- Helm_registry.string "matita.includes")
- lexicon_status
+ ~include_paths lexicon_status
in
match st with
- GrafiteParser.LNone loc
| GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) ->
let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
let remain_len = String.length s - parsed_text_length in
let next = String.sub s parsed_text_length remain_len in
- is_there_and_executable lexicon_status next
- | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false
+ is_there_only_comments lexicon_status next
+ | GrafiteParser.LNone _
+ | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
in
try
- is_there_and_executable self#lexicon_status s
+ is_there_only_comments self#lexicon_status s
with
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
projects / helm.git / blobdiff