Commit ff949144 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

subtype checking doesn't fail

parent 9c8cd47c
......@@ -20,3 +20,10 @@ type Nat ::= [ iszero : Bool ;
let 0 : Nat ::= [ iszero = ς(x : Nat) true ;
pred = ς(x : Nat) x.pred ].
type RomCell ::= [ get : Nat ].
type PromCell ::= [ get : Nat ; set : Nat -> RomCell ].
let myCell : PromCell ::= [ get = ς( self : PromCell ) 0 ;
set = ς( self : PromCell ) λ(n : Nat) self.get := n ].
......@@ -22,6 +22,7 @@ type tline =
type typed_tree = tline list
exception Sty_assoc_arrow
let rec sty_assoc l = function
| Stcid (_, b) -> sty_assoc l b
| Stlist ll -> List.assoc l ll
......@@ -39,7 +40,10 @@ let rec subtype (a : sty) : sty -> bool = function
| Starr (a1, a2) -> eq a1 b1 && eq a2 b2
| _ -> false)
| Stlist [] -> true
| Stlist ((l, bl) :: b) -> eq bl (sty_assoc l a) && subtype a (Stlist b)
| Stlist ((l, bl) :: b) ->
try
eq bl (sty_assoc l a) && subtype a (Stlist b)
with Not_found -> false
and eq a b = subtype a b && subtype b a
let rec infer : tterm -> sty = function
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment