(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://helm.cs.unibo.it/ *) (* $Id$ *) open Printf open GrafiteTypes module TA = GrafiteAst let debug = false let debug_print = if debug then prerr_endline else ignore (** raised when one of the script margins (top or bottom) is reached *) exception Margin exception NoUnfinishedProof exception ActionCancelled of string let safe_substring s i j = try String.sub s i j with Invalid_argument _ -> assert false let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*" let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)" let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$" let multiline_RE = Pcre.regexp "^\n[^\n]+$" let newline_RE = Pcre.regexp "\n" let comment_RE = Pcre.regexp "\\(\\*(.|\n)*\\*\\)\n?" ~flags:[`UNGREEDY] let comment str = if Pcre.pmatch ~rex:multiline_RE str then "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " *)" else "\n(**\n" ^ str ^ "\n*)" let strip_comments str = Pcre.qreplace ~templ:"\n" ~pat:"\n\n" (Pcre.qreplace ~rex:comment_RE str) ;; let first_line s = let s = Pcre.replace ~rex:heading_nl_RE s in try let nl_pos = String.index s '\n' in String.sub s 0 nl_pos with Not_found -> s type guistuff = { mathviewer:MatitaTypes.mathViewer; urichooser: UriManager.uri list -> UriManager.uri list; ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL]; } let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt st = let module TAPp = GrafiteAstPp in let module DTE = DisambiguateTypes.Environment in let module DP = DisambiguatePp in let parsed_text_length = String.length skipped_txt + String.length nonskipped_txt in let text = skipped_txt ^ nonskipped_txt in let prefix_len = MatitaGtkMisc.utf8_string_length skipped_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) in let enriched_history_fragment = List.rev enriched_history_fragment in (* really fragile *) let res,_ = List.fold_left (fun (acc, to_prepend) (status,alias) -> match alias with | None -> (status,to_prepend ^ nonskipped_txt)::acc,"" | Some (k,((v,_) as value)) -> let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in (status,to_prepend ^ newtxt ^ "\n")::acc, "") ([],skipped_txt) enriched_history_fragment in res,"",parsed_text_length ;; (* this function calls the parser in a way that it does not perform inclusions, * 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 = try f ~never_include:true ~include_paths x with | GrafiteParser.NoInclusionPerformed mafilename -> let root, buri, _, tgt = try Librarian.baseuri_of_script ~include_paths mafilename with Librarian.NoRootFor _ -> HLog.error ("The included file '"^mafilename^"' has no root file,"); HLog.error "please create it."; raise (Failure ("No root file for "^mafilename)) in let initial_lexicon_status = CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script in let b,x = try GrafiteSync.push (); LexiconSync.time_travel ~present:x ~past:initial_lexicon_status; let rc = MatitacLib.Make.make root [tgt] in GrafiteSync.pop (); CicNotation.reset (); ignore(CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script); let x = List.fold_left (fun s c -> LexiconEngine.eval_command s c) initial_lexicon_status (List.rev x.LexiconEngine.lexicon_content_rev) in rc,x with | exn -> HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn)); assert false in if b then try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ -> raise (Failure ("Including: "^tgt^ "\nNothing to do... did you run matitadep?")) else raise (Failure ("Compiling: " ^ tgt)) ;; let pp_eager_statement_ast = GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) (* naive implementation of procedural proof script generation, * starting from an applicatiove *auto generated) proof. * this is out of place, but I like it :-P *) let cic2grafite context menv t = (* indents a proof script in a stupid way, better than nothing *) let stupid_indenter s = let next s = let idx_square_o = try String.index s '[' with Not_found -> -1 in let idx_square_c = try String.index s ']' with Not_found -> -1 in let idx_pipe = try String.index s '|' with Not_found -> -1 in let tok = List.sort (fun (i,_) (j,_) -> compare i j) [idx_square_o,'[';idx_square_c,']';idx_pipe,'|'] in let tok = List.filter (fun (i,_) -> i <> -1) tok in match tok with | (i,c)::_ -> Some (i,c) | _ -> None in let break_apply n s = let tab = String.make (n+1) ' ' in Pcre.replace ~templ:(".\n" ^ tab ^ "apply") ~pat:"\\.apply" s in let rec ind n s = match next s with | None -> s | Some (position, char) -> try let s1, s2 = String.sub s 0 position, String.sub s (position+1) (String.length s - (position+1)) in match char with | '[' -> break_apply n s1 ^ "\n" ^ String.make (n+2) ' ' ^ "[" ^ ind (n+2) s2 | '|' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ "|" ^ ind n s2 | ']' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ "]" ^ ind (n-2) s2 | _ -> assert false with Invalid_argument err -> prerr_endline err; s in ind 0 s in let module PT = CicNotationPt in let module GA = GrafiteAst in let pp_t context t = let names = List.map (function Some (n,_) -> Some n | None -> None) context in CicPp.pp t names in let sort_of context t = try let ty,_ = CicTypeChecker.type_of_aux' menv context t CicUniv.oblivion_ugraph in let sort,_ = CicTypeChecker.type_of_aux' menv context ty CicUniv.oblivion_ugraph in match sort with | Cic.Sort Cic.Prop -> true | _ -> false with CicTypeChecker.TypeCheckerFailure _ -> HLog.error "auto proof to sript transformation error"; false in let floc = HExtlib.dummy_floc in (* minimalisti cic.term -> pt.term *) let print_term c t = let rec aux c = function | Cic.Rel _ | Cic.MutConstruct _ | Cic.MutInd _ | 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.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.Prod (Cic.Name n, s, t) -> PT.Binder (`Forall, (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.Sort (Cic.Type u) -> PT.Sort (`Type u) | Cic.Sort Cic.Set -> PT.Sort `Set | Cic.Sort Cic.CProp -> PT.Sort `CProp | Cic.Sort Cic.Prop -> PT.Sort `Prop | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None) in aux c t in (* prints an applicative proof, that is an auto proof. * don't use in the general case! *) let rec print_proof context = function | Cic.Rel _ | Cic.Const _ as t -> [GA.Executable (floc, GA.Tactic (floc, Some (GA.Apply (floc, print_term context t)), GA.Dot floc))] | Cic.Appl (he::tl) -> let tl = List.map (fun t -> t, sort_of context t) tl in let subgoals = HExtlib.filter_map (function (t,true) -> Some t | _ -> None) tl in let args = List.map (function | (t,true) -> Cic.Implicit None | (t,_) -> t) tl in if List.length subgoals > 1 then (* branch *) [GA.Executable (floc, GA.Tactic (floc, Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))), GA.Semicolon floc))] @ [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @ (HExtlib.list_concat ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] (List.map (print_proof context) subgoals)) @ [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))] else (* simple apply *) [GA.Executable (floc, GA.Tactic (floc, Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))] @ (match subgoals with | [] -> [] | [x] -> print_proof context x | _ -> assert false) | Cic.Lambda (Cic.Name n, ty, bo) -> [GA.Executable (floc, GA.Tactic (floc, Some (GA.Cut (floc, Some n, (print_term context ty))), GA.Branch floc))] @ (print_proof (Some (Cic.Name n, Cic.Decl ty)::context) bo) @ [GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] @ [GA.Executable (floc, GA.Tactic (floc, Some (GA.Assumption floc),GA.Merge floc))] | _ -> [] (* debug_print (lazy (CicPp.ppterm t)); assert false *) in (* performs a lambda closure of the proof term abstracting metas. * this is really an approximation of a closure, local subst of metas * is not kept into account *) let close_pt menv context t = let metas = CicUtil.metas_of_term t in let metas = HExtlib.list_uniq ~eq:(fun (i,_) (j,_) -> i = j) (List.sort (fun (i,_) (j,_) -> compare i j) metas) in let mk_rels_and_collapse_metas metas = let rec aux i map acc acc1 = function | [] -> acc, acc1, map | (j,_ as m)::tl -> let _,_,ty = CicUtil.lookup_meta j menv in try let n = List.assoc ty map in aux i map (Cic.Rel n :: acc) (m::acc1) tl with Not_found -> let map = (ty, i)::map in aux (i+1) map (Cic.Rel i :: acc) (m::acc1) tl in aux 1 [] [] [] metas in let rels, metas, map = mk_rels_and_collapse_metas metas in let n_lambdas = List.length map in let t = if metas = [] then t else let t = ProofEngineReduction.replace_lifting ~what:(List.map (fun (x,_) -> Cic.Meta (x,[])) metas) ~with_what:rels ~context:context ~equality:(fun _ x y -> match x,y with | Cic.Meta(i,_), Cic.Meta(j,_) when i=j -> true | _ -> false) ~where:(CicSubstitution.lift n_lambdas t) in let rec mk_lam = function | [] -> t | (ty,n)::tl -> let name = "fresh_"^ string_of_int n in Cic.Lambda (Cic.Name name, ty, mk_lam tl) in mk_lam (fst (List.fold_left (fun (l,liftno) (ty,_) -> (l @ [CicSubstitution.lift liftno ty,liftno] , liftno+1)) ([],0) map)) in t in let ast = print_proof context (close_pt menv context t) in let pp t = (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string * which will show up using the following command line: * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *) let width = max_int in let term_pp content_term = let pres_term = TermContentPres.pp_ast content_term in let dummy_tbl = Hashtbl.create 1 in let markup = CicNotationPres.render dummy_tbl pres_term in let s = "(" ^ BoxPp.render_to_string ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") List.hd width markup ^ ")" in Pcre.substitute ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s in CicNotationPp.set_pp_term term_pp; let lazy_term_pp = fun x -> assert false in let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in GrafiteAstPp.pp_statement ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") ~term_pp ~lazy_term_pp ~obj_pp t in let script = String.concat "" (List.map pp ast) in prerr_endline script; stupid_indenter script ;; 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 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 = let f t = ProofEngineReduction.replace ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false) ~what:[()] ~with_what:[Cic.Implicit None] ~where:t in let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in TAPp.pp_macro ~term_pp:(fun x -> ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x) ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex")) 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, 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 lexicon_status 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.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 ~universe:grafite_status.GrafiteTypes.universe) 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' menv [] proof_term CicUniv.empty_ugraph in prerr_endline (CicPp.ppterm proof_term); (* use declarative output *) let obj = (* il proof_term vive in cc, devo metterci i lambda no? *) (Cic.CurrentProof ("xxx",menv,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 GrafiteAst.Declarative "" obj else if true then (* use cic2grafite *) cic2grafite cc menv proof_term else (* alternative using FG stuff *) let proof_term, how_many_lambdas = Auto.lambda_close ~prefix_name:"orrible_hack_" proof_term menv cc in let ty,_ = CicTypeChecker.type_of_aux' menv [] proof_term CicUniv.empty_ugraph in let obj = Cic.Constant ("",Some proof_term, ty, [], [`Flavour `Lemma]) in Pcre.qreplace ~templ:"?" ~pat:"orrible_hack_[0-9]+" (strip_comments (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 (GrafiteAst.Procedural None) "" obj)) 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 (_,style,suri,prefix) -> let str = ApplyTransformation.txt_of_inline_macro ~map_unicode_to_tex:(Helm_registry.get_bool "matita.paste_unicode_as_tex") style suri prefix in [], 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 script ex loc = let module TAPp = GrafiteAstPp in let module MD = GrafiteDisambiguator 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 (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 (skipped_txt ^ nonskipped_txt) 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; let ast = wrap_with_make include_paths (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status in ast, text | `Ast (st, text) -> (lexicon_status, st), text in let text_of_loc floc = let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in let start, stop = HExtlib.loc_of_floc floc in let floc = HExtlib.floc_of_loc (0, start) in let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in let floc = HExtlib.floc_of_loc (0, stop) in let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in txt,nonskipped_txt,skipped_txt,len in match st with | GrafiteParser.LNone loc -> let parsed_text, _, _, parsed_text_length = text_of_loc loc in [(grafite_status,lexicon_status),parsed_text],"", 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,text,len = try 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:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> raise (GrafiteDisambiguator.DisambiguationError (offset+parsed_text_length, errorll)) in assert (text=""); (* no macros inside comments, please! *) (match s with | (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) ~(mathviewer: MatitaTypes.mathViewer) ~set_star ~ask_confirmation ~urichooser () = let buffer = source_view#buffer in let source_buffer = source_view#source_buffer in let initial_statuses baseuri = let lexicon_status = CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script in let grafite_status = GrafiteSync.init baseuri in grafite_status,lexicon_status in let read_include_paths file = try let root, _buri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:[] file in let rc = Str.split (Str.regexp " ") (List.assoc "include_paths" (Librarian.load_root_file (root^"/root"))) in List.iter (HLog.debug) rc; rc with Librarian.NoRootFor _ | Not_found -> [] in let default_buri = "cic:/matita/tests" in let default_fname = ".unnamed.ma" in object (self) val mutable include_paths_ = [] val scriptId = fresh_script_id () val guistuff = { mathviewer = mathviewer; urichooser = urichooser; ask_confirmation = ask_confirmation; } val mutable filename_ = (None : string option) method has_name = filename_ <> None method include_paths = include_paths_ @ Helm_registry.get_list Helm_registry.string "matita.includes" method private curdir = try let root, _buri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:self#include_paths self#filename in root with Librarian.NoRootFor _ -> Sys.getcwd () method buri_of_current_file = match filename_ with | None -> default_buri | Some f -> try let _root, buri, _fname, _tgt = Librarian.baseuri_of_script ~include_paths:self#include_paths f in buri with Librarian.NoRootFor _ -> default_buri method filename = match filename_ with None -> default_fname | Some f -> f initializer ignore (GMain.Timeout.add ~ms:300000 ~callback:(fun _ -> self#_saveToBackupFile ();true)); ignore (buffer#connect#modified_changed (fun _ -> set_star buffer#modified)) val mutable statements = [] (** executed statements *) val mutable history = [ initial_statuses 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. * 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 = None (** text mark and tag representing locked part of a script *) val locked_mark = buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter val beginning_of_statement_mark = buffer#create_mark ~name:"beginning_of_statement" ~left_gravity:true buffer#start_iter val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false] val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"] method locked_mark = locked_mark method locked_tag = locked_tag method error_tag = error_tag (* 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 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 entries, newtext, parsed_len = try eval_statement self#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 let parsed_text = String.sub s 0 parsed_len in if new_text <> parsed_text then begin let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in buffer#delete ~start ~stop; buffer#insert ~iter:start new_text; end; end; self#moveMark (Glib.Utf8.length new_text); 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 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 = 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 advance ?statement () = try self#_advance ?statement (); self#notify with | Margin -> self#notify | Not_found -> assert false | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" | exc -> self#notify; raise exc method retract () = try let cmp,new_statements,new_history,(grafite_status,lexicon_status) = match statements,history with stat::statements, _::(status::_ as history) -> assert (Glib.Utf8.validate stat); Glib.Utf8.length stat, statements, history, status | [],[_] -> raise Margin | _,_ -> assert false in self#_retract cmp lexicon_status grafite_status new_statements new_history; self#notify with | Margin -> self#notify | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" | exc -> self#notify; raise exc method private getFuture = buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark)) ~stop:buffer#end_iter () (** @param rel_offset relative offset from current position of locked_mark *) method private moveMark rel_offset = let mark = `MARK locked_mark in let old_insert = buffer#get_iter_at_mark `INSERT in buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; let current_mark_pos = buffer#get_iter_at_mark mark in let new_mark_pos = match rel_offset with | 0 -> current_mark_pos | n when n > 0 -> current_mark_pos#forward_chars n | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n) in buffer#move_mark mark ~where:new_mark_pos; buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos; buffer#move_mark `INSERT old_insert; let mark_position = buffer#get_iter_at_mark mark in if source_view#move_mark_onscreen mark then begin buffer#move_mark mark mark_position; source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark; end; while Glib.Main.pending () do ignore(Glib.Main.iteration false); done method clean_dirty_lock = let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter; buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter val mutable observers = [] method addObserver (o: LexiconEngine.status -> 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 method loadFromString s = buffer#set_text s; self#reset_buffer; buffer#set_modified true method loadFromFile f = buffer#set_text (HExtlib.input_file f); self#reset_buffer; buffer#set_modified false method assignFileName file = let file = match file with | 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 -> []); self#reset_buffer; Sys.chdir self#curdir; HLog.debug ("Moving to " ^ Sys.getcwd ()) method saveToFile () = if self#has_name then let oc = open_out self#filename in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; set_star false; buffer#set_modified false else HLog.error "Can't save, no filename selected" method private _saveToBackupFile () = if buffer#modified then begin let f = self#filename in let oc = open_out f in output_string oc (buffer#get_text ~start:buffer#start_iter ~stop:buffer#end_iter ()); close_out oc; 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 ]; 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 reset () = self#reset_buffer; source_buffer#begin_not_undoable_action (); buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter; source_buffer#end_not_undoable_action (); buffer#set_modified false; method template () = let template = HExtlib.input_file BuildTimeConf.script_template in buffer#insert ~iter:(buffer#get_iter `START) template; buffer#set_modified false; set_star false method goto (pos: [`Top | `Bottom | `Cursor]) () = try let old_locked_mark = `MARK (buffer#create_mark ~name:"old_locked_mark" ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in match pos with | `Top -> dispose_old_locked_mark (); self#goto_top; self#reset_buffer; self#notify | `Bottom -> (try let rec dowhile () = self#_advance (); let newpos = getpos () in if (getoldpos ())#compare newpos < 0 then begin buffer#move_mark old_locked_mark newpos; dowhile () end in dowhile (); dispose_old_locked_mark (); self#notify with | Margin -> dispose_old_locked_mark (); self#notify | exc -> dispose_old_locked_mark (); self#notify; raise exc) | `Cursor -> let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in let cursor_iter () = buffer#get_iter_at_mark `INSERT in let remember = `MARK (buffer#create_mark ~name:"initial_insert" ~left_gravity:true (cursor_iter ())) in let dispose_remember () = buffer#delete_mark remember in let remember_iter () = buffer#get_iter_at_mark (`NAME "initial_insert") in let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in let icmp = cmp () in let forward_until_cursor () = (* go forward until locked > cursor *) let rec aux () = self#_advance (); if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0 then begin buffer#move_mark old_locked_mark (getpos ()); aux () end in aux () in let rec back_until_cursor len = (* go backward until locked < cursor *) function 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 - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2) | _,_ -> assert false in (try begin if icmp < 0 then (* locked < cursor *) (forward_until_cursor (); self#notify) else if icmp > 0 then (* locked > cursor *) (back_until_cursor icmp (statements,history); self#notify) else (* cursor = locked *) () end ; dispose_remember (); dispose_old_locked_mark (); with | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify | exc -> dispose_remember (); dispose_old_locked_mark (); self#notify; raise exc) with Invalid_argument "Array.make" -> HLog.error "The script is too big!\n" method onGoingProof () = 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#grafite_status method proofContext = match userGoal with None -> [] | Some n -> GrafiteTypes.get_proof_context self#grafite_status n method proofConclusion = 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 bos = match history with | _::[] -> true | _ -> false method eos = 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:self#include_paths lexicon_status in match st with | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in (* CSC: why +1 in the following lines ???? *) let parsed_text_length = parsed_text_length + 1 in prerr_endline ("## " ^ string_of_int parsed_text_length); let remain_len = String.length s - parsed_text_length in let next = String.sub s parsed_text_length remain_len in is_there_only_comments lexicon_status next | GrafiteParser.LNone _ | GrafiteParser.LSome (GrafiteAst.Executable _) -> false in try is_there_only_comments self#lexicon_status self#getFuture with | LexiconEngine.IncludedFileNotCompiled _ | HExtlib.Localized _ | CicNotationParser.Parse_error _ -> false | Margin | End_of_file -> true | Invalid_argument "Array.make" -> false (* debug *) method dump () = HLog.debug "script status:"; HLog.debug ("history size: " ^ string_of_int (List.length history)); HLog.debug (sprintf "%d statements:" (List.length statements)); List.iter HLog.debug statements; HLog.debug ("Current file name: " ^ self#filename); end let _script = ref None let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star () = let s = new script ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () in _script := Some s; s let current () = match !_script with None -> assert false | Some s -> s