Update: Typpe checker implementation in progress

Author: d-plaindoux

.ocamlformat

@@ -1,4 +1,4 @@
-version = 0.14.2
+version = 0.17.0
 margin = 80
 max-indent = 68
 
@@ -53,7 +53,6 @@ let-and = sparse
 let-binding-indent = 2
 let-binding-spacing = compact
 let-module = compact
-let-open = auto
 
 match-indent = 0
 match-indent-nested = never

Makefile

@@ -1,12 +1,12 @@
 .PHONY: info init all test clean fmt
 
 info:
-	echo "make [init|all|test|clean|fmt]"
+	echo "make [init|build|test|clean|fmt]"
 
 init:
 	eval `(opam env)`
 
-all:
+build:
 	dune build
 
 test:

lib/lexer/lexeme.ml renamed to attic/lib/lexer/lexeme.ml

@@ -0,0 +1,3 @@
+let () =
+  let open Alcotest in
+  run "checker" [ Variables_test.test_cases; Type_check_test.test_cases ]

lib/lexer/lexeme.mli renamed to attic/lib/lexer/lexeme.mli

@@ -21,7 +21,8 @@ let cases =
     , [
         Entity.Sig
           ( "::"
-          , Type.(Forall ("a", Kind.Type, Apply (Variable "list", Variable "a")))
+          , Type.(
+              Forall ("a", Kind.Type, Apply (Variable "list", Variable "a")))
           , None
           , [] )
       ] )
@@ -141,5 +142,5 @@ let test_cases =
   , List.map
       (fun (input, expected) ->
         test_case ("Should parse " ^ input) `Quick (fun () ->
-            should_parse input expected))
+            should_parse input expected ))
       cases )

lib/lexer/lexer.ml renamed to attic/lib/lexer/lexer.ml

@@ -30,5 +30,5 @@ let test_cases =
   , List.map
       (fun (input, expected) ->
         test_case ("Should parse " ^ input) `Quick (fun () ->
-            should_parse input expected))
+            should_parse input expected ))
       cases )

lib/lexer/lexer.mli renamed to attic/lib/lexer/lexer.mli

@@ -23,5 +23,5 @@ let test_cases =
             let t = Sys.time () in
             let fx = should_parse @@ Ioutils.read_fully filename in
             let () = Printf.printf "Execution time: %fs\n" (Sys.time () -. t) in
-            fx))
+            fx ))
       cases )

lib/lexer/location.mli renamed to attic/lib/lexer/location.mli

@@ -53,5 +53,5 @@ let test_cases =
   , List.map
       (fun (input, expected) ->
         test_case ("Should parse " ^ input) `Quick (fun () ->
-            should_parse input expected))
+            should_parse input expected ))
       cases )

lib/syntax/comment.ml renamed to attic/lib/syntax/comment.ml

@@ -54,5 +54,5 @@ let test_cases =
   , List.map
       (fun (input, expected) ->
         test_case ("Should parse " ^ input) `Quick (fun () ->
-            should_parse input expected))
+            should_parse input expected ))
       cases )

lib/syntax/comment.mli renamed to attic/lib/syntax/comment.mli

@@ -0,0 +1,2 @@
+module Kind = Kind
+module Type = Type

lib/syntax/entity.ml renamed to attic/lib/syntax/entity.ml

@@ -1,4 +1,4 @@
 (library
  (name lambe_ast)
  (public_name lambe.ast)
- (modules_without_implementation kind type term entity))
+ (modules_without_implementation kind type ast))

lib/syntax/entity.mli renamed to attic/lib/syntax/entity.mli

@@ -1,3 +1,16 @@
-type t =
-  | Arrow of t * t
-  | Type
+(*
+
+κ =
+  | ⋆
+  | κ→κ
+
+*)
+
+type 'a t =
+  | Type of 'a
+  | Arrow of 'a t * 'a t * 'a
+
+(*
+   The polymorphic type 'a holds open informations
+   like locations etc. depending on the context
+ *)

lib/syntax/entry.mli renamed to attic/lib/syntax/entry.mli

@@ -1,5 +1,46 @@
-type t =
-  | Path of string list (* ??? *)
-  | Variable of string
-  | Apply of t * t
-  | Forall of string * Kind.t * t
+(*
+
+Type and environment definition
+
+τ =
+  | α
+  | m
+  | τ → τ
+  | τ􏰀 #> τ
+  | τ τ
+  | τ + τ
+  | ∀(α : κ).τ
+  | ∃(α : κ).τ
+  | μ(α).τ
+  | c S
+  | Γ
+
+K = {mi:κi}I
+T = {mi􏰁=τi}I
+S = {mi:τi}I
+W = {Γi}I
+M = {mi􏰁εi}I
+Γ = ⟨K,T,S,W⟩
+
+*)
+
+type 'a set = (string * 'a) list
+
+type 'a t =
+  | Variable of string * 'a
+  | Arrow of 'a t * 'a t * 'a
+  | Invoke of 'a t * 'a t * 'a
+  | Apply of 'a t * 'a t * 'a
+  | Sum of 'a t * 'a t * 'a
+  | Forall of string * 'a Kind.t * 'a t * 'a
+  | Exists of string * 'a Kind.t * 'a t * 'a
+  | Rec of string * 'a t * 'a
+  | Const of string * (string * 'a t) list * 'a
+  | Trait of 'a gamma * 'a
+
+and 'a gamma = Gamma of 'a Kind.t set * 'a t set * 'a t set * 'a gamma list
+
+(*
+   The polymorphic type 'a holds open informations
+   like locations etc. depending on the context
+ *)

lib/syntax/kind.ml renamed to attic/lib/syntax/kind.ml

@@ -1,4 +1,5 @@
 (library
  (name lambe_checker)
  (public_name lambe.checker)
- (libraries lambe.ast))
+ (libraries lambe.ast)
+ (modules kind type))

lib/syntax/kind.mli renamed to attic/lib/syntax/kind.mli

@@ -0,0 +1,21 @@
+(*
+
+  ------
+  k ⊆κ ⋆
+
+  k1 ⊆κ k3    k2 ⊆κ k4
+  --------------------
+  k1 → k2 ⊆κ k3 → k4
+
+*)
+
+open Lambe_ast
+
+module Checker = struct
+  let rec subsume k1 k2 =
+    let open Kind in
+    match k1, k2 with
+    | _, Type _ -> true
+    | Arrow (k1, k2, _), Arrow (k3, k4, _) -> subsume k1 k3 && subsume k2 k4
+    | _ -> false
+end

lib/syntax/parser.ml renamed to attic/lib/syntax/parser.ml

@@ -0,0 +1,5 @@
+open Lambe_ast
+
+module Checker : sig
+  val subsume : 'a Kind.t -> 'a Kind.t -> bool
+end

lib/syntax/term.ml renamed to attic/lib/syntax/term.ml

@@ -0,0 +1,67 @@
+open Lambe_ast
+
+(*
+module Gamma = struct
+  open Type
+
+  let neutral = Gamma ([], [], [], [])
+
+  let combine (Gamma (k, t, s, w)) (Gamma (k', t', s', w')) =
+    Gamma (k @ k', t @ t', s @ s', w @ w')
+
+  let k_get = function Gamma (k, _, _, _) -> k
+
+  let k_set k = Gamma (k, [], [], [])
+
+  let t_get = function Gamma (_, t, _, _) -> t
+
+  let t_set t = Gamma ([], t, [], [])
+
+  let s_get = function Gamma (_, _, s, _) -> s
+
+  let w_get = function Gamma (_, _, _, w) -> w
+end
+*)
+
+module Substitution = struct
+  (* Substituste v by r in t *)
+  let rec substitute v r t =
+    let open Type in
+    let subst_field (n, t1) = n, substitute v r t1 in
+    let rec subst_gamma (Gamma (kd, ty, si, wi)) =
+      Gamma
+        ( kd
+        , List.map subst_field ty
+        , List.map subst_field si
+        , List.map subst_gamma wi )
+    in
+    match t with
+    | Variable (a, _) when v = a -> r
+    | Variable _ -> t
+    | Arrow (t1, t2, s) -> Arrow (substitute v r t1, substitute v r t2, s)
+    | Invoke (t1, t2, s) -> Invoke (substitute v r t1, substitute v r t2, s)
+    | Apply (t1, t2, s) -> Apply (substitute v r t1, substitute v r t2, s)
+    | Sum (t1, t2, s) -> Sum (substitute v r t1, substitute v r t2, s)
+    | Forall (a, _, _, _) when a = v -> t
+    | Forall (a, k, t1, s) -> Forall (a, k, substitute v r t1, s)
+    | Exists (a, _, _, _) when a = v -> t
+    | Exists (a, k, t1, s) -> Exists (a, k, substitute v r t1, s)
+    | Rec (a, _, _) when v = a -> t
+    | Rec (a, t1, s) -> Rec (a, substitute v r t1, s)
+    | Const (a, l1, s) -> Const (a, List.map subst_field l1, s)
+    | Trait (gamma, s) -> Trait (subst_gamma gamma, s)
+end
+
+module Checker = struct
+  let rec subsume g t1 t2 =
+    let open Type in
+    let open Substitution in
+    match t1, t2 with
+    | _ when t1 = t2 -> true
+    | Arrow (t1, t2, _), Arrow (t3, t4, _) -> subsume g t3 t1 && subsume g t2 t4
+    | Invoke (t1, t2, _), Invoke (t3, t4, _) ->
+      subsume g t3 t1 && subsume g t2 t4
+    | t1, Sum (t2, t3, _) -> subsume g t1 t2 || subsume g t1 t3
+    | Rec(a,t1,_),Rec(b,t2,s) -> subsume g t1 (substitute b (Variable (a,s)) t2) (* Fresh variable required *)
+    | _ -> false
+end

lib/syntax/term.mli renamed to attic/lib/syntax/term.mli

@@ -0,0 +1,5 @@
+open Lambe_ast
+
+module Checker : sig
+  val subsume : 'a Type.gamma -> 'a Type.t -> 'a Type.t -> bool
+end