initial commit?
This commit is contained in:
commit
fc022a16a4
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
|
@ -0,0 +1 @@
|
|||
_build
|
34
Eval.ml
Normal file
34
Eval.ml
Normal file
|
@ -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"
|
9
README.md
Normal file
9
README.md
Normal file
|
@ -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
|
4
bin/dune
Normal file
4
bin/dune
Normal file
|
@ -0,0 +1,4 @@
|
|||
(executable
|
||||
(public_name implicitt)
|
||||
(name main)
|
||||
(libraries implicitt))
|
1
bin/main.ml
Normal file
1
bin/main.ml
Normal file
|
@ -0,0 +1 @@
|
|||
let () = print_endline "Hello, World!"
|
26
dune-project
Normal file
26
dune-project
Normal file
|
@ -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
|
29
implicitt.opam
Normal file
29
implicitt.opam
Normal file
|
@ -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"
|
34
lib/Term.ml
Normal file
34
lib/Term.ml
Normal file
|
@ -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
|
34
lib/Value.ml
Normal file
34
lib/Value.ml
Normal file
|
@ -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
|
0
test/implicitt.ml
Normal file
0
test/implicitt.ml
Normal file
Loading…
Reference in New Issue
Block a user