Code

Coq lang#38

Code

Open

lucaspena wants to merge 44 commits intomasterkframework/matching-logic-prover:masterfrom coq-langkframework/matching-logic-prover:coq-langCopy head branch name to clipboard

+1,195-5

Commits

Commits on Feb 11, 2020

• begin support for coq in ML

  lucaspena

  committed
  cb093c7

  Copy full SHA for cb093c7

• more support for coq in ML. inductive defs parse

  lucaspena

  committed
  a721d74

  Copy full SHA for a721d74

• coq: Fix parsing of underscores

  

  nishantjr

  authored and

  lucaspena

  committed
  7bb9ed5

  Copy full SHA for 7bb9ed5

• add more parsing rules and Logic examples

  

  xc3

  authored and

  lucaspena

  committed
  1a294cc

  Copy full SHA for 1a294cc

• minor

  

  xc3

  authored and

  lucaspena

  committed
  e9245c3

  Copy full SHA for e9245c3

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

  lucaspena

  committed
  13c1df5

  Copy full SHA for 13c1df5

• coq-lang: format sentences (newline)

  lucaspena

  committed
  7155865

  Copy full SHA for 7155865

• t/Logic.v: added eq inductive type

  lucaspena

  committed
  2413968

  Copy full SHA for 2413968

• coq-driver: begin translating inductive defs to ml

  lucaspena

  committed
  2d5da27

  Copy full SHA for 2d5da27

• coq-driver: begin translating Definitions

  lucaspena

  committed
  40317e2

  Copy full SHA for 40317e2

• coq-driver: translating some definitions/terms

  lucaspena

  committed
  2dd0fac

  Copy full SHA for 2dd0fac

• coq-driver: more translating coq term to pattern. AndComm mostly translated

  lucaspena

  committed
  8e88b50

  Copy full SHA for 8e88b50

• add mu, translating fix

  lucaspena

  committed
  93bb94e

  Copy full SHA for 93bb94e

• coq-driver: translate binders from match clauses

  lucaspena

  committed
  ba95017

  Copy full SHA for ba95017

• translating ind defs

  lucaspena

  committed
  54749f9

  Copy full SHA for 54749f9

• parsing Logic.v

  lucaspena

  committed
  12b53bc

  Copy full SHA for 12b53bc

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

  lucaspena

  committed
  0c60745

  Copy full SHA for 0c60745

• cleanup

  lucaspena

  committed
  46b712b

  Copy full SHA for 46b712b

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

  lucaspena

  committed
  b802ed3

  Copy full SHA for b802ed3

• coq tests in own directory

  lucaspena

  committed
  8585a5d

  Copy full SHA for 8585a5d

• use named axioms

  lucaspena

  committed
  74f3c0b

  Copy full SHA for 74f3c0b

• set variables no longer sorted

  lucaspena

  committed
  968a224

  Copy full SHA for 968a224

Commits on Feb 12, 2020

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

  lucaspena

  committed
  5c2e2ce

  Copy full SHA for 5c2e2ce

Commits on Feb 14, 2020

• change format for terms having type in v files

  lucaspena

  committed
  b2bd250

  Copy full SHA for b2bd250

Commits on Feb 17, 2020

• coq-driver: translate forall to pi

  lucaspena

  committed
  3090652

  Copy full SHA for 3090652

• change type-check to typecheck

  lucaspena

  committed
  61881a2

  Copy full SHA for 61881a2

• placeholder for typecheck strategy

  lucaspena

  committed
  85e8229

  Copy full SHA for 85e8229

Commits on Feb 24, 2020

• encode output type in coq syntax rather than comment

  lucaspena

  committed
  33e7f10

  Copy full SHA for 33e7f10

• begin typecheck strategy

  lucaspena

  committed
  2eb94c1

  Copy full SHA for 2eb94c1

Commits on Feb 27, 2020

• typecheck works for simple examples

  lucaspena

  committed
  974aac4

  Copy full SHA for 974aac4

Commits on Mar 5, 2020

• typecheck: minor change

  lucaspena

  committed
  182db6b

  Copy full SHA for 182db6b

Commits on Mar 10, 2020

• add coq rules

  

  Xiaohong Chen

  committed
  5b13db3

  Copy full SHA for 5b13db3

Commits on Mar 11, 2020

• global environments, begin well-typing defs

  lucaspena

  committed
  724644b

  Copy full SHA for 724644b

Commits on Mar 26, 2020

• add basic Coq typing rules

  

  Xiaohong Chen

  committed
  7011393

  Copy full SHA for 7011393

• add authors

  

  Xiaohong Chen

  committed
  477dde5

  Copy full SHA for 477dde5

• wording of comment in W-Local-Assum

  lucaspena

  committed
  895d236

  Copy full SHA for 895d236

Commits on Mar 30, 2020

• parsing more terms in coq translation

  lucaspena

  committed
  1de1820

  Copy full SHA for 1de1820

Commits on Apr 13, 2020

• coq-lang, coq-driver: handling more constructs for generated verbose defs

  lucaspena

  committed
  07675a4

  Copy full SHA for 07675a4

Commits on Apr 19, 2020

• more parsing

  lucaspena

  committed
  3deae83

  Copy full SHA for 3deae83

Commits on Apr 21, 2020

• coq rules: conversion rules

  lucaspena

  committed
  10c7863

  Copy full SHA for 10c7863

Commits on Apr 24, 2020

• coq_rules: more on conversion rules

  lucaspena

  committed
  74f3359

  Copy full SHA for 74f3359

Commits on May 20, 2020

• coq_rules: subtyping rules

  lucaspena

  committed
  7331f17

  Copy full SHA for 7331f17

Commits on May 22, 2020

• coq_rules: Inductive Definitions

  lucaspena

  committed
  e93c40e

  Copy full SHA for e93c40e

Commits on Jun 3, 2020

• coq_rules: correctness rules

  lucaspena

  committed
  bff2495

  Copy full SHA for bff2495