Skip to content

Navigation Menu

Sign in
Appearance settings

Search code, repositories, users, issues, pull requests...

Provide feedback

We read every piece of feedback, and take your input very seriously.

Saved searches

Use saved searches to filter your results more quickly
Sign up
Appearance settings
This repository was archived by the owner on Jan 23, 2023. It is now read-only.

Commit 4f7f30f

Browse files
Expressions typecheker in progress
1 parent 770f445 commit 4f7f30f

File tree

3 files changed

+79
-67
lines changed

3 files changed

+79
-67
lines changed

‎lib/checker/expr.ml‎

Lines changed: 44 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,7 @@
11
let ( <$> ) = Option.map
22

33
let ( <*> ) f a = (match f with Some f -> f <$> a | None -> None)
4-
(* let ( >>= ) ma f = Option.bind ma f *)
54

6-
(*
7-
Provides basic functions used when a type defnition or kind definition
8-
should be retrieved from Gamma. This operation is performed with a
9-
depth first seach strategy.
10-
*)
115
module Finder = struct
126
let find_signature n g =
137
let open Lambe_ast.Type in
@@ -47,39 +41,53 @@ end
4741

4842
module Checker = struct
4943
let rec check g e t v =
44+
let module T = Lambe_ast.Type in
45+
let print_check = Lambe_render.Expr.Render.check Format.std_formatter in
46+
let _ = print_string " Checking > " in
47+
let _ = print_check e (Some t) in
48+
let result = check_generic g e t v in
49+
let _ = print_string " Checking < " in
50+
let _ = print_check e (Some t) in
51+
result
52+
53+
and check_generic g e t v =
54+
let module T = Lambe_ast.Type in
55+
let open List in
56+
match t with
57+
| T.Forall (n, k, t, _) -> check Gamma.(Helpers.k_set [ n, k ] + g) e t v
58+
| _ -> check_lambda g e t v
59+
60+
and check_lambda g e t v =
5061
let open Context in
51-
let open Lambe_ast.Expr in
52-
let open Type.Checker.Operator in
5362
let module T = Lambe_ast.Type in
5463
let open List in
55-
let print_check = Lambe_render.Expr.Render.check Format.std_formatter in
56-
let rec check g e t v =
57-
let _ = print_string " > " in
58-
let _ = print_check e (Some t) in
59-
let result =
60-
match e with
61-
| Lambda (a, e, s) -> (
62-
let n, v = Variables.fresh v in
63-
let e = Substitution.substitute a (Variable (n, s)) e in
64-
match Type.Checker.reduce g t with
65-
| Some T.(Arrow (t1, t2, _)) ->
66-
check Gamma.(Helpers.s_set [ n, t1 ] + g) e t2 v
67-
| _ -> false, v )
68-
| Method (e, _) -> (
69-
match Type.Checker.reduce g t with
70-
| Some T.(Invoke (t1, t2, _)) ->
71-
check Gamma.(Helpers.s_set [ "self", t1 ] + g) e t2 v
72-
| _ -> false, v )
73-
| _ ->
74-
let r, v = synthetize g e v in
75-
Option.fold ~none:(false, v) ~some:Fun.id
76-
((fun t' -> g |- (t' <? t) v) <$> r)
77-
in
78-
let _ = print_string " < " in
79-
let _ = print_check e (Some t) in
80-
result
81-
in
82-
check g e t v
64+
match e, t with
65+
| Lambda (a, e, s), _ -> (
66+
let n, v = Variables.fresh v in
67+
let e = Substitution.substitute a (Variable (n, s)) e in
68+
match Type.Checker.reduce g t with
69+
| Some T.(Arrow (t1, t2, _)) ->
70+
check Gamma.(Helpers.s_set [ n, t1 ] + g) e t2 v
71+
| _ -> false, v )
72+
| _ -> check_method g e t v
73+
74+
and check_method g e t v =
75+
let module T = Lambe_ast.Type in
76+
let open List in
77+
match e with
78+
| Method (e, _) -> (
79+
match Type.Checker.reduce g t with
80+
| Some T.(Invoke (t1, t2, _)) ->
81+
check Gamma.(Helpers.s_set [ "self", t1 ] + g) e t2 v
82+
| _ -> false, v )
83+
| _ -> check_after_synthetize g e t v
84+
85+
and check_after_synthetize g e t v =
86+
let open Type.Checker.Operator in
87+
let module T = Lambe_ast.Type in
88+
let r, v = synthetize g e v in
89+
Option.fold ~none:(false, v) ~some:Fun.id
90+
((fun t' -> g |- (t' <? t) v) <$> r)
8391

8492
and synthetize g e v =
8593
let print_check = Lambe_render.Expr.Render.check Format.std_formatter in

‎lib/checker/type.ml‎

Lines changed: 21 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -157,45 +157,35 @@ module Checker = struct
157157
let reduce g t =
158158
let open Substitution in
159159
let open Lambe_ast.Type in
160-
let depth = ref 0 in
161-
let print_reduce = Lambe_render.Type.Render.reduce Format.std_formatter in
160+
(* TODO(didier) first is Ugly -> remove it *)
162161
let rec reduce g t first =
163-
let _ = depth := !depth + 1 in
164-
let _ = print_int !depth in
165-
let _ = print_string " > " in
166-
let _ = print_reduce t (Some (Variable ("?", TypeContext.get t))) in
167-
let result =
168-
match t with
169-
| Variable (n, _) ->
170-
Some
171-
(Option.fold ~none:t ~some:Fun.id
172-
(Finder.find_type n g >>= (fun t -> reduce g t first)) )
173-
| Apply (t1, t2, _) -> (
174-
reduce g t1 false
175-
>>= function
176-
| Lambda (n, k, t1', _) when check g t2 k ->
177-
reduce g (substitute n t2 t1') first
178-
| _ -> None )
179-
| Use (t1, (Variable (_, _) as v), _) -> (
180-
reduce g t1 first
181-
>>= function
182-
| Trait (g', _) -> reduce g' v first >>= (fun t2 -> reduce g t2 first)
183-
| _ -> None )
184-
| Use (g, t, s) -> Some (Distribute.distribute g s t)
185-
| Rec (n, _, t', _) when first = false -> Some (substitute n t t')
186-
| _ -> Some t
187-
in
188-
let _ = print_int !depth in
189-
let _ = print_string " < " in
190-
let _ = print_reduce t result in
191-
result
162+
match t with
163+
| Variable (n, _) ->
164+
Some
165+
(Option.fold ~none:t ~some:Fun.id
166+
(Finder.find_type n g >>= (fun t -> reduce g t first)) )
167+
| Apply (t1, t2, _) -> (
168+
reduce g t1 false
169+
>>= function
170+
| Lambda (n, k, t1', _) when check g t2 k ->
171+
reduce g (substitute n t2 t1') first
172+
| _ -> None )
173+
| Use (t1, (Variable (_, _) as v), _) -> (
174+
reduce g t1 first
175+
>>= function
176+
| Trait (g', _) -> reduce g' v first >>= (fun t2 -> reduce g t2 first)
177+
| _ -> None )
178+
| Use (g, t, s) -> Some (Distribute.distribute g s t)
179+
| Rec (n, _, t', _) when first = false -> Some (substitute n t t')
180+
| _ -> Some t
192181
in
193182
reduce g t true
194183

195184
let rec subsume g t1 t2 v =
196185
let open Context in
197186
let module K = Lambe_ast.Kind in
198187
let print_subtype = Lambe_render.Type.Render.subtype Format.std_formatter in
188+
let _ = print_string " Subsume > " in
199189
let _ = print_subtype t1 t2 in
200190
if t1 = t2
201191
then check g t1 (K.Type (TypeContext.get t1)), v

‎test/checker/expr_check.ml‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,17 @@ let test_case_023 () =
248248
| string"
249249
expected computed
250250

251+
let test_case_024 () =
252+
let expected = true
253+
and computed, _ =
254+
empty
255+
|- ( lambda "i" (v "i") <:?> T.(forall ("a", K.star) (v "a" |-> v "a")) )
256+
Variables.create
257+
in
258+
Alcotest.(check bool)
259+
"should accept lambda(v).v : forall (a:*).(a -> a)"
260+
expected computed
261+
251262
let test_cases =
252263
let open Alcotest in
253264
( "Expression check"
@@ -293,4 +304,7 @@ let test_cases =
293304
; test_case
294305
"Accept a:int|string |- when a is int -> a is string -> a :? int|string"
295306
`Quick test_case_023
307+
; test_case
308+
"Accept lambda(v).v : forall (a:*).(a -> a)"
309+
`Quick test_case_024
296310
] )

0 commit comments

Comments
(0)

AltStyle によって変換されたページ (->オリジナル) /