From a6585b6e9197d109cd59665c52643cc4a64628eb Mon Sep 17 00:00:00 2001 From: Your Name Date: Tue, 5 Mar 2019 21:00:44 +0100 Subject: [PATCH] Revert "Does not work" This reverts commit cbf565d4c07407d156e0e7f5cf77dc5240a836eb. --- AST.mli | 16 ++++++++++++---- Typecheck2.ml | 5 ++++- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/AST.mli b/AST.mli index 2f9610e89..d89d92b25 100644 --- a/AST.mli +++ b/AST.mli @@ -161,7 +161,8 @@ type ('a, 'type_expr_typecheck) gadt_if = sufficient. *) type 'x x_sig = 'x -constraint 'x = 'type_annotation * 'type_expr_typecheck +constraint 'x = < annot: 'type_annotation; + type_expr_typecheck: 'bool1 > type 'x ast = { types : 'x type_decl reg list; @@ -220,7 +221,8 @@ and 'x type_expr = | Function of (('x type_expr list) * 'x type_expr, 'type_expr_typecheck) gadt_if | Mutable of ('x type_expr, 'type_expr_typecheck) gadt_if | Unit of (unit, 'type_expr_typecheck) gadt_if -constraint 'x = ('type_annotation * 'type_expr_typecheck) +constraint 'x = < type_expr_typecheck: 'type_expr_typecheck; + .. > constraint 'x = 'x x_sig and 'x cartesian = ('x type_expr, times) nsepseq reg @@ -503,9 +505,15 @@ constraint 'x = 'x x_sig (* Variations on the AST *) -type parse_phase = (unit * tfalse) +type parse_phase = < + annot: unit; + type_expr_typecheck: tfalse; +> -type typecheck_phase = (parse_phase type_expr * ttrue) +type typecheck_phase = < + annot: typecheck_phase type_expr; + type_expr_typecheck: ttrue; +> type t = parse_phase ast diff --git a/Typecheck2.ml b/Typecheck2.ml index 058a25cbf..ae5d9bdb3 100644 --- a/Typecheck2.ml +++ b/Typecheck2.ml @@ -3,7 +3,10 @@ module SMap = Map.Make(String) open AST type i = parse_phase -type typecheck_phase = (parse_phase type_expr * tfalse) +type typecheck_phase = < + annot: typecheck_phase type_expr; + type_expr_typecheck: tfalse; +> type o = typecheck_phase type te = o type_expr list SMap.t (* Type environment *)