Merge pull request #1 from formal-land/guillaume-claret@init-repository

feat: init the project with a simple example

.github/workflows/coq-of-hs.yml

@@ -0,0 +1,127 @@
+name: coq-of-hs CI
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+    branches:
+      - main
+jobs:
+  linux:
+    name: coq-of-hs CI - Linux - ${{ matrix.compiler }}
+    runs-on: ubuntu-22.04
+    timeout-minutes: 60
+    container:
+      image: buildpack-deps:jammy
+    strategy:
+      matrix:
+        include:
+          - compiler: ghc-8.10.7
+            compilerKind: ghc
+            compilerVersion: 8.10.7
+            setup-method: ghcup
+      # Because it is the reverse by default here
+      fail-fast: false
+    steps:
+      - name: apt
+        run: |
+          apt-get update
+          apt-get install -y --no-install-recommends gnupg ca-certificates dirmngr curl git software-properties-common libtinfo5 libnuma-dev
+          mkdir -p "$HOME/.ghcup/bin"
+          curl -sL https://downloads.haskell.org/ghcup/0.1.20.0/x86_64-linux-ghcup-0.1.20.0 > "$HOME/.ghcup/bin/ghcup"
+          chmod a+x "$HOME/.ghcup/bin/ghcup"
+          "$HOME/.ghcup/bin/ghcup" install ghc "$HCVER" || (cat "$HOME"/.ghcup/logs/*.* && false)
+          "$HOME/.ghcup/bin/ghcup" install cabal 3.10.2.0 || (cat "$HOME"/.ghcup/logs/*.* && false)
+        env:
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
+      - name: Set PATH and environment variables
+        run: |
+          echo "$HOME/.cabal/bin" >> $GITHUB_PATH
+          echo "LANG=C.UTF-8" >> "$GITHUB_ENV"
+          echo "CABAL_DIR=$HOME/.cabal" >> "$GITHUB_ENV"
+          echo "CABAL_CONFIG=$HOME/.cabal/config" >> "$GITHUB_ENV"
+          HCDIR=/opt/$HCKIND/$HCVER
+          HC=$("$HOME/.ghcup/bin/ghcup" whereis ghc "$HCVER")
+          HCPKG=$(echo "$HC" | sed 's#ghc$#ghc-pkg#')
+          HADDOCK=$(echo "$HC" | sed 's#ghc$#haddock#')
+          echo "HC=$HC" >> "$GITHUB_ENV"
+          echo "HCPKG=$HCPKG" >> "$GITHUB_ENV"
+          echo "HADDOCK=$HADDOCK" >> "$GITHUB_ENV"
+          echo "CABAL=$HOME/.ghcup/bin/cabal-3.10.2.0 -vnormal+nowrap" >> "$GITHUB_ENV"
+          HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\d+)\.(\d+)\.(\d+)(\.(\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')
+          echo "HCNUMVER=$HCNUMVER" >> "$GITHUB_ENV"
+          echo "ARG_TESTS=--enable-tests" >> "$GITHUB_ENV"
+          echo "ARG_BENCH=--enable-benchmarks" >> "$GITHUB_ENV"
+          echo "HEADHACKAGE=false" >> "$GITHUB_ENV"
+          echo "ARG_COMPILER=--$HCKIND --with-compiler=$HC" >> "$GITHUB_ENV"
+          echo "GHCJSARITH=0" >> "$GITHUB_ENV"
+        env:
+          HCKIND: ${{ matrix.compilerKind }}
+          HCNAME: ${{ matrix.compiler }}
+          HCVER: ${{ matrix.compilerVersion }}
+      - name: env
+        run: |
+          env
+      - name: write cabal config
+        run: |
+          mkdir -p $CABAL_DIR
+          cat >> $CABAL_CONFIG <<EOF
+          remote-build-reporting: anonymous
+          write-ghc-environment-files: never
+          remote-repo-cache: $CABAL_DIR/packages
+          logs-dir:          $CABAL_DIR/logs
+          world-file:        $CABAL_DIR/world
+          extra-prog-path:   $CABAL_DIR/bin
+          symlink-bindir:    $CABAL_DIR/bin
+          installdir:        $CABAL_DIR/bin
+          build-summary:     $CABAL_DIR/logs/build.log
+          store-dir:         $CABAL_DIR/store
+          install-dirs user
+            prefix: $CABAL_DIR
+          repository hackage.haskell.org
+            url: http://hackage.haskell.org/
+          EOF
+          cat >> $CABAL_CONFIG <<EOF
+          jobs: 2
+          EOF
+          GHCJOBS=-j2
+          cat >> $CABAL_CONFIG <<EOF
+          program-default-options
+            ghc-options: $GHCJOBS +RTS -M3G -RTS
+          EOF
+          cat $CABAL_CONFIG
+      - name: versions
+        run: |
+          $HC --version || true
+          $HC --print-project-git-commit-id || true
+          $CABAL --version || true
+      - name: update cabal index
+        run: |
+          $CABAL v2-update -v
+      - name: checkout
+        uses: actions/checkout@v3
+        with:
+          path: source
+      - name: install dependencies
+        run: |
+          cd $GITHUB_WORKSPACE/source/
+          $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks --dependencies-only -j2 all
+          $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH --dependencies-only -j2 all
+      - name: build w/o tests
+        run: |
+          cd $GITHUB_WORKSPACE/source/
+          $CABAL v2-build $ARG_COMPILER --disable-tests --disable-benchmarks all
+      - name: build
+        run: |
+          cd $GITHUB_WORKSPACE/source/
+          $CABAL v2-build $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --write-ghc-environment-files=always
+      - name: tests
+        run: |
+          cd $GITHUB_WORKSPACE/source/
+          $CABAL v2-test $ARG_COMPILER $ARG_TESTS $ARG_BENCH all --test-show-details=direct
+      - name: check that the diff is empty
+        run: |
+          cd $GITHUB_WORKSPACE/source/
+          git -c color.ui=always diff --exit-code

_CoqProject

@@ -0,0 +1 @@
+-arg -impredicative-set

coq-of-hs.cabal

@@ -0,0 +1,21 @@
+cabal-version: 3.8
+name: coq-of-hs
+version: 1.0.0.0
+
+library
+  build-depends:
+    base >= 4.14,
+    directory,
+    filepath,
+    ghc >= 8.10.7,
+    prettyprinter
+  hs-source-dirs: src
+  exposed-modules: CoqOfHs
+
+test-suite test-plugin
+  build-depends:
+    base,
+    coq-of-hs
+  hs-source-dirs: test
+  ghc-options: -fplugin=CoqOfHs
+  main-is: Main.hs

coq_translation/test/Main.v

@@ -0,0 +1,187 @@
+Require Export Coq.Strings.Ascii.
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+
+Local Open Scope list_scope.
+Local Open Scope string_scope.
+Local Open Scope Z_scope.
+
+Import List.ListNotations.
+
+Parameter Rational : Set.
+
+Module Lit.
+  Inductive t : Set :=
+  | Char (_ : ascii)
+  | Number (_ : Z)
+  | String (_ : string)
+  | NullAddr
+  | Rubbish
+  | Float (_ : Rational)
+  | Double (_ : Rational)
+  | Label (_ : string).
+End Lit.
+
+Module Case.
+  Inductive t (A : Set) : Set :=
+  | Con (_ : string) (_ : list A -> A)
+  | Lit (_ : Lit.t) (_ : A)
+  | Default (_ : A).
+  Arguments Con {A}.
+  Arguments Lit {A}.
+  Arguments Default {A}.
+End Case.
+
+Module Val.
+  #[bypass_check(positivity)]
+  CoInductive t : Set :=
+  | Lit (_ : Lit.t)
+  | Con (_ : string) (_ : list t)
+  | App (_ _ : t)
+  | Lam (_ : t -> t)
+  | Case (_ : t) (_ : t -> list (Case.t t))
+  | Impossible.
+End Val.
+
+Definition Isharp' : Val.t :=
+  Val.Lam (fun z => Val.Con "I#" [z]).
+
+Definition lbracket'rbracket' : Val.t :=
+  Val.Con "[]" [].
+
+Definition colon' : Val.t :=
+  Val.Lam (fun x => Val.Lam (fun xs => Val.Con ":" [x; xs])).
+
+Definition build : Val.t :=
+  Val.Lam (fun l => Val.App (Val.App l colon') lbracket'rbracket').
+
+Parameter plus'plus' : Val.t.
+
+Parameter _'Module : Val.t.
+
+Parameter TrNameS : Val.t.
+
+Parameter eq'eq' : Val.t.
+
+Parameter dollar'fEqNatural : Val.t.
+
+Parameter fromInteger : Val.t.
+
+Parameter dollar'fNumNatural : Val.t.
+
+Parameter minus' : Val.t.
+
+Parameter _'False : Val.t.
+
+Parameter _'True : Val.t.
+
+Parameter _'return : Val.t.
+
+Parameter dollar'fMonadIO : Val.t.
+
+Parameter lparen'rparen' : Val.t.
+
+Parameter runMainIO : Val.t.
+
+Definition x : Val.t := (Val.App Isharp' (Val.Lit (Lit.Number 5))).
+
+CoFixpoint onlyOne : Val.t :=
+  (Val.App (Val.App colon' (Val.App Isharp' (Val.Lit (Lit.Number 1)))) onlyOne).
+
+Definition twoOne : Val.t :=
+  (Val.App
+    (Val.App
+      plus'plus'
+      (Val.App
+        build
+        (Val.Lam
+          (fun (c_d1ze : Val.t) =>
+            (Val.Lam
+              (fun (n_d1zf : Val.t) =>
+                (Val.App
+                  (Val.App c_d1ze (Val.App Isharp' (Val.Lit (Lit.Number 2))))
+                  (Val.App
+                    (Val.App c_d1ze (Val.App Isharp' (Val.Lit (Lit.Number 2))))
+                    n_d1zf))))))))
+    onlyOne).
+
+CoFixpoint f : Val.t := (Val.Lam (fun (x : Val.t) => (Val.App f x))).
+
+CoFixpoint fixObvious : Val.t :=
+  (Val.Lam (fun (f : Val.t) => (Val.App f (Val.App fixObvious f)))).
+
+Definition fixSubtle : Val.t :=
+  (Val.Lam (fun (f : Val.t) => let cofix x := (Val.App f x) in x)).
+
+Definition emptyList : Val.t := lbracket'rbracket'.
+
+Definition dollar'trModule : Val.t :=
+  (Val.App
+    (Val.App _'Module (Val.App TrNameS (Val.Lit (Lit.String "main"))))
+    (Val.App TrNameS (Val.Lit (Lit.String "Main")))).
+
+CoFixpoint odd : Val.t :=
+  (Val.Lam
+    (fun (ds_d1yV : Val.t) =>
+      (Val.Case
+        (Val.App
+          (Val.App (Val.App eq'eq' dollar'fEqNatural) ds_d1yV)
+          (Val.App
+            (Val.App fromInteger dollar'fNumNatural)
+            (Val.Lit (Lit.Number 0))))
+        (fun wild_00 =>
+          [
+            Case.Con
+              "False"
+              (fun α =>
+                (match α with
+                | [] =>
+                  (Val.App
+                    even
+                    (Val.App
+                      (Val.App (Val.App minus' dollar'fNumNatural) ds_d1yV)
+                      (Val.App
+                        (Val.App fromInteger dollar'fNumNatural)
+                        (Val.Lit (Lit.Number 1)))))
+                | _ => Val.Impossible
+                end));
+            Case.Con
+              "True"
+              (fun α =>
+                (match α with | [] => _'False | _ => Val.Impossible end))
+          ]))))
+
+with even : Val.t :=
+  (Val.Lam
+    (fun (ds_d1z4 : Val.t) =>
+      (Val.Case
+        (Val.App
+          (Val.App (Val.App eq'eq' dollar'fEqNatural) ds_d1z4)
+          (Val.App
+            (Val.App fromInteger dollar'fNumNatural)
+            (Val.Lit (Lit.Number 0))))
+        (fun wild_00 =>
+          [
+            Case.Con
+              "False"
+              (fun α =>
+                (match α with
+                | [] =>
+                  (Val.App
+                    odd
+                    (Val.App
+                      (Val.App (Val.App minus' dollar'fNumNatural) ds_d1z4)
+                      (Val.App
+                        (Val.App fromInteger dollar'fNumNatural)
+                        (Val.Lit (Lit.Number 1)))))
+                | _ => Val.Impossible
+                end));
+            Case.Con
+              "True"
+              (fun α => (match α with | [] => _'True | _ => Val.Impossible end))
+          ])))).
+
+Definition main : Val.t :=
+  (Val.App (Val.App _'return dollar'fMonadIO) lparen'rparen').
+
+Definition main : Val.t := (Val.App runMainIO main).