diff options
author | Son Ho | 2022-04-26 19:34:12 +0200 |
---|---|---|
committer | Son Ho | 2022-04-26 19:34:12 +0200 |
commit | 79b0bf1fdb0283c2bd9cbca91794105dda88f03b (patch) | |
tree | 4a51f6cf3fcb208f074a306b80cb1a89ddbbbd63 /src/PureUtils.ml | |
parent | 732e3305cba3a628d9408a048978151e4ef2fcc2 (diff) |
Introduce the Abs expression and continue updating the code
Diffstat (limited to 'src/PureUtils.ml')
-rw-r--r-- | src/PureUtils.ml | 82 |
1 files changed, 60 insertions, 22 deletions
diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 0045cc1d..bcf93c3c 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -266,7 +266,7 @@ 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 _ -> false + | Value _ | App _ | Func _ | Abs _ -> false | Let (monadic, _, _, next_e) -> if monadic then true else let_group_requires_parentheses next_e | Switch (_, _) -> false @@ -404,30 +404,68 @@ let destruct_apps (e : texpression) : texpression * texpression list = in aux [] e +(** Make an `App (app, arg)` expression *) +let mk_app (app : texpression) (arg : texpression) : texpression = + match app.ty with + | Arrow (ty0, ty1) -> + (* Sanity check *) + assert (ty0 = arg.ty); + let e = App (app, arg) in + let ty = ty1 in + { e; ty } + | _ -> raise (Failure "Expected an arrow type") + (** The reverse of [destruct_app] *) -let mk_apps (e : texpression) (args : texpression list) : texpression = - (* Reverse the arguments *) - let args = List.rev args in - (* Apply *) - let rec aux (e : texpression) (args : texpression list) : texpression = - match args with - | [] -> e - | arg :: args' -> ( - let e' = aux e args' in - match e'.ty with - | Arrow (ty0, ty1) -> - (* Sanity check *) - assert (ty0 == arg.ty); - let e'' = App (e', arg) in - let ty'' = ty1 in - { e = e''; ty = ty'' } - | _ -> raise (Failure "Expected an arrow type")) - in - aux e args +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, - * if possible *) +(** Destruct an expression into a function identifier and a list of arguments, + * if possible *) let opt_destruct_function_call (e : texpression) : (func * texpression list) option = let app, args = destruct_apps e in match app.e with Func func -> Some (func, 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 opt_destruct_result (ty : ty) : ty option = + match ty with + | Adt (Assumed Result, tys) -> Some (Collections.List.to_cons_nil tys) + | _ -> None + +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 + { e; ty } + +let rec destruct_abs_list (e : texpression) : typed_lvalue list * texpression = + match e.e with + | Abs (x, e') -> + let xl, e'' = destruct_abs_list e' in + (x :: xl, e'') + | _ -> ([], e) |