1. 19 Mar, 2015 1 commit
  2. 03 Mar, 2015 2 commits
  3. 25 Feb, 2015 1 commit
  4. 18 Feb, 2015 1 commit
  5. 17 Feb, 2015 1 commit
  6. 16 Feb, 2015 1 commit
  7. 12 Jan, 2015 2 commits
  8. 12 Dec, 2014 1 commit
  9. 10 Nov, 2014 1 commit
  10. 07 Nov, 2014 1 commit
  11. 25 Oct, 2014 2 commits
  12. 24 Oct, 2014 1 commit
  13. 22 Oct, 2014 3 commits
  14. 17 Oct, 2014 2 commits
  15. 16 Oct, 2014 2 commits
    • Andrei Paskevich's avatar
      Term: revert the two discussion points from the last commit · 8527ea1d
      Andrei Paskevich authored
      - hide the closure variable
      - split t_app_beta into t_func_app_beta, which returns terms,
        and t_pred_app_beta which returns formulas
      
      Also:
      - check for non-recursivity in t_open_lambda
      - implement t_is_lambda via t_open_lambda (less efficient,
        but the correct code without opening would be horrendous)
      - drop t_app_lambda, subsumed by t_[func|pred]_app_beta
      - support nested lambdas in t_[func|pred]_app_beta
      8527ea1d
    • Andrei Paskevich's avatar
      Term: lambda-manipulating functions · 235fac91
      Andrei Paskevich authored
      Two points for discussion:
      
      - t_lambda accepts both terms and formulas for the body.
        Thus, t_open_lambda, t_app_lambda, and t_app_beta can all
        return a term or a formula, depending on what is inside
        the lambda term. The caller should not forget to check.
        We could, in principle, always return a term (bool-typed
        when needed), which would exclude a possible run-time error,
        but then a caller who expects a formula, would have to
        recognize the results of the form [if f then True else False],
        before blindly attaching [== True] to them. Maybe still worth it:
        it's better if a forgotten check leads to an inefficient formula
        than to a type-checking error.
      
      - t_lambda takes a preid which will be the binding variable in the
        produced epsilon. This permits us to give names to our lambdas
        if we want it (what for?) and to give locations to intermediate
        terms inside the epsilon. Overall, it's not very useful and can
        probably be removed.
      235fac91
  16. 22 Sep, 2014 1 commit
  17. 17 Sep, 2014 1 commit
  18. 04 Sep, 2014 2 commits
  19. 02 Sep, 2014 3 commits
  20. 01 Sep, 2014 1 commit
    • Andrei Paskevich's avatar
      fix #17137 · 573870e0
      Andrei Paskevich authored
      Currently, clones "ts -> ty" are represented as "ts -> ts[=ty]",
      where the second type symbol is an alias created on the fly
      for the desired type. The problem comes when we want to clone
      a theory that contains such a cloning declaration. Since these
      aliases are "non-citizens" -- they are not properly declared,
      they are not put in the known_map, and they are not listed as
      locally declared symbols of the theory -- cloning of the cloning
      declaration mistakes them for external symbols and ignores them.
      Thus, the aliased type goes into the cloned theory as is, which
      provokes the error.
      
      The fix consists in an additional test for non-local type symbols.
      If such a symbol is an alias for a type that is actually cloneable,
      we conclude that the symbol is not external, but is a mere proxy
      for the aliased type, and so we clone the type and create a fresh
      type alias for it.
      
      A proper fix would be to always clone type symbols into types and
      never introduce the proxy type aliases. This is a more intrusive
      change, however, so let's start with a bandage.
      573870e0
  21. 20 Aug, 2014 4 commits
  22. 19 Aug, 2014 1 commit
  23. 08 Aug, 2014 1 commit
  24. 15 Apr, 2014 1 commit
  25. 04 Apr, 2014 1 commit
  26. 29 Mar, 2014 1 commit
  27. 19 Mar, 2014 1 commit