helm/matita/matitaEngine.ml

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