X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2FmatitaScript.ml;fp=matita%2FmatitaScript.ml;h=a27b0183197557d16f9782d5099580ef04274391;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/matitaScript.ml b/matita/matitaScript.ml new file mode 100644 index 000000000..a27b01831 --- /dev/null +++ b/matita/matitaScript.ml @@ -0,0 +1,1154 @@ +(* 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 +