(** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
let goal_ast n =
let module A = GrafiteAst in
- let loc = DisambiguateTypes.dummy_floc in
+ let loc = HExtlib.dummy_floc in
A.Executable (loc, A.Tactical (loc,
A.Tactic (loc, A.Goal (loc, n)),
Some (A.Dot loc)))
mutable filenamedata: string option * MatitamakeLib.development option
}
-let eval_with_engine guistuff status user_goal parsed_text st =
+let eval_with_engine guistuff lexicon_status grafite_status user_goal
+ parsed_text st
+=
let module TAPp = GrafiteAstPp in
let include_ =
match guistuff.filenamedata with
pieces.(1), pieces.(2)
with
Not_found -> "", parsed_text in
- (* we add the goal command if needed *)
- let inital_space,new_status,new_status_and_text_list' =
- match status.proof_status with
-(* | Incomplete_proof { stack = stack }
+ 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
+ | Incomplete_proof { stack = stack }
when not (List.mem user_goal (Continuationals.head_goals stack)) ->
- let status =
+ let grafite_status =
MatitaEngine.eval_ast
- ~do_heavy_checks:true status (goal_ast user_goal)
+ ~do_heavy_checks:true grafite_status (goal_ast user_goal)
in
let initial_space = if initial_space = "" then "\n" else initial_space
in
- "\n", status,
- [ status,
- initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ] *)
- | _ -> initial_space,status,[] in
- let new_status =
- GrafiteEngine.eval_ast
- ~baseuri_of_script:(GrafiteParserMisc.baseuri_of_script ~include_paths:include_)
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- ~do_heavy_checks:true new_status st
+ "\n", grafite_status,
+ [ grafite_status,
+ initial_space ^ TAPp.pp_tactical (TA.Select (loc, [user_goal])) ]
+ | _ -> initial_space,grafite_status,[] in *)
+ let new_lexicon_status,new_grafite_status =
+ MatitaEngine.eval_ast ~do_heavy_checks:true
+ new_lexicon_status new_grafite_status st
in
let new_aliases =
- match ex with
- | TA.Command (_, TA.Alias _)
- | TA.Command (_, TA.Include _)
- | TA.Command (_, TA.Interpretation _) -> []
- | _ -> MatitaSync.alias_diff ~from:status new_status
- in
+ LexiconSync.alias_diff ~from:lexicon_status new_lexicon_status in
(* we remove the defined object since we consider them "automatic aliases" *)
let dummy_st =
- TA.Comment (DisambiguateTypes.dummy_floc,
- TA.Note (DisambiguateTypes.dummy_floc, ""))
+ TA.Comment (HExtlib.dummy_floc, TA.Note (HExtlib.dummy_floc, ""))
in
- let initial_space,status,new_status_and_text_list_rev =
+ let initial_space,lexicon_status,new_status_and_text_list_rev =
let module DTE = DisambiguateTypes.Environment in
let module UM = UriManager in
- let baseuri = GrafiteTypes.get_string_option new_status "baseuri" in
+ let baseuri = GrafiteTypes.get_string_option new_grafite_status "baseuri" in
List.fold_left (
- fun (initial_space,status,acc) (k,((v,_) as value)) ->
+ fun (initial_space,lexicon_status,acc) (k,((v,_) as value)) ->
let b =
try
UM.buri_of_uri (UM.uri_of_string v) = baseuri
UriManager.IllFormedUri _ -> false (* v is a description, not a URI *)
in
if b then
- initial_space,status,acc
+ initial_space,lexicon_status,acc
else
let new_text =
let initial_space =
DisambiguatePp.pp_environment
(DisambiguateTypes.Environment.add k value
DisambiguateTypes.Environment.empty) in
- let new_status =
- MatitaSync.set_proof_aliases status [k,value]
+ let new_lexicon_status =
+ LexiconEngine.set_proof_aliases lexicon_status [k,value]
in
- "\n",new_status,((new_status, (new_text, dummy_st))::acc)
- ) (initial_space,status,[]) new_aliases in
+ "\n",new_lexicon_status,(((new_grafite_status,new_lexicon_status), (new_text, Some dummy_st))::acc)
+ ) (initial_space,lexicon_status,[]) new_aliases in
let parsed_text = initial_space ^ parsed_text in
let res =
List.rev new_status_and_text_list_rev @ new_status_and_text_list' @
- [new_status, (parsed_text, st)]
+ [(new_grafite_status,new_lexicon_status),(parsed_text, Some st)]
in
res,parsed_text_length
-let eval_with_engine guistuff status user_goal parsed_text st =
+let eval_with_engine
+ guistuff lexicon_status grafite_status user_goal parsed_text st
+=
try
- eval_with_engine guistuff status user_goal parsed_text st
+ eval_with_engine guistuff lexicon_status grafite_status user_goal parsed_text
+ st
with
- | GrafiteParserMisc.UnableToInclude what
+ | DependenciesParser.UnableToInclude what
| GrafiteEngine.IncludedFileNotCompiled what as exc ->
let compile_needed_and_go_on d =
let target = what in
if not(MatitamakeLib.build_development_in_bg ~target refresh_cb d) then
raise exc
else
- eval_with_engine guistuff status user_goal parsed_text st
+ eval_with_engine guistuff lexicon_status grafite_status user_goal
+ parsed_text st
in
let do_nothing () = [], 0 in
let handle_with_devel d =
| Some d -> handle_with_devel d
;;
-let disambiguate_macro_term term status user_goal =
- let module MD = MatitaDisambiguator in
+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 status in
- let context = GrafiteTypes.get_proof_context status user_goal 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:status.aliases
- ~universe:(Some status.multi_aliases) term in
+ 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
GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
-let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
+let eval_macro 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 status user_goal in
+ 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:"."
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WInstance (loc, term) ->
- let term = disambiguate_macro_term term status user_goal in
+ 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;
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WElim (loc, term) ->
- let term = disambiguate_macro_term term status user_goal in
+ 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
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], parsed_text_length
| TA.WHint (loc, term) ->
- let term = disambiguate_macro_term term status user_goal in
+ 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
[], parsed_text_length
(* REAL macro *)
| TA.Hint loc ->
- let proof = GrafiteTypes.get_current_proof status 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
TA.Apply (loc, CicNotationPt.Uri (suri, None))),
Some (TA.Dot loc))))
in
- let new_status =
- GrafiteEngine.eval_ast
- ~baseuri_of_script:(fun _ -> assert false)
- ~disambiguate_tactic:GrafiteDisambiguate.disambiguate_tactic
- ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
- status ast 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_status , (extra_text, ast) ], parsed_text_length
+ [ (new_grafite_status,new_lexicon_status), (extra_text, Some ast) ],
+ parsed_text_length
| _ ->
HLog.error
"The result of the urichooser should be only 1 uri, not:\n";
) selected;
assert false)
| TA.Check (_,term) ->
- let metasenv = GrafiteTypes.get_proof_metasenv status in
- let context = GrafiteTypes.get_proof_context status user_goal in
+ let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
+ let context = GrafiteTypes.get_proof_context grafite_status user_goal in
let interps =
- MatitaDisambiguator.disambiguate_term ~dbd ~context ~metasenv
- ~aliases:status.aliases ~universe:(Some status.multi_aliases) term
- in
+ 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
[], parsed_text_length
(* | TA.Abort _ ->
let rec go_back () =
- let status = script#status.proof_status in
+ let grafite_status = script#grafite_status.proof_status in
match status with
| No_proof -> ()
| _ -> script#retract ();go_back()
| TA.Search_pat (_, search_kind, str) -> failwith "not implemented"
| TA.Search_term (_, search_kind, term) -> failwith "not implemented"
-let eval_executable guistuff status user_goal unparsed_text parsed_text script
- ex
+let eval_executable guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script ex
=
let module TAPp = GrafiteAstPp in
- let module MD = MatitaDisambiguator in
+ let module MD = GrafiteDisambiguator in
let module ML = MatitaMisc in
match ex with
- | TA.Command (loc, _) | TA.Tactical (loc, _, _) ->
- (try
- (match GrafiteParserMisc.baseuri_of_baseuri_decl (TA.Executable (loc,ex)) with
- | None -> ()
- | Some u ->
+ 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
+ (match
guistuff.ask_confirmation
~title:"Baseuri redefinition"
~message:(
"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);
- eval_with_engine
- guistuff status user_goal parsed_text (TA.Executable (loc, ex))
- with MatitaTypes.Cancel -> [], 0)
+ | `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 status user_goal unparsed_text parsed_text script mac
+ eval_macro guistuff lexicon_status grafite_status user_goal unparsed_text
+ parsed_text script mac
-let rec eval_statement (buffer : GText.buffer) guistuff status user_goal
- script statement
+let rec eval_statement (buffer : GText.buffer) guistuff lexicon_status
+ grafite_status user_goal script statement
=
- let st, unparsed_text =
+ 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), text
- | `Ast (st, text) -> st, text
+ GrafiteParser.parse_statement (Ulexing.from_utf8_string text)
+ ~include_paths:(Helm_registry.get_list
+ Helm_registry.string "matita.includes")
+ lexicon_status, text
+ | `Ast (st, text) -> (lexicon_status, st), text
in
let text_of_loc loc =
let parsed_text_length = snd (HExtlib.loc_of_floc loc) in
parsed_text, parsed_text_length
in
match st with
- | GrafiteAst.Comment (loc, _) ->
+ | GrafiteParser.LNone loc ->
+ let parsed_text, parsed_text_length = text_of_loc loc in
+ [(grafite_status,lexicon_status),(parsed_text,None)],
+ parsed_text_length
+ | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) ->
let parsed_text, parsed_text_length = text_of_loc loc in
let remain_len = String.length unparsed_text - parsed_text_length in
let s = String.sub unparsed_text parsed_text_length remain_len in
let s,len =
try
- eval_statement buffer guistuff status user_goal script
- (`Raw s)
+ eval_statement 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
- | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
+ | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
raise
- (MatitaDisambiguator.DisambiguationError
+ (GrafiteDisambiguator.DisambiguationError
(offset+parsed_text_length, errorll))
in
(match s with
- | (status, (text, ast)) :: tl ->
- ((status, (parsed_text ^ text, ast))::tl), (parsed_text_length + len)
+ | (statuses,(text, ast)) :: tl ->
+ (statuses,(parsed_text ^ text, ast))::tl,
+ parsed_text_length + len
| [] -> [], 0)
- | GrafiteAst.Executable (loc, ex) ->
+ | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
let parsed_text, parsed_text_length = text_of_loc loc in
- eval_executable guistuff status user_goal unparsed_text parsed_text
- script ex
+ eval_executable guistuff lexicon_status grafite_status user_goal
+ unparsed_text parsed_text script 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 =
+ let include_paths =
+ Helm_registry.get_list Helm_registry.string "matita.includes" in
+ let lexicon_status =
+ CicNotation2.load_notation ~include_paths
+ BuildTimeConf.core_notation_script in
+ let grafite_status = GrafiteSync.init () in
+ grafite_status,lexicon_status
+in
object (self)
val scriptId = fresh_script_id ()
ignore (buffer#connect#modified_changed
(fun _ -> set_star (Filename.basename self#ppFilename) buffer#modified))
- val mutable statements = []; (** executed statements *)
- val mutable history = [ MatitaSync.init () ];
+ val mutable statements = [] (** executed statements *)
+
+ val mutable history = [ initial_statuses ]
(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.
method error_tag = error_tag
(* history can't be empty, the invariant above grant that it contains at
- * least the init status *)
- method status = match history with hd :: _ -> hd | _ -> assert false
+ * least the init grafite_status *)
+ method grafite_status = match history with (s,_)::_ -> s | _ -> assert false
+ 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#status userGoal self st
+ eval_statement buffer guistuff self#lexicon_status self#grafite_status
+ userGoal self st
in
let (new_statuses, new_statements, new_asts) =
let statuses, statements = List.split entries in
buffer#insert ~iter:start new_text;
end;
end;
- self#moveMark (String.length new_text);
- (*
- (match List.rev new_asts with (* advance again on punctuation *)
- | TA.Executable (_, TA.Tactical (_, tac, _)) :: _ ->
- let baseoffset =
- (buffer#get_iter_at_mark (`MARK locked_mark))#offset
- in
- let text = self#getFuture in
- (try
- (match parse_statement baseoffset 0 buffer text with
- | TA.Executable (loc, TA.Tactical (_, tac, None)) as st
- when GrafiteAst.is_punctuation tac ->
- let len = snd (CicNotationPt.loc_of_floc loc) in
- aux (`Ast (st, String.sub text 0 len))
- | _ -> ())
- with CicNotationParser.Parse_error _ | End_of_file -> ())
- | _ -> ())
- *)
+ 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)
- method private _retract offset status new_statements new_history =
- let cur_status = match history with s::_ -> s | [] -> assert false in
- MatitaSync.time_travel ~present:cur_status ~past:status;
+ method private _retract offset lexicon_status grafite_status new_statements
+ new_history
+ =
+ let cur_grafite_status,cur_lexicon_status =
+ match history with s::_ -> s | [] -> assert false
+ in
+ LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status;
+ GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
statements <- new_statements;
history <- new_history;
self#moveMark (- offset)
method retract () =
try
- let cmp,new_statements,new_history,status =
+ let cmp,new_statements,new_history,(grafite_status,lexicon_status) =
match statements,history with
stat::statements, _::(status::_ as history) ->
String.length stat, statements, history, status
| [],[_] -> raise Margin
| _,_ -> assert false
in
- self#_retract cmp status new_statements new_history;
+ self#_retract cmp lexicon_status grafite_status new_statements
+ new_history;
self#notify
with
| Margin -> self#notify
val mutable observers = []
- method addObserver (o: GrafiteTypes.status -> unit) =
+ method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) =
observers <- o :: observers
method private notify =
- let status = self#status in
- List.iter (fun o -> o status) observers
+ let lexicon_status = self#lexicon_status in
+ let grafite_status = self#grafite_status in
+ List.iter (fun o -> o lexicon_status grafite_status) observers
method loadFromFile f =
buffer#set_text (HExtlib.input_file f);
end
method private goto_top =
- let init =
+ let grafite_status,lexicon_status =
let rec last x = function
| [] -> x
| hd::tl -> last hd tl
in
- last self#status history
+ last (self#grafite_status,self#lexicon_status) history
in
(* FIXME: this is not correct since there is no undo for
* library_objects.set_default... *)
- MatitaSync.time_travel ~present:self#status ~past:init
+ GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
+ LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
method private reset_buffer =
statements <- [];
- history <- [ MatitaSync.init () ];
+ history <- [ initial_statuses ];
userGoal <- ~-1;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
in
let rec back_until_cursor len = (* go backward until locked < cursor *)
function
- statements, (status::_ as history) when len <= 0 ->
- self#_retract (icmp - len) status statements history
+ statements, ((grafite_status,lexicon_status)::_ as history)
+ when len <= 0 ->
+ self#_retract (icmp - len) lexicon_status grafite_status statements
+ history
| statement::tl1, _::tl2 ->
back_until_cursor (len - String.length statement) (tl1,tl2)
| _,_ -> assert false
self#notify; raise exc)
method onGoingProof () =
- match self#status.proof_status with
+ match self#grafite_status.proof_status with
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
(* method proofStatus = MatitaTypes.get_proof_status self#status *)
- method proofMetasenv = GrafiteTypes.get_proof_metasenv self#status
- method proofContext = GrafiteTypes.get_proof_context self#status userGoal
- method proofConclusion= GrafiteTypes.get_proof_conclusion self#status userGoal
- method stack = GrafiteTypes.get_stack self#status
+ method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status
+ method proofContext =
+ GrafiteTypes.get_proof_context self#grafite_status userGoal
+ method proofConclusion =
+ GrafiteTypes.get_proof_conclusion self#grafite_status userGoal
+ 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 s =
+ let rec is_there_and_executable lexicon_status s =
if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
- let st = GrafiteParser.parse_statement (Ulexing.from_utf8_string s) in
+ 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
+ in
match st with
- | GrafiteAst.Comment (loc,_)->
+ 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 next
- | GrafiteAst.Executable (loc, ex) -> false
+ is_there_and_executable lexicon_status next
+ | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) -> false
in
try
- is_there_and_executable s
+ is_there_and_executable self#lexicon_status s
with
| CicNotationParser.Parse_error _ -> false
| Margin | End_of_file -> true
projects / helm.git / commitdiff