lambda_mountain 1.12.1

Lambda Mountain
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63


context::new := λ . (
   (Context(
      ()
      0
   ))
);

context::lookup := λ ctx key key-type . (tail(
   (local bindings)
   (set bindings (context::get-bindings ctx))
   (local return)
   (while bindings (tail(
      (if (eq( key (head(tail bindings)) )) (tail(
         (if key-type (tail(
            (local body)
            (set body (tail(tail bindings)))
            (local body-type)
            (set body-type (typecheck-lookup body))
            (if (not body-type) (
               (fail (UntypedBinding body))
            ) ())
            (if (not(eq( '-> (head(typecheck-slot( body-type '-> ))) ))) (tail(
               (set return body)
               (set bindings ())
            )) (
               (if (typecheck-apply-plural( body-type key-type )) (tail(
                  (set return body)
                  (set bindings ())
               )) ())
            ))
         )) (tail(
            (set return (tail(tail bindings)))
            (set bindings ())
         )))
      )) ())
      (set bindings (head bindings))
   )))
   return
));

context::bind := λ ctx key term . (match ctx (
   ()
   ( (Context( old-ctx offset )) (tail(
      ()
      (Context( (old-ctx (key term)) offset ))
   )))
));

context::get-bindings := λ ctx . (match ctx (
   ()
   ( (Context( bindings _ )) bindings )
));

context::get-offset := λ ctx . (match ctx (
   ()
   ( (Context( _ offset )) offset )
));

context::set-offset := λ ctx offset . (match ctx (
   ()
   ( (Context( bindings _ )) (Context( bindings offset )) )
));