CameLIGO extraction (#71)

* Add extraction to cameLIGO language* Co-authored-by: Danil <danil.v.annenkov@gmail.com> Co-authored-by: Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>
AU-COBRA · Nov 19, 2020 · 6771127 · 6771127
1 parent cbd18da
commit 6771127
Show file tree

Hide file tree

Showing 11 changed files with 1,763 additions and 7 deletions.
diff --git a/.gitignore b/.gitignore
@@ -39,6 +39,7 @@ _opam/
 *.liq
 *.midlang
 *.out
+*.mligo
 
 ## Elm tests
 extraction/examples/elm-extract/elm-stuff/

diff --git a/extraction/_CoqProject b/extraction/_CoqProject
@@ -11,6 +11,8 @@
 
 -Q theories ConCert.Extraction
 theories/Annotations.v
+theories/CameLIGOExtract.v
+theories/CameLIGOPretty.v
 theories/CertifyingEta.v
 theories/ClosedAux.v
 theories/Common.v
@@ -39,6 +41,7 @@ theories/WcbvEvalAux.v
 
 -Q examples ConCert.Extraction.Examples
 examples/Ack.v
+examples/CameLIGOExtractionTests.v
 examples/CounterCertifiedExtraction.v
 examples/CounterDepCertifiedExtraction.v
 examples/CounterRefinementTypes.v