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
29 ~mk_fresh_name_callback:(namer_of names) ()
30 | TacticAst.Reflexivity _ -> Tactics.reflexivity
31 | TacticAst.Assumption _ -> Tactics.assumption
32 | TacticAst.Contradiction _ -> Tactics.contradiction
33 | TacticAst.Exists _ -> Tactics.exists
34 | TacticAst.Fourier _ -> Tactics.fourier
35 | TacticAst.Goal (_, n) -> Tactics.set_goal n
36 | TacticAst.Left _ -> Tactics.left
37 | TacticAst.Right _ -> Tactics.right
38 | TacticAst.Ring _ -> Tactics.ring
39 | TacticAst.Split _ -> Tactics.split
40 | TacticAst.Symmetry _ -> Tactics.symmetry
41 | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
42 | TacticAst.Apply (_, term) -> Tactics.apply term
43 | TacticAst.Absurd (_, term) -> Tactics.absurd term
44 | TacticAst.Exact (_, term) -> Tactics.exact term
45 | TacticAst.Cut (_, term) -> Tactics.cut term
46 | TacticAst.Elim (_, term, _) ->
47 (* TODO Zack implement "using" argument *)
48 (* old: Tactics.elim_intros_simpl term *)
49 Tactics.elim_intros term
50 | TacticAst.ElimType (_, term) -> Tactics.elim_type term
51 | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
52 | TacticAst.Auto (_,num) ->
53 AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
54 | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
56 (* TODO Zack a lot more of tactics to be implemented here ... *)
57 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
58 | TacticAst.Change of 'term * 'term * 'ident option
59 | TacticAst.Decompose of 'ident * 'ident list
60 | TacticAst.Discriminate of 'ident
61 | TacticAst.Fold of reduction_kind * 'term
62 | TacticAst.Injection of 'ident
63 | TacticAst.Replace_pattern of 'term pattern * 'term
65 | TacticAst.LetIn (loc,term,name) ->
66 Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
67 | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
68 ProofEngineTypes.mk_tactic
69 (fun (((_,metasenv,_,_),goal) as status) ->
70 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
71 let where, also_in_hypotheses =
72 if ident = "goal" then
78 | Some (Cic.Name name,entry) when name = ident -> true
82 Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
85 | Some (_, Cic.Decl term) -> term
86 | Some (_, Cic.Def (term,ty)) -> term
87 | None -> assert false),true
89 let pointers = CicUtil.select ~term:where ~context:path in
90 (match reduction_kind with
92 ProofEngineTypes.apply_tactic
93 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
96 ProofEngineTypes.apply_tactic
97 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
100 ProofEngineTypes.apply_tactic
101 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
104 ProofEngineTypes.apply_tactic
105 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
107 | TacticAst.Reduce (_,reduction_kind,opts) ->
108 let terms, also_in_hypotheses =
110 | Some (l,`Goal) -> Some l, false
111 | Some (l,`Everywhere) -> Some l, true
112 | None -> None, false
114 (match reduction_kind with
115 | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
116 | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
117 | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
118 | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
119 | TacticAst.Rewrite (_,dir,t,ident) ->
121 EqualityTactics.rewrite_tac ~term:t
123 EqualityTactics.rewrite_back_tac ~term:t
126 let eval_tactical status tac =
127 let apply_tactic tactic =
129 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
134 let (_,metasenv,_,_) = proof in
137 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
138 | ng::_ -> Incomplete_proof (proof, ng)
140 { status with proof_status = new_status }
142 let rec tactical_of_ast = function
143 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
144 | TacticAst.Fail loc -> Tacticals.fail
145 | TacticAst.Do (loc, num, tactical) ->
146 Tacticals.do_tactic num (tactical_of_ast tactical)
147 | TacticAst.IdTac loc -> Tacticals.id_tac
148 | TacticAst.Repeat (loc, tactical) ->
149 Tacticals.repeat_tactic (tactical_of_ast tactical)
150 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
151 Tacticals.seq (List.map tactical_of_ast tacticals)
152 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
153 Tacticals.thens (tactical_of_ast tactical)
154 (List.map tactical_of_ast tacticals)
155 | TacticAst.Tries (loc, tacticals) ->
156 Tacticals.try_tactics
157 (List.map (fun t -> "", tactical_of_ast t) tacticals)
158 | TacticAst.Try (loc, tactical) ->
159 Tacticals.try_tactic (tactical_of_ast tactical)
161 apply_tactic (tactical_of_ast tac)
163 (** given a uri and a type list (the contructors types) builds a list of pairs
164 * (name,uri) that is used to generate authomatic aliases **)
165 let extract_alias types uri =
167 fun (acc,i) (name, _, _, cl) ->
168 ((name, UriManager.string_of_uriref (uri,[i]))
170 (fst(List.fold_left (
171 fun (acc,j) (name,_) ->
172 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
176 (** adds a (name,uri) list l to a disambiguation environment e **)
177 let env_of_list l e =
178 let module DT = DisambiguateTypes in
179 let module DTE = DisambiguateTypes.Environment in
184 (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
188 let eval_coercion status coercion =
189 let coer_uri,coer_ty =
194 CicEnvironment.get_obj CicUniv.empty_ugraph uri
197 | Cic.Constant (_,_,ty,_,_)
198 | Cic.Variable (_,_,ty,_,_) ->
201 | Cic.MutConstruct (uri,t,c,_) ->
203 CicEnvironment.get_obj CicUniv.empty_ugraph uri
206 | Cic.InductiveDefinition (l,_,_,_) ->
207 let (_,_,_,cl) = List.nth l t in
208 let (_,cty) = List.nth cl c in
213 (* we have to get the source and the tgt type uri
214 * in Coq syntax we have already their names, but
215 * since we don't support Funclass and similar I think
216 * all the coercion should be of the form
218 * So we should be able to extract them from the coercion type
220 let extract_last_two_p ty =
221 let rec aux = function
222 | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
223 | Cic.Prod( _, src, tgt) -> src, tgt
228 let ty_src,ty_tgt = extract_last_two_p coer_ty in
229 let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
230 let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
232 (* also adds them to the Db *)
233 CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
237 fun s (uri,o,ugraph) ->
239 | Cic.Constant (_,Some body, ty, params, attrs) ->
240 MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
242 ) status new_coercions
244 {status with proof_status = No_proof}
246 let eval_command status cmd =
248 | TacticAst.Set (loc, name, value) -> set_option status name value
249 | TacticAst.Qed loc ->
250 let uri, metasenv, bo, ty =
251 match status.proof_status with
252 | Proof (Some uri, metasenv, body, ty) ->
253 uri, metasenv, body, ty
254 | Proof (None, metasenv, body, ty) ->
256 ("Someone allows to start a thm without giving the "^
257 "name/uri. This should be fixed!")
258 | _-> command_error "You can't qed an uncomplete theorem"
260 let suri = UriManager.string_of_uri uri in
261 if metasenv <> [] then
262 command_error "Proof not completed! metasenv is not empty!";
263 let proved_ty,ugraph =
264 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
267 CicReduction.are_convertible [] proved_ty ty ugraph
271 ("The type of your proof is not convertible with the "^
272 "type you've declared!");
273 MatitaLog.message (sprintf "%s defined" suri);
274 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
276 let name = UriManager.name_of_uri uri in
277 let new_env = env_of_list [(name,suri)] status.aliases in
278 {status with aliases = new_env }
280 {status with proof_status = No_proof }
281 | TacticAst.Inductive (loc, dummy_params, types) ->
282 (* dummy_params are not real params, it is a list of nothing, and the only
283 * semantic content is the len, that is leftno (note: leftno and pamaters
284 * have nothing in common).
288 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
291 let uri = UriManager.uri_of_string suri in
292 let leftno = List.length dummy_params in
293 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
295 CicTypeChecker.typecheck_mutual_inductive_defs uri
296 (types, [], leftno) CicUniv.empty_ugraph
299 MatitaSync.add_inductive_def
300 ~uri ~types ~params:[] ~leftno ~ugraph status
302 (* aliases for the constructors and types *)
303 let aliases = env_of_list (extract_alias types uri) status.aliases in
304 (* aliases for the eliminations principles *)
306 let base = String.sub suri 0 (String.length suri - 4) in
311 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
312 ) status.objects then
313 let u = base ^ suffix in
314 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
317 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
319 let status = {status with proof_status = No_proof } in
320 { status with aliases = aliases}
321 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
323 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
327 match status.proof_status with
328 | Intermediate metasenv ->
329 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
332 let initial_proof = (Some uri, metasenv, body, ty) in
333 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
334 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
336 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
338 let metasenv = MatitaMisc.get_proof_metasenv status in
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 CicMetaSubst.ppmetasenv metasenv []) ;
349 let body = CicMetaSubst.apply_subst subst body in
350 let ty = CicMetaSubst.apply_subst subst ty in
351 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
353 let suri = UriManager.string_of_uri uri in
354 let new_env = env_of_list [(name,suri)] status.aliases in
355 {status with aliases = new_env }
357 {status with proof_status = No_proof}
358 | TacticAst.Theorem (_, _, None, _, _) ->
359 command_error "The grammar should avoid having unnamed theorems!"
360 | TacticAst.Coercion (loc, coercion) ->
361 eval_coercion status coercion
362 | TacticAst.Alias (loc, spec) ->
364 | TacticAst.Ident_alias (id,uri) ->
365 {status with aliases =
366 DisambiguateTypes.Environment.add
367 (DisambiguateTypes.Id id)
368 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
370 | TacticAst.Symbol_alias (symb, instance, desc) ->
371 {status with aliases =
372 DisambiguateTypes.Environment.add
373 (DisambiguateTypes.Symbol (symb,instance))
374 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
376 | TacticAst.Number_alias (instance,desc) ->
377 {status with aliases =
378 DisambiguateTypes.Environment.add
379 (DisambiguateTypes.Num instance)
380 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
382 let eval_executable status ex =
384 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
385 | TacticAst.Command (_, cmd) -> eval_command status cmd
386 | TacticAst.Macro (_, mac) ->
387 command_error (sprintf "The macro %s can't be in a script"
388 (TacticAstPp.pp_macro_cic mac))
390 let eval_comment status c = status
394 | TacticAst.Executable (_,ex) -> eval_executable status ex
395 | TacticAst.Comment (_,c) -> eval_comment status c
397 let disambiguate_term status term =
398 let (aliases, metasenv, cic, _) =
400 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
401 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
402 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
408 match status.proof_status with
409 | No_proof -> Intermediate metasenv
410 | Incomplete_proof ((uri, _, proof, ty), goal) ->
411 Incomplete_proof ((uri, metasenv, proof, ty), goal)
412 | Intermediate _ -> Intermediate metasenv
413 | Proof _ -> assert false
418 proof_status = proof_status }
422 let disambiguate_terms status terms =
423 let term = CicAst.pack terms in
424 let status, term = disambiguate_term status term in
425 status, CicUtil.unpack term
427 let disambiguate_tactic status = function
428 | TacticAst.Transitivity (loc, term) ->
429 let status, cic = disambiguate_term status term in
430 status, TacticAst.Transitivity (loc, cic)
431 | TacticAst.Apply (loc, term) ->
432 let status, cic = disambiguate_term status term in
433 status, TacticAst.Apply (loc, cic)
434 | TacticAst.Absurd (loc, term) ->
435 let status, cic = disambiguate_term status term in
436 status, TacticAst.Absurd (loc, cic)
437 | TacticAst.Exact (loc, term) ->
438 let status, cic = disambiguate_term status term in
439 status, TacticAst.Exact (loc, cic)
440 | TacticAst.Cut (loc, term) ->
441 let status, cic = disambiguate_term status term in
442 status, TacticAst.Cut (loc, cic)
443 | TacticAst.Elim (loc, term, Some term') ->
444 let status, cic1 = disambiguate_term status term in
445 let status, cic2 = disambiguate_term status term' in
446 status, TacticAst.Elim (loc, cic1, Some cic2)
447 | TacticAst.Elim (loc, term, None) ->
448 let status, cic = disambiguate_term status term in
449 status, TacticAst.Elim (loc, cic, None)
450 | TacticAst.ElimType (loc, term) ->
451 let status, cic = disambiguate_term status term in
452 status, TacticAst.ElimType (loc, cic)
453 | TacticAst.Replace (loc, what, with_what) ->
454 let status, cic1 = disambiguate_term status what in
455 let status, cic2 = disambiguate_term status with_what in
456 status, TacticAst.Replace (loc, cic1, cic2)
457 | TacticAst.Change (loc, what, with_what, ident) ->
458 let status, cic1 = disambiguate_term status what in
459 let status, cic2 = disambiguate_term status with_what in
460 status, TacticAst.Change (loc, cic1, cic2, ident)
462 (* TODO Zack a lot more of tactics to be implemented here ... *)
463 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
464 | TacticAst.Change of 'term * 'term * 'ident option
465 | TacticAst.Decompose of 'ident * 'ident list
466 | TacticAst.Discriminate of 'ident
467 | TacticAst.Fold of reduction_kind * 'term
468 | TacticAst.Injection of 'ident
469 | TacticAst.Replace_pattern of 'term pattern * 'term
471 | TacticAst.LetIn (loc,term,name) ->
472 let status, term = disambiguate_term status term in
473 status, TacticAst.LetIn (loc,term,name)
474 | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
475 let path = Disambiguate.interpretate [] status.aliases path in
476 status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
477 | TacticAst.Reduce (loc, reduction_kind, opts) ->
480 | None -> status, None
483 List.fold_right (fun t (status,acc) ->
484 let status',t' = disambiguate_term status t in
488 status, Some (l, pat)
490 status, TacticAst.Reduce (loc, reduction_kind, opts)
491 | TacticAst.Rewrite (loc,dir,t,ident) ->
492 let status, term = disambiguate_term status t in
493 status, TacticAst.Rewrite (loc,dir,term,ident)
494 | TacticAst.Intros (loc, num, names) ->
495 status, TacticAst.Intros (loc, num, names)
496 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
497 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
498 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
499 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
500 | TacticAst.Exists loc -> status, TacticAst.Exists loc
501 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
502 | TacticAst.Left loc -> status, TacticAst.Left loc
503 | TacticAst.Right loc -> status, TacticAst.Right loc
504 | TacticAst.Ring loc -> status, TacticAst.Ring loc
505 | TacticAst.Split loc -> status, TacticAst.Split loc
506 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
507 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
509 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
512 let rec disambiguate_tactical status = function
513 | TacticAst.Tactic (loc, tactic) ->
514 let status, tac = disambiguate_tactic status tactic in
515 status, TacticAst.Tactic (loc, tac)
516 | TacticAst.Do (loc, num, tactical) ->
517 let status, tac = disambiguate_tactical status tactical in
518 status, TacticAst.Do (loc, num, tac)
519 | TacticAst.Repeat (loc, tactical) ->
520 let status, tac = disambiguate_tactical status tactical in
521 status, TacticAst.Repeat (loc, tac)
522 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
523 let status, tacticals = disambiguate_tacticals status tacticals in
524 let tacticals = List.rev tacticals in
525 status, TacticAst.Seq (loc, tacticals)
526 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
527 let status, tactical = disambiguate_tactical status tactical in
528 let status, tacticals = disambiguate_tacticals status tacticals in
529 status, TacticAst.Then (loc, tactical, tacticals)
530 | TacticAst.Tries (loc, tacticals) ->
531 let status, tacticals = disambiguate_tacticals status tacticals in
532 status, TacticAst.Tries (loc, tacticals)
533 | TacticAst.Try (loc, tactical) ->
534 let status, tactical = disambiguate_tactical status tactical in
535 status, TacticAst.Try (loc, tactical)
536 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
539 and disambiguate_tacticals status tacticals =
540 let status, tacticals =
542 (fun (status, tacticals) tactical ->
543 let status, tac = disambiguate_tactical status tactical in
544 status, tac :: tacticals)
548 let tacticals = List.rev tacticals in
551 let disambiguate_inddef status params indTypes =
552 let add_pi binders t =
554 (fun (name, ast) acc ->
555 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
559 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
561 let binders = ind_binders @ params in
563 let add_ast ast = asts := ast :: !asts in
564 let paramsno = List.length params in
565 let indbindersno = List.length ind_binders in
567 (fun (name, _, typ, constructors) ->
568 add_ast (add_pi params typ);
569 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
571 let status, terms = disambiguate_terms status !asts in
572 let terms = ref (List.rev terms) in
574 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
578 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
582 let counter = ref 0 in
586 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
589 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
592 (fun acc (name, inductive, typ, constructors) ->
593 let cicTyp = get_term () in
594 let cicConstructors =
596 (fun acc (name, _) ->
598 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
603 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
606 let cicIndTypes = List.rev cicIndTypes in
607 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
609 let disambiguate_command status = function
610 | TacticAst.Inductive (loc, params, types) ->
611 let (status, (uri, (ind_types, vars, paramsno))) =
612 disambiguate_inddef status params types
614 let rec mk_list = function
616 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
618 (* once we've built the cic inductive types we no longer need terms
619 corresponding to parameters, but we need the leftno, and we encode
620 it as the length of dummy_params
622 let dummy_params = mk_list paramsno in
623 status, TacticAst.Inductive (loc, dummy_params, ind_types)
624 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
625 let status, ty = disambiguate_term status ty in
628 | None -> status, None
630 let status, body = disambiguate_term status body in
633 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
634 | TacticAst.Coercion (loc, term) ->
635 let status, term = disambiguate_term status term in
636 status, TacticAst.Coercion (loc,term)
637 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
639 | TacticAst.Alias _ as x -> status, x
641 let disambiguate_executable status ex =
643 | TacticAst.Tactical (loc, tac) ->
644 let status, tac = disambiguate_tactical status tac in
645 status, (TacticAst.Tactical (loc, tac))
646 | TacticAst.Command (loc, cmd) ->
647 let status, cmd = disambiguate_command status cmd in
648 status, (TacticAst.Command (loc, cmd))
649 | TacticAst.Macro (_, mac) ->
651 (sprintf ("The engine is not allowed to disambiguate any macro, "^^
652 "in particular %s") (TacticAstPp.pp_macro_ast mac))
654 let disambiguate_comment status c =
656 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
657 | TacticAst.Code (loc,ex) ->
658 let status, ex = disambiguate_executable status ex in
659 status, TacticAst.Code (loc,ex)
661 let disambiguate_statement status statement =
663 | TacticAst.Comment (loc,c) ->
664 let status, c = disambiguate_comment status c in
665 status, TacticAst.Comment (loc,c)
666 | TacticAst.Executable (loc,ex) ->
667 let status, ex = disambiguate_executable status ex in
668 status, TacticAst.Executable (loc,ex)
670 let eval_ast status ast =
671 let status,st = disambiguate_statement status ast in
672 (* this disambiguation step should be deferred to support tacticals *)
675 let eval_from_stream status str cb =
676 let stl = CicTextualParser2.parse_statements str in
678 (fun status ast -> cb status ast;eval_ast status ast) status
681 let eval_string status str =
682 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
684 let default_options () =
686 StringMap.add "baseuri"
688 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
692 StringMap.add "basedir"
693 (String (Helm_registry.get "matita.basedir" ))
700 aliases = DisambiguateTypes.empty_environment;
701 proof_status = No_proof;
702 options = default_options ();