From 30b157a85e65ff1599fecfc2c96d43d9637e00d8 Mon Sep 17 00:00:00 2001 From: Dhruv Makwana Date: Sun, 29 Dec 2024 17:10:27 +0000 Subject: [PATCH] CN: Remove WellTyped.Exposed and simplify intf This commit adds a slightly unfortunate wellTyped_intf.ml file so that the signatures contained therein can be use from multiple places. --- backend/cn/lib/typing.mli | 2 +- backend/cn/lib/wellTyped.ml | 99 ++++++++++--------- backend/cn/lib/wellTyped.mli | 6 +- backend/cn/lib/{sigs.ml => wellTyped_intf.ml} | 53 +--------- 4 files changed, 54 insertions(+), 106 deletions(-) rename backend/cn/lib/{sigs.ml => wellTyped_intf.ml} (59%) diff --git a/backend/cn/lib/typing.mli b/backend/cn/lib/typing.mli index 3152e5ec3..e1e70e213 100644 --- a/backend/cn/lib/typing.mli +++ b/backend/cn/lib/typing.mli @@ -189,4 +189,4 @@ val modify_where : (Where.t -> Where.t) -> unit m val init_solver : unit -> unit m -module WellTyped : Sigs.Exposed with type 'a t = 'a t +module WellTyped : WellTyped_intf.S with type 'a t = 'a t diff --git a/backend/cn/lib/wellTyped.ml b/backend/cn/lib/wellTyped.ml index d1a0eee8f..14222bec2 100644 --- a/backend/cn/lib/wellTyped.ml +++ b/backend/cn/lib/wellTyped.ml @@ -9,8 +9,10 @@ let squotes, warn, dot, string, debug, item, colon, comma = Pp.(squotes, warn, dot, string, debug, item, colon, comma) +type 'a t = Context.t -> ('a * Context.t) Or_TypeError.t + module GlobalReader = struct - type 'a t = Context.t -> ('a * Context.t) Or_TypeError.t + type nonrec 'a t = 'a t let return x s = Ok (x, s) @@ -127,13 +129,15 @@ module NoSolver = struct let lift = function Ok x -> return x | Error x -> fail x + + let run ctxt x = x ctxt end let use_ity = ref true open NoSolver -let fail typeErr = fail (NoSolver.liftFail typeErr) +let fail typeErr = fail (liftFail typeErr) open Effectful.Make (NoSolver) @@ -2470,49 +2474,47 @@ module WDT = struct return sccs end -module Exposed = struct - let datatype = WDT.welltyped +let datatype = WDT.welltyped - let datatype_recursion = WDT.check_recursion_ok +let datatype_recursion = WDT.check_recursion_ok - let lemma = WLemma.welltyped +let lemma = WLemma.welltyped - let function_ = WLFD.welltyped +let function_ = WLFD.welltyped - let predicate = WRPD.welltyped +let predicate = WRPD.welltyped - let label_context = WProc.label_context +let label_context = WProc.label_context - let to_argument_type = WProc.typ +let to_argument_type = WProc.typ - let procedure = WProc.welltyped +let procedure = WProc.welltyped - let integer_annot = BaseTyping.integer_annot +let integer_annot = BaseTyping.integer_annot - let infer_expr = BaseTyping.infer_expr +let infer_expr = BaseTyping.infer_expr - let check_expr = BaseTyping.check_expr +let check_expr = BaseTyping.check_expr - let function_type = WFT.welltyped +let function_type = WFT.welltyped - let logical_constraint = WLC.welltyped +let logical_constraint = WLC.welltyped - let oarg_bt_of_pred = WRS.oarg_bt_of_pred +let oarg_bt_of_pred = WRS.oarg_bt_of_pred - let default_quantifier_bt = quantifier_bt +let default_quantifier_bt = quantifier_bt - let infer_term = WIT.infer +let infer_term = WIT.infer - let check_term = WIT.check +let check_term = WIT.check - let check_ct = WCT.is_ct +let check_ct = WCT.is_ct - let compare_by_fst_id = compare_by_fst_id +let compare_by_fst_id = compare_by_fst_id - let ensure_same_argument_number = ensure_same_argument_number +let ensure_same_argument_number = ensure_same_argument_number - let ensure_bits_type = ensure_bits_type -end +let ensure_bits_type = ensure_bits_type module type ErrorReader = sig type 'a t @@ -2530,12 +2532,12 @@ module type ErrorReader = sig val lift : 'a Or_TypeError.t -> 'a t end -module Lift (M : ErrorReader) : Sigs.Exposed with type 'a t := 'a M.t = struct +module Lift (M : ErrorReader) : WellTyped_intf.S with type 'a t := 'a M.t = struct let lift1 f x = let ( let@ ) = M.bind in let@ state = M.get () in let context = M.to_context state in - M.lift (Result.map fst (f x context)) + M.lift (Result.map fst (run context (f x))) let lift2 f x y = @@ -2552,51 +2554,50 @@ module Lift (M : ErrorReader) : Sigs.Exposed with type 'a t := 'a M.t = struct M.lift (Result.map fst (f x y z context)) - let datatype x = lift1 Exposed.datatype x + let datatype x = lift1 datatype x - let datatype_recursion = lift1 Exposed.datatype_recursion + let datatype_recursion = lift1 datatype_recursion - let lemma x y z = lift3 Exposed.lemma x y z + let lemma x y z = lift3 lemma x y z - let function_ = lift1 Exposed.function_ + let function_ = lift1 function_ - let predicate = lift1 Exposed.predicate + let predicate = lift1 predicate - let label_context = Exposed.label_context + let label_context = label_context - let to_argument_type = Exposed.to_argument_type + let to_argument_type = to_argument_type - let procedure x y = lift2 Exposed.procedure x y + let procedure x y = lift2 procedure x y - let integer_annot = Exposed.integer_annot + let integer_annot = integer_annot - let infer_expr x y = lift2 Exposed.infer_expr x y + let infer_expr x y = lift2 infer_expr x y - let check_expr x y z = lift3 Exposed.check_expr x y z + let check_expr x y z = lift3 check_expr x y z - let function_type = lift3 Exposed.function_type + let function_type = lift3 function_type - let logical_constraint = lift2 Exposed.logical_constraint + let logical_constraint = lift2 logical_constraint - let oarg_bt_of_pred = lift2 Exposed.oarg_bt_of_pred + let oarg_bt_of_pred = lift2 oarg_bt_of_pred - let default_quantifier_bt = Exposed.default_quantifier_bt + let default_quantifier_bt = default_quantifier_bt - let infer_term x = lift1 Exposed.infer_term x + let infer_term x = lift1 infer_term x - let check_term x y z = lift3 Exposed.check_term x y z + let check_term x y z = lift3 check_term x y z - let check_ct = lift2 Exposed.check_ct + let check_ct = lift2 check_ct - let compare_by_fst_id = Exposed.compare_by_fst_id + let compare_by_fst_id = compare_by_fst_id let ensure_same_argument_number loc type_ n ~expect = let ( let@ ) = M.bind in let@ state = M.get () in let context = M.to_context state in - M.lift - (Result.map fst (Exposed.ensure_same_argument_number loc type_ n ~expect context)) + M.lift (Result.map fst (ensure_same_argument_number loc type_ n ~expect context)) - let ensure_bits_type = lift2 Exposed.ensure_bits_type + let ensure_bits_type = lift2 ensure_bits_type end diff --git a/backend/cn/lib/wellTyped.mli b/backend/cn/lib/wellTyped.mli index ef35fc3a2..762140161 100644 --- a/backend/cn/lib/wellTyped.mli +++ b/backend/cn/lib/wellTyped.mli @@ -1,8 +1,6 @@ val use_ity : bool ref -module NoSolver : Sigs.NoSolver - -module Exposed : Sigs.Exposed with type 'a t := 'a NoSolver.t +include WellTyped_intf.S module type ErrorReader = sig type 'a t @@ -20,4 +18,4 @@ module type ErrorReader = sig val lift : 'a Or_TypeError.t -> 'a t end -module Lift : functor (M : ErrorReader) -> Sigs.Exposed with type 'a t := 'a M.t +module Lift : functor (M : ErrorReader) -> WellTyped_intf.S with type 'a t := 'a M.t diff --git a/backend/cn/lib/sigs.ml b/backend/cn/lib/wellTyped_intf.ml similarity index 59% rename from backend/cn/lib/sigs.ml rename to backend/cn/lib/wellTyped_intf.ml index 60ab762a0..f16432e1a 100644 --- a/backend/cn/lib/sigs.ml +++ b/backend/cn/lib/wellTyped_intf.ml @@ -1,55 +1,4 @@ -module type NoSolver = sig - type 'a t - - type failure - - val return : 'a -> 'a t - - val bind : 'a t -> ('a -> 'b t) -> 'b t - - val pure : 'a t -> 'a t - - val liftFail : TypeErrors.t -> failure - - val fail : failure -> 'a t - - val bound_a : Sym.t -> bool t - - val bound_l : Sym.t -> bool t - - val get_a : Sym.t -> Context.basetype_or_value t - - val get_l : Sym.t -> Context.basetype_or_value t - - val add_a : Sym.t -> BaseTypes.t -> Context.l_info -> unit t - - val add_l : Sym.t -> BaseTypes.t -> Context.l_info -> unit t - - val get_struct_decl : Locations.t -> Sym.t -> Memory.struct_layout t - - val get_struct_member_type : Locations.t -> Sym.t -> Id.t -> Sctypes.ctype t - - val get_datatype : Locations.t -> Sym.t -> BaseTypes.dt_info t - - val get_datatype_constr : Locations.t -> Sym.t -> BaseTypes.constr_info t - - val get_resource_predicate_def : Locations.t -> Sym.t -> Definition.Predicate.t t - - val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.t t - - val get_lemma : Locations.t -> Sym.t -> (Locations.t * ArgumentTypes.lemmat) t - - val get_fun_decl - : Locations.t -> - Sym.t -> - (Locations.t * ArgumentTypes.ft option * Sctypes.c_concrete_sig) t - - val ensure_base_type : Locations.t -> expect:BaseTypes.t -> BaseTypes.t -> unit t - - val lift : 'a Or_TypeError.t -> 'a t -end - -module type Exposed = sig +module type S = sig type 'a t val ensure_bits_type : Locations.t -> BaseTypes.t -> unit t