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