From fc90b349e9d11ae0d64e23a3c2212c6996586839 Mon Sep 17 00:00:00 2001 From: agle Date: Thu, 9 Jul 2026 18:01:51 +1000 Subject: [PATCH 01/22] wip hm type inference pass --- examples | 2 +- lib/lang/dune | 3 + lib/lang/hm.ml | 724 +++++++++++++++++++++++++++++++++++++++++- lib/lang/procedure.ml | 16 +- lib/lang/program.mli | 6 +- lib/lang/typeExpr.ml | 204 ++++++++++++ lib/passes.ml | 9 + 7 files changed, 944 insertions(+), 20 deletions(-) create mode 100644 lib/lang/typeExpr.ml diff --git a/examples b/examples index 339b7c48..da590450 160000 --- a/examples +++ b/examples @@ -1 +1 @@ -Subproject commit 339b7c483383d3c73af612dc5e612a4d4252b599 +Subproject commit da5904507e8dff136686a1c6da94d09d6baa127e diff --git a/lib/lang/dune b/lib/lang/dune index e2cd189a..f946163e 100644 --- a/lib/lang/dune +++ b/lib/lang/dune @@ -2,6 +2,7 @@ (public_name bincaml.ast) (name lang) (modules + hm abstract_expr attrib spec_modifies @@ -9,6 +10,7 @@ expr algsimp common + typeExpr ops viscfg expr_smt @@ -19,6 +21,7 @@ interp program) (libraries + unionFind zarith fix ocamlgraph diff --git a/lib/lang/hm.ml b/lib/lang/hm.ml index 3f71d220..b96206e9 100644 --- a/lib/lang/hm.ml +++ b/lib/lang/hm.ml @@ -1,10 +1,716 @@ -module Type = struct - type t = - | BVVar of string - | Int - | BV of int - | Bool - | Var of string - | Sort of string - | Fun of t * t +open Common +open UnionFind +open Abstract_expr + +(** Hindley-Milner type inference based on a union-find. *) + +module TypeInference (T : TypeExpr.TypeContext) = struct + open TypeExpr + include T + open Typ + + let printer_alg = function + | Var e -> ID.to_string e + | TypeConstr ([ l ], e) -> l ^ " " ^ e + | TypeConstr ([ a; b ], "->") -> a ^ " -> " ^ b + | TypeConstr ([], e) -> e + | TypeConstr (ls, e) -> + List.to_string ~start:"(" ~stop:")" ~sep:"," Fun.id ls ^ " " ^ e + + let type_to_string t = Rec.cata printer_alg t + + let occurs_in a b = + let check = function + | Var t -> equal_tvar t a + | TypeConstr (ls, _) -> List.fold_left ( || ) false ls + in + Rec.cata check b + + let tmod_const a = TypeConstr ([ a ], "const") + let tmod_shared a = TypeConstr ([ a ], "shared") + let fun_type a b = TypeConstr ([ a; b ], "->") + let int_type = TypeConstr ([], "int") + let nat_val_type i = TypeConstr ([], Int.to_string i) + let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") + let bvunk i = TypeConstr ([ Var i ], "bv") + let bool_type = TypeConstr ([], "bool") + let unit_t = TypeConstr ([], "unit") + let top_t = TypeConstr ([], "top") + let nothing_t = TypeConstr ([], "nothing") + let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") + let ptr_typ = bv_type 64 + + let rec to_basil (t : t) : Types.t = + let open Types in + match unfix t with + | TypeConstr ([ a; b ], "->") -> Map (to_basil a, to_basil b) + | TypeConstr ([ w ], "bv") -> ( + match unfix w with + | TypeConstr ([], a) -> ( + match Int.of_string a with + | Some i -> Bitvector i + | None -> Sort (a ^ "bv", [])) + | _ -> failwith "generic bv") + | TypeConstr ([], "unit") -> Unit + | TypeConstr ([], "bool") -> Boolean + | TypeConstr ([], "int") -> Integer + | TypeConstr ([], "top") -> Top + | TypeConstr ([], "nothing") -> Nothing + | TypeConstr ([], o) -> Sort (o, []) + | _ -> failwith "not impl" + + type scheme = Forall of tvar list * t + + let scheme_to_string = function + | Forall (tl, t) -> + List.to_string ID.to_string tl ^ ". " ^ type_to_string (find t) + + module U = UnionFind + + let plpos (l : Lexing.position) = + Printf.sprintf "%s:%d" l.pos_fname l.pos_lnum + + exception TypeErr of string + + let type_error a b = + let a = find a in + let b = find b in + raise + (TypeErr ("type_error: " ^ type_to_string a ^ " <> " ^ type_to_string b)) + + (** Type unification.*) + let rec unify ?(pos = Lexing.dummy_pos) t t' = + Logs.debug (fun m -> + m "%s" + ("unify: " ^ plpos pos ^ " " + ^ type_to_string (find t) + ^ " with " + ^ type_to_string (find t'))); + match (map_expr unfix @@ Typ.unfix t, map_expr unfix @@ Typ.unfix t') with + | TypeConstr ([], "nothing"), _ -> t + | _, TypeConstr ([], "nothing") -> t' + | Var x, Var y -> union t t' + | Var x, _ when occurs_in x t' -> failwith "recursive type" + | Var _, TypeConstr _ -> merge (fun a b -> b) t t' + | _, Var x -> unify ~pos:[%here] t' t + | TypeConstr ([ a ], "const"), TypeConstr ([ b ], "const") -> + let x = unify ~pos:[%here] (fix a) (fix b) in + fix @@ TypeConstr ([ x ], "const") + | TypeConstr ([ a ], "shared"), TypeConstr ([ b ], "shared") -> + let x = unify ~pos:[%here] (fix a) (fix b) in + fix @@ TypeConstr ([ x ], "const") + | o, TypeConstr ([ b ], "shared") | o, TypeConstr ([ b ], "const") -> + unify ~pos:[%here] t' t + | TypeConstr ([ b ], "shared"), o -> + let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in + fix @@ TypeConstr ([ b ], "shared") + | TypeConstr ([ b ], "const"), o -> + let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in + fix @@ TypeConstr ([ b ], "const") + | TypeConstr (ars, n), TypeConstr (ars', n') when not (String.equal n n') -> + type_error t t' + | TypeConstr (ars, n), TypeConstr (ars', n') + when List.length ars <> List.length ars' -> + type_error t t' + | ( TypeConstr ([ (Var v as vr) ], "bv"), + TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv") ) + | ( TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv"), + TypeConstr ([ (Var v as vr) ], "bv") ) -> + (* prioritise bitvec consts *) + let v = merge (fun _ c -> c) (fix vr) (fix cst) in + fix @@ TypeConstr ([ v ], "bv") + | TypeConstr (ars, n), TypeConstr (ars', n') -> + let args = + List.combine ars ars' + |> List.map (fun (a, b) -> unify ~pos:[%here] (fix a) (fix b)) + in + merge (fun a b -> TypeConstr (args, n)) t t' + + let gen = ID.make_gen () + let bv_type i = bv_type i + let bvunk i = map_expr fix @@ TypeConstr ([ Var i ], "bv") + + let rec ty_of_basil (t : Types.t) : t = + let e = + match t with + | Types.Boolean -> bool_type + | Types.Integer -> int_type + | Types.Bitvector i -> bv_type i + | Types.Unit -> unit_t + | Types.Top -> top_t + | Types.Nothing -> nothing_t + | Types.Map (a, b) -> fun_type (ty_of_basil a) (ty_of_basil b) + | Types.Sort (n, _) -> TypeConstr ([], n) + | Types.Struct _ -> failwith "unsupp" + | Types.Pointer { lower; upper } -> + ptr_typ_sub (ty_of_basil lower) (ty_of_basil upper) + | Types.Variable n -> Var (gen.fresh ~name:n ()) + in + fix e + + let curry (args : t expr list) (v : t expr) = + List.fold_left (fun a p -> fix @@ fun_type (fix p) a) (fix v) args + + let curry_f (args : t list) (v : t) = + List.fold_left (fun a p -> fix @@ fun_type p a) v args + + (** Return the generic type scheme for an op. We generalise the type, and hope + dearly that a concrete type is found by inference. + + TODO: some approach like weak type variables that makes it a type error to + fail to instantiate. *) + let scheme_of_op (gen : ID.generator) + (o : [ Ops.AllOps.const | Ops.AllOps.unary | Ops.AllOps.binary ]) = + let fv () = gen.fresh ~name:"ɑ" () in + match o with + | `Extract (hi, lo) -> curry [ bvunk (fv ()) ] (bv_type (hi - lo)) + | `SignExtend bits -> curry [ bvunk (fv ()) ] (bvunk (fv ())) + | `ZeroExtend bits -> curry [ bvunk (fv ()) ] (bvunk (fv ())) + | `BOOLTOBV1 -> curry [ bool_type ] (bv_type 1) + | `Bitvector b -> fix @@ bv_type (Bitvec.size b) + | #Ops.BVOps.binary_unif -> + let a = fv () in + curry [ bvunk a; bvunk a ] (bvunk a) + | #Ops.BVOps.binary_pred -> + let a = fv () in + curry [ bvunk a; bvunk a ] bool_type + | #Ops.BVOps.unary_unif -> + let a = fv () in + curry [ bvunk a ] (bvunk a) + | `INTNEG -> curry [ int_type ] int_type + | #Ops.IntOps.binary_pred -> curry [ int_type; int_type ] bool_type + | #Ops.IntOps.const -> fix @@ int_type + | #Ops.IntOps.binary_unif -> curry [ int_type; int_type ] bool_type + | #Ops.LogicalOps.binary -> curry [ bool_type; bool_type ] bool_type + | #Ops.LogicalOps.unary -> curry [ bool_type ] bool_type + | #Ops.LogicalOps.const -> fix @@ bool_type + | `Old -> fix @@ Var (fv ()) + | #Ops.AllOps.binary as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + | #Ops.AllOps.unary as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + | #Ops.AllOps.const as o -> + failwith @@ "unsupported op" ^ Ops.AllOps.to_string o + + (** return the generic type scheme of an intrinsic operation *) + let scheme_of_intrin (gen : ID.generator) (o : Ops.AllOps.intrin) args = + let fv () = gen.fresh ~name:"ɑ" () in + match o with + | `BVADD | `BVMUL | `BVOR | `BVXOR | `BVAND -> + let a = fv () in + curry (List.init args (fun _ -> Var a)) (Var a) + | `BVConcat -> curry (List.init args (fun _ -> Var (fv ()))) (Var (fv ())) + | `OR | `AND -> curry (List.init args (fun _ -> bool_type)) bool_type + | `MapUpdate -> + let a = fv () in + let b = fv () in + let m = curry [ Var a ] (Var b) in + curry_f [ m; fix @@ Var a; fix @@ Var b ] m + | `Cases -> fix @@ Var (fv ()) + + (* instantiate typescheme for a single type-annotated variable *) + let inst_annot_v ?(no_constraint = false) v = + let ty = + match Var.typ v with + | _ when no_constraint -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | Nothing -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | o -> ty_of_basil o + in + ty + + (* lookup var and add unify with its type annotation *) + let lookup_var_typ univ ?(no_constraint = false) c v = + let vt = inst_annot_v v in + let a = + let v = V.of_var univ v in + TCtx.find_opt v c |> function + | Some v -> v + | None -> failwith ("var not found: " ^ V.to_string v) + in + let tt = match a with Forall (_, ty) -> union ty vt in + tt + + type typ = t [@@deriving eq, ord] + + module AbsTypingExpr = struct + open Ops + include AllOps + module Var = Var + + type var = Var.t + + type t = E of (const, Var.t, unary, binary, intrin, typ, t) AbstractExpr.t + [@@unboxed] [@@deriving eq, ord] + + type nonrec typ = typ + + let top_typ = fix @@ top_t + let fix i = E i + let unfix i = match i with E i -> i + end + + module TypingExpr = Expr.Make (AbsTypingExpr) + + let getty = AbsTypingExpr.unfix %> Expr.AbstractExpr.get_typ + + let infer_var univ ctx id = + let typ = lookup_var_typ univ ctx id in + (id, typ) + + let do_infer + (infer : + univ:string -> + Lexing.position -> + Program.e -> + scheme TCtx.t -> + AbsTypingExpr.t) univ hr e c : AbsTypingExpr.t = + let mkv v = V.of_var univ v in + let r = fix @@ Var (gen.fresh ()) in + let open Abstract_expr.AbstractExpr in + let e = Expr.BasilExpr.unfix e in + let e = set_typ e r in + match e with + | RVar { id; attrib } -> + let typ = lookup_var_typ univ c id in + AbsTypingExpr.fix (RVar { attrib; id; typ }) + | Lambda { op; bound_vars; in_body; attrib; triggers } -> begin + let tvars = List.map (fun v -> (v, inst_annot_v v)) bound_vars in + let ictx = + List.map (fun (v, t) -> (mkv v, Forall ([], t))) tvars + |> TCtx.add_list c + in + let bdty = infer ~univ [%here] in_body ictx in + let typ = + match op with + | `Lambda -> getty bdty + | `Forall | `Exists -> unify (getty bdty) (fix bool_type) + in + ignore @@ unify r (curry_f (List.map snd tvars) (getty bdty)); + let triggers = + List.map (List.map (fun e -> infer ~univ [%here] e ictx)) triggers + in + AbsTypingExpr.fix + (Lambda { op; bound_vars; in_body = bdty; attrib; typ; triggers }) + end + | Constant { const = #Ops.AllOps.const as op; attrib } -> begin + let f = scheme_of_op gen op in + let r = unify r f in + AbsTypingExpr.fix (Constant { typ = r; const = op; attrib }) + end + | UnaryExpr { op = #Ops.AllOps.unary as op; arg; attrib } -> begin + let f = scheme_of_op gen op in + let arg = infer ~univ [%here] arg c in + ignore @@ unify f (curry_f [ getty arg ] r); + AbsTypingExpr.fix (UnaryExpr { typ = r; op; attrib; arg }) + end + | BinaryExpr { op = #Ops.AllOps.binary as op; arg1; arg2; attrib } -> begin + let f = scheme_of_op gen op in + let arg1 = infer ~univ [%here] arg1 c in + let arg2 = infer ~univ [%here] arg2 c in + ignore @@ unify f (curry_f [ getty arg1; getty arg2 ] r); + AbsTypingExpr.fix (BinaryExpr { typ = r; op; attrib; arg1; arg2 }) + end + | ApplyIntrin { op = #Ops.AllOps.intrin as op; args; attrib } -> begin + let f = scheme_of_intrin gen op (List.length args) in + let args = List.map (fun a -> infer ~univ [%here] a c) args in + ignore @@ unify f (curry_f (List.map getty args) r); + AbsTypingExpr.fix (ApplyIntrin { typ = r; op; attrib; args }) + end + | ApplyFun { func; args; attrib } -> + let f = infer ~univ [%here] func c in + let args = List.map (fun a -> infer ~univ [%here] a c) args in + ignore @@ unify (getty f) (curry_f (List.map getty args) r); + AbsTypingExpr.fix (ApplyFun { typ = r; func = f; attrib; args }) + | Let _ -> failwith "" + + let types_universe = "" + let global_universe = "" + + let decl_type ctx name vt = + let tvar = V.create types_universe name in + TCtx.update tvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + ctx + + let decl_var_typ univ ?(no_constraint = false) c v = + let vvar = V.of_var univ v in + let vt = inst_annot_v v in + TCtx.update vvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + c + + let rec infer_ty ~univ (hr : Lexing.position) e = + fun (c : scheme TCtx.t) -> + Logs.debug (fun m -> + m "%s" @@ "infer " ^ plpos hr ^ " " ^ Expr.BasilExpr.to_string e); + let t = + try do_infer infer_ty univ hr e c + with TypeErr m -> + raise (TypeErr (m ^ " : " ^ Expr.BasilExpr.to_string e)) + in + t + + let infer ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = + infer_ty ~univ hr e c |> AbsTypingExpr.unfix |> AbstractExpr.get_typ + + let retype_var univ ctx id = + lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil + |> fun typ -> Var.copy ~typ id + + (** Extract type after full inference has run. *) + let elaborate_expr ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = + let alg e = + let e = + match e with + | AbstractExpr.RVar { id; attrib; typ } -> + (* FIXME: bad to have two type annotations *) + let id = retype_var univ c id in + AbstractExpr.RVar { id; attrib; typ } + | o -> o + in + let t = AbstractExpr.get_typ e |> find |> to_basil in + AbstractExpr.set_typ e t |> Expr.BasilExpr.fix + in + e |> TypingExpr.cata alg + + let unfix i = match i with Expr.BasilExpr.E i -> i + let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e + + let infer_phi univ ctx (p : Var.t Block.phi list) = + let open Block in + let r = fix @@ Var (gen.fresh ()) in + List.fold_left + (fun acc { lhs; rhs } -> + let lhs = infer [%here] ~univ (Expr.BasilExpr.rvar lhs) ctx in + let e = + List.fold_left + (fun a (_, r) -> + let r = infer [%here] ~univ (Expr.BasilExpr.rvar r) ctx in + unify a r) + lhs rhs + in + unify acc e) + r p + + let elaborate_phi univ ctx (p : Var.t Block.phi list) = + let open Block in + List.map + (fun { lhs; rhs } -> + let lhs = retype_var univ ctx lhs in + let rhs = List.map (fun (a, r) -> (a, retype_var univ ctx r)) rhs in + { lhs; rhs }) + p + + let ctx_to_string ctx = + TCtx.to_iter ctx + |> Iter.to_string (fun (a, b) -> + Printf.sprintf "%s %s" (V.to_string a) (scheme_to_string b)) + + let fresh_tvar ?(n = "a") () = fix @@ Var (gen.fresh ~name:n ()) + + let do_infer_stmt p univ ctx stmt = + let open Stmt in + let infer_ty h e = infer_ty ~univ h e ctx in + + (*let r = fix @@ Var (gen.fresh ()) in*) + match stmt with + | Instr_IntrinCall _ -> failwith "intrin unsupported" + | Instr_Assume { body; branch; attrib } -> + let body = infer_ty [%here] body in + ignore @@ unify (fix bool_type) (getty body); + Instr_Assume { body; branch; attrib } + | Instr_Assert { body; attrib } -> + let body = infer_ty [%here] body in + ignore @@ unify (fix bool_type) (getty body); + Instr_Assert { body; attrib } + | Instr_Assign { al = ls; attrib } -> + let ls = List.map (fun (l, r) -> (l, infer_ty [%here] r)) ls in + List.iter + (fun (l, r) -> + ignore + @@ unify (infer ~univ [%here] (Expr.BasilExpr.rvar l) ctx) (getty r)) + ls; + Instr_Assign { al = ls; attrib } + | Instr_Call { lhs; procid; args; attrib } -> + let p = Program.proc p procid in + let infer_param p = + infer ~univ:(V.proc_univ procid) [%here] (Expr.BasilExpr.rvar p) ctx + in + let args = StringMap.mapi (fun param a -> infer_ty [%here] a) args in + StringMap.iter + (fun parm act -> + let form = + infer_param (StringMap.find parm (Procedure.formal_in_params p)) + in + ignore @@ unify form (getty act)) + args; + lhs + |> StringMap.map (fun a -> infer_ty [%here] (Expr.BasilExpr.rvar a)) + |> StringMap.iter (fun param act -> + let form = + infer_param (StringMap.find param @@ Procedure.formal_out_params p) + in + ignore @@ unify form (getty act)); + Instr_Call { lhs; procid; args; attrib } + | Instr_IndirectCall { target; attrib } -> + let target = infer_ty [%here] target in + ignore @@ unify (getty target) (fix ptr_typ); + Instr_IndirectCall { target; attrib } + | Instr_Load { lhs; rhs; addr = Scalar; attrib } -> + let lhs' = infer_ty [%here] (Expr.BasilExpr.rvar lhs) in + let rhs' = infer_ty [%here] (Expr.BasilExpr.rvar rhs) in + let _ = unify (getty lhs') (getty rhs') in + Instr_Load { lhs; rhs; addr = Scalar; attrib } + | Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } -> + let addr = infer_ty [%here] addr in + let _ = unify (fix @@ ptr_typ) (getty addr) in + let mapt = fix @@ fun_type (getty addr) (fresh_tvar ()) in + let _ = unify (lookup_var_typ univ ctx rhs) mapt in + let _ = + unify + (infer_ty [%here] (Expr.BasilExpr.rvar lhs) |> getty) + (fix @@ bv_type size) + in + Instr_Load { lhs; rhs; addr = Addr { addr; size; endian }; attrib } + | Instr_Store { lhs; rhs; value; addr = Scalar; attrib } -> + let value = infer_ty [%here] value in + let _ = + unify (getty value) + @@ unify + (infer ~univ [%here] (Expr.BasilExpr.rvar lhs) ctx) + (infer ~univ [%here] (Expr.BasilExpr.rvar rhs) ctx) + in + Instr_Store { lhs; rhs; value; addr = Scalar; attrib } + | Instr_Store + { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } -> + let addr = infer_ty [%here] addr in + let _ = unify (fix @@ ptr_typ) (getty addr) in + let mapt = fix @@ fun_type (getty addr) (fresh_tvar ()) in + let _ = + unify mapt (infer ~univ [%here] (Expr.BasilExpr.rvar lhs) ctx) + in + let _ = unify (lookup_var_typ univ ctx rhs) mapt in + let value = infer_ty [%here] value in + let _ = unify (getty value) (fix @@ bv_type size) in + Instr_Store + { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } + + let elaborate_stmt univ ctx stmt = + let retype_var v = + let typ = + lookup_var_typ ~no_constraint:true univ ctx v |> find |> to_basil + in + Var.copy ~typ v + in + Stmt.map + ~f_expr:(fun e -> elaborate_expr ~univ [%here] e ctx) + ~f_lvar:retype_var ~f_rvar:retype_var stmt + + let infer_stmt p univ ctx s = + try do_infer_stmt p univ ctx s + with TypeErr m -> + raise + (TypeErr + (m ^ " " + ^ Stmt.to_string Var.pretty Var.pretty Expr.BasilExpr.pretty s)) + + let infer_block p univ ctx (b : Program.bloc) = + let _ = infer_phi univ ctx b.phis in + Block.map ~phi:Fun.id (infer_stmt p univ ctx) b + + let elaborate_block p univ ctx (b : ('a, 'b) Block.t) = + Block.map ~phi:(elaborate_phi univ ctx) (elaborate_stmt univ ctx) b + + let assume_proc_decl ctx ?(no_constraint = false) (p : Program.proc) = + let globs = Var.Decls.values (Procedure.local_decls p) in + let formals_in = Procedure.formal_in_params p |> StringMap.values in + let formals_out = Procedure.formal_out_params p |> StringMap.values in + let univ = V.proc_univ @@ Procedure.id p in + let ctx = + Iter.fold + (decl_var_typ ~no_constraint univ) + ctx + (Iter.append globs @@ Iter.append formals_in formals_out) + in + ctx + + let infer_proc prog ctx ?(no_constraint = false) (p : Program.proc) = + let spec = Procedure.specification p in + let univ = V.proc_univ @@ Procedure.id p in + let ibool_list b = + List.map + (fun a -> + let a = infer_ty ~univ [%here] a ctx in + let _ = unify (fix bool_type) (getty a) in + a) + b + in + let spec : ('a, 'b) Procedure.proc_spec = + { + requires = ibool_list spec.requires; + ensures = ibool_list spec.ensures; + rely = ibool_list spec.rely; + guarantee = ibool_list spec.guarantee; + captures_globs = + List.map (infer_var global_universe ctx) spec.captures_globs; + modifies_globs = + List.map (infer_var global_universe ctx) spec.modifies_globs; + } + in + + let new_spec ctx : (Var.t, Expr.BasilExpr.t) Procedure.proc_spec = + { + requires = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.requires; + ensures = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.ensures; + rely = List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.rely; + guarantee = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.guarantee; + captures_globs = spec.captures_globs |> List.map fst; + modifies_globs = spec.modifies_globs |> List.map fst; + } + in + + let ctx = assume_proc_decl ctx ~no_constraint p in + let bvlocks = + Procedure.iter_blocks_topo_fwd p + |> Iter.map (fun (i, b) -> (i, infer_block prog univ ctx b)) + |> Iter.persistent + in + + let elaborate_proc ctx = + Procedure.set_specification p (new_spec ctx) + |> (fun p -> + bvlocks + |> Iter.map (fun (bid, b) -> (bid, elaborate_block [%here] univ ctx b)) + |> Iter.fold (fun p (bid, b) -> Procedure.update_block p bid b) p) + |> Procedure.map_formal_in_params (StringMap.map (retype_var univ ctx)) + |> Procedure.map_formal_out_params (StringMap.map (retype_var univ ctx)) + in + Logs.debug (fun m -> m "%s" (ctx_to_string ctx)); + (elaborate_proc, ctx) + + (** Run type inference on a declaration, returning an updated typing scheme, + and elaboration function*) + let infer_decl prog scheme = + let open Program in + (* We have to be careful that inference is run immediately, not delayed until elaboration. *) + fun (decl_id, d) -> + match d with + | Type { binding; typ } -> + let ty = ty_of_basil typ in + let scheme = decl_type scheme binding ty in + let nty scheme = Type { binding; typ = to_basil (find ty) } in + (scheme, `Decl (decl_id, nty)) + | Function { binding; definition; attrib } -> ( + (* elaboration of var binding *) + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + match definition with + | Axiom b -> + let bt = fix bool_type in + let b = infer_ty ~univ:global_universe [%here] b scheme in + let _ = unify (getty b) bt in + let nb scheme = + Function + { + attrib; + binding = binding scheme; + definition = + Axiom + (elaborate_expr ~univ:global_universe [%here] b scheme); + } + in + (scheme, `Decl (decl_id, nb)) + | Uninterpreted -> + let nu s = + Function + { binding = binding s; attrib; definition = Uninterpreted } + in + (scheme, `Decl (decl_id, nu)) + | Function definition -> + let e = + infer_ty ~univ:global_universe [%here] definition scheme + in + let ne scheme = + Function + { + binding = binding scheme; + attrib; + definition = + Function + (elaborate_expr ~univ:global_universe [%here] e scheme); + } + in + (scheme, `Decl (decl_id, ne))) + | Variable { binding; attrib; classification } -> + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + let classification = + let tyv = + classification + |> Option.map (fun classi -> + infer_ty ~univ:global_universe [%here] classi scheme) + in + fun final_scheme -> + tyv + |> Option.map (fun e -> + elaborate_expr ~univ:global_universe [%here] e final_scheme) + in + let nb fscheme = + Variable + { + binding = binding fscheme; + attrib; + classification = classification fscheme; + } + in + (scheme, `Decl (decl_id, nb)) + | Procedure { definition } -> + let elaborate_proc, scheme = infer_proc prog scheme definition in + (scheme, `Procedure (decl_id, elaborate_proc)) + + (** The function that does everything *) + let infer_program prog = + let decls = Program.declarations prog |> Iter.to_list in + (* We fold the inference context through every declaration and + calling the inference functions, returning an expressions typed with the + type expressions herein. We also return the resulting list of elaboration + functions, which take the final inference context and convert the HM-typed + expressions back to bincaml typed expressions. *) + let scheme, new_decls = + decls |> List.fold_map (infer_decl prog) TCtx.empty + in + let prog = + List.fold_left + (fun prog -> function + | `Decl (id, ndecl) -> + let decl = ndecl scheme in + (* assuming the id is the same (it has to be) *) + Program.update_decl prog decl + | `Procedure (id, nproc) -> + let proc = nproc scheme in + (* assuming the id is the same (it has to be) *) + let prog = Program.update_proc id (fun _ -> Some proc) prog in + prog) + prog new_decls + in + (scheme, prog) + + (**let elaborate_program prog (scheme,new_decls) = *) end + +module T = TypeInference (TypeExpr.Make ()) + +let elaborate prog = + (* We need to create a local typing module in order to get fresh state for the union find and hash cons. *) + let module T = TypeInference (TypeExpr.Make ()) in + let scheme, prog = T.infer_program prog in + prog diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 8b421db7..78c7a68c 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -74,10 +74,10 @@ module WTO = Graph.WeakTopological.Make (G) module RevWTO = Graph.WeakTopological.Make (RevG) type ('v, 'e) proc_spec = { - requires : BasilExpr.t list; - ensures : BasilExpr.t list; - rely : BasilExpr.t list; - guarantee : BasilExpr.t list; + requires : 'e list; + ensures : 'e list; + rely : 'e list; + guarantee : 'e list; captures_globs : 'v list; modifies_globs : 'v list; } @@ -118,10 +118,10 @@ module PG : sig ?formal_out_params:'a StringMap.t -> ?captures_globs:'a list -> ?modifies_globs:'a list -> - ?requires:BasilExpr.t list -> - ?ensures:BasilExpr.t list -> - ?rely:BasilExpr.t list -> - ?guarantee:BasilExpr.t list -> + ?requires:'b list -> + ?ensures:'b list -> + ?rely:'b list -> + ?guarantee:'b list -> ?attrib:Attrib.attrib_map -> unit -> ('a, 'b) t diff --git a/lib/lang/program.mli b/lib/lang/program.mli index ea49abae..c7b77560 100644 --- a/lib/lang/program.mli +++ b/lib/lang/program.mli @@ -51,7 +51,7 @@ type declaration = | Procedure of { definition : proc } val decl_binding : declaration -> string -val pretty_proc : (Var.t, 'a) Procedure.t -> Containers_pp.t +val pretty_proc : (Var.t, Expr.BasilExpr.t) Procedure.t -> Containers_pp.t val pretty_declaration : declaration -> Containers_pp.t type t @@ -90,7 +90,9 @@ val update_proc : t -> t -val output_proc_pretty : out_channel -> (Var.t, 'a) Procedure.t -> unit +val output_proc_pretty : + out_channel -> (Var.t, Expr.BasilExpr.t) Procedure.t -> unit + val prog_pretty : t -> Containers_pp.t val declarations : t -> (ID.t * declaration) CCMap.iter val filter_decls : (ID.t -> declaration -> bool) -> t -> t diff --git a/lib/lang/typeExpr.ml b/lib/lang/typeExpr.ml new file mode 100644 index 00000000..15115e49 --- /dev/null +++ b/lib/lang/typeExpr.ml @@ -0,0 +1,204 @@ +(** Hash-consed (interned) type expresions with recusion schemes. *) + +open Common +open UnionFind + +type 'a tycon = 'a list * 'a +type variance = Cov | Contr | Inv +type tvar = ID.t [@@deriving eq, ord, show] + +(** Type scoping is handled by "universe" name strings. Hash consing enables + types to be canonically identified by their representation, then looked up + in the union-find datastructure. The union-find datastructrure is used for + type equivalence/unification solving. *) + +module V = struct + (** scoped type variables *) + + type t = { univ : string; v : string } [@@deriving eq, ord, show] + + let hash { univ; v } = Hash.pair Hash.string Hash.string (univ, v) + let to_string { univ; v } = univ ^ "::" ^ v + let local_univ = "" + let global_univ = "" + let proc_univ p = ID.to_string p + let create univ v = { univ; v } + + let of_var univ v = + if Var.is_global v then { univ = global_univ; v = Var.name v } + else { univ; v = Var.name v } +end + +module TCtx = Map.Make (V) + +(** unfixed type expression *) +module ATyp = struct + type 'a expr = Var of tvar | TypeConstr of 'a list * string + [@@deriving eq, ord, show, map, fold] + + let hash he = function + | Var v -> ID.hash v + | TypeConstr (l, t) -> Hash.pair (Hash.list he) Hash.string (l, t) +end + +(** Type of mutable type context union find *) +module type TypeContext = sig + val compare : 'a Fix.HashCons.cell -> 'a Fix.HashCons.cell -> int + val equal : 'a Fix.HashCons.cell -> 'a Fix.HashCons.cell -> bool + + module Typ : sig + type 'a expr = 'a ATyp.expr = Var of tvar | TypeConstr of 'a list * string + + val equal_expr : ('a -> 'a -> bool) -> 'a expr -> 'a expr -> bool + val compare_expr : ('a -> 'a -> int) -> 'a expr -> 'a expr -> int + + val pp_expr : + (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a expr -> unit + + val show_expr : (Format.formatter -> 'a -> unit) -> 'a expr -> string + val map_expr : ('a -> 'b) -> 'a expr -> 'b expr + val fold_expr : ('a -> 'b -> 'a) -> 'a -> 'b expr -> 'a + val hash : 'a Hash.t -> 'a expr -> int + + type t = nt elem Fix.HashCons.cell + and nt = T of t expr + + module Hashed : sig + type t = nt elem + + val hash : t -> int + val equal : t -> t -> bool + end + + module H : sig + type data = Hashed.t + + val make : data -> data Fix.HashCons.cell + end + + val unfix : nt elem Fix.HashCons.cell -> t expr + val fix : t expr -> H.data Fix.HashCons.cell + val union : t -> t -> t + val find : nt elem Fix.HashCons.cell -> H.data Fix.HashCons.cell + val merge : (t expr -> t expr -> t expr) -> t -> t -> t + end + + module Rec : sig + module O : sig + type 'e expr = 'e ATyp.expr + type t = Typ.t + + val fix : t expr -> t + val unfix : t -> t expr + val map_expr : ('b -> 'a) -> 'b expr -> 'a expr + end + + type 'a alg = 'a ATyp.expr -> 'a + type 'a coalg = 'a -> 'a ATyp.expr + + val cata : 'a alg -> Typ.t -> 'a + val ana : 'a coalg -> 'a -> Typ.t + + val map_fold : + f:('a -> Typ.t ATyp.expr -> 'a) -> + alg:('a -> 'b ATyp.expr -> 'b) -> + 'a -> + Typ.t -> + 'b + + val rw_recurse_down : f:(Typ.t ATyp.expr -> Typ.t) -> Typ.t -> Typ.t + + val mutu : + ?cata:(('a * 'b) alg -> Typ.t -> 'a * 'b) -> + (('a * 'b) ATyp.expr -> 'a) -> + (('a * 'b) ATyp.expr -> 'b) -> + (Typ.t -> 'a) * (Typ.t -> 'b) + + val zygo : + ?cata:(('a * 'b) alg -> Typ.t -> 'a * 'b) -> + 'a alg -> + (('a * 'b) ATyp.expr -> 'b) -> + Typ.t -> + 'b + + val zygo_l : + ?cata:(('b * 'a) alg -> Typ.t -> 'b * 'a) -> + 'a alg -> + (('b * 'a) ATyp.expr -> 'b) -> + Typ.t -> + 'b + + val map_fold2 : + f:('a -> Typ.t ATyp.expr -> 'a) -> + alg1:('a -> ('b * 'c) ATyp.expr -> 'b) -> + alg2:'c alg -> + 'a -> + Typ.t -> + 'b + + val para_f : (('a * 'b) ATyp.expr -> 'b) -> (Typ.t -> 'a) -> Typ.t -> 'b + val para : ((Typ.t * 'a) ATyp.expr -> 'a) -> Typ.t -> 'a + + val cata_context : + ((Typ.t ATyp.expr ATyp.expr * 'a) ATyp.expr -> 'a) -> Typ.t -> 'a + + val iter_children : (Typ.t ATyp.expr -> unit) -> Typ.t -> unit + val children_iter : Typ.t -> Typ.t ATyp.expr Iter.t + end +end + +(** Create the union find and hash-consing structure for recording type + relations. This must be done per-program as its all implcit mutable state + tied to the module *) +module Make () = struct + module Typ = struct + include ATyp + + type t = nt UnionFind.elem Fix.HashCons.cell + and nt = T of t expr + + module Hashed = struct + type t = nt elem + (* we hash cons the data underlying the uf reference so we can construct the + type and get the UF reference *) + + let hash (e : t) : int = + e |> UnionFind.get |> function T e -> ATyp.hash Fix.HashCons.hash e + + let equal (i : t) (j : t) : bool = + match (UnionFind.get i, UnionFind.get j) with + | T i, T j -> ATyp.equal_expr Fix.HashCons.equal i j + end + + open struct + module M = Fix.Memoize.ForHashedType (Hashed) + (** we need to make *) + end + + module H = Fix.HashCons.Make (M) + + let unfix = + Fix.HashCons.data %> UnionFind.find %> UnionFind.get %> function + | T e -> e + + let fix e = H.make (UnionFind.make (T e)) + + let union (a : t) (b : t) : t = + H.make @@ UnionFind.union (Fix.HashCons.data a) (Fix.HashCons.data b) + + (** dubious; has invariant that H.make returns same ref as find ; + - should be true if we don't reassign refs but *) + let find e = Fix.HashCons.data e |> UnionFind.find |> H.make + + let merge f (a : t) (b : t) : t = + H.make + @@ UnionFind.merge + (fun (T a) (T b) -> T (f a b)) + (Fix.HashCons.data a) (Fix.HashCons.data b) + end + + let compare a b = Fix.HashCons.compare a b + let equal a b = Fix.HashCons.equal a b + + module Rec = Bincaml_util.Recursionscheme.Recursion (Typ) +end diff --git a/lib/passes.ml b/lib/passes.ml index 49168f62..33ae617c 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -28,6 +28,14 @@ module PassManager = struct type t = { avail : pass StringMap.t } + let hm_elaborate = + { + name = "hindley-milner-elaborate"; + apply = Prog Hm.elaborate; + invariants = Invariants.make (); + doc = "Perform hindley milner type inference on program"; + } + let chop_unreachable = { name = "trim-unreachable-proc"; @@ -435,6 +443,7 @@ module PassManager = struct let passes = [ lift_intrinsics_aarch64; + hm_elaborate; chop_unreachable; cse_elim; flatten_phis; From a131e789e4693a687bbe203c772c7618b9c88ee0 Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 12:25:45 +1000 Subject: [PATCH 02/22] small tests --- lib/lang/expr.ml | 1 + lib/lang/hm.ml | 91 ++++++++++++++++++++++++++++++++++++++++++------ 2 files changed, 82 insertions(+), 10 deletions(-) diff --git a/lib/lang/expr.ml b/lib/lang/expr.ml index 0bfc1223..ca673a08 100644 --- a/lib/lang/expr.ml +++ b/lib/lang/expr.ml @@ -393,6 +393,7 @@ module BasilExpr = struct | BinaryExpr { op; arg1 = l; arg2 = r } -> ret_type_bin op l r |> get_ty | ApplyIntrin { op; args } -> ret_type_intrin op args |> get_ty | ApplyFun { func; args } -> + (* FIXME: this is wrong *) let _, rt = Types.uncurry func in rt | Lambda { op; bound_vars; in_body = b } -> diff --git a/lib/lang/hm.ml b/lib/lang/hm.ml index b96206e9..ac4043ad 100644 --- a/lib/lang/hm.ml +++ b/lib/lang/hm.ml @@ -32,7 +32,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let int_type = TypeConstr ([], "int") let nat_val_type i = TypeConstr ([], Int.to_string i) let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") - let bvunk i = TypeConstr ([ Var i ], "bv") let bool_type = TypeConstr ([], "bool") let unit_t = TypeConstr ([], "unit") let top_t = TypeConstr ([], "top") @@ -128,6 +127,8 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let gen = ID.make_gen () let bv_type i = bv_type i + + (* bitvector of unknown width *) let bvunk i = map_expr fix @@ TypeConstr ([ Var i ], "bv") let rec ty_of_basil (t : Types.t) : t = @@ -232,6 +233,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct type typ = t [@@deriving eq, ord] + (** An AbstractExpr.t with [t] used as the type. *) module AbsTypingExpr = struct open Ops include AllOps @@ -326,6 +328,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let types_universe = "" let global_universe = "" + (* declare type with name in type scheme *) let decl_type ctx name vt = let tvar = V.create types_universe name in TCtx.update tvar @@ -335,6 +338,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct | _ -> failwith "unk") ctx + (* declare var with type in type scheme *) let decl_var_typ univ ?(no_constraint = false) c v = let vvar = V.of_var univ v in let vt = inst_annot_v v in @@ -345,19 +349,19 @@ module TypeInference (T : TypeExpr.TypeContext) = struct | _ -> failwith "unk") c - let rec infer_ty ~univ (hr : Lexing.position) e = + let rec infer_expr ~univ (hr : Lexing.position) e = fun (c : scheme TCtx.t) -> Logs.debug (fun m -> m "%s" @@ "infer " ^ plpos hr ^ " " ^ Expr.BasilExpr.to_string e); let t = - try do_infer infer_ty univ hr e c + try do_infer infer_expr univ hr e c with TypeErr m -> raise (TypeErr (m ^ " : " ^ Expr.BasilExpr.to_string e)) in t let infer ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = - infer_ty ~univ hr e c |> AbsTypingExpr.unfix |> AbstractExpr.get_typ + infer_expr ~univ hr e c |> AbsTypingExpr.unfix |> AbstractExpr.get_typ let retype_var univ ctx id = lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil @@ -416,7 +420,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let do_infer_stmt p univ ctx stmt = let open Stmt in - let infer_ty h e = infer_ty ~univ h e ctx in + let infer_ty h e = infer_expr ~univ h e ctx in (*let r = fix @@ Var (gen.fresh ()) in*) match stmt with @@ -546,7 +550,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let ibool_list b = List.map (fun a -> - let a = infer_ty ~univ [%here] a ctx in + let a = infer_expr ~univ [%here] a ctx in let _ = unify (fix bool_type) (getty a) in a) b @@ -616,7 +620,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct match definition with | Axiom b -> let bt = fix bool_type in - let b = infer_ty ~univ:global_universe [%here] b scheme in + let b = infer_expr ~univ:global_universe [%here] b scheme in let _ = unify (getty b) bt in let nb scheme = Function @@ -637,7 +641,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (scheme, `Decl (decl_id, nu)) | Function definition -> let e = - infer_ty ~univ:global_universe [%here] definition scheme + infer_expr ~univ:global_universe [%here] definition scheme in let ne scheme = Function @@ -657,7 +661,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let tyv = classification |> Option.map (fun classi -> - infer_ty ~univ:global_universe [%here] classi scheme) + infer_expr ~univ:global_universe [%here] classi scheme) in fun final_scheme -> tyv @@ -688,6 +692,10 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let scheme, new_decls = decls |> List.fold_map (infer_decl prog) TCtx.empty in + (* TODO: implicit decls; constructors need to be added after the types they + construct, probably simples to do implicits immediately after the thing they + relate to. Maybe they should just appear this way in the declaration + list. *) let prog = List.fold_left (fun prog -> function @@ -709,8 +717,71 @@ end module T = TypeInference (TypeExpr.Make ()) +module type HM = module type of TypeInference (TypeExpr.Make ()) + +(* in order to maintain well-typedness of rewrites we will probably want to + inject the global type definitions into the program, always. Otherwise we + probably risk inferring inconsistent types. Maybe this goes for for all the + global bindings. I.e. if we use a definition incorrectly it will end up + ill-typed and that error will be harder to track down. Injecting all the + bindings is somewhat giving up though. We could justifiably just require + transforms to "know what they are doing" and inject enough type information for + it to be well-typed coming out. Mistakes could be found by running a global + program typecheck after the transform. *) + +(** Algebra that infers types of expressions *) +let locally_elaborate_expr (e : Expr.BasilExpr.t) = + let open AbstractExpr in + let open Ops.AllOps in + let module T = TypeInference (TypeExpr.Make ()) in + (* TODO: need mode where we absorb take the existing annotations and try to + extend , rather than expecting everythign declared in context. *) + let i = T.infer_expr ~univ:"expr local" [%here] e TypeExpr.TCtx.empty in + let e = T.elaborate_expr ~univ:"expr local" [%here] i TypeExpr.TCtx.empty in + e + +(** Algebra for returning the annotated type (for use with functions like + fold_with_type)*) +let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = + Expr.AbstractExpr.get_typ e + +(* Partially apply args list to function type funtype and return resulting type *) +let type_applied (funtype : Types.t) (args : Types.t list) = + let module T = TypeInference (TypeExpr.Make ()) in + let rt = T.fresh_tvar ~n:"ret" () in + let args = List.map T.ty_of_basil args in + let funt = T.curry_f args rt in + let ft = T.ty_of_basil funtype in + try + T.unify ~pos:[%here] ft funt |> ignore; + Ok (T.to_basil rt) + with T.TypeErr e -> Error e + let elaborate prog = - (* We need to create a local typing module in order to get fresh state for the union find and hash cons. *) + (* We need to create a local typing module in order to get fresh state for the + union find and hash cons. *) let module T = TypeInference (TypeExpr.Make ()) in let scheme, prog = T.infer_program prog in prog + +let%expect_test "return type of function" = + let open Types in + let args = [ Bitvector 64 ] in + let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in + Printf.printf "function type: %s\n" (Types.to_string ft); + let _, ort = Types.uncurry ft in + Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); + Format.force_newline (); + Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) + (type_applied ft args) Format.newline (); + Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) + (type_applied ft [ Bitvector 24 ]) + Format.newline (); + [%expect + {| + function type: ((bv64)->(bv64->bv64)) + uncurry ret type: bv64 + + partially apply bv64: ok((bv64->bv64)) + type error: error(type_error: 64 <> 24) + |}] From ba52521633c229c33c3e7289e3ee7903d2672022 Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 13:09:37 +1000 Subject: [PATCH 03/22] unionfind --- bincaml.opam | 1 + dune-project | 1 + 2 files changed, 2 insertions(+) diff --git a/bincaml.opam b/bincaml.opam index 532328ea..f86f83c6 100644 --- a/bincaml.opam +++ b/bincaml.opam @@ -13,6 +13,7 @@ bug-reports: "https://github.com/username/reponame/issues" depends: [ "dune" {>= "3.19"} "ocaml" + "unionFind" "capstone_arm64_disas" "aslp_lifter_ocaml" {>= "1.1"} "ocaml-protoc-plugin" {>= "6.1.0"} diff --git a/dune-project b/dune-project index 6911101f..3878a8d8 100644 --- a/dune-project +++ b/dune-project @@ -37,6 +37,7 @@ (description "A longer description") (depends ocaml + unionFind capstone_arm64_disas (aslp_lifter_ocaml (>= 1.1)) (ocaml-protoc-plugin (>= 6.1.0)) From 9789589a3ff48608bafa290fc56f7a4f655d89fc Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 14:24:19 +1000 Subject: [PATCH 04/22] docs --- lib/lang/dune | 21 +----- lib/lang/hm/hm.ml | 104 ++++++++++++++++++++++++++++ lib/lang/{hm.ml => hm/inference.ml} | 44 +++++------- lib/lang/{ => hm}/typeExpr.ml | 17 +++-- lib/passes.ml | 2 +- 5 files changed, 137 insertions(+), 51 deletions(-) create mode 100644 lib/lang/hm/hm.ml rename lib/lang/{hm.ml => hm/inference.ml} (96%) rename lib/lang/{ => hm}/typeExpr.ml (91%) diff --git a/lib/lang/dune b/lib/lang/dune index f946163e..858d4b56 100644 --- a/lib/lang/dune +++ b/lib/lang/dune @@ -1,25 +1,8 @@ +(include_subdirs qualified) + (library (public_name bincaml.ast) (name lang) - (modules - hm - abstract_expr - attrib - spec_modifies - check - expr - algsimp - common - typeExpr - ops - viscfg - expr_smt - expr_eval - stmt - block - procedure - interp - program) (libraries unionFind zarith diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml new file mode 100644 index 00000000..6b225656 --- /dev/null +++ b/lib/lang/hm/hm.ml @@ -0,0 +1,104 @@ +(** Simple hindley-milner type inference *) + +(** + + {1 Type Expressions } + + Bincaml's AST is generic in the type annotation expression. + + The type system that is embedded in the concrete expression type we use is + defined in {! Common.Types}. + + This is the type loaded by the frontend, and attached to variables, and + expressions, and which all prettyprinters assume. + + + The underlying expression type though, {! Expr.AbstractExpr.t} is generic in the type. + + To perform type inference we lift the bincaml type to a minimal representation, and create + expressions annotated with this type expression. + + Once inference has finished, we extract again expressions typed with the bincaml type. + + The HM type is simple, it is either + + {ul + {- a type variable } + {- a type constructor of the form [(type list, constr. name)]} + } + + [ + type 'a expr = + Var of tvar + | TypeConstr of 'a list * string + ] + + This type is open recursive so we can traverse it using the {! Bincaml_util.Recursionscheme} module. + + This type is hash-consed so we can retrieve a canonical reference for each corresponding bincaml type. + + This type is placed in a union-find datastructre in order to perform type unification. + + *) + + + +module TypeExpr = TypeExpr + + +(** + + {1 Type Inference } + + Type inference is split into two phases, inference and elaboration. + Inference determines the type for each expression in the program, raising + type errors when conflicts arise. Elaboration anotates the program with + these expressions. + + {2 Inference } + + We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of + each expression, and perform unification to determine what the type is. + + {3 Parametric Bitvectors} + + Bitvector types are parametric in their widths, technically some operations, such + as concatenation, are typed depending on the arguments passed to them. For + now our approach is to hope there is enogugh typing information to fully + propagate concrete types. + + We define the types like "5" to represent the number 5. The + "Bitvector" type is parametric in its width type, i.e [bv5] is defined as + [TypeConstr ([TypeConstr ([],"5")], "bv")]. When we do not know the exact + width we use a type variable, and rely on unification to determine the precise + type. Our type constraints cannot fully represent our value-dependent bitvector + widths, this will fail (emitting a type varable) unless there are sufficient + type annotations. + + + {3 Ad-hoc polymorpic operators } + + Bincaml has some specific concerns, namely our operators are ad-hoc polymorphic. For each op (e.g. bvadd) + + A type-scheme in HM is a non-recursive universal quantifier over type variables. + + [type scheme = Forall of tvar list * t] + + We represent our ad-hoc polymorphic operators by immediately generalising + them, returning a type scheme for a generic function type. For instance + for [bvadd] we know all the widths have to be equal, so the type scheme is + + [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] + + + {2 Elaboration } + + As the inference returns a version of the program typed with the HM [TypeExpr]s, the + elaboration amounts to a traversal of the program which constructs + bincaml-typed representations of these structures. + + + *) + + +module Inference = Inference diff --git a/lib/lang/hm.ml b/lib/lang/hm/inference.ml similarity index 96% rename from lib/lang/hm.ml rename to lib/lang/hm/inference.ml index ac4043ad..28b9690c 100644 --- a/lib/lang/hm.ml +++ b/lib/lang/hm/inference.ml @@ -28,14 +28,25 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let tmod_const a = TypeConstr ([ a ], "const") let tmod_shared a = TypeConstr ([ a ], "shared") + + (** Function type, takes two arguments: we always curry. *) let fun_type a b = TypeConstr ([ a; b ], "->") - let int_type = TypeConstr ([], "int") + + (** A type representing a number *) let nat_val_type i = TypeConstr ([], Int.to_string i) + + (** A bitvector type parametric in its width *) let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") + + (** Primitive types *) + + let int_type = TypeConstr ([], "int") let bool_type = TypeConstr ([], "bool") let unit_t = TypeConstr ([], "unit") let top_t = TypeConstr ([], "top") let nothing_t = TypeConstr ([], "nothing") + + let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") let ptr_typ = bv_type 64 @@ -719,12 +730,17 @@ module T = TypeInference (TypeExpr.Make ()) module type HM = module type of TypeInference (TypeExpr.Make ()) -(* in order to maintain well-typedness of rewrites we will probably want to +(* + TODO: + + In order to maintain well-typedness of rewrites we will probably want to inject the global type definitions into the program, always. Otherwise we probably risk inferring inconsistent types. Maybe this goes for for all the global bindings. I.e. if we use a definition incorrectly it will end up ill-typed and that error will be harder to track down. Injecting all the - bindings is somewhat giving up though. We could justifiably just require + bindings is somewhat giving up though. + + We could justifiably just require transforms to "know what they are doing" and inject enough type information for it to be well-typed coming out. Mistakes could be found by running a global program typecheck after the transform. *) @@ -763,25 +779,3 @@ let elaborate prog = let module T = TypeInference (TypeExpr.Make ()) in let scheme, prog = T.infer_program prog in prog - -let%expect_test "return type of function" = - let open Types in - let args = [ Bitvector 64 ] in - let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in - Printf.printf "function type: %s\n" (Types.to_string ft); - let _, ort = Types.uncurry ft in - Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); - Format.force_newline (); - Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) - (type_applied ft args) Format.newline (); - Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) - (type_applied ft [ Bitvector 24 ]) - Format.newline (); - [%expect - {| - function type: ((bv64)->(bv64->bv64)) - uncurry ret type: bv64 - - partially apply bv64: ok((bv64->bv64)) - type error: error(type_error: 64 <> 24) - |}] diff --git a/lib/lang/typeExpr.ml b/lib/lang/hm/typeExpr.ml similarity index 91% rename from lib/lang/typeExpr.ml rename to lib/lang/hm/typeExpr.ml index 15115e49..00789935 100644 --- a/lib/lang/typeExpr.ml +++ b/lib/lang/hm/typeExpr.ml @@ -3,8 +3,7 @@ open Common open UnionFind -type 'a tycon = 'a list * 'a -type variance = Cov | Contr | Inv +(** Type variable identifier *) type tvar = ID.t [@@deriving eq, ord, show] (** Type scoping is handled by "universe" name strings. Hash consing enables @@ -13,7 +12,10 @@ type tvar = ID.t [@@deriving eq, ord, show] type equivalence/unification solving. *) module V = struct - (** scoped type variables *) + (** The keys for the typing context map. + We use a simple "universe" string to distinguish types defined in different + scopes (i.e. local variables from globals.) + *) type t = { univ : string; v : string } [@@deriving eq, ord, show] @@ -29,10 +31,12 @@ module V = struct else { univ; v = Var.name v } end +(** The type scheme / typing context : to store a map from scoped type variables to types. *) module TCtx = Map.Make (V) -(** unfixed type expression *) module ATyp = struct + (** Open recursive type expression, either a variable or type constructor. *) + type 'a expr = Var of tvar | TypeConstr of 'a list * string [@@deriving eq, ord, show, map, fold] @@ -148,8 +152,9 @@ module type TypeContext = sig end (** Create the union find and hash-consing structure for recording type - relations. This must be done per-program as its all implcit mutable state - tied to the module *) + relations. This must be done each time we want to perform inference in an + independent environment, in order to construct a fresh hash-consing and + union-find state. *) module Make () = struct module Typ = struct include ATyp diff --git a/lib/passes.ml b/lib/passes.ml index 33ae617c..6d0a1933 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -31,7 +31,7 @@ module PassManager = struct let hm_elaborate = { name = "hindley-milner-elaborate"; - apply = Prog Hm.elaborate; + apply = Prog Hm.Inference.elaborate; invariants = Invariants.make (); doc = "Perform hindley milner type inference on program"; } From 3f7786da98fa0f9150077d1be6647d5559935228 Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 14:25:05 +1000 Subject: [PATCH 05/22] tests --- test/lang/dune | 2 +- test/lang/test_hm.ml | 25 +++++++++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 test/lang/test_hm.ml diff --git a/test/lang/dune b/test/lang/dune index ffb11755..0035d09c 100644 --- a/test/lang/dune +++ b/test/lang/dune @@ -33,7 +33,7 @@ (library (name test_expr_eval_expect) - (modules test_expr_eval_expect test_stmt test_interp test_expr_hash) + (modules test_expr_eval_expect test_stmt test_interp test_expr_hash test_hm) (libraries loader) (inline_tests) (preprocess diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml new file mode 100644 index 00000000..ef71de3d --- /dev/null +++ b/test/lang/test_hm.ml @@ -0,0 +1,25 @@ +open Lang +open Common +open Hm.Inference + +let%expect_test "return type of function" = + let open Types in + let args = [ Bitvector 64 ] in + let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in + Printf.printf "function type: %s\n" (Types.to_string ft); + let _, ort = Types.uncurry ft in + Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); + Format.force_newline (); + Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) + (type_applied ft args) Format.newline (); + Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) + (type_applied ft [ Bitvector 24 ]) + Format.newline (); + [%expect + {| + function type: ((bv64)->(bv64->bv64)) + uncurry ret type: bv64 + + partially apply bv64: ok((bv64->bv64)) + type error: error(type_error: 64 <> 24) + |}] From 1ba9d7da0bcba4fe4c35997f2a334c7466b373db Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 14:25:14 +1000 Subject: [PATCH 06/22] fmt --- lib/lang/hm/hm.ml | 119 +++++++++++++++++---------------------- lib/lang/hm/inference.ml | 2 - lib/lang/hm/typeExpr.ml | 12 ++-- 3 files changed, 58 insertions(+), 75 deletions(-) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 6b225656..a4e01364 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -1,8 +1,6 @@ (** Simple hindley-milner type inference *) -(** - - {1 Type Expressions } +(** {1 Type Expressions} Bincaml's AST is generic in the type annotation expression. @@ -10,95 +8,82 @@ defined in {! Common.Types}. This is the type loaded by the frontend, and attached to variables, and - expressions, and which all prettyprinters assume. - - - The underlying expression type though, {! Expr.AbstractExpr.t} is generic in the type. + expressions, and which all prettyprinters assume. - To perform type inference we lift the bincaml type to a minimal representation, and create - expressions annotated with this type expression. + The underlying expression type though, {! Expr.AbstractExpr.t} is generic in + the type. - Once inference has finished, we extract again expressions typed with the bincaml type. + To perform type inference we lift the bincaml type to a minimal + representation, and create expressions annotated with this type expression. - The HM type is simple, it is either + Once inference has finished, we extract again expressions typed with the + bincaml type. - {ul - {- a type variable } - {- a type constructor of the form [(type list, constr. name)]} - } + The HM type is simple, it is either - [ - type 'a expr = - Var of tvar - | TypeConstr of 'a list * string - ] + - a type variable + - a type constructor of the form [(type list, constr. name)] - This type is open recursive so we can traverse it using the {! Bincaml_util.Recursionscheme} module. + [ type 'a expr = Var of tvar | TypeConstr of 'a list * string ] - This type is hash-consed so we can retrieve a canonical reference for each corresponding bincaml type. - - This type is placed in a union-find datastructre in order to perform type unification. - - *) + This type is open recursive so we can traverse it using the + {! Bincaml_util.Recursionscheme} module. + This type is hash-consed so we can retrieve a canonical reference for each + corresponding bincaml type. + This type is placed in a union-find datastructre in order to perform type + unification. *) module TypeExpr = TypeExpr +(** {1 Type Inference} -(** - - {1 Type Inference } - - Type inference is split into two phases, inference and elaboration. - Inference determines the type for each expression in the program, raising - type errors when conflicts arise. Elaboration anotates the program with - these expressions. - - {2 Inference } - - We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of - each expression, and perform unification to determine what the type is. - - {3 Parametric Bitvectors} - - Bitvector types are parametric in their widths, technically some operations, such - as concatenation, are typed depending on the arguments passed to them. For - now our approach is to hope there is enogugh typing information to fully - propagate concrete types. - - We define the types like "5" to represent the number 5. The - "Bitvector" type is parametric in its width type, i.e [bv5] is defined as - [TypeConstr ([TypeConstr ([],"5")], "bv")]. When we do not know the exact - width we use a type variable, and rely on unification to determine the precise - type. Our type constraints cannot fully represent our value-dependent bitvector - widths, this will fail (emitting a type varable) unless there are sufficient - type annotations. + Type inference is split into two phases, inference and elaboration. + Inference determines the type for each expression in the program, raising + type errors when conflicts arise. Elaboration anotates the program with + these expressions. + {2 Inference} - {3 Ad-hoc polymorpic operators } + We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of + each expression, and perform unification to determine what the type is. - Bincaml has some specific concerns, namely our operators are ad-hoc polymorphic. For each op (e.g. bvadd) + {3 Parametric Bitvectors} - A type-scheme in HM is a non-recursive universal quantifier over type variables. + Bitvector types are parametric in their widths, technically some operations, + such as concatenation, are typed depending on the arguments passed to them. + For now our approach is to hope there is enogugh typing information to fully + propagate concrete types. - [type scheme = Forall of tvar list * t] + We define the types like "5" to represent the number 5. The "Bitvector" type + is parametric in its width type, i.e [bv5] is defined as + [TypeConstr ([TypeConstr ([],"5")], "bv")]. When we do not know the exact + width we use a type variable, and rely on unification to determine the + precise type. Our type constraints cannot fully represent our + value-dependent bitvector widths, this will fail (emitting a type varable) + unless there are sufficient type annotations. - We represent our ad-hoc polymorphic operators by immediately generalising - them, returning a type scheme for a generic function type. For instance - for [bvadd] we know all the widths have to be equal, so the type scheme is + {3 Ad-hoc polymorpic operators} - [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] + Bincaml has some specific concerns, namely our operators are ad-hoc + polymorphic. For each op (e.g. bvadd) + A type-scheme in HM is a non-recursive universal quantifier over type + variables. - {2 Elaboration } + [type scheme = Forall of tvar list * t] - As the inference returns a version of the program typed with the HM [TypeExpr]s, the - elaboration amounts to a traversal of the program which constructs - bincaml-typed representations of these structures. + We represent our ad-hoc polymorphic operators by immediately generalising + them, returning a type scheme for a generic function type. For instance for + [bvadd] we know all the widths have to be equal, so the type scheme is + [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] - *) + {2 Elaboration} + As the inference returns a version of the program typed with the HM + [TypeExpr]s, the elaboration amounts to a traversal of the program which + constructs bincaml-typed representations of these structures. *) module Inference = Inference diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 28b9690c..07d38e6f 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -45,8 +45,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let unit_t = TypeConstr ([], "unit") let top_t = TypeConstr ([], "top") let nothing_t = TypeConstr ([], "nothing") - - let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") let ptr_typ = bv_type 64 diff --git a/lib/lang/hm/typeExpr.ml b/lib/lang/hm/typeExpr.ml index 00789935..0c37410f 100644 --- a/lib/lang/hm/typeExpr.ml +++ b/lib/lang/hm/typeExpr.ml @@ -3,8 +3,8 @@ open Common open UnionFind -(** Type variable identifier *) type tvar = ID.t [@@deriving eq, ord, show] +(** Type variable identifier *) (** Type scoping is handled by "universe" name strings. Hash consing enables types to be canonically identified by their representation, then looked up @@ -12,10 +12,9 @@ type tvar = ID.t [@@deriving eq, ord, show] type equivalence/unification solving. *) module V = struct - (** The keys for the typing context map. - We use a simple "universe" string to distinguish types defined in different - scopes (i.e. local variables from globals.) - *) + (** The keys for the typing context map. We use a simple "universe" string to + distinguish types defined in different scopes (i.e. local variables from + globals.) *) type t = { univ : string; v : string } [@@deriving eq, ord, show] @@ -31,8 +30,9 @@ module V = struct else { univ; v = Var.name v } end -(** The type scheme / typing context : to store a map from scoped type variables to types. *) module TCtx = Map.Make (V) +(** The type scheme / typing context : to store a map from scoped type variables + to types. *) module ATyp = struct (** Open recursive type expression, either a variable or type constructor. *) From 837dc96893fecd98fc65a1923032f87a8ecbb0a4 Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 14:42:49 +1000 Subject: [PATCH 07/22] cleanup --- lib/lang/hm/hm.ml | 8 +++++--- lib/lang/hm/inference.ml | 14 ++++++++++---- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index a4e01364..39cf5b76 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -24,7 +24,9 @@ - a type variable - a type constructor of the form [(type list, constr. name)] - [ type 'a expr = Var of tvar | TypeConstr of 'a list * string ] + {[ + type 'a expr = Var of tvar | TypeConstr of 'a list * string + ]} This type is open recursive so we can traverse it using the {! Bincaml_util.Recursionscheme} module. @@ -58,7 +60,7 @@ module TypeExpr = TypeExpr We define the types like "5" to represent the number 5. The "Bitvector" type is parametric in its width type, i.e [bv5] is defined as - [TypeConstr ([TypeConstr ([],"5")], "bv")]. When we do not know the exact + {[TypeConstr ([TypeConstr ([],"5")], "bv")]}. When we do not know the exact width we use a type variable, and rely on unification to determine the precise type. Our type constraints cannot fully represent our value-dependent bitvector widths, this will fail (emitting a type varable) @@ -72,7 +74,7 @@ module TypeExpr = TypeExpr A type-scheme in HM is a non-recursive universal quantifier over type variables. - [type scheme = Forall of tvar list * t] + {[type scheme = Forall of tvar list * t]} We represent our ad-hoc polymorphic operators by immediately generalising them, returning a type scheme for a generic function type. For instance for diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 07d38e6f..6519cccd 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -9,6 +9,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct include T open Typ + (** Recursion algebra for printing types *) let printer_alg = function | Var e -> ID.to_string e | TypeConstr ([ l ], e) -> l ^ " " ^ e @@ -19,6 +20,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let type_to_string t = Rec.cata printer_alg t + (** Check for type recursion: recursion is failure. *) let occurs_in a b = let check = function | Var t -> equal_tvar t a @@ -86,6 +88,12 @@ module TypeInference (T : TypeExpr.TypeContext) = struct raise (TypeErr ("type_error: " ^ type_to_string a ^ " <> " ^ type_to_string b)) + let recursion_error a b = + let b = find b in + raise + (TypeErr + ("recursive: tvar " ^ ID.to_string a ^ " occurs in " ^ type_to_string b)) + (** Type unification.*) let rec unify ?(pos = Lexing.dummy_pos) t t' = Logs.debug (fun m -> @@ -98,7 +106,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct | TypeConstr ([], "nothing"), _ -> t | _, TypeConstr ([], "nothing") -> t' | Var x, Var y -> union t t' - | Var x, _ when occurs_in x t' -> failwith "recursive type" + | Var x, _ when occurs_in x t' -> recursion_error x t' | Var _, TypeConstr _ -> merge (fun a b -> b) t t' | _, Var x -> unify ~pos:[%here] t' t | TypeConstr ([ a ], "const"), TypeConstr ([ b ], "const") -> @@ -720,15 +728,13 @@ module TypeInference (T : TypeExpr.TypeContext) = struct prog new_decls in (scheme, prog) - - (**let elaborate_program prog (scheme,new_decls) = *) end module T = TypeInference (TypeExpr.Make ()) module type HM = module type of TypeInference (TypeExpr.Make ()) -(* +(* TODO: In order to maintain well-typedness of rewrites we will probably want to From aae17f39e7dd1b8da8a0fa0c4ceabb4a3c13f58a Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 16:41:46 +1000 Subject: [PATCH 08/22] naive dependent bv solver --- lib/lang/hm/inference.ml | 215 ++++++++++++++++++++++++++++-------- test/lang/dune | 15 ++- test/lang/test_hm.ml | 59 ++++++---- test/lang/test_hm_inline.ml | 25 +++++ 4 files changed, 246 insertions(+), 68 deletions(-) create mode 100644 test/lang/test_hm_inline.ml diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 6519cccd..272cba61 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -35,7 +35,17 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let fun_type a b = TypeConstr ([ a; b ], "->") (** A type representing a number *) - let nat_val_type i = TypeConstr ([], Int.to_string i) + let nat_val_type i = + let num = fix (TypeConstr ([], Int.to_string i)) in + TypeConstr ([ num ], "ℕ") + + let is_nat_val_type (i : t) = + match unfix i with + | TypeConstr ([ num ], "ℕ") -> ( + match unfix num with + | TypeConstr ([], num) -> Int.of_string num + | _ -> None) + | _ -> None (** A bitvector type parametric in its width *) let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") @@ -50,17 +60,25 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") let ptr_typ = bv_type 64 + exception TypeErr of string + let rec to_basil (t : t) : Types.t = + let wrapped t f = + try f () + with TypeErr e -> + raise (TypeErr ("error in " ^ (type_to_string @@ t) ^ ": " ^ e)) + in let open Types in + wrapped t @@ fun () -> match unfix t with - | TypeConstr ([ a; b ], "->") -> Map (to_basil a, to_basil b) + | TypeConstr ([ a; b ], "->") -> + let a = wrapped a @@ fun () -> to_basil a in + let b = wrapped b @@ fun () -> to_basil b in + Map (a, b) | TypeConstr ([ w ], "bv") -> ( - match unfix w with - | TypeConstr ([], a) -> ( - match Int.of_string a with - | Some i -> Bitvector i - | None -> Sort (a ^ "bv", [])) - | _ -> failwith "generic bv") + match is_nat_val_type w with + | Some i -> Bitvector i + | None -> raise (TypeErr ("bitvector unresolved: " ^ type_to_string t))) | TypeConstr ([], "unit") -> Unit | TypeConstr ([], "bool") -> Boolean | TypeConstr ([], "int") -> Integer @@ -80,8 +98,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let plpos (l : Lexing.position) = Printf.sprintf "%s:%d" l.pos_fname l.pos_lnum - exception TypeErr of string - let type_error a b = let a = find a in let b = find b in @@ -142,11 +158,75 @@ module TypeInference (T : TypeExpr.TypeContext) = struct in merge (fun a b -> TypeConstr (args, n)) t t' + (** {2 Bitvector constraint solving} *) + + type dependent_bv_constraints = + | Add of { a : Typ.t; b : Typ.t; equ : Typ.t } (** a + b = equ*) + | AddConst of { a : Typ.t; b : int; equ : Typ.t } (** a + b = equ*) + + let show_dependent_bv_constraints = function + | Add { a; b; equ } -> + Printf.sprintf "%s + %s = %s" (type_to_string a) (type_to_string b) + (type_to_string equ) + | AddConst { a; b; equ } -> + Printf.sprintf "%s + (const %d) = %s" (type_to_string a) b + (type_to_string equ) + + let is_const a = is_nat_val_type a + + let unify_bv_constraint a : Typ.t option = + match a with + | Add { a; b; equ } -> ( + match List.map is_nat_val_type [ find a; find b; find equ ] with + | [ Some _; Some _; Some _ ] -> Some equ + | [ Some a; Some b; None ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a + b)) equ) + | [ Some a; None; Some b ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) + | [ None; Some a; Some b ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) + | _ -> None) + | AddConst { a; b; equ } -> ( + match (is_nat_val_type (find a), is_nat_val_type (find equ)) with + | Some i, None -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) + | Some i, Some equ_c -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) + | None, Some e -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e - b)) a) + | _ -> None) + + (** Naive solver; loop over constraints and unify until everything is solved. + *) + let solve_constraints ~max_iters cls = + let show = List.to_string ~sep:"\n" show_dependent_bv_constraints in + let rec solve tries cs = + match cs with + | [] -> () + | _ when tries > max_iters -> + raise + (TypeErr + ("Gave up solving bitvec constraints with remaining:\n" ^ show cs)) + | cs -> + let remaining = + List.filter_map + (fun c -> + match unify_bv_constraint c with + | Some e -> None + | None -> Some c) + cs + in + solve (tries + 1) remaining + in + solve 0 cls + let gen = ID.make_gen () let bv_type i = bv_type i - (* bitvector of unknown width *) - let bvunk i = map_expr fix @@ TypeConstr ([ Var i ], "bv") + (** {1 Type inference from exprs}*) + + (* Bitvector of unknown width *) + let bvunk i = TypeConstr ([ i ], "bv") let rec ty_of_basil (t : Types.t) : t = let e = @@ -177,13 +257,21 @@ module TypeInference (T : TypeExpr.TypeContext) = struct TODO: some approach like weak type variables that makes it a type error to fail to instantiate. *) - let scheme_of_op (gen : ID.generator) + let scheme_of_op ~visit_constraint (gen : ID.generator) (o : [ Ops.AllOps.const | Ops.AllOps.unary | Ops.AllOps.binary ]) = - let fv () = gen.fresh ~name:"ɑ" () in + let fv () = fix @@ Var (gen.fresh ~name:"a" ()) in match o with | `Extract (hi, lo) -> curry [ bvunk (fv ()) ] (bv_type (hi - lo)) - | `SignExtend bits -> curry [ bvunk (fv ()) ] (bvunk (fv ())) - | `ZeroExtend bits -> curry [ bvunk (fv ()) ] (bvunk (fv ())) + | `SignExtend bits -> + let a = fv () in + let equ = fv () in + let r = curry [ bvunk a ] (bvunk equ) in + visit_constraint @@ AddConst { a; b = bits; equ }; + r + | `ZeroExtend bits -> + let a = fv () and equ = fv () in + visit_constraint @@ AddConst { a; b = bits; equ }; + curry [ bvunk a ] (bvunk equ) | `BOOLTOBV1 -> curry [ bool_type ] (bv_type 1) | `Bitvector b -> fix @@ bv_type (Bitvec.size b) | #Ops.BVOps.binary_unif -> @@ -202,7 +290,9 @@ module TypeInference (T : TypeExpr.TypeContext) = struct | #Ops.LogicalOps.binary -> curry [ bool_type; bool_type ] bool_type | #Ops.LogicalOps.unary -> curry [ bool_type ] bool_type | #Ops.LogicalOps.const -> fix @@ bool_type - | `Old -> fix @@ Var (fv ()) + | `Old -> + let a = fv () in + curry_f [ a ] a | #Ops.AllOps.binary as o -> failwith @@ "unsupported op" ^ Ops.AllOps.to_string o | #Ops.AllOps.unary as o -> @@ -211,20 +301,33 @@ module TypeInference (T : TypeExpr.TypeContext) = struct failwith @@ "unsupported op" ^ Ops.AllOps.to_string o (** return the generic type scheme of an intrinsic operation *) - let scheme_of_intrin (gen : ID.generator) (o : Ops.AllOps.intrin) args = - let fv () = gen.fresh ~name:"ɑ" () in + let scheme_of_intrin ?(visit_constraint = fun a -> ()) (gen : ID.generator) + (o : Ops.AllOps.intrin) args = + let fv () = fix @@ Var (gen.fresh ~name:"a" ()) in match o with | `BVADD | `BVMUL | `BVOR | `BVXOR | `BVAND -> let a = fv () in - curry (List.init args (fun _ -> Var a)) (Var a) - | `BVConcat -> curry (List.init args (fun _ -> Var (fv ()))) (Var (fv ())) + curry_f (List.init args (fun _ -> a)) a + | `BVConcat -> + let args = List.init args (fun _ -> fv ()) in + let rs = + List.reduce_exn + (fun a b -> + let equ = fv () in + visit_constraint (Add { a; b; equ }); + equ) + args + in + let rs = bvunk rs in + let args = List.map bvunk args in + curry args rs | `OR | `AND -> curry (List.init args (fun _ -> bool_type)) bool_type | `MapUpdate -> let a = fv () in let b = fv () in - let m = curry [ Var a ] (Var b) in - curry_f [ m; fix @@ Var a; fix @@ Var b ] m - | `Cases -> fix @@ Var (fv ()) + let m = curry_f [ a ] b in + curry_f [ m; a; b ] m + | `Cases -> fv () (* instantiate typescheme for a single type-annotated variable *) let inst_annot_v ?(no_constraint = false) v = @@ -276,7 +379,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let typ = lookup_var_typ univ ctx id in (id, typ) - let do_infer + let do_infer ~visit_constraint (infer : univ:string -> Lexing.position -> @@ -312,25 +415,25 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (Lambda { op; bound_vars; in_body = bdty; attrib; typ; triggers }) end | Constant { const = #Ops.AllOps.const as op; attrib } -> begin - let f = scheme_of_op gen op in + let f = scheme_of_op ~visit_constraint gen op in let r = unify r f in AbsTypingExpr.fix (Constant { typ = r; const = op; attrib }) end | UnaryExpr { op = #Ops.AllOps.unary as op; arg; attrib } -> begin - let f = scheme_of_op gen op in + let f = scheme_of_op ~visit_constraint gen op in let arg = infer ~univ [%here] arg c in ignore @@ unify f (curry_f [ getty arg ] r); AbsTypingExpr.fix (UnaryExpr { typ = r; op; attrib; arg }) end | BinaryExpr { op = #Ops.AllOps.binary as op; arg1; arg2; attrib } -> begin - let f = scheme_of_op gen op in + let f = scheme_of_op ~visit_constraint gen op in let arg1 = infer ~univ [%here] arg1 c in let arg2 = infer ~univ [%here] arg2 c in ignore @@ unify f (curry_f [ getty arg1; getty arg2 ] r); AbsTypingExpr.fix (BinaryExpr { typ = r; op; attrib; arg1; arg2 }) end | ApplyIntrin { op = #Ops.AllOps.intrin as op; args; attrib } -> begin - let f = scheme_of_intrin gen op (List.length args) in + let f = scheme_of_intrin ~visit_constraint gen op (List.length args) in let args = List.map (fun a -> infer ~univ [%here] a c) args in ignore @@ unify f (curry_f (List.map getty args) r); AbsTypingExpr.fix (ApplyIntrin { typ = r; op; attrib; args }) @@ -366,19 +469,24 @@ module TypeInference (T : TypeExpr.TypeContext) = struct | _ -> failwith "unk") c - let rec infer_expr ~univ (hr : Lexing.position) e = + let rec infer_expr visit_constraint ~univ (hr : Lexing.position) e = fun (c : scheme TCtx.t) -> Logs.debug (fun m -> m "%s" @@ "infer " ^ plpos hr ^ " " ^ Expr.BasilExpr.to_string e); let t = - try do_infer infer_expr univ hr e c + try do_infer ~visit_constraint (infer_expr visit_constraint) univ hr e c with TypeErr m -> raise (TypeErr (m ^ " : " ^ Expr.BasilExpr.to_string e)) in t - let infer ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = - infer_expr ~univ hr e c |> AbsTypingExpr.unfix |> AbstractExpr.get_typ + let infer visit_constraint ~univ (hr : Lexing.position) e (c : scheme TCtx.t) + = + let nexpr = + infer_expr visit_constraint ~univ hr e c + |> AbsTypingExpr.unfix |> AbstractExpr.get_typ + in + nexpr let retype_var univ ctx id = lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil @@ -403,7 +511,8 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let unfix i = match i with Expr.BasilExpr.E i -> i let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e - let infer_phi univ ctx (p : Var.t Block.phi list) = + let infer_phi visit_constraint univ ctx (p : Var.t Block.phi list) = + let infer = infer visit_constraint in let open Block in let r = fix @@ Var (gen.fresh ()) in List.fold_left @@ -435,9 +544,10 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let fresh_tvar ?(n = "a") () = fix @@ Var (gen.fresh ~name:n ()) - let do_infer_stmt p univ ctx stmt = + let do_infer_stmt visit_constraint p univ ctx stmt = let open Stmt in - let infer_ty h e = infer_expr ~univ h e ctx in + let infer_ty h e = infer_expr visit_constraint ~univ h e ctx in + let infer = infer visit_constraint in (*let r = fix @@ Var (gen.fresh ()) in*) match stmt with @@ -533,17 +643,17 @@ module TypeInference (T : TypeExpr.TypeContext) = struct ~f_expr:(fun e -> elaborate_expr ~univ [%here] e ctx) ~f_lvar:retype_var ~f_rvar:retype_var stmt - let infer_stmt p univ ctx s = - try do_infer_stmt p univ ctx s + let infer_stmt vc p univ ctx s = + try do_infer_stmt vc p univ ctx s with TypeErr m -> raise (TypeErr (m ^ " " ^ Stmt.to_string Var.pretty Var.pretty Expr.BasilExpr.pretty s)) - let infer_block p univ ctx (b : Program.bloc) = - let _ = infer_phi univ ctx b.phis in - Block.map ~phi:Fun.id (infer_stmt p univ ctx) b + let infer_block vc p univ ctx (b : Program.bloc) = + let _ = infer_phi vc univ ctx b.phis in + Block.map ~phi:Fun.id (infer_stmt vc p univ ctx) b let elaborate_block p univ ctx (b : ('a, 'b) Block.t) = Block.map ~phi:(elaborate_phi univ ctx) (elaborate_stmt univ ctx) b @@ -561,13 +671,13 @@ module TypeInference (T : TypeExpr.TypeContext) = struct in ctx - let infer_proc prog ctx ?(no_constraint = false) (p : Program.proc) = + let infer_proc vc prog ctx ?(no_constraint = false) (p : Program.proc) = let spec = Procedure.specification p in let univ = V.proc_univ @@ Procedure.id p in let ibool_list b = List.map (fun a -> - let a = infer_expr ~univ [%here] a ctx in + let a = infer_expr vc ~univ [%here] a ctx in let _ = unify (fix bool_type) (getty a) in a) b @@ -602,7 +712,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let ctx = assume_proc_decl ctx ~no_constraint p in let bvlocks = Procedure.iter_blocks_topo_fwd p - |> Iter.map (fun (i, b) -> (i, infer_block prog univ ctx b)) + |> Iter.map (fun (i, b) -> (i, infer_block vc prog univ ctx b)) |> Iter.persistent in @@ -620,8 +730,10 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (** Run type inference on a declaration, returning an updated typing scheme, and elaboration function*) - let infer_decl prog scheme = + let infer_decl visit_constraint prog scheme = let open Program in + let infer_expr = infer_expr visit_constraint in + let infer_proc = infer_proc visit_constraint in (* We have to be careful that inference is run immediately, not delayed until elaboration. *) fun (decl_id, d) -> match d with @@ -701,14 +813,17 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (** The function that does everything *) let infer_program prog = let decls = Program.declarations prog |> Iter.to_list in + let constraints = ref [] in + let visit_constraint c = constraints := c :: !constraints in (* We fold the inference context through every declaration and calling the inference functions, returning an expressions typed with the type expressions herein. We also return the resulting list of elaboration functions, which take the final inference context and convert the HM-typed expressions back to bincaml typed expressions. *) let scheme, new_decls = - decls |> List.fold_map (infer_decl prog) TCtx.empty + decls |> List.fold_map (infer_decl visit_constraint prog) TCtx.empty in + let _ = solve_constraints ~max_iters:50 !constraints in (* TODO: implicit decls; constructors need to be added after the types they construct, probably simples to do implicits immediately after the thing they relate to. Maybe they should just appear this way in the declaration @@ -754,9 +869,15 @@ let locally_elaborate_expr (e : Expr.BasilExpr.t) = let open AbstractExpr in let open Ops.AllOps in let module T = TypeInference (TypeExpr.Make ()) in + let constraints = ref [] in + let visit_constraint c = constraints := c :: !constraints in (* TODO: need mode where we absorb take the existing annotations and try to extend , rather than expecting everythign declared in context. *) - let i = T.infer_expr ~univ:"expr local" [%here] e TypeExpr.TCtx.empty in + let i = + T.infer_expr visit_constraint ~univ:"expr local" [%here] e + TypeExpr.TCtx.empty + in + let _ = T.solve_constraints ~max_iters:100 !constraints in let e = T.elaborate_expr ~univ:"expr local" [%here] i TypeExpr.TCtx.empty in e diff --git a/test/lang/dune b/test/lang/dune index 0035d09c..3e4e0560 100644 --- a/test/lang/dune +++ b/test/lang/dune @@ -33,7 +33,12 @@ (library (name test_expr_eval_expect) - (modules test_expr_eval_expect test_stmt test_interp test_expr_hash test_hm) + (modules + test_expr_eval_expect + test_stmt + test_interp + test_expr_hash + test_hm_inline) (libraries loader) (inline_tests) (preprocess @@ -63,6 +68,14 @@ (modules test_pagetable_qcheck) (libraries test_pagetable_spec qcheck-core.runner qcheck-stm.sequential)) +(test + (name test_hm) + (package bincaml) + (modules test_hm) + (preprocess + (pps ppx_expect)) + (libraries expr_gen alcotest qcheck-alcotest qcheck-core bincaml.analysis)) + (test (name test_value_soundness) (package bincaml) diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml index ef71de3d..046c3f5e 100644 --- a/test/lang/test_hm.ml +++ b/test/lang/test_hm.ml @@ -2,24 +2,43 @@ open Lang open Common open Hm.Inference -let%expect_test "return type of function" = - let open Types in - let args = [ Bitvector 64 ] in - let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in - Printf.printf "function type: %s\n" (Types.to_string ft); - let _, ort = Types.uncurry ft in - Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); - Format.force_newline (); - Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) - (type_applied ft args) Format.newline (); - Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) - (type_applied ft [ Bitvector 24 ]) - Format.newline (); - [%expect - {| - function type: ((bv64)->(bv64->bv64)) - uncurry ret type: bv64 +module HMDifferential = struct + let arb_expr = + let open QCheck.Gen in + let* wd = Expr_gen.gen_width in + Expr_gen.gen_bvexpr (5, wd) - partially apply bv64: ok((bv64->bv64)) - type error: error(type_error: 64 <> 24) - |}] + let infer e = + try + Ok + (locally_elaborate_expr e |> Expr.BasilExpr.unfix + |> Expr.AbstractExpr.get_typ) + with e -> Result.of_exn e + + let gener = + QCheck.make ~print:(fun (e, inf_b, inf_hm) -> + Printf.sprintf "%s : %s = %s" + (Expr.BasilExpr.to_string e) + (Types.to_string inf_b) + (Format.sprintf "%a" (Result.pp Types.pp) inf_hm)) + @@ + let open QCheck.Gen in + let* exp = arb_expr in + let inf_b = Expr.BasilExpr.get_typ exp in + let inf_hm = infer exp in + return (exp, inf_b, inf_hm) + + let predicate (a, b, hm) = Result.is_ok hm && Types.equal b (Result.get_ok hm) + + let test = + QCheck.Test.make ~name:"Hm inference matches" ~count:1000 ~max_fail:1 gener + predicate +end + +let _ = + let suite = + List.map + (QCheck_alcotest.to_alcotest ~long:true ~speed_level:`Slow ~verbose:true) + [ HMDifferential.test ] + in + Alcotest.run "hm" [ ("diff", suite) ] diff --git a/test/lang/test_hm_inline.ml b/test/lang/test_hm_inline.ml new file mode 100644 index 00000000..ef71de3d --- /dev/null +++ b/test/lang/test_hm_inline.ml @@ -0,0 +1,25 @@ +open Lang +open Common +open Hm.Inference + +let%expect_test "return type of function" = + let open Types in + let args = [ Bitvector 64 ] in + let ft = Map (Bitvector 64, Map (Bitvector 64, Bitvector 64)) in + Printf.printf "function type: %s\n" (Types.to_string ft); + let _, ort = Types.uncurry ft in + Printf.printf "uncurry ret type: %s\n" (Types.to_string ort); + Format.force_newline (); + Format.printf "%s%a%a" "partially apply bv64: " (Result.pp Types.pp) + (type_applied ft args) Format.newline (); + Format.printf "%s%a%a" "type error: " (Result.pp Types.pp) + (type_applied ft [ Bitvector 24 ]) + Format.newline (); + [%expect + {| + function type: ((bv64)->(bv64->bv64)) + uncurry ret type: bv64 + + partially apply bv64: ok((bv64->bv64)) + type error: error(type_error: 64 <> 24) + |}] From 1c5758956d0bdb6b49bb858abcae30cedcdcd41a Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 16:46:07 +1000 Subject: [PATCH 09/22] dont spell out module sig --- lib/lang/hm/typeExpr.ml | 109 ++-------------------------------------- 1 file changed, 3 insertions(+), 106 deletions(-) diff --git a/lib/lang/hm/typeExpr.ml b/lib/lang/hm/typeExpr.ml index 0c37410f..4b500058 100644 --- a/lib/lang/hm/typeExpr.ml +++ b/lib/lang/hm/typeExpr.ml @@ -45,112 +45,6 @@ module ATyp = struct | TypeConstr (l, t) -> Hash.pair (Hash.list he) Hash.string (l, t) end -(** Type of mutable type context union find *) -module type TypeContext = sig - val compare : 'a Fix.HashCons.cell -> 'a Fix.HashCons.cell -> int - val equal : 'a Fix.HashCons.cell -> 'a Fix.HashCons.cell -> bool - - module Typ : sig - type 'a expr = 'a ATyp.expr = Var of tvar | TypeConstr of 'a list * string - - val equal_expr : ('a -> 'a -> bool) -> 'a expr -> 'a expr -> bool - val compare_expr : ('a -> 'a -> int) -> 'a expr -> 'a expr -> int - - val pp_expr : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a expr -> unit - - val show_expr : (Format.formatter -> 'a -> unit) -> 'a expr -> string - val map_expr : ('a -> 'b) -> 'a expr -> 'b expr - val fold_expr : ('a -> 'b -> 'a) -> 'a -> 'b expr -> 'a - val hash : 'a Hash.t -> 'a expr -> int - - type t = nt elem Fix.HashCons.cell - and nt = T of t expr - - module Hashed : sig - type t = nt elem - - val hash : t -> int - val equal : t -> t -> bool - end - - module H : sig - type data = Hashed.t - - val make : data -> data Fix.HashCons.cell - end - - val unfix : nt elem Fix.HashCons.cell -> t expr - val fix : t expr -> H.data Fix.HashCons.cell - val union : t -> t -> t - val find : nt elem Fix.HashCons.cell -> H.data Fix.HashCons.cell - val merge : (t expr -> t expr -> t expr) -> t -> t -> t - end - - module Rec : sig - module O : sig - type 'e expr = 'e ATyp.expr - type t = Typ.t - - val fix : t expr -> t - val unfix : t -> t expr - val map_expr : ('b -> 'a) -> 'b expr -> 'a expr - end - - type 'a alg = 'a ATyp.expr -> 'a - type 'a coalg = 'a -> 'a ATyp.expr - - val cata : 'a alg -> Typ.t -> 'a - val ana : 'a coalg -> 'a -> Typ.t - - val map_fold : - f:('a -> Typ.t ATyp.expr -> 'a) -> - alg:('a -> 'b ATyp.expr -> 'b) -> - 'a -> - Typ.t -> - 'b - - val rw_recurse_down : f:(Typ.t ATyp.expr -> Typ.t) -> Typ.t -> Typ.t - - val mutu : - ?cata:(('a * 'b) alg -> Typ.t -> 'a * 'b) -> - (('a * 'b) ATyp.expr -> 'a) -> - (('a * 'b) ATyp.expr -> 'b) -> - (Typ.t -> 'a) * (Typ.t -> 'b) - - val zygo : - ?cata:(('a * 'b) alg -> Typ.t -> 'a * 'b) -> - 'a alg -> - (('a * 'b) ATyp.expr -> 'b) -> - Typ.t -> - 'b - - val zygo_l : - ?cata:(('b * 'a) alg -> Typ.t -> 'b * 'a) -> - 'a alg -> - (('b * 'a) ATyp.expr -> 'b) -> - Typ.t -> - 'b - - val map_fold2 : - f:('a -> Typ.t ATyp.expr -> 'a) -> - alg1:('a -> ('b * 'c) ATyp.expr -> 'b) -> - alg2:'c alg -> - 'a -> - Typ.t -> - 'b - - val para_f : (('a * 'b) ATyp.expr -> 'b) -> (Typ.t -> 'a) -> Typ.t -> 'b - val para : ((Typ.t * 'a) ATyp.expr -> 'a) -> Typ.t -> 'a - - val cata_context : - ((Typ.t ATyp.expr ATyp.expr * 'a) ATyp.expr -> 'a) -> Typ.t -> 'a - - val iter_children : (Typ.t ATyp.expr -> unit) -> Typ.t -> unit - val children_iter : Typ.t -> Typ.t ATyp.expr Iter.t - end -end - (** Create the union find and hash-consing structure for recording type relations. This must be done each time we want to perform inference in an independent environment, in order to construct a fresh hash-consing and @@ -207,3 +101,6 @@ module Make () = struct module Rec = Bincaml_util.Recursionscheme.Recursion (Typ) end + +module type TypeContext = module type of Make () +(** Type of mutable type context union find *) From 9e04455745a5e2919e763d49acd4483679608672 Mon Sep 17 00:00:00 2001 From: agle Date: Fri, 10 Jul 2026 17:02:12 +1000 Subject: [PATCH 10/22] test --- examples | 2 +- test/lang/test_expr_eval_qcheck.ml | 2 -- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/examples b/examples index da590450..339b7c48 160000 --- a/examples +++ b/examples @@ -1 +1 @@ -Subproject commit da5904507e8dff136686a1c6da94d09d6baa127e +Subproject commit 339b7c483383d3c73af612dc5e612a4d4252b599 diff --git a/test/lang/test_expr_eval_qcheck.ml b/test/lang/test_expr_eval_qcheck.ml index df87dcf6..af9b713c 100644 --- a/test/lang/test_expr_eval_qcheck.ml +++ b/test/lang/test_expr_eval_qcheck.ml @@ -19,8 +19,6 @@ module EvalExprGen = struct let* wd = Expr_gen.gen_width in Expr_gen.gen_bvexpr (1, wd) - let arb_bvexpr = QCheck.make ~print:Expr.BasilExpr.to_string_annot eval_expr - let arb_partial_eval_bvexpr = QCheck.make ~print:(fun (e, p) -> Printf.sprintf "%s ~> %s" From e43c147ddf87d97d74810234bd29d89d392dc03d Mon Sep 17 00:00:00 2001 From: agle Date: Mon, 13 Jul 2026 16:06:31 +1000 Subject: [PATCH 11/22] infer vars in local elaboration --- lib/lang/hm/inference.ml | 17 ++++++++----- test/lang/expr_gen.ml | 41 +++++++++++++++++++++--------- test/lang/test_expr_eval_qcheck.ml | 2 +- test/lang/test_hm.ml | 2 +- test/lang/test_value_soundness.ml | 5 ++-- 5 files changed, 44 insertions(+), 23 deletions(-) diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 272cba61..99fe8475 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -498,8 +498,9 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let e = match e with | AbstractExpr.RVar { id; attrib; typ } -> - (* FIXME: bad to have two type annotations *) - let id = retype_var univ c id in + (* avoid looking up the id in context as we may be in a local + binding *) + let id = Var.copy id ~typ:(to_basil @@ find typ) in AbstractExpr.RVar { id; attrib; typ } | o -> o in @@ -870,15 +871,17 @@ let locally_elaborate_expr (e : Expr.BasilExpr.t) = let open Ops.AllOps in let module T = TypeInference (TypeExpr.Make ()) in let constraints = ref [] in + let univ = "" in + let ctx = + Expr.BasilExpr.free_vars_iter e + |> Iter.fold (T.decl_var_typ univ) TypeExpr.TCtx.empty + in let visit_constraint c = constraints := c :: !constraints in (* TODO: need mode where we absorb take the existing annotations and try to extend , rather than expecting everythign declared in context. *) - let i = - T.infer_expr visit_constraint ~univ:"expr local" [%here] e - TypeExpr.TCtx.empty - in + let i = T.infer_expr visit_constraint ~univ [%here] e ctx in let _ = T.solve_constraints ~max_iters:100 !constraints in - let e = T.elaborate_expr ~univ:"expr local" [%here] i TypeExpr.TCtx.empty in + let e = T.elaborate_expr ~univ [%here] i ctx in e (** Algebra for returning the annotated type (for use with functions like diff --git a/test/lang/expr_gen.ml b/test/lang/expr_gen.ml index d8428d3d..eecba9f5 100644 --- a/test/lang/expr_gen.ml +++ b/test/lang/expr_gen.ml @@ -60,6 +60,21 @@ let gen_bvconst ?min w = let* c = gen_bv ?min w in return (BasilExpr.bvconst c) +let vname = + let v = int_bound 8 in + let vl = "abcdefghijklmnopqrstuvwxyz" |> String.to_list in + let vl = vl @ List.map Char.uppercase_ascii vl in + let cs = QCheck.Gen.oneof_list vl in + QCheck.Gen.(string_size ~gen:cs v) + +let gen_bvvar ?min w = + let* n = vname in + return (BasilExpr.rvar (Common.Var.create n (Common.Types.Bitvector w))) + +let gen_boolvar = + let* n = vname in + return (BasilExpr.rvar @@ Var.create n Common.Types.Boolean) + let make_bvconst wd x = BasilExpr.bvconst @@ Bitvec.of_int ~size:wd x let ensure_nonzero wd e = BasilExpr.binexp ~op:`BVOR e (make_bvconst wd 1) @@ -95,14 +110,15 @@ let gen_unop_advanced gen_bvexpr wd = (* assert (BasilExpr.type_of e = Bitvector wd); *) (* e *) -let gen_bvexpr = +let gen_bvexpr ~with_var = fix (fun self (size, wd) -> + let gvs = if with_var then [ (1, gen_bvvar wd) ] else [] in let self wd = self (size / 2, wd) in match size with | 0 -> gen_bvconst wd | size -> - oneof_weighted - [ + oneof_weighted @@ gvs + @ [ (1, gen_bvconst wd); (2, self wd >>= gen_unop); (2, gen_unop_advanced self wd); @@ -126,10 +142,10 @@ let gen_not f = module LT = List.Traverse (QCheck.Gen) -let gen_bv_pred = +let gen_bv_pred ~with_var = let* w = int_range 2 32 in - let* a = gen_bvexpr (2, w) in - let* b = gen_bvexpr (2, w) in + let* a = gen_bvexpr ~with_var (2, w) in + let* b = gen_bvexpr ~with_var (2, w) in let* op = oneof_list bv_binops_pred in return @@ BasilExpr.binexp ~op a b @@ -139,16 +155,17 @@ let gen_pred f = let* op = oneof_list [ `AND; `OR ] in return @@ BasilExpr.applyintrin ~op args -let gen_pred_expr = +let gen_pred_expr ~with_var = fix (fun self size -> let self = self (size / 2) in + let v = if with_var then [ (1, gen_boolvar) ] else [] in match size with | 0 -> gen_bool | size -> - oneof_weighted - [ + oneof_weighted @@ v + @ [ (1, gen_bool); - (2, gen_bv_pred); + (2, gen_bv_pred ~with_var); (2, gen_not self); (2, gen_pred self); ]) @@ -157,10 +174,10 @@ let gen_expr = let gbv = let* wd = int_range 2 65 in let* c = int_bound 3 in - gen_bvexpr (wd, c) + gen_bvexpr ~with_var:false (wd, c) in let gpred = let* c = int_bound 3 in - gen_pred_expr c + gen_pred_expr ~with_var:false c in oneof_weighted [ (1, gpred); (1, gbv) ] diff --git a/test/lang/test_expr_eval_qcheck.ml b/test/lang/test_expr_eval_qcheck.ml index af9b713c..111d9f55 100644 --- a/test/lang/test_expr_eval_qcheck.ml +++ b/test/lang/test_expr_eval_qcheck.ml @@ -17,7 +17,7 @@ module EvalExprGen = struct let eval_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (1, wd) + Expr_gen.gen_bvexpr ~with_var:false (1, wd) let arb_partial_eval_bvexpr = QCheck.make ~print:(fun (e, p) -> diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml index 046c3f5e..c139e1f5 100644 --- a/test/lang/test_hm.ml +++ b/test/lang/test_hm.ml @@ -6,7 +6,7 @@ module HMDifferential = struct let arb_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (5, wd) + Expr_gen.gen_bvexpr ~with_var:true (5, wd) let infer e = try diff --git a/test/lang/test_value_soundness.ml b/test/lang/test_value_soundness.ml index 67064ca3..12659161 100644 --- a/test/lang/test_value_soundness.ml +++ b/test/lang/test_value_soundness.ml @@ -11,7 +11,8 @@ struct let arb_expr = let open QCheck.Gen in let* wd = Expr_gen.gen_width in - Expr_gen.gen_bvexpr (5, wd) + (* FIXME: soundness issues when variables *) + Expr_gen.gen_bvexpr ~with_var:false (5, wd) let arb_val = let open QCheck.Gen in @@ -37,7 +38,7 @@ struct let eval_abs e = Eval.eval Ops.AllOps.show_const Ops.AllOps.show_unary Ops.AllOps.show_binary Ops.AllOps.show_intrin - (fun _ -> failwith "no vars") + (fun _ -> V.top) e let join_symm (l, r) = From 715ff80b3e8c221a6d261f13977b58d9bd36c044 Mon Sep 17 00:00:00 2001 From: agle Date: Mon, 13 Jul 2026 23:00:38 +1000 Subject: [PATCH 12/22] split into multiple files --- lib/lang/hm/elaboration.ml | 248 +++++++++++++++ lib/lang/hm/hm.ml | 78 +++++ lib/lang/hm/hm_types.ml | 121 +++++++ lib/lang/hm/inference.ml | 612 ++---------------------------------- lib/lang/hm/solve_bv.ml | 72 +++++ lib/lang/hm/typeExpr.ml | 15 +- lib/lang/hm/unification.ml | 124 ++++++++ lib/passes.ml | 2 +- test/lang/test_hm.ml | 6 +- test/lang/test_hm_inline.ml | 2 +- 10 files changed, 679 insertions(+), 601 deletions(-) create mode 100644 lib/lang/hm/elaboration.ml create mode 100644 lib/lang/hm/hm_types.ml create mode 100644 lib/lang/hm/solve_bv.ml create mode 100644 lib/lang/hm/unification.ml diff --git a/lib/lang/hm/elaboration.ml b/lib/lang/hm/elaboration.ml new file mode 100644 index 00000000..8714c18d --- /dev/null +++ b/lib/lang/hm/elaboration.ml @@ -0,0 +1,248 @@ +open Common +open UnionFind +open Abstract_expr + +(** Hindley-Milner type inference based on a union-find. *) + +module TypeInference (T : TypeExpr.TypeContext) = struct + include Inference.Make (T) + + let retype_var univ ctx id = + lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil + |> fun typ -> Var.copy ~typ id + + let elaborate_phi univ ctx (p : Var.t Block.phi list) = + let open Block in + List.map + (fun { lhs; rhs } -> + let lhs = retype_var univ ctx lhs in + let rhs = List.map (fun (a, r) -> (a, retype_var univ ctx r)) rhs in + { lhs; rhs }) + p + + let ctx_to_string ctx = + TCtx.to_iter ctx + |> Iter.to_string (fun (a, b) -> + Printf.sprintf "%s %s" (V.to_string a) (scheme_to_string b)) + + let fresh_tvar ?(n = "a") () = fix @@ Var (gen.fresh ~name:n ()) + let unfix i = match i with Expr.BasilExpr.E i -> i + let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e + + (** Extract type after full inference has run. *) + let elaborate_expr ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = + let alg e = + let e = + match e with + | AbstractExpr.RVar { id; attrib; typ } -> + (* avoid looking up the id in context as we may be in a local + binding *) + let id = Var.copy id ~typ:(to_basil @@ find typ) in + AbstractExpr.RVar { id; attrib; typ } + | o -> o + in + let t = AbstractExpr.get_typ e |> find |> to_basil in + AbstractExpr.set_typ e t |> Expr.BasilExpr.fix + in + e |> TypingExpr.cata alg + + let elaborate_stmt univ ctx stmt = + let retype_var v = + let typ = + lookup_var_typ ~no_constraint:true univ ctx v |> find |> to_basil + in + Var.copy ~typ v + in + Stmt.map + ~f_expr:(fun e -> elaborate_expr ~univ [%here] e ctx) + ~f_lvar:retype_var ~f_rvar:retype_var stmt + + let elaborate_block p univ ctx (b : ('a, 'b) Block.t) = + Block.map ~phi:(elaborate_phi univ ctx) (elaborate_stmt univ ctx) b + + let assume_proc_decl ctx ?(no_constraint = false) (p : Program.proc) = + let globs = Var.Decls.values (Procedure.local_decls p) in + let formals_in = Procedure.formal_in_params p |> StringMap.values in + let formals_out = Procedure.formal_out_params p |> StringMap.values in + let univ = V.proc_univ @@ Procedure.id p in + let ctx = + Iter.fold + (decl_var_typ ~no_constraint univ) + ctx + (Iter.append globs @@ Iter.append formals_in formals_out) + in + ctx + + let infer_proc vc prog ctx ?(no_constraint = false) (p : Program.proc) = + let spec = Procedure.specification p in + let univ = V.proc_univ @@ Procedure.id p in + let ibool_list b = + List.map + (fun a -> + let a = infer_expr vc ~univ [%here] a ctx in + let _ = unify (fix bool_type) (getty a) in + a) + b + in + let spec : ('a, 'b) Procedure.proc_spec = + { + requires = ibool_list spec.requires; + ensures = ibool_list spec.ensures; + rely = ibool_list spec.rely; + guarantee = ibool_list spec.guarantee; + captures_globs = + List.map (infer_var global_universe ctx) spec.captures_globs; + modifies_globs = + List.map (infer_var global_universe ctx) spec.modifies_globs; + } + in + + let new_spec ctx : (Var.t, Expr.BasilExpr.t) Procedure.proc_spec = + { + requires = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.requires; + ensures = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.ensures; + rely = List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.rely; + guarantee = + List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.guarantee; + captures_globs = spec.captures_globs |> List.map fst; + modifies_globs = spec.modifies_globs |> List.map fst; + } + in + + let ctx = assume_proc_decl ctx ~no_constraint p in + let bvlocks = + Procedure.iter_blocks_topo_fwd p + |> Iter.map (fun (i, b) -> (i, infer_block vc prog univ ctx b)) + |> Iter.persistent + in + + let elaborate_proc ctx = + Procedure.set_specification p (new_spec ctx) + |> (fun p -> + bvlocks + |> Iter.map (fun (bid, b) -> (bid, elaborate_block [%here] univ ctx b)) + |> Iter.fold (fun p (bid, b) -> Procedure.update_block p bid b) p) + |> Procedure.map_formal_in_params (StringMap.map (retype_var univ ctx)) + |> Procedure.map_formal_out_params (StringMap.map (retype_var univ ctx)) + in + Logs.debug (fun m -> m "%s" (ctx_to_string ctx)); + (elaborate_proc, ctx) + + (** Run type inference on a declaration, returning an updated typing scheme, + and elaboration function*) + let infer_decl visit_constraint prog scheme = + let open Program in + let infer_expr = infer_expr visit_constraint in + let infer_proc = infer_proc visit_constraint in + (* We have to be careful that inference is run immediately, not delayed until elaboration. *) + fun (decl_id, d) -> + match d with + | Type { binding; typ } -> + let ty = ty_of_basil typ in + let scheme = decl_type scheme binding ty in + let nty scheme = Type { binding; typ = to_basil (find ty) } in + (scheme, `Decl (decl_id, nty)) + | Function { binding; definition; attrib } -> ( + (* elaboration of var binding *) + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + match definition with + | Axiom b -> + let bt = fix bool_type in + let b = infer_expr ~univ:global_universe [%here] b scheme in + let _ = unify (getty b) bt in + let nb scheme = + Function + { + attrib; + binding = binding scheme; + definition = + Axiom + (elaborate_expr ~univ:global_universe [%here] b scheme); + } + in + (scheme, `Decl (decl_id, nb)) + | Uninterpreted -> + let nu s = + Function + { binding = binding s; attrib; definition = Uninterpreted } + in + (scheme, `Decl (decl_id, nu)) + | Function definition -> + let e = + infer_expr ~univ:global_universe [%here] definition scheme + in + let ne scheme = + Function + { + binding = binding scheme; + attrib; + definition = + Function + (elaborate_expr ~univ:global_universe [%here] e scheme); + } + in + (scheme, `Decl (decl_id, ne))) + | Variable { binding; attrib; classification } -> + let scheme = decl_var_typ global_universe scheme binding in + let binding s = retype_var global_universe s binding in + let classification = + let tyv = + classification + |> Option.map (fun classi -> + infer_expr ~univ:global_universe [%here] classi scheme) + in + fun final_scheme -> + tyv + |> Option.map (fun e -> + elaborate_expr ~univ:global_universe [%here] e final_scheme) + in + let nb fscheme = + Variable + { + binding = binding fscheme; + attrib; + classification = classification fscheme; + } + in + (scheme, `Decl (decl_id, nb)) + | Procedure { definition } -> + let elaborate_proc, scheme = infer_proc prog scheme definition in + (scheme, `Procedure (decl_id, elaborate_proc)) + + (** The function that does everything *) + let infer_program prog = + let decls = Program.declarations prog |> Iter.to_list in + let constraints = ref [] in + let visit_constraint c = constraints := c :: !constraints in + (* We fold the inference context through every declaration and + calling the inference functions, returning an expressions typed with the + type expressions herein. We also return the resulting list of elaboration + functions, which take the final inference context and convert the HM-typed + expressions back to bincaml typed expressions. *) + let scheme, new_decls = + decls |> List.fold_map (infer_decl visit_constraint prog) TCtx.empty + in + let _ = solve_constraints ~max_iters:50 !constraints in + (* TODO: implicit decls; constructors need to be added after the types they + construct, probably simples to do implicits immediately after the thing they + relate to. Maybe they should just appear this way in the declaration + list. *) + let prog = + List.fold_left + (fun prog -> function + | `Decl (id, ndecl) -> + let decl = ndecl scheme in + (* assuming the id is the same (it has to be) *) + Program.update_decl prog decl + | `Procedure (id, nproc) -> + let proc = nproc scheme in + (* assuming the id is the same (it has to be) *) + let prog = Program.update_proc id (fun _ -> Some proc) prog in + prog) + prog new_decls + in + (scheme, prog) +end diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 39cf5b76..9c849132 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -39,6 +39,15 @@ module TypeExpr = TypeExpr +module Hm_types = Hm_types +(** Conversions to/form HM state and bincaml types *) + +module Unification = Unification +(** Unification of type-expressions *) + +module Solve_bv = Solve_bv +(** Simple solver for dependently-sized bitvectors *) + (** {1 Type Inference} Type inference is split into two phases, inference and elaboration. @@ -89,3 +98,72 @@ module TypeExpr = TypeExpr constructs bincaml-typed representations of these structures. *) module Inference = Inference +(** Traversal of expressions to infer types *) + +module Elaboration = Elaboration +(** Annotating the AST with the inferred types *) + +(** {1 High-level type-inference operations}*) + +open Common +open UnionFind +open Abstract_expr + +(* + TODO: + + In order to maintain well-typedness of rewrites we will probably want to + inject the global type definitions into the program, always. Otherwise we + probably risk inferring inconsistent types. Maybe this goes for for all the + global bindings. I.e. if we use a definition incorrectly it will end up + ill-typed and that error will be harder to track down. Injecting all the + bindings is somewhat giving up though. + + We could justifiably just require + transforms to "know what they are doing" and inject enough type information for + it to be well-typed coming out. Mistakes could be found by running a global + program typecheck after the transform. *) + +(** Algebra that infers types of expressions *) +let locally_elaborate_expr (e : Expr.BasilExpr.t) = + let open AbstractExpr in + let open Ops.AllOps in + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let constraints = ref [] in + let univ = "" in + let ctx = + Expr.BasilExpr.free_vars_iter e + |> Iter.fold (T.decl_var_typ univ) TypeExpr.TCtx.empty + in + let visit_constraint c = constraints := c :: !constraints in + (* TODO: need mode where we absorb take the existing annotations and try to + extend , rather than expecting everythign declared in context. *) + let i = T.infer_expr visit_constraint ~univ [%here] e ctx in + let _ = T.solve_constraints ~max_iters:100 !constraints in + let e = T.elaborate_expr ~univ [%here] i ctx in + e + +(** Algebra for returning the annotated type (for use with functions like + fold_with_type)*) +let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = + Expr.AbstractExpr.get_typ e + +(* Partially apply args list to function type funtype and return resulting type *) +let type_applied (funtype : Types.t) (args : Types.t list) = + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let rt = T.fresh_tvar ~n:"ret" () in + let args = List.map T.ty_of_basil args in + + let funt = T.curry_f args rt in + let ft = T.ty_of_basil funtype in + try + T.unify ~pos:[%here] ft funt |> ignore; + Ok (T.to_basil rt) + with Hm_types.TypeErr e -> Error e + +let elaborate_prog prog = + (* We need to create a local typing module in order to get fresh state for the + union find and hash cons. *) + let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in + let scheme, prog = T.infer_program prog in + prog diff --git a/lib/lang/hm/hm_types.ml b/lib/lang/hm/hm_types.ml new file mode 100644 index 00000000..88889de1 --- /dev/null +++ b/lib/lang/hm/hm_types.ml @@ -0,0 +1,121 @@ +(** Conversion from bincaml types to and from HM type infernece environment *) + +open Common +open UnionFind +open Abstract_expr + +exception TypeErr of string + +module Make (T : TypeExpr.TypeContext) = struct + module Ctx = T + include Ctx + include TypeExpr + include Typ + + type typ = T.Typ.t [@@deriving eq, ord] + + (** Recursion algebra for printing types *) + let printer_alg = function + | Var e -> ID.to_string e + | TypeConstr ([ l ], e) -> l ^ " " ^ e + | TypeConstr ([ a; b ], "->") -> a ^ " -> " ^ b + | TypeConstr ([], e) -> e + | TypeConstr (ls, e) -> + List.to_string ~start:"(" ~stop:")" ~sep:"," Fun.id ls ^ " " ^ e + + let type_to_string t = Rec.cata printer_alg t + + let plpos (l : Lexing.position) = + Printf.sprintf "%s:%d" l.pos_fname l.pos_lnum + + (** Type schemes; how values of the typing context are typed. *) + type scheme = Forall of tvar list * t + + let scheme_to_string = function + | Forall (tl, t) -> + List.to_string ID.to_string tl ^ ". " ^ type_to_string (find t) + + (** Function type, takes two arguments: we always curry. *) + let fun_type a b = TypeConstr ([ a; b ], "->") + + (** A type representing a number *) + let nat_val_type i = + let num = fix (TypeConstr ([], Int.to_string i)) in + TypeConstr ([ num ], "ℕ") + + let is_nat_val_type (i : t) = + match unfix i with + | TypeConstr ([ num ], "ℕ") -> ( + match unfix num with + | TypeConstr ([], num) -> Int.of_string num + | _ -> None) + | _ -> None + + (** A bitvector type parametric in its width *) + let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") + + (** Bitvector of arbitrary size *) + let bvunk i = TypeConstr ([ i ], "bv") + + (** {2 Primitive types} *) + + let int_type = TypeConstr ([], "int") + let bool_type = TypeConstr ([], "bool") + let unit_t = TypeConstr ([], "unit") + let top_t = TypeConstr ([], "top") + let nothing_t = TypeConstr ([], "nothing") + let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") + let ptr_typ = bv_type 64 + + let rec to_basil (t : t) : Types.t = + let wrapped t f = + try f () + with TypeErr e -> + raise (TypeErr ("error in " ^ (type_to_string @@ t) ^ ": " ^ e)) + in + let open Types in + wrapped t @@ fun () -> + match unfix t with + | TypeConstr ([ a; b ], "->") -> + let a = wrapped a @@ fun () -> to_basil a in + let b = wrapped b @@ fun () -> to_basil b in + Map (a, b) + | TypeConstr ([ w ], "bv") -> ( + match is_nat_val_type w with + | Some i -> Bitvector i + | None -> raise (TypeErr ("bitvector unresolved: " ^ type_to_string t))) + | TypeConstr ([], "unit") -> Unit + | TypeConstr ([], "bool") -> Boolean + | TypeConstr ([], "int") -> Integer + | TypeConstr ([], "top") -> Top + | TypeConstr ([], "nothing") -> Nothing + | TypeConstr ([], o) -> Sort (o, []) + | _ -> failwith "not impl" + + let rec ty_of_basil (t : Types.t) : t = + let e = + match t with + | Types.Boolean -> bool_type + | Types.Integer -> int_type + | Types.Bitvector i -> bv_type i + | Types.Unit -> unit_t + | Types.Top -> top_t + | Types.Nothing -> nothing_t + | Types.Map (a, b) -> fun_type (ty_of_basil a) (ty_of_basil b) + | Types.Sort (n, _) -> TypeConstr ([], n) + | Types.Struct _ -> failwith "unsupp" + | Types.Pointer { lower; upper } -> + ptr_typ_sub (ty_of_basil lower) (ty_of_basil upper) + | Types.Variable n -> Var (gen.fresh ~name:n ()) + in + fix e + + let curry (args : t expr list) (v : t expr) = + List.fold_left (fun a p -> fix @@ fun_type (fix p) a) (fix v) args + + let curry_f (args : t list) (v : t) = + List.fold_left (fun a p -> fix @@ fun_type p a) v args + + let types_universe = "" + let global_universe = "" +end diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 99fe8475..45dc0d9f 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -1,256 +1,39 @@ open Common open UnionFind open Abstract_expr +open Hm_types (** Hindley-Milner type inference based on a union-find. *) -module TypeInference (T : TypeExpr.TypeContext) = struct +module Make (T : TypeExpr.TypeContext) = struct open TypeExpr - include T - open Typ + include Solve_bv.Make (T) - (** Recursion algebra for printing types *) - let printer_alg = function - | Var e -> ID.to_string e - | TypeConstr ([ l ], e) -> l ^ " " ^ e - | TypeConstr ([ a; b ], "->") -> a ^ " -> " ^ b - | TypeConstr ([], e) -> e - | TypeConstr (ls, e) -> - List.to_string ~start:"(" ~stop:")" ~sep:"," Fun.id ls ^ " " ^ e - - let type_to_string t = Rec.cata printer_alg t - - (** Check for type recursion: recursion is failure. *) - let occurs_in a b = - let check = function - | Var t -> equal_tvar t a - | TypeConstr (ls, _) -> List.fold_left ( || ) false ls - in - Rec.cata check b - - let tmod_const a = TypeConstr ([ a ], "const") - let tmod_shared a = TypeConstr ([ a ], "shared") - - (** Function type, takes two arguments: we always curry. *) - let fun_type a b = TypeConstr ([ a; b ], "->") - - (** A type representing a number *) - let nat_val_type i = - let num = fix (TypeConstr ([], Int.to_string i)) in - TypeConstr ([ num ], "ℕ") - - let is_nat_val_type (i : t) = - match unfix i with - | TypeConstr ([ num ], "ℕ") -> ( - match unfix num with - | TypeConstr ([], num) -> Int.of_string num - | _ -> None) - | _ -> None - - (** A bitvector type parametric in its width *) - let bv_type i = map_expr fix @@ TypeConstr ([ nat_val_type i ], "bv") - - (** Primitive types *) - - let int_type = TypeConstr ([], "int") - let bool_type = TypeConstr ([], "bool") - let unit_t = TypeConstr ([], "unit") - let top_t = TypeConstr ([], "top") - let nothing_t = TypeConstr ([], "nothing") - let ptr_typ_sub a b = TypeConstr ([ a; b ], "ptr") - let ptr_typ = bv_type 64 - - exception TypeErr of string - - let rec to_basil (t : t) : Types.t = - let wrapped t f = - try f () - with TypeErr e -> - raise (TypeErr ("error in " ^ (type_to_string @@ t) ^ ": " ^ e)) - in - let open Types in - wrapped t @@ fun () -> - match unfix t with - | TypeConstr ([ a; b ], "->") -> - let a = wrapped a @@ fun () -> to_basil a in - let b = wrapped b @@ fun () -> to_basil b in - Map (a, b) - | TypeConstr ([ w ], "bv") -> ( - match is_nat_val_type w with - | Some i -> Bitvector i - | None -> raise (TypeErr ("bitvector unresolved: " ^ type_to_string t))) - | TypeConstr ([], "unit") -> Unit - | TypeConstr ([], "bool") -> Boolean - | TypeConstr ([], "int") -> Integer - | TypeConstr ([], "top") -> Top - | TypeConstr ([], "nothing") -> Nothing - | TypeConstr ([], o) -> Sort (o, []) - | _ -> failwith "not impl" - - type scheme = Forall of tvar list * t - - let scheme_to_string = function - | Forall (tl, t) -> - List.to_string ID.to_string tl ^ ". " ^ type_to_string (find t) - - module U = UnionFind - - let plpos (l : Lexing.position) = - Printf.sprintf "%s:%d" l.pos_fname l.pos_lnum - - let type_error a b = - let a = find a in - let b = find b in - raise - (TypeErr ("type_error: " ^ type_to_string a ^ " <> " ^ type_to_string b)) - - let recursion_error a b = - let b = find b in - raise - (TypeErr - ("recursive: tvar " ^ ID.to_string a ^ " occurs in " ^ type_to_string b)) - - (** Type unification.*) - let rec unify ?(pos = Lexing.dummy_pos) t t' = - Logs.debug (fun m -> - m "%s" - ("unify: " ^ plpos pos ^ " " - ^ type_to_string (find t) - ^ " with " - ^ type_to_string (find t'))); - match (map_expr unfix @@ Typ.unfix t, map_expr unfix @@ Typ.unfix t') with - | TypeConstr ([], "nothing"), _ -> t - | _, TypeConstr ([], "nothing") -> t' - | Var x, Var y -> union t t' - | Var x, _ when occurs_in x t' -> recursion_error x t' - | Var _, TypeConstr _ -> merge (fun a b -> b) t t' - | _, Var x -> unify ~pos:[%here] t' t - | TypeConstr ([ a ], "const"), TypeConstr ([ b ], "const") -> - let x = unify ~pos:[%here] (fix a) (fix b) in - fix @@ TypeConstr ([ x ], "const") - | TypeConstr ([ a ], "shared"), TypeConstr ([ b ], "shared") -> - let x = unify ~pos:[%here] (fix a) (fix b) in - fix @@ TypeConstr ([ x ], "const") - | o, TypeConstr ([ b ], "shared") | o, TypeConstr ([ b ], "const") -> - unify ~pos:[%here] t' t - | TypeConstr ([ b ], "shared"), o -> - let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in - fix @@ TypeConstr ([ b ], "shared") - | TypeConstr ([ b ], "const"), o -> - let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in - fix @@ TypeConstr ([ b ], "const") - | TypeConstr (ars, n), TypeConstr (ars', n') when not (String.equal n n') -> - type_error t t' - | TypeConstr (ars, n), TypeConstr (ars', n') - when List.length ars <> List.length ars' -> - type_error t t' - | ( TypeConstr ([ (Var v as vr) ], "bv"), - TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv") ) - | ( TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv"), - TypeConstr ([ (Var v as vr) ], "bv") ) -> - (* prioritise bitvec consts *) - let v = merge (fun _ c -> c) (fix vr) (fix cst) in - fix @@ TypeConstr ([ v ], "bv") - | TypeConstr (ars, n), TypeConstr (ars', n') -> - let args = - List.combine ars ars' - |> List.map (fun (a, b) -> unify ~pos:[%here] (fix a) (fix b)) - in - merge (fun a b -> TypeConstr (args, n)) t t' - - (** {2 Bitvector constraint solving} *) - - type dependent_bv_constraints = - | Add of { a : Typ.t; b : Typ.t; equ : Typ.t } (** a + b = equ*) - | AddConst of { a : Typ.t; b : int; equ : Typ.t } (** a + b = equ*) - - let show_dependent_bv_constraints = function - | Add { a; b; equ } -> - Printf.sprintf "%s + %s = %s" (type_to_string a) (type_to_string b) - (type_to_string equ) - | AddConst { a; b; equ } -> - Printf.sprintf "%s + (const %d) = %s" (type_to_string a) b - (type_to_string equ) - - let is_const a = is_nat_val_type a - - let unify_bv_constraint a : Typ.t option = - match a with - | Add { a; b; equ } -> ( - match List.map is_nat_val_type [ find a; find b; find equ ] with - | [ Some _; Some _; Some _ ] -> Some equ - | [ Some a; Some b; None ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (a + b)) equ) - | [ Some a; None; Some b ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) - | [ None; Some a; Some b ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) - | _ -> None) - | AddConst { a; b; equ } -> ( - match (is_nat_val_type (find a), is_nat_val_type (find equ)) with - | Some i, None -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) - | Some i, Some equ_c -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) - | None, Some e -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (e - b)) a) - | _ -> None) + (** An AbstractExpr.t with [t] used as the type. *) + module AbsTypingExpr = struct + open Ops + include AllOps + module Var = Var - (** Naive solver; loop over constraints and unify until everything is solved. - *) - let solve_constraints ~max_iters cls = - let show = List.to_string ~sep:"\n" show_dependent_bv_constraints in - let rec solve tries cs = - match cs with - | [] -> () - | _ when tries > max_iters -> - raise - (TypeErr - ("Gave up solving bitvec constraints with remaining:\n" ^ show cs)) - | cs -> - let remaining = - List.filter_map - (fun c -> - match unify_bv_constraint c with - | Some e -> None - | None -> Some c) - cs - in - solve (tries + 1) remaining - in - solve 0 cls + type var = Var.t - let gen = ID.make_gen () - let bv_type i = bv_type i + type t = E of (const, Var.t, unary, binary, intrin, typ, t) AbstractExpr.t + [@@unboxed] [@@deriving eq, ord] - (** {1 Type inference from exprs}*) + type nonrec typ = typ - (* Bitvector of unknown width *) - let bvunk i = TypeConstr ([ i ], "bv") + let top_typ = fix @@ top_t + let fix i = E i + let unfix i = match i with E i -> i + end - let rec ty_of_basil (t : Types.t) : t = - let e = - match t with - | Types.Boolean -> bool_type - | Types.Integer -> int_type - | Types.Bitvector i -> bv_type i - | Types.Unit -> unit_t - | Types.Top -> top_t - | Types.Nothing -> nothing_t - | Types.Map (a, b) -> fun_type (ty_of_basil a) (ty_of_basil b) - | Types.Sort (n, _) -> TypeConstr ([], n) - | Types.Struct _ -> failwith "unsupp" - | Types.Pointer { lower; upper } -> - ptr_typ_sub (ty_of_basil lower) (ty_of_basil upper) - | Types.Variable n -> Var (gen.fresh ~name:n ()) - in - fix e + module TypingExpr = Expr.Make (AbsTypingExpr) - let curry (args : t expr list) (v : t expr) = - List.fold_left (fun a p -> fix @@ fun_type (fix p) a) (fix v) args + let getty = AbsTypingExpr.unfix %> Expr.AbstractExpr.get_typ - let curry_f (args : t list) (v : t) = - List.fold_left (fun a p -> fix @@ fun_type p a) v args + let infer_var univ ctx id = + let typ = lookup_var_typ univ ctx id in + (id, typ) (** Return the generic type scheme for an op. We generalise the type, and hope dearly that a concrete type is found by inference. @@ -329,56 +112,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct curry_f [ m; a; b ] m | `Cases -> fv () - (* instantiate typescheme for a single type-annotated variable *) - let inst_annot_v ?(no_constraint = false) v = - let ty = - match Var.typ v with - | _ when no_constraint -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) - | Nothing -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) - | o -> ty_of_basil o - in - ty - - (* lookup var and add unify with its type annotation *) - let lookup_var_typ univ ?(no_constraint = false) c v = - let vt = inst_annot_v v in - let a = - let v = V.of_var univ v in - TCtx.find_opt v c |> function - | Some v -> v - | None -> failwith ("var not found: " ^ V.to_string v) - in - let tt = match a with Forall (_, ty) -> union ty vt in - tt - - type typ = t [@@deriving eq, ord] - - (** An AbstractExpr.t with [t] used as the type. *) - module AbsTypingExpr = struct - open Ops - include AllOps - module Var = Var - - type var = Var.t - - type t = E of (const, Var.t, unary, binary, intrin, typ, t) AbstractExpr.t - [@@unboxed] [@@deriving eq, ord] - - type nonrec typ = typ - - let top_typ = fix @@ top_t - let fix i = E i - let unfix i = match i with E i -> i - end - - module TypingExpr = Expr.Make (AbsTypingExpr) - - let getty = AbsTypingExpr.unfix %> Expr.AbstractExpr.get_typ - - let infer_var univ ctx id = - let typ = lookup_var_typ univ ctx id in - (id, typ) - let do_infer ~visit_constraint (infer : univ:string -> @@ -445,30 +178,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct AbsTypingExpr.fix (ApplyFun { typ = r; func = f; attrib; args }) | Let _ -> failwith "" - let types_universe = "" - let global_universe = "" - - (* declare type with name in type scheme *) - let decl_type ctx name vt = - let tvar = V.create types_universe name in - TCtx.update tvar - (function - | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) - | None -> Some (Forall ([], vt)) - | _ -> failwith "unk") - ctx - - (* declare var with type in type scheme *) - let decl_var_typ univ ?(no_constraint = false) c v = - let vvar = V.of_var univ v in - let vt = inst_annot_v v in - TCtx.update vvar - (function - | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) - | None -> Some (Forall ([], vt)) - | _ -> failwith "unk") - c - let rec infer_expr visit_constraint ~univ (hr : Lexing.position) e = fun (c : scheme TCtx.t) -> Logs.debug (fun m -> @@ -488,27 +197,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct in nexpr - let retype_var univ ctx id = - lookup_var_typ ~no_constraint:true univ ctx id |> find |> to_basil - |> fun typ -> Var.copy ~typ id - - (** Extract type after full inference has run. *) - let elaborate_expr ~univ (hr : Lexing.position) e (c : scheme TCtx.t) = - let alg e = - let e = - match e with - | AbstractExpr.RVar { id; attrib; typ } -> - (* avoid looking up the id in context as we may be in a local - binding *) - let id = Var.copy id ~typ:(to_basil @@ find typ) in - AbstractExpr.RVar { id; attrib; typ } - | o -> o - in - let t = AbstractExpr.get_typ e |> find |> to_basil in - AbstractExpr.set_typ e t |> Expr.BasilExpr.fix - in - e |> TypingExpr.cata alg - let unfix i = match i with Expr.BasilExpr.E i -> i let rec cata alg e = (unfix %> AbstractExpr.map (cata alg) %> alg) e @@ -529,15 +217,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct unify acc e) r p - let elaborate_phi univ ctx (p : Var.t Block.phi list) = - let open Block in - List.map - (fun { lhs; rhs } -> - let lhs = retype_var univ ctx lhs in - let rhs = List.map (fun (a, r) -> (a, retype_var univ ctx r)) rhs in - { lhs; rhs }) - p - let ctx_to_string ctx = TCtx.to_iter ctx |> Iter.to_string (fun (a, b) -> @@ -633,17 +312,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct Instr_Store { lhs; rhs; value; addr = Addr { addr; size; endian }; attrib } - let elaborate_stmt univ ctx stmt = - let retype_var v = - let typ = - lookup_var_typ ~no_constraint:true univ ctx v |> find |> to_basil - in - Var.copy ~typ v - in - Stmt.map - ~f_expr:(fun e -> elaborate_expr ~univ [%here] e ctx) - ~f_lvar:retype_var ~f_rvar:retype_var stmt - let infer_stmt vc p univ ctx s = try do_infer_stmt vc p univ ctx s with TypeErr m -> @@ -656,9 +324,6 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let _ = infer_phi vc univ ctx b.phis in Block.map ~phi:Fun.id (infer_stmt vc p univ ctx) b - let elaborate_block p univ ctx (b : ('a, 'b) Block.t) = - Block.map ~phi:(elaborate_phi univ ctx) (elaborate_stmt univ ctx) b - let assume_proc_decl ctx ?(no_constraint = false) (p : Program.proc) = let globs = Var.Decls.values (Procedure.local_decls p) in let formals_in = Procedure.formal_in_params p |> StringMap.values in @@ -671,239 +336,4 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (Iter.append globs @@ Iter.append formals_in formals_out) in ctx - - let infer_proc vc prog ctx ?(no_constraint = false) (p : Program.proc) = - let spec = Procedure.specification p in - let univ = V.proc_univ @@ Procedure.id p in - let ibool_list b = - List.map - (fun a -> - let a = infer_expr vc ~univ [%here] a ctx in - let _ = unify (fix bool_type) (getty a) in - a) - b - in - let spec : ('a, 'b) Procedure.proc_spec = - { - requires = ibool_list spec.requires; - ensures = ibool_list spec.ensures; - rely = ibool_list spec.rely; - guarantee = ibool_list spec.guarantee; - captures_globs = - List.map (infer_var global_universe ctx) spec.captures_globs; - modifies_globs = - List.map (infer_var global_universe ctx) spec.modifies_globs; - } - in - - let new_spec ctx : (Var.t, Expr.BasilExpr.t) Procedure.proc_spec = - { - requires = - List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.requires; - ensures = - List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.ensures; - rely = List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.rely; - guarantee = - List.map (fun e -> elaborate_expr ~univ [%here] e ctx) spec.guarantee; - captures_globs = spec.captures_globs |> List.map fst; - modifies_globs = spec.modifies_globs |> List.map fst; - } - in - - let ctx = assume_proc_decl ctx ~no_constraint p in - let bvlocks = - Procedure.iter_blocks_topo_fwd p - |> Iter.map (fun (i, b) -> (i, infer_block vc prog univ ctx b)) - |> Iter.persistent - in - - let elaborate_proc ctx = - Procedure.set_specification p (new_spec ctx) - |> (fun p -> - bvlocks - |> Iter.map (fun (bid, b) -> (bid, elaborate_block [%here] univ ctx b)) - |> Iter.fold (fun p (bid, b) -> Procedure.update_block p bid b) p) - |> Procedure.map_formal_in_params (StringMap.map (retype_var univ ctx)) - |> Procedure.map_formal_out_params (StringMap.map (retype_var univ ctx)) - in - Logs.debug (fun m -> m "%s" (ctx_to_string ctx)); - (elaborate_proc, ctx) - - (** Run type inference on a declaration, returning an updated typing scheme, - and elaboration function*) - let infer_decl visit_constraint prog scheme = - let open Program in - let infer_expr = infer_expr visit_constraint in - let infer_proc = infer_proc visit_constraint in - (* We have to be careful that inference is run immediately, not delayed until elaboration. *) - fun (decl_id, d) -> - match d with - | Type { binding; typ } -> - let ty = ty_of_basil typ in - let scheme = decl_type scheme binding ty in - let nty scheme = Type { binding; typ = to_basil (find ty) } in - (scheme, `Decl (decl_id, nty)) - | Function { binding; definition; attrib } -> ( - (* elaboration of var binding *) - let scheme = decl_var_typ global_universe scheme binding in - let binding s = retype_var global_universe s binding in - match definition with - | Axiom b -> - let bt = fix bool_type in - let b = infer_expr ~univ:global_universe [%here] b scheme in - let _ = unify (getty b) bt in - let nb scheme = - Function - { - attrib; - binding = binding scheme; - definition = - Axiom - (elaborate_expr ~univ:global_universe [%here] b scheme); - } - in - (scheme, `Decl (decl_id, nb)) - | Uninterpreted -> - let nu s = - Function - { binding = binding s; attrib; definition = Uninterpreted } - in - (scheme, `Decl (decl_id, nu)) - | Function definition -> - let e = - infer_expr ~univ:global_universe [%here] definition scheme - in - let ne scheme = - Function - { - binding = binding scheme; - attrib; - definition = - Function - (elaborate_expr ~univ:global_universe [%here] e scheme); - } - in - (scheme, `Decl (decl_id, ne))) - | Variable { binding; attrib; classification } -> - let scheme = decl_var_typ global_universe scheme binding in - let binding s = retype_var global_universe s binding in - let classification = - let tyv = - classification - |> Option.map (fun classi -> - infer_expr ~univ:global_universe [%here] classi scheme) - in - fun final_scheme -> - tyv - |> Option.map (fun e -> - elaborate_expr ~univ:global_universe [%here] e final_scheme) - in - let nb fscheme = - Variable - { - binding = binding fscheme; - attrib; - classification = classification fscheme; - } - in - (scheme, `Decl (decl_id, nb)) - | Procedure { definition } -> - let elaborate_proc, scheme = infer_proc prog scheme definition in - (scheme, `Procedure (decl_id, elaborate_proc)) - - (** The function that does everything *) - let infer_program prog = - let decls = Program.declarations prog |> Iter.to_list in - let constraints = ref [] in - let visit_constraint c = constraints := c :: !constraints in - (* We fold the inference context through every declaration and - calling the inference functions, returning an expressions typed with the - type expressions herein. We also return the resulting list of elaboration - functions, which take the final inference context and convert the HM-typed - expressions back to bincaml typed expressions. *) - let scheme, new_decls = - decls |> List.fold_map (infer_decl visit_constraint prog) TCtx.empty - in - let _ = solve_constraints ~max_iters:50 !constraints in - (* TODO: implicit decls; constructors need to be added after the types they - construct, probably simples to do implicits immediately after the thing they - relate to. Maybe they should just appear this way in the declaration - list. *) - let prog = - List.fold_left - (fun prog -> function - | `Decl (id, ndecl) -> - let decl = ndecl scheme in - (* assuming the id is the same (it has to be) *) - Program.update_decl prog decl - | `Procedure (id, nproc) -> - let proc = nproc scheme in - (* assuming the id is the same (it has to be) *) - let prog = Program.update_proc id (fun _ -> Some proc) prog in - prog) - prog new_decls - in - (scheme, prog) end - -module T = TypeInference (TypeExpr.Make ()) - -module type HM = module type of TypeInference (TypeExpr.Make ()) - -(* - TODO: - - In order to maintain well-typedness of rewrites we will probably want to - inject the global type definitions into the program, always. Otherwise we - probably risk inferring inconsistent types. Maybe this goes for for all the - global bindings. I.e. if we use a definition incorrectly it will end up - ill-typed and that error will be harder to track down. Injecting all the - bindings is somewhat giving up though. - - We could justifiably just require - transforms to "know what they are doing" and inject enough type information for - it to be well-typed coming out. Mistakes could be found by running a global - program typecheck after the transform. *) - -(** Algebra that infers types of expressions *) -let locally_elaborate_expr (e : Expr.BasilExpr.t) = - let open AbstractExpr in - let open Ops.AllOps in - let module T = TypeInference (TypeExpr.Make ()) in - let constraints = ref [] in - let univ = "" in - let ctx = - Expr.BasilExpr.free_vars_iter e - |> Iter.fold (T.decl_var_typ univ) TypeExpr.TCtx.empty - in - let visit_constraint c = constraints := c :: !constraints in - (* TODO: need mode where we absorb take the existing annotations and try to - extend , rather than expecting everythign declared in context. *) - let i = T.infer_expr visit_constraint ~univ [%here] e ctx in - let _ = T.solve_constraints ~max_iters:100 !constraints in - let e = T.elaborate_expr ~univ [%here] i ctx in - e - -(** Algebra for returning the annotated type (for use with functions like - fold_with_type)*) -let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = - Expr.AbstractExpr.get_typ e - -(* Partially apply args list to function type funtype and return resulting type *) -let type_applied (funtype : Types.t) (args : Types.t list) = - let module T = TypeInference (TypeExpr.Make ()) in - let rt = T.fresh_tvar ~n:"ret" () in - let args = List.map T.ty_of_basil args in - let funt = T.curry_f args rt in - let ft = T.ty_of_basil funtype in - try - T.unify ~pos:[%here] ft funt |> ignore; - Ok (T.to_basil rt) - with T.TypeErr e -> Error e - -let elaborate prog = - (* We need to create a local typing module in order to get fresh state for the - union find and hash cons. *) - let module T = TypeInference (TypeExpr.Make ()) in - let scheme, prog = T.infer_program prog in - prog diff --git a/lib/lang/hm/solve_bv.ml b/lib/lang/hm/solve_bv.ml new file mode 100644 index 00000000..08095288 --- /dev/null +++ b/lib/lang/hm/solve_bv.ml @@ -0,0 +1,72 @@ +(** Solve constraint system of dependently width typed bitvectors *) + +open Common +open UnionFind +open Abstract_expr +open Hm_types + +module Make (T : TypeExpr.TypeContext) = struct + include Unification.Make (T) + + (** Naive solver *) + + (** Constraints between nat val types. *) + type dependent_bv_constraints = + | Add of { a : Typ.t; b : Typ.t; equ : Typ.t } (** a + b = equ*) + | AddConst of { a : Typ.t; b : int; equ : Typ.t } (** a + b = equ*) + + let show_dependent_bv_constraints = function + | Add { a; b; equ } -> + Printf.sprintf "%s + %s = %s" (type_to_string a) (type_to_string b) + (type_to_string equ) + | AddConst { a; b; equ } -> + Printf.sprintf "%s + (const %d) = %s" (type_to_string a) b + (type_to_string equ) + + (** Deduce the width if two values of the constraint have inferred widths *) + let unify_bv_constraint a : Typ.t option = + match a with + | Add { a; b; equ } -> ( + match List.map is_nat_val_type [ find a; find b; find equ ] with + | [ Some _; Some _; Some _ ] -> Some equ + | [ Some a; Some b; None ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a + b)) equ) + | [ Some a; None; Some b ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) + | [ None; Some a; Some b ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) + | _ -> None) + | AddConst { a; b; equ } -> ( + match (is_nat_val_type (find a), is_nat_val_type (find equ)) with + | Some i, None -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) + | Some i, Some equ_c -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) + | None, Some e -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e - b)) a) + | _ -> None) + + (** Naive solver; loop over constraints and unify until everything is solved. + *) + let solve_constraints ~max_iters cls = + let show = List.to_string ~sep:"\n" show_dependent_bv_constraints in + let rec solve tries cs = + match cs with + | [] -> () + | _ when tries > max_iters -> + raise + (TypeErr + ("Gave up solving bitvec constraints with remaining:\n" ^ show cs)) + | cs -> + let remaining = + List.filter_map + (fun c -> + match unify_bv_constraint c with + | Some e -> None + | None -> Some c) + cs + in + solve (tries + 1) remaining + in + solve 0 cls +end diff --git a/lib/lang/hm/typeExpr.ml b/lib/lang/hm/typeExpr.ml index 4b500058..8c4f9068 100644 --- a/lib/lang/hm/typeExpr.ml +++ b/lib/lang/hm/typeExpr.ml @@ -49,7 +49,7 @@ end relations. This must be done each time we want to perform inference in an independent environment, in order to construct a fresh hash-consing and union-find state. *) -module Make () = struct +module MakeFresh () = struct module Typ = struct include ATyp @@ -76,11 +76,11 @@ module Make () = struct module H = Fix.HashCons.Make (M) - let unfix = + let unfix : t -> t expr = Fix.HashCons.data %> UnionFind.find %> UnionFind.get %> function | T e -> e - let fix e = H.make (UnionFind.make (T e)) + let fix (e : t expr) : t = H.make (UnionFind.make (T e)) let union (a : t) (b : t) : t = H.make @@ UnionFind.union (Fix.HashCons.data a) (Fix.HashCons.data b) @@ -94,13 +94,16 @@ module Make () = struct @@ UnionFind.merge (fun (T a) (T b) -> T (f a b)) (Fix.HashCons.data a) (Fix.HashCons.data b) + + let compare a b = Fix.HashCons.compare a b + let equal a b = Fix.HashCons.equal a b end - let compare a b = Fix.HashCons.compare a b - let equal a b = Fix.HashCons.equal a b + (** type name generator *) + let gen = ID.make_gen () module Rec = Bincaml_util.Recursionscheme.Recursion (Typ) end -module type TypeContext = module type of Make () +module type TypeContext = module type of MakeFresh () (** Type of mutable type context union find *) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml new file mode 100644 index 00000000..465ed99f --- /dev/null +++ b/lib/lang/hm/unification.ml @@ -0,0 +1,124 @@ +(** Unification of types *) + +open Common +open UnionFind +open Abstract_expr + +module Make (T : TypeExpr.TypeContext) = struct + open TypeExpr + include T + include Typ + open Hm_types + include Hm_types.Make (T) + + let type_error a b = + let a = find a in + let b = find b in + raise + (TypeErr ("type_error: " ^ type_to_string a ^ " <> " ^ type_to_string b)) + + let recursion_error a b = + let b = find b in + raise + (TypeErr + ("recursive: tvar " ^ ID.to_string a ^ " occurs in " ^ type_to_string b)) + + (** Check for type recursion: recursion is failure. *) + let occurs_in a b = + let check = function + | Var t -> equal_tvar t a + | TypeConstr (ls, _) -> List.fold_left ( || ) false ls + in + Rec.cata check b + + (** Type unification.*) + let rec unify ?(pos = Lexing.dummy_pos) t t' = + Logs.debug (fun m -> + m "%s" + ("unify: " ^ plpos pos ^ " " + ^ type_to_string (find t) + ^ " with " + ^ type_to_string (find t'))); + match (map_expr unfix @@ Typ.unfix t, map_expr unfix @@ Typ.unfix t') with + | TypeConstr ([], "nothing"), _ -> t + | _, TypeConstr ([], "nothing") -> t' + | Var x, Var y -> union t t' + | Var x, _ when occurs_in x t' -> recursion_error x t' + | Var _, TypeConstr _ -> merge (fun a b -> b) t t' + | _, Var x -> unify ~pos:[%here] t' t + | TypeConstr ([ a ], "const"), TypeConstr ([ b ], "const") -> + let x = unify ~pos:[%here] (fix a) (fix b) in + fix @@ TypeConstr ([ x ], "const") + | TypeConstr ([ a ], "shared"), TypeConstr ([ b ], "shared") -> + let x = unify ~pos:[%here] (fix a) (fix b) in + fix @@ TypeConstr ([ x ], "const") + | o, TypeConstr ([ b ], "shared") | o, TypeConstr ([ b ], "const") -> + unify ~pos:[%here] t' t + | TypeConstr ([ b ], "shared"), o -> + let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in + fix @@ TypeConstr ([ b ], "shared") + | TypeConstr ([ b ], "const"), o -> + let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in + fix @@ TypeConstr ([ b ], "const") + | TypeConstr (ars, n), TypeConstr (ars', n') when not (String.equal n n') -> + type_error t t' + | TypeConstr (ars, n), TypeConstr (ars', n') + when List.length ars <> List.length ars' -> + type_error t t' + | ( TypeConstr ([ (Var v as vr) ], "bv"), + TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv") ) + | ( TypeConstr ([ (TypeConstr ([], a) as cst) ], "bv"), + TypeConstr ([ (Var v as vr) ], "bv") ) -> + (* prioritise bitvec consts *) + let v = merge (fun _ c -> c) (fix vr) (fix cst) in + fix @@ TypeConstr ([ v ], "bv") + | TypeConstr (ars, n), TypeConstr (ars', n') -> + let args = + List.combine ars ars' + |> List.map (fun (a, b) -> unify ~pos:[%here] (fix a) (fix b)) + in + merge (fun a b -> TypeConstr (args, n)) t t' + + (* instantiate typescheme for a single type-annotated variable *) + let inst_annot_v ?(no_constraint = false) v = + let ty = + match Var.typ v with + | _ when no_constraint -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | Nothing -> fix @@ Var (gen.fresh ~name:(Var.name v) ()) + | o -> ty_of_basil o + in + ty + + (* lookup var and add unify with its type annotation *) + let lookup_var_typ univ ?(no_constraint = false) c v = + let vt = inst_annot_v v in + let a = + let v = V.of_var univ v in + TCtx.find_opt v c |> function + | Some v -> v + | None -> failwith ("var not found: " ^ V.to_string v) + in + let tt = match a with Forall (_, ty) -> union ty vt in + tt + + (* declare type with name in type scheme *) + let decl_type ctx name vt = + let tvar = V.create types_universe name in + TCtx.update tvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + ctx + + (* declare var with type in type scheme *) + let decl_var_typ univ ?(no_constraint = false) c v = + let vvar = V.of_var univ v in + let vt = inst_annot_v v in + TCtx.update vvar + (function + | Some (Forall ([], t)) -> Some (Forall ([], unify vt t)) + | None -> Some (Forall ([], vt)) + | _ -> failwith "unk") + c +end diff --git a/lib/passes.ml b/lib/passes.ml index 6d0a1933..e753dd81 100644 --- a/lib/passes.ml +++ b/lib/passes.ml @@ -31,7 +31,7 @@ module PassManager = struct let hm_elaborate = { name = "hindley-milner-elaborate"; - apply = Prog Hm.Inference.elaborate; + apply = Prog Hm.elaborate_prog; invariants = Invariants.make (); doc = "Perform hindley milner type inference on program"; } diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml index c139e1f5..8b1477b0 100644 --- a/test/lang/test_hm.ml +++ b/test/lang/test_hm.ml @@ -1,6 +1,6 @@ open Lang open Common -open Hm.Inference +open Hm module HMDifferential = struct let arb_expr = @@ -35,10 +35,12 @@ module HMDifferential = struct predicate end +type t = Alcotest.speed_level + let _ = let suite = List.map - (QCheck_alcotest.to_alcotest ~long:true ~speed_level:`Slow ~verbose:true) + (QCheck_alcotest.to_alcotest ~long:false ~speed_level:`Quick ~verbose:true) [ HMDifferential.test ] in Alcotest.run "hm" [ ("diff", suite) ] diff --git a/test/lang/test_hm_inline.ml b/test/lang/test_hm_inline.ml index ef71de3d..e7fea613 100644 --- a/test/lang/test_hm_inline.ml +++ b/test/lang/test_hm_inline.ml @@ -1,6 +1,6 @@ open Lang open Common -open Hm.Inference +open Hm let%expect_test "return type of function" = let open Types in From 2adcd51c8ff71fb13a9cb1cb4ec018e319afccea Mon Sep 17 00:00:00 2001 From: agle Date: Tue, 14 Jul 2026 14:00:04 +1000 Subject: [PATCH 13/22] fix test when same var of diff types --- test/lang/expr_gen.ml | 2 +- test/lang/test_hm.ml | 23 +++++++++++++++++++---- 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/test/lang/expr_gen.ml b/test/lang/expr_gen.ml index eecba9f5..e0709e3d 100644 --- a/test/lang/expr_gen.ml +++ b/test/lang/expr_gen.ml @@ -61,7 +61,7 @@ let gen_bvconst ?min w = return (BasilExpr.bvconst c) let vname = - let v = int_bound 8 in + let v = int_range 1 3 in let vl = "abcdefghijklmnopqrstuvwxyz" |> String.to_list in let vl = vl @ List.map Char.uppercase_ascii vl in let cs = QCheck.Gen.oneof_list vl in diff --git a/test/lang/test_hm.ml b/test/lang/test_hm.ml index 8b1477b0..b99a6fe6 100644 --- a/test/lang/test_hm.ml +++ b/test/lang/test_hm.ml @@ -28,15 +28,30 @@ module HMDifferential = struct let inf_hm = infer exp in return (exp, inf_b, inf_hm) - let predicate (a, b, hm) = Result.is_ok hm && Types.equal b (Result.get_ok hm) + let expect_type_error e = + (* multiple variables with different types *) + let has_type (acc, m) v = + let e = + StringMap.find_opt (Var.name v) m + |> Option.for_all (Types.equal (Var.typ v)) + in + (acc && e, StringMap.add (Var.name v) (Var.typ v) m) + in + let var_types_compat, _ = + Expr.BasilExpr.free_vars_iter e + |> Iter.fold has_type (true, StringMap.empty) + in + not var_types_compat + + let predicate (a, b, hm) = + (expect_type_error a && Result.is_error hm) + || (Result.is_ok hm && Types.equal b (Result.get_ok hm)) let test = - QCheck.Test.make ~name:"Hm inference matches" ~count:1000 ~max_fail:1 gener + QCheck.Test.make ~name:"Hm inference matches" ~count:10000 ~max_fail:1 gener predicate end -type t = Alcotest.speed_level - let _ = let suite = List.map From 19cfa6a2bfba567f135333a74e5a10a6f7a3858d Mon Sep 17 00:00:00 2001 From: agle Date: Tue, 14 Jul 2026 14:21:11 +1000 Subject: [PATCH 14/22] docs --- lib/lang/hm/hm.ml | 111 +++++++++++++++++++++++-------------- lib/lang/hm/unification.ml | 2 +- 2 files changed, 71 insertions(+), 42 deletions(-) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 9c849132..39d2df22 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -1,5 +1,6 @@ (** Simple hindley-milner type inference *) +module TypeExpr = TypeExpr (** {1 Type Expressions} Bincaml's AST is generic in the type annotation expression. @@ -37,17 +38,6 @@ This type is placed in a union-find datastructre in order to perform type unification. *) -module TypeExpr = TypeExpr - -module Hm_types = Hm_types -(** Conversions to/form HM state and bincaml types *) - -module Unification = Unification -(** Unification of type-expressions *) - -module Solve_bv = Solve_bv -(** Simple solver for dependently-sized bitvectors *) - (** {1 Type Inference} Type inference is split into two phases, inference and elaboration. @@ -55,53 +45,89 @@ module Solve_bv = Solve_bv type errors when conflicts arise. Elaboration anotates the program with these expressions. - {2 Inference} + {2 Inference} *) - We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of - each expression, and perform unification to determine what the type is. +module Hm_types = Hm_types +(** Conversions to/form HM state and bincaml types *) - {3 Parametric Bitvectors} +module Unification = Unification +module Inference = Inference - Bitvector types are parametric in their widths, technically some operations, - such as concatenation, are typed depending on the arguments passed to them. - For now our approach is to hope there is enogugh typing information to fully - propagate concrete types. +(** Traversal of expressions to infer types - We define the types like "5" to represent the number 5. The "Bitvector" type - is parametric in its width type, i.e [bv5] is defined as - {[TypeConstr ([TypeConstr ([],"5")], "bv")]}. When we do not know the exact - width we use a type variable, and rely on unification to determine the - precise type. Our type constraints cannot fully represent our - value-dependent bitvector widths, this will fail (emitting a type varable) - unless there are sufficient type annotations. + We traverse the bincaml AST and construct a {! TypeExpr.t} for the type of + each expression, and perform unification to determine what the type is. - {3 Ad-hoc polymorpic operators} + Bincaml has some specific concerns: for its type system: - Bincaml has some specific concerns, namely our operators are ad-hoc - polymorphic. For each op (e.g. bvadd) + {3 Ad-hoc polymorpic operators} - A type-scheme in HM is a non-recursive universal quantifier over type - variables. + Our operators are ad-hoc polymorphic. Polymorphism in HM is represented with + type schemes. A type-scheme in HM is a non-recursive universal quantifier + over type variables. - {[type scheme = Forall of tvar list * t]} + {[ + type scheme = Forall of tvar list * t + ]} We represent our ad-hoc polymorphic operators by immediately generalising them, returning a type scheme for a generic function type. For instance for [bvadd] we know all the widths have to be equal, so the type scheme is - [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] + [bvadd :: Forall i : Bitvector i -> Bitvector i -> Bitvector i] *) - {2 Elaboration} +module Solve_bv = Solve_bv - As the inference returns a version of the program typed with the HM - [TypeExpr]s, the elaboration amounts to a traversal of the program which - constructs bincaml-typed representations of these structures. *) +(** {3 Parametric Bitvectors} -module Inference = Inference -(** Traversal of expressions to infer types *) + For cases like [bvadd], it is enough that one of their arguments (or return) + be type annotated in order to infer concrete types for all type variables in + the type scheme. + + However some operations, such as concatenation, are typed depending on + arithmetic over the width values of the arguments passed to them. + + We define the type constructor ℕ to represent numeric types, we interpret it + as a number when its argument is a type constructor which is the string + representation of a number. E.g. the type "5 ℕ" represents the number 5. + + The [bv] bitvector type is parametric in its width, i.e [bv5] is defined as; + + {[ + TypeConstr ([5 ℕ, "bv") + ]} + + When we do not know the exact width we use a type variable, and rely on + unification, and a width-solving post-pass to determine the precise type. + + If there is not enough information to determine a concrete width, extraction + to a bincaml type will fail with a type error. + + In order to solve for widths, we represent width-dependent operations as a a + pair of a type scheme and type constraint. E.g. for [concat] this type + constraint is of the form + + {[ + (* scheme *) + concat :: Forall a b c : Bitvector a -> Bitvector b -> Bitvector c + + (* constraint *) + Add { a ; b; equ=c } (** a + b = c *) + ]} + + These constraints are collected, and solved iteratively after the inference + pass has run. This proces is naive and exponential in the number of + deductive steps it has to make. *) module Elaboration = Elaboration -(** Annotating the AST with the inferred types *) +(** {2 Elaboration} + + As the inference returns a version of the program typed with the HM + [TypeExpr]s, the elaboration amounts to a traversal of the program which + constructs bincaml-typed representations of these structures. + + This module implements both inference and elaboratino for the high-level + program structures as this simplifies book-keeping of types. *) (** {1 High-level type-inference operations}*) @@ -124,7 +150,8 @@ open Abstract_expr it to be well-typed coming out. Mistakes could be found by running a global program typecheck after the transform. *) -(** Algebra that infers types of expressions *) +(** Algebra that infers types of expressions in a fresh local context, assuming + all free variables are defined and annotated. *) let locally_elaborate_expr (e : Expr.BasilExpr.t) = let open AbstractExpr in let open Ops.AllOps in @@ -161,6 +188,8 @@ let type_applied (funtype : Types.t) (args : Types.t list) = Ok (T.to_basil rt) with Hm_types.TypeErr e -> Error e +(** Apply type inference to a program and return a fully type-annotated copy of + the program. *) let elaborate_prog prog = (* We need to create a local typing module in order to get fresh state for the union find and hash cons. *) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml index 465ed99f..210219d7 100644 --- a/lib/lang/hm/unification.ml +++ b/lib/lang/hm/unification.ml @@ -1,4 +1,4 @@ -(** Unification of types *) +(** Unification of type expressions *) open Common open UnionFind From 715da7b1e8ec77838cc2dfee08a216f577d47dba Mon Sep 17 00:00:00 2001 From: am Date: Tue, 14 Jul 2026 16:14:12 +1000 Subject: [PATCH 15/22] Update lib/lang/hm/inference.ml Co-authored-by: Kait <39479354+katrinafyi@users.noreply.github.com> --- lib/lang/hm/inference.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 45dc0d9f..1d2a1e04 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -69,7 +69,7 @@ module Make (T : TypeExpr.TypeContext) = struct | `INTNEG -> curry [ int_type ] int_type | #Ops.IntOps.binary_pred -> curry [ int_type; int_type ] bool_type | #Ops.IntOps.const -> fix @@ int_type - | #Ops.IntOps.binary_unif -> curry [ int_type; int_type ] bool_type + | #Ops.IntOps.binary_unif -> curry [ int_type; int_type ] int_type | #Ops.LogicalOps.binary -> curry [ bool_type; bool_type ] bool_type | #Ops.LogicalOps.unary -> curry [ bool_type ] bool_type | #Ops.LogicalOps.const -> fix @@ bool_type From d1c631352afe382a570c25a8818797efa2161ff7 Mon Sep 17 00:00:00 2001 From: agle Date: Tue, 14 Jul 2026 16:36:04 +1000 Subject: [PATCH 16/22] fixes --- lib/lang/hm/elaboration.ml | 1 - lib/lang/hm/hm.ml | 1 - lib/lang/hm/hm_types.ml | 1 - lib/lang/hm/inference.ml | 1 - lib/lang/hm/solve_bv.ml | 33 +++++++++++++++++++-------------- lib/lang/hm/unification.ml | 19 ++----------------- 6 files changed, 21 insertions(+), 35 deletions(-) diff --git a/lib/lang/hm/elaboration.ml b/lib/lang/hm/elaboration.ml index 8714c18d..aa69c1c0 100644 --- a/lib/lang/hm/elaboration.ml +++ b/lib/lang/hm/elaboration.ml @@ -1,5 +1,4 @@ open Common -open UnionFind open Abstract_expr (** Hindley-Milner type inference based on a union-find. *) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 39d2df22..23e345ac 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -132,7 +132,6 @@ module Elaboration = Elaboration (** {1 High-level type-inference operations}*) open Common -open UnionFind open Abstract_expr (* diff --git a/lib/lang/hm/hm_types.ml b/lib/lang/hm/hm_types.ml index 88889de1..23022539 100644 --- a/lib/lang/hm/hm_types.ml +++ b/lib/lang/hm/hm_types.ml @@ -1,7 +1,6 @@ (** Conversion from bincaml types to and from HM type infernece environment *) open Common -open UnionFind open Abstract_expr exception TypeErr of string diff --git a/lib/lang/hm/inference.ml b/lib/lang/hm/inference.ml index 1d2a1e04..123f49e3 100644 --- a/lib/lang/hm/inference.ml +++ b/lib/lang/hm/inference.ml @@ -1,5 +1,4 @@ open Common -open UnionFind open Abstract_expr open Hm_types diff --git a/lib/lang/hm/solve_bv.ml b/lib/lang/hm/solve_bv.ml index 08095288..def11dbb 100644 --- a/lib/lang/hm/solve_bv.ml +++ b/lib/lang/hm/solve_bv.ml @@ -1,7 +1,6 @@ (** Solve constraint system of dependently width typed bitvectors *) open Common -open UnionFind open Abstract_expr open Hm_types @@ -28,22 +27,28 @@ module Make (T : TypeExpr.TypeContext) = struct match a with | Add { a; b; equ } -> ( match List.map is_nat_val_type [ find a; find b; find equ ] with - | [ Some _; Some _; Some _ ] -> Some equ - | [ Some a; Some b; None ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (a + b)) equ) - | [ Some a; None; Some b ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) - | [ None; Some a; Some b ] -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (b - a)) equ) + | [ Some a_n; Some b_n; Some e_n ] -> + (* check constraint *) + if a_n + b_n <> e_n then + type_error (fix @@ nat_val_type (a_n + b_n)) equ; + Some equ + | [ Some a_n; Some b_n; None ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a_n + b_n)) equ) + | [ Some a_n; None; Some e_n ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - a_n)) b) + | [ None; Some b_n; Some e_n ] -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - b_n)) a) | _ -> None) | AddConst { a; b; equ } -> ( match (is_nat_val_type (find a), is_nat_val_type (find equ)) with - | Some i, None -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) - | Some i, Some equ_c -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (i + b)) equ) - | None, Some e -> - Some (unify ~pos:[%here] (fix @@ nat_val_type (e - b)) a) + | Some a_n, Some e_n -> + (* check constraint *) + let e = fix @@ nat_val_type (a_n + b) in + Some (unify ~pos:[%here] e equ) + | Some a_n, None -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (a_n + b)) equ) + | None, Some e_n -> + Some (unify ~pos:[%here] (fix @@ nat_val_type (e_n - b)) a) | _ -> None) (** Naive solver; loop over constraints and unify until everything is solved. diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml index 210219d7..9e6e7302 100644 --- a/lib/lang/hm/unification.ml +++ b/lib/lang/hm/unification.ml @@ -1,7 +1,6 @@ (** Unification of type expressions *) open Common -open UnionFind open Abstract_expr module Make (T : TypeExpr.TypeContext) = struct @@ -27,7 +26,7 @@ module Make (T : TypeExpr.TypeContext) = struct let occurs_in a b = let check = function | Var t -> equal_tvar t a - | TypeConstr (ls, _) -> List.fold_left ( || ) false ls + | TypeConstr (ls, _) -> List.for_all Fun.id ls in Rec.cata check b @@ -42,24 +41,10 @@ module Make (T : TypeExpr.TypeContext) = struct match (map_expr unfix @@ Typ.unfix t, map_expr unfix @@ Typ.unfix t') with | TypeConstr ([], "nothing"), _ -> t | _, TypeConstr ([], "nothing") -> t' - | Var x, Var y -> union t t' + | Var x, Var y -> Typ.union t t' | Var x, _ when occurs_in x t' -> recursion_error x t' | Var _, TypeConstr _ -> merge (fun a b -> b) t t' | _, Var x -> unify ~pos:[%here] t' t - | TypeConstr ([ a ], "const"), TypeConstr ([ b ], "const") -> - let x = unify ~pos:[%here] (fix a) (fix b) in - fix @@ TypeConstr ([ x ], "const") - | TypeConstr ([ a ], "shared"), TypeConstr ([ b ], "shared") -> - let x = unify ~pos:[%here] (fix a) (fix b) in - fix @@ TypeConstr ([ x ], "const") - | o, TypeConstr ([ b ], "shared") | o, TypeConstr ([ b ], "const") -> - unify ~pos:[%here] t' t - | TypeConstr ([ b ], "shared"), o -> - let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in - fix @@ TypeConstr ([ b ], "shared") - | TypeConstr ([ b ], "const"), o -> - let b = unify ~pos:[%here] (fix b) (fix (map_expr fix o)) in - fix @@ TypeConstr ([ b ], "const") | TypeConstr (ars, n), TypeConstr (ars', n') when not (String.equal n n') -> type_error t t' | TypeConstr (ars, n), TypeConstr (ars', n') From d345c4707958f6b6fbdaeb95e22e5f9af50d477e Mon Sep 17 00:00:00 2001 From: am Date: Wed, 15 Jul 2026 11:38:27 +1000 Subject: [PATCH 17/22] doc comments Co-authored-by: Kait <39479354+katrinafyi@users.noreply.github.com> --- lib/lang/hm/unification.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml index 9e6e7302..fcf568d8 100644 --- a/lib/lang/hm/unification.ml +++ b/lib/lang/hm/unification.ml @@ -64,7 +64,7 @@ module Make (T : TypeExpr.TypeContext) = struct in merge (fun a b -> TypeConstr (args, n)) t t' - (* instantiate typescheme for a single type-annotated variable *) + (** instantiate typescheme for a single type-annotated variable *) let inst_annot_v ?(no_constraint = false) v = let ty = match Var.typ v with @@ -74,7 +74,7 @@ module Make (T : TypeExpr.TypeContext) = struct in ty - (* lookup var and add unify with its type annotation *) + (** lookup var and add unify with its type annotation *) let lookup_var_typ univ ?(no_constraint = false) c v = let vt = inst_annot_v v in let a = @@ -86,7 +86,7 @@ module Make (T : TypeExpr.TypeContext) = struct let tt = match a with Forall (_, ty) -> union ty vt in tt - (* declare type with name in type scheme *) + (** declare type with name in type scheme *) let decl_type ctx name vt = let tvar = V.create types_universe name in TCtx.update tvar From 54a8814ac0c601d561a6673bacc4e8a8c77aba26 Mon Sep 17 00:00:00 2001 From: am Date: Wed, 15 Jul 2026 11:47:48 +1000 Subject: [PATCH 18/22] doc suggestions Co-authored-by: Kait <39479354+katrinafyi@users.noreply.github.com> --- lib/lang/hm/hm.ml | 2 +- lib/lang/hm/hm_types.ml | 2 +- lib/lang/hm/solve_bv.ml | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 23e345ac..0f3cb751 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -174,7 +174,7 @@ let locally_elaborate_expr (e : Expr.BasilExpr.t) = let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = Expr.AbstractExpr.get_typ e -(* Partially apply args list to function type funtype and return resulting type *) +(** Partially apply args list to function type funtype and return resulting type *) let type_applied (funtype : Types.t) (args : Types.t list) = let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in let rt = T.fresh_tvar ~n:"ret" () in diff --git a/lib/lang/hm/hm_types.ml b/lib/lang/hm/hm_types.ml index 23022539..1563b94e 100644 --- a/lib/lang/hm/hm_types.ml +++ b/lib/lang/hm/hm_types.ml @@ -1,4 +1,4 @@ -(** Conversion from bincaml types to and from HM type infernece environment *) +(** Conversion from bincaml types to and from HM type inference environment *) open Common open Abstract_expr diff --git a/lib/lang/hm/solve_bv.ml b/lib/lang/hm/solve_bv.ml index def11dbb..1d00c305 100644 --- a/lib/lang/hm/solve_bv.ml +++ b/lib/lang/hm/solve_bv.ml @@ -23,8 +23,8 @@ module Make (T : TypeExpr.TypeContext) = struct (type_to_string equ) (** Deduce the width if two values of the constraint have inferred widths *) - let unify_bv_constraint a : Typ.t option = - match a with + let unify_bv_constraint constr : Typ.t option = + match constr with | Add { a; b; equ } -> ( match List.map is_nat_val_type [ find a; find b; find equ ] with | [ Some a_n; Some b_n; Some e_n ] -> From 41b36be8c2f3ddde1f4e9e7a2a351d51be5f071f Mon Sep 17 00:00:00 2001 From: am Date: Wed, 15 Jul 2026 11:49:36 +1000 Subject: [PATCH 19/22] Apply suggestions from code review Co-authored-by: Kait <39479354+katrinafyi@users.noreply.github.com> --- lib/lang/hm/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml index fcf568d8..4e718a90 100644 --- a/lib/lang/hm/unification.ml +++ b/lib/lang/hm/unification.ml @@ -96,7 +96,7 @@ module Make (T : TypeExpr.TypeContext) = struct | _ -> failwith "unk") ctx - (* declare var with type in type scheme *) + (** declare var with type in type scheme *) let decl_var_typ univ ?(no_constraint = false) c v = let vvar = V.of_var univ v in let vt = inst_annot_v v in From cfe39ebd00ce8e82690cdeab34b3384735e3b8d0 Mon Sep 17 00:00:00 2001 From: agle Date: Wed, 15 Jul 2026 12:50:18 +1000 Subject: [PATCH 20/22] doc intro --- lib/lang/hm/hm.ml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/lib/lang/hm/hm.ml b/lib/lang/hm/hm.ml index 0f3cb751..c8a9b1ea 100644 --- a/lib/lang/hm/hm.ml +++ b/lib/lang/hm/hm.ml @@ -1,5 +1,16 @@ (** Simple hindley-milner type inference *) +(** Union-find-based implementation of Hindley-Milner type inference for + type-annotating the AST, without let-generalisation at the moment. + + This is based on Algorithm J described in Milner, 1978; + {:https://doi.org/10.1016%2F0022-0000%2878%2990014-4}. + + The following may be more accessible: + + - {:https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Algorithm_J} + - {:https://bernsteinbear.com/blog/type-inference/} *) + module TypeExpr = TypeExpr (** {1 Type Expressions} @@ -174,7 +185,8 @@ let locally_elaborate_expr (e : Expr.BasilExpr.t) = let elaborated_type_alg (e : Types.t Expr.BasilExpr.abstract_expr) = Expr.AbstractExpr.get_typ e -(** Partially apply args list to function type funtype and return resulting type *) +(** Partially apply args list to function type funtype and return resulting type +*) let type_applied (funtype : Types.t) (args : Types.t list) = let module T = Elaboration.TypeInference (TypeExpr.MakeFresh ()) in let rt = T.fresh_tvar ~n:"ret" () in From 03a6e43103f4b7720604bf1f59b9752f6325b192 Mon Sep 17 00:00:00 2001 From: agle Date: Wed, 15 Jul 2026 12:54:04 +1000 Subject: [PATCH 21/22] rename vars --- lib/lang/hm/elaboration.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/lib/lang/hm/elaboration.ml b/lib/lang/hm/elaboration.ml index aa69c1c0..0bfab1e3 100644 --- a/lib/lang/hm/elaboration.ml +++ b/lib/lang/hm/elaboration.ml @@ -152,7 +152,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct let bt = fix bool_type in let b = infer_expr ~univ:global_universe [%here] b scheme in let _ = unify (getty b) bt in - let nb scheme = + let new_axiom scheme = Function { attrib; @@ -162,18 +162,18 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (elaborate_expr ~univ:global_universe [%here] b scheme); } in - (scheme, `Decl (decl_id, nb)) + (scheme, `Decl (decl_id, new_axiom)) | Uninterpreted -> - let nu s = + let new_uf s = Function { binding = binding s; attrib; definition = Uninterpreted } in - (scheme, `Decl (decl_id, nu)) + (scheme, `Decl (decl_id, new_uf)) | Function definition -> let e = infer_expr ~univ:global_universe [%here] definition scheme in - let ne scheme = + let new_fundef scheme = Function { binding = binding scheme; @@ -183,7 +183,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct (elaborate_expr ~univ:global_universe [%here] e scheme); } in - (scheme, `Decl (decl_id, ne))) + (scheme, `Decl (decl_id, new_fundef))) | Variable { binding; attrib; classification } -> let scheme = decl_var_typ global_universe scheme binding in let binding s = retype_var global_universe s binding in @@ -198,7 +198,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct |> Option.map (fun e -> elaborate_expr ~univ:global_universe [%here] e final_scheme) in - let nb fscheme = + let new_vardef fscheme = Variable { binding = binding fscheme; @@ -206,7 +206,7 @@ module TypeInference (T : TypeExpr.TypeContext) = struct classification = classification fscheme; } in - (scheme, `Decl (decl_id, nb)) + (scheme, `Decl (decl_id, new_vardef)) | Procedure { definition } -> let elaborate_proc, scheme = infer_proc prog scheme definition in (scheme, `Procedure (decl_id, elaborate_proc)) From c1197a82f5e24be4bc859e58f058ba0b53fbdcc0 Mon Sep 17 00:00:00 2001 From: agle Date: Wed, 15 Jul 2026 13:18:28 +1000 Subject: [PATCH 22/22] fix occurs check --- lib/lang/hm/unification.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/lang/hm/unification.ml b/lib/lang/hm/unification.ml index 4e718a90..cce1e5c1 100644 --- a/lib/lang/hm/unification.ml +++ b/lib/lang/hm/unification.ml @@ -26,7 +26,7 @@ module Make (T : TypeExpr.TypeContext) = struct let occurs_in a b = let check = function | Var t -> equal_tvar t a - | TypeConstr (ls, _) -> List.for_all Fun.id ls + | TypeConstr (ls, _) -> List.exists Fun.id ls in Rec.cata check b