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