1. 04 Jun, 2017 3 commits
    • Andrei Paskevich's avatar
      syntax: use "pure { term }" instead of "{| term |}" · e63151cf
      Andrei Paskevich authored
      Aesthetics is a harsh mistress.
    • Andrei Paskevich's avatar
      Mlw: overloaded symbols · 1aa6a8b1
      Andrei Paskevich authored
      This is a prototype version that requires no additional annotation.
      In addition to the existing rules of scoping:
        - it is forbidden to declare two symbols with the same name
          in the same scope ("everything can be unambiguously named"),
        - it is allowed to shadow an earlier declaration with a newer one,
          if they belong to different scopes (e.g., via import),
      we define one new rule:
        - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
          but (1) both of them are either
            - binary relations: t -> t -> bool,
            - binary operators: t -> t -> t, or
            - unary operators:  t -> t
          and (2) their argument types are not the same,
          then rs_old remains visible in the current scope.
          Both symbols should take non-ghost arguments and
          return non-ghost results, but effects are allowed.
          The name itself is not taken into account, hence
          it is possible to overload "div", "mod", or "fact".
      Clause (1) allows us to perform type inference for a family of rsymbols,
      using an appropriate generalized signature.
      Clause (2) removes guaranteed ambiguities: we treat this case as
      the user's intention to redefine the symbol for a given type.
      Type inference failures are still possible: either due to
      polymorphism (['a -> 'a] combines with [int -> int] and
      will fail with the "ambiguous notation" error), or due
      to inability to infer the precise types of arguments.
      Explicit type annotations and/or use of qualified names
      for disambiguation should always allow to bypass the errors.
      Binary operations on Booleans are treated as relations, not as
      operators. Thus, (+) on bool will not combine with (+) on int.
      This overloading only concerns programs: in logic, the added rule
      does not apply, and the old symbols get shadowed by the new ones.
      In this setting, modules never export families of overloaded symbols:
      it is impossible to "use import" a single module, and have access to
      several rsymbols for (=) or (+).
      The new "overloading" rule prefers to silently discard the previous
      binding when it cannot be combined with the new one. This allows us
      to be mostly backward compatible with existing programs (except for
      the cases where type inference fails, as discussed above).
      This rule should be enough to have several equalities for different
      program types or overloaded arithmetic operations for bounded integers.
      These rsymbols should not be defined as let-functions: in fact, it is
      forbidden now to redefine equality in logic, and the bounded integers
      should be all coerced into mathematical integers anyway.
      I would like to be able to overload mixfix operators too, but
      there is no reasonable generalized signature for them: compare
      "([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
      with "([]) : monomap -> key -> elt". If we restrict the overloading
      to symbols with specific names, we might go with "'a -> 'b -> 'c" for
      type inference (and even "'a -> 'b" for some prefix operators, such
      as "!" or "?"). To discuss.
    • Andrei Paskevich's avatar
      minor · 025d36c7
      Andrei Paskevich authored
  2. 03 Jun, 2017 2 commits
  3. 02 Jun, 2017 5 commits
  4. 01 Jun, 2017 5 commits
  5. 31 May, 2017 14 commits
  6. 30 May, 2017 1 commit
  7. 29 May, 2017 2 commits
  8. 27 May, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: support Epure in the surface language (with type inference) · 72714897
      Andrei Paskevich authored
      The current syntax is "{| <term> |}", which is shorter than
      "pure { <term> }", and does not require a keyword. Better
      alternatives are welcome.
      As for type inference, we infer the type pf the term under Epure
      without binding destructible type variables in the program.
      In particular,
        let ghost fn x = {| x + 1 |}
      will not typecheck. Indeed, even if we detect that the result
      is [int], the type of the formal parameter [x[ is not inferred
      in the process, and thus stays at ['xi].
      Another problem is related to the fact that variable and function
      namespaces are not yet separated when we perform type inference.
      Thus both fuctions
        let ghost fn (x: int) = let x a = a in {| x + 5 |}
        let ghost fn (x: int) = let x a = a in {| x 5 |}
      will not typecheck, since the type of [x] is ['a -> 'a] when
      we infer the type for the Epure term, but it becomes [int],
      when we construct the final program expression. Probably,
      the only reasonable solution is to keep variables and
      functions in the same namespace, so that [x] simply can
      not be used in annotations after being redefined as a
      program function.
  9. 25 May, 2017 3 commits
  10. 24 May, 2017 4 commits
    • MARCHE Claude's avatar
      update obsolete sessions · 30fd6bb4
      MARCHE Claude authored
    • Guillaume Melquiond's avatar
      Update some Coq realizations. · 721c0867
      Guillaume Melquiond authored
    • Andrei Paskevich's avatar
      Split_goal: make introduce_premises less aggressige · 8b809621
      Andrei Paskevich authored
      Prevent introduce_premises from splitting too aggressively
      on the left-hand side:
      - under quantifiers:
          "forall x. P /\ Q" =/=> "(forall x. P) /\ (forall x. Q)"
      - match-with:
          "match t with A -> P | B -> Q" =/=> "(t = A -> P) /\ (t = B -> Q)"
      - if-then-else:
          "if f then P else Q" =/=> "(f -> P) /\ (not f -> Q)"
      - equivalence:
          "P <-> Q" =/=> "(P -> Q) /\ (Q -> P)"
      Those splits duplicate formulas, hinder readability and do not
      really simplify anything. Moreover, in case of a split under
      a quantifier, they create several universal premises for provers
      to instantiate, instead of just one.
      TODO: introduce_premises should be able to split under
      a single-branch match. However, this requires special
      treatment in Introduce.dequant, since the pattern
      should be rather skolemized than used as a condition.
    • Guillaume Melquiond's avatar
      Update some Coq realizations. · 501bde2a
      Guillaume Melquiond authored