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