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