]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/matitaEngine.ml
bugfix: "LPAREN" vs LPAREN
[helm.git] / helm / matita / matitaEngine.ml
1
2 open Printf
3 open MatitaTypes
4
5 exception Drop;;
6
7 let debug = false ;;
8 let debug_print = if debug then prerr_endline else ignore ;;
9
10 type options = { do_heavy_checks: bool ; include_paths: string list }
11
12 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
13   * names as long as they are available, then it fallbacks to name generation
14   * using FreshNamesGenerator module *)
15 let namer_of names =
16   let len = List.length names in
17   let count = ref 0 in
18   fun metasenv context name ~typ ->
19     if !count < len then begin
20       let name = Cic.Name (List.nth names !count) in
21       incr count;
22       name
23     end else
24       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
25
26 let tactic_of_ast = function
27   | TacticAst.Absurd (_, term) -> Tactics.absurd term
28   | TacticAst.Apply (_, term) -> Tactics.apply term
29   | TacticAst.Assumption _ -> Tactics.assumption
30   | TacticAst.Auto (_,depth,width) -> 
31       AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
32   | TacticAst.Change (_, pattern, with_what) ->
33      Tactics.change ~pattern with_what
34   | TacticAst.Clear (_,id) -> Tactics.clear id
35   | TacticAst.ClearBody (_,id) -> Tactics.clearbody id
36   | TacticAst.Contradiction _ -> Tactics.contradiction
37   | TacticAst.Compare (_, term) -> Tactics.compare term
38   | TacticAst.Constructor (_, n) -> Tactics.constructor n
39   | TacticAst.Cut (_, ident, term) ->
40      let names = match ident with None -> [] | Some id -> [id] in
41      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
42   | TacticAst.DecideEquality _ -> Tactics.decide_equality
43   | TacticAst.Decompose (_,term) -> Tactics.decompose term
44   | TacticAst.Discriminate (_,term) -> Tactics.discriminate term
45   | TacticAst.Elim (_, what, using, depth, names) ->
46       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
47   | TacticAst.ElimType (_, what, using, depth, names) ->
48       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names) what
49   | TacticAst.Exact (_, term) -> Tactics.exact term
50   | TacticAst.Exists _ -> Tactics.exists
51   | TacticAst.Fail _ -> Tactics.fail
52   | TacticAst.Fold (_, reduction_kind, term, pattern) ->
53      let reduction =
54       match reduction_kind with
55        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
56        | `Reduce -> ProofEngineReduction.reduce
57        | `Simpl -> ProofEngineReduction.simpl
58        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
59      in
60       Tactics.fold ~reduction ~term ~pattern
61   | TacticAst.Fourier _ -> Tactics.fourier
62   | TacticAst.FwdSimpl (_, hyp, names) -> 
63      Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names) ~dbd:(MatitaDb.instance ()) hyp
64   | TacticAst.Generalize (_,pattern,ident) ->
65      let names = match ident with None -> [] | Some id -> [id] in
66      Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern 
67   | TacticAst.Goal (_, n) -> Tactics.set_goal n
68   | TacticAst.IdTac _ -> Tactics.id
69   | TacticAst.Injection (_,term) -> Tactics.injection term
70   | TacticAst.Intros (_, None, names) ->
71       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
72   | TacticAst.Intros (_, Some num, names) ->
73       PrimitiveTactics.intros_tac ~howmany:num
74         ~mk_fresh_name_callback:(namer_of names) ()
75   | TacticAst.LApply (_, how_many, to_what, what, ident) ->
76      let names = match ident with None -> [] | Some id -> [id] in
77      Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many ~to_what what
78   | TacticAst.Left _ -> Tactics.left
79   | TacticAst.LetIn (loc,term,name) ->
80       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
81   | TacticAst.Reduce (_, reduction_kind, pattern) ->
82       (match reduction_kind with
83       | `Normalize -> Tactics.normalize ~pattern
84       | `Reduce -> Tactics.reduce ~pattern  
85       | `Simpl -> Tactics.simpl ~pattern 
86       | `Whd -> Tactics.whd ~pattern)
87   | TacticAst.Reflexivity _ -> Tactics.reflexivity
88   | TacticAst.Replace (_, pattern, with_what) ->
89      Tactics.replace ~pattern ~with_what
90   | TacticAst.Rewrite (_, direction, t, pattern) ->
91      EqualityTactics.rewrite_tac ~direction ~pattern t
92   | TacticAst.Right _ -> Tactics.right
93   | TacticAst.Ring _ -> Tactics.ring
94   | TacticAst.Split _ -> Tactics.split
95   | TacticAst.Symmetry _ -> Tactics.symmetry
96   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
97
98 let disambiguate_term status term =
99   let (aliases, metasenv, cic, _) =
100     match
101       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
102         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
103         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
104     with
105     | [x] -> x
106     | _ -> assert false
107   in
108   let proof_status =
109     match status.proof_status with
110     | No_proof -> Intermediate metasenv
111     | Incomplete_proof ((uri, _, proof, ty), goal) ->
112         Incomplete_proof ((uri, metasenv, proof, ty), goal)
113     | Intermediate _ -> Intermediate metasenv 
114     | Proof _ -> assert false
115   in
116   let status = { status with proof_status = proof_status } in
117   let status = MatitaSync.set_proof_aliases status aliases in
118   status, cic
119   
120 let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
121   let interp path = Disambiguate.interpretate_path [] status.aliases path in
122   let goal_path = interp goal_path in
123   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
124   let status,wanted =
125    match wanted with
126       None -> status,None
127     | Some wanted ->
128        let status,wanted = disambiguate_term status wanted in
129         status, Some wanted
130   in
131    status, (wanted, hyp_paths ,goal_path)
132   
133 let disambiguate_tactic status = function
134   | TacticAst.Apply (loc, term) ->
135       let status, cic = disambiguate_term status term in
136       status, TacticAst.Apply (loc, cic)
137   | TacticAst.Absurd (loc, term) -> 
138       let status, cic = disambiguate_term status term in
139       status, TacticAst.Absurd (loc, cic)
140   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
141   | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
142   | TacticAst.Change (loc, pattern, with_what) -> 
143       let status, with_what = disambiguate_term status with_what in
144       let status, pattern = disambiguate_pattern status pattern in
145       status, TacticAst.Change (loc, pattern, with_what)
146   | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
147   | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
148   | TacticAst.Compare (loc,term) ->
149       let status, term = disambiguate_term status term in
150       status, TacticAst.Compare (loc,term)
151   | TacticAst.Constructor (loc,n) ->
152       status, TacticAst.Constructor (loc,n)
153   | TacticAst.Contradiction loc ->
154       status, TacticAst.Contradiction loc
155   | TacticAst.Cut (loc, ident, term) -> 
156       let status, cic = disambiguate_term status term in
157       status, TacticAst.Cut (loc, ident, cic)
158   | TacticAst.DecideEquality loc ->
159       status, TacticAst.DecideEquality loc
160   | TacticAst.Decompose (loc,term) ->
161       let status,term = disambiguate_term status term in
162       status, TacticAst.Decompose(loc,term)
163   | TacticAst.Discriminate (loc,term) ->
164       let status,term = disambiguate_term status term in
165       status, TacticAst.Discriminate(loc,term)
166   | TacticAst.Exact (loc, term) -> 
167       let status, cic = disambiguate_term status term in
168       status, TacticAst.Exact (loc, cic)
169   | TacticAst.Elim (loc, what, Some using, depth, idents) ->
170       let status, what = disambiguate_term status what in
171       let status, using = disambiguate_term status using in
172       status, TacticAst.Elim (loc, what, Some using, depth, idents)
173   | TacticAst.Elim (loc, what, None, depth, idents) ->
174       let status, what = disambiguate_term status what in
175       status, TacticAst.Elim (loc, what, None, depth, idents)
176   | TacticAst.ElimType (loc, what, Some using, depth, idents) ->
177       let status, what = disambiguate_term status what in
178       let status, using = disambiguate_term status using in
179       status, TacticAst.ElimType (loc, what, Some using, depth, idents)
180   | TacticAst.ElimType (loc, what, None, depth, idents) ->
181       let status, what = disambiguate_term status what in
182       status, TacticAst.ElimType (loc, what, None, depth, idents)
183   | TacticAst.Exists loc -> status, TacticAst.Exists loc 
184   | TacticAst.Fail loc -> status,TacticAst.Fail loc
185   | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
186      let status, pattern = disambiguate_pattern status pattern in
187      let status, term = disambiguate_term status term in
188      status, TacticAst.Fold (loc,reduction_kind, term, pattern)
189   | TacticAst.FwdSimpl (loc, hyp, names) ->
190      status, TacticAst.FwdSimpl (loc, hyp, names)  
191   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
192   | TacticAst.Generalize (loc,pattern,ident) ->
193       let status, pattern = disambiguate_pattern status pattern in
194       status, TacticAst.Generalize(loc,pattern,ident)
195   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
196   | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
197   | TacticAst.Injection (loc,term) ->
198       let status, term = disambiguate_term status term in
199       status, TacticAst.Injection (loc,term)
200   | TacticAst.Intros (loc, num, names) ->
201       status, TacticAst.Intros (loc, num, names)
202   | TacticAst.LApply (loc, depth, to_what, what, ident) ->
203      let f term (status, to_what) =
204         let status, term = disambiguate_term status term in
205         status, term :: to_what
206      in
207      let status, to_what = List.fold_right f to_what (status, []) in 
208      let status, what = disambiguate_term status what in
209      status, TacticAst.LApply (loc, depth, to_what, what, ident)
210   | TacticAst.Left loc -> status, TacticAst.Left loc
211   | TacticAst.LetIn (loc, term, name) ->
212       let status, term = disambiguate_term status term in
213       status, TacticAst.LetIn (loc,term,name)
214   | TacticAst.Reduce (loc, reduction_kind, pattern) ->
215       let status, pattern = disambiguate_pattern status pattern in
216       status, TacticAst.Reduce(loc, reduction_kind, pattern)
217   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
218   | TacticAst.Replace (loc, pattern, with_what) -> 
219       let status, pattern = disambiguate_pattern status pattern in
220       let status, with_what = disambiguate_term status with_what in
221       status, TacticAst.Replace (loc, pattern, with_what)
222   | TacticAst.Rewrite (loc, dir, t, pattern) ->
223       let status, term = disambiguate_term status t in
224       let status, pattern = disambiguate_pattern status pattern in
225       status, TacticAst.Rewrite (loc, dir, term, pattern)
226   | TacticAst.Right loc -> status, TacticAst.Right loc
227   | TacticAst.Ring loc -> status, TacticAst.Ring loc
228   | TacticAst.Split loc -> status, TacticAst.Split loc
229   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
230   | TacticAst.Transitivity (loc, term) -> 
231       let status, cic = disambiguate_term status term in
232       status, TacticAst.Transitivity (loc, cic)
233
234 let apply_tactic tactic status =
235  let status,tactic = disambiguate_tactic status tactic in
236  let tactic = tactic_of_ast tactic in
237  let (proof, goals) =
238   ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
239  let dummy = -1 in
240   { status with
241      proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
242
243 module MatitaStatus =
244  struct
245   type input_status = MatitaTypes.status
246   type output_status = MatitaTypes.status * ProofEngineTypes.goal list
247   type tactic = input_status -> output_status
248
249   let focus (status,_) goal =
250    let proof,_ = MatitaMisc.get_proof_status status in
251     {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)}
252
253   let goals (_,goals) = goals
254
255   let set_goals (status,_) goals = status,goals
256
257   let id_tac status = apply_tactic (TacticAst.IdTac CicAst.dummy_floc) status
258
259   let mk_tactic tac = tac
260
261   let apply_tactic tac = tac
262
263  end
264
265 module MatitaTacticals = Tacticals.Make(MatitaStatus)
266
267 let eval_tactical status tac =
268  let rec tactical_of_ast tac =
269   match tac with
270     | TacticAst.Tactic (loc, tactic) -> apply_tactic tactic
271     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
272        MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals)
273     | TacticAst.Do (loc, num, tactical) ->
274         MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical)
275     | TacticAst.Repeat (loc, tactical) ->
276         MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical)
277     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
278         MatitaTacticals.thens ~start:(tactical_of_ast tactical)
279           ~continuations:(List.map tactical_of_ast tacticals)
280     | TacticAst.First (loc, tacticals) ->
281         MatitaTacticals.first
282           ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals)
283     | TacticAst.Try (loc, tactical) ->
284         MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical)
285     | TacticAst.Solve (loc, tacticals) ->
286         MatitaTacticals.solve_tactics
287          ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)
288  in
289   let status,goals = tactical_of_ast tac status in
290   let proof,_ = MatitaMisc.get_proof_status status in
291   let new_status =
292    match goals with
293    | [] -> 
294        let (_,metasenv,_,_) = proof in
295        (match metasenv with
296        | [] -> Proof proof
297        | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
298    | ng::_ -> Incomplete_proof (proof, ng)
299   in
300    { status with proof_status = new_status }
301
302 let eval_coercion status coercion = 
303   let coer_uri,coer_ty =
304     match coercion with 
305     | Cic.Const (uri,_)
306     | Cic.Var (uri,_) ->
307         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
308         (match o with
309         | Cic.Constant (_,_,ty,_,_)
310         | Cic.Variable (_,_,ty,_,_) ->
311             uri,ty
312         | _ -> assert false)
313     | Cic.MutConstruct (uri,t,c,_) ->
314         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
315         (match o with
316         | Cic.InductiveDefinition (l,_,_,_) ->
317             let (_,_,_,cl) = List.nth l t in
318             let (_,cty) = List.nth cl c in
319               uri,cty
320         | _ -> assert false)
321     | _ -> assert false 
322   in
323   (* we have to get the source and the tgt type uri 
324    * in Coq syntax we have already their names, but 
325    * since we don't support Funclass and similar I think
326    * all the coercion should be of the form
327    * (A:?)(B:?)T1->T2
328    * So we should be able to extract them from the coercion type
329    *)
330   let extract_last_two_p ty =
331     let rec aux = function
332       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))   
333       | Cic.Prod( _, src, tgt) -> src, tgt
334       | _ -> assert false
335     in  
336     aux ty
337   in
338   let ty_src,ty_tgt = extract_last_two_p coer_ty in
339   let context = [] in 
340   let src_uri = 
341     let ty_src = CicReduction.whd context ty_src in
342      CicUtil.uri_of_term ty_src
343   in
344   let tgt_uri = 
345     let ty_tgt = CicReduction.whd context ty_tgt in
346      CicUtil.uri_of_term ty_tgt
347   in
348   let new_coercions =
349     (* also adds them to the Db *)
350     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
351   let status =
352    List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status)
353     status new_coercions in
354   let statement_of name =
355     TacticAstPp.pp_statement 
356       (TacticAst.Executable (CicAst.dummy_floc,
357         (TacticAst.Command (CicAst.dummy_floc,
358           (TacticAst.Coercion (CicAst.dummy_floc, 
359             (CicAst.Ident (name, None)))))))) ^ "\n"
360   in
361   let moo_content_rev =
362     [statement_of (UriManager.name_of_uri coer_uri)] @ 
363     (List.map 
364       (fun (uri, _, _) -> 
365         statement_of (UriManager.name_of_uri uri))
366     new_coercions) @ status.moo_content_rev 
367   in
368   let status =  {status with moo_content_rev = moo_content_rev} in
369   {status with proof_status = No_proof}
370
371 let generate_elimination_principles uri status =
372  let elim sort status =
373    try
374     let uri,obj = CicElim.elim_of ~sort uri 0 in
375      MatitaSync.add_obj uri obj status
376    with CicElim.Can_t_eliminate -> status
377  in
378  List.fold_left (fun status sort -> elim sort status) status
379   [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
380
381 let generate_projections uri fields status =
382  let projections = CicRecord.projections_of uri fields in
383   List.fold_left
384    (fun status (uri, name, bo) -> 
385      try 
386       let ty, ugraph = 
387         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
388       let bo = Unshare.unshare bo in
389       let ty = Unshare.unshare ty in
390       let attrs = [`Class `Projection; `Generated] in
391       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
392        MatitaSync.add_obj uri obj status
393      with
394         CicTypeChecker.TypeCheckerFailure s ->
395          MatitaLog.message 
396           ("Unable to create projection " ^ name ^ " cause: " ^ s);
397          status
398       | CicEnvironment.Object_not_found uri ->
399          let depend = UriManager.name_of_uri uri in
400           MatitaLog.message 
401            ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
402          status
403   ) status projections
404
405 (* to avoid a long list of recursive functions *)
406 let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
407  
408 let disambiguate_obj status obj =
409   let uri =
410    match obj with
411       TacticAst.Inductive (_,(name,_,_,_)::_)
412     | TacticAst.Record (_,name,_,_) ->
413        Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
414     | TacticAst.Inductive _ -> assert false
415     | TacticAst.Theorem _ -> None in
416   let (aliases, metasenv, cic, _) =
417     match
418       MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
419         ~aliases:(status.aliases) ~uri obj
420     with
421     | [x] -> x
422     | _ -> assert false
423   in
424   let proof_status =
425     match status.proof_status with
426     | No_proof -> Intermediate metasenv
427     | Incomplete_proof _
428     | Intermediate _
429     | Proof _ -> assert false
430   in
431   let status = { status with proof_status = proof_status } in
432   let status = MatitaSync.set_proof_aliases status aliases in
433   status, cic
434   
435 let disambiguate_command status = function
436   | TacticAst.Default _
437   | TacticAst.Alias _
438   | TacticAst.Include _ as cmd  -> status,cmd
439   | TacticAst.Coercion (loc, term) ->
440       let status, term = disambiguate_term status term in
441       status, TacticAst.Coercion (loc,term)
442   | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
443       status, cmd
444   | TacticAst.Obj (loc,obj) ->
445       let status,obj = disambiguate_obj status obj in
446        status, TacticAst.Obj (loc,obj)
447
448 let try_open_in paths path =
449   let rec aux = function
450   | [] -> open_in path
451   | p :: tl ->
452       try
453         open_in (p ^ "/" ^ path)
454       with Sys_error _ -> aux tl
455   in
456   try
457     aux paths
458   with Sys_error _ as exc ->
459     MatitaLog.error ("Unable to read " ^ path);
460     MatitaLog.error ("opts.include_paths was " ^ String.concat ":" paths);
461     raise exc
462 ;;
463        
464 let eval_command opts status cmd =
465  let status,cmd = disambiguate_command status cmd in
466   match cmd with
467   | TacticAst.Default (loc, what, uris) as cmd ->
468      LibraryObjects.set_default what uris;
469      {status with moo_content_rev =
470         (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
471   | TacticAst.Include (loc, path) ->
472      let path = MatitaMisc.obj_file_of_script path in
473      let stream = Stream.of_channel (try_open_in opts.include_paths path) in
474      let status = ref status in
475       !eval_from_stream_ref status stream (fun _ _ -> ());
476       !status
477   | TacticAst.Set (loc, name, value) -> 
478       let value = 
479         if name = "baseuri" then
480           let v = MatitaMisc.strip_trailing_slash value in
481           try
482             ignore (String.index v ' ');
483             command_error "baseuri can't contain spaces"
484           with Not_found -> v
485         else
486           value
487       in
488       set_option status name value
489   | TacticAst.Drop loc -> raise Drop
490   | TacticAst.Qed loc ->
491       let uri, metasenv, bo, ty = 
492         match status.proof_status with
493         | Proof (Some uri, metasenv, body, ty) ->
494             uri, metasenv, body, ty
495         | Proof (None, metasenv, body, ty) -> 
496             command_error 
497               ("Someone allows to start a thm without giving the "^
498                "name/uri. This should be fixed!")
499         | _-> command_error "You can't qed an uncomplete theorem"
500       in
501       let suri = UriManager.string_of_uri uri in
502       if metasenv <> [] then 
503         command_error "Proof not completed! metasenv is not empty!";
504       let name = UriManager.name_of_uri uri in
505       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
506       MatitaSync.add_obj uri obj status
507   | TacticAst.Coercion (loc, coercion) -> 
508       eval_coercion status coercion
509   | TacticAst.Alias (loc, spec) -> 
510      let aliases =
511       match spec with
512       | TacticAst.Ident_alias (id,uri) -> 
513          DisambiguateTypes.Environment.add 
514           (DisambiguateTypes.Id id) 
515           (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
516           status.aliases 
517       | TacticAst.Symbol_alias (symb, instance, desc) ->
518          DisambiguateTypes.Environment.add 
519           (DisambiguateTypes.Symbol (symb,instance))
520           (DisambiguateChoices.lookup_symbol_by_dsc symb desc) 
521           status.aliases
522       | TacticAst.Number_alias (instance,desc) ->
523          DisambiguateTypes.Environment.add 
524           (DisambiguateTypes.Num instance) 
525           (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
526      in
527       MatitaSync.set_proof_aliases status aliases
528   | TacticAst.Obj (loc,obj) ->
529      let ext,name =
530       match obj with
531          Cic.Constant (name,_,_,_,_)
532        | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
533        | Cic.InductiveDefinition (types,_,_,_) ->
534           ".ind",
535           (match types with (name,_,_,_)::_ -> name | _ -> assert false)
536        | _ -> assert false in
537      let uri = 
538        UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext) 
539      in
540      let metasenv = MatitaMisc.get_proof_metasenv status in
541      match obj with
542      | Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
543          let name = UriManager.name_of_uri uri in
544          if not(CicPp.check name ty) then
545            MatitaLog.warn ("Bad name: " ^ name);
546          if opts.do_heavy_checks then
547            begin
548              let dbd = MatitaDb.instance () in
549              let similar = MetadataQuery.match_term ~dbd ty in
550              let convertible =
551                List.filter (
552                  fun u ->
553                    let t = CicUtil.term_of_uri u in
554                    let ty',g = 
555                      CicTypeChecker.type_of_aux' 
556                        metasenv' [] t CicUniv.empty_ugraph
557                    in
558                    fst(CicReduction.are_convertible [] ty' ty g)) 
559                similar 
560              in
561              (match convertible with
562              | [] -> ()
563              | x::_ -> 
564                  MatitaLog.warn  
565                  ("Theorem already proved: " ^ UriManager.string_of_uri x ^ 
566                   "\nPlease use a variant."));
567            end;
568          assert (metasenv = metasenv');
569          let goalno =
570            match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false 
571          in
572          let initial_proof = (Some uri, metasenv, bo, ty) in
573          { status with proof_status = Incomplete_proof (initial_proof,goalno)}
574      | _ ->
575          if metasenv <> [] then
576           command_error (
577             "metasenv not empty while giving a definition with body: " ^
578             CicMetaSubst.ppmetasenv metasenv []);
579          let status = MatitaSync.add_obj uri obj status in
580           match obj with
581              Cic.Constant _ -> status
582            | Cic.InductiveDefinition (_,_,_,attrs) ->
583               let status = generate_elimination_principles uri status in
584               let rec get_record_attrs =
585                function
586                   [] -> None
587                 | (`Class (`Record fields))::_ -> Some fields
588                 | _::tl -> get_record_attrs tl
589               in
590                (match get_record_attrs attrs with
591                    None -> status (* not a record *)
592                  | Some fields -> generate_projections uri fields status)
593            | Cic.CurrentProof _
594            | Cic.Variable _ -> assert false
595
596 let eval_executable opts status ex =
597   match ex with
598   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
599   | TacticAst.Command (_, cmd) -> eval_command opts status cmd
600   | TacticAst.Macro (_, mac) -> 
601       command_error (sprintf "The macro %s can't be in a script" 
602         (TacticAstPp.pp_macro_ast mac))
603
604 let eval_comment status c = status
605             
606
607 let eval_ast ?(do_heavy_checks=false) ?(include_paths=[]) status st =
608   let opts = 
609     {do_heavy_checks = do_heavy_checks ; include_paths = include_paths}
610   in
611   match st with
612   | TacticAst.Executable (_,ex) -> eval_executable opts status ex
613   | TacticAst.Comment (_,c) -> eval_comment status c
614
615 let eval_from_stream ?do_heavy_checks ?include_paths status str cb =
616   let stl = CicTextualParser2.parse_statements str in
617   List.iter
618    (fun ast -> 
619      cb !status ast;
620      status := eval_ast ?do_heavy_checks ?include_paths !status ast) 
621    stl
622 ;;
623
624 (* to avoid a long list of recursive functions *)
625 eval_from_stream_ref := eval_from_stream;;
626   
627 let eval_from_stream_greedy ?do_heavy_checks ?include_paths status str cb =
628   while true do
629     print_string "matita> ";
630     flush stdout;
631     let ast = CicTextualParser2.parse_statement str in
632     cb !status ast;
633     status := eval_ast ?do_heavy_checks ?include_paths !status ast 
634   done
635 ;;
636
637 let eval_string ?do_heavy_checks ?include_paths status str =
638   eval_from_stream 
639     ?do_heavy_checks ?include_paths status (Stream.of_string str) (fun _ _ ->())
640
641 let default_options () =
642 (*
643   let options =
644     StringMap.add "baseuri"
645       (String
646         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
647       no_options
648   in
649 *)
650   let options =
651     StringMap.add "basedir"
652       (String (Helm_registry.get "matita.basedir"))
653       no_options
654   in
655   options
656
657 let initial_status =
658   lazy {
659     aliases = DisambiguateTypes.empty_environment;
660     moo_content_rev = [];
661     proof_status = No_proof;
662     options = default_options ();
663     objects = [];
664   }
665
666