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 (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
83 raise (ProofEngineTypes.Fail
84 (ident ^ " is not an hypothesis"))
87 | Some (_, Cic.Decl term) -> term
88 | Some (_, Cic.Def (term,ty)) -> term
89 | None -> assert false),true
91 let pointers = CicUtil.select ~term:where ~context:path in
92 (match reduction_kind with
94 ProofEngineTypes.apply_tactic
95 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
98 ProofEngineTypes.apply_tactic
99 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
102 ProofEngineTypes.apply_tactic
103 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
106 ProofEngineTypes.apply_tactic
107 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
109 | TacticAst.Reduce (_,reduction_kind,opts) ->
110 let terms, also_in_hypotheses =
112 | Some (l,`Goal) -> Some l, false
113 | Some (l,`Everywhere) -> Some l, true
114 | None -> None, false
116 (match reduction_kind with
117 | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
118 | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
119 | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
120 | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
121 | TacticAst.Rewrite (_,dir,t,ident) ->
123 EqualityTactics.rewrite_tac ~term:t
125 EqualityTactics.rewrite_back_tac ~term:t
128 let eval_tactical status tac =
129 let apply_tactic tactic =
131 ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
136 let (_,metasenv,_,_) = proof in
139 | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
140 | ng::_ -> Incomplete_proof (proof, ng)
142 { status with proof_status = new_status }
144 let rec tactical_of_ast = function
145 | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
146 | TacticAst.Fail loc -> Tacticals.fail
147 | TacticAst.Do (loc, num, tactical) ->
148 Tacticals.do_tactic num (tactical_of_ast tactical)
149 | TacticAst.IdTac loc -> Tacticals.id_tac
150 | TacticAst.Repeat (loc, tactical) ->
151 Tacticals.repeat_tactic (tactical_of_ast tactical)
152 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
153 Tacticals.seq (List.map tactical_of_ast tacticals)
154 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
155 Tacticals.thens (tactical_of_ast tactical)
156 (List.map tactical_of_ast tacticals)
157 | TacticAst.Tries (loc, tacticals) ->
158 Tacticals.try_tactics
159 (List.map (fun t -> "", tactical_of_ast t) tacticals)
160 | TacticAst.Try (loc, tactical) ->
161 Tacticals.try_tactic (tactical_of_ast tactical)
163 apply_tactic (tactical_of_ast tac)
165 let eval_coercion status coercion =
166 let coer_uri,coer_ty =
171 CicEnvironment.get_obj CicUniv.empty_ugraph uri
174 | Cic.Constant (_,_,ty,_,_)
175 | Cic.Variable (_,_,ty,_,_) ->
178 | Cic.MutConstruct (uri,t,c,_) ->
180 CicEnvironment.get_obj CicUniv.empty_ugraph uri
183 | Cic.InductiveDefinition (l,_,_,_) ->
184 let (_,_,_,cl) = List.nth l t in
185 let (_,cty) = List.nth cl c in
190 (* we have to get the source and the tgt type uri
191 * in Coq syntax we have already their names, but
192 * since we don't support Funclass and similar I think
193 * all the coercion should be of the form
195 * So we should be able to extract them from the coercion type
197 let extract_last_two_p ty =
198 let rec aux = function
199 | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
200 | Cic.Prod( _, src, tgt) -> src, tgt
205 let ty_src,ty_tgt = extract_last_two_p coer_ty in
208 let ty_src = CicReduction.whd context ty_src in
209 UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
212 let ty_tgt = CicReduction.whd context ty_tgt in
213 UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
216 (* also adds them to the Db *)
217 CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
221 fun s (uri,o,ugraph) ->
223 | Cic.Constant (_,Some body, ty, params, attrs) ->
224 MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
226 ) status new_coercions
228 {status with proof_status = No_proof}
230 let eval_command status cmd =
232 | TacticAst.Set (loc, name, value) -> set_option status name value
233 | TacticAst.Qed loc ->
234 let uri, metasenv, bo, ty =
235 match status.proof_status with
236 | Proof (Some uri, metasenv, body, ty) ->
237 uri, metasenv, body, ty
238 | Proof (None, metasenv, body, ty) ->
240 ("Someone allows to start a thm without giving the "^
241 "name/uri. This should be fixed!")
242 | _-> command_error "You can't qed an uncomplete theorem"
244 let suri = UriManager.string_of_uri uri in
245 if metasenv <> [] then
246 command_error "Proof not completed! metasenv is not empty!";
247 let proved_ty,ugraph =
248 CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
251 CicReduction.are_convertible [] proved_ty ty ugraph
255 ("The type of your proof is not convertible with the "^
256 "type you've declared!");
257 MatitaLog.message (sprintf "%s defined" suri);
258 let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
259 {status with proof_status = No_proof }
260 | TacticAst.Record (loc, params, name, ty, fields) ->
261 let suri = MatitaMisc.qualify status name ^ ".ind" in
262 let record_spec = (suri, params, ty, fields) in
263 let status = MatitaSync.add_record_def record_spec status in
264 {status with proof_status = No_proof }
265 | TacticAst.Inductive (loc, dummy_params, types) ->
266 (* dummy_params are not real params, it is a list of nothing, and the only
267 * semantic content is the len, that is leftno (note: leftno and
268 * paramaters have nothing in common).
272 | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
275 let uri = UriManager.uri_of_string suri in
276 let leftno = List.length dummy_params in
277 let obj = Cic.InductiveDefinition (types, [], leftno, []) in
279 CicTypeChecker.typecheck_mutual_inductive_defs uri
280 (types, [], leftno) CicUniv.empty_ugraph
283 MatitaSync.add_inductive_def ~uri ~types ~leftno ~ugraph status
285 {status with proof_status = No_proof }
286 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
288 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
292 match status.proof_status with
293 | Intermediate metasenv ->
294 ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
297 let initial_proof = (Some uri, metasenv, body, ty) in
298 { status with proof_status = Incomplete_proof (initial_proof,goalno)}
299 | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
301 UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
303 let metasenv = MatitaMisc.get_proof_metasenv status in
304 let (body_type, ugraph) =
305 CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
307 let (subst, metasenv, ugraph) =
308 CicUnification.fo_unif metasenv [] body_type ty ugraph
310 if metasenv <> [] then
312 "metasenv not empty while giving a definition with body: " ^
313 CicMetaSubst.ppmetasenv metasenv []) ;
314 let body = CicMetaSubst.apply_subst subst body in
315 let ty = CicMetaSubst.apply_subst subst ty in
316 let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
317 {status with proof_status = No_proof}
318 | TacticAst.Theorem (_, _, None, _, _) ->
319 command_error "The grammar should avoid having unnamed theorems!"
320 | TacticAst.Coercion (loc, coercion) ->
321 eval_coercion status coercion
322 | TacticAst.Alias (loc, spec) ->
324 | TacticAst.Ident_alias (id,uri) ->
325 {status with aliases =
326 DisambiguateTypes.Environment.add
327 (DisambiguateTypes.Id id)
328 ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
330 | TacticAst.Symbol_alias (symb, instance, desc) ->
331 {status with aliases =
332 DisambiguateTypes.Environment.add
333 (DisambiguateTypes.Symbol (symb,instance))
334 (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
336 | TacticAst.Number_alias (instance,desc) ->
337 {status with aliases =
338 DisambiguateTypes.Environment.add
339 (DisambiguateTypes.Num instance)
340 (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
342 let eval_executable status ex =
344 | TacticAst.Tactical (_, tac) -> eval_tactical status tac
345 | TacticAst.Command (_, cmd) -> eval_command status cmd
346 | TacticAst.Macro (_, mac) ->
347 command_error (sprintf "The macro %s can't be in a script"
348 (TacticAstPp.pp_macro_cic mac))
350 let eval_comment status c = status
354 | TacticAst.Executable (_,ex) -> eval_executable status ex
355 | TacticAst.Comment (_,c) -> eval_comment status c
357 let disambiguate_term status term =
358 let (aliases, metasenv, cic, _) =
360 MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
361 ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
362 ~metasenv:(MatitaMisc.get_proof_metasenv status) term
368 match status.proof_status with
369 | No_proof -> Intermediate metasenv
370 | Incomplete_proof ((uri, _, proof, ty), goal) ->
371 Incomplete_proof ((uri, metasenv, proof, ty), goal)
372 | Intermediate _ -> Intermediate metasenv
373 | Proof _ -> assert false
378 proof_status = proof_status }
382 let disambiguate_closedtypes status terms =
383 let term = CicAst.pack terms in
384 let status, term = disambiguate_term status term in
385 status, CicUtil.unpack term
387 let disambiguate_tactic status = function
388 | TacticAst.Transitivity (loc, term) ->
389 let status, cic = disambiguate_term status term in
390 status, TacticAst.Transitivity (loc, cic)
391 | TacticAst.Apply (loc, term) ->
392 let status, cic = disambiguate_term status term in
393 status, TacticAst.Apply (loc, cic)
394 | TacticAst.Absurd (loc, term) ->
395 let status, cic = disambiguate_term status term in
396 status, TacticAst.Absurd (loc, cic)
397 | TacticAst.Exact (loc, term) ->
398 let status, cic = disambiguate_term status term in
399 status, TacticAst.Exact (loc, cic)
400 | TacticAst.Cut (loc, term) ->
401 let status, cic = disambiguate_term status term in
402 status, TacticAst.Cut (loc, cic)
403 | TacticAst.Elim (loc, term, Some term') ->
404 let status, cic1 = disambiguate_term status term in
405 let status, cic2 = disambiguate_term status term' in
406 status, TacticAst.Elim (loc, cic1, Some cic2)
407 | TacticAst.Elim (loc, term, None) ->
408 let status, cic = disambiguate_term status term in
409 status, TacticAst.Elim (loc, cic, None)
410 | TacticAst.ElimType (loc, term) ->
411 let status, cic = disambiguate_term status term in
412 status, TacticAst.ElimType (loc, cic)
413 | TacticAst.Replace (loc, what, with_what) ->
414 let status, cic1 = disambiguate_term status what in
415 let status, cic2 = disambiguate_term status with_what in
416 status, TacticAst.Replace (loc, cic1, cic2)
417 | TacticAst.Change (loc, what, with_what, ident) ->
418 let status, cic1 = disambiguate_term status what in
419 let status, cic2 = disambiguate_term status with_what in
420 status, TacticAst.Change (loc, cic1, cic2, ident)
422 (* TODO Zack a lot more of tactics to be implemented here ... *)
423 | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
424 | TacticAst.Change of 'term * 'term * 'ident option
425 | TacticAst.Decompose of 'ident * 'ident list
426 | TacticAst.Discriminate of 'ident
427 | TacticAst.Fold of reduction_kind * 'term
428 | TacticAst.Injection of 'ident
429 | TacticAst.Replace_pattern of 'term pattern * 'term
431 | TacticAst.LetIn (loc,term,name) ->
432 let status, term = disambiguate_term status term in
433 status, TacticAst.LetIn (loc,term,name)
434 | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
435 let path = Disambiguate.interpretate [] status.aliases path in
436 status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
437 | TacticAst.Reduce (loc, reduction_kind, opts) ->
440 | None -> status, None
443 List.fold_right (fun t (status,acc) ->
444 let status',t' = disambiguate_term status t in
448 status, Some (l, pat)
450 status, TacticAst.Reduce (loc, reduction_kind, opts)
451 | TacticAst.Rewrite (loc,dir,t,ident) ->
452 let status, term = disambiguate_term status t in
453 status, TacticAst.Rewrite (loc,dir,term,ident)
454 | TacticAst.Intros (loc, num, names) ->
455 status, TacticAst.Intros (loc, num, names)
456 | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
457 | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
458 | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
459 | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
460 | TacticAst.Exists loc -> status, TacticAst.Exists loc
461 | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
462 | TacticAst.Left loc -> status, TacticAst.Left loc
463 | TacticAst.Right loc -> status, TacticAst.Right loc
464 | TacticAst.Ring loc -> status, TacticAst.Ring loc
465 | TacticAst.Split loc -> status, TacticAst.Split loc
466 | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
467 | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
469 print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
472 let rec disambiguate_tactical status = function
473 | TacticAst.Tactic (loc, tactic) ->
474 let status, tac = disambiguate_tactic status tactic in
475 status, TacticAst.Tactic (loc, tac)
476 | TacticAst.Do (loc, num, tactical) ->
477 let status, tac = disambiguate_tactical status tactical in
478 status, TacticAst.Do (loc, num, tac)
479 | TacticAst.Repeat (loc, tactical) ->
480 let status, tac = disambiguate_tactical status tactical in
481 status, TacticAst.Repeat (loc, tac)
482 | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
483 let status, tacticals = disambiguate_tacticals status tacticals in
484 let tacticals = List.rev tacticals in
485 status, TacticAst.Seq (loc, tacticals)
486 | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
487 let status, tactical = disambiguate_tactical status tactical in
488 let status, tacticals = disambiguate_tacticals status tacticals in
489 status, TacticAst.Then (loc, tactical, tacticals)
490 | TacticAst.Tries (loc, tacticals) ->
491 let status, tacticals = disambiguate_tacticals status tacticals in
492 status, TacticAst.Tries (loc, tacticals)
493 | TacticAst.Try (loc, tactical) ->
494 let status, tactical = disambiguate_tactical status tactical in
495 status, TacticAst.Try (loc, tactical)
496 | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
499 and disambiguate_tacticals status tacticals =
500 let status, tacticals =
502 (fun (status, tacticals) tactical ->
503 let status, tac = disambiguate_tactical status tactical in
504 status, tac :: tacticals)
508 let tacticals = List.rev tacticals in
511 let disambiguate_inddef status params indTypes =
512 let add_pi binders t =
514 (fun (name, ast) acc ->
515 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
519 List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
521 let binders = ind_binders @ params in
523 let add_ast ast = asts := ast :: !asts in
524 let paramsno = List.length params in
525 let indbindersno = List.length ind_binders in
527 (fun (name, _, typ, constructors) ->
528 add_ast (add_pi params typ);
529 List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
531 let status, terms = disambiguate_closedtypes status !asts in
532 let terms = ref (List.rev terms) in
534 match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
538 | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
542 let counter = ref 0 in
546 CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
549 let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
552 (fun acc (name, inductive, typ, constructors) ->
553 let cicTyp = get_term () in
554 let cicConstructors =
556 (fun acc (name, _) ->
558 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
563 (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
566 let cicIndTypes = List.rev cicIndTypes in
567 status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
569 let disambiguate_record status params ty fields =
572 (fun (name,ast) acc ->
573 CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
574 (params @ ["",ty] @ fields) (CicAst.Sort `Type)
576 debug_print (CicAstPp.pp_term packed);
577 let status, packed = disambiguate_term status packed in
578 let rec split t = function
582 | Cic.Prod (_, src, tgt) ->
583 let l, t = split tgt tl in
587 let params, t = split packed params in
590 | Cic.Prod (_ , ty, t) -> ty, t
594 split (let t,_,_ = CicMetaSubst.delift_rels [] [] 1 t in t) fields
598 let disambiguate_command status = function
599 | TacticAst.Record(loc, params,name,ty,fields) ->
600 let params, ty, fields =
601 disambiguate_record status params ty fields
603 status, TacticAst.Record(loc, params, name, ty, fields)
604 | TacticAst.Inductive (loc, params, types) ->
605 let (status, (uri, (ind_types, vars, paramsno))) =
606 disambiguate_inddef status params types
608 let rec mk_list = function
610 | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
612 (* once we've built the cic inductive types we no longer need terms
613 corresponding to parameters, but we need the leftno, and we encode
614 it as the length of dummy_params
616 let dummy_params = mk_list paramsno in
617 status, TacticAst.Inductive (loc, dummy_params, ind_types)
618 | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
619 let status, ty = disambiguate_term status ty in
622 | None -> status, None
624 let status, body = disambiguate_term status body in
627 status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
628 | TacticAst.Coercion (loc, term) ->
629 let status, term = disambiguate_term status term in
630 status, TacticAst.Coercion (loc,term)
631 | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
633 | TacticAst.Alias _ as x -> status, x
635 let disambiguate_executable status ex =
637 | TacticAst.Tactical (loc, tac) ->
638 let status, tac = disambiguate_tactical status tac in
639 status, (TacticAst.Tactical (loc, tac))
640 | TacticAst.Command (loc, cmd) ->
641 let status, cmd = disambiguate_command status cmd in
642 status, (TacticAst.Command (loc, cmd))
643 | TacticAst.Macro (_, mac) ->
644 command_error (sprintf "The macro %s can't be in a script"
645 (TacticAstPp.pp_macro_ast mac))
647 let disambiguate_comment status c =
649 | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
650 | TacticAst.Code (loc,ex) ->
651 let status, ex = disambiguate_executable status ex in
652 status, TacticAst.Code (loc,ex)
654 let disambiguate_statement status statement =
656 | TacticAst.Comment (loc,c) ->
657 let status, c = disambiguate_comment status c in
658 status, TacticAst.Comment (loc,c)
659 | TacticAst.Executable (loc,ex) ->
660 let status, ex = disambiguate_executable status ex in
661 status, TacticAst.Executable (loc,ex)
663 let eval_ast status ast =
664 let status,st = disambiguate_statement status ast in
665 (* this disambiguation step should be deferred to support tacticals *)
668 let eval_from_stream status str cb =
669 let stl = CicTextualParser2.parse_statements str in
671 (fun status ast -> cb status ast;eval_ast status ast) status
674 let eval_string status str =
675 eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
677 let default_options () =
679 StringMap.add "baseuri"
681 (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
685 StringMap.add "basedir"
686 (String (Helm_registry.get "matita.basedir" ))
693 aliases = DisambiguateTypes.empty_environment;
694 proof_status = No_proof;
695 options = default_options ();