commit 709308d515cbf0daac98bb6b0a03a1d0f5ab1cc9
Author: Mava <maxime.jacquemin@pm.me>
Date:   Fri Nov 8 12:55:19 2024 +0100

    First steps into Type Systems

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..88f9974
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+_build/*
diff --git a/PTS.opam b/PTS.opam
new file mode 100644
index 0000000..b296c11
--- /dev/null
+++ b/PTS.opam
@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "A short synopsis"
+description: "A longer description"
+maintainer: ["Maintainer Name"]
+authors: ["Author Name"]
+license: "LICENSE"
+tags: ["topics" "to describe" "your" "project"]
+homepage: "https://github.com/username/reponame"
+doc: "https://url/to/documentation"
+bug-reports: "https://github.com/username/reponame/issues"
+depends: [
+  "ocaml"
+  "dune" {>= "3.16"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/username/reponame.git"
diff --git a/bin/dune b/bin/dune
new file mode 100644
index 0000000..166c9ee
--- /dev/null
+++ b/bin/dune
@@ -0,0 +1,4 @@
+(executable
+ (public_name PTS)
+ (name main)
+ (libraries PTS))
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..112143d
--- /dev/null
+++ b/dune-project
@@ -0,0 +1,26 @@
+(lang dune 3.16)
+
+(name PTS)
+
+(generate_opam_files true)
+
+(source
+ (github username/reponame))
+
+(authors "Author Name")
+
+(maintainers "Maintainer Name")
+
+(license LICENSE)
+
+(documentation https://url/to/documentation)
+
+(package
+ (name PTS)
+ (synopsis "A short synopsis")
+ (description "A longer description")
+ (depends ocaml dune)
+ (tags
+  (topics "to describe" your project)))
+
+; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html
diff --git a/lib/dune b/lib/dune
new file mode 100644
index 0000000..c49e41e
--- /dev/null
+++ b/lib/dune
@@ -0,0 +1,3 @@
+(library
+ (libraries bindlib)
+ (name PTS))
diff --git a/lib/types.ml b/lib/types.ml
new file mode 100644
index 0000000..96bf3f1
--- /dev/null
+++ b/lib/types.ml
@@ -0,0 +1,274 @@
+open Bindlib
+
+let ( let* ) m f = Option.bind m f
+let ( let+ ) m f = Option.map  f m
+let ( let$ ) m f = match m with None -> f () | Some x -> Some x
+
+type ('a, 'b) eq = Eq : ('a, 'a) eq
+
+module type ReflexiveType = sig
+  type 'a t
+  val equal : 'a t -> 'b t -> ('a, 'b) eq option
+end
+
+
+
+module type Parameters = sig
+
+  module Sort : ReflexiveType
+  type 'a sort = 'a Sort.t
+
+  type ('a, 'b) axiom
+  val is_valid_axiom : 'a sort -> 'b sort -> ('a, 'b) axiom option
+
+  type ('a, 'b, 'c) rule
+  val is_valid_rule : 'a sort -> 'b sort -> 'c sort -> ('a, 'b, 'c) rule option
+
+end
+
+
+
+module Make (Parameters : Parameters) = struct
+  include Parameters
+
+  type term =
+    | Sort        : 'n  sort -> term
+    | Variable    : term var -> term
+    | Application : application -> term
+    | Function    : abstraction -> term
+    | Product     : abstraction -> term
+
+  and application =
+    { func : term ; parameter : term }
+
+  and abstraction =
+    { binder : (term, term) binder ; parameter_typ : term }
+
+
+
+  let rec equal (l : term) (r : term) =
+    match l, r with
+    | Sort l, Sort r -> Option.is_some (Sort.equal l r)
+    | Variable l, Variable r -> eq_vars l r
+    | Application l, Application r ->
+      equal l.parameter r.parameter
+      && equal l.func r.func
+    | Function l, Function r ->
+      equal l.parameter_typ r.parameter_typ
+      && eq_binder equal l.binder r.binder
+    | Product l, Function r ->
+      equal l.parameter_typ r.parameter_typ
+      && eq_binder equal l.binder r.binder
+    | _, _ -> false
+
+  let rec beta_reduction = function
+    | Sort     s -> Sort     s
+    | Variable x -> Variable x
+    | Application { func = Function f ; parameter } -> subst f.binder parameter
+    | Application app ->
+      let func = beta_reduction app.func in
+      let parameter = beta_reduction app.parameter in
+      Application { func ; parameter }
+    | Function f ->
+      let parameter_typ = beta_reduction f.parameter_typ in
+      let binder = binder_compose f.binder beta_reduction in
+      Function { binder ; parameter_typ }
+    | Product p ->
+      let parameter_typ = beta_reduction p.parameter_typ in
+      let binder = binder_compose p.binder beta_reduction in
+      Product { binder ; parameter_typ }
+
+
+
+  module Context = Map.Make (struct
+    type t = term var
+    let compare = compare_vars
+  end)
+
+  type context  = term Context.t
+  type judgment = { context : context ; term : term ; typ : term }
+
+  type universe = Universe : _ sort -> universe
+  type checked  = Checked
+
+
+
+  let rec check universe { context ; term ; typ } =
+    let typ = beta_reduction typ in
+    let* Universe _ = universe context typ in
+    let judgment = { context ; term ; typ } in
+    let$ () = axiom       universe judgment in
+    let$ () = product     universe judgment in
+    let$ () = abstraction universe judgment in
+    let$ () = application universe judgment in
+    weakening universe judgment
+
+  and axiom _ { context ; term ; typ } =
+    match term, typ with
+    | Sort s1, Sort s2 when Context.is_empty context ->
+      let+ _ = is_valid_axiom s1 s2 in
+      Checked
+    | _, _ -> None
+
+  and start universe { context ; term ; typ } =
+    match term, typ with
+    | Variable x, a ->
+      let* a' = Context.find_opt x context in
+      let* () = if equal a a' then Some () else None in
+      let context = Context.remove x context in
+      let+ Universe _ = universe context a in
+      Checked
+    | _, _ -> None
+
+  and weakening universe { context ; term ; typ } =
+    let* x, b = Context.choose_opt context in
+    let* Universe _ = universe context b in
+    let context = Context.remove x context in
+    check universe { context ; term ; typ }
+
+  and product universe { context ; term ; typ } =
+    match term, typ with
+    | Product p, Sort s3 ->
+      let* Universe s1 = universe context p.parameter_typ in
+      let x, b = unbind p.binder in
+      let context = Context.add x p.parameter_typ context in
+      let* Universe s2 = universe context b in
+      let+ _ = is_valid_rule s1 s2 s3 in
+      Checked
+    | _, _ -> None
+
+  and application universe { context ; term ; typ } =
+    match term, typ with
+    | Application { func ; parameter }, app_typ ->
+      let* product = match func with Product p -> Some p | _ -> None in
+      let result_typ = subst product.binder parameter in
+      let* () = if equal app_typ result_typ then Some () else None in
+      let term = parameter and typ = product.parameter_typ in
+      check universe { context ; term ; typ }
+    | _, _ -> None
+
+  and abstraction universe { context ; term ; typ } =
+    match term, typ with
+    | Function f, Product p ->
+      let x, m = unbind f.binder in
+      let b = subst p.binder (Variable x) in
+      let* Universe _ = universe context (Product p) in
+      let context = Context.add x f.parameter_typ context in
+      check universe { context ; term = m ; typ = b }
+    | _, _ -> None
+
+end
+
+
+
+module Inductive_Constructions_Parameters = struct
+
+  type    zero = |
+  type 'n succ = |
+  type 'n nat = Zero : zero nat | Succ : 'n nat -> 'n succ nat
+
+  let rec eq : type a b. a nat -> b nat -> (a, b) eq option = fun l r ->
+    match l, r with
+    | Zero  , Zero   -> Some Eq
+    | Zero  , Succ _ -> None
+    | Succ _, Zero   -> None
+    | Succ l, Succ r ->
+      match eq l r with
+      | Some Eq -> Some Eq
+      | None -> None
+
+  type ('a, 'b) leq =
+    | LTZero : (zero, 'a) leq
+    | LTSucc : ('a, 'b) leq -> ('a succ, 'b succ) leq
+
+  let rec leq : type a b. a nat -> b nat -> (a, b) leq option = fun l r ->
+    match l, r with
+    | Zero  , Zero   -> Some LTZero
+    | Zero  , Succ _ -> Some LTZero
+    | Succ _, Zero   -> None
+    | Succ l, Succ r -> let+ prf = leq l r in LTSucc prf
+
+
+
+  type    set  = |
+  type    prop = |
+  type 'n typ  = |
+
+  type 's sort =
+    | Set  : set  sort
+    | Prop : prop sort
+    | Type : 'n nat -> 'n typ sort
+
+  type ('a, 'b) axiom =
+    | Set_is_Type_0     : (set , zero typ) axiom
+    | Prop_is_Type_0    : (prop, zero typ) axiom
+    | Type_Start : (zero typ, zero succ typ) axiom
+    | Type_Incr  : ('a typ, 'b typ) axiom -> ('a succ typ, 'b succ typ) axiom
+
+  type ('a, 'b, 'c) rule =
+    | Prop_Prop : (prop, prop, prop) rule
+    | Set_Prop  : (set , prop, prop) rule
+    | Prop_Set  : (prop, set , set ) rule
+    | Set_Set   : (set , set , set ) rule
+    | Type_Prop : ('n typ, prop, prop) rule
+    | Type_Right : ('l, 'r) leq -> ('l typ, 'r typ, 'r typ) rule
+    | Type_Left  : ('r, 'l) leq -> ('l typ, 'r typ, 'l typ) rule
+
+
+
+  type ('a, 'b) is_valid_axiom =
+    'a sort -> 'b sort -> ('a, 'b) axiom option
+
+  let rec is_valid_axiom : type a b. (a, b) is_valid_axiom = fun l r ->
+    match l, r with
+    | Set , Type Zero -> Some Set_is_Type_0
+    | Prop, Type Zero -> Some Prop_is_Type_0
+    | Type Zero, Type Succ Zero -> Some Type_Start
+    | Type Succ l, Type Succ r ->
+      let+ prf = is_valid_axiom (Type l) (Type r) in
+      Type_Incr prf
+    | _, _ -> None
+
+  type ('a, 'b,' c) is_valid_rule =
+    'a sort -> 'b sort -> 'c sort -> ('a, 'b, 'c) rule option
+
+  let rec is_valid_rule : type a b c. (a, b, c) is_valid_rule = fun a b c ->
+    match a, b, c with
+    | Prop, Prop, Prop -> Some Prop_Prop
+    | Set , Prop, Prop -> Some Set_Prop
+    | Prop, Set , Set  -> Some Prop_Set
+    | Set , Set , Set  -> Some Set_Set
+    | Type _, Prop, Prop -> Some Type_Prop
+    | Type a, Type b, Type c ->
+      begin match leq a b, eq b c, leq b a, eq a c with
+        | Some leq, Some Eq, _, _ -> Some (Type_Right leq)
+        | _, _, Some geq, Some Eq -> Some (Type_Left  geq)
+        | _, _, _, _ -> None
+      end
+    | _, _, _ -> None
+
+
+
+  type ('a, 'b) eq_sort = 'a sort -> 'b sort -> ('a, 'b) eq option
+
+  let equal : type a b. (a, b) eq_sort = fun l r ->
+    match l, r with
+    | Set, Set -> Some Eq
+    | Prop, Prop -> Some Eq
+    | Type l, Type r ->
+      begin match eq l r with
+        | Some Eq -> Some Eq
+        | None -> None
+      end
+    | _, _ -> None
+
+  module Sort = struct
+    type 'a t = 'a sort
+    let equal = equal
+  end
+
+end
+
+
+
+module Inductive_Constructions = Make (Inductive_Constructions_Parameters)
diff --git a/test/dune b/test/dune
new file mode 100644
index 0000000..e112afb
--- /dev/null
+++ b/test/dune
@@ -0,0 +1,2 @@
+(test
+ (name test_PTS))
diff --git a/test/test_PTS.ml b/test/test_PTS.ml
new file mode 100644
index 0000000..e69de29