helm/matita/matitaEngine.ml

   1
   2 open Printf
   3
   4 open MatitaTypes
   5
   6
   7 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   8   * names as long as they are available, then it fallbacks to name generation
   9   * using FreshNamesGenerator module *)
  10 let namer_of names =
  11   let len = List.length names in
  12   let count = ref 0 in
  13   fun metasenv context name ~typ ->
  14     if !count < len then begin
  15       let name = Cic.Name (List.nth names !count) in
  16       incr count;
  17       name
  18     end else
  19       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  20
  21 let tactic_of_ast = function
  22   | TacticAst.Intros (_, None, names) ->
  23       (* TODO Zack implement intros length *)
  24       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  25   | TacticAst.Intros (_, Some num, names) ->
  26       (* TODO Zack implement intros length *)
  27       PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
  28   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  29   | TacticAst.Assumption _ -> Tactics.assumption
  30   | TacticAst.Contradiction _ -> Tactics.contradiction
  31   | TacticAst.Exists _ -> Tactics.exists
  32   | TacticAst.Fourier _ -> Tactics.fourier
  33   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  34   | TacticAst.Left _ -> Tactics.left
  35   | TacticAst.Right _ -> Tactics.right
  36   | TacticAst.Ring _ -> Tactics.ring
  37   | TacticAst.Split _ -> Tactics.split
  38   | TacticAst.Symmetry _ -> Tactics.symmetry
  39   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  40   | TacticAst.Apply (_, term) -> Tactics.apply term
  41   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  42   | TacticAst.Exact (_, term) -> Tactics.exact term
  43   | TacticAst.Cut (_, term) -> Tactics.cut term
  44   | TacticAst.Elim (_, term, _) ->
  45       (* TODO Zack implement "using" argument *)
  46       (* old: Tactics.elim_intros_simpl term *)
  47       Tactics.elim_intros term
  48   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  49   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  50   | TacticAst.Auto (_,num) ->
  51       AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
  52   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  53 (*
  54   (* TODO Zack a lot more of tactics to be implemented here ... *)
  55   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  56   | TacticAst.Change of 'term * 'term * 'ident option
  57   | TacticAst.Decompose of 'ident * 'ident list
  58   | TacticAst.Discriminate of 'ident
  59   | TacticAst.Fold of reduction_kind * 'term
  60   | TacticAst.Injection of 'ident
  61   | TacticAst.LetIn of 'term * 'ident
  62   | TacticAst.Replace_pattern of 'term pattern * 'term
  63 *)
  64   | TacticAst.Reduce (_,reduction_kind,opts) ->
  65       let terms, also_in_hypotheses =
  66         match opts with
  67         | Some (l,`Goal) -> Some l, false
  68         | Some (l,`Everywhere) -> Some l, true
  69         | None -> None, false
  70       in
  71       (match reduction_kind with
  72       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
  73       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
  74       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
  75   | TacticAst.Rewrite (_,dir,t,ident) ->
  76       if dir = `Left then
  77         EqualityTactics.rewrite_tac ~term:t
  78       else
  79         EqualityTactics.rewrite_back_tac ~term:t
  80   | _ -> assert false
  81
  82 let eval_tactical status tac =
  83   let apply_tactic tactic =
  84     let (proof, goals) =
  85       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
  86     in
  87     let new_status =
  88       match goals with
  89       | [] ->
  90           let (_,metasenv,_,_) = proof in
  91           (match metasenv with
  92           | [] -> Proof proof
  93           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
  94       | ng::_ -> Incomplete_proof (proof, ng)
  95     in
  96     { status with proof_status = new_status }
  97   in
  98   let rec tactical_of_ast = function
  99     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
 100     | TacticAst.Fail loc -> Tacticals.fail
 101     | TacticAst.Do (loc, num, tactical) ->
 102         Tacticals.do_tactic num (tactical_of_ast tactical)
 103     | TacticAst.IdTac loc -> Tacticals.id_tac
 104     | TacticAst.Repeat (loc, tactical) ->
 105         Tacticals.repeat_tactic (tactical_of_ast tactical)
 106     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 107         Tacticals.seq (List.map tactical_of_ast tacticals)
 108     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 109         Tacticals.thens (tactical_of_ast tactical)
 110           (List.map tactical_of_ast tacticals)
 111     | TacticAst.Tries (loc, tacticals) ->
 112         Tacticals.try_tactics
 113           (List.map (fun t -> "", tactical_of_ast t) tacticals)
 114     | TacticAst.Try (loc, tactical) ->
 115         Tacticals.try_tactic (tactical_of_ast tactical)
 116   in
 117   apply_tactic (tactical_of_ast tac)
 118
 119 let eval_command status cmd =
 120   match cmd with
 121   | TacticAst.Set (loc, name, value) -> set_option status name value
 122   | TacticAst.Qed loc ->
 123       let uri, metasenv, bo, ty =
 124         match status.proof_status with
 125         | Proof (Some uri, metasenv, body, ty) ->
 126             uri, metasenv, body, ty
 127         | Proof (None, metasenv, body, ty) ->
 128             command_error
 129               ("Someone allows to start a thm without giving the "^
 130                "name/uri. This should be fixed!")
 131         | _-> command_error "You can't qed an uncomplete theorem"
 132       in
 133       let suri = UriManager.string_of_uri uri in
 134       if metasenv <> [] then
 135         command_error "Proof not completed! metasenv is not empty!";
 136       let proved_ty,ugraph =
 137         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 138       in
 139       let b,ugraph =
 140         CicReduction.are_convertible [] proved_ty ty ugraph
 141       in
 142       if not b then
 143         command_error
 144           ("The type of your proof is not convertible with the "^
 145           "type you've declared!");
 146       MatitaLog.message (sprintf "%s defined" suri);
 147       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 148       {status with proof_status = No_proof }
 149   | TacticAst.Inductive (loc, dummy_params, types) ->
 150       (* dummy_params are not real params, it is a list of nothing, and the only
 151        * semantic content is the len, that is leftno (note: leftno and pamaters
 152        * have nothing in common).
 153        *)
 154       let suri =
 155         match types with
 156         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 157         | _ -> assert false
 158       in
 159       let uri = UriManager.uri_of_string suri in
 160       let leftno = List.length dummy_params in
 161       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 162       let ugraph =
 163         CicTypeChecker.typecheck_mutual_inductive_defs uri
 164           (types, [], leftno) CicUniv.empty_ugraph
 165       in
 166       let status =
 167         MatitaSync.add_inductive_def
 168           ~uri ~types ~params:[] ~leftno ~ugraph status
 169       in
 170       let extract_alias types uri =
 171         fst(List.fold_left (
 172           fun (acc,i) (name, _, _, cl) ->
 173             ((name, UriManager.string_of_uriref (uri,[i]))
 174             ::
 175             (fst(List.fold_left (
 176               fun (acc,j) (name,_) ->
 177                 (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
 178               ) (acc,1) cl))),i+1
 179         ) ([],0) types)
 180       in
 181       let env_of_list l e =
 182         let module DT = DisambiguateTypes in
 183         let module DTE = DisambiguateTypes.Environment in
 184         List.fold_left (
 185           fun e (name,uri) ->
 186             DTE.add
 187              (DT.Id name)
 188              (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
 189              e
 190         ) e l
 191       in
 192       let aliases = env_of_list (extract_alias types uri) status.aliases in
 193       let status = {status with proof_status = No_proof } in
 194       { status with aliases = aliases}
 195   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 196       let uri =
 197         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 198       in
 199       let goalno = 1 in
 200       let metasenv, body =
 201         match status.proof_status with
 202         | Intermediate metasenv ->
 203             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 204         | _-> assert false
 205       in
 206       let initial_proof = (Some uri, metasenv, body, ty) in
 207       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 208   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 209       let uri =
 210         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 211       in
 212       let metasenv = MatitaMisc.get_proof_metasenv status in
 213       let (body_type, ugraph) =
 214         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 215       in
 216       let (subst, metasenv, ugraph) =
 217         CicUnification.fo_unif metasenv [] body_type ty ugraph
 218       in
 219       if metasenv <> [] then
 220         command_error
 221           "metasenv not empty while giving a definition with body";
 222       let body = CicMetaSubst.apply_subst subst body in
 223       let ty = CicMetaSubst.apply_subst subst ty in
 224       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
 225       {status with proof_status = No_proof}
 226   | TacticAst.Theorem (_, _, None, _, _) ->
 227       command_error "The grammas should avoid having unnamed theorems!"
 228   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 229   | TacticAst.Alias (loc, spec) ->
 230       match spec with
 231       | TacticAst.Ident_alias (id,uri) ->
 232           {status with aliases =
 233             DisambiguateTypes.Environment.add
 234               (DisambiguateTypes.Id id)
 235               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 236               status.aliases }
 237       | TacticAst.Symbol_alias (symb, instance, desc) ->
 238           {status with aliases =
 239             DisambiguateTypes.Environment.add
 240               (DisambiguateTypes.Symbol (symb,instance))
 241               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 242               status.aliases }
 243       | TacticAst.Number_alias (instance,desc) ->
 244           {status with aliases =
 245             DisambiguateTypes.Environment.add
 246               (DisambiguateTypes.Num instance)
 247               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 248
 249 let eval_executable status ex =
 250   match ex with
 251   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 252   | TacticAst.Command (_, cmd) -> eval_command status cmd
 253   | TacticAst.Macro (_, mac) ->
 254       command_error (sprintf "The macro %s can't be in a script"
 255         (TacticAstPp.pp_macro_cic mac))
 256
 257 let eval_comment status c = status
 258
 259 let eval status st =
 260   match st with
 261   | TacticAst.Executable (_,ex) -> eval_executable status ex
 262   | TacticAst.Comment (_,c) -> eval_comment status c
 263
 264 let disambiguate_term status term =
 265   let (aliases, metasenv, cic, _) =
 266     match
 267       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 268         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 269         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 270     with
 271     | [x] -> x
 272     | _ -> assert false
 273   in
 274   let proof_status =
 275     match status.proof_status with
 276     | No_proof -> Intermediate metasenv
 277     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 278         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 279     | Intermediate _ -> Intermediate metasenv
 280     | Proof _ -> assert false
 281   in
 282   let status =
 283     { status with
 284         aliases = aliases;
 285         proof_status = proof_status }
 286   in
 287   status, cic
 288
 289 let disambiguate_terms status terms =
 290   let term = CicAst.pack terms in
 291   let status, term = disambiguate_term status term in
 292   status, CicUtil.unpack term
 293
 294 let disambiguate_tactic status = function
 295   | TacticAst.Transitivity (loc, term) ->
 296       let status, cic = disambiguate_term status term in
 297       status, TacticAst.Transitivity (loc, cic)
 298   | TacticAst.Apply (loc, term) ->
 299       let status, cic = disambiguate_term status term in
 300       status, TacticAst.Apply (loc, cic)
 301   | TacticAst.Absurd (loc, term) ->
 302       let status, cic = disambiguate_term status term in
 303       status, TacticAst.Absurd (loc, cic)
 304   | TacticAst.Exact (loc, term) ->
 305       let status, cic = disambiguate_term status term in
 306       status, TacticAst.Exact (loc, cic)
 307   | TacticAst.Cut (loc, term) ->
 308       let status, cic = disambiguate_term status term in
 309       status, TacticAst.Cut (loc, cic)
 310   | TacticAst.Elim (loc, term, Some term') ->
 311       let status, cic1 = disambiguate_term status term in
 312       let status, cic2 = disambiguate_term status term' in
 313       status, TacticAst.Elim (loc, cic1, Some cic2)
 314   | TacticAst.Elim (loc, term, None) ->
 315       let status, cic = disambiguate_term status term in
 316       status, TacticAst.Elim (loc, cic, None)
 317   | TacticAst.ElimType (loc, term) ->
 318       let status, cic = disambiguate_term status term in
 319       status, TacticAst.ElimType (loc, cic)
 320   | TacticAst.Replace (loc, what, with_what) ->
 321       let status, cic1 = disambiguate_term status what in
 322       let status, cic2 = disambiguate_term status with_what in
 323       status, TacticAst.Replace (loc, cic1, cic2)
 324   | TacticAst.Change (loc, what, with_what, ident) ->
 325       let status, cic1 = disambiguate_term status what in
 326       let status, cic2 = disambiguate_term status with_what in
 327       status, TacticAst.Change (loc, cic1, cic2, ident)
 328 (*
 329   (* TODO Zack a lot more of tactics to be implemented here ... *)
 330   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 331   | TacticAst.Change of 'term * 'term * 'ident option
 332   | TacticAst.Decompose of 'ident * 'ident list
 333   | TacticAst.Discriminate of 'ident
 334   | TacticAst.Fold of reduction_kind * 'term
 335   | TacticAst.Injection of 'ident
 336   | TacticAst.LetIn of 'term * 'ident
 337   | TacticAst.Replace_pattern of 'term pattern * 'term
 338 *)
 339   | TacticAst.Reduce (loc, reduction_kind, opts) ->
 340       let status, opts =
 341         match opts with
 342         | None -> status, None
 343         | Some (l,pat) ->
 344             let status, l =
 345               List.fold_right (fun t (status,acc) ->
 346                 let status',t' = disambiguate_term status t in
 347                 status', t'::acc)
 348               l (status,[])
 349             in
 350             status, Some (l, pat)
 351       in
 352       status, TacticAst.Reduce (loc, reduction_kind, opts)
 353   | TacticAst.Rewrite (loc,dir,t,ident) ->
 354       let status, term = disambiguate_term status t in
 355       status, TacticAst.Rewrite (loc,dir,term,ident)
 356   | TacticAst.Intros (loc, num, names) ->
 357       status, TacticAst.Intros (loc, num, names)
 358   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 359   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 360   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 361   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 362   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 363   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 364   | TacticAst.Left loc -> status, TacticAst.Left loc
 365   | TacticAst.Right loc -> status, TacticAst.Right loc
 366   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 367   | TacticAst.Split loc -> status, TacticAst.Split loc
 368   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 369   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 370   | x ->
 371       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 372       assert false
 373
 374 let rec disambiguate_tactical status = function
 375   | TacticAst.Tactic (loc, tactic) ->
 376       let status, tac = disambiguate_tactic status tactic in
 377       status, TacticAst.Tactic (loc, tac)
 378   | TacticAst.Do (loc, num, tactical) ->
 379       let status, tac = disambiguate_tactical status tactical in
 380       status, TacticAst.Do (loc, num, tac)
 381   | TacticAst.Repeat (loc, tactical) ->
 382       let status, tac = disambiguate_tactical status tactical in
 383       status, TacticAst.Repeat (loc, tac)
 384   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 385       let status, tacticals = disambiguate_tacticals status tacticals in
 386       let tacticals = List.rev tacticals in
 387       status, TacticAst.Seq (loc, tacticals)
 388   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 389       let status, tactical = disambiguate_tactical status tactical in
 390       let status, tacticals = disambiguate_tacticals status tacticals in
 391       status, TacticAst.Then (loc, tactical, tacticals)
 392   | TacticAst.Tries (loc, tacticals) ->
 393       let status, tacticals = disambiguate_tacticals status tacticals in
 394       status, TacticAst.Tries (loc, tacticals)
 395   | TacticAst.Try (loc, tactical) ->
 396       let status, tactical = disambiguate_tactical status tactical in
 397       status, TacticAst.Try (loc, tactical)
 398   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 399       status, tac
 400
 401 and disambiguate_tacticals status tacticals =
 402   let status, tacticals =
 403     List.fold_left
 404       (fun (status, tacticals) tactical ->
 405         let status, tac = disambiguate_tactical status tactical in
 406         status, tac :: tacticals)
 407       (status, [])
 408       tacticals
 409   in
 410   let tacticals = List.rev tacticals in
 411   status, tacticals
 412
 413 let disambiguate_inddef status params indTypes =
 414   let add_pi binders t =
 415     List.fold_right
 416       (fun (name, ast) acc ->
 417         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 418       binders t
 419   in
 420   let ind_binders =
 421     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 422   in
 423   let binders = ind_binders @ params in
 424   let asts = ref [] in
 425   let add_ast ast = asts := ast :: !asts in
 426   let paramsno = List.length params in
 427   let indbindersno = List.length ind_binders in
 428   List.iter
 429     (fun (name, _, typ, constructors) ->
 430       add_ast (add_pi params typ);
 431       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 432     indTypes;
 433   let status, terms = disambiguate_terms status !asts in
 434   let terms = ref (List.rev terms) in
 435   let get_term () =
 436     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 437   in
 438   let uri =
 439     match indTypes with
 440     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 441     | _ -> assert false
 442   in
 443   let mutinds =
 444     let counter = ref 0 in
 445     List.map
 446       (fun _ ->
 447         incr counter;
 448         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 449       indTypes
 450   in
 451   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 452   let cicIndTypes =
 453     List.fold_left
 454       (fun acc (name, inductive, typ, constructors) ->
 455         let cicTyp = get_term () in
 456         let cicConstructors =
 457           List.fold_left
 458             (fun acc (name, _) ->
 459               let typ =
 460                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 461               in
 462               (name, typ) :: acc)
 463             [] constructors
 464         in
 465         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 466       [] indTypes
 467   in
 468   let cicIndTypes = List.rev cicIndTypes in
 469   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 470
 471 let disambiguate_command status = function
 472   | TacticAst.Inductive (loc, params, types) ->
 473       let (status, (uri, (ind_types, vars, paramsno))) =
 474         disambiguate_inddef status params types
 475       in
 476       let rec mk_list = function
 477         | 0 -> []
 478         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 479       in
 480       (* once we've built the cic inductive types we no longer need terms
 481          corresponding to parameters, but we need the leftno, and we encode
 482          it as the length of dummy_params
 483       *)
 484       let dummy_params = mk_list paramsno in
 485       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 486   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 487       let status, ty = disambiguate_term status ty in
 488       let status, body =
 489         match body with
 490         | None -> status, None
 491         | Some body ->
 492             let status, body = disambiguate_term status body in
 493             status, Some body
 494       in
 495       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 496   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 497   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 498       status, cmd
 499   | TacticAst.Alias _ as x -> status, x
 500
 501 let disambiguate_executable status ex =
 502   match ex with
 503   | TacticAst.Tactical (loc, tac) ->
 504       let status, tac = disambiguate_tactical status tac in
 505       status, (TacticAst.Tactical (loc, tac))
 506   | TacticAst.Command (loc, cmd) ->
 507       let status, cmd = disambiguate_command status cmd in
 508       status, (TacticAst.Command (loc, cmd))
 509   | TacticAst.Macro (_, mac) ->
 510       command_error
 511         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 512                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 513
 514 let disambiguate_comment status c =
 515   match c with
 516   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 517   | TacticAst.Code (loc,ex) ->
 518         let status, ex = disambiguate_executable status ex in
 519         status, TacticAst.Code (loc,ex)
 520
 521 let disambiguate_statement status statement =
 522   match statement with
 523   | TacticAst.Comment (loc,c) ->
 524         let status, c = disambiguate_comment status c in
 525         status, TacticAst.Comment (loc,c)
 526   | TacticAst.Executable (loc,ex) ->
 527         let status, ex = disambiguate_executable status ex in
 528         status, TacticAst.Executable (loc,ex)
 529
 530 let eval_ast status ast =
 531   let status,st = disambiguate_statement status ast in
 532   (* this disambiguation step should be deferred to support tacticals *)
 533   eval status st
 534
 535 let eval_from_stream status str cb =
 536   let stl = CicTextualParser2.parse_statements str in
 537   List.fold_left
 538     (fun status ast -> cb status ast;eval_ast status ast) status
 539   stl
 540
 541 let eval_string status str =
 542   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 543
 544 let default_options () =
 545   let options =
 546     StringMap.add "baseuri"
 547       (String
 548         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 549       no_options
 550   in
 551   let options =
 552     StringMap.add "basedir"
 553       (String (Helm_registry.get "matita.basedir" ))
 554       options
 555   in
 556   options
 557
 558 let initial_status =
 559   lazy {
 560     aliases = DisambiguateTypes.empty_environment;
 561     proof_status = No_proof;
 562     options = default_options ();
 563     coercions = [];
 564     objects = [];
 565   }
 566