Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Coq lang #38

Open
wants to merge 44 commits into
base: master
Choose a base branch
from
Open

Coq lang #38

wants to merge 44 commits into from

Commits on Feb 11, 2020

  1. begin support for coq in ML

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    cb093c7 View commit details
    Browse the repository at this point in the history

  2. more support for coq in ML. inductive defs parse

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    a721d74 View commit details
    Browse the repository at this point in the history

  3. coq: Fix parsing of underscores

    @nishantjr @lucaspena
    nishantjr authored and lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    7bb9ed5 View commit details
    Browse the repository at this point in the history

  4. add more parsing rules and Logic examples

    @lucaspena
    xc3 authored and lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    1a294cc View commit details
    Browse the repository at this point in the history

  5. minor

    @lucaspena
    xc3 authored and lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    e9245c3 View commit details
    Browse the repository at this point in the history

  6. coq-lang: parsing more logic, can parse exists and AndComm

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    13c1df5 View commit details
    Browse the repository at this point in the history

  7. coq-lang: format sentences (newline)

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    7155865 View commit details
    Browse the repository at this point in the history

  8. t/Logic.v: added eq inductive type

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    2413968 View commit details
    Browse the repository at this point in the history

  9. coq-driver: begin translating inductive defs to ml

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    2d5da27 View commit details
    Browse the repository at this point in the history

  10. coq-driver: begin translating Definitions

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    40317e2 View commit details
    Browse the repository at this point in the history

  11. coq-driver: translating some definitions/terms

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    2dd0fac View commit details
    Browse the repository at this point in the history

  12. coq-driver: more translating coq term to pattern. AndComm mostly tran… 

    …slated
    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    8e88b50 View commit details
    Browse the repository at this point in the history

  13. add mu, translating fix

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    93bb94e View commit details
    Browse the repository at this point in the history

  14. coq-driver: translate binders from match clauses

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    ba95017 View commit details
    Browse the repository at this point in the history

  15. translating ind defs

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    54749f9 View commit details
    Browse the repository at this point in the history

  16. parsing Logic.v

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    12b53bc View commit details
    Browse the repository at this point in the history

  17. kore-lang: for aml: application is Pattern(Patterns)

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    0c60745 View commit details
    Browse the repository at this point in the history

  18. cleanup

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    46b712b View commit details
    Browse the repository at this point in the history

  19. remove coq tests besides Logic and nat_ind, add expeted output for those

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    b802ed3 View commit details
    Browse the repository at this point in the history

  20. coq tests in own directory

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    8585a5d View commit details
    Browse the repository at this point in the history

  21. use named axioms

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    74f3c0b View commit details
    Browse the repository at this point in the history

  22. set variables no longer sorted

    @lucaspena
    lucaspena committed Feb 11, 2020
    Configuration menu
    Copy the full SHA
    968a224 View commit details
    Browse the repository at this point in the history

Commits on Feb 12, 2020

  1. create goals for typing coq defs. add result type to definitions

    @lucaspena
    lucaspena committed Feb 12, 2020
    Configuration menu
    Copy the full SHA
    5c2e2ce View commit details
    Browse the repository at this point in the history

Commits on Feb 14, 2020

  1. change format for terms having type in v files

    @lucaspena
    lucaspena committed Feb 14, 2020
    Configuration menu
    Copy the full SHA
    b2bd250 View commit details
    Browse the repository at this point in the history

Commits on Feb 17, 2020

  1. coq-driver: translate forall to pi

    @lucaspena
    lucaspena committed Feb 17, 2020
    Configuration menu
    Copy the full SHA
    3090652 View commit details
    Browse the repository at this point in the history

  2. change type-check to typecheck

    @lucaspena
    lucaspena committed Feb 17, 2020
    Configuration menu
    Copy the full SHA
    61881a2 View commit details
    Browse the repository at this point in the history

  3. placeholder for typecheck strategy

    @lucaspena
    lucaspena committed Feb 17, 2020
    Configuration menu
    Copy the full SHA
    85e8229 View commit details
    Browse the repository at this point in the history

Commits on Feb 24, 2020

  1. encode output type in coq syntax rather than comment

    @lucaspena
    lucaspena committed Feb 24, 2020
    Configuration menu
    Copy the full SHA
    33e7f10 View commit details
    Browse the repository at this point in the history

  2. begin typecheck strategy

    @lucaspena
    lucaspena committed Feb 24, 2020
    Configuration menu
    Copy the full SHA
    2eb94c1 View commit details
    Browse the repository at this point in the history

Commits on Feb 27, 2020

  1. typecheck works for simple examples

    @lucaspena
    lucaspena committed Feb 27, 2020
    Configuration menu
    Copy the full SHA
    974aac4 View commit details
    Browse the repository at this point in the history

Commits on Mar 5, 2020

  1. typecheck: minor change

    @lucaspena
    lucaspena committed Mar 5, 2020
    Configuration menu
    Copy the full SHA
    182db6b View commit details
    Browse the repository at this point in the history

Commits on Mar 10, 2020

  1. add coq rules

    Xiaohong Chen committed Mar 10, 2020
    Configuration menu
    Copy the full SHA
    5b13db3 View commit details
    Browse the repository at this point in the history

Commits on Mar 11, 2020

  1. global environments, begin well-typing defs

    @lucaspena
    lucaspena committed Mar 11, 2020
    Configuration menu
    Copy the full SHA
    724644b View commit details
    Browse the repository at this point in the history

Commits on Mar 26, 2020

  1. add basic Coq typing rules

    Xiaohong Chen committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    7011393 View commit details
    Browse the repository at this point in the history

  2. add authors

    Xiaohong Chen committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    477dde5 View commit details
    Browse the repository at this point in the history

  3. wording of comment in W-Local-Assum

    @lucaspena
    lucaspena committed Mar 26, 2020
    Configuration menu
    Copy the full SHA
    895d236 View commit details
    Browse the repository at this point in the history

Commits on Mar 30, 2020

  1. parsing more terms in coq translation

    @lucaspena
    lucaspena committed Mar 30, 2020
    Configuration menu
    Copy the full SHA
    1de1820 View commit details
    Browse the repository at this point in the history

Commits on Apr 13, 2020

  1. coq-lang, coq-driver: handling more constructs for generated verbose … 

    …defs
    @lucaspena
    lucaspena committed Apr 13, 2020
    Configuration menu
    Copy the full SHA
    07675a4 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2020

  1. more parsing

    @lucaspena
    lucaspena committed Apr 19, 2020
    Configuration menu
    Copy the full SHA
    3deae83 View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2020

  1. coq rules: conversion rules

    @lucaspena
    lucaspena committed Apr 21, 2020
    Configuration menu
    Copy the full SHA
    10c7863 View commit details
    Browse the repository at this point in the history

Commits on Apr 24, 2020

  1. coq_rules: more on conversion rules

    @lucaspena
    lucaspena committed Apr 24, 2020
    Configuration menu
    Copy the full SHA
    74f3359 View commit details
    Browse the repository at this point in the history

Commits on May 20, 2020

  1. coq_rules: subtyping rules

    @lucaspena
    lucaspena committed May 20, 2020
    Configuration menu
    Copy the full SHA
    7331f17 View commit details
    Browse the repository at this point in the history

Commits on May 22, 2020

  1. coq_rules: Inductive Definitions

    @lucaspena
    lucaspena committed May 22, 2020
    Configuration menu
    Copy the full SHA
    e93c40e View commit details
    Browse the repository at this point in the history

Commits on Jun 3, 2020

  1. coq_rules: correctness rules

    @lucaspena
    lucaspena committed Jun 3, 2020
    Configuration menu
    Copy the full SHA
    bff2495 View commit details
    Browse the repository at this point in the history