1. 06 Mar, 2013 1 commit
  2. 04 Mar, 2013 1 commit
    • Andrei Paskevich's avatar
      whyml: match expression is ghost if we look inside ghost fields · 43b684d0
      Andrei Paskevich authored
      We store in every lsymbol a new integer field ls_constr,
      equal to zero if the lsymbol is not a constructor, and equal
      to the number of constructors of the lsymbol's type otherwise.
      It is allowed to declare or define an lsymbol with ls_constr > 0
      as an ordinary function (otherwise algebraic type elimination
      wouldn't work - though we might still check this in theories),
      but it is forbidden to use a wrong ls_constr in algebraic type
      The ghostness of a match expression is now determined as follows:
      If at least one branch expression is ghost,
        then the match is ghost;
      else if there is only one branch,
        then the match is not ghost;
      else if the matched expression is ghost,
        then the match is ghost;
      else if at least one pattern matches a ghost field
              against a constructor with ls_constr > 1
        then the match is ghost;
        the match is not ghost.
      We do just enough to recognize obvious non-ghost cases, and
      make no attempt to handle redundant matches or to detect
      exhaustive or-patterns in subpatterns.
  3. 03 Mar, 2013 1 commit
    • Andrei Paskevich's avatar
      track dangerous applications of equality · bb6734a1
      Andrei Paskevich authored
      In programs, but also in pure theories, it is not safe to compare
      arbitrary types. For example, if we have a record with ghost fields,
      a comparison may produce different results before and after ghost
      code elimination. Even for pure types like 'map' or 'set', it is
      unlikely that the result of logical equality will be the same as
      the result of OCaml structural equality on the implemented type.
      This commit makes the first step towards fixing this issue.
      We proceed in the following way:
      1. Every lsymbol (pure function or predicate symbol) carries
         a subset of type variables of its signature, called "opaque
         type variables". By marking a type variable 'a opaque in an
         lsymbol's signature, the user guarantees that this lsymbol
         can be implemented without ever comparing values of type 'a.
         In other words, this is a promise not to break into a type
         The corresponding syntax is: "predicate safe (x y : ~'a)".
         All type variables in undefined symbols are non-opaque,
         unless annotated otherwise. Non-opaque is the default
         to keep the change conservative.
         Opacity of type variables in defined symbols is inferred
         from the definition. If the definition violates a given
         opacity annotation, an exception is raised. Notice that
         we only check definitions in _theory_ declarations. One
         can define an lsymbol in a _task_ in a way that violates
         opacity. We cannot forbid it, because various elimination
         transformations would replace safe operations (such as
         matching) with equalities. This is not a problem, since in
         the pure logical realm of provers opacity is not required
         One exception would be Coq, whose transformation chain must
         never perform such operations.
         All type variables in inductive predicates are non-opaque.
         Indeed, we can redefine equality via an inductive predicate.
         [TODO: find safe forms of inductive definitions and implement
         more reasonable restrictions.]
         All type variables in constructors and field symbols are opaque.
         It is forbidden to instantiate an opacity-preserving symbol
         with an opacity-breaking one in a clone substitution.
      2. Similar type variable tracking is implemented for program symbols.
         Type variables in the signature of a "val" are non-opaque unless
         annotated otherwise. Opacity of type variables in defined symbols
         is inferred from the definition, and an exception is raised, if
         a given annotation is violated.
         The internal mechanism of tracking is different: the "eff_compar"
         field in effects contains the type variables that occur under
         equality or any other opacity-breaking operation. In this respect,
         our API is inconsistent between lsymbols and psymbols: the former
         asks for the opaque tvsymbols, the latter requires us to fill the
         spec with "comparison effects" for the non-opaque ones. [TODO:
         add the "~opaque" argument to create_psymbol and make the WhyML
         core fill the effect under the hood.]
         Every time an lsymbol or a psymbol is applied in a program,
         we check the substitution into its signature's type variables.
         If a non-opaque type variable is instantiated with a program type,
         an exception is raised. [TODO: be more precise and reject only
         types with ghost and model components - being mutable, private,
         or carrying an invariant doesn't conflict with equality.]
         Notice that we do not allow to compare program types even in
         the ghost code. This is not needed if we only consider the
         problems of the code extraction, but _might_ be necessary,
         if we also want to protect Coq realisations (see below).
      This commit fixes the immediate problem of breaking the ghost
      guarantees when equality or some other opacity-breaking lsymbol
      is applied in a program to a type with ghost or "model" parts.
      This leaves the problem of code extraction for programs that
      compare complex types such as maps or sets (Coq driver is
      affected by this, too, I guess). The next step is to provide
      annotations for problematic type constructors. A declaration
      "type ~map 'a 'b" would mean "logical equality on this type
      is likely to be different from the structural equality on any
      implementation of this type - therefore do not apply equality
      to it: neither in programs (because this can't be implemented),
      nor in pure functions (because they are extracted, too, and
      because this can't be realized with Leibniz equality in Coq)."
      [TODO: discuss and implement.]
      [TODO: mb choose better term for "opaque" and notation for ~'a.]
  4. 17 Feb, 2013 1 commit
  5. 05 Feb, 2013 2 commits
  6. 21 Jan, 2013 1 commit
  7. 06 Jan, 2013 1 commit
    • Andrei Paskevich's avatar
      put built-in theories and modules under the library path "why3" · 3df85aba
      Andrei Paskevich authored
      In this way, we can always distinguish them from local theories and
      modules. Both 'use Bool' and 'use why3.Bool' are accepted. No support
      for use/clone of built-in modules is done yet, but so far we don't
      needed (the only built-in module is why3.Prelude which is used by
      As of now, one cannot put a file "why3.why" at the root of loadpath,
      since it will be inaccessible. Paths like why3/toto.why are still
      admitted, but we will probably ban them too and reserve the whole
      "why3.xxx.yyy" hierarchy for the built-in theories and modules.
  8. 19 Dec, 2012 1 commit
  9. 08 Nov, 2012 1 commit
  10. 06 Nov, 2012 1 commit
  11. 05 Nov, 2012 1 commit
  12. 04 Nov, 2012 2 commits
  13. 29 Oct, 2012 2 commits
  14. 27 Oct, 2012 1 commit
  15. 26 Oct, 2012 1 commit
  16. 23 Oct, 2012 1 commit
  17. 21 Oct, 2012 5 commits
  18. 20 Oct, 2012 1 commit
    • Andrei Paskevich's avatar
      simplify copyright headers · 11598d2b
      Andrei Paskevich authored
      + create AUTHORS file
      + fix the linking exception in LICENSE
      + update the "About" in IDE
      + remove the trailing whitespace
      + inflate my scores at Ohloh
  19. 09 Oct, 2012 1 commit
  20. 17 Sep, 2012 1 commit
  21. 11 Sep, 2012 1 commit
  22. 04 Sep, 2012 1 commit
  23. 01 Sep, 2012 1 commit
  24. 30 Aug, 2012 1 commit
  25. 27 Aug, 2012 2 commits
  26. 20 Aug, 2012 2 commits
    • François Bobot's avatar
      session: metas can be added · 3e20cfe5
      François Bobot authored
        - the symbols that appear in the metas are identified in the xml by
          their position in the task:
          - in which declaration
          - in which definition (if that apply otherwise -1)
          - in which constructor(or case in inductive predicate) (if that apply otherwise -1)
          - in which field (if that apply otherwise -1)
        - the md5sum of the prefix of the task that end with the declaration is used to know if the
          symbol have been changed, and if it is obsolete.
        - currently metas that contains obsolete symbol are removed.
    • François Bobot's avatar
      stdlib: remove polymorphic hashtbl · 068ddc7b
      François Bobot authored
         - add functions to Hashtbl.S
         - without ocaml 3.12 its not possible to do that for Hashtbl without
           copying the signature
         - "open Stdlib" hides the polymorphic hashtbl, perhaps a good idea
           since that avoid errors.
  27. 16 Aug, 2012 1 commit
  28. 05 Aug, 2012 3 commits
  29. 04 Aug, 2012 1 commit
    • Andrei Paskevich's avatar
      make the meta_desc field immutable · 5ae69cd3
      Andrei Paskevich authored
      Provers will have native polymorphism support long before people will
      start writing third-party polymorphism encoding procedures for Why3.
      (And it's not that I have high hopes about the former.)