aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/context.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* A missing newline after a comment.Gravatar Hugo Herbelin2017-10-24
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | This allows the decoupling of the notions of context containing kernel terms and context containing tactic-level terms.
* CLEANUP: adding "Context.Compacted.Declaration.of_named_decl" function, ↵Gravatar Matej Kosik2016-08-26
| | | | which can be useful in general, and then simplifying "Printer.pr_named_decl" function
* CLEANUP: rename "Context.Named.{to,of}_rel" functions to ↵Gravatar Matej Kosik2016-08-26
| | | | "Context.Named.{to,of}_rel_decl"
* CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
|
* CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
|
* CLEANUP: Type alias "Context.section_context" was removedGravatar Matej Kosik2016-08-25
|
* CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to ↵Gravatar Matej Kosik2016-08-25
| | | | "Context.{Rel,Named}.fold_constr"
* Merging a branch that adds "Context.Named.Declaration.to_rel" function.Gravatar Matej Kosik2016-08-24
|\
| * Adding "Context.Named.Declaration.to_rel" functionGravatar Matej Kosik2016-08-24
| |
* | Revert "CLEANUP: removing the definition of the ↵Gravatar Pierre-Marie Pédrot2016-08-17
|/ | | | | | | | | | | "Context.Rel.Declaration.to_tuple" function" This reverts commit 4b24bb7d3b770592015c264001b9aed9fe95c200. While the of_tuple function is clearly dubious and mostly used for compatiblity reasons, and thus had to be removed, I think that the to_tuple function is still useful as it allows to access each component of the declaration piecewise. Without it, some codes tend to get cluttered with useless projections here and there.
* Adding "Context.Named.Declaraton.of_rel" functionGravatar Matej Kosik2016-08-11
|
* CLEANUP: removing the definition of the "Context.Rel.Declaration.of_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | function
* CLEANUP: removing the definition of the "Context.Rel.Declaration.to_tuple" ↵Gravatar Matej Kosik2016-08-11
| | | | function
* REFORMATTING: kernel/context.ml{,i}Gravatar Matej Kosik2016-02-09
|
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
|/ | | | | | | | It will later be used to fix a bug and improve some code. Interestingly, there were a redundant semantic equivalent to extended_rel_list in the kernel called local_rels, and another private copy of extended_rel_list in exactly the same file.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Remove an ununsed pattern and commented code in the kernel.Gravatar Matthieu Sozeau2014-10-24
| | | | | Reestablish completeness in conversion when Opaque primitive projections are used.
* Pushing Pierre's factorization of names in goal context printing fromGravatar Hugo Herbelin2014-10-22
| | | | | | coqide to coqtop. (Joint work with Pierre)
* A patch for printing "match" when constructors are defined with let-inGravatar Hugo Herbelin2014-10-20
| | | | | | | | | | | but the internal representation dropped let-in. Ideally, the internal representation of the "match" should use contexts for the predicate and the branches. This would however be a rather significant change. In the meantime, just a hack. To do, there is still an extra @ in the constructor name that does not need to be there.
* Coqide prints succesive hyps of the same type on 1 lineGravatar Pierre Boutillier2014-09-01
| | | | | This revert somehow f5d7b2b1eda550f5bf0965286d449112acbbadde about "Hypotheses don't respect Barendregt convention".
* Removing some generic equalities.Gravatar ppedrot2013-10-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7