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
231 let ty_src = CicReduction.whd context ty_src in
232 UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
235 let ty_tgt = CicReduction.whd context ty_tgt in
236 UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
239 (* also adds them to the Db *)
240 CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
244 fun s (uri,o,ugraph) ->
246 | Cic.Constant (_,Some body, ty, params, attrs) ->
247 MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
249 ) status new_coercions
251 {status with proof_status = No_proof}
253 let eval_command status cmd =
255 | TacticAst.Set (loc, name, value) -> set_option status name value
256 | TacticAst.Qed loc ->
257 let uri, metasenv, bo, ty =
258 match status.proof_status with
259 | Proof (Some uri, metasenv, body, ty) ->
260 uri, metasenv, body, ty
261 | Proof (None, metasenv, body, ty) ->
263 ("Someone allows to start a thm without giving the "^
264 "name/uri. This should be fixed!")
265 | _-> command_error "You can't qed an uncomplete theorem"
267 let suri = UriManager.string_of_uri uri in
268 if metasenv <> [] then
269 command_error "Proof not completed! metasenv is not empty!";
270 let proved_ty,ugraph =
271 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
274 CicReduction.are_convertible [] proved_ty ty ugraph
278 ("The type of your proof is not convertible with the "^
279 "type you've declared!");
280 MatitaLog.message (sprintf "%s defined" suri);
281 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
283 let name = UriManager.name_of_uri uri in
284 let new_env = env_of_list [(name,suri)] status.aliases in
285 {status with aliases = new_env }
287 {status with proof_status = No_proof }
288 | TacticAst.Inductive (loc, dummy_params, types) ->
289 (* dummy_params are not real params, it is a list of nothing, and the only
290 * semantic content is the len, that is leftno (note: leftno and pamaters
291 * have nothing in common).
295 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
298 let uri = UriManager.uri_of_string suri in
299 let leftno = List.length dummy_params in
300 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
302 CicTypeChecker.typecheck_mutual_inductive_defs uri
303 (types, [], leftno) CicUniv.empty_ugraph
306 MatitaSync.add_inductive_def
307 ~uri ~types ~params:[] ~leftno ~ugraph status
309 (* aliases for the constructors and types *)
310 let aliases = env_of_list (extract_alias types uri) status.aliases in
311 (* aliases for the eliminations principles *)
313 let base = String.sub suri 0 (String.length suri - 4) in
318 fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
319 ) status.objects then
320 let u = base ^ suffix in
321 (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
324 ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
326 let status = {status with proof_status = No_proof } in
327 { status with aliases = aliases}
328 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
330 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
334 match status.proof_status with
335 | Intermediate metasenv ->
336 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
339 let initial_proof = (Some uri, metasenv, body, ty) in
340 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
341 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
343 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
345 let metasenv = MatitaMisc.get_proof_metasenv status in
346 let (body_type, ugraph) =
347 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
349 let (subst, metasenv, ugraph) =
350 CicUnification.fo_unif metasenv [] body_type ty ugraph
352 if metasenv <> [] then
354 "metasenv not empty while giving a definition with body: " ^
355 CicMetaSubst.ppmetasenv metasenv []) ;
356 let body = CicMetaSubst.apply_subst subst body in
357 let ty = CicMetaSubst.apply_subst subst ty in
358 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
360 let suri = UriManager.string_of_uri uri in
361 let new_env = env_of_list [(name,suri)] status.aliases in
362 {status with aliases = new_env }
364 {status with proof_status = No_proof}
365 | TacticAst.Theorem (_, _, None, _, _) ->
366 command_error "The grammar should avoid having unnamed theorems!"
367 | TacticAst.Coercion (loc, coercion) ->
368 eval_coercion status coercion
369 | TacticAst.Alias (loc, spec) ->
371 | TacticAst.Ident_alias (id,uri) ->
372 {status with aliases =
373 DisambiguateTypes.Environment.add
374 (DisambiguateTypes.Id id)
375 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
377 | TacticAst.Symbol_alias (symb, instance, desc) ->
378 {status with aliases =
379 DisambiguateTypes.Environment.add
380 (DisambiguateTypes.Symbol (symb,instance))
381 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
383 | TacticAst.Number_alias (instance,desc) ->
384 {status with aliases =
385 DisambiguateTypes.Environment.add
386 (DisambiguateTypes.Num instance)
387 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
389 let eval_executable status ex =
391 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
392 | TacticAst.Command (_, cmd) -> eval_command status cmd
393 | TacticAst.Macro (_, mac) ->
394 command_error (sprintf "The macro %s can't be in a script"
395 (TacticAstPp.pp_macro_cic mac))
397 let eval_comment status c = status
401 | TacticAst.Executable (_,ex) -> eval_executable status ex
402 | TacticAst.Comment (_,c) -> eval_comment status c
404 let disambiguate_term status term =
405 let (aliases, metasenv, cic, _) =
407 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
408 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
409 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
415 match status.proof_status with
416 | No_proof -> Intermediate metasenv
417 | Incomplete_proof ((uri, _, proof, ty), goal) ->
418 Incomplete_proof ((uri, metasenv, proof, ty), goal)
419 | Intermediate _ -> Intermediate metasenv
420 | Proof _ -> assert false
425 proof_status = proof_status }
429 let disambiguate_terms status terms =
430 let term = CicAst.pack terms in
431 let status, term = disambiguate_term status term in
432 status, CicUtil.unpack term
434 let disambiguate_tactic status = function
435 | TacticAst.Transitivity (loc, term) ->
436 let status, cic = disambiguate_term status term in
437 status, TacticAst.Transitivity (loc, cic)
438 | TacticAst.Apply (loc, term) ->
439 let status, cic = disambiguate_term status term in
440 status, TacticAst.Apply (loc, cic)
441 | TacticAst.Absurd (loc, term) ->
442 let status, cic = disambiguate_term status term in
443 status, TacticAst.Absurd (loc, cic)
444 | TacticAst.Exact (loc, term) ->
445 let status, cic = disambiguate_term status term in
446 status, TacticAst.Exact (loc, cic)
447 | TacticAst.Cut (loc, term) ->
448 let status, cic = disambiguate_term status term in
449 status, TacticAst.Cut (loc, cic)
450 | TacticAst.Elim (loc, term, Some term') ->
451 let status, cic1 = disambiguate_term status term in
452 let status, cic2 = disambiguate_term status term' in
453 status, TacticAst.Elim (loc, cic1, Some cic2)
454 | TacticAst.Elim (loc, term, None) ->
455 let status, cic = disambiguate_term status term in
456 status, TacticAst.Elim (loc, cic, None)
457 | TacticAst.ElimType (loc, term) ->
458 let status, cic = disambiguate_term status term in
459 status, TacticAst.ElimType (loc, cic)
460 | TacticAst.Replace (loc, what, with_what) ->
461 let status, cic1 = disambiguate_term status what in
462 let status, cic2 = disambiguate_term status with_what in
463 status, TacticAst.Replace (loc, cic1, cic2)
464 | TacticAst.Change (loc, what, with_what, ident) ->
465 let status, cic1 = disambiguate_term status what in
466 let status, cic2 = disambiguate_term status with_what in
467 status, TacticAst.Change (loc, cic1, cic2, ident)
469 (* TODO Zack a lot more of tactics to be implemented here ... *)
470 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
471 | TacticAst.Change of 'term * 'term * 'ident option
472 | TacticAst.Decompose of 'ident * 'ident list
473 | TacticAst.Discriminate of 'ident
474 | TacticAst.Fold of reduction_kind * 'term
475 | TacticAst.Injection of 'ident
476 | TacticAst.Replace_pattern of 'term pattern * 'term
478 | TacticAst.LetIn (loc,term,name) ->
479 let status, term = disambiguate_term status term in
480 status, TacticAst.LetIn (loc,term,name)
481 | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
482 let path = Disambiguate.interpretate [] status.aliases path in
483 status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
484 | TacticAst.Reduce (loc, reduction_kind, opts) ->
487 | None -> status, None
490 List.fold_right (fun t (status,acc) ->
491 let status',t' = disambiguate_term status t in
495 status, Some (l, pat)
497 status, TacticAst.Reduce (loc, reduction_kind, opts)
498 | TacticAst.Rewrite (loc,dir,t,ident) ->
499 let status, term = disambiguate_term status t in
500 status, TacticAst.Rewrite (loc,dir,term,ident)
501 | TacticAst.Intros (loc, num, names) ->
502 status, TacticAst.Intros (loc, num, names)
503 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
504 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
505 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
506 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
507 | TacticAst.Exists loc -> status, TacticAst.Exists loc
508 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
509 | TacticAst.Left loc -> status, TacticAst.Left loc
510 | TacticAst.Right loc -> status, TacticAst.Right loc
511 | TacticAst.Ring loc -> status, TacticAst.Ring loc
512 | TacticAst.Split loc -> status, TacticAst.Split loc
513 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
514 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
516 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
519 let rec disambiguate_tactical status = function
520 | TacticAst.Tactic (loc, tactic) ->
521 let status, tac = disambiguate_tactic status tactic in
522 status, TacticAst.Tactic (loc, tac)
523 | TacticAst.Do (loc, num, tactical) ->
524 let status, tac = disambiguate_tactical status tactical in
525 status, TacticAst.Do (loc, num, tac)
526 | TacticAst.Repeat (loc, tactical) ->
527 let status, tac = disambiguate_tactical status tactical in
528 status, TacticAst.Repeat (loc, tac)
529 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
530 let status, tacticals = disambiguate_tacticals status tacticals in
531 let tacticals = List.rev tacticals in
532 status, TacticAst.Seq (loc, tacticals)
533 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
534 let status, tactical = disambiguate_tactical status tactical in
535 let status, tacticals = disambiguate_tacticals status tacticals in
536 status, TacticAst.Then (loc, tactical, tacticals)
537 | TacticAst.Tries (loc, tacticals) ->
538 let status, tacticals = disambiguate_tacticals status tacticals in
539 status, TacticAst.Tries (loc, tacticals)
540 | TacticAst.Try (loc, tactical) ->
541 let status, tactical = disambiguate_tactical status tactical in
542 status, TacticAst.Try (loc, tactical)
543 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
546 and disambiguate_tacticals status tacticals =
547 let status, tacticals =
549 (fun (status, tacticals) tactical ->
550 let status, tac = disambiguate_tactical status tactical in
551 status, tac :: tacticals)
555 let tacticals = List.rev tacticals in
558 let disambiguate_inddef status params indTypes =
559 let add_pi binders t =
561 (fun (name, ast) acc ->
562 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
566 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
568 let binders = ind_binders @ params in
570 let add_ast ast = asts := ast :: !asts in
571 let paramsno = List.length params in
572 let indbindersno = List.length ind_binders in
574 (fun (name, _, typ, constructors) ->
575 add_ast (add_pi params typ);
576 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
578 let status, terms = disambiguate_terms status !asts in
579 let terms = ref (List.rev terms) in
581 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
585 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
589 let counter = ref 0 in
593 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
596 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
599 (fun acc (name, inductive, typ, constructors) ->
600 let cicTyp = get_term () in
601 let cicConstructors =
603 (fun acc (name, _) ->
605 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
610 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
613 let cicIndTypes = List.rev cicIndTypes in
614 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
616 let disambiguate_command status = function
617 | TacticAst.Inductive (loc, params, types) ->
618 let (status, (uri, (ind_types, vars, paramsno))) =
619 disambiguate_inddef status params types
621 let rec mk_list = function
623 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
625 (* once we've built the cic inductive types we no longer need terms
626 corresponding to parameters, but we need the leftno, and we encode
627 it as the length of dummy_params
629 let dummy_params = mk_list paramsno in
630 status, TacticAst.Inductive (loc, dummy_params, ind_types)
631 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
632 let status, ty = disambiguate_term status ty in
635 | None -> status, None
637 let status, body = disambiguate_term status body in
640 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
641 | TacticAst.Coercion (loc, term) ->
642 let status, term = disambiguate_term status term in
643 status, TacticAst.Coercion (loc,term)
644 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
646 | TacticAst.Alias _ as x -> status, x
648 let disambiguate_executable status ex =
650 | TacticAst.Tactical (loc, tac) ->
651 let status, tac = disambiguate_tactical status tac in
652 status, (TacticAst.Tactical (loc, tac))
653 | TacticAst.Command (loc, cmd) ->
654 let status, cmd = disambiguate_command status cmd in
655 status, (TacticAst.Command (loc, cmd))
656 | TacticAst.Macro (_, mac) ->
657 command_error (sprintf "The macro %s can't be in a script"
658 (TacticAstPp.pp_macro_ast mac))
660 let disambiguate_comment status c =
662 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
663 | TacticAst.Code (loc,ex) ->
664 let status, ex = disambiguate_executable status ex in
665 status, TacticAst.Code (loc,ex)
667 let disambiguate_statement status statement =
669 | TacticAst.Comment (loc,c) ->
670 let status, c = disambiguate_comment status c in
671 status, TacticAst.Comment (loc,c)
672 | TacticAst.Executable (loc,ex) ->
673 let status, ex = disambiguate_executable status ex in
674 status, TacticAst.Executable (loc,ex)
676 let eval_ast status ast =
677 let status,st = disambiguate_statement status ast in
678 (* this disambiguation step should be deferred to support tacticals *)
681 let eval_from_stream status str cb =
682 let stl = CicTextualParser2.parse_statements str in
684 (fun status ast -> cb status ast;eval_ast status ast) status
687 let eval_string status str =
688 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
690 let default_options () =
692 StringMap.add "baseuri"
694 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
698 StringMap.add "basedir"
699 (String (Helm_registry.get "matita.basedir" ))
706 aliases = DisambiguateTypes.empty_environment;
707 proof_status = No_proof;
708 options = default_options ();