diff options
Diffstat (limited to 'src/PureUtils.ml')
| -rw-r--r-- | src/PureUtils.ml | 564 |
1 files changed, 332 insertions, 232 deletions
diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 873931be..c01dd5c9 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -43,96 +43,7 @@ let binop_can_fail (binop : E.binop) : bool = | Div | Rem | Add | Sub | Mul -> true | Shl | Shr -> raise Errors.Unimplemented -let mk_place_from_var (v : var) : place = { var = v.id; projection = [] } - -(** Make a "simplified" tuple type from a list of types: - - if there is exactly one type, just return it - - if there is > one type: wrap them in a tuple - *) -let mk_simpl_tuple_ty (tys : ty list) : ty = - match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys) - -let unit_ty : ty = Adt (Tuple, []) - -let unit_rvalue : typed_rvalue = - let value = RvAdt { variant_id = None; field_values = [] } in - let ty = unit_ty in - { value; ty } - -let mk_typed_rvalue_from_var (v : var) : typed_rvalue = - let value = RvPlace (mk_place_from_var v) in - let ty = v.ty in - { value; ty } - -let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = - let value = LvVar (Var (v, mp)) in - let ty = v.ty in - { value; ty } - -(** Make a "simplified" tuple value from a list of values: - - if there is exactly one value, just return it - - if there is > one value: wrap them in a tuple - *) -let mk_simpl_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue = - match vl with - | [ v ] -> v - | _ -> - let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in - let ty = Adt (Tuple, tys) in - let value = LvAdt { variant_id = None; field_values = vl } in - { value; ty } - -(** Similar to [mk_simpl_tuple_lvalue] *) -let mk_simpl_tuple_rvalue (vl : typed_rvalue list) : typed_rvalue = - match vl with - | [ v ] -> v - | _ -> - let tys = List.map (fun (v : typed_rvalue) -> v.ty) vl in - let ty = Adt (Tuple, tys) in - let value = RvAdt { variant_id = None; field_values = vl } in - { value; ty } - -let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id) - (vl : typed_lvalue list) : typed_lvalue = - let value = LvAdt { variant_id = Some variant_id; field_values = vl } in - { value; ty = adt_ty } - -let ty_as_integer (t : ty) : T.integer_type = - match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable") - -(* TODO: move *) -let type_decl_is_enum (def : T.type_decl) : bool = - match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false - -let mk_state_ty : ty = Adt (Assumed State, []) - -let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) - -let mk_result_fail_rvalue (ty : ty) : typed_rvalue = - let ty = Adt (Assumed Result, [ ty ]) in - let value = RvAdt { variant_id = Some result_fail_id; field_values = [] } in - { value; ty } - -let mk_result_return_rvalue (v : typed_rvalue) : typed_rvalue = - let ty = Adt (Assumed Result, [ v.ty ]) in - let value = - RvAdt { variant_id = Some result_return_id; field_values = [ v ] } - in - { value; ty } - -let mk_result_fail_lvalue (ty : ty) : typed_lvalue = - let ty = Adt (Assumed Result, [ ty ]) in - let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in - { value; ty } - -let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue = - let ty = Adt (Assumed Result, [ v.ty ]) in - let value = - LvAdt { variant_id = Some result_return_id; field_values = [ v ] } - in - { value; ty } - -let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty) +(*let mk_arrow_ty (arg_ty : ty) (ret_ty : ty) : ty = Arrow (arg_ty, ret_ty)*) let dest_arrow_ty (ty : ty) : ty * ty = match ty with @@ -150,10 +61,10 @@ let mk_typed_lvalue_from_constant_value (cv : constant_value) : typed_lvalue = let ty = compute_constant_value_ty cv in { value = LvConcrete cv; ty } -let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression = - let e = Value (v, mp) in - let ty = v.ty in - { e; ty } +(*let mk_value_expression (v : typed_rvalue) (mp : mplace option) : texpression = + let e = Value (v, mp) in + let ty = v.ty in + { e; ty }*) let mk_let (monadic : bool) (lv : typed_lvalue) (re : texpression) (next_e : texpression) : texpression = @@ -244,9 +155,12 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool = object inherit [_] iter_expression as super - method! visit_func env func = - if FunIdSet.mem func.func !ids then raise Utils.Found - else super#visit_func env func + method! visit_qualif env qualif = + match qualif.id with + | Func fun_id -> + if FunIdSet.mem fun_id !ids then raise Utils.Found + else super#visit_qualif env qualif + | _ -> super#visit_qualif env qualif end in @@ -266,126 +180,24 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool = *) let rec let_group_requires_parentheses (e : texpression) : bool = match e.e with - | Value _ | App _ | Func _ | Abs _ -> false + | Local _ | Const _ | App _ | Abs _ | Qualif _ -> false | Let (monadic, _, _, next_e) -> if monadic then true else let_group_requires_parentheses next_e | Switch (_, _) -> false | Meta (_, next_e) -> let_group_requires_parentheses next_e -(** Module to perform type checking - we use this for sanity checks only *) -module TypeCheck = struct - type tc_ctx = { type_decls : type_decl TypeDeclId.Map.t } - - let check_constant_value (ty : ty) (v : constant_value) : unit = - match (ty, v) with - | Integer int_ty, V.Scalar sv -> assert (int_ty = sv.V.int_ty) - | Bool, Bool _ | Char, Char _ | Str, String _ -> () - | _ -> raise (Failure "Inconsistent type") - - let check_adt_g_value (ctx : tc_ctx) (check_value : ty -> 'v -> unit) - (variant_id : VariantId.id option) (field_values : 'v list) (ty : ty) : - unit = - (* Retrieve the field types *) - let field_tys = - match ty with - | Adt (Tuple, tys) -> - (* Tuple *) - tys - | Adt (AdtId def_id, tys) -> - (* "Regular" ADT *) - let def = TypeDeclId.Map.find def_id ctx.type_decls in - type_decl_get_instantiated_fields_types def variant_id tys - | Adt (Assumed aty, tys) -> ( - (* Assumed type *) - match aty with - | State -> - (* `State` is opaque *) - raise (Failure "Unreachable: `State` values are opaque") - | Result -> - let ty = Collections.List.to_cons_nil tys in - let variant_id = Option.get variant_id in - if variant_id = result_return_id then [ ty ] - else if variant_id = result_fail_id then [] - else - raise - (Failure "Unreachable: improper variant id for result type") - | Option -> - let ty = Collections.List.to_cons_nil tys in - let variant_id = Option.get variant_id in - if variant_id = option_some_id then [ ty ] - else if variant_id = option_none_id then [] - else - raise - (Failure "Unreachable: improper variant id for result type") - | Vec -> - assert (variant_id = None); - let ty = Collections.List.to_cons_nil tys in - List.map (fun _ -> ty) field_values) - | _ -> raise (Failure "Inconsistently typed value") - in - (* Check that the field values have the expected types *) - List.iter - (fun (ty, v) -> check_value ty v) - (List.combine field_tys field_values) - - let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : unit = - log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v)); - match v.value with - | LvConcrete cv -> check_constant_value v.ty cv - | LvVar _ -> () - | LvAdt av -> - check_adt_g_value ctx - (fun ty (v : typed_lvalue) -> - if ty <> v.ty then ( - log#serror - ("check_typed_lvalue: not the same types:" ^ "\n- ty: " - ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); - raise (Failure "Inconsistent types")); - check_typed_lvalue ctx v) - av.variant_id av.field_values v.ty - - let rec check_typed_rvalue (ctx : tc_ctx) (v : typed_rvalue) : unit = - log#ldebug (lazy ("check_typed_rvalue: " ^ show_typed_rvalue v)); - match v.value with - | RvConcrete cv -> check_constant_value v.ty cv - | RvPlace _ -> - (* TODO: *) - () - | RvAdt av -> - check_adt_g_value ctx - (fun ty (v : typed_rvalue) -> - if ty <> v.ty then ( - log#serror - ("check_typed_rvalue: not the same types:" ^ "\n- ty: " - ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); - raise (Failure "Inconsistent types")); - check_typed_rvalue ctx v) - av.variant_id av.field_values v.ty -end - -let is_value (e : texpression) : bool = - match e.e with Value _ -> true | _ -> false - let is_var (e : texpression) : bool = - match e.e with - | Value (v, _) -> ( - match v.value with - | RvPlace { var = _; projection = [] } -> true - | _ -> false) - | _ -> false + match e.e with Local _ -> true | _ -> false let as_var (e : texpression) : VarId.id = - match e.e with - | Value (v, _) -> ( - match v.value with - | RvPlace { var; projection = [] } -> var - | _ -> raise (Failure "Unreachable")) - | _ -> raise (Failure "Unreachable") + match e.e with Local (v, _) -> v | _ -> raise (Failure "Unreachable") (** Remove the external occurrences of [Meta] *) let rec unmeta (e : texpression) : texpression = match e.e with Meta (_, e) -> unmeta e | _ -> e +let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1) + (** Construct a type as a list of arrows: ty1 -> ... tyn *) let mk_arrows (inputs : ty list) (output : ty) = let rec aux (tys : ty list) : ty = @@ -419,16 +231,16 @@ let mk_app (app : texpression) (arg : texpression) : texpression = let mk_apps (app : texpression) (args : texpression list) : texpression = List.fold_left (fun app arg -> mk_app app arg) app args -(** Destruct an expression into a function identifier and a list of arguments, +(** Destruct an expression into a qualif identifier and a list of arguments, * if possible *) -let opt_destruct_function_call (e : texpression) : - (func * texpression list) option = +let opt_destruct_qualif_app (e : texpression) : + (qualif * texpression list) option = let app, args = destruct_apps e in - match app.e with Func func -> Some (func, args) | _ -> None + match app.e with Qualif qualif -> Some (qualif, args) | _ -> None (** Destruct an expression into a function identifier and a list of arguments *) -let destruct_function_call (e : texpression) : func * texpression list = - Option.get (opt_destruct_function_call e) +let destruct_qualif_app (e : texpression) : qualif * texpression list = + Option.get (opt_destruct_qualif_app e) let opt_destruct_result (ty : ty) : ty option = match ty with @@ -440,26 +252,6 @@ let destruct_result (ty : ty) : ty = Option.get (opt_destruct_result ty) let opt_destruct_tuple (ty : ty) : ty list option = match ty with Adt (Tuple, tys) -> Some tys | _ -> None -let opt_destruct_state_monad_result (ty : ty) : ty option = - (* Checking: - * ty == state -> result (state & _) ? *) - match ty with - | Arrow (ty0, ty1) -> - (* ty == ty0 -> ty1 - * Checking: ty0 == state ? - * *) - if ty0 = mk_state_ty then - (* Checking: ty1 == result (state & _) *) - match opt_destruct_result ty1 with - | None -> None - | Some ty2 -> ( - (* Checking: ty2 == state & _ *) - match opt_destruct_tuple ty2 with - | Some [ ty3; ty4 ] -> if ty3 = mk_state_ty then Some ty4 else None - | _ -> None) - else None - | _ -> None - let mk_abs (x : typed_lvalue) (e : texpression) : texpression = let ty = Arrow (x.ty, e.ty) in let e = Abs (x, e) in @@ -475,9 +267,14 @@ let rec destruct_abs_list (e : texpression) : typed_lvalue list * texpression = let destruct_arrow (ty : ty) : ty * ty = match ty with | Arrow (ty0, ty1) -> (ty0, ty1) - | _ -> raise (Failure "Unreachable") + | _ -> raise (Failure "Not an arrow type") -let mk_arrow (ty0 : ty) (ty1 : ty) : ty = Arrow (ty0, ty1) +let rec destruct_arrows (ty : ty) : ty list * ty = + match ty with + | Arrow (ty0, ty1) -> + let tys, out_ty = destruct_arrows ty1 in + (ty0 :: tys, out_ty) + | _ -> ([], ty) let get_switch_body_ty (sb : switch_body) : ty = match sb with @@ -512,3 +309,306 @@ let mk_switch (scrut : texpression) (sb : switch_body) : texpression = (* Put together *) let e = Switch (scrut, sb) in { e; ty } + +(** Make a "simplified" tuple type from a list of types: + - if there is exactly one type, just return it + - if there is > one type: wrap them in a tuple + *) +let mk_simpl_tuple_ty (tys : ty list) : ty = + match tys with [ ty ] -> ty | _ -> Adt (Tuple, tys) + +(** TODO: rename to "mk_..." *) +let unit_ty : ty = Adt (Tuple, []) + +(** TODO: rename to "mk_..." *) +let unit_rvalue : texpression = + let id = AdtCons { adt_id = Tuple; variant_id = None } in + let qualif = { id; type_params = [] } in + let e = Qualif qualif in + let ty = unit_ty in + { e; ty } + +let mk_texpression_from_var (v : var) (mp : mplace option) : texpression = + let e = Local (v.id, mp) in + let ty = v.ty in + { e; ty } + +let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = + let value = LvVar (Var (v, mp)) in + let ty = v.ty in + { value; ty } + +(** Make a "simplified" tuple value from a list of values: + - if there is exactly one value, just return it + - if there is > one value: wrap them in a tuple + *) +let mk_simpl_tuple_lvalue (vl : typed_lvalue list) : typed_lvalue = + match vl with + | [ v ] -> v + | _ -> + let tys = List.map (fun (v : typed_lvalue) -> v.ty) vl in + let ty = Adt (Tuple, tys) in + let value = LvAdt { variant_id = None; field_values = vl } in + { value; ty } + +(** Similar to [mk_simpl_tuple_lvalue] *) +let mk_simpl_tuple_texpression (vl : texpression list) : texpression = + match vl with + | [ v ] -> v + | _ -> + (* Compute the types of the fields, and the type of the tuple constructor *) + let tys = List.map (fun (v : texpression) -> v.ty) vl in + let ty = Adt (Tuple, tys) in + let ty = mk_arrows tys ty in + (* Construct the tuple constructor qualifier *) + let id = AdtCons { adt_id = Tuple; variant_id = None } in + let qualif = { id; type_params = tys } in + (* Put everything together *) + let cons = { e = Qualif qualif; ty } in + mk_apps cons vl + +let mk_adt_lvalue (adt_ty : ty) (variant_id : VariantId.id) + (vl : typed_lvalue list) : typed_lvalue = + let value = LvAdt { variant_id = Some variant_id; field_values = vl } in + { value; ty = adt_ty } + +let ty_as_integer (t : ty) : T.integer_type = + match t with Integer int_ty -> int_ty | _ -> raise (Failure "Unreachable") + +(* TODO: move *) +let type_decl_is_enum (def : T.type_decl) : bool = + match def.kind with T.Struct _ -> false | Enum _ -> true | Opaque -> false + +let mk_state_ty : ty = Adt (Assumed State, []) + +let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) + +let mk_result_fail_rvalue (ty : ty) : texpression = + let type_args = [ ty ] in + let ty = Adt (Assumed Result, type_args) in + let id = + AdtCons { adt_id = Assumed Result; variant_id = Some result_fail_id } + in + let qualif = { id; type_params = type_args } in + let cons_e = Qualif qualif in + let cons_ty = ty in + let cons = { e = cons_e; ty = cons_ty } in + cons + +let mk_result_return_rvalue (v : texpression) : texpression = + let type_args = [ v.ty ] in + let ty = Adt (Assumed Result, type_args) in + let id = + AdtCons { adt_id = Assumed Result; variant_id = Some result_return_id } + in + let qualif = { id; type_params = type_args } in + let cons_e = Qualif qualif in + let cons_ty = mk_arrow v.ty ty in + let cons = { e = cons_e; ty = cons_ty } in + mk_app cons v + +let mk_result_fail_lvalue (ty : ty) : typed_lvalue = + let ty = Adt (Assumed Result, [ ty ]) in + let value = LvAdt { variant_id = Some result_fail_id; field_values = [] } in + { value; ty } + +let mk_result_return_lvalue (v : typed_lvalue) : typed_lvalue = + let ty = Adt (Assumed Result, [ v.ty ]) in + let value = + LvAdt { variant_id = Some result_return_id; field_values = [ v ] } + in + { value; ty } + +let opt_destruct_state_monad_result (ty : ty) : ty option = + (* Checking: + * ty == state -> result (state & _) ? *) + match ty with + | Arrow (ty0, ty1) -> + (* ty == ty0 -> ty1 + * Checking: ty0 == state ? + * *) + if ty0 = mk_state_ty then + (* Checking: ty1 == result (state & _) *) + match opt_destruct_result ty1 with + | None -> None + | Some ty2 -> ( + (* Checking: ty2 == state & _ *) + match opt_destruct_tuple ty2 with + | Some [ ty3; ty4 ] -> if ty3 = mk_state_ty then Some ty4 else None + | _ -> None) + else None + | _ -> None + +(** Utility function, used for type checking - TODO: move *) +let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t) + (type_id : type_id) (variant_id : VariantId.id option) (tys : ty list) : + ty list = + match type_id with + | Tuple -> + (* Tuple *) + assert (variant_id = None); + tys + | AdtId def_id -> + (* "Regular" ADT *) + let def = TypeDeclId.Map.find def_id type_decls in + type_decl_get_instantiated_fields_types def variant_id tys + | Assumed aty -> ( + (* Assumed type *) + match aty with + | State -> + (* `State` is opaque *) + raise (Failure "Unreachable: `State` values are opaque") + | Result -> + let ty = Collections.List.to_cons_nil tys in + let variant_id = Option.get variant_id in + if variant_id = result_return_id then [ ty ] + else if variant_id = result_fail_id then [] + else + raise (Failure "Unreachable: improper variant id for result type") + | Option -> + let ty = Collections.List.to_cons_nil tys in + let variant_id = Option.get variant_id in + if variant_id = option_some_id then [ ty ] + else if variant_id = option_none_id then [] + else + raise (Failure "Unreachable: improper variant id for result type") + | Vec -> raise (Failure "Unreachable: `Vector` values are opaque")) + +(** Module to perform type checking - we use this for sanity checks only + + TODO: move to a special file (so that we can also use PrintPure for + debugging) + *) +module TypeCheck = struct + type tc_ctx = { + type_decls : type_decl TypeDeclId.Map.t; (** The type declarations *) + env : ty VarId.Map.t; (** Environment from variables to types *) + } + + let check_constant_value (v : constant_value) (ty : ty) : unit = + match (ty, v) with + | Integer int_ty, V.Scalar sv -> assert (int_ty = sv.V.int_ty) + | Bool, Bool _ | Char, Char _ | Str, String _ -> () + | _ -> raise (Failure "Inconsistent type") + + let rec check_typed_lvalue (ctx : tc_ctx) (v : typed_lvalue) : tc_ctx = + log#ldebug (lazy ("check_typed_lvalue: " ^ show_typed_lvalue v)); + match v.value with + | LvConcrete cv -> + check_constant_value cv v.ty; + ctx + | LvVar Dummy -> ctx + | LvVar (Var (var, _)) -> + assert (var.ty = v.ty); + let env = VarId.Map.add var.id var.ty ctx.env in + { ctx with env } + | LvAdt av -> + (* Compute the field types *) + let type_id, tys = + match v.ty with + | Adt (type_id, tys) -> (type_id, tys) + | _ -> raise (Failure "Inconsistently typed value") + in + let field_tys = + get_adt_field_types ctx.type_decls type_id av.variant_id tys + in + let check_value (ctx : tc_ctx) (ty : ty) (v : typed_lvalue) : tc_ctx = + if ty <> v.ty then ( + log#serror + ("check_typed_lvalue: not the same types:" ^ "\n- ty: " + ^ show_ty ty ^ "\n- v.ty: " ^ show_ty v.ty); + raise (Failure "Inconsistent types")); + check_typed_lvalue ctx v + in + (* Check the field types - TODO: we might also want to check that the + * type of the applied constructor is correct *) + List.fold_left + (fun ctx (ty, v) -> check_value ctx ty v) + ctx + (List.combine field_tys av.field_values) + + let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = + match e.e with + | Local (var_id, _) -> ( + (* Lookup the variable - note that the variable may not be there, + * if we type-check a subexpression (i.e.: if the variable is introduced + * "outside" of the expression) - TODO: this won't happen once + * we use a locally nameless representation *) + match VarId.Map.find_opt var_id ctx.env with + | None -> () + | Some ty -> assert (ty = e.ty)) + | Const cv -> check_constant_value cv e.ty + | App (app, arg) -> + let input_ty, output_ty = destruct_arrow app.ty in + assert (input_ty = arg.ty); + assert (output_ty = e.ty); + check_texpression ctx app; + check_texpression ctx arg + | Abs (pat, body) -> + let pat_ty, body_ty = destruct_arrow e.ty in + assert (pat.ty = pat_ty); + assert (body.ty = body_ty); + (* Check the pattern and register the introduced variables at the same time *) + let ctx = check_typed_lvalue ctx pat in + check_texpression ctx body + | Qualif qualif -> ( + match qualif.id with + | Func _ -> () (* TODO *) + | Proj (ProjField (type_id, field_id)) -> + (* Note we can only project fields of structurs (not enumerations) *) + let variant_id = None in + let expected_field_tys = + get_adt_field_types ctx.type_decls type_id variant_id + qualif.type_params + in + let expected_field_ty = FieldId.nth expected_field_tys field_id in + let _adt_ty, field_ty = destruct_arrow e.ty in + (* TODO: check the adt_ty *) + assert (expected_field_ty = field_ty) + | Proj (ProjTuple field_id) -> ( + let tuple_ty, field_ty = destruct_arrow e.ty in + match tuple_ty with + | Adt (Tuple, tys) -> + let expected_field_ty = List.nth tys field_id in + assert (field_ty = expected_field_ty) + | _ -> raise (Failure "Inconsistently typed projector")) + | AdtCons id -> + (* TODO: we might also want to check the out type *) + let expected_field_tys = + get_adt_field_types ctx.type_decls id.adt_id id.variant_id + qualif.type_params + in + let field_tys, _ = destruct_arrows e.ty in + assert (expected_field_tys = field_tys)) + | Let (monadic, pat, re, e_next) -> + let expected_pat_ty = + if monadic then destruct_result re.ty else re.ty + in + assert (pat.ty = expected_pat_ty); + assert (e.ty = e_next.ty); + (* Check the right-expression *) + check_texpression ctx re; + (* Check the pattern and register the introduced variables at the same time *) + let ctx = check_typed_lvalue ctx pat in + (* Check the next expression *) + check_texpression ctx e_next + | Switch (scrut, switch_body) -> ( + check_texpression ctx scrut; + match switch_body with + | If (e_then, e_else) -> + assert (scrut.ty = Bool); + assert (e_then.ty = e.ty); + assert (e_else.ty = e.ty); + check_texpression ctx e_then; + check_texpression ctx e_else + | Match branches -> + let check_branch (br : match_branch) : unit = + assert (br.pat.ty = scrut.ty); + let ctx = check_typed_lvalue ctx br.pat in + check_texpression ctx br.branch + in + List.iter check_branch branches) + | Meta (_, e_next) -> + assert (e_next.ty = e.ty); + check_texpression ctx e_next +end |