ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
}
-let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal
+let eval_with_engine include_paths guistuff grafite_status user_goal
skipped_txt nonskipped_txt st
=
- let module TAPp = GrafiteAstPp in
- let module DTE = DisambiguateTypes.Environment in
let parsed_text_length =
String.length skipped_txt + String.length nonskipped_txt
in
let enriched_history_fragment =
MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
"matita.do_heavy_checks")
- lexicon_status grafite_status (text,prefix_len,st)
+ grafite_status (text,prefix_len,st)
in
let enriched_history_fragment = List.rev enriched_history_fragment in
(* really fragile *)
* so that we can ensure the inclusion is performed after the included file
* is compiled (if needed). matitac does not need that, since it compiles files
* in the good order, here files may be compiled on demand. *)
-let wrap_with_make include_paths (f : GrafiteParser.statement) x =
+let wrap_with_make include_paths (f : #LexiconEngine.status GrafiteParser.statement) x =
try
f ~never_include:true ~include_paths x
with
| Cic.Const _ as t ->
PT.Ident (pp_t c t, None)
| Cic.Appl l -> PT.Appl (List.map (aux c) l)
- | Cic.Implicit _ -> PT.Implicit
+ | Cic.Implicit _ -> PT.Implicit `JustOne
| Cic.Lambda (Cic.Name n, s, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Decl s)::c) t)
| Cic.LetIn (Cic.Name n, s, ty, t) ->
PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
- | Cic.Meta _ -> PT.Implicit
+ | Cic.Meta _ -> PT.Implicit `JustOne
| Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
| Cic.Sort Cic.Set -> PT.Sort `Set
| Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
prerr_endline script;
stupid_indenter script
;;
+let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
+ let parsed_text_length = String.length parsed_text in
+ match mac with
+ | TA.Screenshot (_,name) ->
+ let status = script#grafite_status in
+ let _,_,menv,subst,_ = status#obj in
+ let name = Filename.dirname (script#filename) ^ "/" ^ name in
+ let sequents =
+ let selected = Continuationals.Stack.head_goals status#stack in
+ List.filter (fun x,_ -> List.mem x selected) menv
+ in
+ guistuff.mathviewer#screenshot status sequents menv subst name;
+ [status, parsed_text], "", parsed_text_length
+ | TA.NCheck (_,t) ->
+ let status = script#grafite_status in
+ let _,_,menv,subst,_ = status#obj in
+ let ctx =
+ try let _,(_,ctx,_) = List.hd menv in ctx
+ with Failure "hd" -> []
+ in
+ let m, s, status, t =
+ GrafiteDisambiguate.disambiguate_nterm
+ None status ctx menv subst (parsed_text,parsed_text_length,
+ CicNotationPt.Cast (t,CicNotationPt.Implicit `JustOne))
+ (* XXX use the metasenv, if possible *)
+ in
+ guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
+ [status, parsed_text], "", parsed_text_length
+ | TA.NIntroGuess _loc ->
+ let names_ref = ref [] in
+ let s =
+ NTactics.intros_tac ~names_ref [] script#grafite_status
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ "#" ^ String.concat " " !names_ref ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_loc, (None,a)) ->
+ let trace_ref = ref [] in
+ let s =
+ NnAuto.auto_tac
+ ~params:(None,a) ~trace_ref script#grafite_status
+ in
+ let depth =
+ try List.assoc "depth" a
+ with Not_found -> ""
+ in
+ let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+ let thms =
+ match !trace_ref with
+ | [] -> "{}"
+ | thms ->
+ String.concat ", "
+ (HExtlib.filter_map (function
+ | CicNotationPt.NRef r -> Some (NCicPp.r2s true r)
+ | _ -> None)
+ thms)
+ in
+ let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+ let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+ [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+ | TA.NAutoInteractive (_, (Some _,_)) -> assert false
-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 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 MDB = LibraryDb in
let module CTC = CicTypeChecker in
- let module CU = CicUniv 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
+ let pp_macro = ApplyTransformation.txt_of_macro ~map_unicode_to_tex:false in
match mac with
(* WHELP's stuff *)
| TA.WMatch (loc, term) ->
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
+ eval_statement include_paths buffer guistuff
grafite_status user_goal script statement
in
(* we need to replace all the parsed_text *)
in
let t_and_ty = Cic.Cast (term,ty) in
guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
- [({grafite_status with proof_status = No_proof},lexicon_status), parsed_text ],"",
+ [(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 (_,menv,subst,_,_,_), _ =
ProofEngineTypes.apply_tactic
(Auto.auto_tac ~dbd ~params
- ~automation_cache:grafite_status.GrafiteTypes.automation_cache)
+ ~automation_cache:grafite_status#automation_cache)
proof_status
in
let proof_term =
in
let ty,_ =
CicTypeChecker.type_of_aux'
- menv [] proof_term CicUniv.empty_ugraph
+ [] [] proof_term CicUniv.empty_ugraph
in
- prerr_endline (CicPp.ppterm proof_term);
+ 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",menv,proof_term,ty,[],[]))
+ (Cic.CurrentProof ("xxx",[],proof_term,ty,[],[]))
in
ApplyTransformation.txt_of_cic_object
~map_unicode_to_tex:(Helm_registry.get_bool
[], str, String.length parsed_text
and eval_executable include_paths (buffer : GText.buffer) guistuff
-lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
+grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
script ex loc
=
- let module TAPp = GrafiteAstPp in
- let module MD = MultiPassDisambiguator in
- let module ML = MatitaMisc in
try
ignore (buffer#move_mark (`NAME "beginning_of_statement")
~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
(Glib.Utf8.length skipped_txt))) ;
eval_with_engine include_paths
- guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
+ guistuff grafite_status user_goal skipped_txt nonskipped_txt
(TA.Executable (loc, ex))
with
MatitaTypes.Cancel -> [], "", 0
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
+ eval_macro include_paths buffer guistuff grafite_status
user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+ | GrafiteEngine.NMacro (_loc,macro) ->
+ eval_nmacro include_paths buffer guistuff grafite_status
+ user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
+
-and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
+and eval_statement include_paths (buffer : GText.buffer) guistuff
grafite_status user_goal script statement
=
- let (lexicon_status,st), unparsed_text =
+ let (grafite_status,st), unparsed_text =
match statement with
| `Raw text ->
if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
let ast =
wrap_with_make include_paths
- (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status
+ (GrafiteParser.parse_statement (Ulexing.from_utf8_string text))
+ grafite_status
in
ast, text
- | `Ast (st, text) -> (lexicon_status, st), text
+ | `Ast (st, text) -> (grafite_status, st), text
in
let text_of_loc floc =
let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
match st with
| GrafiteParser.LNone loc ->
let parsed_text, _, _, parsed_text_length = text_of_loc loc in
- [(grafite_status,lexicon_status),parsed_text],"",
+ [grafite_status,parsed_text],"",
parsed_text_length
+ | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
+ let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
+ eval_executable include_paths buffer guistuff
+ grafite_status user_goal unparsed_text skipped nonskipped script ex loc
+ | GrafiteParser.LSome (GrafiteAst.Comment (loc, GrafiteAst.Code (_, ex)))
+ when Helm_registry.get_bool "matita.execcomments" ->
+ let _, nonskipped, skipped, parsed_text_length = text_of_loc loc in
+ eval_executable include_paths buffer guistuff
+ grafite_status user_goal unparsed_text skipped nonskipped script ex loc
| 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,text,len =
try
- eval_statement include_paths buffer guistuff lexicon_status
+ eval_statement include_paths buffer guistuff
grafite_status user_goal script (`Raw s)
with
HExtlib.Localized (floc, exn) ->
| (statuses,text)::tl ->
(statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
| [] -> [], "", 0)
- | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
- let _, nonskipped, skipped, parsed_text_length =
- text_of_loc loc
- in
- eval_executable include_paths buffer guistuff lexicon_status
- grafite_status user_goal unparsed_text skipped nonskipped script ex loc
let fresh_script_id =
let i = ref 0 in
fun () -> incr i; !i
-class script ~(source_view: GSourceView.source_view)
+class script ~(source_view: GSourceView2.source_view)
~(mathviewer: MatitaTypes.mathViewer)
~set_star
~ask_confirmation
() =
let buffer = source_view#buffer in
let source_buffer = source_view#source_buffer in
-let initial_statuses baseuri =
+let initial_statuses current baseuri =
+ let empty_lstatus = new LexiconEngine.status in
+ (match current with
+ Some current ->
+ LexiconSync.time_travel ~present:current ~past:empty_lstatus;
+ GrafiteSync.time_travel ~present:current ();
+ (* CSC: there is a known bug in invalidation; temporary fix here *)
+ NCicEnvironment.invalidate ()
+ | None -> ());
let lexicon_status =
- CicNotation2.load_notation ~include_paths:[]
+ CicNotation2.load_notation ~include_paths:[] empty_lstatus
BuildTimeConf.core_notation_script
in
let grafite_status = GrafiteSync.init lexicon_status baseuri in
- grafite_status,lexicon_status
+ grafite_status
in
let read_include_paths file =
try
val mutable statements = [] (** executed statements *)
- val mutable history = [ initial_statuses default_buri ]
+ val mutable history = [ initial_statuses None default_buri ]
(** 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.
(* history can't be empty, the invariant above grant that it contains at
* 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 grafite_status = match history with s::_ -> s | _ -> assert false
method private _advance ?statement () =
let s = match statement with Some s -> s | None -> self#getFuture in
if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
HLog.debug ("evaluating: " ^ first_line s ^ " ...");
+ let time1 = Unix.gettimeofday () in
let entries, newtext, parsed_len =
try
- eval_statement self#include_paths buffer guistuff self#lexicon_status
+ eval_statement self#include_paths buffer guistuff
self#grafite_status userGoal self (`Raw s)
with End_of_file -> raise Margin
in
+ let time2 = Unix.gettimeofday () in
+ HLog.debug ("... done in " ^ string_of_float (time2 -. time1) ^ "s");
let new_statuses, new_statements =
let statuses, texts = List.split entries in
statuses, texts
buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
(* 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
+ 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
+ method private _retract offset grafite_status new_statements
new_history
=
- let cur_grafite_status,cur_lexicon_status =
+ let cur_grafite_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;
+ LexiconSync.time_travel ~present:cur_grafite_status ~past:grafite_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,(grafite_status,lexicon_status) =
+ let cmp,new_statements,new_history,grafite_status =
match statements,history with
stat::statements, _::(status::_ as history) ->
assert (Glib.Utf8.validate stat);
| [],[_] -> raise Margin
| _,_ -> assert false
in
- self#_retract cmp lexicon_status grafite_status new_statements
+ self#_retract cmp grafite_status new_statements
new_history;
self#notify
with
val mutable observers = []
- method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) =
+ method addObserver (o: GrafiteTypes.status -> unit) =
observers <- o :: observers
method private notify =
- let lexicon_status = self#lexicon_status in
let grafite_status = self#grafite_status in
- List.iter (fun o -> o lexicon_status grafite_status) observers
+ List.iter (fun o -> o grafite_status) observers
method loadFromString s =
buffer#set_text s;
| Some f -> Some (Librarian.absolutize f)
| None -> None
in
- self#goto_top;
filename_ <- file;
include_paths_ <-
(match file with Some file -> read_include_paths file | None -> []);
HLog.debug ("backup " ^ f ^ " saved")
end
- method private goto_top =
- let grafite_status,lexicon_status =
- let rec last x = function
- | [] -> x
- | hd::tl -> last hd tl
- in
- last (self#grafite_status,self#lexicon_status) history
- in
- (* FIXME: this is not correct since there is no undo for
- * library_objects.set_default... *)
- 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 <- [ initial_statuses self#buri_of_current_file ];
+ history <- [ initial_statuses (Some self#grafite_status) self#buri_of_current_file ];
userGoal <- None;
self#notify;
buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
match pos with
| `Top ->
dispose_old_locked_mark ();
- self#goto_top;
self#reset_buffer;
self#notify
| `Bottom ->
in
let rec back_until_cursor len = (* go backward until locked < cursor *)
function
- statements, ((grafite_status,lexicon_status)::_ as history)
+ statements, ((grafite_status)::_ as history)
when len <= 0 ->
- self#_retract (icmp - len) lexicon_status grafite_status statements
+ self#_retract (icmp - len) grafite_status statements
history
| statement::tl1, _::tl2 ->
back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2)
HLog.error "The script is too big!\n"
method onGoingProof () =
- match self#grafite_status.proof_status with
+ match self#grafite_status#proof_status with
| No_proof | Proof _ -> false
| Incomplete_proof _ -> true
| Intermediate _ -> assert false
| GrafiteParser.LNone _
| GrafiteParser.LSome (GrafiteAst.Executable _) -> false
in
- try
- is_there_only_comments self#lexicon_status self#getFuture
+ try is_there_only_comments self#grafite_status self#getFuture
with
| LexiconEngine.IncludedFileNotCompiled _
| HExtlib.Localized _
projects / helm.git / blobdiff