Joachim’s Haskell and lean4 experiments

.github/workflows/ci-spectec.yml

@@ -17,11 +17,23 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repo
-        uses: actions/checkout@v2
+        uses: actions/checkout@v3
+        with:
+          ref: ${{ github.event.pull_request.head.sha }}
       - name: Setup OCaml
         uses: ocaml/setup-ocaml@v2
         with:
           ocaml-compiler: 4.14.x
+      - name: Setup Haskell
+        uses: haskell/actions/setup@v2
+        with:
+          ghc-version: 9.2
+      - name: Setup Lean
+        run: |
+          cd /tmp
+          curl -LO https://github.com/leanprover/lean4-nightly/releases/download/nightly-2023-02-10/lean-4.0.0-nightly-2023-02-10-linux.tar.zst
+          tar xaf lean-4.0.0-nightly-2023-02-10-linux.tar.zst
+          echo "/tmp/lean-4.0.0-nightly-2023-02-10-linux/bin" >> $GITHUB_PATH
       - name: Setup Dune
         run: opam install --yes dune menhir mdx
       - name: Setup Latex

spectec/.gitignore

@@ -1 +1,9 @@
 watsup
+watsup-haskell
+watsup-lean4
+
+# lean stuff
+build
+lake-packages
+
+.direnv

spectec/Makefile

@@ -3,16 +3,18 @@
 NAME = watsup
 EXT = $(NAME)
 
-TESTDIRS = test-frontend test-latex
+TESTDIRS = test-frontend test-middlend test-latex
 
 
+DUNE_OPTS ?=
+
 # Main targets
 
 .PHONY: default all ci
 
-default: exe
+default: exe exe-haskell
 all: exe latex test
-ci: all test-frontend test-latex
+ci: all test-frontend test-middlend test-latex
 
 
 # Executable
@@ -24,9 +26,8 @@ OUTDIR = _build/default/src
 .PHONY: exe
 
 exe:
-	dune build $(SRCDIR)/$(EXE)
-	ln -f $(OUTDIR)/$(EXE) ./$(NAME)
-
+	dune build $(DUNE_OPTS) $(SRCDIR)/$(EXE)
+	ln -sf $(OUTDIR)/$(EXE) ./$(NAME)
 
 # Latex
 

spectec/lake-manifest.json

@@ -0,0 +1 @@
+{"version": 4, "packagesDir": "lake-packages", "packages": []}

spectec/lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+
+open Lake DSL
+
+package spectec
+
+@[default_target]
+lean_lib SpecTec where
+
+/- require std from git "https://github.com/leanprover/std4" @ "main" -/

spectec/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2023-02-10

spectec/src/backend-haskell/dune

@@ -0,0 +1,5 @@
+(library
+  (name backend_haskell)
+  (libraries util el frontend str)
+  (modules gen)
+)

spectec/src/backend-haskell/gen.ml

@@ -0,0 +1,157 @@
+open Il.Ast
+
+let include_input = false
+
+let parens s = "(" ^ s ^ ")"
+let ($$) s1 s2 = parens (s1 ^ " " ^ s2)
+let render_tuple how tys = parens (String.concat ", " (List.map how tys))
+
+let render_type_name (id : id) = String.capitalize_ascii id.it
+
+let render_rec_con (id : id) = "Mk" ^ render_type_name id
+
+let is_reserved = function
+ | "data"
+ -> true
+ | _ -> false
+
+let make_id s = match s with
+ | s when is_reserved s ->  s ^ "_"
+ | s -> String.map (function
+    | '.' -> '_'
+    | '-' -> '_'
+    | c -> c
+    ) s
+
+let render_con_name id : atom -> string = function
+  | Atom s ->
+    (* Lets disambiguate always, to start with 
+    if String.starts_with ~prefix:"_" s
+    then render_type_name id ^ s
+    else String.capitalize_ascii s
+    *)
+    if String.starts_with ~prefix:"_" s
+    then render_type_name id ^ make_id s
+    else render_type_name id ^ "_" ^ make_id s
+  | a -> "{- render_con_name: TODO -} " ^ Il.Print.string_of_atom a
+
+let render_con_name' (typ : typ) a = match typ.it with
+  | VarT id -> render_con_name id a
+  | _ -> "_ {- render_con_name': Typ not id " ^ Il.Print.string_of_typ typ ^ " -}"
+
+let render_field_name : atom -> string = function
+  | Atom s -> String.uncapitalize_ascii (make_id s)
+  | a -> "{- render_field_name: TODO -} " ^ Il.Print.string_of_atom a
+
+
+let rec render_typ (ty : typ) = match ty.it with
+  | VarT id -> render_type_name id
+  | BoolT -> "Bool"
+  | NatT -> "Natural"
+  | TextT -> "String"
+  | TupT tys -> render_tuple render_typ tys
+  | IterT (ty, Opt) -> "Maybe" $$ render_typ ty
+  | IterT (ty, _) -> "[" ^ render_typ ty ^ "]"
+
+let _unsupported_def d =
+  "{- " ^
+  Il.Print.string_of_def d ^
+  "\n-}"
+
+let rec prepend first rest = function
+  | [] -> ""
+  | (x::xs) -> first ^ x ^ prepend rest rest xs
+
+
+let render_variant_inj id1 id2 =
+  render_type_name id1 ^ "_of_" ^ render_type_name id2
+
+let render_variant_inj' (typ1 : typ) (typ2 : typ) = match typ1.it, typ2.it with
+  | VarT id1, VarT id2 -> render_variant_inj id1 id2
+  | _, _ -> "_ {- render_variant_inj': Typs not ids -}"
+
+let render_variant_case id (case : typcase) = match case with
+  | (a, {it = TupT [];_}, _hints) -> render_con_name id a
+  | (a, ty, _hints) -> render_con_name id a ^ " " ^ render_typ ty
+
+let rec render_exp (exp : exp) = match exp.it with
+  | VarE v -> v.it
+  | BoolE true -> "True"
+  | BoolE false -> "Frue"
+  | NatE n -> string_of_int n
+  | TextE t -> "\"" ^ String.escaped t ^ "\""
+  | MixE (_, e) -> render_exp e
+  | TupE es -> render_tuple render_exp es
+  | IterE (e, _) -> render_exp e
+  | CaseE (a, e) -> render_case a e exp.note
+  | SubE (e, typ1, typ2) -> render_variant_inj' typ2 typ1 $$ render_exp e
+  | DotE (e, a) -> render_exp e ^ "." ^ render_field_name a
+  | IdxE (e1, e2) -> parens (render_exp e1 ^ " !! " ^ ("fromIntegral" $$ render_exp e2))
+  | BinE (AddOp, e1, e2) -> parens (render_exp e1 ^ " + " ^ render_exp e2)
+  | _ -> "undefined {- " ^ Il.Print.string_of_exp exp ^ " -}"
+
+and render_case a e typ =
+    if e.it = TupE []
+    then render_con_name' typ a
+    else render_con_name' typ a $$ render_exp e
+
+let render_clause (id : id) (clause : clause) = match clause.it with
+  | DefD (_binds, lhs, rhs, premise) ->
+   (if premise <> [] then "-- Premises ignored! \n" else "") ^
+   make_id id.it ^ " " ^ render_exp lhs ^ " = " ^ render_exp rhs
+
+let rec render_def (d : def) =
+  begin
+    if include_input then
+    "{- " (*  ^ Util.Source.string_of_region d.at ^ "\n"*)  ^
+    Il.Print.string_of_def d ^
+    "\n-}\n"
+    else ""
+  end ^
+  match d.it with
+  | SynD (id, deftyp) ->
+    begin match deftyp.it with
+    | AliasT ty ->
+      "type " ^ render_type_name id ^ " = " ^ render_typ ty
+    | NotationT (mop, ty) ->
+      "type " ^ render_type_name id ^ " = {- mixop: " ^ Il.Print.string_of_mixop mop ^ " -} " ^ render_typ ty
+    | VariantT cases ->
+      "data " ^ render_type_name id ^ prepend "\n = " "\n | " (
+        List.map (render_variant_case id) cases
+      )
+    | StructT fields ->
+      (*
+      "type " ^ render_type_name id ^ " = " ^ render_tuple render_typ (
+        List.map (fun (_a, ty, _hints) -> ty) fields
+      )
+      *)
+      "data " ^ render_type_name id ^ " = " ^ render_rec_con id ^ prepend "\n { " "\n , " (
+        List.map (fun (a, ty, _hints) -> render_field_name a ^ " :: " ^ render_typ ty) fields
+      ) ^ "\n }"
+    end
+  | DecD (id, typ1, typ2, clauses) ->
+    make_id id.it ^ " :: " ^ render_typ typ1 ^ " -> " ^ render_typ typ2 ^ "\n" ^
+    if clauses = []
+    then make_id id.it ^ " = error \"function without clauses\""
+    else String.concat "\n" (List.map (render_clause id) clauses)
+  | RecD defs ->
+    String.concat "\n" (List.map render_def defs)
+  | _ -> ""
+
+let render_script (el : script) =
+  String.concat "\n\n" (List.map render_def el)
+
+let gen_string (el : script) =
+  "{-# LANGUAGE OverloadedRecordDot #-}\n" ^
+  "{-# LANGUAGE DuplicateRecordFields #-}\n" ^
+  "module Test where\n" ^
+  "import Prelude (Bool, String, undefined, error, Maybe, fromIntegral, (+), (!!))\n" ^
+  "import Numeric.Natural (Natural)\n" ^
+  render_script el
+
+
+let gen_file file el =
+  let haskell_code = gen_string el in
+  let oc = Out_channel.open_text file in
+  Fun.protect (fun () -> Out_channel.output_string oc haskell_code)
+    ~finally:(fun () -> Out_channel.close oc)

spectec/src/backend-haskell/gen.mli

@@ -0,0 +1,2 @@
+val gen_string : Il.Ast.script -> string
+val gen_file : string -> Il.Ast.script -> unit

spectec/src/backend-lean4/dune

@@ -0,0 +1,5 @@
+(library
+  (name backend_lean4)
+  (libraries util el frontend str)
+  (modules gen)
+)