-
Notifications
You must be signed in to change notification settings - Fork 237
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Browse files
Browse the repository at this point in the history
- Loading branch information
Showing
4 changed files
with
91 additions
and
3 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| module Bug2894 | ||
|
|
||
| #set-options "--warn_error -328" // unused let rec | ||
|
|
||
| type comparator_for (t:Type) = x:t -> y:t -> int | ||
|
|
||
| val term_eq : comparator_for int | ||
| let rec term_eq t1 t2 = 0 | ||
|
|
||
| let t = term_eq |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,41 @@ | ||
| module Bug2895 | ||
|
|
||
| // let rec not used | ||
| #set-options "--warn_error -328" | ||
|
|
||
| (* Recursive functions must be literals, but the annotated type | ||
| can be an _abbreviation_ of an arrow type, as in the examples that | ||
| follow. See issue #2895. *) | ||
|
|
||
| type foo (t:Type) = t -> bool | ||
| val f : foo string | ||
| let rec f (u : string) : bool = false | ||
| let test = f "123" | ||
|
|
||
| (* From the issue *) | ||
| type comparator_for (t:Type) = t -> t -> bool | ||
| val univ_eq : comparator_for int | ||
| let rec univ_eq (u1 u2 : int) : bool = false | ||
|
|
||
| (* A more involved variant, that could fail to extract due to coercions. | ||
| *) | ||
|
|
||
| type cmpres #t (x y : t) = bool | ||
| type comparator_for' (t:Type) = x:t -> y:t -> cmpres x y | ||
|
|
||
| let string_eq : comparator_for' string = fun x y -> x = y | ||
| let bool_eq : comparator_for' bool = fun x y -> x = y | ||
|
|
||
| type sb = | S of string | B of bool | ||
| val sb_eq : comparator_for' sb | ||
|
|
||
| (* The body of this function gets a coercion, as the branches | ||
| are of seemingly different types (due to the refinement). Extraction | ||
| must make sure to push that coercion in, or we otherwise define | ||
| an ocaml let rec where the body is an Obj.magic call (and not | ||
| a literal fun), which fails to compile. *) | ||
| let rec sb_eq (sb1 sb2 : sb) : cmpres sb1 sb2 = | ||
| match sb1, sb2 with | ||
| | S s1, S s2 -> string_eq s1 s2 | ||
| | B b1, B b2 -> bool_eq b1 b2 | ||
| | _ -> false |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,29 @@ | ||
| open Prims | ||
| type 't foo = 't -> Prims.bool | ||
| let rec (f : Prims.string foo) = fun u -> false | ||
| let (test : Prims.bool) = f "123" | ||
| type 't comparator_for = 't -> 't -> Prims.bool | ||
| let rec (univ_eq : Prims.int comparator_for) = fun u1 -> fun u2 -> false | ||
| type ('t, 'x, 'y) cmpres = Prims.bool | ||
| type 't comparator_for' = 't -> 't -> ('t, unit, unit) cmpres | ||
| let (string_eq : Prims.string comparator_for') = fun x -> fun y -> x = y | ||
| let (bool_eq : Prims.bool comparator_for') = fun x -> fun y -> x = y | ||
| type sb = | ||
| | S of Prims.string | ||
| | B of Prims.bool | ||
| let (uu___is_S : sb -> Prims.bool) = | ||
| fun projectee -> match projectee with | S _0 -> true | uu___ -> false | ||
| let (__proj__S__item___0 : sb -> Prims.string) = | ||
| fun projectee -> match projectee with | S _0 -> _0 | ||
| let (uu___is_B : sb -> Prims.bool) = | ||
| fun projectee -> match projectee with | B _0 -> true | uu___ -> false | ||
| let (__proj__B__item___0 : sb -> Prims.bool) = | ||
| fun projectee -> match projectee with | B _0 -> _0 | ||
| let rec (sb_eq : sb comparator_for') = | ||
| Obj.magic | ||
| (fun sb1 -> | ||
| fun sb2 -> | ||
| match (sb1, sb2) with | ||
| | (S s1, S s2) -> Obj.repr (string_eq s1 s2) | ||
| | (B b1, B b2) -> Obj.repr (bool_eq b1 b2) | ||
| | uu___ -> Obj.repr false) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters