]> matita.cs.unibo.it Git - helm.git/blob - components/grafite_engine/grafiteEngine.ml
Bug fixed in pretty printing in new syntax of MutCases on inductive types
[helm.git] / components / grafite_engine / grafiteEngine.ml
1 (* Copyright (C) 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 module GT = GrafiteTypes
29
30 open Printf
31
32 exception Drop
33 (* mo file name, ma file name *)
34 exception IncludedFileNotCompiled of string * string 
35 exception Macro of
36  GrafiteAst.loc *
37   (Cic.context -> GT.status * Cic.term GrafiteAst.macro)
38 exception ReadOnlyUri of string
39
40 type 'a disambiguator_input = string * int * 'a
41
42 type options = { 
43   do_heavy_checks: bool ; 
44   clean_baseuri: bool
45 }
46
47 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
48   * names as long as they are available, then it fallbacks to name generation
49   * using FreshNamesGenerator module *)
50 let namer_of names =
51   let len = List.length names in
52   let count = ref 0 in
53   fun metasenv context name ~typ ->
54     if !count < len then begin
55       let name = Cic.Name (List.nth names !count) in
56       incr count;
57       name
58     end else
59       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
60
61 let tactic_of_ast ast =
62   let module PET = ProofEngineTypes in
63   match ast with
64   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
65   | GrafiteAst.Apply (_, term) -> Tactics.apply term
66   | GrafiteAst.ApplyS (_, term) ->
67      Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
68   | GrafiteAst.Assumption _ -> Tactics.assumption
69   | GrafiteAst.Auto (_,params) ->
70       AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
71   | GrafiteAst.Change (_, pattern, with_what) ->
72      Tactics.change ~pattern with_what
73   | GrafiteAst.Clear (_,id) -> Tactics.clear id
74   | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
75   | GrafiteAst.Contradiction _ -> Tactics.contradiction
76   | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
77   | GrafiteAst.Cut (_, ident, term) ->
78      let names = match ident with None -> [] | Some id -> [id] in
79      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
80   | GrafiteAst.Decompose (_, types, what, names) -> 
81       let to_type = function
82          | GrafiteAst.Type (uri, typeno) -> uri, typeno
83          | GrafiteAst.Ident _            -> assert false
84       in
85       let user_types = List.rev_map to_type types in
86       let dbd = LibraryDb.instance () in
87       let mk_fresh_name_callback = namer_of names in
88       Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
89   | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
90   | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
91   | GrafiteAst.Elim (_, what, using, depth, names) ->
92       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
93         what
94   | GrafiteAst.ElimType (_, what, using, depth, names) ->
95       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
96         what
97   | GrafiteAst.Exact (_, term) -> Tactics.exact term
98   | GrafiteAst.Exists _ -> Tactics.exists
99   | GrafiteAst.Fail _ -> Tactics.fail
100   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
101       let reduction =
102         match reduction_kind with
103         | `Normalize ->
104             PET.const_lazy_reduction
105               (CicReduction.normalize ~delta:false ~subst:[])
106         | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
107         | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
108         | `Unfold None ->
109             PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
110         | `Unfold (Some lazy_term) ->
111            (fun context metasenv ugraph ->
112              let what, metasenv, ugraph = lazy_term context metasenv ugraph in
113              ProofEngineReduction.unfold ~what, metasenv, ugraph)
114         | `Whd ->
115             PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[])
116       in
117       Tactics.fold ~reduction ~term ~pattern
118   | GrafiteAst.Fourier _ -> Tactics.fourier
119   | GrafiteAst.FwdSimpl (_, hyp, names) -> 
120      Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
121       ~dbd:(LibraryDb.instance ()) hyp
122   | GrafiteAst.Generalize (_,pattern,ident) ->
123      let names = match ident with None -> [] | Some id -> [id] in
124      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
125   | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
126   | GrafiteAst.IdTac _ -> Tactics.id
127   | GrafiteAst.Injection (_,term) -> Tactics.injection term
128   | GrafiteAst.Intros (_, None, names) ->
129       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
130   | GrafiteAst.Intros (_, Some num, names) ->
131       PrimitiveTactics.intros_tac ~howmany:num
132         ~mk_fresh_name_callback:(namer_of names) ()
133   | GrafiteAst.Inversion (_, term) ->
134       Tactics.inversion term
135   | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
136       let names = match ident with None -> [] | Some id -> [id] in
137       Tactics.lapply ~mk_fresh_name_callback:(namer_of names) 
138         ~linear ?how_many ~to_what what
139   | GrafiteAst.Left _ -> Tactics.left
140   | GrafiteAst.LetIn (loc,term,name) ->
141       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
142   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
143       (match reduction_kind with
144          | `Normalize -> Tactics.normalize ~pattern
145          | `Reduce -> Tactics.reduce ~pattern  
146          | `Simpl -> Tactics.simpl ~pattern 
147          | `Unfold what -> Tactics.unfold ~pattern what
148          | `Whd -> Tactics.whd ~pattern)
149   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
150   | GrafiteAst.Replace (_, pattern, with_what) ->
151      Tactics.replace ~pattern ~with_what
152   | GrafiteAst.Rewrite (_, direction, t, pattern) ->
153      EqualityTactics.rewrite_tac ~direction ~pattern t
154   | GrafiteAst.Right _ -> Tactics.right
155   | GrafiteAst.Ring _ -> Tactics.ring
156   | GrafiteAst.Split _ -> Tactics.split
157   | GrafiteAst.Subst _ -> Tactics.subst
158   | GrafiteAst.Symmetry _ -> Tactics.symmetry
159   | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
160   (* Implementazioni Aggiunte *)
161   | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
162   | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1
163   | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) ->
164      Declarative.by_term_we_proved ~dbd:(LibraryDb.instance()) t ty id t1
165   | GrafiteAst.We_need_to_prove (_, t, id, t2) ->
166      Declarative.we_need_to_prove t id t2
167   | GrafiteAst.Bydone (_, t) -> Declarative.bydone ~dbd:(LibraryDb.instance()) t
168   | GrafiteAst.We_proceed_by_induction_on (_, t, t1) ->
169      Declarative.we_proceed_by_induction_on t t1
170   | GrafiteAst.Byinduction (_, t, id) -> Declarative.byinduction t id
171   | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t
172   | GrafiteAst.ExistsElim (_, t, id1, t1, id2, t2) ->
173      Declarative.existselim t id1 t1 id2 t2
174   | GrafiteAst.Case (_,id,params) -> Declarative.case id params
175   | GrafiteAst.AndElim(_,t,id1,t1,id2,t2) -> Declarative.andelim t id1 t1 id2 t2
176   | GrafiteAst.RewritingStep (_,termine,t1,t2,cont) ->
177      Declarative.rewritingstep ~dbd:(LibraryDb.instance ()) termine t1 t2 cont
178
179 let classify_tactic tactic = 
180   match tactic with
181   (* tactics that can't close the goal (return a goal we want to "select") *)
182   | GrafiteAst.Rewrite _ 
183   | GrafiteAst.Split _ 
184   | GrafiteAst.Replace _ 
185   | GrafiteAst.Reduce _
186   | GrafiteAst.Injection _ 
187   | GrafiteAst.IdTac _ 
188   | GrafiteAst.Generalize _ 
189   | GrafiteAst.Elim _ 
190   | GrafiteAst.Cut _
191   | GrafiteAst.Decompose _ -> true, true
192   (* tactics we don't want to reorder goals. I think only Goal needs this. *)
193   | GrafiteAst.Goal _ -> false, true
194   (* tactics like apply *)
195   | _ -> true, false
196   
197 let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
198   let module PEH = ProofEngineHelpers in
199 (*   let print_m name metasenv =
200     prerr_endline (">>>>> " ^ name);
201     prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)
202   in *)
203   (* phase one calculates:
204    *   new_goals_from_refine:  goals added by refine
205    *   head_goal:              the first goal opened by ythe tactic 
206    *   other_goals:            other goals opened by the tactic
207    *)
208   let new_goals_from_refine = PEH.compare_metasenvs start refine in
209   let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
210   let head_goal, other_goals, goals = 
211     match goals with
212     | [] -> None,[],goals
213     | hd::tl -> 
214         (* assert (List.mem hd new_goals_from_tactic);
215          * invalidato dalla goal_tac
216          * *)
217         Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
218         hd) goals
219   in
220   let produced_goals = 
221     match head_goal with
222     | None -> new_goals_from_refine @ other_goals
223     | Some x -> x :: new_goals_from_refine @ other_goals
224   in
225   (* extract the metas generated by refine and tactic *)
226   let metas_for_tactic_head = 
227     match head_goal with
228     | None -> []
229     | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
230   let metas_for_tactic_goals = 
231     List.map 
232       (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
233     goals 
234   in
235   let metas_for_refine_goals = 
236     List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
237   let produced_metas, goals = 
238     let produced_metas =
239       if always_opens_a_goal then
240         metas_for_tactic_head @ metas_for_refine_goals @ 
241           metas_for_tactic_goals
242       else begin
243 (*         print_m "metas_for_refine_goals" metas_for_refine_goals;
244         print_m "metas_for_tactic_head" metas_for_tactic_head;
245         print_m "metas_for_tactic_goals" metas_for_tactic_goals; *)
246         metas_for_refine_goals @ metas_for_tactic_head @ 
247           metas_for_tactic_goals
248       end
249     in
250     let goals = List.map (fun (metano, _, _) -> metano)  produced_metas in
251     produced_metas, goals
252   in
253   (* residual metas, preserving the original order *)
254   let before, after = 
255     let rec split e =
256       function 
257       | [] -> [],[]
258       | (metano, _, _) :: tl when metano = e -> 
259           [], List.map (fun (x,_,_) -> x) tl
260       | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
261     in
262     let find n metasenv =
263       try
264         Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
265       with Not_found -> None
266     in
267     let extract l =
268       List.fold_right 
269         (fun n acc -> 
270           match find n tactic with
271           | Some x -> x::acc
272           | None -> acc
273         ) l [] in
274     let before_l, after_l = split current_goal start in
275     let before_l = 
276       List.filter (fun x -> not (List.mem x produced_goals)) before_l in
277     let after_l = 
278       List.filter (fun x -> not (List.mem x produced_goals)) after_l in
279     let before = extract before_l in
280     let after = extract after_l in
281       before, after
282   in
283 (* |+   DEBUG CODE  +|
284   print_m "BEGIN" start;
285   prerr_endline ("goal was: " ^ string_of_int current_goal);
286   prerr_endline ("and metas from refine are:");
287   List.iter 
288     (fun t -> prerr_string (" " ^ string_of_int t)) 
289   new_goals_from_refine;
290   prerr_endline "";
291   print_m "before" before;
292   print_m "metas_for_tactic_head" metas_for_tactic_head;
293   print_m "metas_for_refine_goals" metas_for_refine_goals;
294   print_m "metas_for_tactic_goals" metas_for_tactic_goals;
295   print_m "produced_metas" produced_metas;
296   print_m "after" after; 
297 |+   FINE DEBUG CODE +| *)
298   before @ produced_metas @ after, goals 
299   
300 let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) =
301 (* prerr_endline "apply_tactic"; *)
302 (* prerr_endline (Continuationals.Stack.pp (GT.get_stack status)); *)
303  let starting_metasenv = GT.get_proof_metasenv status in
304  let before = List.map (fun g, _, _ -> g) starting_metasenv in
305 (* prerr_endline "disambiguate"; *)
306  let status, tactic = disambiguate_tactic status goal (text,prefix_len,tactic) in
307  let metasenv_after_refinement =  GT.get_proof_metasenv status in
308  let proof = GT.get_current_proof status in
309  let proof_status = proof, goal in
310  let needs_reordering, always_opens_a_goal = classify_tactic tactic in
311  let tactic = tactic_of_ast tactic in
312  (* apply tactic will change the lexicon_status ... *)
313 (* prerr_endline "apply_tactic bassa"; *)
314  let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
315  let after = ProofEngineTypes.goals_of_proof proof in
316  let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
317 (* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before));
318 prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after));
319 prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *)
320 (* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals));
321 prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *)
322  let proof, opened_goals = 
323    if needs_reordering then begin
324      let uri, metasenv_after_tactic, t, ty = proof in
325 (* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *)
326      let reordered_metasenv, opened_goals = 
327        reorder_metasenv
328         starting_metasenv
329         metasenv_after_refinement metasenv_after_tactic
330         opened goal always_opens_a_goal
331      in
332      let proof' = uri, reordered_metasenv, t, ty in
333 (* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *)
334      proof', opened_goals
335    end
336       else
337         proof, opened_goals
338  in
339  let incomplete_proof =
340    match status.GT.proof_status with
341    | GT.Incomplete_proof p -> p
342    | _ -> assert false
343  in
344  { status with GT.proof_status =
345     GT.Incomplete_proof
346      { incomplete_proof with GT.proof = proof } },
347  opened_goals, closed_goals
348
349 type eval_ast =
350  {ea_go:
351   'term 'lazy_term 'reduction 'obj 'ident.
352   disambiguate_tactic:
353    (GT.status ->
354     ProofEngineTypes.goal ->
355     (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic)
356     disambiguator_input ->
357     GT.status *
358    (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
359
360   disambiguate_command:
361    (GT.status ->
362     ('obj GrafiteAst.command) disambiguator_input ->
363     GT.status * Cic.obj GrafiteAst.command) ->
364
365   disambiguate_macro:
366    (GT.status ->
367     ('term GrafiteAst.macro) disambiguator_input ->
368     Cic.context -> GT.status * Cic.term GrafiteAst.macro) ->
369
370   ?do_heavy_checks:bool ->
371   ?clean_baseuri:bool ->
372   GT.status ->
373   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement)
374   disambiguator_input ->
375   GT.status * UriManager.uri list
376  }
377
378 type 'a eval_command =
379  {ec_go: 'term 'obj.
380   disambiguate_command:
381    (GT.status -> ('obj GrafiteAst.command) disambiguator_input ->
382     GT.status * Cic.obj GrafiteAst.command) -> 
383   options -> GT.status -> 
384     ('obj GrafiteAst.command) disambiguator_input ->
385    GT.status * UriManager.uri list
386  }
387
388 type 'a eval_executable =
389  {ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
390   disambiguate_tactic:
391    (GT.status ->
392     ProofEngineTypes.goal ->
393     (('term, 'lazy_term, 'reduction, 'ident) GrafiteAst.tactic)
394     disambiguator_input ->
395     GT.status *
396    (Cic.term, Cic.lazy_term, Cic.lazy_term GrafiteAst.reduction, string) GrafiteAst.tactic) ->
397
398   disambiguate_command:
399    (GT.status ->
400     ('obj GrafiteAst.command) disambiguator_input ->
401     GT.status * Cic.obj GrafiteAst.command) ->
402
403   disambiguate_macro:
404    (GT.status ->
405     ('term GrafiteAst.macro) disambiguator_input ->
406     Cic.context -> GT.status * Cic.term GrafiteAst.macro) ->
407
408   options ->
409   GT.status ->
410   (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input ->
411   GT.status * UriManager.uri list
412  }
413
414 type 'a eval_from_moo =
415  { efm_go: GT.status -> string -> GT.status }
416       
417 let coercion_moo_statement_of arity uri =
418   GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false, arity)
419
420 let refinement_toolkit = {
421   RefinementTool.type_of_aux' = 
422     (fun ?localization_tbl e c t u ->
423       let saved = !CicRefine.insert_coercions in 
424       CicRefine.insert_coercions:= false;
425       let rc = 
426         try 
427           let t, ty, metasenv, ugraph = 
428             CicRefine.type_of_aux' ?localization_tbl e c t u in
429           RefinementTool.Success (t, ty, metasenv, ugraph)
430         with
431         | CicRefine.RefineFailure s
432         | CicRefine.Uncertain s 
433         | CicRefine.AssertFailure s -> RefinementTool.Exception s
434       in
435       CicRefine.insert_coercions := saved;
436       rc);
437   RefinementTool.ppsubst = CicMetaSubst.ppsubst;
438   RefinementTool.apply_subst = CicMetaSubst.apply_subst; 
439   RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv; 
440   RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
441  }
442   
443 let eval_coercion status ~add_composites uri arity =
444  let status,compounds =
445   GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri arity 
446  in
447  let moo_content = 
448    List.map (coercion_moo_statement_of arity) (uri::compounds)
449  in
450  let status = GT.add_moo_content moo_content status in
451   {status with GT.proof_status = GT.No_proof},
452    compounds
453
454 let eval_tactical ~disambiguate_tactic status tac =
455  let apply_tactic = apply_tactic ~disambiguate_tactic in
456  let module MatitaStatus =
457   struct
458    type input_status = GT.status * ProofEngineTypes.goal
459  
460    type output_status =
461      GT.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
462  
463    type tactic = input_status -> output_status
464  
465    let id_tactic = apply_tactic ("",0,(GrafiteAst.IdTac HExtlib.dummy_floc))
466    let mk_tactic tac = tac
467    let apply_tactic tac = tac
468    let goals (_, opened, closed) = opened, closed
469    let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
470    let get_stack (status, _) = GT.get_stack status
471    
472    let get_status (status, goal) =
473       match status.GT.proof_status with
474          | GT.Incomplete_proof incomplete -> incomplete.GT.proof, goal
475          | _                              -> assert false
476       
477    let get_proof (status, _, _) =
478       match status.GT.proof_status with
479          | GT.Incomplete_proof incomplete -> incomplete.GT.proof
480          | _                              -> assert false
481  
482    let set_stack stack (status, opened, closed) = 
483      GT.set_stack stack status, opened, closed
484  
485    let inject (status, _) = (status, [], [])
486    let focus goal (status, _, _) = (status, goal)
487   end
488  in
489  let module MatitaTacticals = Tacticals.Make (MatitaStatus) in
490   let rec tactical_of_ast l (text,prefix_len,tac) =
491     let apply_tactic t = apply_tactic (text, prefix_len, t) in
492     let tactical_of_ast l t = tactical_of_ast l (text,prefix_len,t) in
493     match tac with
494     | GrafiteAst.Tactic (loc, tactic) ->
495         MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
496     | GrafiteAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
497        assert (l > 0);
498        MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
499     | GrafiteAst.Do (loc, n, tactical) ->
500         MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
501     | GrafiteAst.Repeat (loc, tactical) ->
502         MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
503     | GrafiteAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
504         assert (l > 0);
505         MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
506           ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
507     | GrafiteAst.First (loc, tacticals) ->
508         MatitaTacticals.first
509           ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
510     | GrafiteAst.Try (loc, tactical) ->
511         MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
512     | GrafiteAst.Solve (loc, tacticals) ->
513         MatitaTacticals.solve_tactics
514          ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
515     | GrafiteAst.Progress (loc, tactical) ->
516         MatitaTacticals.progress_tactic ~tactic:(tactical_of_ast (l+1) tactical)
517
518     | GrafiteAst.Skip _loc -> MatitaTacticals.skip
519     | GrafiteAst.Dot _loc -> MatitaTacticals.dot
520     | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
521     | GrafiteAst.Branch _loc -> MatitaTacticals.branch
522     | GrafiteAst.Shift _loc -> MatitaTacticals.shift
523     | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
524     | GrafiteAst.Merge _loc -> MatitaTacticals.merge
525     | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
526     | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
527     | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
528   in
529   let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
530   let status =  (* is proof completed? *)
531     match status.GT.proof_status with
532     | GT.Incomplete_proof
533        { GT.stack = stack; proof = proof }
534       when Continuationals.Stack.is_empty stack ->
535         { status with GT.proof_status = GT.Proof proof }
536     | _ -> status
537   in
538   status
539
540 let eval_comment status c = status
541
542 (* since the record syntax allows to declare coercions, we have to put this
543  * information inside the moo *)
544 let add_coercions_of_record_to_moo obj lemmas status =
545   let attributes = CicUtil.attributes_of_obj obj in
546   let is_record = function `Class (`Record att) -> Some att | _-> None in
547   match HExtlib.list_findopt is_record attributes with
548   | None -> status,[]
549   | Some fields -> 
550       let is_a_coercion uri =
551         try
552           let obj,_ = 
553             CicEnvironment.get_cooked_obj  CicUniv.empty_ugraph uri in
554           let attrs = CicUtil.attributes_of_obj obj in
555           try 
556             match List.find 
557              (function `Class (`Coercion _) -> true | _-> false) attrs
558             with `Class (`Coercion n) -> true,n | _ -> assert false
559           with Not_found -> false,0            
560         with Not_found -> assert false
561       in
562       (* looking at the fields we can know the 'wanted' coercions, but not the 
563        * actually generated ones. So, only the intersection between the wanted
564        * and the actual should be in the moo as coercion, while everithing in
565        * lemmas should go as aliases *)
566       let wanted_coercions = 
567         HExtlib.filter_map 
568           (function 
569             | (name,true,arity) -> 
570                Some 
571                  (arity, UriManager.uri_of_string 
572                    (GT.qualify status name ^ ".con"))
573             | _ -> None) 
574           fields
575       in
576       (*prerr_endline "wanted coercions:";
577       List.iter 
578         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
579         wanted_coercions; *)
580       let coercions, moo_content = 
581         List.split
582           (HExtlib.filter_map 
583             (fun uri ->
584               let is_a_wanted_coercion,arity_wanted = 
585                 try
586                   let arity,_ = 
587                     List.find (fun (n,u) -> UriManager.eq u uri) 
588                       wanted_coercions
589                   in
590                   true, arity
591                 with Not_found -> false, 0
592               in
593               let is_a_coercion, arity_coercion = is_a_coercion uri in
594               if is_a_coercion then
595                 Some (uri, coercion_moo_statement_of arity_coercion uri)
596               else if is_a_wanted_coercion then
597                 Some (uri, coercion_moo_statement_of arity_wanted uri)
598               else
599                 None)
600             lemmas)
601       in
602       (*prerr_endline "actual coercions:";
603       List.iter 
604         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
605         coercions; 
606       prerr_endline "lemmas was:";
607       List.iter 
608         (fun u -> prerr_endline (UriManager.string_of_uri u)) 
609         lemmas; *)
610       let status = GT.add_moo_content moo_content status in 
611       {status with 
612         GT.coercions = coercions @ status.GT.coercions}, 
613       lemmas
614
615 let add_obj uri obj status =
616  let status,lemmas = GrafiteSync.add_obj refinement_toolkit uri obj status in
617  status, lemmas 
618       
619 let rec eval_command = {ec_go = fun ~disambiguate_command opts status
620 (text,prefix_len,cmd) ->
621  let status,cmd = disambiguate_command status (text,prefix_len,cmd) in
622  let status,uris =
623   match cmd with
624   | GrafiteAst.Print (_,"proofterm") ->
625       let _,_,p,_ = GT.get_current_proof status in
626       print_endline (AutoTactic.pp_proofterm p);
627       status,[]
628   | GrafiteAst.Print (_,_) -> status,[]
629   | GrafiteAst.Default (loc, what, uris) as cmd ->
630      LibraryObjects.set_default what uris;
631      GT.add_moo_content [cmd] status,[]
632   | GrafiteAst.Include (loc, baseuri) ->
633      let moopath_rw, moopath_r = 
634        LibraryMisc.obj_file_of_baseuri 
635          ~must_exist:false ~baseuri ~writable:true,
636        LibraryMisc.obj_file_of_baseuri 
637          ~must_exist:false ~baseuri ~writable:false
638      in
639      let moopath = 
640        if Sys.file_exists moopath_r then moopath_r else
641          if Sys.file_exists moopath_rw then moopath_rw else
642            raise (IncludedFileNotCompiled (moopath_rw,baseuri))
643      in
644      let status = eval_from_moo.efm_go status moopath in
645      status,[]
646   | GrafiteAst.Set (loc, name, value) -> 
647       if name = "baseuri" then begin
648         let value = 
649           let v = Http_getter_misc.strip_trailing_slash value in
650           try
651             ignore (String.index v ' ');
652             GT.command_error "baseuri can't contain spaces"
653           with Not_found -> v
654         in
655         if Http_getter_storage.is_read_only value then begin
656           HLog.error (sprintf "uri %s belongs to a read-only repository" value);
657           raise (ReadOnlyUri value)
658         end;
659         if not (Http_getter_storage.is_empty value) && 
660            opts.clean_baseuri 
661           then begin
662           HLog.message ("baseuri " ^ value ^ " is not empty");
663           HLog.message ("cleaning baseuri " ^ value);
664           LibraryClean.clean_baseuris [value];
665           assert (Http_getter_storage.is_empty value);
666         end;
667         if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk"
668                   ~default:false) 
669         then
670           HExtlib.mkdir 
671             (Filename.dirname (Http_getter.filename ~writable:true (value ^
672               "/foo.con")));
673       end;
674       GT.set_option status name value,[]
675   | GrafiteAst.Drop loc -> raise Drop
676   | GrafiteAst.Qed loc ->
677       let uri, metasenv, bo, ty =
678         match status.GT.proof_status with
679         | GT.Proof (Some uri, metasenv, body, ty) ->
680             uri, metasenv, body, ty
681         | GT.Proof (None, metasenv, body, ty) -> 
682             raise (GT.Command_error 
683               ("Someone allows to start a theorem without giving the "^
684                "name/uri. This should be fixed!"))
685         | _->
686           raise
687            (GT.Command_error "You can't Qed an incomplete theorem")
688       in
689       if metasenv <> [] then 
690         raise
691          (GT.Command_error
692            "Proof not completed! metasenv is not empty!");
693       let name = UriManager.name_of_uri uri in
694       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
695       let status, lemmas = add_obj uri obj status in
696        {status with GT.proof_status = GT.No_proof},
697         uri::lemmas
698   | GrafiteAst.Coercion (loc, uri, add_composites, arity) ->
699      eval_coercion status ~add_composites uri arity
700   | GrafiteAst.Obj (loc,obj) ->
701      let ext,name =
702       match obj with
703          Cic.Constant (name,_,_,_,_)
704        | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
705        | Cic.InductiveDefinition (types,_,_,_) ->
706           ".ind",
707           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
708        | _ -> assert false in
709      let uri = 
710        UriManager.uri_of_string (GT.qualify status name ^ ext) in
711      let obj = CicRefine.pack_coercion_obj obj in
712      let metasenv = GT.get_proof_metasenv status in
713      match obj with
714      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
715          let name = UriManager.name_of_uri uri in
716          if not(CicPp.check name ty) then
717            HLog.error ("Bad name: " ^ name);
718          if opts.do_heavy_checks then
719            begin
720              let dbd = LibraryDb.instance () in
721              let similar = Whelp.match_term ~dbd ty in
722              let similar_len = List.length similar in
723              if similar_len> 30 then
724                (HLog.message
725                  ("Duplicate check will compare your theorem with " ^ 
726                    string_of_int similar_len ^ 
727                    " theorems, this may take a while."));
728              let convertible =
729                List.filter (
730                  fun u ->
731                    let t = CicUtil.term_of_uri u in
732                    let ty',g = 
733                      CicTypeChecker.type_of_aux' 
734                        metasenv' [] t CicUniv.empty_ugraph
735                    in
736                    fst(CicReduction.are_convertible [] ty' ty g)) 
737                similar 
738              in
739              (match convertible with
740              | [] -> ()
741              | x::_ -> 
742                  HLog.warn  
743                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
744                   "\nPlease use a variant."));
745            end;
746          let initial_proof = (Some uri, metasenv', bo, ty) in
747          let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
748          { status with GT.proof_status =
749             GT.Incomplete_proof
750              { GT.proof = initial_proof; stack = initial_stack } },
751           []
752      | _ ->
753          if metasenv <> [] then
754           raise (GT.Command_error (
755             "metasenv not empty while giving a definition with body: " ^
756             CicMetaSubst.ppmetasenv [] metasenv));
757          let status, lemmas = add_obj uri obj status in 
758          let status,new_lemmas =
759           add_coercions_of_record_to_moo obj lemmas status
760          in
761           {status with GT.proof_status = GT.No_proof},
762            uri::new_lemmas@lemmas
763  in
764   match status.GT.proof_status with
765      GT.Intermediate _ ->
766       {status with GT.proof_status = GT.No_proof},uris
767    | _ -> status,uris
768
769 } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
770 ~disambiguate_macro opts status (text,prefix_len,ex) ->
771   match ex with
772   | GrafiteAst.Tactical (_, tac, None) ->
773      eval_tactical ~disambiguate_tactic status (text,prefix_len,tac),[]
774   | GrafiteAst.Tactical (_, tac, Some punct) ->
775      let status = 
776        eval_tactical ~disambiguate_tactic status (text,prefix_len,tac) in
777       eval_tactical ~disambiguate_tactic status (text,prefix_len,punct),[]
778   | GrafiteAst.Command (_, cmd) ->
779       eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
780   | GrafiteAst.Macro (loc, macro) ->
781      raise (Macro (loc,disambiguate_macro status (text,prefix_len,macro)))
782
783 } and eval_from_moo = {efm_go = fun status fname ->
784   let ast_of_cmd cmd =
785     ("",0,GrafiteAst.Executable (HExtlib.dummy_floc,
786       GrafiteAst.Command (HExtlib.dummy_floc,
787         cmd)))
788   in
789   let moo = GrafiteMarshal.load_moo fname in
790   List.fold_left 
791     (fun status ast -> 
792       let ast = ast_of_cmd ast in
793       let status,lemmas =
794        eval_ast.ea_go
795          ~disambiguate_tactic:(fun status _ (_,_,tactic) -> status,tactic)
796          ~disambiguate_command:(fun status (_,_,cmd) -> status,cmd)
797          ~disambiguate_macro:(fun _ _ -> assert false)
798          status ast
799       in
800        assert (lemmas=[]);
801        status)
802     status moo
803 } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
804 ~disambiguate_macro ?(do_heavy_checks=false) ?(clean_baseuri=true) status
805 (text,prefix_len,st)
806 ->
807   let opts = {
808     do_heavy_checks = do_heavy_checks ; 
809     clean_baseuri = clean_baseuri }
810   in
811   match st with
812   | GrafiteAst.Executable (_,ex) ->
813      eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command
814       ~disambiguate_macro opts status (text,prefix_len,ex)
815   | GrafiteAst.Comment (_,c) -> eval_comment status (text,prefix_len,c),[]
816 }
817
818 let eval_ast = eval_ast.ea_go