fstar

.gitignore

@@ -1,2 +1,4 @@
 .direnv
 _build
+
+Hello.ml

.vscode/settings.json

@@ -1,5 +1,6 @@
 {
-    "ocaml.sandbox": {
+	"ocaml.sandbox": {
-        "kind": "global"
+		"kind": "global"
-    }
+	},
+	"editor.formatOnSave": false
 }

Makefile

@@ -0,0 +1,2 @@
+watch:
+	watchexec -e fst fstar.exe core/hello.fst --codegen OCaml --extract_module Hello

core/hello.fst

@@ -0,0 +1,102 @@
+// https://www.fstar-lang.org/tutorial/book/part2/part2_stlc.html
+
+module Hello
+
+open FStar.Exn
+
+type monotype =
+  | MTVar of string
+  | MTArrow of monotype * monotype
+  | MTEmpty
+  | MTUnit
+  | MTSum of monotype * monotype
+  | MTProd of monotype * monotype
+  | MTInductive of string * monotype
+
+type polytype =
+  | Mono of monotype
+  | Forall of string * polytype
+
+type expr =
+  | EVar of string
+  | EPoly of string * expr
+  | ETypeSub
+  | ELam of string * monotype * expr
+  | EApp of expr * expr
+  | EAbort of expr
+  | EInl of expr
+  | EInr of expr
+  | ECase of expr * (string * expr) * (string * expr)
+  | EUnit
+  | EPair of expr * expr
+  | EFst of expr
+  | ESnd of expr
+  | ERoll of string * monotype * expr
+  | EFold of (string * monotype) * monotype * (expr * string * expr)
+
+let rec appearsIn
+  (a : string)
+  (mono : monotype)
+  : prop
+=
+  match mono with
+  | MTEmpty -> False
+  | MTUnit -> False
+  | MTVar b -> if a = b then True else False
+  | MTProd (left, right) -> appearsIn a left \/ appearsIn a right
+  | MTSum (left, right) -> appearsIn a left \/ appearsIn a right
+  | MTArrow (left, right) -> appearsIn a left \/ appearsIn a right
+  | MTInductive (b, t) -> if a = b then False else appearsIn a t
+
+let rec strictlyPositive
+  (a : string)
+  (mono : monotype)
+  : prop
+=
+  match mono with
+  | MTEmpty -> True
+  | MTUnit -> True
+  | MTVar b -> True
+  | MTProd (left, right) -> strictlyPositive a left /\ strictlyPositive a right
+  | MTSum (left, right) -> strictlyPositive a left /\ strictlyPositive a right
+  | MTArrow (t1, t2) -> ~(appearsIn a t1) /\ strictlyPositive a t2
+  | MTInductive (_, t) -> strictlyPositive a t
+
+exception InductiveCase
+
+let rec logNoInductive
+  (mono : monotype)
+  (a : string)
+  : Exn monotype (requires True) (ensures (fun _ -> True))
+=
+  match mono with
+  | MTEmpty -> MTEmpty
+  | MTUnit -> MTEmpty
+  | MTVar a' -> if a' = a then MTUnit else MTEmpty
+  | MTArrow (t1, t2) -> MTProd (t1, logNoInductive t2 a)
+  | MTProd (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
+  | MTSum (left, right) -> MTSum (logNoInductive left a, logNoInductive right a)
+  | MTInductive (_, _) -> raise InductiveCase
+
+let rec isVal
+  (e : expr)
+  : prop
+=
+  match e with
+  | EPoly (_, _) -> True
+  | ELam (_, _, _) -> True
+  | EInl e' -> isVal e'
+  | EInr e' -> isVal e'
+  | EUnit -> True
+  | EPair (e1, e2) -> isVal e1 /\ isVal e2
+  | ERoll (_, _, e') -> isVal e'
+  | _ -> False
+
+  // | EVar _ -> True
+  // | ETypeSub -> True
+  // | EApp (_, _) -> True
+  // | EAbort _ -> True
+  // | ECase (_, _, _) -> True
+  // | EFst _ -> True
+  // | ESnd _ -> True
+  // | EFold (_, _, _) -> True

flake.nix

@@ -7,16 +7,18 @@ inputs.nixpkgs.url = "github:nixos/nixpkgs";
         flakePkgs = { main = pkgs.ocamlPackages.callPackage ./. { }; };
       in {
         devShell = pkgs.mkShell {
-          inputsFrom = with flakePkgs; [ main ];
+          # inputsFrom = with flakePkgs; [ main ];
           packages = (with pkgs; [
-inotify-tools
+# inotify-tools
+fstar
+nixfmt-rfc-style
            ]) ++ (with pkgs.ocamlPackages; [
-            ocaml-lsp
+            # ocaml-lsp
-            ppxlib
+            # ppxlib
-            ppx_deriving
+            # ppx_deriving
-            alcotest
+            # alcotest
-            yojson
+            # yojson
-            ezjsonm
+            # ezjsonm
           ]);
         };
       });