From fc022a16a452231f4249669eb8fca85702705888 Mon Sep 17 00:00:00 2001 From: depsterr Date: Thu, 25 Aug 2022 20:29:55 +0200 Subject: [PATCH] initial commit? --- .gitignore | 1 + Eval.ml | 34 ++++++++++++++++++++++++++++++++++ README.md | 9 +++++++++ bin/dune | 4 ++++ bin/main.ml | 1 + dune-project | 26 ++++++++++++++++++++++++++ implicitt.opam | 29 +++++++++++++++++++++++++++++ lib/Term.ml | 34 ++++++++++++++++++++++++++++++++++ lib/Value.ml | 34 ++++++++++++++++++++++++++++++++++ lib/dune | 2 ++ test/dune | 2 ++ test/implicitt.ml | 0 12 files changed, 176 insertions(+) create mode 100644 .gitignore create mode 100644 Eval.ml create mode 100644 README.md create mode 100644 bin/dune create mode 100644 bin/main.ml create mode 100644 dune-project create mode 100644 implicitt.opam create mode 100644 lib/Term.ml create mode 100644 lib/Value.ml create mode 100644 lib/dune create mode 100644 test/dune create mode 100644 test/implicitt.ml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e35d885 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +_build diff --git a/Eval.ml b/Eval.ml new file mode 100644 index 0000000..4a12c29 --- /dev/null +++ b/Eval.ml @@ -0,0 +1,34 @@ +module V = Value +module T = Term + +let rec index : V.env -> int -> V.value + = fun env i -> + match env with + | [] -> failwith "Can't happen" + | x :: xs -> if i < 1 then x else index xs (i-1) + +let rec eval : V.env -> t.term -> V.value + = fun env tr -> + match tr with + | Var i -> index env i + | Type -> V.Type + | T0 -> V.T0 + | Ind0 (B b, t) -> failwith "todo" + | T1 -> V.T1 + | T1tr -> V.T1tr + | Ind1 (B b, t1 tr) -> failwith "todo" + | TNat -> V.TNat + | Zero -> V.Zero + | Suc n -> failwith "todo" + | IndN (B b, tz, B B ts, n) -> failwith "todo" + | TBool -> failwith "todo" + | True -> failwith "todo" + | False -> failwith "todo" + | IndB (B b, tt, tf, b) -> failwith "todo" + | Pi (dom, B cod) -> failwith "todo" + | Lam (B body) -> failwith "todo" + | App (f, x) -> failwith "todo" + | Sg (ty, tr) -> failwith "todo" + | Pair (x, y) -> failwith "todo" + | Fst tr -> failwith "todo" + | Snd tr -> failwith "todo" diff --git a/README.md b/README.md new file mode 100644 index 0000000..1f44228 --- /dev/null +++ b/README.md @@ -0,0 +1,9 @@ +# implicitt + +A "proof assistant" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml + +# TODO + +* Id types, lol (oops) +* evaluation +* conversion diff --git a/bin/dune b/bin/dune new file mode 100644 index 0000000..4f94a6e --- /dev/null +++ b/bin/dune @@ -0,0 +1,4 @@ +(executable + (public_name implicitt) + (name main) + (libraries implicitt)) diff --git a/bin/main.ml b/bin/main.ml new file mode 100644 index 0000000..7bf6048 --- /dev/null +++ b/bin/main.ml @@ -0,0 +1 @@ +let () = print_endline "Hello, World!" diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..e486793 --- /dev/null +++ b/dune-project @@ -0,0 +1,26 @@ +(lang dune 3.3) + +(name implicitt) + +(generate_opam_files true) + +(source + (uri "https://githug.xyz/depsterr/implcitt")) + +(authors "depsterr") + +(maintainers "depsterr") + +(license ISC) + +; (documentation https://url/to/documentation) + +(package + (name implicitt) + (synopsis "A poor proof assitant") + (description "A \"proof assistant\" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml.") + (depends ocaml dune) + (tags + (topics "proof assistant"))) + +; See the complete stanza docs at https://dune.readthedocs.io/en/stable/dune-files.html#dune-project diff --git a/implicitt.opam b/implicitt.opam new file mode 100644 index 0000000..f318f65 --- /dev/null +++ b/implicitt.opam @@ -0,0 +1,29 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "A poor proof assitant" +description: + "A \"proof assistant\" with holes and implcit arguments. Developed to learn about elaboration, meta variables and OCaml." +maintainer: ["depsterr"] +authors: ["depsterr"] +license: "ISC" +tags: ["topics" "proof assistant"] +depends: [ + "ocaml" + "dune" {>= "3.3"} + "odoc" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [ + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "https://githug.xyz/depsterr/implcitt" diff --git a/lib/Term.ml b/lib/Term.ml new file mode 100644 index 0000000..27f0789 --- /dev/null +++ b/lib/Term.ml @@ -0,0 +1,34 @@ +type var = Ix of int + +type 'a binder = B of 'a + +type term + = Var of var + + | Type + + | T0 + | Ind0 of term binder * term + + | T1 + | T1tr + | Ind1 of term binder * term * term + + | TNat + | Zero + | Suc of term + | IndN of term binder * term * term binder binder * term + + | TBool + | True + | False + | IndB of term binder * term * term * term + + | Pi of term * term binder + | Lam of term binder + | App of term * term + + | Sg of term * term binder + | Pair of term * term + | Fst of term + | Snd of term diff --git a/lib/Value.ml b/lib/Value.ml new file mode 100644 index 0000000..b808561 --- /dev/null +++ b/lib/Value.ml @@ -0,0 +1,34 @@ +module T = Term + +type lvl = Lvl of int + +type closure = C of env * T.term + +and env = value list + +and value + = Type + | T0 + | T1 + | T1vl + | TNat + | Suc of value + | Zero + | TBool + | True + | False + | Pi of value * closure + | Lam of closure + | Sg of value * closure + | Pair of value * value + | Stuck of stuck * value (* second arg is type *) + +and stuck + = Var of lvl + | Ind0 of closure * stuck + | Ind1 of closure * value * stuck + | IndN of closure * value * closure * stuck + | IndB of closure * value * value * stuck + | App of stuck * value * value (* fn; val; type of fn *) + | Fst of stuck + | Snd of stuck diff --git a/lib/dune b/lib/dune new file mode 100644 index 0000000..c76f468 --- /dev/null +++ b/lib/dune @@ -0,0 +1,2 @@ +(library + (name implicitt)) diff --git a/test/dune b/test/dune new file mode 100644 index 0000000..ebe353d --- /dev/null +++ b/test/dune @@ -0,0 +1,2 @@ +(test + (name implicitt)) diff --git a/test/implicitt.ml b/test/implicitt.ml new file mode 100644 index 0000000..e69de29