diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index 70c5bc1635d..ee9b4b36c5e 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -374,9 +374,14 @@ let (op_as_term : FStar_Syntax_Syntax.delta_equational | "@" -> ((let uu___3 = FStar_Ident.range_of_id op in - FStar_Errors.log_issue uu___3 - (FStar_Errors_Codes.Warning_DeprecatedGeneric, - "The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'")); + let uu___4 = + let uu___5 = + let uu___6 = + FStar_Errors_Msg.text + "The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'." in + [uu___6] in + (FStar_Errors_Codes.Warning_DeprecatedGeneric, uu___5) in + FStar_Errors.log_issue_doc uu___3 uu___4); r FStar_Parser_Const.list_tot_append_lid (FStar_Syntax_Syntax.Delta_equational_at_level (Prims.of_int (2)))) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml index 3ce3db5a5aa..bfeaa3b68b4 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml @@ -402,7 +402,24 @@ let (__proj__Mkcontext__item__error_context : fun projectee -> match projectee with | { no_guard; error_context;_} -> error_context let (showable_context : context FStar_Class_Show.showable) = - { FStar_Class_Show.show = (fun uu___ -> "") } + { + FStar_Class_Show.show = + (fun context1 -> + let uu___ = + FStar_Class_Show.show + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_bool) context1.no_guard in + let uu___1 = + let uu___2 = + FStar_Compiler_List.map FStar_Pervasives_Native.fst + context1.error_context in + FStar_Class_Show.show + (FStar_Class_Show.show_list + (FStar_Class_Show.printableshow + FStar_Class_Printable.printable_string)) uu___2 in + FStar_Compiler_Util.format2 "{no_guard=%s, error_context=%s}" uu___ + uu___1) + } let (print_context : context -> Prims.string) = fun ctx -> let rec aux depth ctx1 = @@ -428,7 +445,33 @@ let (print_error : error -> Prims.string) = FStar_Compiler_Util.format2 "%s%s" uu___1 msg let (print_error_short : error -> Prims.string) = fun err -> FStar_Pervasives_Native.snd err -type 'a result = context -> ('a success, error) FStar_Pervasives.either +type 'a __result = + | Success of 'a + | Error of error +let uu___is_Success : 'a . 'a __result -> Prims.bool = + fun projectee -> match projectee with | Success _0 -> true | uu___ -> false +let __proj__Success__item___0 : 'a . 'a __result -> 'a = + fun projectee -> match projectee with | Success _0 -> _0 +let uu___is_Error : 'a . 'a __result -> Prims.bool = + fun projectee -> match projectee with | Error _0 -> true | uu___ -> false +let __proj__Error__item___0 : 'a . 'a __result -> error = + fun projectee -> match projectee with | Error _0 -> _0 +let showable_result : + 'a . 'a FStar_Class_Show.showable -> 'a __result FStar_Class_Show.showable + = + fun uu___ -> + { + FStar_Class_Show.show = + (fun uu___1 -> + match uu___1 with + | Success a1 -> + let uu___2 = FStar_Class_Show.show uu___ a1 in + Prims.strcat "Success " uu___2 + | Error e -> + let uu___2 = print_error_short e in + Prims.strcat "Error " uu___2) + } +type 'a result = context -> 'a success __result type hash_entry = { he_term: FStar_Syntax_Syntax.term ; @@ -521,8 +564,7 @@ let (insert : } in FStar_Syntax_TermHashTable.insert e entry table let return : 'a . 'a -> 'a result = - fun x -> - fun uu___ -> FStar_Pervasives.Inl (x, FStar_Pervasives_Native.None) + fun x -> fun uu___ -> Success (x, FStar_Pervasives_Native.None) let (and_pre : precondition -> precondition -> @@ -548,45 +590,44 @@ let op_let_Bang : 'a 'b . 'a result -> ('a -> 'b result) -> 'b result = fun ctx0 -> let uu___ = x ctx0 in match uu___ with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___1 = let uu___2 = y x1 in uu___2 ctx0 in (match uu___1 with - | FStar_Pervasives.Inl (y1, g2) -> + | Success (y1, g2) -> let uu___2 = let uu___3 = and_pre g1 g2 in (y1, uu___3) in - FStar_Pervasives.Inl uu___2 + Success uu___2 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> Error err let op_and_Bang : 'a 'b . 'a result -> 'b result -> ('a * 'b) result = fun x -> fun y -> fun ctx0 -> let uu___ = x ctx0 in match uu___ with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___1 = let uu___2 ctx01 = let uu___3 = y ctx01 in match uu___3 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___4 = let uu___5 uu___6 = - FStar_Pervasives.Inl - ((x1, x2), FStar_Pervasives_Native.None) in + Success ((x1, x2), FStar_Pervasives_Native.None) in uu___5 ctx01 in (match uu___4 with - | FStar_Pervasives.Inl (y1, g2) -> + | Success (y1, g2) -> let uu___5 = let uu___6 = and_pre g11 g2 in (y1, uu___6) in - FStar_Pervasives.Inl uu___5 + Success uu___5 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + | Error err -> Error err in uu___2 ctx0 in (match uu___1 with - | FStar_Pervasives.Inl (y1, g2) -> + | Success (y1, g2) -> let uu___2 = let uu___3 = and_pre g1 g2 in (y1, uu___3) in - FStar_Pervasives.Inl uu___2 + Success uu___2 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> Error err let op_let_Question : 'a 'b . 'a FStar_Pervasives_Native.option -> @@ -599,13 +640,12 @@ let op_let_Question : | FStar_Pervasives_Native.None -> FStar_Pervasives_Native.None | FStar_Pervasives_Native.Some x1 -> f x1 let fail : 'a . Prims.string -> 'a result = - fun msg -> fun ctx -> FStar_Pervasives.Inr (ctx, msg) + fun msg -> fun ctx -> Error (ctx, msg) let (dump_context : unit result) = fun ctx -> (let uu___1 = print_context ctx in FStar_Compiler_Util.print_string uu___1); - (let uu___1 uu___2 = - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None) in + (let uu___1 uu___2 = Success ((), FStar_Pervasives_Native.None) in uu___1 ctx) let handle_with : 'a . 'a result -> (unit -> 'a result) -> 'a result = fun x -> @@ -613,7 +653,7 @@ let handle_with : 'a . 'a result -> (unit -> 'a result) -> 'a result = fun ctx -> let uu___ = x ctx in match uu___ with - | FStar_Pervasives.Inr uu___1 -> let uu___2 = h () in uu___2 ctx + | Error uu___1 -> let uu___2 = h () in uu___2 ctx | res -> res let with_context : 'a . @@ -648,8 +688,7 @@ let (is_type : uu___1.FStar_Syntax_Syntax.n in match uu___ with | FStar_Syntax_Syntax.Tm_type u -> - (fun uu___1 -> - FStar_Pervasives.Inl (u, FStar_Pervasives_Native.None)) + (fun uu___1 -> Success (u, FStar_Pervasives_Native.None)) | uu___1 -> let uu___2 = let uu___3 = FStar_Syntax_Print.term_to_string t1 in @@ -668,7 +707,7 @@ let (is_type : fun ctx2 -> let uu___2 = uu___1 ctx2 in match uu___2 with - | FStar_Pervasives.Inr uu___3 -> + | Error uu___3 -> let uu___4 = let uu___5 = let uu___6 = @@ -705,7 +744,7 @@ let rec (is_arrow : let uu___3 = FStar_Syntax_Util.is_total_comp c1 in if uu___3 then E_Total else E_Ghost in (fun uu___3 -> - FStar_Pervasives.Inl + Success ((x1, eff, (FStar_Syntax_Util.comp_result c1)), FStar_Pervasives_Native.None))) else @@ -785,7 +824,7 @@ let rec (is_arrow : (x1.FStar_Syntax_Syntax.binder_attrs) } in (fun uu___8 -> - FStar_Pervasives.Inl + Success ((x2, e_tag1, res_typ), FStar_Pervasives_Native.None))))) | FStar_Syntax_Syntax.Tm_arrow @@ -803,8 +842,7 @@ let rec (is_arrow : (match uu___1 with | (g1, x1, t3) -> (fun uu___2 -> - FStar_Pervasives.Inl - ((x1, E_Total, t3), FStar_Pervasives_Native.None))) + Success ((x1, E_Total, t3), FStar_Pervasives_Native.None))) | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = uu___1;_} -> is_arrow g x.FStar_Syntax_Syntax.sort @@ -835,7 +873,7 @@ let rec (is_arrow : fun ctx2 -> let uu___2 = uu___1 ctx2 in match uu___2 with - | FStar_Pervasives.Inr uu___3 -> + | Error uu___3 -> let uu___4 = let uu___5 = FStar_TypeChecker_Normalize.unfold_whnf g.tcenv t in @@ -853,18 +891,14 @@ let (check_arg_qual : | FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.aqual_implicit = true; FStar_Syntax_Syntax.aqual_attributes = uu___1;_} - -> - (fun uu___2 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + -> (fun uu___2 -> Success ((), FStar_Pervasives_Native.None)) | uu___1 -> fail "missing arg qualifier implicit") | FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta uu___) -> (match a with | FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.aqual_implicit = true; FStar_Syntax_Syntax.aqual_attributes = uu___1;_} - -> - (fun uu___2 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + -> (fun uu___2 -> Success ((), FStar_Pervasives_Native.None)) | uu___1 -> fail "missing arg qualifier implicit") | uu___ -> (match a with @@ -873,31 +907,25 @@ let (check_arg_qual : FStar_Syntax_Syntax.aqual_attributes = uu___1;_} -> fail "extra arg qualifier implicit" | uu___1 -> - (fun uu___2 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None))) + (fun uu___2 -> Success ((), FStar_Pervasives_Native.None))) let (check_bqual : FStar_Syntax_Syntax.bqual -> FStar_Syntax_Syntax.bqual -> unit result) = fun b0 -> fun b1 -> match (b0, b1) with | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None) -> - (fun uu___ -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + (fun uu___ -> Success ((), FStar_Pervasives_Native.None)) | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit b01), FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Implicit b11)) -> - (fun uu___ -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + (fun uu___ -> Success ((), FStar_Pervasives_Native.None)) | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Equality), FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Equality)) -> - (fun uu___ -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + (fun uu___ -> Success ((), FStar_Pervasives_Native.None)) | (FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta t1), FStar_Pervasives_Native.Some (FStar_Syntax_Syntax.Meta t2)) -> let uu___ = equal_term t1 t2 in if uu___ - then - (fun uu___1 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + then (fun uu___1 -> Success ((), FStar_Pervasives_Native.None)) else fail "Binder qualifier mismatch" | uu___ -> fail "Binder qualifier mismatch" let (check_aqual : @@ -906,8 +934,7 @@ let (check_aqual : fun a1 -> match (a0, a1) with | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None) -> - (fun uu___ -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + (fun uu___ -> Success ((), FStar_Pervasives_Native.None)) | (FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.aqual_implicit = b0; FStar_Syntax_Syntax.aqual_attributes = uu___;_}, @@ -916,9 +943,7 @@ let (check_aqual : FStar_Syntax_Syntax.aqual_attributes = uu___1;_}) -> if b0 = b1 - then - (fun uu___2 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + then (fun uu___2 -> Success ((), FStar_Pervasives_Native.None)) else (let uu___3 = let uu___4 = FStar_Compiler_Util.string_of_bool b0 in @@ -930,15 +955,12 @@ let (check_aqual : | (FStar_Pervasives_Native.None, FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.aqual_implicit = false; FStar_Syntax_Syntax.aqual_attributes = uu___;_}) - -> - (fun uu___1 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + -> (fun uu___1 -> Success ((), FStar_Pervasives_Native.None)) | (FStar_Pervasives_Native.Some { FStar_Syntax_Syntax.aqual_implicit = false; FStar_Syntax_Syntax.aqual_attributes = uu___;_}, FStar_Pervasives_Native.None) -> - (fun uu___1 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + (fun uu___1 -> Success ((), FStar_Pervasives_Native.None)) | uu___ -> let uu___1 = let uu___2 = FStar_Syntax_Print.aqual_to_string a0 in @@ -960,9 +982,7 @@ let (check_positivity_qual : FStar_TypeChecker_Common.check_positivity_qual (uu___is_SUBTYPING rel) p0 p1 in if uu___ - then - fun uu___1 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None) + then fun uu___1 -> Success ((), FStar_Pervasives_Native.None) else fail "Unequal positivity qualifiers" let (mk_forall_l : FStar_Syntax_Syntax.universes -> @@ -1026,9 +1046,9 @@ let with_binders : fun ctx -> let uu___ = f ctx in match uu___ with - | FStar_Pervasives.Inl (t, g) -> + | Success (t, g) -> let uu___1 = let uu___2 = close_guard xs us g in (t, uu___2) in - FStar_Pervasives.Inl uu___1 + Success uu___1 | err -> err let with_definition : 'a . @@ -1043,15 +1063,14 @@ let with_definition : fun ctx -> let uu___ = f ctx in match uu___ with - | FStar_Pervasives.Inl (a1, g) -> + | Success (a1, g) -> let uu___1 = let uu___2 = close_guard_with_definition x u t g in (a1, uu___2) in - FStar_Pervasives.Inl uu___1 + Success uu___1 | err -> err let (guard : FStar_Syntax_Syntax.typ -> unit result) = - fun t -> - fun uu___ -> FStar_Pervasives.Inl ((), (FStar_Pervasives_Native.Some t)) + fun t -> fun uu___ -> Success ((), (FStar_Pervasives_Native.Some t)) let (abs : FStar_Syntax_Syntax.typ -> (FStar_Syntax_Syntax.binder -> FStar_Syntax_Syntax.term) -> @@ -1080,23 +1099,22 @@ let (strengthen_subtyping_guard : FStar_Pervasives_Native.Some uu___ let weaken : 'a . - FStar_Syntax_Syntax.term -> - 'a result -> context -> ('a success, error) FStar_Pervasives.either + FStar_Syntax_Syntax.term -> 'a result -> context -> 'a success __result = fun p -> fun g -> fun ctx -> let uu___ = g ctx in match uu___ with - | FStar_Pervasives.Inl (x, q) -> + | Success (x, q) -> let uu___1 = let uu___2 = weaken_subtyping_guard p q in (x, uu___2) in - FStar_Pervasives.Inl uu___1 + Success uu___1 | err -> err let weaken_with_guard_formula : 'a . FStar_TypeChecker_Common.guard_formula -> - 'a result -> context -> ('a success, error) FStar_Pervasives.either + 'a result -> context -> 'a success __result = fun p -> fun g -> @@ -1113,27 +1131,26 @@ let (push_hypothesis : env -> FStar_Syntax_Syntax.term -> env) = let uu___ = fresh_binder g b in FStar_Pervasives_Native.fst uu___ let strengthen : 'a . - FStar_Syntax_Syntax.term -> - 'a result -> context -> ('a success, error) FStar_Pervasives.either + FStar_Syntax_Syntax.term -> 'a result -> context -> 'a success __result = fun p -> fun g -> fun ctx -> let uu___ = g ctx in match uu___ with - | FStar_Pervasives.Inl (x, q) -> + | Success (x, q) -> let uu___1 = let uu___2 = strengthen_subtyping_guard p q in (x, uu___2) in - FStar_Pervasives.Inl uu___1 + Success uu___1 | err -> err let no_guard : 'a . 'a result -> 'a result = fun g -> fun ctx -> let uu___ = g { no_guard = true; error_context = (ctx.error_context) } in match uu___ with - | FStar_Pervasives.Inl (x, FStar_Pervasives_Native.None) -> - FStar_Pervasives.Inl (x, FStar_Pervasives_Native.None) - | FStar_Pervasives.Inl (x, FStar_Pervasives_Native.Some g1) -> + | Success (x, FStar_Pervasives_Native.None) -> + Success (x, FStar_Pervasives_Native.None) + | Success (x, FStar_Pervasives_Native.Some g1) -> let uu___1 = let uu___2 = let uu___3 = FStar_Syntax_Print.term_to_string g1 in @@ -1289,9 +1306,7 @@ let (lookup : context_included he.he_gamma (g.tcenv).FStar_TypeChecker_Env.gamma in if uu___1 - then - (record_cache_hit (); - (fun uu___3 -> FStar_Pervasives.Inl (he.he_res))) + then (record_cache_hit (); (fun uu___3 -> Success (he.he_res))) else fail "not in cache" let (check_no_escape : FStar_Syntax_Syntax.binders -> FStar_Syntax_Syntax.term -> unit result) = @@ -1306,49 +1321,46 @@ let (check_no_escape : b.FStar_Syntax_Syntax.binder_bv xs in Prims.op_Negation uu___1) bs in if uu___ - then - fun uu___1 -> FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None) + then fun uu___1 -> Success ((), FStar_Pervasives_Native.None) else fail "Name escapes its scope" let rec map : 'a 'b . ('a -> 'b result) -> 'a Prims.list -> 'b Prims.list result = fun f -> fun l -> match l with - | [] -> - (fun uu___ -> - FStar_Pervasives.Inl ([], FStar_Pervasives_Native.None)) + | [] -> (fun uu___ -> Success ([], FStar_Pervasives_Native.None)) | hd::tl -> let uu___ = f hd in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = let uu___4 = map f tl in fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 uu___8 = - FStar_Pervasives.Inl + Success ((x :: x1), FStar_Pervasives_Native.None) in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + | Error err -> Error err in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) let mapi : 'a 'b . (Prims.int -> 'a -> 'b result) -> 'a Prims.list -> 'b Prims.list result @@ -1357,44 +1369,41 @@ let mapi : fun l -> let rec aux i l1 = match l1 with - | [] -> - (fun uu___ -> - FStar_Pervasives.Inl ([], FStar_Pervasives_Native.None)) + | [] -> (fun uu___ -> Success ([], FStar_Pervasives_Native.None)) | hd::tl -> let uu___ = f i hd in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = let uu___4 = aux (i + Prims.int_one) tl in fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 uu___8 = - FStar_Pervasives.Inl + Success ((x :: x1), FStar_Pervasives_Native.None) in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) in + | Error err -> Error err) in aux Prims.int_zero l let rec map2 : 'a 'b 'c . @@ -1406,66 +1415,62 @@ let rec map2 : fun l2 -> match (l1, l2) with | ([], []) -> - (fun uu___ -> - FStar_Pervasives.Inl ([], FStar_Pervasives_Native.None)) + (fun uu___ -> Success ([], FStar_Pervasives_Native.None)) | (hd1::tl1, hd2::tl2) -> let uu___ = f hd1 hd2 in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = let uu___4 = map2 f tl1 tl2 in fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 uu___8 = - FStar_Pervasives.Inl + Success ((x :: x1), FStar_Pervasives_Native.None) in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) let rec fold : 'a 'b . ('a -> 'b -> 'a result) -> 'a -> 'b Prims.list -> 'a result = fun f -> fun x -> fun l -> match l with - | [] -> - (fun uu___ -> - FStar_Pervasives.Inl (x, FStar_Pervasives_Native.None)) + | [] -> (fun uu___ -> Success (x, FStar_Pervasives_Native.None)) | hd::tl -> let uu___ = f x hd in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___2 = let uu___3 = fold f x1 tl in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) let rec fold2 : 'a 'b 'c . ('a -> 'b -> 'c -> 'a result) -> @@ -1477,23 +1482,22 @@ let rec fold2 : fun l2 -> match (l1, l2) with | ([], []) -> - (fun uu___ -> - FStar_Pervasives.Inl (x, FStar_Pervasives_Native.None)) + (fun uu___ -> Success (x, FStar_Pervasives_Native.None)) | (hd1::tl1, hd2::tl2) -> let uu___ = f x hd1 hd2 in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___2 = let uu___3 = fold2 f x1 tl1 tl2 in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) let rec iter2 : 'a 'b . 'a Prims.list -> @@ -1505,23 +1509,22 @@ let rec iter2 : fun b1 -> match (xs, ys) with | ([], []) -> - (fun uu___ -> - FStar_Pervasives.Inl (b1, FStar_Pervasives_Native.None)) + (fun uu___ -> Success (b1, FStar_Pervasives_Native.None)) | (x::xs1, y::ys1) -> let uu___ = f x y b1 in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___2 = let uu___3 = iter2 xs1 ys1 f x1 in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y1, g2) -> + | Success (y1, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y1, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | uu___ -> fail "Lists of differing length" let (is_non_informative : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> Prims.bool) = @@ -1567,17 +1570,7 @@ let (join_eff : tot_or_ghost -> tot_or_ghost -> tot_or_ghost) = let (join_eff_l : tot_or_ghost Prims.list -> tot_or_ghost) = fun es -> FStar_List_Tot_Base.fold_right join_eff es E_Total let (guard_not_allowed : Prims.bool result) = - fun ctx -> - FStar_Pervasives.Inl ((ctx.no_guard), FStar_Pervasives_Native.None) -let (default_norm_steps : FStar_TypeChecker_Env.steps) = - [FStar_TypeChecker_Env.Primops; - FStar_TypeChecker_Env.Weak; - FStar_TypeChecker_Env.HNF; - FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant; - FStar_TypeChecker_Env.Unascribe; - FStar_TypeChecker_Env.Eager_unfolding; - FStar_TypeChecker_Env.Iota; - FStar_TypeChecker_Env.Exclude FStar_TypeChecker_Env.Zeta] + fun ctx -> Success ((ctx.no_guard), FStar_Pervasives_Native.None) let (debug : env -> (unit -> unit) -> unit) = fun g -> fun f -> @@ -1723,7 +1716,7 @@ let rec (check_relation : (fun ctx0 -> let uu___1 = guard_not_allowed ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = let guard_ok = Prims.op_Negation x in @@ -1808,7 +1801,7 @@ let rec (check_relation : fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 = match x1 with @@ -1817,7 +1810,7 @@ let rec (check_relation : (fun ctx02 -> let uu___10 = uu___9 ctx02 in match uu___10 with - | FStar_Pervasives.Inl (x2, g12) -> + | Success (x2, g12) -> let uu___11 = let uu___12 = let uu___13 = @@ -1826,26 +1819,23 @@ let rec (check_relation : guard uu___13 in uu___12 ctx02 in (match uu___11 with - | FStar_Pervasives.Inl (y, g2) - -> + | Success (y, g2) -> let uu___12 = let uu___13 = and_pre g12 g2 in ((), uu___13) in - FStar_Pervasives.Inl uu___12 + Success uu___12 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1) in + | Error err1 -> Error err1) in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in ((), uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in let fallback t01 t11 = if guard_ok then @@ -1895,11 +1885,15 @@ let rec (check_relation : FStar_Pervasives_Native.None "FStar.TypeChecker.Core.beta_iota_reduce" in let t01 = - let uu___4 = beta_iota_reduce1 t0 in - FStar_Syntax_Subst.compress uu___4 in + let uu___4 = + let uu___5 = beta_iota_reduce1 t0 in + FStar_Syntax_Subst.compress uu___5 in + FStar_Syntax_Util.unlazy_emb uu___4 in let t11 = - let uu___4 = beta_iota_reduce1 t1 in - FStar_Syntax_Subst.compress uu___4 in + let uu___4 = + let uu___5 = beta_iota_reduce1 t1 in + FStar_Syntax_Subst.compress uu___5 in + FStar_Syntax_Util.unlazy_emb uu___4 in let check_relation1 g2 rel1 t02 t12 ctx = let ctx1 = { @@ -1916,8 +1910,7 @@ let rec (check_relation : if uu___4 then fun uu___5 -> - FStar_Pervasives.Inl - ((), FStar_Pervasives_Native.None) + Success ((), FStar_Pervasives_Native.None) else (match ((t01.FStar_Syntax_Syntax.n), (t11.FStar_Syntax_Syntax.n)) @@ -1930,8 +1923,7 @@ let rec (check_relation : if uu___6 then (fun uu___7 -> - FStar_Pervasives.Inl - ((), FStar_Pervasives_Native.None)) + Success ((), FStar_Pervasives_Native.None)) else err () | (FStar_Syntax_Syntax.Tm_meta { FStar_Syntax_Syntax.tm2 = t02; @@ -1994,8 +1986,7 @@ let rec (check_relation : (if uu___7 then fun uu___8 -> - FStar_Pervasives.Inl - ((), FStar_Pervasives_Native.None) + Success ((), FStar_Pervasives_Native.None) else err ()) else maybe_unfold_and_retry t01 t11 | (FStar_Syntax_Syntax.Tm_fvar uu___6, @@ -2020,7 +2011,7 @@ let rec (check_relation : (fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___9 = let uu___10 = let uu___11 = @@ -2029,8 +2020,7 @@ let rec (check_relation : fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl (x3, g12) - -> + | Success (x3, g12) -> let uu___13 = let uu___14 = let uu___15 = @@ -2051,8 +2041,8 @@ let rec (check_relation : guard_not_allowed ctx03 in match uu___16 with - | FStar_Pervasives.Inl - (x4, g13) -> + | Success (x4, g13) + -> let uu___17 = let uu___18 = if x4 @@ -2091,7 +2081,7 @@ let rec (check_relation : match uu___22 with | - FStar_Pervasives.Inr + Error uu___23 -> let uu___24 @@ -2148,7 +2138,7 @@ let rec (check_relation : uu___18 ctx03 in (match uu___17 with - | FStar_Pervasives.Inl + | Success (y, g21) -> let uu___18 @@ -2159,36 +2149,30 @@ let rec (check_relation : g13 g21 in ((), uu___19) in - FStar_Pervasives.Inl + Success uu___18 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1) in + | Error err1 -> + Error err1) in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in ((), uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in ((), uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1) + | Error err1 -> Error err1) else (let uu___8 = maybe_unfold x0.FStar_Syntax_Syntax.sort @@ -2280,7 +2264,7 @@ let rec (check_relation : (fun ctx01 -> let uu___9 = uu___8 ctx01 in match uu___9 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___10 = let uu___11 = let uu___12 = @@ -2289,8 +2273,7 @@ let rec (check_relation : fun ctx02 -> let uu___13 = uu___12 ctx02 in match uu___13 with - | FStar_Pervasives.Inl (x3, g12) - -> + | Success (x3, g12) -> let uu___14 = let uu___15 = let uu___16 = @@ -2305,8 +2288,8 @@ let rec (check_relation : guard_not_allowed ctx03 in match uu___17 with - | FStar_Pervasives.Inl - (x4, g13) -> + | Success (x4, g13) + -> let uu___18 = let uu___19 = if x4 @@ -2347,7 +2330,7 @@ let rec (check_relation : match uu___23 with | - FStar_Pervasives.Inr + Error uu___24 -> let uu___25 @@ -2390,7 +2373,7 @@ let rec (check_relation : uu___19 ctx03 in (match uu___18 with - | FStar_Pervasives.Inl + | Success (y, g21) -> let uu___19 @@ -2401,36 +2384,30 @@ let rec (check_relation : g13 g21 in ((), uu___20) in - FStar_Pervasives.Inl + Success uu___19 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1) in + | Error err1 -> + Error err1) in uu___15 ctx02 in (match uu___14 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___15 = let uu___16 = and_pre g12 g2 in ((), uu___16) in - FStar_Pervasives.Inl - uu___15 + Success uu___15 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___11 ctx01 in (match uu___10 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___11 = let uu___12 = and_pre g11 g2 in ((), uu___12) in - FStar_Pervasives.Inl uu___11 + Success uu___11 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1) + | Error err1 -> Error err1) else (let uu___9 = maybe_unfold t01 x1.FStar_Syntax_Syntax.sort in @@ -2485,30 +2462,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2527,8 +2499,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2563,30 +2534,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2605,8 +2571,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2641,30 +2606,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2683,8 +2643,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2719,30 +2678,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2761,8 +2715,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2797,30 +2750,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2839,8 +2787,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2875,30 +2822,25 @@ let rec (check_relation : fun ctx01 -> let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___15 = let uu___16 = check_relation_args g EQUALITY args0 args1 in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___16 = let uu___17 = and_pre g11 g2 in ((), uu___17) in - FStar_Pervasives.Inl - uu___16 + Success uu___16 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = maybe_unfold_side_and_retry Both t01 t11 in @@ -2917,8 +2859,7 @@ let rec (check_relation : fun ctx -> let uu___13 = uu___12 ctx in match uu___13 with - | FStar_Pervasives.Inr uu___14 - -> + | Error uu___14 -> let uu___15 = emit_guard t01 t11 in uu___15 ctx @@ -2954,7 +2895,7 @@ let rec (check_relation : (fun ctx01 -> let uu___9 = uu___8 ctx01 in match uu___9 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___10 = let uu___11 = let uu___12 = @@ -2964,7 +2905,7 @@ let rec (check_relation : fun ctx02 -> let uu___13 = uu___12 ctx02 in match uu___13 with - | FStar_Pervasives.Inl (x2, g12) -> + | Success (x2, g12) -> let uu___14 = let uu___15 = let uu___16 = @@ -2976,8 +2917,7 @@ let rec (check_relation : let uu___17 = uu___16 ctx03 in match uu___17 with - | FStar_Pervasives.Inl - (x3, g13) -> + | Success (x3, g13) -> let uu___18 = let uu___19 = let uu___20 = @@ -2988,7 +2928,7 @@ let rec (check_relation : uu___20 ctx04 in match uu___21 with - | FStar_Pervasives.Inl + | Success (x4, g14) -> let uu___22 = @@ -3028,7 +2968,7 @@ let rec (check_relation : ctx04 in (match uu___22 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___23 @@ -3039,53 +2979,42 @@ let rec (check_relation : g14 g2 in ((), uu___24) in - FStar_Pervasives.Inl + Success uu___23 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1 in + | Error err1 -> + Error err1 in uu___19 ctx03 in (match uu___18 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___19 = let uu___20 = and_pre g13 g2 in ((), uu___20) in - FStar_Pervasives.Inl - uu___19 + Success uu___19 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1 in + | Error err1 -> Error err1 in uu___15 ctx02 in (match uu___14 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___15 = let uu___16 = and_pre g12 g2 in ((), uu___16) in - FStar_Pervasives.Inl - uu___15 + Success uu___15 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___11 ctx01 in (match uu___10 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___11 = let uu___12 = and_pre g11 g2 in ((), uu___12) in - FStar_Pervasives.Inl uu___11 + Success uu___11 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1) + | Error err1 -> Error err1) | (FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = x0::x1::xs; FStar_Syntax_Syntax.comp = c0;_}, @@ -3122,7 +3051,7 @@ let rec (check_relation : fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___9 = let uu___10 = let uu___11 = @@ -3132,8 +3061,7 @@ let rec (check_relation : fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl (x3, g12) - -> + | Success (x3, g12) -> let uu___13 = let uu___14 = let uu___15 = @@ -3143,8 +3071,7 @@ let rec (check_relation : let uu___16 = uu___15 ctx03 in match uu___16 with - | FStar_Pervasives.Inl - (x4, g13) -> + | Success (x4, g13) -> let uu___17 = let uu___18 = let uu___19 = @@ -3243,7 +3170,7 @@ let rec (check_relation : match uu___22 with | - FStar_Pervasives.Inl + Success (x5, g14) -> let uu___23 @@ -3276,7 +3203,7 @@ let rec (check_relation : (match uu___23 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___24 @@ -3287,15 +3214,15 @@ let rec (check_relation : g14 g2 in ((), uu___25) in - FStar_Pervasives.Inl + Success uu___24 | err1 -> err1) | - FStar_Pervasives.Inr + Error err1 -> - FStar_Pervasives.Inr + Error err1 in with_binders [x11] @@ -3304,7 +3231,7 @@ let rec (check_relation : uu___18 ctx03 in (match uu___17 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___18 = let uu___19 @@ -3313,36 +3240,30 @@ let rec (check_relation : g13 g2 in ((), uu___19) in - FStar_Pervasives.Inl + Success uu___18 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1 in + | Error err1 -> + Error err1 in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in ((), uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in ((), uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___6 ctx1) | (FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = e0; @@ -3391,8 +3312,7 @@ let rec (check_relation : (fun ctx01 -> let uu___19 = uu___18 ctx01 in match uu___19 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___20 = let uu___21 = let uu___22 = @@ -3403,19 +3323,14 @@ let rec (check_relation : uu___22 in uu___21 ctx01 in (match uu___20 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___21 = let uu___22 = and_pre g11 g2 in ((), uu___22) in - FStar_Pervasives.Inl - uu___21 + Success uu___21 | err1 -> err1) - | FStar_Pervasives.Inr err1 - -> - FStar_Pervasives.Inr - err1) + | Error err1 -> Error err1) | uu___17 -> fail "raw_pat_as_exp failed in check_equality match rule")) @@ -3427,35 +3342,34 @@ let rec (check_relation : fun ctx01 -> let uu___12 = uu___11 ctx01 in match uu___12 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___13 = let uu___14 = iter2 brs0 brs1 relate_branch () in uu___14 ctx01 in (match uu___13 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g11 g2 in ((), uu___15) in - FStar_Pervasives.Inl uu___14 + Success uu___14 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in (fun ctx -> let uu___11 = uu___10 ctx in match uu___11 with - | FStar_Pervasives.Inr uu___12 -> + | Error uu___12 -> let uu___13 = fallback t01 t11 in uu___13 ctx | res -> res) | uu___6 -> fallback t01 t11) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in ((), uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> FStar_Pervasives.Inr err1) + | Error err1 -> Error err1) and (check_relation_args : env -> relation -> @@ -3478,19 +3392,18 @@ and (check_relation_args : (fun ctx0 -> let uu___4 = uu___3 ctx0 in match uu___4 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___5 = let uu___6 = check_relation g rel t0 t1 in uu___6 ctx0 in (match uu___5 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___6 = let uu___7 = and_pre g1 g2 in ((), uu___7) in - FStar_Pervasives.Inl uu___6 + Success uu___6 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err)) () + | Error err -> Error err)) () else fail "Unequal number of arguments" and (check_relation_comp : env -> @@ -3523,27 +3436,25 @@ and (check_relation_comp : let uu___3 = FStar_Syntax_Util.eq_comp c0 c1 in uu___3 = FStar_Syntax_Util.Equal in if uu___2 - then - (fun uu___3 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + then (fun uu___3 -> Success ((), FStar_Pervasives_Native.None)) else (let ct_eq res0 args0 res1 args1 = let uu___4 = check_relation g EQUALITY res0 res1 in fun ctx0 -> let uu___5 = uu___4 ctx0 in match uu___5 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___6 = let uu___7 = check_relation_args g EQUALITY args0 args1 in uu___7 ctx0 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g1 g2 in ((), uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + | Error err -> Error err in let uu___4 = FStar_Syntax_Util.comp_eff_name_res_and_args c0 in match uu___4 with | (eff0, res0, args0) -> @@ -3588,27 +3499,25 @@ and (check_relation_comp : let uu___3 = FStar_Syntax_Util.eq_comp c0 c1 in uu___3 = FStar_Syntax_Util.Equal in if uu___2 - then - (fun uu___3 -> - FStar_Pervasives.Inl ((), FStar_Pervasives_Native.None)) + then (fun uu___3 -> Success ((), FStar_Pervasives_Native.None)) else (let ct_eq res0 args0 res1 args1 = let uu___4 = check_relation g EQUALITY res0 res1 in fun ctx0 -> let uu___5 = uu___4 ctx0 in match uu___5 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___6 = let uu___7 = check_relation_args g EQUALITY args0 args1 in uu___7 ctx0 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g1 g2 in ((), uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + | Error err -> Error err in let uu___4 = FStar_Syntax_Util.comp_eff_name_res_and_args c0 in match uu___4 with | (eff0, res0, args0) -> @@ -3664,8 +3573,7 @@ and (check_subtype : env -> FStar_Syntax_Syntax.term FStar_Pervasives_Native.option -> FStar_Syntax_Syntax.typ -> - FStar_Syntax_Syntax.typ -> - context -> (unit success, error) FStar_Pervasives.either) + FStar_Syntax_Syntax.typ -> context -> unit success __result) = fun g -> fun e -> @@ -3700,9 +3608,9 @@ and (memo_check : let check_then_memo g1 e1 ctx = let r = let uu___ = do_check_and_promote g1 e1 in uu___ ctx in match r with - | FStar_Pervasives.Inl (res, FStar_Pervasives_Native.None) -> + | Success (res, FStar_Pervasives_Native.None) -> (insert g1 e1 (res, FStar_Pervasives_Native.None); r) - | FStar_Pervasives.Inl (res, FStar_Pervasives_Native.Some guard1) -> + | Success (res, FStar_Pervasives_Native.Some guard1) -> (match g1.guard_handler with | FStar_Pervasives_Native.None -> (insert g1 e1 (res, (FStar_Pervasives_Native.Some guard1)); @@ -3712,7 +3620,7 @@ and (memo_check : if uu___ then let r1 = (res, FStar_Pervasives_Native.None) in - (insert g1 e1 r1; FStar_Pervasives.Inl r1) + (insert g1 e1 r1; Success r1) else (let uu___2 = fail "guard handler failed" in uu___2 ctx)) | uu___ -> r in @@ -3722,14 +3630,13 @@ and (memo_check : else (let uu___1 = let uu___2 = lookup g e in uu___2 ctx in match uu___1 with - | FStar_Pervasives.Inr uu___2 -> check_then_memo g e ctx - | FStar_Pervasives.Inl (et, FStar_Pervasives_Native.None) -> - FStar_Pervasives.Inl (et, FStar_Pervasives_Native.None) - | FStar_Pervasives.Inl (et, FStar_Pervasives_Native.Some pre) -> + | Error uu___2 -> check_then_memo g e ctx + | Success (et, FStar_Pervasives_Native.None) -> + Success (et, FStar_Pervasives_Native.None) + | Success (et, FStar_Pervasives_Native.Some pre) -> (match g.guard_handler with | FStar_Pervasives_Native.None -> - FStar_Pervasives.Inl - (et, (FStar_Pervasives_Native.Some pre)) + Success (et, (FStar_Pervasives_Native.Some pre)) | FStar_Pervasives_Native.Some uu___2 -> check_then_memo { @@ -3769,7 +3676,7 @@ and (do_check_and_promote : fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with @@ -3781,15 +3688,14 @@ and (do_check_and_promote : let uu___4 = non_informative g t in if uu___4 then E_Total else E_Ghost in (fun uu___4 -> - FStar_Pervasives.Inl - ((eff1, t), FStar_Pervasives_Native.None)) in + Success ((eff1, t), FStar_Pervasives_Native.None)) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> Error err and (do_check : env -> FStar_Syntax_Syntax.term -> @@ -3808,7 +3714,7 @@ and (do_check : -> let uu___4 = FStar_Syntax_Util.unlazy e1 in do_check g uu___4 | FStar_Syntax_Syntax.Tm_lazy i -> (fun uu___ -> - FStar_Pervasives.Inl + Success ((E_Total, (i.FStar_Syntax_Syntax.ltyp)), FStar_Pervasives_Native.None)) | FStar_Syntax_Syntax.Tm_meta @@ -3820,8 +3726,7 @@ and (do_check : let uu___2 = FStar_Syntax_Util.ctx_uvar_typ uv in FStar_Syntax_Subst.subst' s uu___2 in (E_Total, uu___1) in - (fun uu___1 -> - FStar_Pervasives.Inl (uu___, FStar_Pervasives_Native.None)) + (fun uu___1 -> Success (uu___, FStar_Pervasives_Native.None)) | FStar_Syntax_Syntax.Tm_name x -> let uu___ = FStar_TypeChecker_Env.try_lookup_bv g.tcenv x in (match uu___ with @@ -3832,8 +3737,7 @@ and (do_check : fail uu___1 | FStar_Pervasives_Native.Some (t, uu___1) -> (fun uu___2 -> - FStar_Pervasives.Inl - ((E_Total, t), FStar_Pervasives_Native.None))) + Success ((E_Total, t), FStar_Pervasives_Native.None))) | FStar_Syntax_Syntax.Tm_fvar f -> let uu___ = FStar_TypeChecker_Env.try_lookup_lid g.tcenv @@ -3841,8 +3745,7 @@ and (do_check : (match uu___ with | FStar_Pervasives_Native.Some (([], t), uu___1) -> (fun uu___2 -> - FStar_Pervasives.Inl - ((E_Total, t), FStar_Pervasives_Native.None)) + Success ((E_Total, t), FStar_Pervasives_Native.None)) | uu___1 -> fail "Missing universes instantiation") | FStar_Syntax_Syntax.Tm_uinst ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar f; @@ -3865,8 +3768,7 @@ and (do_check : fail uu___4 | FStar_Pervasives_Native.Some (t, uu___4) -> (fun uu___5 -> - FStar_Pervasives.Inl - ((E_Total, t), FStar_Pervasives_Native.None))) + Success ((E_Total, t), FStar_Pervasives_Native.None))) | FStar_Syntax_Syntax.Tm_constant c -> (match c with | FStar_Const.Const_range_of -> fail "Unhandled constant" @@ -3878,21 +3780,19 @@ and (do_check : FStar_TypeChecker_TcTerm.tc_constant g.tcenv e1.FStar_Syntax_Syntax.pos c in (fun uu___1 -> - FStar_Pervasives.Inl - ((E_Total, t), FStar_Pervasives_Native.None))) + Success ((E_Total, t), FStar_Pervasives_Native.None))) | FStar_Syntax_Syntax.Tm_type u -> let uu___ = let uu___1 = mk_type (FStar_Syntax_Syntax.U_succ u) in (E_Total, uu___1) in - (fun uu___1 -> - FStar_Pervasives.Inl (uu___, FStar_Pervasives_Native.None)) + (fun uu___1 -> Success (uu___, FStar_Pervasives_Native.None)) | FStar_Syntax_Syntax.Tm_refine { FStar_Syntax_Syntax.b = x; FStar_Syntax_Syntax.phi = phi;_} -> let uu___ = check "refinement head" g x.FStar_Syntax_Syntax.sort in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___2 = let uu___3 = match x1 with @@ -3901,7 +3801,7 @@ and (do_check : (fun ctx01 -> let uu___6 = uu___5 ctx01 in match uu___6 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___7 = let uu___8 = let uu___9 = @@ -3917,8 +3817,7 @@ and (do_check : fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl (x4, g12) - -> + | Success (x4, g12) -> let uu___13 = let uu___14 = match x4 with @@ -3929,12 +3828,12 @@ and (do_check : let uu___17 = uu___16 ctx03 in match uu___17 with - | FStar_Pervasives.Inl + | Success (x5, g13) -> let uu___18 = let uu___19 uu___20 = - FStar_Pervasives.Inl + Success ((E_Total, t), FStar_Pervasives_Native.None) in @@ -3942,7 +3841,7 @@ and (do_check : ctx03 in (match uu___18 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___19 @@ -3953,44 +3852,38 @@ and (do_check : g13 g2 in (y, uu___20) in - FStar_Pervasives.Inl + Success uu___19 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err -> + Error err) in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in (y, uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in with_binders [x3] [x2] uu___10 in uu___8 ctx01 in (match uu___7 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___8 = let uu___9 = and_pre g11 g2 in (y, uu___9) in - FStar_Pervasives.Inl uu___8 + Success uu___8 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Tm_abs { FStar_Syntax_Syntax.bs = xs; FStar_Syntax_Syntax.body = body; FStar_Syntax_Syntax.rc_opt = uu___;_} @@ -4010,7 +3903,7 @@ and (do_check : (fun ctx0 -> let uu___3 = uu___2 ctx0 in match uu___3 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___4 = let uu___5 = let uu___6 = @@ -4018,7 +3911,7 @@ and (do_check : fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___9 = let uu___10 = let uu___11 = @@ -4027,28 +3920,27 @@ and (do_check : FStar_Syntax_Util.arrow xs1 uu___13 in (E_Total, uu___12) in fun uu___12 -> - FStar_Pervasives.Inl + Success (uu___11, FStar_Pervasives_Native.None) in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in (y, uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in with_binders xs1 x uu___6 in uu___5 ctx0 in (match uu___4 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___5 = let uu___6 = and_pre g1 g2 in (y, uu___6) in - FStar_Pervasives.Inl uu___5 + Success uu___5 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err)) + | Error err -> Error err)) | FStar_Syntax_Syntax.Tm_arrow { FStar_Syntax_Syntax.bs1 = xs; FStar_Syntax_Syntax.comp = c;_} -> let uu___ = open_comp_binders g xs c in @@ -4066,7 +3958,7 @@ and (do_check : (fun ctx0 -> let uu___2 = uu___1 ctx0 in match uu___2 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___3 = let uu___4 = let uu___5 = @@ -4083,7 +3975,7 @@ and (do_check : fun ctx01 -> let uu___7 = uu___6 ctx01 in match uu___7 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___8 = let uu___9 = let uu___10 = @@ -4093,28 +3985,27 @@ and (do_check : x)) in (E_Total, uu___11) in fun uu___11 -> - FStar_Pervasives.Inl + Success (uu___10, FStar_Pervasives_Native.None) in uu___9 ctx01 in (match uu___8 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___9 = let uu___10 = and_pre g11 g2 in (y, uu___10) in - FStar_Pervasives.Inl uu___9 + Success uu___9 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in with_binders xs1 x uu___5 in uu___4 ctx0 in (match uu___3 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___4 = let uu___5 = and_pre g1 g2 in (y, uu___5) in - FStar_Pervasives.Inl uu___4 + Success uu___4 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err)) + | Error err -> Error err)) | FStar_Syntax_Syntax.Tm_app uu___ -> let rec check_app_arg uu___1 uu___2 = match (uu___1, uu___2) with @@ -4123,7 +4014,7 @@ and (do_check : (fun ctx0 -> let uu___4 = uu___3 ctx0 in match uu___4 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___5 = let uu___6 = match x with @@ -4132,7 +4023,7 @@ and (do_check : (fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___9 = let uu___10 = match x2 with @@ -4155,8 +4046,7 @@ and (do_check : (fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl - (x3, g12) -> + | Success (x3, g12) -> let uu___13 = let uu___14 = let uu___15 ctx = @@ -4180,7 +4070,7 @@ and (do_check : let uu___16 = uu___15 ctx03 in match uu___16 with - | FStar_Pervasives.Inl + | Success (x4, g13) -> let uu___17 = let uu___18 @@ -4203,14 +4093,14 @@ and (do_check : fun uu___20 -> - FStar_Pervasives.Inl + Success (uu___19, FStar_Pervasives_Native.None) in uu___18 ctx03 in (match uu___17 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___18 @@ -4221,62 +4111,55 @@ and (do_check : g13 g2 in (y, uu___19) in - FStar_Pervasives.Inl + Success uu___18 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + | Error err -> + Error err in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in (y, uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err -> err) - | FStar_Pervasives.Inr err - -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in (y, uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___6 ctx0 in (match uu___5 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___6 = let uu___7 = and_pre g1 g2 in (y, uu___7) in - FStar_Pervasives.Inl uu___6 + Success uu___6 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) in + | Error err -> Error err) in let check_app hd args = let uu___1 = check "app head" g hd in fun ctx0 -> let uu___2 = uu___1 ctx0 in match uu___2 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___3 = let uu___4 = match x with | (eff_hd, t) -> fold check_app_arg (eff_hd, t) args in uu___4 ctx0 in (match uu___3 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___4 = let uu___5 = and_pre g1 g2 in (y, uu___5) in - FStar_Pervasives.Inl uu___4 + Success uu___4 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + | Error err -> Error err in let uu___1 = FStar_Syntax_Util.head_and_args_full e1 in (match uu___1 with | (hd, args) -> @@ -4288,7 +4171,7 @@ and (do_check : (fun ctx0 -> let uu___3 = uu___2 ctx0 in match uu___3 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___4 = let uu___5 = match x with @@ -4297,7 +4180,7 @@ and (do_check : (fun ctx01 -> let uu___7 = uu___6 ctx01 in match uu___7 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___8 = let uu___9 = match x1 with @@ -4308,8 +4191,7 @@ and (do_check : let uu___11 = uu___10 ctx02 in match uu___11 with - | FStar_Pervasives.Inl - (x3, g12) -> + | Success (x3, g12) -> let uu___12 = let uu___13 = match x3 with @@ -4347,7 +4229,7 @@ and (do_check : match uu___15 with | - FStar_Pervasives.Inl + Success (x4, g13) -> let uu___16 @@ -4373,7 +4255,7 @@ and (do_check : match uu___19 with | - FStar_Pervasives.Inl + Success (x5, g14) -> let uu___20 @@ -4423,7 +4305,7 @@ and (do_check : match uu___23 with | - FStar_Pervasives.Inl + Success (x6, g15) -> let uu___24 @@ -4468,7 +4350,7 @@ and (do_check : match uu___27 with | - FStar_Pervasives.Inl + Success (x7, g16) -> let uu___28 @@ -4494,7 +4376,7 @@ and (do_check : fun uu___31 -> - FStar_Pervasives.Inl + Success (uu___30, FStar_Pervasives_Native.None) in uu___29 @@ -4502,7 +4384,7 @@ and (do_check : (match uu___28 with | - FStar_Pervasives.Inl + Success (y1, g2) -> let uu___29 @@ -4513,22 +4395,21 @@ and (do_check : g16 g2 in (y1, uu___30) in - FStar_Pervasives.Inl + Success uu___29 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___25 ctx05 in (match uu___24 with | - FStar_Pervasives.Inl + Success (y1, g2) -> let uu___25 @@ -4539,22 +4420,21 @@ and (do_check : g15 g2 in (y1, uu___26) in - FStar_Pervasives.Inl + Success uu___25 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___21 ctx04 in (match uu___20 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___21 @@ -4565,22 +4445,21 @@ and (do_check : g14 g2 in (y, uu___22) in - FStar_Pervasives.Inl + Success uu___21 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + Error err + -> + Error err in uu___17 ctx03 in (match uu___16 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___17 @@ -4591,50 +4470,44 @@ and (do_check : g13 g2 in (y, uu___18) in - FStar_Pervasives.Inl + Success uu___17 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___13 ctx02 in (match uu___12 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) + -> let uu___13 = let uu___14 = and_pre g12 g2 in (y, uu___14) in - FStar_Pervasives.Inl - uu___13 + Success uu___13 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err -> Error err) in uu___9 ctx01 in (match uu___8 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___9 = let uu___10 = and_pre g11 g2 in (y, uu___10) in - FStar_Pervasives.Inl uu___9 + Success uu___9 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___5 ctx0 in (match uu___4 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___5 = let uu___6 = and_pre g1 g2 in (y, uu___6) in - FStar_Pervasives.Inl uu___5 + Success uu___5 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | uu___2 -> check_app hd args)) | FStar_Syntax_Syntax.Tm_ascribed { FStar_Syntax_Syntax.tm = e2; @@ -4645,7 +4518,7 @@ and (do_check : (fun ctx0 -> let uu___3 = uu___2 ctx0 in match uu___3 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___4 = let uu___5 = match x with @@ -4654,7 +4527,7 @@ and (do_check : (fun ctx01 -> let uu___7 = uu___6 ctx01 in match uu___7 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___8 = let uu___9 = match x1 with @@ -4663,8 +4536,7 @@ and (do_check : (fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl (x2, g12) - -> + | Success (x2, g12) -> let uu___13 = let uu___14 = let uu___15 ctx = @@ -4687,60 +4559,51 @@ and (do_check : let uu___16 = uu___15 ctx03 in match uu___16 with - | FStar_Pervasives.Inl - (x3, g13) -> + | Success (x3, g13) -> let uu___17 = let uu___18 uu___19 = - FStar_Pervasives.Inl + Success ((eff, t), FStar_Pervasives_Native.None) in uu___18 ctx03 in (match uu___17 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) + -> let uu___18 = let uu___19 = and_pre g13 g2 in (y, uu___19) in - FStar_Pervasives.Inl - uu___18 + Success uu___18 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + | Error err -> Error err in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in (y, uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___9 ctx01 in (match uu___8 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___9 = let uu___10 = and_pre g11 g2 in (y, uu___10) in - FStar_Pervasives.Inl uu___9 + Success uu___9 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___5 ctx0 in (match uu___4 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___5 = let uu___6 = and_pre g1 g2 in (y, uu___6) in - FStar_Pervasives.Inl uu___5 + Success uu___5 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Tm_ascribed { FStar_Syntax_Syntax.tm = e2; FStar_Syntax_Syntax.asc = (FStar_Pervasives.Inr c, uu___, uu___1); @@ -4753,7 +4616,7 @@ and (do_check : (fun ctx0 -> let uu___5 = uu___4 ctx0 in match uu___5 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___6 = let uu___7 = match x with @@ -4771,7 +4634,7 @@ and (do_check : (fun ctx01 -> let uu___9 = uu___8 ctx01 in match uu___9 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___10 = let uu___11 = let c_e = as_comp g (eff, te) in @@ -4783,7 +4646,7 @@ and (do_check : fun ctx02 -> let uu___13 = uu___12 ctx02 in match uu___13 with - | FStar_Pervasives.Inl (x2, g12) -> + | Success (x2, g12) -> let uu___14 = let uu___15 = let uu___16 = @@ -4793,39 +4656,36 @@ and (do_check : | FStar_Pervasives_Native.Some (eff1, t) -> (fun uu___17 -> - FStar_Pervasives.Inl + Success ((eff1, t), FStar_Pervasives_Native.None)) in uu___15 ctx02 in (match uu___14 with - | FStar_Pervasives.Inl (y, g2) - -> + | Success (y, g2) -> let uu___15 = let uu___16 = and_pre g12 g2 in (y, uu___16) in - FStar_Pervasives.Inl uu___15 + Success uu___15 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___11 ctx01 in (match uu___10 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___11 = let uu___12 = and_pre g11 g2 in (y, uu___12) in - FStar_Pervasives.Inl uu___11 + Success uu___11 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___7 ctx0 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g1 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) else (let uu___5 = let uu___6 = FStar_Syntax_Print.comp_to_string c in @@ -4854,7 +4714,7 @@ and (do_check : (fun ctx0 -> let uu___4 = uu___3 ctx0 in match uu___4 with - | FStar_Pervasives.Inl (x2, g1) -> + | Success (x2, g1) -> let uu___5 = let uu___6 = match x2 with @@ -4865,7 +4725,7 @@ and (do_check : (fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x3, g11) -> + | Success (x3, g11) -> let uu___9 = let uu___10 = match x3 with @@ -4876,8 +4736,7 @@ and (do_check : let uu___13 = uu___12 ctx02 in match uu___13 with - | FStar_Pervasives.Inl - (x4, g12) -> + | Success (x4, g12) -> let uu___14 = let uu___15 = let uu___16 @@ -4909,7 +4768,7 @@ and (do_check : ctx03 in match uu___17 with - | FStar_Pervasives.Inl + | Success (x5, g13) -> let uu___18 @@ -4932,7 +4791,7 @@ and (do_check : match uu___22 with | - FStar_Pervasives.Inl + Success (x6, g14) -> let uu___23 @@ -4957,14 +4816,14 @@ and (do_check : match uu___26 with | - FStar_Pervasives.Inl + Success (x7, g15) -> let uu___27 = let uu___28 uu___29 = - FStar_Pervasives.Inl + Success (((join_eff eff_def eff_body), @@ -4975,7 +4834,7 @@ and (do_check : (match uu___27 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___28 @@ -4986,22 +4845,21 @@ and (do_check : g15 g2 in (y, uu___29) in - FStar_Pervasives.Inl + Success uu___28 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___24 ctx04 in (match uu___23 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___24 @@ -5012,16 +4870,15 @@ and (do_check : g14 g2 in (y, uu___25) in - FStar_Pervasives.Inl + Success uu___24 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + Error err + -> + Error err in with_definition x1 x4 lb.FStar_Syntax_Syntax.lbdef @@ -5031,7 +4888,7 @@ and (do_check : (match uu___18 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___19 @@ -5042,19 +4899,18 @@ and (do_check : g13 g2 in (y, uu___20) in - FStar_Pervasives.Inl + Success uu___19 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + | Error err + -> + Error err in uu___15 ctx02 in (match uu___14 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___15 = let uu___16 @@ -5063,34 +4919,29 @@ and (do_check : g12 g2 in (y, uu___16) in - FStar_Pervasives.Inl + Success uu___15 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err -> + Error err) in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) - -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in (y, uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___6 ctx0 in (match uu___5 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___6 = let uu___7 = and_pre g1 g2 in (y, uu___7) in - FStar_Pervasives.Inl uu___6 + Success uu___6 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) + | Error err -> Error err) else fail "Let binding is effectful")) | FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = sc; @@ -5102,7 +4953,7 @@ and (do_check : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with @@ -5121,7 +4972,7 @@ and (do_check : (fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 = let rec check_branches path_condition @@ -5141,7 +4992,7 @@ and (do_check : | FStar_Pervasives_Native.None -> (fun uu___9 -> - FStar_Pervasives.Inl + Success (et, FStar_Pervasives_Native.None)) | FStar_Pervasives_Native.Some @@ -5155,18 +5006,17 @@ and (do_check : let uu___10 = uu___9 ctx02 in match uu___10 with - | FStar_Pervasives.Inl - (x2, g12) -> + | Success (x2, g12) -> let uu___11 = let uu___12 uu___13 = - FStar_Pervasives.Inl + Success (et, FStar_Pervasives_Native.None) in uu___12 ctx02 in (match uu___11 with - | FStar_Pervasives.Inl + | Success (y, g21) -> let uu___12 = let uu___13 @@ -5175,13 +5025,11 @@ and (do_check : g12 g21 in (y, uu___13) in - FStar_Pervasives.Inl + Success uu___12 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err))) + | Error err -> + Error err))) | (p, FStar_Pervasives_Native.None, b)::rest -> let uu___8 = @@ -5208,8 +5056,7 @@ and (do_check : (fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl - (x2, g12) -> + | Success (x2, g12) -> let uu___13 = let uu___14 = match x2 with @@ -5224,7 +5071,7 @@ and (do_check : ctx03 in match uu___16 with - | FStar_Pervasives.Inl + | Success (x3, g13) -> let uu___17 @@ -5307,7 +5154,7 @@ and (do_check : match uu___24 with | - FStar_Pervasives.Inl + Success (x4, g14) -> let uu___25 @@ -5337,14 +5184,14 @@ and (do_check : match uu___28 with | - FStar_Pervasives.Inl + Success (x5, g15) -> let uu___29 = let uu___30 uu___31 = - FStar_Pervasives.Inl + Success ((eff_br, tbr), FStar_Pervasives_Native.None) in @@ -5353,7 +5200,7 @@ and (do_check : (match uu___29 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___30 @@ -5364,16 +5211,15 @@ and (do_check : g15 g2 in (y, uu___31) in - FStar_Pervasives.Inl + Success uu___30 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) + Error err + -> + Error err) | FStar_Pervasives_Native.Some (acc_eff, @@ -5418,14 +5264,14 @@ and (do_check : match uu___28 with | - FStar_Pervasives.Inl + Success (x5, g15) -> let uu___29 = let uu___30 uu___31 = - FStar_Pervasives.Inl + Success (((join_eff eff_br acc_eff), @@ -5436,7 +5282,7 @@ and (do_check : (match uu___29 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___30 @@ -5447,22 +5293,21 @@ and (do_check : g15 g2 in (y, uu___31) in - FStar_Pervasives.Inl + Success uu___30 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err)) in + Error err + -> + Error err)) in uu___26 ctx04 in (match uu___25 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___26 @@ -5473,16 +5318,15 @@ and (do_check : g14 g2 in (y, uu___27) in - FStar_Pervasives.Inl + Success uu___26 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + Error err + -> + Error err in weaken this_path_condition uu___22 in @@ -5498,7 +5342,7 @@ and (do_check : match uu___21 with | - FStar_Pervasives.Inl + Success (x4, g14) -> let uu___22 @@ -5530,7 +5374,7 @@ and (do_check : (fun uu___26 -> - FStar_Pervasives.Inl + Success ((eff_br, tbr), FStar_Pervasives_Native.None))) @@ -5548,7 +5392,7 @@ and (do_check : (match uu___22 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___23 @@ -5559,22 +5403,21 @@ and (do_check : g14 g2 in (y, uu___24) in - FStar_Pervasives.Inl + Success uu___23 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___18 ctx03 in (match uu___17 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___18 @@ -5585,30 +5428,24 @@ and (do_check : g13 g2 in (y, uu___19) in - FStar_Pervasives.Inl + Success uu___18 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err + -> + Error err) in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in (y, uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err -> err) - | FStar_Pervasives.Inr err - -> - FStar_Pervasives.Inr - err)) in + | Error err -> Error err)) in let uu___8 = match rc_opt with | FStar_Pervasives_Native.Some @@ -5636,36 +5473,32 @@ and (do_check : (fun ctx02 -> let uu___12 = uu___11 ctx02 in match uu___12 with - | FStar_Pervasives.Inl (x2, g12) - -> + | Success (x2, g12) -> let uu___13 = let uu___14 uu___15 = - FStar_Pervasives.Inl + Success ((FStar_Pervasives_Native.Some (E_Total, t)), FStar_Pervasives_Native.None) in uu___14 ctx02 in (match uu___13 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___14 = let uu___15 = and_pre g12 g2 in (y, uu___15) in - FStar_Pervasives.Inl - uu___14 + Success uu___14 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) + | Error err -> Error err) | uu___9 -> (fun uu___10 -> - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None)) in fun ctx02 -> let uu___9 = uu___8 ctx02 in match uu___9 with - | FStar_Pervasives.Inl (x2, g12) -> + | Success (x2, g12) -> let uu___10 = let uu___11 = let uu___12 = @@ -5696,14 +5529,13 @@ and (do_check : fun ctx03 -> let uu___13 = uu___12 ctx03 in match uu___13 with - | FStar_Pervasives.Inl - (x3, g13) -> + | Success (x3, g13) -> let uu___14 = let uu___15 = match x3 with | (eff_br, t_br) -> (fun uu___16 -> - FStar_Pervasives.Inl + Success (((join_eff eff_sc eff_br), @@ -5711,44 +5543,39 @@ and (do_check : FStar_Pervasives_Native.None)) in uu___15 ctx03 in (match uu___14 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___15 = let uu___16 = and_pre g13 g2 in (y, uu___16) in - FStar_Pervasives.Inl - uu___15 + Success uu___15 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___11 ctx02 in (match uu___10 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___11 = let uu___12 = and_pre g12 g2 in (y, uu___12) in - FStar_Pervasives.Inl uu___11 + Success uu___11 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Tm_match { FStar_Syntax_Syntax.scrutinee = sc; FStar_Syntax_Syntax.ret_opt = FStar_Pervasives_Native.Some @@ -5762,7 +5589,7 @@ and (do_check : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with @@ -5781,7 +5608,7 @@ and (do_check : (fun ctx01 -> let uu___5 = uu___4 ctx01 in match uu___5 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___6 = let uu___7 = let as_x1 = @@ -5815,8 +5642,7 @@ and (do_check : (fun ctx02 -> let uu___10 = uu___9 ctx02 in match uu___10 with - | FStar_Pervasives.Inl (x2, g12) - -> + | Success (x2, g12) -> let uu___11 = let uu___12 = match x2 with @@ -5829,8 +5655,8 @@ and (do_check : let uu___14 = uu___13 ctx03 in match uu___14 with - | FStar_Pervasives.Inl - (x3, g13) -> + | Success (x3, g13) + -> let uu___15 = let uu___16 = let rec check_branches @@ -5853,7 +5679,7 @@ and (do_check : (fun uu___18 -> - FStar_Pervasives.Inl + Success (acc_eff, FStar_Pervasives_Native.None)) | @@ -5876,14 +5702,14 @@ and (do_check : match uu___19 with | - FStar_Pervasives.Inl + Success (x4, g14) -> let uu___20 = let uu___21 uu___22 = - FStar_Pervasives.Inl + Success (acc_eff, FStar_Pervasives_Native.None) in uu___21 @@ -5891,7 +5717,7 @@ and (do_check : (match uu___20 with | - FStar_Pervasives.Inl + Success (y, g21) -> let uu___21 @@ -5902,16 +5728,15 @@ and (do_check : g14 g21 in (y, uu___22) in - FStar_Pervasives.Inl + Success uu___21 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err)) + Error err + -> + Error err)) | (p, FStar_Pervasives_Native.None, @@ -5961,7 +5786,7 @@ and (do_check : match uu___21 with | - FStar_Pervasives.Inl + Success (x4, g14) -> let uu___22 @@ -5986,7 +5811,7 @@ and (do_check : match uu___25 with | - FStar_Pervasives.Inl + Success (x5, g15) -> let uu___26 @@ -6051,7 +5876,7 @@ and (do_check : match uu___33 with | - FStar_Pervasives.Inl + Success (x6, g16) -> let uu___34 @@ -6094,14 +5919,14 @@ and (do_check : match uu___37 with | - FStar_Pervasives.Inl + Success (x7, g17) -> let uu___38 = let uu___39 uu___40 = - FStar_Pervasives.Inl + Success (((join_eff eff_br acc_eff), @@ -6112,7 +5937,7 @@ and (do_check : (match uu___38 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___39 @@ -6123,22 +5948,21 @@ and (do_check : g17 g2 in (y, uu___40) in - FStar_Pervasives.Inl + Success uu___39 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___35 ctx06 in (match uu___34 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___35 @@ -6149,16 +5973,15 @@ and (do_check : g16 g2 in (y, uu___36) in - FStar_Pervasives.Inl + Success uu___35 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + Error err + -> + Error err in weaken this_path_condition uu___31 in @@ -6174,7 +5997,7 @@ and (do_check : match uu___30 with | - FStar_Pervasives.Inl + Success (x6, g16) -> let uu___31 @@ -6206,7 +6029,7 @@ and (do_check : (fun uu___35 -> - FStar_Pervasives.Inl + Success (eff_br, FStar_Pervasives_Native.None))) | @@ -6221,7 +6044,7 @@ and (do_check : (match uu___31 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___32 @@ -6232,22 +6055,21 @@ and (do_check : g16 g2 in (y, uu___33) in - FStar_Pervasives.Inl + Success uu___32 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___27 ctx05 in (match uu___26 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___27 @@ -6258,22 +6080,21 @@ and (do_check : g15 g2 in (y, uu___28) in - FStar_Pervasives.Inl + Success uu___27 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___23 ctx04 in (match uu___22 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___23 @@ -6284,16 +6105,15 @@ and (do_check : g14 g2 in (y, uu___24) in - FStar_Pervasives.Inl + Success uu___23 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err)) in + Error err + -> + Error err)) in let uu___17 = check_branches @@ -6309,7 +6129,7 @@ and (do_check : match uu___18 with | - FStar_Pervasives.Inl + Success (x4, g14) -> let uu___19 @@ -6326,7 +6146,7 @@ and (do_check : fun uu___21 -> - FStar_Pervasives.Inl + Success ((x4, ty), FStar_Pervasives_Native.None) in uu___20 @@ -6334,7 +6154,7 @@ and (do_check : (match uu___19 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___20 @@ -6345,20 +6165,19 @@ and (do_check : g14 g2 in (y, uu___21) in - FStar_Pervasives.Inl + Success uu___20 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + Error err + -> + Error err in uu___16 ctx03 in (match uu___15 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___16 = @@ -6368,43 +6187,37 @@ and (do_check : g13 g2 in (y, uu___17) in - FStar_Pervasives.Inl + Success uu___16 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err -> + Error err) in uu___12 ctx02 in (match uu___11 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___12 = let uu___13 = and_pre g12 g2 in (y, uu___13) in - FStar_Pervasives.Inl - uu___12 + Success uu___12 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___7 ctx01 in (match uu___6 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___7 = let uu___8 = and_pre g11 g2 in (y, uu___8) in - FStar_Pervasives.Inl uu___7 + Success uu___7 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Tm_match uu___ -> fail "Match with effect returns ascription, or tactic handler" | uu___ -> @@ -6421,9 +6234,7 @@ and (check_binders : fun xs -> let rec aux g xs1 = match xs1 with - | [] -> - (fun uu___ -> - FStar_Pervasives.Inl ([], FStar_Pervasives_Native.None)) + | [] -> (fun uu___ -> Success ([], FStar_Pervasives_Native.None)) | x::xs2 -> let uu___ = check "binder sort" g @@ -6431,7 +6242,7 @@ and (check_binders : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x1, g1) -> + | Success (x1, g1) -> let uu___2 = let uu___3 = match x1 with @@ -6440,7 +6251,7 @@ and (check_binders : (fun ctx01 -> let uu___6 = uu___5 ctx01 in match uu___6 with - | FStar_Pervasives.Inl (x2, g11) -> + | Success (x2, g11) -> let uu___7 = let uu___8 = let uu___9 = @@ -6450,44 +6261,40 @@ and (check_binders : fun ctx02 -> let uu___11 = uu___10 ctx02 in match uu___11 with - | FStar_Pervasives.Inl (x3, g12) -> + | Success (x3, g12) -> let uu___12 = let uu___13 uu___14 = - FStar_Pervasives.Inl + Success ((x2 :: x3), FStar_Pervasives_Native.None) in uu___13 ctx02 in (match uu___12 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___13 = let uu___14 = and_pre g12 g2 in (y, uu___14) in - FStar_Pervasives.Inl - uu___13 + Success uu___13 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in with_binders [x] [x2] uu___9 in uu___8 ctx01 in (match uu___7 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___8 = let uu___9 = and_pre g11 g2 in (y, uu___9) in - FStar_Pervasives.Inl uu___8 + Success uu___8 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) in + | Error err -> Error err) in aux g_initial xs and (check_comp : env -> FStar_Syntax_Syntax.comp -> FStar_Syntax_Syntax.universe result) = @@ -6500,32 +6307,32 @@ and (check_comp : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with | (uu___4, t1) -> is_type g t1 in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.GTotal t -> let uu___ = check "(G)Tot comp result" g (FStar_Syntax_Util.comp_result c) in (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with | (uu___4, t1) -> is_type g t1 in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Comp ct -> if (FStar_Compiler_List.length ct.FStar_Syntax_Syntax.comp_univs) <> @@ -6551,7 +6358,7 @@ and (check_comp : fun ctx0 -> let uu___2 = uu___1 ctx0 in match uu___2 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___3 = let uu___4 = match x with @@ -6572,7 +6379,7 @@ and (check_comp : (fun ctx01 -> let uu___7 = uu___6 ctx01 in match uu___7 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___8 = let uu___9 = let c_lid = @@ -6591,7 +6398,7 @@ and (check_comp : if Prims.op_Negation is_total then fun uu___10 -> - FStar_Pervasives.Inl + Success (FStar_Syntax_Syntax.U_zero, FStar_Pervasives_Native.None) else @@ -6601,7 +6408,7 @@ and (check_comp : if uu___11 then fun uu___12 -> - FStar_Pervasives.Inl + Success (u, FStar_Pervasives_Native.None) else @@ -6626,22 +6433,21 @@ and (check_comp : -> universe_of g tm)) in uu___9 ctx01 in (match uu___8 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___9 = let uu___10 = and_pre g11 g2 in (y, uu___10) in - FStar_Pervasives.Inl uu___9 + Success uu___9 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___4 ctx0 in (match uu___3 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___4 = let uu___5 = and_pre g1 g2 in (y, uu___5) in - FStar_Pervasives.Inl uu___4 + Success uu___4 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) and (universe_of : env -> FStar_Syntax_Syntax.typ -> FStar_Syntax_Syntax.universe result) = fun g -> @@ -6650,16 +6456,16 @@ and (universe_of : fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with | (uu___4, t1) -> is_type g t1 in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> Error err and (check_pat : env -> FStar_Syntax_Syntax.pat -> @@ -6690,7 +6496,7 @@ and (check_pat : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with @@ -6702,30 +6508,29 @@ and (check_pat : (fun ctx01 -> let uu___6 = uu___5 ctx01 in match uu___6 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___7 = let uu___8 uu___9 = - FStar_Pervasives.Inl + Success (([], []), FStar_Pervasives_Native.None) in uu___8 ctx01 in (match uu___7 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___8 = let uu___9 = and_pre g11 g2 in (y, uu___9) in - FStar_Pervasives.Inl uu___8 + Success uu___8 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err) in + | Error err -> Error err) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Pat_var bv -> let b = FStar_Syntax_Syntax.mk_binder @@ -6747,22 +6552,22 @@ and (check_pat : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with | u::[] -> (fun uu___4 -> - FStar_Pervasives.Inl + Success (([b], [u]), FStar_Pervasives_Native.None)) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Pat_cons (fv, usopt, pats) -> let us = if FStar_Compiler_Util.is_none usopt @@ -6824,7 +6629,7 @@ and (check_pat : (FStar_Pervasives_Native.Some t) -> (fun uu___9 -> - FStar_Pervasives.Inl + Success (t, FStar_Pervasives_Native.None)) | uu___9 -> @@ -6833,8 +6638,7 @@ and (check_pat : (fun ctx0 -> let uu___9 = uu___8 ctx0 in match uu___9 with - | FStar_Pervasives.Inl (x, g1) - -> + | Success (x, g1) -> let uu___10 = let uu___11 = let uu___12 = @@ -6844,8 +6648,7 @@ and (check_pat : let uu___13 = uu___12 ctx01 in match uu___13 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) -> let uu___14 = let uu___15 = match x1 with @@ -6864,14 +6667,14 @@ and (check_pat : match uu___17 with | - FStar_Pervasives.Inl + Success (x2, g12) -> let uu___18 = let uu___19 uu___20 = - FStar_Pervasives.Inl + Success ((FStar_List_Tot_Base.op_At ss [ @@ -6883,7 +6686,7 @@ and (check_pat : (match uu___18 with | - FStar_Pervasives.Inl + Success (y, g2) -> let uu___19 @@ -6894,20 +6697,19 @@ and (check_pat : g12 g2 in (y, uu___20) in - FStar_Pervasives.Inl + Success uu___19 | err -> err) | - FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + Error err + -> + Error err) in uu___15 ctx01 in (match uu___14 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___15 = let uu___16 @@ -6916,31 +6718,26 @@ and (check_pat : g11 g2 in (y, uu___16) in - FStar_Pervasives.Inl + Success uu___15 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err in + | Error err -> + Error err in uu___11 ctx0 in (match uu___10 with - | FStar_Pervasives.Inl - (y, g2) -> + | Success (y, g2) -> let uu___11 = let uu___12 = and_pre g1 g2 in (y, uu___12) in - FStar_Pervasives.Inl - uu___11 + Success uu___11 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err)) - [] dot_formals dot_pats in + | Error err -> Error err)) [] + dot_formals dot_pats in (fun ctx0 -> let uu___4 = uu___3 ctx0 in match uu___4 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___5 = let uu___6 = let uu___7 = @@ -6974,8 +6771,8 @@ and (check_pat : let uu___14 = uu___13 ctx01 in match uu___14 with - | FStar_Pervasives.Inl - (x1, g11) -> + | Success (x1, g11) + -> let uu___15 = let uu___16 = match x1 with @@ -7012,13 +6809,13 @@ and (check_pat : (fun uu___18 -> - FStar_Pervasives.Inl + Success (uu___17, FStar_Pervasives_Native.None)) in uu___16 ctx01 in (match uu___15 with - | FStar_Pervasives.Inl + | Success (y, g21) -> let uu___16 = @@ -7028,19 +6825,17 @@ and (check_pat : g11 g21 in (y, uu___17) in - FStar_Pervasives.Inl + Success uu___16 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err)) + | Error err -> + Error err)) (g, x, [], []) rest_formals rest_pats in fun ctx01 -> let uu___8 = uu___7 ctx01 in match uu___8 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___9 = let uu___10 = match x1 with @@ -7059,18 +6854,17 @@ and (check_pat : let uu___13 = uu___12 ctx02 in match uu___13 with - | FStar_Pervasives.Inl - (x2, g12) -> + | Success (x2, g12) -> let uu___14 = let uu___15 uu___16 = - FStar_Pervasives.Inl + Success ((bs, us1), FStar_Pervasives_Native.None) in uu___15 ctx02 in (match uu___14 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___15 = let uu___16 @@ -7079,35 +6873,30 @@ and (check_pat : g12 g2 in (y, uu___16) in - FStar_Pervasives.Inl + Success uu___15 | err -> err) - | FStar_Pervasives.Inr - err -> - FStar_Pervasives.Inr - err) in + | Error err -> + Error err) in uu___10 ctx01 in (match uu___9 with - | FStar_Pervasives.Inl (y, g2) - -> + | Success (y, g2) -> let uu___10 = let uu___11 = and_pre g11 g2 in (y, uu___11) in - FStar_Pervasives.Inl uu___10 + Success uu___10 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err in + | Error err -> Error err in uu___6 ctx0 in (match uu___5 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___6 = let uu___7 = and_pre g1 g2 in (y, uu___7) in - FStar_Pervasives.Inl uu___6 + Success uu___6 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err)))) + | Error err -> Error err)))) | uu___ -> fail "check_pat called with a dot pattern" and (check_scrutinee_pattern_type_compatible : env -> @@ -7146,8 +6935,7 @@ and (check_scrutinee_pattern_type_compatible : let uu___5 = FStar_Syntax_Syntax.lid_of_fv fv_pat in FStar_Ident.lid_equals uu___4 uu___5 -> (fun uu___4 -> - FStar_Pervasives.Inl - (fv_head, FStar_Pervasives_Native.None)) + Success (fv_head, FStar_Pervasives_Native.None)) | (FStar_Syntax_Syntax.Tm_uinst ({ FStar_Syntax_Syntax.n = FStar_Syntax_Syntax.Tm_fvar @@ -7173,8 +6961,7 @@ and (check_scrutinee_pattern_type_compatible : if uu___10 then (fun uu___11 -> - FStar_Pervasives.Inl - (fv_head, FStar_Pervasives_Native.None)) + Success (fv_head, FStar_Pervasives_Native.None)) else err "Incompatible universe instantiations" | (uu___4, uu___5) -> let uu___6 = @@ -7187,7 +6974,7 @@ and (check_scrutinee_pattern_type_compatible : (fun ctx0 -> let uu___3 = uu___2 ctx0 in match uu___3 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___4 = let uu___5 = let uu___6 = @@ -7198,8 +6985,7 @@ and (check_scrutinee_pattern_type_compatible : if uu___7 then fun uu___8 -> - FStar_Pervasives.Inl - (x, FStar_Pervasives_Native.None) + Success (x, FStar_Pervasives_Native.None) else (let uu___9 = let uu___10 = @@ -7210,7 +6996,7 @@ and (check_scrutinee_pattern_type_compatible : fun ctx01 -> let uu___7 = uu___6 ctx01 in match uu___7 with - | FStar_Pervasives.Inl (x1, g11) -> + | Success (x1, g11) -> let uu___8 = let uu___9 = let uu___10 = @@ -7221,7 +7007,7 @@ and (check_scrutinee_pattern_type_compatible : args_pat) then fun uu___11 -> - FStar_Pervasives.Inl + Success (x, FStar_Pervasives_Native.None) else @@ -7241,7 +7027,7 @@ and (check_scrutinee_pattern_type_compatible : fun ctx02 -> let uu___11 = uu___10 ctx02 in match uu___11 with - | FStar_Pervasives.Inl (x2, g12) -> + | Success (x2, g12) -> let uu___12 = let uu___13 = let uu___14 = @@ -7296,18 +7082,17 @@ and (check_scrutinee_pattern_type_compatible : let uu___16 = uu___15 ctx03 in match uu___16 with - | FStar_Pervasives.Inl - (x3, g13) -> + | Success (x3, g13) -> let uu___17 = let uu___18 uu___19 = - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None) in uu___18 ctx03 in (match uu___17 with - | FStar_Pervasives.Inl + | Success (y, g2) -> let uu___18 = let uu___19 @@ -7316,43 +7101,38 @@ and (check_scrutinee_pattern_type_compatible : g13 g2 in (y, uu___19) in - FStar_Pervasives.Inl + Success uu___18 | err1 -> err1) - | FStar_Pervasives.Inr - err1 -> - FStar_Pervasives.Inr - err1) in + | Error err1 -> + Error err1) in uu___13 ctx02 in (match uu___12 with - | FStar_Pervasives.Inl (y, g2) - -> + | Success (y, g2) -> let uu___13 = let uu___14 = and_pre g12 g2 in (y, uu___14) in - FStar_Pervasives.Inl uu___13 + Success uu___13 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___9 ctx01 in (match uu___8 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___9 = let uu___10 = and_pre g11 g2 in (y, uu___10) in - FStar_Pervasives.Inl uu___9 + Success uu___9 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> - FStar_Pervasives.Inr err1 in + | Error err1 -> Error err1 in uu___5 ctx0 in (match uu___4 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___5 = let uu___6 = and_pre g1 g2 in (y, uu___6) in - FStar_Pervasives.Inl uu___5 + Success uu___5 | err1 -> err1) - | FStar_Pervasives.Inr err1 -> FStar_Pervasives.Inr err1)) + | Error err1 -> Error err1)) and (pattern_branch_condition : env -> FStar_Syntax_Syntax.term -> @@ -7365,7 +7145,7 @@ and (pattern_branch_condition : match pat.FStar_Syntax_Syntax.v with | FStar_Syntax_Syntax.Pat_var uu___ -> (fun uu___1 -> - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None)) | FStar_Syntax_Syntax.Pat_constant c -> let const_exp = @@ -7379,7 +7159,7 @@ and (pattern_branch_condition : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = match x with @@ -7390,16 +7170,15 @@ and (pattern_branch_condition : scrutinee const_exp in FStar_Pervasives_Native.Some uu___6 in (fun uu___6 -> - FStar_Pervasives.Inl - (uu___5, FStar_Pervasives_Native.None)) in + Success (uu___5, FStar_Pervasives_Native.None)) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) | FStar_Syntax_Syntax.Pat_cons (fv, us_opt, sub_pats) -> let wild_pat pos = let uu___ = @@ -7522,12 +7301,12 @@ and (pattern_branch_condition : (match pi.FStar_Syntax_Syntax.v with | FStar_Syntax_Syntax.Pat_dot_term uu___3 -> (fun uu___4 -> - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None)) | FStar_Syntax_Syntax.Pat_var uu___3 -> (fun uu___4 -> - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None)) | uu___3 -> @@ -7537,7 +7316,7 @@ and (pattern_branch_condition : (fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g1) -> + | Success (x, g1) -> let uu___2 = let uu___3 = let guards = @@ -7550,7 +7329,7 @@ and (pattern_branch_condition : match guards with | [] -> (fun uu___4 -> - FStar_Pervasives.Inl + Success (FStar_Pervasives_Native.None, FStar_Pervasives_Native.None)) | guards1 -> @@ -7558,16 +7337,15 @@ and (pattern_branch_condition : let uu___5 = FStar_Syntax_Util.mk_and_l guards1 in FStar_Pervasives_Native.Some uu___5 in (fun uu___5 -> - FStar_Pervasives.Inl - (uu___4, FStar_Pervasives_Native.None)) in + Success (uu___4, FStar_Pervasives_Native.None)) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g1 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) + | Error err -> Error err) let (initial_env : FStar_TypeChecker_Env.env -> guard_handler_t FStar_Pervasives_Native.option -> env) @@ -7609,7 +7387,7 @@ let (check_term_top : fun ctx0 -> let uu___1 = uu___ ctx0 in match uu___1 with - | FStar_Pervasives.Inl (x, g11) -> + | Success (x, g11) -> let uu___2 = let uu___3 = match topt with @@ -7628,13 +7406,12 @@ let (check_term_top : fail "expected total effect, found ghost" else (fun uu___7 -> - FStar_Pervasives.Inl + Success ((E_Total, t), FStar_Pervasives_Native.None))) else (fun uu___5 -> - FStar_Pervasives.Inl - (x, FStar_Pervasives_Native.None)) + Success (x, FStar_Pervasives_Native.None)) | FStar_Pervasives_Native.Some t -> let uu___4 = if @@ -7676,30 +7453,29 @@ let (check_term_top : (fun ctx01 -> let uu___6 = uu___5 ctx01 in match uu___6 with - | FStar_Pervasives.Inl (x1, g12) -> + | Success (x1, g12) -> let uu___7 = let uu___8 uu___9 = - FStar_Pervasives.Inl + Success ((eff, t), FStar_Pervasives_Native.None) in uu___8 ctx01 in (match uu___7 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___8 = let uu___9 = and_pre g12 g2 in (y, uu___9) in - FStar_Pervasives.Inl uu___8 + Success uu___8 | err -> err) - | FStar_Pervasives.Inr err -> - FStar_Pervasives.Inr err)) in + | Error err -> Error err)) in uu___3 ctx0 in (match uu___2 with - | FStar_Pervasives.Inl (y, g2) -> + | Success (y, g2) -> let uu___3 = let uu___4 = and_pre g11 g2 in (y, uu___4) in - FStar_Pervasives.Inl uu___3 + Success uu___3 | err -> err) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> Error err let (simplify_steps : FStar_TypeChecker_Env.step Prims.list) = [FStar_TypeChecker_Env.Beta; FStar_TypeChecker_Env.UnfoldUntil FStar_Syntax_Syntax.delta_constant; @@ -7716,8 +7492,8 @@ let (check_term_top_gh : FStar_Syntax_Syntax.typ FStar_Pervasives_Native.option -> Prims.bool -> guard_handler_t FStar_Pervasives_Native.option -> - (((tot_or_ghost * FStar_Syntax_Syntax.typ) * precondition), - error) FStar_Pervasives.either) + ((tot_or_ghost * FStar_Syntax_Syntax.typ) * precondition) + __result) = fun g -> fun e -> @@ -7766,15 +7542,12 @@ let (check_term_top_gh : let uu___6 = check_term_top g e topt must_tot gh in uu___6 ctx in match uu___5 with - | FStar_Pervasives.Inl (et, g1) -> - FStar_Pervasives.Inl (et, g1) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err) - FStar_Pervasives_Native.None + | Success (et, g1) -> Success (et, g1) + | Error err -> Error err) FStar_Pervasives_Native.None "FStar.TypeChecker.Core.check_term_top" in let res1 = match res with - | FStar_Pervasives.Inl - (et, FStar_Pervasives_Native.Some guard0) -> + | Success (et, FStar_Pervasives_Native.Some guard0) -> let guard1 = FStar_TypeChecker_Normalize.normalize simplify_steps g guard0 in @@ -7827,9 +7600,8 @@ let (check_term_top_gh : uu___8 | uu___8 -> ())) else ()); - FStar_Pervasives.Inl - (et, (FStar_Pervasives_Native.Some guard1))) - | FStar_Pervasives.Inl uu___4 -> + Success (et, (FStar_Pervasives_Native.Some guard1))) + | Success uu___4 -> ((let uu___6 = (FStar_TypeChecker_Env.debug g (FStar_Options.Other "Core")) @@ -7845,7 +7617,7 @@ let (check_term_top_gh : uu___7 else ()); res) - | FStar_Pervasives.Inr uu___4 -> + | Error uu___4 -> ((let uu___6 = (FStar_TypeChecker_Env.debug g (FStar_Options.Other "Core")) @@ -7889,8 +7661,8 @@ let (check_term : check_term_top_gh g e (FStar_Pervasives_Native.Some t) must_tot FStar_Pervasives_Native.None in match uu___ with - | FStar_Pervasives.Inl (uu___1, g1) -> FStar_Pervasives.Inl g1 - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Success (uu___1, g1) -> FStar_Pervasives.Inl g1 + | Error err -> FStar_Pervasives.Inr err let (check_term_at_type : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> @@ -7907,9 +7679,8 @@ let (check_term_at_type : check_term_top_gh g e (FStar_Pervasives_Native.Some t) must_tot FStar_Pervasives_Native.None in match uu___ with - | FStar_Pervasives.Inl ((eff, uu___1), g1) -> - FStar_Pervasives.Inl (eff, g1) - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Success ((eff, uu___1), g1) -> FStar_Pervasives.Inl (eff, g1) + | Error err -> FStar_Pervasives.Inr err let (compute_term_type_handle_guards : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> @@ -7926,13 +7697,11 @@ let (compute_term_type_handle_guards : check_term_top_gh g e1 FStar_Pervasives_Native.None must_tot (FStar_Pervasives_Native.Some gh) in match uu___ with - | FStar_Pervasives.Inl (r, FStar_Pervasives_Native.None) -> - FStar_Pervasives.Inl r - | FStar_Pervasives.Inl (uu___1, FStar_Pervasives_Native.Some uu___2) - -> + | Success (r, FStar_Pervasives_Native.None) -> FStar_Pervasives.Inl r + | Success (uu___1, FStar_Pervasives_Native.Some uu___2) -> FStar_Compiler_Effect.failwith "Impossible: All guards should have been handled already" - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err + | Error err -> FStar_Pervasives.Inr err let (open_binders_in_term : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.binders -> @@ -7987,12 +7756,7 @@ let (check_term_equality : no_guard = false; error_context = [("Eq", FStar_Pervasives_Native.None)] } in - let r = - let uu___1 = - let uu___2 = check_relation g1 EQUALITY t0 t1 in uu___2 ctx in - match uu___1 with - | FStar_Pervasives.Inl (uu___2, g2) -> FStar_Pervasives.Inl g2 - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err in + let r = let uu___1 = check_relation g1 EQUALITY t0 t1 in uu___1 ctx in (let uu___2 = FStar_TypeChecker_Env.debug g1.tcenv (FStar_Options.Other "CoreTop") in @@ -8004,17 +7768,21 @@ let (check_term_equality : FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in let uu___5 = FStar_Class_Show.show - (FStar_Class_Show.show_either - (FStar_Class_Show.show_option - FStar_Syntax_Print.showable_term) - (FStar_Class_Show.show_tuple2 showable_context + (showable_result + (FStar_Class_Show.show_tuple2 (FStar_Class_Show.printableshow - FStar_Class_Printable.printable_string))) r in + FStar_Class_Printable.printable_unit) + (FStar_Class_Show.show_option + FStar_Syntax_Print.showable_term))) r in FStar_Compiler_Util.print3 "} Exiting check_term_equality (%s, %s). Result = %s.\n" uu___3 uu___4 uu___5 else ()); - r) + (let r1 = + match r with + | Success (uu___2, g2) -> FStar_Pervasives.Inl g2 + | Error err -> FStar_Pervasives.Inr err in + r1)) let (check_term_subtyping : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> @@ -8036,5 +7804,5 @@ let (check_term_subtyping : check_relation g1 (SUBTYPING FStar_Pervasives_Native.None) t0 t1 in uu___1 ctx in match uu___ with - | FStar_Pervasives.Inl (uu___1, g2) -> FStar_Pervasives.Inl g2 - | FStar_Pervasives.Inr err -> FStar_Pervasives.Inr err \ No newline at end of file + | Success (uu___1, g2) -> FStar_Pervasives.Inl g2 + | Error err -> FStar_Pervasives.Inr err \ No newline at end of file diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index b0a2ebae20a..be4e0cdd8fd 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -246,11 +246,14 @@ let op_as_term env arity op : option S.term = | "%" -> r C.op_Modulus delta_equational | "@" -> - FStar.Errors.log_issue + FStar.Errors.log_issue_doc (range_of_id op) - (FStar.Errors.Warning_DeprecatedGeneric, - "The operator '@' has been resolved to FStar.List.Tot.append even though FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to stop relying on this deprecated, special treatment of '@'"); + (FStar.Errors.Warning_DeprecatedGeneric, [ + Errors.Msg.text "The operator '@' has been resolved to FStar.List.Tot.append even though \ + FStar.List.Tot is not in scope. Please add an 'open FStar.List.Tot' to \ + stop relying on this deprecated, special treatment of '@'."]); r C.list_tot_append_lid (Delta_equational_at_level 2) + | "<>" -> r C.op_notEq delta_equational | "~" -> diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst index 0c7aaea04e6..ee59a716f2b 100644 --- a/src/typechecker/FStar.TypeChecker.Core.fst +++ b/src/typechecker/FStar.TypeChecker.Core.fst @@ -166,8 +166,12 @@ type context = { error_context: list (string & option context_term) } +(* The instance prints some brief info on the error_context. `print_context` +below is a full printer. *) instance showable_context : showable context = { - show = (fun _ -> ""); + show = (fun context -> BU.format2 "{no_guard=%s, error_context=%s}" + (show context.no_guard) + (show (List.map fst context.error_context))); } let print_context (ctx:context) @@ -196,7 +200,17 @@ let print_error (err:error) = let print_error_short (err:error) = snd err -let result a = context -> either (success a) error +type __result a = + | Success of a + | Error of error + +instance showable_result #a (_ : showable a) : Tot (showable (__result a)) = { + show = (function + | Success a -> "Success " ^ show a + | Error e -> "Error " ^ print_error_short e); +} + +let result a = context -> __result (success a) type hash_entry = { he_term:term; @@ -232,7 +246,7 @@ let insert (g:env) (e:term) (res:success (tot_or_ghost & typ)) = THT.insert e entry table inline_for_extraction -let return (#a:Type) (x:a) : result a = fun _ -> Inl (x, None) +let return (#a:Type) (x:a) : result a = fun _ -> Success (x, None) let and_pre (p1 p2:precondition) = match p1, p2 with @@ -246,11 +260,11 @@ let (let!) (#a:Type) (#b:Type) (x:result a) (y:a -> result b) : result b = fun ctx0 -> match x ctx0 with - | Inl (x, g1) -> + | Success (x, g1) -> (match y x ctx0 with - | Inl (y, g2) -> Inl (y, and_pre g1 g2) + | Success (y, g2) -> Success (y, and_pre g1 g2) | err -> err) - | Inr err -> Inr err + | Error err -> Error err inline_for_extraction let (and!) (#a:Type) (#b:Type) (x:result a) (y:result b) @@ -265,7 +279,7 @@ let (let?) (#a:Type) (#b:Type) (x:option a) (f: a -> option b) | None -> None | Some x -> f x -let fail #a msg : result a = fun ctx -> Inr (ctx, msg) +let fail #a msg : result a = fun ctx -> Error (ctx, msg) let dump_context : result unit @@ -278,7 +292,7 @@ let handle_with (#a:Type) (x:result a) (h: unit -> result a) : result a = fun ctx -> match x ctx with - | Inr _ -> h () ctx + | Error _ -> h () ctx | res -> res inline_for_extraction @@ -461,19 +475,19 @@ let with_binders (#a:Type) (xs:binders) (us:universes) (f:result a) : result a = fun ctx -> match f ctx with - | Inl (t, g) -> Inl (t, close_guard xs us g) + | Success (t, g) -> Success (t, close_guard xs us g) | err -> err let with_definition (#a:Type) (x:binder) (u:universe) (t:term) (f:result a) : result a = fun ctx -> match f ctx with - | Inl (a, g) -> Inl (a, close_guard_with_definition x u t g) + | Success (a, g) -> Success (a, close_guard_with_definition x u t g) | err -> err let guard (t:typ) : result unit - = fun _ -> Inl ((), Some t) + = fun _ -> Success ((), Some t) let abs (a:typ) (f: binder -> term) : term = let x = S.new_bv None a in @@ -493,7 +507,7 @@ let strengthen_subtyping_guard (p:term) let weaken (p:term) (g:result 'a) = fun ctx -> match g ctx with - | Inl (x, q) -> Inl (x, weaken_subtyping_guard p q) + | Success (x, q) -> Success (x, weaken_subtyping_guard p q) | err -> err let weaken_with_guard_formula (p:FStar.TypeChecker.Common.guard_formula) (g:result 'a) @@ -509,15 +523,15 @@ let push_hypothesis (g:env) (h:term) = let strengthen (p:term) (g:result 'a) = fun ctx -> match g ctx with - | Inl (x, q) -> Inl (x, strengthen_subtyping_guard p q) + | Success (x, q) -> Success (x, strengthen_subtyping_guard p q) | err -> err let no_guard (g:result 'a) : result 'a = fun ctx -> match g ({ ctx with no_guard = true}) with - | Inl (x, None) -> Inl (x, None) - | Inl (x, Some g) -> fail (BU.format1 "Unexpected guard: %s" (P.term_to_string g)) ctx + | Success (x, None) -> Success (x, None) + | Success (x, Some g) -> fail (BU.format1 "Unexpected guard: %s" (P.term_to_string g)) ctx | err -> err let equatable g t = @@ -579,7 +593,7 @@ let lookup (g:env) (e:term) : result (tot_or_ghost & typ) = // (P.term_to_string e) // (P.term_to_string (snd (fst he.he_res))) // (show he.he_gamma); - fun _ -> Inl he.he_res + fun _ -> Success he.he_res ) else ( // record_cache_miss(); @@ -675,18 +689,7 @@ let join_eff_l es = List.Tot.fold_right join_eff es E_Total let guard_not_allowed : result bool - = fun ctx -> Inl (ctx.no_guard, None) - -let default_norm_steps : Env.steps = - let open Env in - [ Primops; - Weak; - HNF; - UnfoldUntil delta_constant; - Unascribe; - Eager_unfolding; - Iota; - Exclude Zeta ] + = fun ctx -> Success (ctx.no_guard, None) let debug g f = if Env.debug g.tcenv (Options.Other "Core") @@ -875,8 +878,8 @@ let rec check_relation (g:env) (rel:relation) (t0 t1:typ) None "FStar.TypeChecker.Core.beta_iota_reduce" in - let t0 = Subst.compress (beta_iota_reduce t0) in - let t1 = Subst.compress (beta_iota_reduce t1) in + let t0 = Subst.compress (beta_iota_reduce t0) |> U.unlazy_emb in + let t1 = Subst.compress (beta_iota_reduce t1) |> U.unlazy_emb in let check_relation g rel t0 t1 = with_context "check_relation" (Some (CtxRel t0 rel t1)) (fun _ -> check_relation g rel t0 t1) @@ -1184,17 +1187,17 @@ and memo_check (g:env) (e:term) = let check_then_memo g e ctx = let r = do_check_and_promote g e ctx in match r with - | Inl (res, None) -> + | Success (res, None) -> insert g e (res, None); r - | Inl (res, Some guard) -> + | Success (res, Some guard) -> (match g.guard_handler with | None -> insert g e (res, Some guard); r | Some gh -> if gh g.tcenv guard then let r = (res, None) in - insert g e r; Inl r + insert g e r; Success r else fail "guard handler failed" ctx) | _ -> r @@ -1204,15 +1207,15 @@ and memo_check (g:env) (e:term) then check_then_memo g e ctx else ( match lookup g e ctx with - | Inr _ -> //cache miss; check and insert + | Error _ -> //cache miss; check and insert check_then_memo g e ctx - | Inl (et, None) -> //cache hit with no guard; great, just return - Inl (et, None) + | Success (et, None) -> //cache hit with no guard; great, just return + Success (et, None) - | Inl (et, Some pre) -> //cache hit with a guard + | Success (et, Some pre) -> //cache hit with a guard match g.guard_handler with - | None -> Inl (et, Some pre) //if there's no guard handler, then just return + | None -> Success (et, Some pre) //if there's no guard handler, then just return | Some _ -> //otherwise check then memo, since this can //repopulate the cache with a "better" entry that has no guard @@ -1839,7 +1842,7 @@ let simplify_steps = let check_term_top_gh g e topt (must_tot:bool) (gh:option guard_handler_t) - : either ((tot_or_ghost & S.typ) & precondition) error + : __result ((tot_or_ghost & S.typ) & precondition) = if Env.debug g (Options.Other "CoreEq") then BU.print1 "(%s) Entering core ... \n" (BU.string_of_int (get_goal_ctr())); @@ -1857,15 +1860,15 @@ let check_term_top_gh g e topt (must_tot:bool) (gh:option guard_handler_t) Profiling.profile (fun () -> match check_term_top g e topt must_tot gh ctx with - | Inl (et, g) -> Inl (et, g) - | Inr err -> Inr err) + | Success (et, g) -> Success (et, g) + | Error err -> Error err) None "FStar.TypeChecker.Core.check_term_top" in ( let res = match res with - | Inl (et, Some guard0) -> + | Success (et, Some guard0) -> // Options.push(); // Options.set_option "debug_level" (Options.List [Options.String "Unfolding"]); let guard = N.normalize simplify_steps g guard0 in @@ -1887,16 +1890,16 @@ let check_term_top_gh g e topt (must_tot:bool) (gh:option guard_handler_t) BU.print1 "WARNING: %s is free in the core generated guard\n" (P.term_to_string (S.bv_to_name bv)) | _ -> () end; - Inl (et, Some guard) + Success (et, Some guard) - | Inl _ -> + | Success _ -> if Env.debug g (Options.Other "Core") || Env.debug g (Options.Other "CoreTop") then BU.print1 "(%s) Exiting core (ok)\n" (BU.string_of_int (get_goal_ctr())); res - | Inr _ -> + | Error _ -> if Env.debug g (Options.Other "Core") || Env.debug g (Options.Other "CoreTop") then BU.print1 "(%s) Exiting core (failed)\n" @@ -1916,22 +1919,22 @@ let check_term_top_gh g e topt (must_tot:bool) (gh:option guard_handler_t) let check_term g e t must_tot = match check_term_top_gh g e (Some t) must_tot None with - | Inl (_, g) -> Inl g - | Inr err -> Inr err + | Success (_, g) -> Inl g + | Error err -> Inr err let check_term_at_type g e t = let must_tot = false in match check_term_top_gh g e (Some t) must_tot None with - | Inl ((eff, _), g) -> Inl (eff, g) - | Inr err -> Inr err + | Success ((eff, _), g) -> Inl (eff, g) + | Error err -> Inr err let compute_term_type_handle_guards g e gh = let e = FStar.Syntax.Compress.deep_compress true true e in let must_tot = false in match check_term_top_gh g e None must_tot (Some gh) with - | Inl (r, None) -> Inl r - | Inl (_, Some _) -> failwith "Impossible: All guards should have been handled already" - | Inr err -> Inr err + | Success (r, None) -> Inl r + | Success (_, Some _) -> failwith "Impossible: All guards should have been handled already" + | Error err -> Inr err let open_binders_in_term (env:Env.env) (bs:binders) (t:term) = let g = initial_env env None in @@ -1947,19 +1950,20 @@ let check_term_equality g t0 t1 = let g = initial_env g None in if Env.debug g.tcenv (Options.Other "CoreTop") then BU.print2 "Entering check_term_equality with %s and %s {\n" (show t0) (show t1); - let ctx = { no_guard = false; error_context = [("Eq", None)] } in - let r = - match check_relation g EQUALITY t0 t1 ctx with - | Inl (_, g) -> Inl g - | Inr err -> Inr err - in + let ctx = { no_guard = false ; error_context = [("Eq", None)] } in + let r = check_relation g EQUALITY t0 t1 ctx in if Env.debug g.tcenv (Options.Other "CoreTop") then BU.print3 "} Exiting check_term_equality (%s, %s). Result = %s.\n" (show t0) (show t1) (show r); + let r = + match r with + | Success (_, g) -> Inl g + | Error err -> Inr err + in r let check_term_subtyping g t0 t1 = let g = initial_env g None in let ctx = { no_guard = false; error_context = [("Subtyping", None)] } in match check_relation g (SUBTYPING None) t0 t1 ctx with - | Inl (_, g) -> Inl g - | Inr err -> Inr err + | Success (_, g) -> Inl g + | Error err -> Inr err