6 let debug_print = if debug then prerr_endline else ignore ;;
8 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
9 * names as long as they are available, then it fallbacks to name generation
10 * using FreshNamesGenerator module *)
12 let len = List.length names in
14 fun metasenv context name ~typ ->
15 if !count < len then begin
16 let name = Cic.Name (List.nth names !count) in
20 FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
22 let tactic_of_ast = function
23 | TacticAst.Intros (_, None, names) ->
24 (* TODO Zack implement intros length *)
25 PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
26 | TacticAst.Intros (_, Some num, names) ->
27 (* TODO Zack implement intros length *)
28 PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
29 | TacticAst.Reflexivity _ -> Tactics.reflexivity
30 | TacticAst.Assumption _ -> Tactics.assumption
31 | TacticAst.Contradiction _ -> Tactics.contradiction
32 | TacticAst.Exists _ -> Tactics.exists
33 | TacticAst.Fourier _ -> Tactics.fourier
34 | TacticAst.Goal (_, n) -> Tactics.set_goal n
35 | TacticAst.Left _ -> Tactics.left
36 | TacticAst.Right _ -> Tactics.right
37 | TacticAst.Ring _ -> Tactics.ring
38 | TacticAst.Split _ -> Tactics.split
39 | TacticAst.Symmetry _ -> Tactics.symmetry
40 | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
41 | TacticAst.Apply (_, term) -> Tactics.apply term
42 | TacticAst.Absurd (_, term) -> Tactics.absurd term
43 | TacticAst.Exact (_, term) -> Tactics.exact term
44 | TacticAst.Cut (_, term) -> Tactics.cut term
45 | TacticAst.Elim (_, term, _) ->
46 (* TODO Zack implement "using" argument *)
47 (* old: Tactics.elim_intros_simpl term *)
48 Tactics.elim_intros term
49 | TacticAst.ElimType (_, term) -> Tactics.elim_type term
50 | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
51 | TacticAst.Auto (_,num) ->
52 AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
53 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
55 (* TODO Zack a lot more of tactics to be implemented here ... *)
56 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
57 | TacticAst.Change of 'term * 'term * 'ident option
58 | TacticAst.Decompose of 'ident * 'ident list
59 | TacticAst.Discriminate of 'ident
60 | TacticAst.Fold of reduction_kind * 'term
61 | TacticAst.Injection of 'ident
62 | TacticAst.Replace_pattern of 'term pattern * 'term
64 | TacticAst.LetIn (loc,term,name) ->
65 Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
66 | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
67 ProofEngineTypes.mk_tactic
68 (fun (((_,metasenv,_,_),goal) as status) ->
69 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
70 let where, also_in_hypotheses =
71 if ident = "goal" then
77 | Some (Cic.Name name,entry) when name = ident -> true
81 Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
84 | Some (_, Cic.Decl term) -> term
85 | Some (_, Cic.Def (term,ty)) -> term
86 | None -> assert false),true
88 let pointers = CicUtil.select ~term:where ~context:path in
89 (match reduction_kind with
91 ProofEngineTypes.apply_tactic
92 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
95 ProofEngineTypes.apply_tactic
96 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
99 ProofEngineTypes.apply_tactic
100 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
103 ProofEngineTypes.apply_tactic
104 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
106 | TacticAst.Reduce (_,reduction_kind,opts) ->
107 let terms, also_in_hypotheses =
109 | Some (l,`Goal) -> Some l, false
110 | Some (l,`Everywhere) -> Some l, true
111 | None -> None, false
113 (match reduction_kind with
114 | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
115 | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
116 | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
117 | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
118 | TacticAst.Rewrite (_,dir,t,ident) ->
120 EqualityTactics.rewrite_tac ~term:t
122 EqualityTactics.rewrite_back_tac ~term:t
125 let eval_tactical status tac =
126 let apply_tactic tactic =
128 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
133 let (_,metasenv,_,_) = proof in
136 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
137 | ng::_ -> Incomplete_proof (proof, ng)
139 { status with proof_status = new_status }
141 let rec tactical_of_ast = function
142 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
143 | TacticAst.Fail loc -> Tacticals.fail
144 | TacticAst.Do (loc, num, tactical) ->
145 Tacticals.do_tactic num (tactical_of_ast tactical)
146 | TacticAst.IdTac loc -> Tacticals.id_tac
147 | TacticAst.Repeat (loc, tactical) ->
148 Tacticals.repeat_tactic (tactical_of_ast tactical)
149 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
150 Tacticals.seq (List.map tactical_of_ast tacticals)
151 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
152 Tacticals.thens (tactical_of_ast tactical)
153 (List.map tactical_of_ast tacticals)
154 | TacticAst.Tries (loc, tacticals) ->
155 Tacticals.try_tactics
156 (List.map (fun t -> "", tactical_of_ast t) tacticals)
157 | TacticAst.Try (loc, tactical) ->
158 Tacticals.try_tactic (tactical_of_ast tactical)
160 apply_tactic (tactical_of_ast tac)
162 (** given a uri and a type list (the contructors types) builds a list of pairs
163 * (name,uri) that is used to generate authomatic aliases **)
164 let extract_alias types uri =
166 fun (acc,i) (name, _, _, cl) ->
167 ((name, UriManager.string_of_uriref (uri,[i]))
169 (fst(List.fold_left (
170 fun (acc,j) (name,_) ->
171 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
175 (** adds a (name,uri) list l to a disambiguation environment e **)
176 let env_of_list l e =
177 let module DT = DisambiguateTypes in
178 let module DTE = DisambiguateTypes.Environment in
183 (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
187 let eval_coercion status coercion =
188 let coer_uri,coer_ty =
193 CicEnvironment.get_obj CicUniv.empty_ugraph uri
196 | Cic.Constant (_,_,ty,_,_)
197 | Cic.Variable (_,_,ty,_,_) ->
200 | Cic.MutConstruct (uri,t,c,_) ->
202 CicEnvironment.get_obj CicUniv.empty_ugraph uri
205 | Cic.InductiveDefinition (l,_,_,_) ->
206 let (_,_,_,cl) = List.nth l t in
207 let (_,cty) = List.nth cl c in
212 (* we have to get the source and the tgt type uri
213 * in Coq syntax we have already their names, but
214 * since we don't support Funclass and similar I think
215 * all the coercion should be of the form
217 * So we should be able to extract them from the coercion type
219 let extract_last_two_p ty =
220 let rec aux = function
221 | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
222 | Cic.Prod( _, src, tgt) -> src, tgt
227 let ty_src,ty_tgt = extract_last_two_p coer_ty in
228 let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
229 let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
231 (* also adds them to the Db *)
232 CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
236 fun s (uri,o,ugraph) ->
238 | Cic.Constant (_,Some body, ty, params, attrs) ->
239 MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
241 ) status new_coercions
243 {status with proof_status = No_proof}
245 let eval_command status cmd =
247 | TacticAst.Set (loc, name, value) -> set_option status name value
248 | TacticAst.Qed loc ->
249 let uri, metasenv, bo, ty =
250 match status.proof_status with
251 | Proof (Some uri, metasenv, body, ty) ->
252 uri, metasenv, body, ty
253 | Proof (None, metasenv, body, ty) ->
255 ("Someone allows to start a thm without giving the "^
256 "name/uri. This should be fixed!")
257 | _-> command_error "You can't qed an uncomplete theorem"
259 let suri = UriManager.string_of_uri uri in
260 if metasenv <> [] then
261 command_error "Proof not completed! metasenv is not empty!";
262 let proved_ty,ugraph =
263 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
266 CicReduction.are_convertible [] proved_ty ty ugraph
270 ("The type of your proof is not convertible with the "^
271 "type you've declared!");
272 MatitaLog.message (sprintf "%s defined" suri);
273 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
275 let name = UriManager.name_of_uri uri in
276 let new_env = env_of_list [(name,suri)] status.aliases in
277 {status with aliases = new_env }
279 {status with proof_status = No_proof }
280 | TacticAst.Inductive (loc, dummy_params, types) ->
281 (* dummy_params are not real params, it is a list of nothing, and the only
282 * semantic content is the len, that is leftno (note: leftno and pamaters
283 * have nothing in common).
287 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
290 let uri = UriManager.uri_of_string suri in
291 let leftno = List.length dummy_params in
292 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
294 CicTypeChecker.typecheck_mutual_inductive_defs uri
295 (types, [], leftno) CicUniv.empty_ugraph
298 MatitaSync.add_inductive_def
299 ~uri ~types ~params:[] ~leftno ~ugraph status
301 (* aliases for the constructors and types *)
302 let aliases = env_of_list (extract_alias types uri) status.aliases in
303 (* aliases for the eliminations principles *)
305 let base = String.sub suri 0 (String.length suri - 4) in
310 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
311 ) status.objects then
312 let u = base ^ suffix in
313 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
316 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
318 let status = {status with proof_status = No_proof } in
319 { status with aliases = aliases}
320 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
322 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
326 match status.proof_status with
327 | Intermediate metasenv ->
328 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
331 let initial_proof = (Some uri, metasenv, body, ty) in
332 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
333 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
335 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
337 let metasenv = MatitaMisc.get_proof_metasenv status in
338 debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
339 let (body_type, ugraph) =
340 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
342 let (subst, metasenv, ugraph) =
343 CicUnification.fo_unif metasenv [] body_type ty ugraph
345 if metasenv <> [] then
347 "metasenv not empty while giving a definition with body";
348 let body = CicMetaSubst.apply_subst subst body in
349 let ty = CicMetaSubst.apply_subst subst ty in
350 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
352 let suri = UriManager.string_of_uri uri in
353 let new_env = env_of_list [(name,suri)] status.aliases in
354 {status with aliases = new_env }
356 {status with proof_status = No_proof}
357 | TacticAst.Theorem (_, _, None, _, _) ->
358 command_error "The grammar should avoid having unnamed theorems!"
359 | TacticAst.Coercion (loc, coercion) ->
360 eval_coercion status coercion
361 | TacticAst.Alias (loc, spec) ->
363 | TacticAst.Ident_alias (id,uri) ->
364 {status with aliases =
365 DisambiguateTypes.Environment.add
366 (DisambiguateTypes.Id id)
367 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
369 | TacticAst.Symbol_alias (symb, instance, desc) ->
370 {status with aliases =
371 DisambiguateTypes.Environment.add
372 (DisambiguateTypes.Symbol (symb,instance))
373 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
375 | TacticAst.Number_alias (instance,desc) ->
376 {status with aliases =
377 DisambiguateTypes.Environment.add
378 (DisambiguateTypes.Num instance)
379 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
381 let eval_executable status ex =
383 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
384 | TacticAst.Command (_, cmd) -> eval_command status cmd
385 | TacticAst.Macro (_, mac) ->
386 command_error (sprintf "The macro %s can't be in a script"
387 (TacticAstPp.pp_macro_cic mac))
389 let eval_comment status c = status
393 | TacticAst.Executable (_,ex) -> eval_executable status ex
394 | TacticAst.Comment (_,c) -> eval_comment status c
396 let disambiguate_term status term =
397 let (aliases, metasenv, cic, _) =
399 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
400 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
401 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
407 match status.proof_status with
408 | No_proof -> Intermediate metasenv
409 | Incomplete_proof ((uri, _, proof, ty), goal) ->
410 Incomplete_proof ((uri, metasenv, proof, ty), goal)
411 | Intermediate _ -> Intermediate metasenv
412 | Proof _ -> assert false
417 proof_status = proof_status }
421 let disambiguate_terms status terms =
422 let term = CicAst.pack terms in
423 let status, term = disambiguate_term status term in
424 status, CicUtil.unpack term
426 let disambiguate_tactic status = function
427 | TacticAst.Transitivity (loc, term) ->
428 let status, cic = disambiguate_term status term in
429 status, TacticAst.Transitivity (loc, cic)
430 | TacticAst.Apply (loc, term) ->
431 let status, cic = disambiguate_term status term in
432 status, TacticAst.Apply (loc, cic)
433 | TacticAst.Absurd (loc, term) ->
434 let status, cic = disambiguate_term status term in
435 status, TacticAst.Absurd (loc, cic)
436 | TacticAst.Exact (loc, term) ->
437 let status, cic = disambiguate_term status term in
438 status, TacticAst.Exact (loc, cic)
439 | TacticAst.Cut (loc, term) ->
440 let status, cic = disambiguate_term status term in
441 status, TacticAst.Cut (loc, cic)
442 | TacticAst.Elim (loc, term, Some term') ->
443 let status, cic1 = disambiguate_term status term in
444 let status, cic2 = disambiguate_term status term' in
445 status, TacticAst.Elim (loc, cic1, Some cic2)
446 | TacticAst.Elim (loc, term, None) ->
447 let status, cic = disambiguate_term status term in
448 status, TacticAst.Elim (loc, cic, None)
449 | TacticAst.ElimType (loc, term) ->
450 let status, cic = disambiguate_term status term in
451 status, TacticAst.ElimType (loc, cic)
452 | TacticAst.Replace (loc, what, with_what) ->
453 let status, cic1 = disambiguate_term status what in
454 let status, cic2 = disambiguate_term status with_what in
455 status, TacticAst.Replace (loc, cic1, cic2)
456 | TacticAst.Change (loc, what, with_what, ident) ->
457 let status, cic1 = disambiguate_term status what in
458 let status, cic2 = disambiguate_term status with_what in
459 status, TacticAst.Change (loc, cic1, cic2, ident)
461 (* TODO Zack a lot more of tactics to be implemented here ... *)
462 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
463 | TacticAst.Change of 'term * 'term * 'ident option
464 | TacticAst.Decompose of 'ident * 'ident list
465 | TacticAst.Discriminate of 'ident
466 | TacticAst.Fold of reduction_kind * 'term
467 | TacticAst.Injection of 'ident
468 | TacticAst.Replace_pattern of 'term pattern * 'term
470 | TacticAst.LetIn (loc,term,name) ->
471 let status, term = disambiguate_term status term in
472 status, TacticAst.LetIn (loc,term,name)
473 | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
474 let path = Disambiguate.interpretate [] status.aliases path in
475 status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
476 | TacticAst.Reduce (loc, reduction_kind, opts) ->
479 | None -> status, None
482 List.fold_right (fun t (status,acc) ->
483 let status',t' = disambiguate_term status t in
487 status, Some (l, pat)
489 status, TacticAst.Reduce (loc, reduction_kind, opts)
490 | TacticAst.Rewrite (loc,dir,t,ident) ->
491 let status, term = disambiguate_term status t in
492 status, TacticAst.Rewrite (loc,dir,term,ident)
493 | TacticAst.Intros (loc, num, names) ->
494 status, TacticAst.Intros (loc, num, names)
495 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
496 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
497 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
498 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
499 | TacticAst.Exists loc -> status, TacticAst.Exists loc
500 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
501 | TacticAst.Left loc -> status, TacticAst.Left loc
502 | TacticAst.Right loc -> status, TacticAst.Right loc
503 | TacticAst.Ring loc -> status, TacticAst.Ring loc
504 | TacticAst.Split loc -> status, TacticAst.Split loc
505 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
506 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
508 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
511 let rec disambiguate_tactical status = function
512 | TacticAst.Tactic (loc, tactic) ->
513 let status, tac = disambiguate_tactic status tactic in
514 status, TacticAst.Tactic (loc, tac)
515 | TacticAst.Do (loc, num, tactical) ->
516 let status, tac = disambiguate_tactical status tactical in
517 status, TacticAst.Do (loc, num, tac)
518 | TacticAst.Repeat (loc, tactical) ->
519 let status, tac = disambiguate_tactical status tactical in
520 status, TacticAst.Repeat (loc, tac)
521 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
522 let status, tacticals = disambiguate_tacticals status tacticals in
523 let tacticals = List.rev tacticals in
524 status, TacticAst.Seq (loc, tacticals)
525 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
526 let status, tactical = disambiguate_tactical status tactical in
527 let status, tacticals = disambiguate_tacticals status tacticals in
528 status, TacticAst.Then (loc, tactical, tacticals)
529 | TacticAst.Tries (loc, tacticals) ->
530 let status, tacticals = disambiguate_tacticals status tacticals in
531 status, TacticAst.Tries (loc, tacticals)
532 | TacticAst.Try (loc, tactical) ->
533 let status, tactical = disambiguate_tactical status tactical in
534 status, TacticAst.Try (loc, tactical)
535 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
538 and disambiguate_tacticals status tacticals =
539 let status, tacticals =
541 (fun (status, tacticals) tactical ->
542 let status, tac = disambiguate_tactical status tactical in
543 status, tac :: tacticals)
547 let tacticals = List.rev tacticals in
550 let disambiguate_inddef status params indTypes =
551 let add_pi binders t =
553 (fun (name, ast) acc ->
554 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
558 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
560 let binders = ind_binders @ params in
562 let add_ast ast = asts := ast :: !asts in
563 let paramsno = List.length params in
564 let indbindersno = List.length ind_binders in
566 (fun (name, _, typ, constructors) ->
567 add_ast (add_pi params typ);
568 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
570 let status, terms = disambiguate_terms status !asts in
571 let terms = ref (List.rev terms) in
573 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
577 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
581 let counter = ref 0 in
585 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
588 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
591 (fun acc (name, inductive, typ, constructors) ->
592 let cicTyp = get_term () in
593 let cicConstructors =
595 (fun acc (name, _) ->
597 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
602 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
605 let cicIndTypes = List.rev cicIndTypes in
606 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
608 let disambiguate_command status = function
609 | TacticAst.Inductive (loc, params, types) ->
610 let (status, (uri, (ind_types, vars, paramsno))) =
611 disambiguate_inddef status params types
613 let rec mk_list = function
615 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
617 (* once we've built the cic inductive types we no longer need terms
618 corresponding to parameters, but we need the leftno, and we encode
619 it as the length of dummy_params
621 let dummy_params = mk_list paramsno in
622 status, TacticAst.Inductive (loc, dummy_params, ind_types)
623 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
624 let status, ty = disambiguate_term status ty in
627 | None -> status, None
629 let status, body = disambiguate_term status body in
632 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
633 | TacticAst.Coercion (loc, term) ->
634 let status, term = disambiguate_term status term in
635 status, TacticAst.Coercion (loc,term)
636 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
638 | TacticAst.Alias _ as x -> status, x
640 let disambiguate_executable status ex =
642 | TacticAst.Tactical (loc, tac) ->
643 let status, tac = disambiguate_tactical status tac in
644 status, (TacticAst.Tactical (loc, tac))
645 | TacticAst.Command (loc, cmd) ->
646 let status, cmd = disambiguate_command status cmd in
647 status, (TacticAst.Command (loc, cmd))
648 | TacticAst.Macro (_, mac) ->
650 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
651 "in particular %s") (TacticAstPp.pp_macro_ast mac))
653 let disambiguate_comment status c =
655 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
656 | TacticAst.Code (loc,ex) ->
657 let status, ex = disambiguate_executable status ex in
658 status, TacticAst.Code (loc,ex)
660 let disambiguate_statement status statement =
662 | TacticAst.Comment (loc,c) ->
663 let status, c = disambiguate_comment status c in
664 status, TacticAst.Comment (loc,c)
665 | TacticAst.Executable (loc,ex) ->
666 let status, ex = disambiguate_executable status ex in
667 status, TacticAst.Executable (loc,ex)
669 let eval_ast status ast =
670 let status,st = disambiguate_statement status ast in
671 (* this disambiguation step should be deferred to support tacticals *)
674 let eval_from_stream status str cb =
675 let stl = CicTextualParser2.parse_statements str in
677 (fun status ast -> cb status ast;eval_ast status ast) status
680 let eval_string status str =
681 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
683 let default_options () =
685 StringMap.add "baseuri"
687 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
691 StringMap.add "basedir"
692 (String (Helm_registry.get "matita.basedir" ))
699 aliases = DisambiguateTypes.empty_environment;
700 proof_status = No_proof;
701 options = default_options ();