]> matita.cs.unibo.it Git - helm.git/blob - matita/components/grafite_engine/grafiteEngine.ml
sem_exec_move completed
[helm.git] / matita / 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 (* mo file name, ma file name *)
29 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
30
31 type 'a disambiguator_input = string * int * 'a
32
33 type options = { 
34   do_heavy_checks: bool ; 
35 }
36
37 let basic_eval_unification_hint (t,n) status =
38  NCicUnifHint.add_user_provided_hint status t n
39 ;;
40
41 let inject_unification_hint =
42  let basic_eval_unification_hint (t,n) 
43    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
44    ~alias_only status
45  =
46   if not alias_only then
47    let t = refresh_uri_in_term (status :> NCic.status) t in
48     basic_eval_unification_hint (t,n) status
49   else
50    status
51  in
52   GrafiteTypes.Serializer.register#run "unification_hints"
53    basic_eval_unification_hint
54 ;;
55
56 let eval_unification_hint status t n = 
57  let metasenv,subst,status,t =
58   GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
59  assert (metasenv=[]);
60  let t = NCicUntrusted.apply_subst status subst [] t in
61  let status = basic_eval_unification_hint (t,n) status in
62   NCicLibrary.dump_obj status (inject_unification_hint (t,n))
63 ;;
64
65 let basic_index_obj l (status:#NCic.status) =
66   status#set_auto_cache 
67     (List.fold_left
68       (fun t (ks,v) -> 
69          List.fold_left (fun t k ->
70            NDiscriminationTree.DiscriminationTree.index t k v)
71           t ks) 
72     status#auto_cache l) 
73 ;;     
74
75 let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
76  let status =
77   if not alias_only then
78    Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
79   else
80    status
81  in
82  let mode = GrafiteAst.WithPreferences (*assert false*) in (* MATITA 1.0 VEDI SOTTO *)
83  let diff =
84   [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)]
85  in
86   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
87 ;;
88
89 let inject_interpretation =
90  let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
91    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
92    ~alias_only
93  =
94   let rec refresh =
95    function
96       NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
97        NotationPt.NRefPattern
98         (NReference.reference_of_spec (NCicLibrary.refresh_uri uri) spec)
99     | NotationPt.VarPattern _
100     | NotationPt.ImplicitPattern as x -> x
101     | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
102   in
103   let cic_appl_pattern = refresh cic_appl_pattern in
104    basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
105  in
106   GrafiteTypes.Serializer.register#run "interpretation"
107    basic_eval_interpretation
108 ;;
109
110 let eval_interpretation status data= 
111  let status = basic_eval_interpretation ~alias_only:false data status in
112   NCicLibrary.dump_obj status (inject_interpretation data)
113 ;;
114
115 let basic_eval_alias (mode,diff) status =
116   GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false mode diff
117 ;;
118
119 let inject_alias =
120  let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
121    ~refresh_uri_in_reference ~alias_only =
122    basic_eval_alias (mode,diff)
123  in
124   GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
125 ;;
126
127 let eval_alias status data= 
128  let status = basic_eval_alias data status in
129   NCicLibrary.dump_obj status (inject_alias data)
130 ;;
131
132 let basic_eval_input_notation (l1,l2) status =
133   GrafiteParser.extend status l1 
134    (fun env loc ->
135      NotationPt.AttributedTerm
136       (`Loc loc,TermContentPres.instantiate_level2 status env l2)) 
137 ;;
138
139 let inject_input_notation =
140  let basic_eval_input_notation (l1,l2)
141   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
142   ~alias_only status
143  =
144    if not alias_only then
145     let l1 =
146      CicNotationParser.refresh_uri_in_checked_l1_pattern
147       ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
148       ~refresh_uri_in_reference l1 in
149     let l2 = NotationUtil.refresh_uri_in_term
150       ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
151       ~refresh_uri_in_reference l2
152     in
153      basic_eval_input_notation (l1,l2) status
154    else
155     status
156  in
157   GrafiteTypes.Serializer.register#run "input_notation"
158    basic_eval_input_notation
159 ;;
160
161 let eval_input_notation status data= 
162  let status = basic_eval_input_notation data status in
163   NCicLibrary.dump_obj status (inject_input_notation data)
164 ;;
165
166 let basic_eval_output_notation (l1,l2) status =
167  TermContentPres.add_pretty_printer status l2 l1
168 ;;
169
170 let inject_output_notation =
171  let basic_eval_output_notation (l1,l2)
172   ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
173   ~alias_only status
174  =
175   if not alias_only then
176    let l1 =
177     CicNotationParser.refresh_uri_in_checked_l1_pattern
178      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
179       ~refresh_uri_in_reference l1 in
180    let l2 = NotationUtil.refresh_uri_in_term
181      ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCic.status))
182       ~refresh_uri_in_reference l2
183    in
184     basic_eval_output_notation (l1,l2) status
185   else
186    status
187  in
188   GrafiteTypes.Serializer.register#run "output_notation"
189    basic_eval_output_notation
190 ;;
191
192 let eval_output_notation status data= 
193  let status = basic_eval_output_notation data status in
194   NCicLibrary.dump_obj status (inject_output_notation data)
195 ;;
196
197 let record_index_obj = 
198  let aux l ~refresh_uri_in_universe 
199    ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
200  =
201   let refresh_uri_in_term = refresh_uri_in_term (status:>NCic.status) in
202   if not alias_only then
203     basic_index_obj
204       (List.map 
205         (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v) 
206       l) status
207   else
208    status
209  in
210   GrafiteTypes.Serializer.register#run "index_obj" aux
211 ;;
212
213 let compute_keys status uri height kind = 
214  let mk_item ty spec =
215    let orig_ty = NTacStatus.mk_cic_term [] ty in
216    let status,keys = NnAuto.keys_of_type status orig_ty in
217    let keys =  
218      List.map 
219        (fun t -> 
220           snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
221        keys
222    in
223    keys,NCic.Const(NReference.reference_of_spec uri spec)
224  in
225  let data = 
226   match kind with
227   | NCic.Fixpoint (ind,ifl,_) -> 
228      HExtlib.list_mapi 
229        (fun (_,_,rno,ty,_) i -> 
230           if ind then mk_item ty (NReference.Fix (i,rno,height)) 
231           else mk_item ty (NReference.CoFix height)) ifl
232   | NCic.Inductive (b,lno,itl,_) -> 
233      HExtlib.list_mapi 
234        (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl 
235      @
236      List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
237        (List.flatten (HExtlib.list_mapi 
238          (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
239          itl))
240   | NCic.Constant (_,_,Some _, ty, _) -> 
241      [ mk_item ty (NReference.Def height) ]
242   | NCic.Constant (_,_,None, ty, _) ->
243      [ mk_item ty NReference.Decl ]
244  in
245   HExtlib.filter_map
246    (fun (keys, t) ->
247      let keys = List.filter
248        (function 
249          | (NCic.Meta _) 
250          | (NCic.Appl (NCic.Meta _::_)) -> false 
251          | _ -> true) 
252        keys
253      in
254      if keys <> [] then 
255       begin
256         HLog.debug ("Indexing:" ^ 
257           status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
258         HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
259           status#ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
260         Some (keys,t) 
261       end
262      else 
263       begin
264         HLog.debug ("Not indexing:" ^ 
265           status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
266         None
267       end)
268     data
269 ;;
270
271 let index_obj_for_auto status (uri, height, _, _, kind) = 
272  (*prerr_endline (string_of_int height);*)
273   let data = compute_keys status uri height kind in
274   let status = basic_index_obj data status in
275    NCicLibrary.dump_obj status (record_index_obj data)
276 ;; 
277
278 let basic_extract_obj obj status =
279  try
280   ignore (Helm_registry.get "extract_haskell");
281   let status,(msg,infos) = NCicExtraction.haskell_of_obj status obj in
282    prerr_endline msg;
283    status,infos
284  with
285     Helm_registry.Key_not_found _ -> status,NCicExtraction.empty_info
286   | exn -> prerr_endline ("EXTRACTION FAILURE: " ^ Printexc.to_string exn); assert false
287 ;;
288
289 let inject_extract_obj =
290  let basic_extract_obj info
291    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
292    ~alias_only status
293  =
294   let info= NCicExtraction.refresh_uri_in_info ~refresh_uri_in_reference info in
295    status#set_extraction_db
296     (NCicExtraction.register_infos status#extraction_db info)
297  in
298   GrafiteTypes.Serializer.register#run "extraction" basic_extract_obj
299 ;;
300
301 let eval_extract_obj status obj = 
302  let status,infos = basic_extract_obj obj status in
303   NCicLibrary.dump_obj status (inject_extract_obj infos)
304 ;;
305
306 (*
307 module EmptyC = 
308   struct
309     let metasenv = []
310     let subst = []
311     let context = []
312   end
313 *)
314
315 let index_eq print uri (status:#NCic.status) =
316   let eq_status = status#eq_cache in
317   let eq_status,clause = NCicParamod.index_obj status eq_status uri in
318   if print then
319    ((*let module NCicBlob =
320     struct
321      include NCicBlob.NCicBlob(EmptyC)
322      let pp t = status#ppterm ~metasenv:[] ~subst:[] ~context:[] t
323     end in
324    let module Pp = Pp.Pp(NCicBlob) in*)
325    (match clause with
326      | Some (*clause*) (_,Terms.Equation (_,_,_,o),_,_) ->
327         HLog.debug ("Indexed with orientation: " ^ Pp.string_of_comparison o);
328         (*HLog.debug ("Indexed as:" ^ Pp.pp_unit_clause clause)*)
329      | _ -> HLog.debug "Not indexed (i.e. pruned)")) ;
330   status#set_eq_cache eq_status
331 ;;
332
333 let record_index_eq =
334  let basic_index_eq uri
335    ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference 
336    ~alias_only status
337    = if not alias_only then index_eq false (NCicLibrary.refresh_uri uri) status 
338      else
339       status
340  in
341   GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
342 ;;
343
344 let index_eq_for_auto status uri =
345  if NnAuto.is_a_fact_obj status uri then
346    let newstatus = index_eq true uri status in
347      if newstatus#eq_cache == status#eq_cache then status 
348      else
349        ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
350         NCicLibrary.dump_obj newstatus (record_index_eq uri))
351  else 
352    ((*prerr_endline "Not a fact";*)
353    status)
354 ;; 
355
356 let inject_constraint =
357  let basic_eval_add_constraint (u1,u2) 
358      ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
359      ~alias_only status
360  =
361   if not alias_only then
362    let u1 = refresh_uri_in_universe u1 in 
363    let u2 = refresh_uri_in_universe u2 in 
364     (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
365      * and also to the storage (for undo/redo). During inclusion of compiled
366      * files the storage must not be touched. *)
367     NCicEnvironment.add_lt_constraint u1 u2;
368     status
369   else
370    status
371  in
372   GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint 
373 ;;
374
375 let eval_add_constraint status u1 u2 = 
376  let status = NCicLibrary.add_constraint status u1 u2 in
377   NCicLibrary.dump_obj status (inject_constraint (u1,u2))
378 ;;
379
380 let eval_ng_tac tac =
381  let rec aux f (text, prefix_len, tac) =
382   match tac with
383   | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t) 
384   | GrafiteAst.NSmartApply (_loc, t) -> 
385       NnAuto.smart_apply_tac (text,prefix_len,t) 
386   | GrafiteAst.NAssert (_loc, seqs) ->
387      NTactics.assert_tac
388       ((List.map
389         (function (hyps,concl) ->
390           List.map
391            (function
392               (id,`Decl t) -> id,`Decl (text,prefix_len,t)
393              |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
394            ) hyps,
395           (text,prefix_len,concl))
396        ) seqs)
397   | GrafiteAst.NAuto (_loc, (None,a)) -> 
398       NnAuto.auto_tac ~params:(None,a) ?trace_ref:None
399   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
400       NnAuto.auto_tac
401         ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
402   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
403   | GrafiteAst.NCases (_loc, what, where) ->
404       NTactics.cases_tac 
405         ~what:(text,prefix_len,what)
406         ~where:(text,prefix_len,where)
407   | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
408   | GrafiteAst.NChange (_loc, pat, ww) -> 
409       NTactics.change_tac 
410        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
411   | GrafiteAst.NConstructor (_loc,num,args) -> 
412      NTactics.constructor_tac 
413        ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
414   | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t) 
415 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
416   | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
417   | GrafiteAst.NClear (_loc, l) -> NTactics.clear_tac l
418   | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
419   | GrafiteAst.NDot _ -> NTactics.dot_tac 
420   | GrafiteAst.NElim (_loc, what, where) ->
421       NTactics.elim_tac 
422         ~what:(text,prefix_len,what)
423         ~where:(text,prefix_len,where)
424   | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
425   | GrafiteAst.NGeneralize (_loc, where) -> 
426       NTactics.generalize_tac ~where:(text,prefix_len,where)
427   | GrafiteAst.NId _ -> (fun x -> x)
428   | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
429   | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
430   | GrafiteAst.NInversion (_loc, what, where) ->
431       NTactics.inversion_tac 
432         ~what:(text,prefix_len,what)
433         ~where:(text,prefix_len,where)
434   | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t) 
435   | GrafiteAst.NLetIn (_loc,where,what,name) ->
436       NTactics.letin_tac ~where:(text,prefix_len,where) 
437         ~what:(text,prefix_len,what) name
438   | GrafiteAst.NMerge _ -> NTactics.merge_tac 
439   | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
440   | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
441   | GrafiteAst.NReduce (_loc, reduction, where) ->
442       NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
443   | GrafiteAst.NRewrite (_loc,dir,what,where) ->
444      NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
445       ~where:(text,prefix_len,where)
446   | GrafiteAst.NSemicolon _ -> fun x -> x
447   | GrafiteAst.NShift _ -> NTactics.shift_tac 
448   | GrafiteAst.NSkip _ -> NTactics.skip_tac
449   | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
450   | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac 
451   | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
452       (f f (text, prefix_len, tac))
453   | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
454   | GrafiteAst.NBlock (_,l) -> 
455       NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
456   |GrafiteAst.NRepeat (_,tac) ->
457       NTactics.repeat_tac (f f (text, prefix_len, tac))
458  in
459   aux aux tac (* trick for non uniform recursion call *)
460 ;;
461       
462 let subst_metasenv_and_fix_names status =
463   let u,h,metasenv, subst,o = status#obj in
464   let o = 
465     NCicUntrusted.map_obj_kind ~skip_body:true 
466      (NCicUntrusted.apply_subst status subst []) o
467   in
468    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
469 ;;
470
471 let is_proof_irrelevant status context ty =
472   match
473     NCicReduction.whd status ~subst:[] context
474      (NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context ty)
475   with
476      NCic.Sort NCic.Prop -> true
477    | NCic.Sort _ -> false
478    | _ -> assert false
479 ;;
480
481 let rec relevance_of status ?(context=[]) ty =
482  match NCicReduction.whd status ~subst:[] context ty with
483     NCic.Prod (n,s,t) ->
484      not (is_proof_irrelevant status context s) ::
485       relevance_of status ~context:((n,NCic.Decl s)::context) t
486   | _ -> []
487 ;;
488
489 let compute_relevance status uri =
490  function
491     NCic.Constant (_,name,bo,ty,attrs) ->
492      let relevance = relevance_of status ty in
493       NCic.Constant (relevance,name,bo,ty,attrs)
494   | NCic.Fixpoint (ind,funs,attrs) ->
495      let funs =
496        List.map
497        (fun (_,name,recno,ty,bo) ->
498          let relevance = relevance_of status ty in
499           relevance,name,recno,ty,bo
500         ) funs
501      in
502       NCic.Fixpoint (ind,funs,attrs)
503   | NCic.Inductive (ind,leftno,tys,attrs) ->
504      let context =
505       List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
506      let tysno = List.length tys in
507      let tys =
508        List.map
509         (fun (_,name,arity,cons) ->
510          let relevance = relevance_of status arity in
511          let cons =
512           List.map
513            (fun (_,name,ty) ->
514              let dety =
515                NCicTypeChecker.debruijn status uri tysno ~subst:[] [] ty in
516              let relevance = relevance_of status ~context dety in
517               relevance,name,ty
518            ) cons
519          in
520           (relevance,name,arity,cons)
521         ) tys
522      in
523       NCic.Inductive (ind,leftno,tys,attrs)
524 ;;
525
526
527 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
528   match cmd with
529   | GrafiteAst.Include (loc, mode, fname) ->
530      let _root, baseuri, fullpath, _rrelpath = 
531        Librarian.baseuri_of_script ~include_paths fname in
532      let baseuri = NUri.uri_of_string baseuri in
533      (* MATITA 1.0: keep WithoutPreferences? *)
534      let alias_only = (mode = GrafiteAst.OnlyPreferences) in
535       GrafiteTypes.Serializer.require
536        ~alias_only ~baseuri ~fname:fullpath status
537   | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
538   | GrafiteAst.NCoercion (loc, name, compose, None) ->
539      let status, t, ty, source, target =
540        let o_t = NotationPt.Ident (name,None) in
541        let metasenv,subst, status,t =
542          GrafiteDisambiguate.disambiguate_nterm 
543            status None [] [] [] ("",0,o_t) in
544        assert( metasenv = [] && subst = []);
545        let ty = NCicTypeChecker.typeof status [] [] [] t in
546        let source, target =
547          let clean = function
548            | NCic.Appl (NCic.Const _ as r :: l) -> 
549                NotationPt.Appl (NotationPt.NCic r ::
550                  List.map (fun _ -> NotationPt.Implicit `JustOne)l)
551            | NCic.Const _ as r -> NotationPt.NCic r
552            | NCic.Sort _ as r -> NotationPt.NCic r (* FG: missing case *)
553            | _ -> assert false
554          in
555          let rec aux = function
556            | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
557            | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
558            | _ -> assert false
559          in
560          aux ty
561        in
562        status, o_t, NotationPt.NCic ty, source, target
563      in
564      let status, composites =
565       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
566        target
567      in
568      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
569      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
570       eval_alias status (mode,aliases)
571   | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
572      let status, composites =
573       NCicCoercDeclaration.eval_ncoercion status name compose t ty source
574        target in
575      let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
576      let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
577       eval_alias status (mode,aliases)
578   | GrafiteAst.NQed (loc,index) ->
579      if status#ng_mode <> `ProofMode then
580       raise (GrafiteTypes.Command_error "Not in proof mode")
581      else
582       let uri,height,menv,subst,obj_kind = status#obj in
583        if menv <> [] then
584         raise
585          (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
586        else
587         let obj_kind =
588          NCicUntrusted.map_obj_kind 
589           (NCicUntrusted.apply_subst status subst []) obj_kind in
590         let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
591         (* fix the height inside the object *)
592         let rec fix () = function 
593           | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri -> 
594              NCic.Const (NReference.reference_of_spec u
595               (match spec with
596               | NReference.Def _ -> NReference.Def height
597               | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
598               | NReference.CoFix i -> NReference.CoFix i
599               | NReference.Ind _ | NReference.Con _
600               | NReference.Decl as s -> s))
601           | t -> NCicUtils.map status (fun _ () -> ()) () fix t
602         in
603         let obj_kind = 
604           match obj_kind with
605           | NCic.Fixpoint _ -> 
606               NCicUntrusted.map_obj_kind (fix ()) obj_kind 
607           | _ -> obj_kind
608         in
609         let obj_kind = compute_relevance status uri obj_kind in
610         let obj = uri,height,[],[],obj_kind in
611         let old_status = status in
612         let status = NCicLibrary.add_obj status obj in
613         let status = eval_extract_obj status obj in
614        (try
615         let index_obj = index &&
616          match obj_kind with
617             NCic.Constant (_,_,_,_,(_,`Example,_))
618           | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
619           | _ -> true
620         in
621         let status =
622          if index_obj then
623           let status = index_obj_for_auto status obj in
624            (try index_eq_for_auto status uri
625            with
626               Sys.Break as exn -> raise exn
627             | _ -> status)
628          else
629           status in
630 (*
631           try 
632             index_eq uri status
633           with _ -> prerr_endline "got an exception"; status
634         in *)
635 (*         prerr_endline (status#ppobj obj); *)
636         HLog.message ("New object: " ^ NUri.string_of_uri uri);
637        (*prerr_endline (status#ppobj obj);*)
638            let boxml = NCicElim.mk_elims status obj in
639            let boxml = boxml @ NCicElim.mk_projections status obj in
640            let status = status#set_ng_mode `CommandMode in
641            let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
642            let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
643            let status = eval_alias status (mode,xxaliases) in
644            let status =
645             List.fold_left
646              (fun status boxml ->
647                try
648                 let nstatus =
649                  eval_ncommand ~include_paths opts status
650                   ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
651                 in
652                 if nstatus#ng_mode <> `CommandMode then
653                   begin
654                     (*HLog.warn "error in generating projection/eliminator";*)
655                     assert(status#ng_mode = `CommandMode);
656                     status
657                   end
658                 else
659                   nstatus
660                with
661                | MultiPassDisambiguator.DisambiguationError _
662                | NCicTypeChecker.TypeCheckerFailure _ ->
663                   (*HLog.warn "error in generating projection/eliminator";*)
664                   status
665              ) status boxml in             
666            let _,_,_,_,nobj = obj in
667            (* attempting to generate an inversion principle on the maximum
668             * universe can take a long time to fail: this code removes maximal
669             * sorts from the universe list *)
670            let universes = NCicEnvironment.get_universes () in
671            let max_univ = List.fold_left max [] universes in
672            let universes = 
673              List.filter (fun x -> NCicEnvironment.universe_lt x max_univ)
674                universes
675            in
676            let status = match nobj with
677                NCic.Inductive (is_ind,leftno,itl,_) ->
678                  List.fold_left (fun status it ->      
679                  (let _,ind_name,ty,cl = it in
680                   List.fold_left 
681                    (fun status outsort ->
682                       let status = status#set_ng_mode `ProofMode in
683                       try
684                        (let status,invobj =
685                          NInversion.mk_inverter 
686                           (ind_name ^ "_inv_" ^
687                             (snd (NCicElim.ast_of_sort outsort)))
688                           is_ind it leftno outsort status status#baseuri in
689                        let _,_,menv,_,_ = invobj in
690                         (match menv with
691                              [] -> eval_ncommand ~include_paths opts status
692                                     ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
693                            | _ -> status))
694                        (* XXX *)
695                       with
696                          Sys.Break as exn -> raise exn
697                        | _ -> (*HLog.warn "error in generating inversion principle"; *)
698                                 let status = status#set_ng_mode `CommandMode in status)
699                   status
700                   (NCic.Prop::
701                     List.map (fun s -> NCic.Type s) universes))) status itl
702               | _ -> status
703            in
704            let status = match nobj with
705                NCic.Inductive (is_ind,leftno,itl,_) ->
706                  (* first leibniz *)
707                  let status' = List.fold_left
708                    (fun status it ->
709                       let _,ind_name,ty,cl = it in
710                       let status = status#set_ng_mode `ProofMode in
711                       try
712                        (let status,invobj =
713                          NDestructTac.mk_discriminator ~use_jmeq:false
714                           (ind_name ^ "_discr")
715                           it leftno status status#baseuri in
716                        let _,_,menv,_,_ = invobj in
717                         (match menv with
718                              [] -> eval_ncommand ~include_paths opts status
719                                     ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
720                            | _ -> status))
721                        (* XXX *)
722                       with 
723                       | NDestructTac.ConstructorTooBig k -> 
724                           HLog.warn (Printf.sprintf 
725                            "unable to generate leibniz discrimination principle (constructor %s too big)"
726                            k);
727                            let status = status#set_ng_mode `CommandMode in status
728                       | _ -> (*HLog.warn "error in generating discrimination principle"; *)
729                                 let status = status#set_ng_mode `CommandMode in
730                                 status)
731                   status itl
732                 in
733                 (* then JMeq *)
734                 List.fold_left
735                    (fun status it ->
736                       let _,ind_name,ty,cl = it in
737                       let status = status#set_ng_mode `ProofMode in
738                       try
739                        (let status,invobj =
740                          NDestructTac.mk_discriminator ~use_jmeq:true
741                           (ind_name ^ "_jmdiscr")
742                           it leftno status status#baseuri in
743                        let _,_,menv,_,_ = invobj in
744                         (match menv with
745                              [] -> eval_ncommand ~include_paths opts status
746                                     ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
747                            | _ -> status))
748                        (* XXX *)
749                       with
750                          Sys.Break as exn -> raise exn
751                        | _ -> (*HLog.warn "error in generating discrimination principle"; *)
752                                 let status = status#set_ng_mode `CommandMode in
753                                 status)
754                   status' itl
755               | _ -> status
756            in
757            let coercions =
758             match obj with
759               _,_,_,_,NCic.Inductive
760                (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
761                ->
762                 HExtlib.filter_map
763                  (fun (name,is_coercion,arity) ->
764                    if is_coercion then Some(name,leftno,arity) else None) fields
765             | _ -> [] in
766            let status =
767             List.fold_left
768              (fun status (name,cpos,arity) ->
769                try
770                  let metasenv,subst,status,t =
771                   GrafiteDisambiguate.disambiguate_nterm status None [] [] []
772                    ("",0,NotationPt.Ident (name,None)) in
773                  assert (metasenv = [] && subst = []);
774                  let status, nuris = 
775                    NCicCoercDeclaration.
776                      basic_eval_and_record_ncoercion_from_t_cpos_arity 
777                       status (name,true,t,cpos,arity) in
778                  let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
779                  let status =
780                   List.fold_left
781                    (fun status uri ->
782                      let obj = NCicEnvironment.get_checked_obj status uri in
783                       eval_extract_obj status obj
784                    ) status nuris
785                  in
786                   eval_alias status (mode,aliases)
787                with MultiPassDisambiguator.DisambiguationError _-> 
788                  HLog.warn ("error in generating coercion: "^name);
789                  status) 
790              status coercions
791            in
792             status
793           with
794            exn ->
795             NCicLibrary.time_travel old_status;
796             raise exn)
797   | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
798      if status#ng_mode <> `CommandMode then
799       raise (GrafiteTypes.Command_error "Not in command mode")
800      else
801        let tgt_uri_ext, old_ok = 
802          match NCicEnvironment.get_checked_obj status src_uri with
803          | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
804          | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
805          | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
806          | _ -> assert false
807        in
808        let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
809        let map = (src_uri, tgt_uri) :: map in
810        let ok = 
811          let rec subst () = function
812            | NCic.Meta _ -> assert false
813            | NCic.Const (NReference.Ref (u,spec)) as t ->
814                (try NCic.Const 
815                  (NReference.reference_of_spec (List.assoc u map)spec)
816                with Not_found -> t)
817            | t -> NCicUtils.map status (fun _ _ -> ()) () subst t
818          in
819          NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
820        in
821        let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
822        let status = status#set_obj (tgt_uri,0,[],[],ok) in
823        (*prerr_endline (status#ppobj (tgt_uri,0,[],[],ok));*)
824        let status = status#set_stack ninitial_stack in
825        let status = subst_metasenv_and_fix_names status in
826        let status = status#set_ng_mode `ProofMode in
827        eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
828   | GrafiteAst.NObj (loc,obj,index) ->
829      if status#ng_mode <> `CommandMode then
830       raise (GrafiteTypes.Command_error "Not in command mode")
831      else
832       let status,obj =
833        GrafiteDisambiguate.disambiguate_nobj status
834         ~baseuri:status#baseuri (text,prefix_len,obj) in
835       let uri,height,nmenv,nsubst,nobj = obj in
836       let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
837       let status = status#set_obj obj in
838       let status = status#set_stack ninitial_stack in
839       let status = subst_metasenv_and_fix_names status in
840       let status = status#set_ng_mode `ProofMode in
841       (match nmenv with
842           [] ->
843            eval_ncommand ~include_paths opts status
844              ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,index))
845         | _ -> status)
846   | GrafiteAst.NDiscriminator (loc, indty) ->
847       if status#ng_mode <> `CommandMode then
848         raise (GrafiteTypes.Command_error "Not in command mode")
849       else
850         let status = status#set_ng_mode `ProofMode in
851         let metasenv,subst,status,indty =
852           GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in
853         let indtyno, (_,_,tys,_,_),leftno = match indty with
854             NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
855               indtyno, NCicEnvironment.get_checked_indtys status r, leftno
856           | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
857         let (_,ind_name,_,_ as it) = List.nth tys indtyno in
858         let status,obj =  
859           NDestructTac.mk_discriminator ~use_jmeq:true ~force:true (ind_name ^ "_jmdiscr")
860            it leftno status status#baseuri in
861         let _,_,menv,_,_ = obj in
862           (match menv with
863                [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
864              | _ -> prerr_endline ("Discriminator: non empty metasenv");
865                     status)
866   | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
867      if status#ng_mode <> `CommandMode then
868       raise (GrafiteTypes.Command_error "Not in command mode")
869      else
870       let metasenv,subst,status,sort = match sort with
871         | None -> [],[],status,NCic.Sort NCic.Prop
872         | Some s ->
873            GrafiteDisambiguate.disambiguate_nterm status None [] [] []
874             (text,prefix_len,s) 
875       in
876       assert (metasenv = []);
877       let sort = NCicReduction.whd status ~subst [] sort in
878       let sort =
879        match sort with 
880           NCic.Sort s -> s
881         | _ ->
882            raise (Invalid_argument (Printf.sprintf
883             "ninverter: found target %s, which is not a sort"
884              (status#ppterm ~metasenv ~subst ~context:[] sort))) in
885       let status = status#set_ng_mode `ProofMode in
886       let metasenv,subst,status,indty =
887        GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
888         (text,prefix_len,indty) in
889       let indtyno,(_,leftno,tys,_,_) =
890        match indty with
891           NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
892            indtyno, NCicEnvironment.get_checked_indtys status r
893         | _ ->
894           prerr_endline ("engine: indty ="  ^ status#ppterm ~metasenv:[]
895            ~subst:[] ~context:[] indty);
896           assert false in
897       let it = List.nth tys indtyno in
898       let status,obj =
899        NInversion.mk_inverter name true it leftno ?selection sort 
900         status status#baseuri in
901       let _,_,menv,_,_ = obj in
902        (match menv with
903           [] ->
904             eval_ncommand ~include_paths opts status
905              ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
906         | _ -> assert false)
907   | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
908       eval_add_constraint status [`Type,u1] [`Type,u2]
909   (* ex lexicon commands *)
910   | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
911      let cic_appl_pattern =
912       GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
913        cic_appl_pattern
914      in
915       eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
916   | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
917       let l1 = 
918         CicNotationParser.check_l1_pattern
919          l1 (dir = Some `RightToLeft) precedence associativity
920       in
921       let status =
922         if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
923         else status
924       in
925        if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
926        else status
927   | GrafiteAst.Alias (loc, spec) -> 
928      let diff =
929       (*CSC: Warning: this code should be factorized with the corresponding
930              code in DisambiguatePp *)
931       match spec with
932       | GrafiteAst.Ident_alias (id,uri) -> 
933          [DisambiguateTypes.Id id,spec]
934       | GrafiteAst.Symbol_alias (symb, instance, desc) ->
935          [DisambiguateTypes.Symbol (symb,instance),spec]
936       | GrafiteAst.Number_alias (instance,desc) ->
937          [DisambiguateTypes.Num instance,spec]
938      in
939       let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
940        eval_alias status (mode,diff)
941 ;;
942
943 let eval_comment opts status (text,prefix_len,c) = status
944
945 let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
946   match ex with
947   | GrafiteAst.NTactic (_(*loc*), tacl) ->
948       if status#ng_mode <> `ProofMode then
949        raise (GrafiteTypes.Command_error "Not in proof mode")
950       else
951        let status =
952         List.fold_left 
953           (fun status tac ->
954             let time0 = Unix.gettimeofday () in
955             let status = eval_ng_tac (text,prefix_len,tac) status in
956             let time3 = Unix.gettimeofday () in
957             HLog.debug ("... eval_ng_tac done in " ^ string_of_float (time3 -. time0) ^ "s");
958             let status = subst_metasenv_and_fix_names status in
959             let time3 = Unix.gettimeofday () in
960             HLog.debug ("... subst_metasenv_and_fix_names done in " ^ string_of_float (time3 -. time0) ^ "s"); status)
961           status tacl
962        in
963         status
964   | GrafiteAst.NCommand (_, cmd) ->
965       eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
966   | GrafiteAst.NMacro (loc, macro) ->
967      raise (NMacro (loc,macro))
968
969 and eval_ast ~include_paths ?(do_heavy_checks=false) status (text,prefix_len,st)
970 =
971   let opts = { do_heavy_checks = do_heavy_checks ; } in
972   match st with
973   | GrafiteAst.Executable (_,ex) ->
974      eval_executable ~include_paths opts status (text,prefix_len,ex)
975   | GrafiteAst.Comment (_,c) -> 
976       eval_comment opts status (text,prefix_len,c) 
977 ;;