diff options
Diffstat (limited to '')
| -rw-r--r-- | src/ExtractToFStar.ml | 15 | ||||
| -rw-r--r-- | src/PrintPure.ml | 11 | ||||
| -rw-r--r-- | src/Pure.ml | 12 | ||||
| -rw-r--r-- | src/PureToExtract.ml | 3 | ||||
| -rw-r--r-- | src/PureUtils.ml | 3 |
5 files changed, 35 insertions, 9 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 02005f2b..3840ea1e 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -302,6 +302,7 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : | Assumed Result -> "r" | Assumed Option -> "opt" | Assumed Vec -> "v" + | Assumed State -> "st" | AdtId adt_id -> let def = TypeDefId.Map.find adt_id ctx.type_context.type_defs @@ -317,15 +318,13 @@ let mk_formatter (ctx : trans_ctx) (variant_concatenate_type_name : bool) : let cl = List.filter (fun s -> String.length s > 0) cl in assert (List.length cl > 0); let cl = List.map (fun s -> s.[0]) cl in - StringUtils.string_of_chars cl - (* let c = (get_type_name def.name).[0] in - let c = StringUtils.lowercase_ascii c in - String.make 1 c *)) + StringUtils.string_of_chars cl) | TypeVar _ -> "x" (* lacking imagination here... *) | Bool -> "b" | Char -> "c" | Integer _ -> "i" | Str -> "s" + | Arrow _ -> "f" | Array _ | Slice _ -> raise Unimplemented) in let type_var_basename (_varset : StringSet.t) (basename : string) : string = @@ -406,6 +405,14 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) | Char -> F.pp_print_string fmt ctx.fmt.char_name | Integer int_ty -> F.pp_print_string fmt (ctx.fmt.int_name int_ty) | Str -> F.pp_print_string fmt ctx.fmt.str_name + | Arrow (arg_ty, ret_ty) -> + if inside then F.pp_print_string fmt "("; + extract_ty ctx fmt false arg_ty; + F.pp_print_space fmt (); + F.pp_print_string fmt "->"; + F.pp_print_space fmt (); + extract_ty ctx fmt false ret_ty; + if inside then F.pp_print_string fmt ")" | Array _ | Slice _ -> raise Unimplemented (** Compute the names for all the top-level identifiers used in a type diff --git a/src/PrintPure.ml b/src/PrintPure.ml index f66aadfb..0b5d0a93 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -130,7 +130,11 @@ let type_id_to_string (fmt : type_formatter) (id : type_id) : string = | AdtId id -> fmt.type_def_id_to_string id | Tuple -> "" | Assumed aty -> ( - match aty with Result -> "Result" | Option -> "Option" | Vec -> "Vec") + match aty with + | State -> "State" + | Result -> "Result" + | Option -> "Option" + | Vec -> "Vec") let rec ty_to_string (fmt : type_formatter) (ty : ty) : string = match ty with @@ -148,6 +152,8 @@ let rec ty_to_string (fmt : type_formatter) (ty : ty) : string = | Str -> "str" | Array aty -> "[" ^ ty_to_string fmt aty ^ "; ?]" | Slice sty -> "[" ^ ty_to_string fmt sty ^ "]" + | Arrow (arg_ty, ret_ty) -> + ty_to_string fmt arg_ty ^ " -> " ^ ty_to_string fmt ret_ty let field_to_string fmt (f : field) : string = match f.field_name with @@ -257,6 +263,9 @@ let adt_g_value_to_string (fmt : value_formatter) | Adt (Assumed aty, _) -> ( (* Assumed type *) match aty with + | State -> + (* The `State` type is opaque: we can't get there *) + raise (Failure "Unreachable") | Result -> let variant_id = Option.get variant_id in if variant_id = result_return_id then diff --git a/src/Pure.ml b/src/Pure.ml index d706a366..387d229f 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -24,10 +24,15 @@ type integer_type = T.integer_type [@@deriving show, ord] In comparison with CFIM: - we removed `Box` (because it is translated as the identity: `Box T == T`) - - we added `Result`, which is the type used in the error monad. This allows - us to have a unified treatment of expressions. + - we added: + - `Result`: the type used in the error monad. This allows us to have a + unified treatment of expressions (especially when we have to unfold the + monadic binds) + - `State`: the type of the state, when using state-error monads. Note that + this state is opaque to Aeneas (the user can define it, or leave it as + assumed) *) -type assumed_ty = Result | Vec | Option [@@deriving show, ord] +type assumed_ty = State | Result | Vec | Option [@@deriving show, ord] let result_return_id = VariantId.of_int 0 @@ -81,6 +86,7 @@ type ty = | Str | Array of ty (* TODO: this should be an assumed type?... *) | Slice of ty (* TODO: this should be an assumed type?... *) + | Arrow of ty * ty [@@deriving show, visitors diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml index 42a4c589..21212cd0 100644 --- a/src/PureToExtract.ml +++ b/src/PureToExtract.ml @@ -369,6 +369,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let variant_name = match id with | Tuple -> failwith "Unreachable" + | Assumed State -> failwith "Unreachable" | Assumed Result -> if variant_id = result_return_id then "@result::Return" else if variant_id = result_fail_id then "@result::Fail" @@ -391,7 +392,7 @@ let id_to_string (id : id) (ctx : extraction_ctx) : string = let field_name = match id with | Tuple -> failwith "Unreachable" - | Assumed (Result | Option) -> failwith "Unreachable" + | Assumed (State | Result | Option) -> failwith "Unreachable" | Assumed Vec -> (* We can't directly have access to the fields of a vector *) failwith "Unreachable" diff --git a/src/PureUtils.ml b/src/PureUtils.ml index f51f9415..e637b6ba 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -286,6 +286,9 @@ module TypeCheck = struct | 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 |