1 (* Copyright (C) 2005, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 (* mo file name, ma file name *)
29 exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro
31 type 'a disambiguator_input = string * int * 'a
34 do_heavy_checks: bool ;
37 let prerr_endline _ = ()
39 let basic_eval_unification_hint (t,n) status =
40 NCicUnifHint.add_user_provided_hint status t n
43 let inject_unification_hint =
44 let basic_eval_unification_hint (t,n)
45 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
48 if not alias_only then
49 let t = refresh_uri_in_term (status :> NCicEnvironment.status) t in
50 basic_eval_unification_hint (t,n) status
54 GrafiteTypes.Serializer.register#run "unification_hints"
55 basic_eval_unification_hint
58 let eval_unification_hint status t n =
59 let metasenv,subst,status,t =
60 GrafiteDisambiguate.disambiguate_nterm status None [] [] [] ("",0,t) in
62 let t = NCicUntrusted.apply_subst status subst [] t in
63 let status = basic_eval_unification_hint (t,n) status in
64 NCicLibrary.dump_obj status (inject_unification_hint (t,n))
67 let basic_index_obj l status =
71 List.fold_left (fun t k ->
72 NDiscriminationTree.DiscriminationTree.index t k v)
77 let basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern) status =
79 if not alias_only then
80 Interpretations.add_interpretation status dsc (symbol, args) cic_appl_pattern
85 (* FIXME! the uri should be filled with something meaningful! *)
86 [DisambiguateTypes.Symbol symbol,
87 GrafiteAst.Symbol_alias (symbol,None,dsc)]
89 GrafiteDisambiguate.add_to_disambiguation_univ status diff
92 let inject_interpretation =
93 let basic_eval_interpretation (dsc, (symbol, args), cic_appl_pattern)
94 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
99 NotationPt.NRefPattern (NReference.Ref (uri,spec)) ->
100 NotationPt.NRefPattern
101 (NReference.reference_of_spec (NCicLibrary.refresh_uri uri) spec)
102 | NotationPt.VarPattern _
103 | NotationPt.ImplicitPattern as x -> x
104 | NotationPt.ApplPattern l -> NotationPt.ApplPattern (List.map refresh l)
106 let cic_appl_pattern = refresh cic_appl_pattern in
107 basic_eval_interpretation ~alias_only (dsc, (symbol, args), cic_appl_pattern)
109 GrafiteTypes.Serializer.register#run "interpretation"
110 basic_eval_interpretation
113 let eval_interpretation status data=
114 let status = basic_eval_interpretation ~alias_only:false data status in
115 NCicLibrary.dump_obj status (inject_interpretation data)
118 let basic_eval_alias (mode,diff) status =
119 prerr_endline "basic_eval_alias";
120 GrafiteDisambiguate.add_to_disambiguation_univ status diff
124 let basic_eval_alias (mode,diff) ~refresh_uri_in_universe ~refresh_uri_in_term
125 ~refresh_uri_in_reference ~alias_only =
126 basic_eval_alias (mode,diff)
128 GrafiteTypes.Serializer.register#run "alias" basic_eval_alias
131 let eval_alias status data=
132 let status = basic_eval_alias data status in
133 NCicLibrary.dump_obj status (inject_alias data)
136 let basic_eval_input_notation (l1,l2) status =
137 GrafiteParser.extend status l1
139 let rec get_disamb = function
140 | [] -> Stdpp.dummy_loc,None,None
141 | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
142 | _::tl -> get_disamb tl
144 let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
145 prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
146 NotationPt.AttributedTerm (`Loc loc,l2'))
149 let inject_input_notation =
150 let basic_eval_input_notation (l1,l2)
151 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
154 if not alias_only then
156 CicNotationParser.refresh_uri_in_checked_l1_pattern
157 ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
158 ~refresh_uri_in_reference l1 in
159 let l2 = NotationUtil.refresh_uri_in_term
160 ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
161 ~refresh_uri_in_reference l2
163 basic_eval_input_notation (l1,l2) status
167 GrafiteTypes.Serializer.register#run "input_notation"
168 basic_eval_input_notation
171 let eval_input_notation status data=
172 let status = basic_eval_input_notation data status in
173 NCicLibrary.dump_obj status (inject_input_notation data)
176 let basic_eval_output_notation (l1,l2) status =
177 TermContentPres.add_pretty_printer status l2 l1
180 let inject_output_notation =
181 let basic_eval_output_notation (l1,l2)
182 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
185 if not alias_only then
187 CicNotationParser.refresh_uri_in_checked_l1_pattern
188 ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
189 ~refresh_uri_in_reference l1 in
190 let l2 = NotationUtil.refresh_uri_in_term
191 ~refresh_uri_in_term:(refresh_uri_in_term (status:>NCicEnvironment.status))
192 ~refresh_uri_in_reference l2
194 basic_eval_output_notation (l1,l2) status
198 GrafiteTypes.Serializer.register#run "output_notation"
199 basic_eval_output_notation
202 let eval_output_notation status data=
203 let status = basic_eval_output_notation data status in
204 NCicLibrary.dump_obj status (inject_output_notation data)
207 let record_index_obj =
208 let aux l ~refresh_uri_in_universe
209 ~refresh_uri_in_term ~refresh_uri_in_reference ~alias_only status
211 let refresh_uri_in_term = refresh_uri_in_term (status:>NCicEnvironment.status) in
212 if not alias_only then
215 (fun ks,v -> List.map refresh_uri_in_term ks, refresh_uri_in_term v)
220 GrafiteTypes.Serializer.register#run "index_obj" aux
223 let compute_keys status uri height kind =
224 let mk_item ty spec =
225 let orig_ty = NTacStatus.mk_cic_term [] ty in
226 let status,keys = NnAuto.keys_of_type status orig_ty in
230 snd (NTacStatus.term_of_cic_term status t (NTacStatus.ctx_of t)))
233 keys,NCic.Const(NReference.reference_of_spec uri spec)
237 | NCic.Fixpoint (ind,ifl,_) ->
239 (fun (_,_,rno,ty,_) i ->
240 if ind then mk_item ty (NReference.Fix (i,rno,height))
241 else mk_item ty (NReference.CoFix height)) ifl
242 | NCic.Inductive (b,lno,itl,_) ->
244 (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl
246 List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno)))
247 (List.flatten (HExtlib.list_mapi
248 (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl)
250 | NCic.Constant (_,_,Some _, ty, _) ->
251 [ mk_item ty (NReference.Def height) ]
252 | NCic.Constant (_,_,None, ty, _) ->
253 [ mk_item ty NReference.Decl ]
257 let keys = List.filter
260 | (NCic.Appl (NCic.Meta _::_)) -> false
266 HLog.debug ("Indexing:" ^
267 status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
268 HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t ->
269 status#ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys));
274 HLog.debug ("Not indexing:" ^
275 status#ppterm ~metasenv:[] ~subst:[] ~context:[] t);
281 let index_obj_for_auto status (uri, height, _, _, kind) =
282 (*prerr_endline (string_of_int height);*)
283 let data = compute_keys status uri height kind in
284 let status = basic_index_obj data status in
285 NCicLibrary.dump_obj status (record_index_obj data)
288 let index_eq uri status =
289 let eq_status = status#eq_cache in
290 let eq_status = NCicParamod.index_obj status eq_status uri in
291 status#set_eq_cache eq_status
294 let record_index_eq =
295 let basic_index_eq uri
296 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
298 = if not alias_only then index_eq (NCicLibrary.refresh_uri uri) status else
301 GrafiteTypes.Serializer.register#run "index_eq" basic_index_eq
304 let index_eq_for_auto status uri =
305 if NnAuto.is_a_fact_obj status uri then
306 let newstatus = index_eq uri status in
307 if newstatus#eq_cache == status#eq_cache then status
309 ((*prerr_endline ("recording " ^ (NUri.string_of_uri uri));*)
310 NCicLibrary.dump_obj newstatus (record_index_eq uri))
312 ((*prerr_endline "Not a fact";*)
316 let inject_constraint =
317 let basic_eval_add_constraint (u1,u2)
318 ~refresh_uri_in_universe ~refresh_uri_in_term ~refresh_uri_in_reference
321 if not alias_only then
322 let u1 = refresh_uri_in_universe u1 in
323 let u2 = refresh_uri_in_universe u2 in
324 (* NCicLibrary.add_constraint adds the constraint to the NCicEnvironment
325 * and also to the storage (for undo/redo). During inclusion of compiled
326 * files the storage must not be touched. *)
327 NCicEnvironment.add_lt_constraint status u1 u2;
332 GrafiteTypes.Serializer.register#run "constraints" basic_eval_add_constraint
335 let eval_add_constraint status u1 u2 =
336 let status = NCicLibrary.add_constraint status u1 u2 in
337 NCicLibrary.dump_obj status (inject_constraint (u1,u2))
340 let eval_ng_tac tac =
341 let rec aux f (text, prefix_len, tac) =
343 | GrafiteAst.NApply (_loc, t) -> NTactics.apply_tac (text,prefix_len,t)
344 | GrafiteAst.NSmartApply (_loc, t) ->
345 NnAuto.smart_apply_tac (text,prefix_len,t)
346 | GrafiteAst.NAssert (_loc, seqs) ->
349 (function (hyps,concl) ->
352 (id,`Decl t) -> id,`Decl (text,prefix_len,t)
353 |(id,`Def (b,t))->id,`Def((text,prefix_len,b),(text,prefix_len,t))
355 (text,prefix_len,concl))
357 | GrafiteAst.NAuto (_loc, (None,a)) ->
358 NnAuto.auto_tac ~params:(None,a) ?trace_ref:None
359 | GrafiteAst.NAuto (_loc, (Some (_,l),a)) ->
361 ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
362 | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
363 | GrafiteAst.NCases (_loc, what, where) ->
365 ~what:(text,prefix_len,what)
366 ~where:(text,prefix_len,where)
367 | GrafiteAst.NCase1 (_loc,n) -> NTactics.case1_tac n
368 | GrafiteAst.NChange (_loc, pat, ww) ->
370 ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww)
371 | GrafiteAst.NConstructor (_loc,num,args) ->
372 NTactics.constructor_tac
373 ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
374 | GrafiteAst.NCut (_loc, t) -> NTactics.cut_tac (text,prefix_len,t)
375 (*| GrafiteAst.NDiscriminate (_,what) -> NDestructTac.discriminate_tac ~what:(text,prefix_len,what)
376 | GrafiteAst.NSubst (_,what) -> NDestructTac.subst_tac ~what:(text,prefix_len,what)*)
377 | GrafiteAst.NClear (_loc, l) -> NTactics.clear_tac l
378 | GrafiteAst.NDestruct (_,dom,skip) -> NDestructTac.destruct_tac dom skip
379 | GrafiteAst.NDot _ -> NTactics.dot_tac
380 | GrafiteAst.NElim (_loc, what, where) ->
382 ~what:(text,prefix_len,what)
383 ~where:(text,prefix_len,where)
384 | GrafiteAst.NFocus (_,l) -> NTactics.focus_tac l
385 | GrafiteAst.NGeneralize (_loc, where) ->
386 NTactics.generalize_tac ~where:(text,prefix_len,where)
387 | GrafiteAst.NId _ -> (fun x -> x)
388 | GrafiteAst.NIntro (_loc,n) -> NTactics.intro_tac n
389 | GrafiteAst.NIntros (_loc,ns) -> NTactics.intros_tac ns
390 | GrafiteAst.NInversion (_loc, what, where) ->
391 NTactics.inversion_tac
392 ~what:(text,prefix_len,what)
393 ~where:(text,prefix_len,where)
394 | GrafiteAst.NLApply (_loc, t) -> NTactics.lapply_tac (text,prefix_len,t)
395 | GrafiteAst.NLetIn (_loc,where,what,name) ->
396 NTactics.letin_tac ~where:(text,prefix_len,where)
397 ~what:(text,prefix_len,what) name
398 | GrafiteAst.NMerge _ -> NTactics.merge_tac
399 | GrafiteAst.NPos (_,l) -> NTactics.pos_tac l
400 | GrafiteAst.NPosbyname (_,s) -> NTactics.case_tac s
401 | GrafiteAst.NReduce (_loc, reduction, where) ->
402 NTactics.reduce_tac ~reduction ~where:(text,prefix_len,where)
403 | GrafiteAst.NRewrite (_loc,dir,what,where) ->
404 NTactics.rewrite_tac ~dir ~what:(text,prefix_len,what)
405 ~where:(text,prefix_len,where)
406 | GrafiteAst.NSemicolon _ -> fun x -> x
407 | GrafiteAst.NShift _ -> NTactics.shift_tac
408 | GrafiteAst.NSkip _ -> NTactics.skip_tac
409 | GrafiteAst.NUnfocus _ -> NTactics.unfocus_tac
410 | GrafiteAst.NWildcard _ -> NTactics.wildcard_tac
411 | GrafiteAst.NTry (_,tac) -> NTactics.try_tac
412 (f f (text, prefix_len, tac))
413 | GrafiteAst.NAssumption _ -> NTactics.assumption_tac
414 | GrafiteAst.NBlock (_,l) ->
415 NTactics.block_tac (List.map (fun x -> aux f (text,prefix_len,x)) l)
416 |GrafiteAst.NRepeat (_,tac) ->
417 NTactics.repeat_tac (f f (text, prefix_len, tac))
419 aux aux tac (* trick for non uniform recursion call *)
422 let subst_metasenv_and_fix_names status =
423 let u,h,metasenv, subst,o = status#obj in
425 NCicUntrusted.map_obj_kind ~skip_body:true
426 (NCicUntrusted.apply_subst status subst []) o
428 status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
431 let is_proof_irrelevant status context ty =
433 NCicReduction.whd status ~subst:[] context
434 (NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context ty)
436 NCic.Sort NCic.Prop -> true
437 | NCic.Sort _ -> false
441 let rec relevance_of status ?(context=[]) ty =
442 match NCicReduction.whd status ~subst:[] context ty with
444 not (is_proof_irrelevant status context s) ::
445 relevance_of status ~context:((n,NCic.Decl s)::context) t
449 let compute_relevance status uri =
451 NCic.Constant (_,name,bo,ty,attrs) ->
452 let relevance = relevance_of status ty in
453 NCic.Constant (relevance,name,bo,ty,attrs)
454 | NCic.Fixpoint (ind,funs,attrs) ->
457 (fun (_,name,recno,ty,bo) ->
458 let relevance = relevance_of status ty in
459 relevance,name,recno,ty,bo
462 NCic.Fixpoint (ind,funs,attrs)
463 | NCic.Inductive (ind,leftno,tys,attrs) ->
465 List.rev_map (fun (_,name,arity,_) -> name,NCic.Decl arity) tys in
466 let tysno = List.length tys in
469 (fun (_,name,arity,cons) ->
470 let relevance = relevance_of status arity in
475 NCicTypeChecker.debruijn status uri tysno ~subst:[] [] ty in
476 let relevance = relevance_of status ~context dety in
480 (relevance,name,arity,cons)
483 NCic.Inductive (ind,leftno,tys,attrs)
487 let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
489 | GrafiteAst.Include (loc, mode, fname) ->
490 let _root, baseuri, fullpath, _rrelpath =
491 Librarian.baseuri_of_script ~include_paths fname in
492 let baseuri = NUri.uri_of_string baseuri in
493 (* MATITA 1.0: keep WithoutPreferences? *)
494 let alias_only = (mode = GrafiteAst.OnlyPreferences) in
495 GrafiteTypes.Serializer.require
496 ~alias_only ~baseuri ~fname:fullpath status
497 | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n
498 | GrafiteAst.NCoercion (loc, name, compose, None) ->
499 let status, t, ty, source, target =
500 let o_t = NotationPt.Ident (name,`Ambiguous) in
501 let metasenv,subst, status,t =
502 GrafiteDisambiguate.disambiguate_nterm
503 status None [] [] [] ("",0,o_t) in
504 assert( metasenv = [] && subst = []);
505 let ty = NCicTypeChecker.typeof status [] [] [] t in
508 | NCic.Appl (NCic.Const _ as r :: l) ->
509 NotationPt.Appl (NotationPt.NCic r ::
510 List.map (fun _ -> NotationPt.Implicit `JustOne)l)
511 | NCic.Const _ as r -> NotationPt.NCic r
512 | _ -> assert false in
513 let rec aux = function
514 | NCic.Prod (_,_, (NCic.Prod _ as rest)) -> aux rest
515 | NCic.Prod (name, src, tgt) -> (name, clean src), clean tgt
516 | _ -> assert false in aux ty in
517 status, o_t, NotationPt.NCic ty, source, target in
518 let status, composites =
519 NCicCoercDeclaration.eval_ncoercion status name compose t ty source
521 let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
522 let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
523 eval_alias status (mode,aliases)
524 | GrafiteAst.NCoercion (loc, name, compose, Some (t, ty, source, target)) ->
525 let status, composites =
526 NCicCoercDeclaration.eval_ncoercion status name compose t ty source
528 let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
529 let aliases = GrafiteDisambiguate.aliases_for_objs status composites in
530 eval_alias status (mode,aliases)
531 | GrafiteAst.NQed (loc,index) ->
532 if status#ng_mode <> `ProofMode then
533 raise (GrafiteTypes.Command_error "Not in proof mode")
535 let uri,height,menv,subst,obj_kind = status#obj in
538 (GrafiteTypes.Command_error"You can't Qed an incomplete theorem")
541 NCicUntrusted.map_obj_kind
542 (NCicUntrusted.apply_subst status subst []) obj_kind in
543 let height = NCicTypeChecker.height_of_obj_kind status uri [] obj_kind in
544 (* fix the height inside the object *)
545 let rec fix () = function
546 | NCic.Const (NReference.Ref (u,spec)) when NUri.eq u uri ->
547 NCic.Const (NReference.reference_of_spec u
549 | NReference.Def _ -> NReference.Def height
550 | NReference.Fix (i,j,_) -> NReference.Fix(i,j,height)
551 | NReference.CoFix i -> NReference.CoFix i
552 | NReference.Ind _ | NReference.Con _
553 | NReference.Decl as s -> s))
554 | t -> NCicUtils.map status (fun _ () -> ()) () fix t
559 NCicUntrusted.map_obj_kind (fix ()) obj_kind
562 let obj_kind = compute_relevance status uri obj_kind in
563 let obj = uri,height,[],[],obj_kind in
564 let old_status = status in
565 let status = NCicLibrary.add_obj status obj in
566 let index_obj = index &&
568 NCic.Constant (_,_,_,_,(_,`Example,_))
569 | NCic.Fixpoint (_,_,(_,`Example,_)) -> false
574 let status = index_obj_for_auto status obj in
575 (try index_eq_for_auto status uri
582 with _ -> prerr_endline "got an exception"; status
584 (* prerr_endline (status#ppobj obj); *)
585 HLog.message ("New object: " ^ NUri.string_of_uri uri);
587 (*prerr_endline (status#ppobj obj);*)
588 let boxml = NCicElim.mk_elims status obj in
589 let boxml = boxml @ NCicElim.mk_projections status obj in
590 let status = status#set_ng_mode `CommandMode in
591 let xxaliases = GrafiteDisambiguate.aliases_for_objs status [uri] in
592 let mode = GrafiteAst.WithPreferences in (* MATITA 1.0: fixme *)
593 let status = eval_alias status (mode,xxaliases) in
599 eval_ncommand ~include_paths opts status
600 ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml,true))
602 if nstatus#ng_mode <> `CommandMode then
604 (*HLog.warn "error in generating projection/eliminator";*)
605 assert(status#ng_mode = `CommandMode);
611 | GrafiteDisambiguate.Error _
612 | NCicTypeChecker.TypeCheckerFailure _ ->
613 (*HLog.warn "error in generating projection/eliminator";*)
616 let _,_,_,_,nobj = obj in
617 let status = match nobj with
618 NCic.Inductive (is_ind,leftno,itl,_) ->
619 List.fold_left (fun status it ->
620 (let _,ind_name,ty,cl = it in
622 (fun status outsort ->
623 let status = status#set_ng_mode `ProofMode in
626 NInversion.mk_inverter
627 (ind_name ^ "_inv_" ^
628 (snd (NCicElim.ast_of_sort outsort)))
629 is_ind it leftno outsort status status#baseuri in
630 let _,_,menv,_,_ = invobj in
632 [] -> eval_ncommand ~include_paths opts status
633 ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
636 with _ -> (*HLog.warn "error in generating inversion principle"; *)
637 let status = status#set_ng_mode `CommandMode in status)
640 List.map (fun s -> NCic.Type s)
641 (NCicEnvironment.get_universes status)))) status itl
644 let status = match nobj with
645 NCic.Inductive (is_ind,leftno,itl,_) ->
647 let status' = List.fold_left
649 let _,ind_name,ty,cl = it in
650 let status = status#set_ng_mode `ProofMode in
652 prerr_endline ("creazione discriminatore per " ^ ind_name);
654 NDestructTac.mk_discriminator ~use_jmeq:false
655 (ind_name ^ "_discr")
656 it leftno status status#baseuri in
657 let _,_,menv,_,_ = invobj in
659 [] -> eval_ncommand ~include_paths opts status
660 ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
664 | NDestructTac.ConstructorTooBig k ->
665 prerr_endline (Printf.sprintf
666 "unable to generate leibniz discrimination principle (constructor %s too big)"
668 HLog.warn (Printf.sprintf
669 "unable to generate leibniz discrimination principle (constructor %s too big)"
671 let status = status#set_ng_mode `CommandMode in status
673 prerr_endline "error in generating discrimination principle";
674 (*HLog.warn "error in generating discrimination principle"; *)
675 let status = status#set_ng_mode `CommandMode in
682 let _,ind_name,ty,cl = it in
683 let status = status#set_ng_mode `ProofMode in
685 prerr_endline ("creazione discriminatore per " ^ ind_name);
687 NDestructTac.mk_discriminator ~use_jmeq:true
688 (ind_name ^ "_jmdiscr")
689 it leftno status status#baseuri in
690 let _,_,menv,_,_ = invobj in
692 [] -> eval_ncommand ~include_paths opts status
693 ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
696 with _ -> (*HLog.warn "error in generating discrimination principle"; *)
697 prerr_endline "error in generating discrimination principle";
698 let status = status#set_ng_mode `CommandMode in
705 _,_,_,_,NCic.Inductive
706 (true,leftno,[_,_,_,[_,_,_]],(_,`Record fields))
709 (fun (name,is_coercion,arity) ->
710 if is_coercion then Some(name,leftno,arity) else None) fields
714 (fun status (name,cpos,arity) ->
716 let metasenv,subst,status,t =
717 GrafiteDisambiguate.disambiguate_nterm status None [] [] []
718 ("",0,NotationPt.Ident (name,`Ambiguous)) in
719 assert (metasenv = [] && subst = []);
721 NCicCoercDeclaration.
722 basic_eval_and_record_ncoercion_from_t_cpos_arity
724 status (name,true,t,cpos,arity) in
725 let aliases = GrafiteDisambiguate.aliases_for_objs status nuris in
726 eval_alias status (mode,aliases)
727 with GrafiteDisambiguate.Error _ ->
728 HLog.warn ("error in generating coercion: "^name);
735 NCicLibrary.time_travel old_status;
737 | GrafiteAst.NCopy (log,tgt,src_uri, map) ->
738 if status#ng_mode <> `CommandMode then
739 raise (GrafiteTypes.Command_error "Not in command mode")
741 let tgt_uri_ext, old_ok =
742 match NCicEnvironment.get_checked_obj status src_uri with
743 | _,_,[],[], (NCic.Inductive _ as ok) -> ".ind", ok
744 | _,_,[],[], (NCic.Fixpoint _ as ok) -> ".con", ok
745 | _,_,[],[], (NCic.Constant _ as ok) -> ".con", ok
748 let tgt_uri = NUri.uri_of_string (status#baseuri^"/"^tgt^tgt_uri_ext) in
749 let map = (src_uri, tgt_uri) :: map in
751 let rec subst () = function
752 | NCic.Meta _ -> assert false
753 | NCic.Const (NReference.Ref (u,spec)) as t ->
755 (NReference.reference_of_spec (List.assoc u map)spec)
757 | t -> NCicUtils.map status (fun _ _ -> ()) () subst t
759 NCicUntrusted.map_obj_kind ~skip_body:false (subst ()) old_ok
761 let ninitial_stack = Continuationals.Stack.of_nmetasenv [] in
762 let status = status#set_obj (tgt_uri,0,[],[],ok) in
763 (*prerr_endline (status#ppobj (tgt_uri,0,[],[],ok));*)
764 let status = status#set_stack ninitial_stack in
765 let status = subst_metasenv_and_fix_names status in
766 let status = status#set_ng_mode `ProofMode in
767 eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
768 | GrafiteAst.NObj (loc,obj,index) ->
769 if status#ng_mode <> `CommandMode then
770 raise (GrafiteTypes.Command_error "Not in command mode")
773 GrafiteDisambiguate.disambiguate_nobj status
774 ~baseuri:status#baseuri (text,prefix_len,obj) in
775 let uri,height,nmenv,nsubst,nobj = obj in
776 let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
777 let status = status#set_obj obj in
778 let status = status#set_stack ninitial_stack in
779 let status = subst_metasenv_and_fix_names status in
780 let status = status#set_ng_mode `ProofMode in
783 eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed
784 (Stdpp.dummy_loc,index))
786 | GrafiteAst.NDiscriminator (loc, indty) ->
787 if status#ng_mode <> `CommandMode then
788 raise (GrafiteTypes.Command_error "Not in command mode")
790 let status = status#set_ng_mode `ProofMode in
791 let metasenv,subst,status,indty =
792 GrafiteDisambiguate.disambiguate_nterm status None [] [] [] (text,prefix_len,indty) in
793 let indtyno, (_,_,tys,_,_), leftno = match indty with
794 NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,leftno))) as r) ->
795 indtyno, NCicEnvironment.get_checked_indtys status r, leftno
796 | _ -> prerr_endline ("engine: indty expected... (fix this error message)"); assert false in
797 let (_,ind_name,_,_ as it) = List.nth tys indtyno in
799 NDestructTac.mk_discriminator ~use_jmeq:true (ind_name ^ "_jmdiscr")
800 it leftno status status#baseuri in
801 let _,_,menv,_,_ = obj in
803 [] -> eval_ncommand ~include_paths opts status
804 ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
805 | _ -> prerr_endline ("Discriminator: non empty metasenv");
807 | GrafiteAst.NInverter (loc, name, indty, selection, sort) ->
808 if status#ng_mode <> `CommandMode then
809 raise (GrafiteTypes.Command_error "Not in command mode")
811 let metasenv,subst,status,sort = match sort with
812 | None -> [],[],status,NCic.Sort NCic.Prop
814 let metasenv,subst,status,sort =
815 GrafiteDisambiguate.disambiguate_nterm status None [] [] []
817 in metasenv,subst,status,sort
819 assert (metasenv = []);
820 let sort = NCicReduction.whd status ~subst [] sort in
825 raise (Invalid_argument (Printf.sprintf
826 "ninverter: found target %s, which is not a sort"
827 (status#ppterm ~metasenv ~subst ~context:[] sort))) in
828 let status = status#set_ng_mode `ProofMode in
829 let metasenv,subst,status,indty =
830 GrafiteDisambiguate.disambiguate_nterm status None [] [] subst
831 (text,prefix_len,indty) in
832 let indtyno,(_,leftno,tys,_,_) =
834 NCic.Const ((NReference.Ref (_,NReference.Ind (_,indtyno,_))) as r) ->
835 indtyno, NCicEnvironment.get_checked_indtys status r
837 prerr_endline ("engine: indty =" ^ status#ppterm ~metasenv:[]
838 ~subst:[] ~context:[] indty);
840 let it = List.nth tys indtyno in
842 NInversion.mk_inverter name true it leftno ?selection sort
843 status status#baseuri in
844 let _,_,menv,_,_ = obj in
847 eval_ncommand ~include_paths opts status
848 ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
850 | GrafiteAst.NUnivConstraint (loc,u1,u2) ->
851 eval_add_constraint status [`Type,u1] [`Type,u2]
852 (* ex lexicon commands *)
853 | GrafiteAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
854 let cic_appl_pattern =
855 GrafiteDisambiguate.disambiguate_cic_appl_pattern status args
858 eval_interpretation status (dsc,(symbol, args),cic_appl_pattern)
859 | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) ->
860 prerr_endline ("new notation: " ^ (NotationPp.pp_term status l1));
862 CicNotationParser.check_l1_pattern
863 l1 (dir = Some `RightToLeft) precedence associativity
866 if dir <> Some `RightToLeft then eval_input_notation status (l1,l2)
870 if dir <> Some `LeftToRight then eval_output_notation status (l1,l2)
872 in prerr_endline ("new grammar:\n" ^ (Print_grammar.ebnf_of_term status));
874 | GrafiteAst.Alias (loc, spec) ->
876 (*CSC: Warning: this code should be factorized with the corresponding
877 code in DisambiguatePp *)
879 | GrafiteAst.Ident_alias (id,uri) ->
880 [DisambiguateTypes.Id id,spec]
881 | GrafiteAst.Symbol_alias (symb, uri, desc) ->
882 [DisambiguateTypes.Symbol symb,spec]
883 | GrafiteAst.Number_alias (uri,desc) ->
884 [DisambiguateTypes.Num,spec]
886 let mode = GrafiteAst.WithPreferences in(*assert false in (* VEDI SOPRA *) MATITA 1.0*)
887 eval_alias status (mode,diff)
890 let eval_comment opts status (text,prefix_len,c) = status
892 let rec eval_executable ~include_paths opts status (text,prefix_len,ex) =
894 | GrafiteAst.NTactic (_(*loc*), tacl) ->
895 if status#ng_mode <> `ProofMode then
896 (prerr_endline ("not in proof mode 2: " ^ GrafiteAstPp.pp_executable status ~map_unicode_to_tex:false ex);
897 raise (GrafiteTypes.Command_error "Not in proof mode"))
902 let status = eval_ng_tac (text,prefix_len,tac) status in
903 prerr_endline "prima di subst_metasenv_and_fix_names";
904 subst_metasenv_and_fix_names status)
908 | GrafiteAst.NCommand (_, cmd) ->
909 eval_ncommand ~include_paths opts status (text,prefix_len,cmd)
910 | GrafiteAst.NMacro (loc, macro) ->
911 raise (NMacro (loc,macro))
913 and eval_ast ~include_paths ?(do_heavy_checks=false) status (text,prefix_len,st)
915 let opts = { do_heavy_checks = do_heavy_checks ; } in
917 | GrafiteAst.Executable (_,ex) ->
918 eval_executable ~include_paths opts status (text,prefix_len,ex)
919 | GrafiteAst.Comment (_,c) ->
920 eval_comment opts status (text,prefix_len,c)