]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/matitaScript.ml
Procedural: we removed some commented code
[helm.git] / helm / software / matita / matitaScript.ml
1 (* Copyright (C) 2004-2005, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 (* $Id$ *)
27
28 open Printf
29 open GrafiteTypes
30
31 module TA = GrafiteAst
32
33 let debug = false
34 let debug_print = if debug then prerr_endline else ignore
35
36   (** raised when one of the script margins (top or bottom) is reached *)
37 exception Margin
38 exception NoUnfinishedProof
39 exception ActionCancelled of string
40
41 let safe_substring s i j =
42   try String.sub s i j with Invalid_argument _ -> assert false
43
44 let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*"
45 let heading_nl_RE' = Pcre.regexp "^(\\s*\n\\s*)"
46 let only_dust_RE = Pcre.regexp "^(\\s|\n|%%[^\n]*\n)*$"
47 let multiline_RE = Pcre.regexp "^\n[^\n]+$"
48 let newline_RE = Pcre.regexp "\n"
49 let comment_RE = Pcre.regexp "\\(\\*(.|\n)*\\*\\)\n?" ~flags:[`UNGREEDY]
50  
51 let comment str =
52   if Pcre.pmatch ~rex:multiline_RE str then
53     "\n(** " ^ (Pcre.replace ~rex:newline_RE str) ^ " *)"
54   else
55     "\n(**\n" ^ str ^ "\n*)"
56
57 let strip_comments str =
58   Pcre.qreplace ~templ:"\n" ~pat:"\n\n" (Pcre.qreplace ~rex:comment_RE str)
59 ;;
60                      
61 let first_line s =
62   let s = Pcre.replace ~rex:heading_nl_RE s in
63   try
64     let nl_pos = String.index s '\n' in
65     String.sub s 0 nl_pos
66   with Not_found -> s
67
68 type guistuff = {
69   mathviewer:MatitaTypes.mathViewer;
70   urichooser: UriManager.uri list -> UriManager.uri list;
71   ask_confirmation: title:string -> message:string -> [`YES | `NO | `CANCEL];
72 }
73
74 let eval_with_engine include_paths guistuff lexicon_status grafite_status user_goal
75  skipped_txt nonskipped_txt st
76 =
77   let module TAPp = GrafiteAstPp in
78   let module DTE = DisambiguateTypes.Environment in
79   let module DP = DisambiguatePp in
80   let parsed_text_length =
81     String.length skipped_txt + String.length nonskipped_txt 
82   in
83   let text = skipped_txt ^ nonskipped_txt in
84   let prefix_len = MatitaGtkMisc.utf8_string_length skipped_txt in
85   let enriched_history_fragment =
86    MatitaEngine.eval_ast ~do_heavy_checks:(Helm_registry.get_bool
87      "matita.do_heavy_checks")
88     lexicon_status grafite_status (text,prefix_len,st)
89   in
90   let enriched_history_fragment = List.rev enriched_history_fragment in
91   (* really fragile *)
92   let res,_ = 
93     List.fold_left 
94       (fun (acc, to_prepend) (status,alias) ->
95        match alias with
96        | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
97        | Some (k,((v,_) as value)) ->
98             let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in
99             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
100       ([],skipped_txt) enriched_history_fragment
101   in
102   res,"",parsed_text_length
103 ;;
104
105 (* this function calls the parser in a way that it does not perform inclusions,
106  * so that we can ensure the inclusion is performed after the included file 
107  * is compiled (if needed). matitac does not need that, since it compiles files
108  * in the good order, here files may be compiled on demand. *)
109 let wrap_with_make include_paths (f : GrafiteParser.statement) x = 
110   try      
111     f ~never_include:true ~include_paths x
112   with
113   | GrafiteParser.NoInclusionPerformed mafilename ->
114       let root, buri, _, tgt = 
115         try Librarian.baseuri_of_script ~include_paths mafilename
116         with Librarian.NoRootFor _ -> 
117           HLog.error ("The included file '"^mafilename^"' has no root file,");
118           HLog.error "please create it.";
119           raise (Failure ("No root file for "^mafilename))
120       in
121       let b = 
122         try
123           GrafiteSync.push ();
124           LexiconSync.push ();
125           let rc = MatitacLib.Make.make root [tgt] in 
126           LexiconSync.pop ();
127           GrafiteSync.pop ();
128           rc
129         with 
130         | exn ->
131             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
132             assert false
133       in
134       if b then 
135         try f ~include_paths x with LexiconEngine.IncludedFileNotCompiled _ ->
136          raise 
137            (Failure ("Including: "^tgt^
138              "\nNothing to do... did you run matitadep?"))
139       else raise (Failure ("Compiling: " ^ tgt))
140 ;;
141
142 let pp_eager_statement_ast =
143   GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
144     ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
145
146 (* naive implementation of procedural proof script generation, 
147  * starting from an applicatiove *auto generated) proof.
148  * this is out of place, but I like it :-P *)
149 let cic2grafite context menv t =
150   (* indents a proof script in a stupid way, better than nothing *)
151   let stupid_indenter s =
152     let next s = 
153       let idx_square_o = try String.index s '[' with Not_found -> -1 in
154       let idx_square_c = try String.index s ']' with Not_found -> -1 in
155       let idx_pipe = try String.index s '|' with Not_found -> -1 in
156       let tok = 
157         List.sort (fun (i,_) (j,_) -> compare i j)
158           [idx_square_o,'[';idx_square_c,']';idx_pipe,'|']
159       in
160       let tok = List.filter (fun (i,_) -> i <> -1) tok in
161       match tok with
162       | (i,c)::_ -> Some (i,c)
163       | _ -> None
164     in
165     let break_apply n s =
166       let tab = String.make (n+1) ' ' in
167       Pcre.replace ~templ:(".\n" ^ tab ^ "apply") ~pat:"\\.apply" s
168     in
169     let rec ind n s =
170       match next s with
171       | None -> 
172           s
173       | Some (position, char) ->
174           try 
175             let s1, s2 = 
176               String.sub s 0 position, 
177               String.sub s (position+1) (String.length s - (position+1))
178             in
179             match char with
180             | '[' -> break_apply n s1 ^ "\n" ^ String.make (n+2) ' ' ^
181                        "[" ^ ind (n+2) s2
182             | '|' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ 
183                        "|" ^ ind n s2
184             | ']' -> break_apply n s1 ^ "\n" ^ String.make n ' ' ^ 
185                        "]" ^ ind (n-2) s2
186             | _ -> assert false
187           with
188           Invalid_argument err -> 
189             prerr_endline err;
190             s
191     in
192      ind 0 s
193   in
194   let module PT = CicNotationPt in
195   let module GA = GrafiteAst in
196   let pp_t context t =
197     let names = 
198       List.map (function Some (n,_) -> Some n | None -> None) context 
199     in
200     CicPp.pp t names
201   in
202   let sort_of context t = 
203     try
204       let ty,_ = 
205         CicTypeChecker.type_of_aux' menv context t
206           CicUniv.oblivion_ugraph 
207       in
208       let sort,_ = CicTypeChecker.type_of_aux' menv context ty
209           CicUniv.oblivion_ugraph
210       in
211       match sort with
212       | Cic.Sort Cic.Prop -> true
213       | _ -> false
214     with
215       CicTypeChecker.TypeCheckerFailure _ ->
216         HLog.error "auto proof to sript transformation error"; false
217   in
218   let floc = HExtlib.dummy_floc in
219   (* minimalisti cic.term -> pt.term *)
220   let print_term c t =
221     let rec aux c = function
222       | Cic.Rel _
223       | Cic.MutConstruct _ 
224       | Cic.MutInd _ 
225       | Cic.Const _ as t -> 
226           PT.Ident (pp_t c t, None)
227       | Cic.Appl l -> PT.Appl (List.map (aux c) l)
228       | Cic.Implicit _ -> PT.Implicit
229       | Cic.Lambda (Cic.Name n, s, t) ->
230           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
231             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
232       | Cic.Prod (Cic.Name n, s, t) ->
233           PT.Binder (`Forall, (PT.Ident (n,None), Some (aux c s)),
234             aux (Some (Cic.Name n, Cic.Decl s)::c) t)
235       | Cic.LetIn (Cic.Name n, s, ty, t) ->
236           PT.Binder (`Lambda, (PT.Ident (n,None), Some (aux c s)),
237             aux (Some (Cic.Name n, Cic.Def (s,ty))::c) t)
238       | Cic.Meta _ -> PT.Implicit
239       | Cic.Sort (Cic.Type u) -> PT.Sort (`Type u)
240       | Cic.Sort Cic.Set -> PT.Sort `Set
241       | Cic.Sort (Cic.CProp u) -> PT.Sort (`CProp u)
242       | Cic.Sort Cic.Prop -> PT.Sort `Prop
243       | _ as t -> PT.Ident ("ERROR: "^CicPp.ppterm t, None)
244     in
245     aux c t
246   in
247   (* prints an applicative proof, that is an auto proof.
248    * don't use in the general case! *)
249   let rec print_proof context = function
250     | Cic.Rel _
251     | Cic.Const _ as t -> 
252         [GA.Executable (floc, 
253           GA.Tactic (floc,
254           Some (GA.Apply (floc, print_term context t)), GA.Dot floc))]
255     | Cic.Appl (he::tl) ->
256         let tl = List.map (fun t -> t, sort_of context t) tl in
257         let subgoals = 
258           HExtlib.filter_map (function (t,true) -> Some t | _ -> None) tl
259         in
260         let args = 
261           List.map (function | (t,true) -> Cic.Implicit None | (t,_) -> t) tl
262         in
263         if List.length subgoals > 1 then
264           (* branch *)
265           [GA.Executable (floc, 
266             GA.Tactic (floc,
267               Some (GA.Apply (floc, print_term context (Cic.Appl (he::args)))),
268               GA.Semicolon floc))] @
269           [GA.Executable (floc, GA.Tactic (floc, None, GA.Branch floc))] @
270           (HExtlib.list_concat 
271           ~sep:[GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))]
272             (List.map (print_proof context) subgoals)) @
273           [GA.Executable (floc, GA.Tactic (floc, None,GA.Merge floc))]
274         else
275           (* simple apply *)
276           [GA.Executable (floc, 
277             GA.Tactic (floc,
278             Some (GA.Apply 
279               (floc, print_term context (Cic.Appl (he::args)) )), GA.Dot floc))]
280           @
281           (match subgoals with
282           | [] -> []
283           | [x] -> print_proof context x
284           | _ -> assert false)
285     | Cic.Lambda (Cic.Name n, ty, bo) ->
286         [GA.Executable (floc, 
287           GA.Tactic (floc,
288             Some (GA.Cut (floc, Some n, (print_term context ty))),
289             GA.Branch floc))] @
290         (print_proof (Some (Cic.Name n, Cic.Decl ty)::context) bo) @
291         [GA.Executable (floc, GA.Tactic (floc, None,GA.Shift floc))] @
292         [GA.Executable (floc, GA.Tactic (floc, 
293           Some (GA.Assumption floc),GA.Merge floc))]
294     | _ -> []
295     (*
296         debug_print (lazy (CicPp.ppterm t));
297         assert false
298         *)
299   in
300   (* performs a lambda closure of the proof term abstracting metas.
301    * this is really an approximation of a closure, local subst of metas 
302    * is not kept into account *)
303   let close_pt menv context t =
304     let metas = CicUtil.metas_of_term t in
305     let metas = 
306       HExtlib.list_uniq ~eq:(fun (i,_) (j,_) -> i = j)
307         (List.sort (fun (i,_) (j,_) -> compare i j) metas)
308     in
309     let mk_rels_and_collapse_metas metas = 
310       let rec aux i map acc acc1 = function 
311         | [] -> acc, acc1, map
312         | (j,_ as m)::tl -> 
313             let _,_,ty = CicUtil.lookup_meta j menv in
314             try 
315               let n = List.assoc ty map in
316               aux i map (Cic.Rel n :: acc) (m::acc1) tl 
317             with Not_found -> 
318               let map = (ty, i)::map in
319               aux (i+1) map (Cic.Rel i :: acc) (m::acc1) tl
320       in
321       aux 1 [] [] [] metas
322     in
323     let rels, metas, map = mk_rels_and_collapse_metas metas in
324     let n_lambdas = List.length map in
325     let t = 
326       if metas = [] then 
327         t 
328       else
329         let t =
330           ProofEngineReduction.replace_lifting
331            ~what:(List.map (fun (x,_) -> Cic.Meta (x,[])) metas)
332            ~with_what:rels
333            ~context:context
334            ~equality:(fun _ x y ->
335              match x,y with
336              | Cic.Meta(i,_), Cic.Meta(j,_) when i=j -> true
337              | _ -> false)
338            ~where:(CicSubstitution.lift n_lambdas t)
339         in
340         let rec mk_lam = function 
341           | [] -> t 
342           | (ty,n)::tl -> 
343               let name = "fresh_"^ string_of_int n in
344               Cic.Lambda (Cic.Name name, ty, mk_lam tl)
345         in
346          mk_lam 
347           (fst (List.fold_left 
348             (fun (l,liftno) (ty,_)  -> 
349               (l @ [CicSubstitution.lift liftno ty,liftno] , liftno+1))
350             ([],0) map))
351     in
352       t
353   in
354   let ast = print_proof context (close_pt menv context t) in
355   let pp t = 
356     (* ZACK: setting width to 80 will trigger a bug of BoxPp.render_to_string
357      * which will show up using the following command line:
358      * ./tptp2grafite -tptppath ~tassi/TPTP-v3.1.1 GRP170-1 *)
359     let width = max_int in
360     let term_pp content_term =
361       let pres_term = TermContentPres.pp_ast content_term in
362       let dummy_tbl = Hashtbl.create 1 in
363       let markup = CicNotationPres.render dummy_tbl pres_term in
364       let s = "(" ^ BoxPp.render_to_string
365        ~map_unicode_to_tex:(Helm_registry.get_bool
366          "matita.paste_unicode_as_tex")
367        List.hd width markup ^ ")" in
368       Pcre.substitute 
369         ~pat:"\\\\forall [Ha-z][a-z0-9_]*" ~subst:(fun x -> "\n" ^ x) s
370     in
371     CicNotationPp.set_pp_term term_pp;
372     let lazy_term_pp = fun x -> assert false in
373     let obj_pp = CicNotationPp.pp_obj CicNotationPp.pp_term in
374     GrafiteAstPp.pp_statement
375      ~map_unicode_to_tex:(Helm_registry.get_bool
376        "matita.paste_unicode_as_tex")
377      ~term_pp ~lazy_term_pp ~obj_pp t
378   in
379   let script = String.concat "" (List.map pp ast) in
380   prerr_endline script;
381   stupid_indenter script
382 ;;
383
384 let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status grafite_status user_goal unparsed_text parsed_text script mac =
385   let module TAPp = GrafiteAstPp in
386   let module MQ = MetadataQuery in
387   let module MDB = LibraryDb in
388   let module CTC = CicTypeChecker in
389   let module CU = CicUniv in
390   (* no idea why ocaml wants this *)
391   let parsed_text_length = String.length parsed_text in
392   let dbd = LibraryDb.instance () in
393   let pp_macro = 
394     let f t = ProofEngineReduction.replace 
395       ~equality:(fun _ t -> match t with Cic.Meta _ -> true | _ -> false)
396       ~what:[()] ~with_what:[Cic.Implicit None] ~where:t
397     in
398     let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
399     TAPp.pp_macro 
400       ~term_pp:(fun x -> 
401         ApplyTransformation.txt_of_cic_term max_int metasenv [] (f x)
402          ~map_unicode_to_tex:(Helm_registry.get_bool
403            "matita.paste_unicode_as_tex"))
404   in
405   match mac with
406   (* WHELP's stuff *)
407   | TA.WMatch (loc, term) -> 
408      let l =  Whelp.match_term ~dbd term in
409      let entry = `Whelp (pp_macro mac, l) in
410      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
411      [], "", parsed_text_length
412   | TA.WInstance (loc, term) ->
413      let l = Whelp.instance ~dbd term in
414      let entry = `Whelp (pp_macro mac, l) in
415      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
416      [], "", parsed_text_length
417   | TA.WLocate (loc, s) -> 
418      let l = Whelp.locate ~dbd s in
419      let entry = `Whelp (pp_macro mac, l) in
420      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
421      [], "", parsed_text_length
422   | TA.WElim (loc, term) ->
423      let uri =
424        match term with
425        | Cic.MutInd (uri,n,_) -> UriManager.uri_of_uriref uri n None 
426        | _ -> failwith "Not a MutInd"
427      in
428      let l = Whelp.elim ~dbd uri in
429      let entry = `Whelp (pp_macro mac, l) in
430      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
431      [], "", parsed_text_length
432   | TA.WHint (loc, term) ->
433      let _subst = [] in
434      let s = ((None,[0,[],term], _subst, lazy (Cic.Meta (0,[])) ,term, []),0) in
435      let l = List.map fst (MQ.experimental_hint ~dbd s) in
436      let entry = `Whelp (pp_macro mac, l) in
437      guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
438      [], "", parsed_text_length
439   (* REAL macro *)
440   | TA.Hint (loc, rewrite) -> 
441       let user_goal' =
442        match user_goal with
443           Some n -> n
444         | None -> raise NoUnfinishedProof
445       in
446       let proof = GrafiteTypes.get_current_proof grafite_status in
447       let proof_status = proof,user_goal' in
448       if rewrite then
449         let l = MQ.equations_for_goal ~dbd proof_status in
450         let l = List.filter (fun u -> not (LibraryObjects.in_eq_URIs u)) l in
451         let entry = `Whelp (pp_macro (TA.WHint(loc, Cic.Implicit None)), l) in
452         guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
453         [], "", parsed_text_length
454       else
455         let l = List.map fst (MQ.experimental_hint ~dbd proof_status) in
456         let selected = guistuff.urichooser l in
457         (match selected with
458         | [] -> [], "", parsed_text_length
459         | [uri] -> 
460             let suri = UriManager.string_of_uri uri in
461             let ast loc =
462               TA.Executable (loc, (TA.Tactic (loc,
463                Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
464                TA.Dot loc))) in
465             let text =
466              comment parsed_text ^ "\n" ^
467               pp_eager_statement_ast (ast HExtlib.dummy_floc)
468               ~map_unicode_to_tex:(Helm_registry.get_bool
469                 "matita.paste_unicode_as_tex")
470             in
471             let text_len = MatitaGtkMisc.utf8_string_length text in
472             let loc = HExtlib.floc_of_loc (0,text_len) in
473             let statement = `Ast (GrafiteParser.LSome (ast loc),text) in
474             let res,_,_parsed_text_len =
475              eval_statement include_paths buffer guistuff lexicon_status
476               grafite_status user_goal script statement
477             in
478              (* we need to replace all the parsed_text *)
479              res,"",String.length parsed_text
480         | _ -> 
481             HLog.error 
482               "The result of the urichooser should be only 1 uri, not:\n";
483             List.iter (
484               fun u -> HLog.error (UriManager.string_of_uri u ^ "\n")
485             ) selected;
486             assert false)
487   | TA.Check (_,term) ->
488       let metasenv = GrafiteTypes.get_proof_metasenv grafite_status in
489       let context =
490        match user_goal with
491           None -> []
492         | Some n -> GrafiteTypes.get_proof_context grafite_status n in
493       let ty,_ = CTC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
494       let t_and_ty = Cic.Cast (term,ty) in
495       guistuff.mathviewer#show_entry (`Cic (t_and_ty,metasenv));
496       [], "", parsed_text_length
497   | TA.AutoInteractive (_, params) ->
498       let user_goal' =
499        match user_goal with
500           Some n -> n
501         | None -> raise NoUnfinishedProof
502       in
503       let proof = GrafiteTypes.get_current_proof grafite_status in
504       let proof_status = proof,user_goal' in
505       (try
506         let _,menv,_,_,_,_ = proof in
507         let i,cc,ty = CicUtil.lookup_meta user_goal' menv in
508         let timestamp = Unix.gettimeofday () in
509         let (_,menv,subst,_,_,_), _ = 
510           ProofEngineTypes.apply_tactic
511             (Auto.auto_tac ~dbd ~params
512               ~universe:grafite_status.GrafiteTypes.universe) proof_status
513         in
514         let proof_term = 
515           let irl = 
516             CicMkImplicit.identity_relocation_list_for_metavariable cc
517           in
518           CicMetaSubst.apply_subst subst (Cic.Meta (i,irl))
519         in
520         let time = Unix.gettimeofday () -. timestamp in
521         let size, depth = Auto.size_and_depth cc menv proof_term in
522         let trailer = 
523           Printf.sprintf 
524             "\n(* end auto(%s) proof: TIME=%4.2f SIZE=%d DEPTH=%d *)"
525             Auto.revision time size depth
526         in
527         let proof_script = 
528           if List.exists (fun (s,_) -> s = "paramodulation") (snd params) then
529               let proof_term, how_many_lambdas = 
530                 Auto.lambda_close ~prefix_name:"orrible_hack_" 
531                   proof_term menv cc 
532               in
533               let ty,_ = 
534                 CicTypeChecker.type_of_aux'
535                   menv [] proof_term CicUniv.empty_ugraph
536               in
537               prerr_endline (CicPp.ppterm proof_term);
538               (* use declarative output *)
539               let obj =
540                 (* il proof_term vive in cc, devo metterci i lambda no? *)
541                 (Cic.CurrentProof ("xxx",menv,proof_term,ty,[],[]))
542               in
543                ApplyTransformation.txt_of_cic_object
544                 ~map_unicode_to_tex:(Helm_registry.get_bool
545                   "matita.paste_unicode_as_tex")
546                 ~skip_thm_and_qed:true
547                 ~skip_initial_lambdas:how_many_lambdas
548                 80 GrafiteAst.Declarative "" obj
549           else
550             if true then
551               (* use cic2grafite *)
552               cic2grafite cc menv proof_term 
553             else
554               (* alternative using FG stuff *)
555               let map_unicode_to_tex =
556                  Helm_registry.get_bool "matita.paste_unicode_as_tex"
557               in
558               ApplyTransformation.procedural_txt_of_cic_term
559                  ~map_unicode_to_tex 78 cc proof_term
560         in
561         let text = comment parsed_text ^ "\n" ^ proof_script ^ trailer in
562         [],text,parsed_text_length
563       with
564         ProofEngineTypes.Fail _ as exn -> 
565           raise exn
566           (* [], comment parsed_text ^ "\nfail.\n", parsed_text_length *))
567   | TA.Inline (_,style,suri,prefix,flavour) ->
568        let str = 
569          ApplyTransformation.txt_of_inline_macro
570           ~map_unicode_to_tex:(Helm_registry.get_bool
571             "matita.paste_unicode_as_tex")
572           style ?flavour prefix suri 
573        in
574        [], str, String.length parsed_text
575                                 
576 and eval_executable include_paths (buffer : GText.buffer) guistuff
577 lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
578 script ex loc
579 =
580  let module TAPp = GrafiteAstPp in
581  let module MD = GrafiteDisambiguator in
582  let module ML = MatitaMisc in
583   try
584    ignore (buffer#move_mark (`NAME "beginning_of_statement")
585     ~where:((buffer#get_iter_at_mark (`NAME "locked"))#forward_chars
586        (Glib.Utf8.length skipped_txt))) ;
587    eval_with_engine include_paths 
588     guistuff lexicon_status grafite_status user_goal skipped_txt nonskipped_txt
589      (TA.Executable (loc, ex))
590   with
591      MatitaTypes.Cancel -> [], "", 0
592    | GrafiteEngine.Macro (_loc,lazy_macro) ->
593       let context =
594        match user_goal with
595           None -> []
596         | Some n -> GrafiteTypes.get_proof_context grafite_status n in
597       let grafite_status,macro = lazy_macro context in
598        eval_macro include_paths buffer guistuff lexicon_status grafite_status
599         user_goal unparsed_text (skipped_txt ^ nonskipped_txt) script macro
600
601 and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
602  grafite_status user_goal script statement
603 =
604   let (lexicon_status,st), unparsed_text =
605     match statement with
606     | `Raw text ->
607         if Pcre.pmatch ~rex:only_dust_RE text then raise Margin;
608         let ast = 
609          wrap_with_make include_paths
610           (GrafiteParser.parse_statement (Ulexing.from_utf8_string text)) lexicon_status 
611         in
612           ast, text
613     | `Ast (st, text) -> (lexicon_status, st), text
614   in
615   let text_of_loc floc = 
616     let nonskipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
617     let start, stop = HExtlib.loc_of_floc floc in 
618     let floc = HExtlib.floc_of_loc (0, start) in
619     let skipped_txt,_ = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
620     let floc = HExtlib.floc_of_loc (0, stop) in
621     let txt,len = MatitaGtkMisc.utf8_parsed_text unparsed_text floc in
622     txt,nonskipped_txt,skipped_txt,len
623   in 
624   match st with
625   | GrafiteParser.LNone loc ->
626       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
627        [(grafite_status,lexicon_status),parsed_text],"",
628         parsed_text_length
629   | GrafiteParser.LSome (GrafiteAst.Comment (loc, _)) -> 
630       let parsed_text, _, _, parsed_text_length = text_of_loc loc in
631       let remain_len = String.length unparsed_text - parsed_text_length in
632       let s = String.sub unparsed_text parsed_text_length remain_len in
633       let s,text,len = 
634        try
635         eval_statement include_paths buffer guistuff lexicon_status
636          grafite_status user_goal script (`Raw s)
637        with
638           HExtlib.Localized (floc, exn) ->
639            HExtlib.raise_localized_exception 
640              ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
641         | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
642            raise
643             (GrafiteDisambiguator.DisambiguationError
644               (offset+parsed_text_length, errorll))
645       in
646       assert (text=""); (* no macros inside comments, please! *)
647       (match s with
648       | (statuses,text)::tl ->
649          (statuses,parsed_text ^ text)::tl,"",parsed_text_length + len
650       | [] -> [], "", 0)
651   | GrafiteParser.LSome (GrafiteAst.Executable (loc, ex)) ->
652      let _, nonskipped, skipped, parsed_text_length = 
653        text_of_loc loc 
654      in
655       eval_executable include_paths buffer guistuff lexicon_status
656        grafite_status user_goal unparsed_text skipped nonskipped script ex loc
657   
658 let fresh_script_id =
659   let i = ref 0 in
660   fun () -> incr i; !i
661
662 class script  ~(source_view: GSourceView.source_view)
663               ~(mathviewer: MatitaTypes.mathViewer) 
664               ~set_star
665               ~ask_confirmation
666               ~urichooser 
667               () =
668 let buffer = source_view#buffer in
669 let source_buffer = source_view#source_buffer in
670 let initial_statuses baseuri =
671  let lexicon_status =
672    CicNotation2.load_notation ~include_paths:[]
673      BuildTimeConf.core_notation_script 
674  in
675  let grafite_status = GrafiteSync.init baseuri in
676   grafite_status,lexicon_status
677 in
678 let read_include_paths file =
679  try 
680    let root, _buri, _fname, _tgt = 
681      Librarian.baseuri_of_script ~include_paths:[] file 
682    in 
683    let rc = 
684     Str.split (Str.regexp " ") 
685      (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
686    in
687    List.iter (HLog.debug) rc; rc
688  with Librarian.NoRootFor _ | Not_found -> []
689 in
690 let default_buri = "cic:/matita/tests" in
691 let default_fname = ".unnamed.ma" in
692 object (self)
693   val mutable include_paths_ = []
694
695   val scriptId = fresh_script_id ()
696
697   val guistuff = {
698     mathviewer = mathviewer;
699     urichooser = urichooser;
700     ask_confirmation = ask_confirmation;
701   }
702
703   val mutable filename_ = (None : string option)
704
705   method has_name = filename_ <> None
706   
707   method include_paths =
708     include_paths_ @ 
709     Helm_registry.get_list Helm_registry.string "matita.includes"
710
711   method private curdir =
712     try
713      let root, _buri, _fname, _tgt = 
714        Librarian.baseuri_of_script ~include_paths:self#include_paths
715        self#filename 
716      in 
717      root
718     with Librarian.NoRootFor _ -> Sys.getcwd ()
719
720   method buri_of_current_file =
721     match filename_ with
722     | None -> default_buri 
723     | Some f ->
724         try 
725           let _root, buri, _fname, _tgt = 
726             Librarian.baseuri_of_script ~include_paths:self#include_paths f 
727           in 
728           buri
729         with Librarian.NoRootFor _ -> default_buri
730
731   method filename = match filename_ with None -> default_fname | Some f -> f
732
733   initializer 
734     ignore (GMain.Timeout.add ~ms:300000 
735        ~callback:(fun _ -> self#_saveToBackupFile ();true));
736     ignore (buffer#connect#modified_changed 
737       (fun _ -> set_star buffer#modified))
738
739   val mutable statements = []    (** executed statements *)
740
741   val mutable history = [ initial_statuses default_buri ]
742     (** list of states before having executed statements. Head element of this
743       * list is the current state, last element is the state at the beginning of
744       * the script.
745       * Invariant: this list length is 1 + length of statements *)
746
747   (** goal as seen by the user (i.e. metano corresponding to current tab) *)
748   val mutable userGoal = None
749
750   (** text mark and tag representing locked part of a script *)
751   val locked_mark =
752     buffer#create_mark ~name:"locked" ~left_gravity:true buffer#start_iter
753   val beginning_of_statement_mark =
754     buffer#create_mark ~name:"beginning_of_statement"
755      ~left_gravity:true buffer#start_iter
756   val locked_tag = buffer#create_tag [`BACKGROUND "lightblue"; `EDITABLE false]
757   val error_tag = buffer#create_tag [`UNDERLINE `SINGLE; `FOREGROUND "red"]
758
759   method locked_mark = locked_mark
760   method locked_tag = locked_tag
761   method error_tag = error_tag
762
763     (* history can't be empty, the invariant above grant that it contains at
764      * least the init grafite_status *)
765   method grafite_status = match history with (s,_)::_ -> s | _ -> assert false
766   method lexicon_status = match history with (_,ss)::_ -> ss | _ -> assert false
767
768   method private _advance ?statement () =
769    let s = match statement with Some s -> s | None -> self#getFuture in
770    if self#bos then LibraryClean.clean_baseuris [self#buri_of_current_file];
771    HLog.debug ("evaluating: " ^ first_line s ^ " ...");
772    let entries, newtext, parsed_len = 
773     try
774      eval_statement self#include_paths buffer guistuff self#lexicon_status
775       self#grafite_status userGoal self (`Raw s)
776     with End_of_file -> raise Margin
777    in
778    let new_statuses, new_statements =
779      let statuses, texts = List.split entries in
780      statuses, texts
781    in
782    history <- new_statuses @ history;
783    statements <- new_statements @ statements;
784    let start = buffer#get_iter_at_mark (`MARK locked_mark) in
785    let new_text = String.concat "" (List.rev new_statements) in
786    if statement <> None then
787      buffer#insert ~iter:start new_text
788    else begin
789      let parsed_text = String.sub s 0 parsed_len in
790      if new_text <> parsed_text then begin
791        let stop = start#copy#forward_chars (Glib.Utf8.length parsed_text) in
792        buffer#delete ~start ~stop;
793        buffer#insert ~iter:start new_text;
794      end;
795    end;
796    self#moveMark (Glib.Utf8.length new_text);
797    buffer#insert ~iter:(buffer#get_iter_at_mark (`MARK locked_mark)) newtext;
798    (* here we need to set the Goal in case we are going to cursor (or to
799       bottom) and we will face a macro *)
800    match self#grafite_status.proof_status with
801       Incomplete_proof p ->
802        userGoal <-
803          (try Some (Continuationals.Stack.find_goal p.stack)
804          with Failure _ -> None)
805     | _ -> userGoal <- None
806
807   method private _retract offset lexicon_status grafite_status new_statements
808    new_history
809   =
810    let cur_grafite_status,cur_lexicon_status =
811     match history with s::_ -> s | [] -> assert false
812    in
813     LexiconSync.time_travel ~present:cur_lexicon_status ~past:lexicon_status;
814     GrafiteSync.time_travel ~present:cur_grafite_status ~past:grafite_status;
815     statements <- new_statements;
816     history <- new_history;
817     self#moveMark (- offset)
818
819   method advance ?statement () =
820     try
821       self#_advance ?statement ();
822       self#notify
823     with 
824     | Margin -> self#notify
825     | Not_found -> assert false
826     | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
827     | exc -> self#notify; raise exc
828
829   method retract () =
830     try
831       let cmp,new_statements,new_history,(grafite_status,lexicon_status) =
832        match statements,history with
833           stat::statements, _::(status::_ as history) ->
834            assert (Glib.Utf8.validate stat);
835            Glib.Utf8.length stat, statements, history, status
836        | [],[_] -> raise Margin
837        | _,_ -> assert false
838       in
839        self#_retract cmp lexicon_status grafite_status new_statements
840         new_history;
841        self#notify
842     with 
843     | Margin -> self#notify
844     | Invalid_argument "Array.make" -> HLog.error "The script is too big!\n"
845     | exc -> self#notify; raise exc
846
847   method private getFuture =
848     buffer#get_text ~start:(buffer#get_iter_at_mark (`MARK locked_mark))
849       ~stop:buffer#end_iter ()
850
851       
852   (** @param rel_offset relative offset from current position of locked_mark *)
853   method private moveMark rel_offset =
854     let mark = `MARK locked_mark in
855     let old_insert = buffer#get_iter_at_mark `INSERT in
856     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
857     let current_mark_pos = buffer#get_iter_at_mark mark in
858     let new_mark_pos =
859       match rel_offset with
860       | 0 -> current_mark_pos
861       | n when n > 0 -> current_mark_pos#forward_chars n
862       | n (* when n < 0 *) -> current_mark_pos#backward_chars (abs n)
863     in
864     buffer#move_mark mark ~where:new_mark_pos;
865     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:new_mark_pos;
866     buffer#move_mark `INSERT old_insert;
867     let mark_position = buffer#get_iter_at_mark mark in
868     if source_view#move_mark_onscreen mark then
869      begin
870       buffer#move_mark mark mark_position;
871       source_view#scroll_to_mark ~use_align:true ~xalign:1.0 ~yalign:0.1 mark;
872      end;
873     while Glib.Main.pending () do ignore(Glib.Main.iteration false); done
874
875   method clean_dirty_lock =
876     let lock_mark_iter = buffer#get_iter_at_mark (`MARK locked_mark) in
877     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
878     buffer#apply_tag locked_tag ~start:buffer#start_iter ~stop:lock_mark_iter
879
880   val mutable observers = []
881
882   method addObserver (o: LexiconEngine.status -> GrafiteTypes.status -> unit) =
883     observers <- o :: observers
884
885   method private notify =
886     let lexicon_status = self#lexicon_status in
887     let grafite_status = self#grafite_status in
888     List.iter (fun o -> o lexicon_status grafite_status) observers
889
890   method loadFromString s =
891     buffer#set_text s;
892     self#reset_buffer;
893     buffer#set_modified true
894
895   method loadFromFile f =
896     buffer#set_text (HExtlib.input_file f);
897     self#reset_buffer;
898     buffer#set_modified false
899
900   method assignFileName file =
901     let file = 
902       match file with 
903       | Some f -> Some (Librarian.absolutize f)
904       | None -> None
905     in
906     self#goto_top;
907     filename_ <- file; 
908     include_paths_ <- 
909       (match file with Some file -> read_include_paths file | None -> []);
910     self#reset_buffer;
911     Sys.chdir self#curdir;
912     HLog.debug ("Moving to " ^ Sys.getcwd ())
913     
914   method saveToFile () =
915     if self#has_name then
916       let oc = open_out self#filename in
917       output_string oc (buffer#get_text ~start:buffer#start_iter
918                         ~stop:buffer#end_iter ());
919       close_out oc;
920       set_star false;
921       buffer#set_modified false
922     else
923       HLog.error "Can't save, no filename selected"
924   
925   method private _saveToBackupFile () =
926     if buffer#modified then
927       begin
928         let f = self#filename in
929         let oc = open_out f in
930         output_string oc (buffer#get_text ~start:buffer#start_iter
931                             ~stop:buffer#end_iter ());
932         close_out oc;
933         HLog.debug ("backup " ^ f ^ " saved")                    
934       end
935   
936   method private goto_top =
937     let grafite_status,lexicon_status = 
938       let rec last x = function 
939       | [] -> x
940       | hd::tl -> last hd tl
941       in
942       last (self#grafite_status,self#lexicon_status) history
943     in
944     (* FIXME: this is not correct since there is no undo for 
945      * library_objects.set_default... *)
946     GrafiteSync.time_travel ~present:self#grafite_status ~past:grafite_status;
947     LexiconSync.time_travel ~present:self#lexicon_status ~past:lexicon_status
948
949   method private reset_buffer = 
950     statements <- [];
951     history <- [ initial_statuses self#buri_of_current_file ];
952     userGoal <- None;
953     self#notify;
954     buffer#remove_tag locked_tag ~start:buffer#start_iter ~stop:buffer#end_iter;
955     buffer#move_mark (`MARK locked_mark) ~where:buffer#start_iter
956
957   method reset () =
958     self#reset_buffer;
959     source_buffer#begin_not_undoable_action ();
960     buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter;
961     source_buffer#end_not_undoable_action ();
962     buffer#set_modified false;
963   
964   method template () =
965     let template = HExtlib.input_file BuildTimeConf.script_template in 
966     buffer#insert ~iter:(buffer#get_iter `START) template;
967     buffer#set_modified false;
968     set_star false
969
970   method goto (pos: [`Top | `Bottom | `Cursor]) () =
971   try  
972     let old_locked_mark =
973      `MARK
974        (buffer#create_mark ~name:"old_locked_mark"
975          ~left_gravity:true (buffer#get_iter_at_mark (`MARK locked_mark))) in
976     let getpos _ = buffer#get_iter_at_mark (`MARK locked_mark) in 
977     let getoldpos _ = buffer#get_iter_at_mark old_locked_mark in 
978     let dispose_old_locked_mark () = buffer#delete_mark old_locked_mark in
979     match pos with
980     | `Top -> 
981         dispose_old_locked_mark (); 
982         self#goto_top; 
983         self#reset_buffer;
984         self#notify
985     | `Bottom ->
986         (try 
987           let rec dowhile () =
988             self#_advance ();
989             let newpos = getpos () in
990             if (getoldpos ())#compare newpos < 0 then
991               begin
992                 buffer#move_mark old_locked_mark newpos;
993                 dowhile ()
994               end
995           in
996           dowhile ();
997           dispose_old_locked_mark ();
998           self#notify 
999         with 
1000         | Margin -> dispose_old_locked_mark (); self#notify
1001         | exc -> dispose_old_locked_mark (); self#notify; raise exc)
1002     | `Cursor ->
1003         let locked_iter () = buffer#get_iter_at_mark (`NAME "locked") in
1004         let cursor_iter () = buffer#get_iter_at_mark `INSERT in
1005         let remember =
1006          `MARK
1007            (buffer#create_mark ~name:"initial_insert"
1008              ~left_gravity:true (cursor_iter ())) in
1009         let dispose_remember () = buffer#delete_mark remember in
1010         let remember_iter () =
1011          buffer#get_iter_at_mark (`NAME "initial_insert") in
1012         let cmp () = (locked_iter ())#offset - (remember_iter ())#offset in
1013         let icmp = cmp () in
1014         let forward_until_cursor () = (* go forward until locked > cursor *)
1015           let rec aux () =
1016             self#_advance ();
1017             if cmp () < 0 && (getoldpos ())#compare (getpos ()) < 0 
1018             then
1019              begin
1020               buffer#move_mark old_locked_mark (getpos ());
1021               aux ()
1022              end
1023           in
1024           aux ()
1025         in
1026         let rec back_until_cursor len = (* go backward until locked < cursor *)
1027          function
1028             statements, ((grafite_status,lexicon_status)::_ as history)
1029             when len <= 0 ->
1030              self#_retract (icmp - len) lexicon_status grafite_status statements
1031               history
1032           | statement::tl1, _::tl2 ->
1033              back_until_cursor (len - MatitaGtkMisc.utf8_string_length statement) (tl1,tl2)
1034           | _,_ -> assert false
1035         in
1036         (try
1037           begin
1038            if icmp < 0 then       (* locked < cursor *)
1039              (forward_until_cursor (); self#notify)
1040            else if icmp > 0 then  (* locked > cursor *)
1041              (back_until_cursor icmp (statements,history); self#notify)
1042            else                  (* cursor = locked *)
1043                ()
1044           end ;
1045           dispose_remember ();
1046           dispose_old_locked_mark ();
1047         with 
1048         | Margin -> dispose_remember (); dispose_old_locked_mark (); self#notify
1049         | exc -> dispose_remember (); dispose_old_locked_mark ();
1050                  self#notify; raise exc)
1051   with Invalid_argument "Array.make" ->
1052      HLog.error "The script is too big!\n"
1053   
1054   method onGoingProof () =
1055     match self#grafite_status.proof_status with
1056     | No_proof | Proof _ -> false
1057     | Incomplete_proof _ -> true
1058     | Intermediate _ -> assert false
1059
1060 (*   method proofStatus = MatitaTypes.get_proof_status self#status *)
1061   method proofMetasenv = GrafiteTypes.get_proof_metasenv self#grafite_status
1062
1063   method proofContext =
1064    match userGoal with
1065       None -> []
1066     | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
1067
1068   method proofConclusion =
1069    match userGoal with
1070       None -> assert false
1071     | Some n ->
1072        GrafiteTypes.get_proof_conclusion self#grafite_status n
1073
1074   method stack = GrafiteTypes.get_stack self#grafite_status
1075   method setGoal n = userGoal <- n
1076   method goal = userGoal
1077
1078   method bos = 
1079     match history with
1080     | _::[] -> true
1081     | _ -> false
1082
1083   method eos = 
1084     let rec is_there_only_comments lexicon_status s = 
1085       if Pcre.pmatch ~rex:only_dust_RE s then raise Margin;
1086       let lexicon_status,st =
1087        GrafiteParser.parse_statement (Ulexing.from_utf8_string s)
1088         ~include_paths:self#include_paths lexicon_status
1089       in
1090       match st with
1091       | GrafiteParser.LSome (GrafiteAst.Comment (loc,_)) -> 
1092           let _,parsed_text_length = MatitaGtkMisc.utf8_parsed_text s loc in
1093           (* CSC: why +1 in the following lines ???? *)
1094           let parsed_text_length = parsed_text_length + 1 in
1095           let remain_len = String.length s - parsed_text_length in
1096           let next = String.sub s parsed_text_length remain_len in
1097           is_there_only_comments lexicon_status next
1098       | GrafiteParser.LNone _
1099       | GrafiteParser.LSome (GrafiteAst.Executable _) -> false
1100     in
1101     try
1102       is_there_only_comments self#lexicon_status self#getFuture
1103     with 
1104     | LexiconEngine.IncludedFileNotCompiled _
1105     | HExtlib.Localized _
1106     | CicNotationParser.Parse_error _ -> false
1107     | Margin | End_of_file -> true
1108     | Invalid_argument "Array.make" -> false
1109
1110   (* debug *)
1111   method dump () =
1112     HLog.debug "script status:";
1113     HLog.debug ("history size: " ^ string_of_int (List.length history));
1114     HLog.debug (sprintf "%d statements:" (List.length statements));
1115     List.iter HLog.debug statements;
1116     HLog.debug ("Current file name: " ^ self#filename);
1117 end
1118
1119 let _script = ref None
1120
1121 let script ~source_view ~mathviewer ~urichooser ~ask_confirmation ~set_star ()
1122 =
1123   let s = new script 
1124     ~source_view ~mathviewer ~ask_confirmation ~urichooser ~set_star () 
1125   in
1126   _script := Some s;
1127   s
1128
1129 let current () = match !_script with None -> assert false | Some s -> s
1130