)]}'
{
  "commit": "16598391a07d4a4c55c3229a3511cbf0ad9232e9",
  "tree": "596c09552c6063cd697349d323965d7cb6f00c7e",
  "parents": [
    "9d35d3152903a39278a24d9039aee0d13f87b7d0"
  ],
  "author": {
    "name": "Leonardo de Moura",
    "email": "leonardo@microsoft.com",
    "time": "Tue Jun 26 15:13:25 2018 -0700"
  },
  "committer": {
    "name": "Leonardo de Moura",
    "email": "leonardo@microsoft.com",
    "time": "Wed Aug 01 15:05:31 2018 -0700"
  },
  "message": "refactor(kernel): declaration vs constant_info\n\n@Kha This is the change I wanted to talk with you.\nThis is a work-in-progress commit.\nDoes it sound reasonable to you?\n\nIn Lean3, we use the `declaration` objects to represent new declarations\nthat are sent to the kernel, and to store information for all constants\ndeclared in an environment.\nThis design decision was done when we did not have support for\nmutual (meta) declarations, and information about inductive datatypes,\nconstructors and recursors were stored in an environment extension.\nThis design now seems weird since we have four different methods for\nadding declarations into the environment:\n```\n    environment add(certified_declaration const \u0026 d) const;\n    environment add_meta(buffer\u003cdeclaration\u003e const \u0026 ds, bool check \u003d true) const;\n    environment add(inductive_decl const \u0026 decl) const;\n    environment add_quot() const;\n```\nMoreover, we use `mk_constant_assumption` to represent inductive\ndatatype, constructors, recursors, and `quot` primitives.\nSince inductive datatypes, constructors, recursors and `quot` primitives\nare not considered axioms, we have the method:\n```\n    bool environment::is_builtin(name const \u0026 n) const;\n```\n\nWe can avoid these hacks by having a type for representing\ndeclarations (i.e., objects that are sent to the kernel) and\nobjects for storing information of the constant declarations stored\nin an environment object.\n\nA `declaration` object is now of the form\n```\ninductive declaration\n| assump_decl      (val : assumption_val)\n| defn_decl        (val : definition_val)\n| axiom_decl       (val : axiom_val)\n| thm_decl         (val : theorem_val)\n| quot_decl\n| mutual_defn_decl (defns : list definition_val) -- All definitions must be marked as `meta`\n| induct_decl      (lparams : list name) (nparams : nat) (types : list inductive_type) (is_meta : bool)\n\n/-\nIf we want, we can let users specify their own names for `quot`,\n`quot.mk`, `quot.lift` and `quot.ind`. We just need to add them\nas fields of `declaration.quot_decl`.\n-/\n```\n\nWhen we check a declaration, one or more `constant_info` objects are\ncreated for each new constant in the declaration.\n```\ninductive constant_info\n| assump_info   (val : assumption_val)\n| defn_info     (val : definition_val)\n| axiom_info    (val : axiom_val)\n| thm_info      (val : theorem_val)\n| quot_info     (val : quot_val)\n| induct_info   (val : inductive_val)\n| cnstr_info    (val : constructor_val)\n| rec_info      (val : recursor_val)\n```\nFor simple declarations `constant` (aka `assumption`), `definition`,\n`theorem` and `axiom`, the information stored in the `constant_info` is\nidentical to the information in the `declaration` object. This is\nexpected since these are the original Lean3 declarations.\n\nThe `environment` object stores a mapping from `name` to\n`constant_info`. The function `check` validates a declaration\nand produces a `certified_declaration`. A `certified_declaration` is\na pair `(declaration, list constant_info)`. The `list` here makes it\nexplicit that a declaration may add one or more new constants into the\nenvironment. Finally, the `environment` object has a single `add`\nmethod and a single `get` and `find`:\n```\n    environment add(certified_declaration const \u0026 d) const;\n\n    /** \\brief Return info for the constant with name \\c n (if it is defined in this environment). */\n    optional\u003cconstant_info\u003e find(name const \u0026 n) const;\n\n    /** \\brief Return info for the constant with name \\c n. Throws an\n        exception if has not been declared in this environment. */\n    constant_info get(name const \u0026 n) const;\n```\n\nMoreover, the method `environment::builtin` is not necessary anymore.\nIf `environment::get(n)` returns an `axiom_info` or an `assump_info`, then\nwe know for sure the constant named `n` has been postulated.\n\nThis commit only defined the new types in Lean. I still need to make\nthe changes to the C++ code base.\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "1af2053cf424300151b1454afd872ac1ab593542",
      "old_mode": 33188,
      "old_path": "library/init/lean/declaration.lean",
      "new_id": "6e13a1499e7df4db87f54a4bfbffe81f9d2ae21b",
      "new_mode": 33188,
      "new_path": "library/init/lean/declaration.lean"
    },
    {
      "type": "modify",
      "old_id": "07ac0a3545b197c7e2b172a194f8c7246ce1c0e9",
      "old_mode": 33188,
      "old_path": "library/init/meta/declaration.lean",
      "new_id": "1a226b4775a6437e8b1300f4709343532d6f273e",
      "new_mode": 33188,
      "new_path": "library/init/meta/declaration.lean"
    },
    {
      "type": "modify",
      "old_id": "8a80a924cd3b7d82782fcad4dd3d9db5d63c2bf6",
      "old_mode": 33188,
      "old_path": "library/init/meta/environment.lean",
      "new_id": "d217edbb16d7e4066994a434b3349b256dd4e854",
      "new_mode": 33188,
      "new_path": "library/init/meta/environment.lean"
    }
  ]
}