meta_language/translation/
types.rs

1//! Portable-core types.
2//!
3//! Numeric types keep their source semantics apart:
4//! `nat` and `int` are unbounded, `fixed` is a Rust machine integer whose
5//! arithmetic aborts on overflow, and `float` is a JavaScript Number, an
6//! IEEE-754 binary64. Data types are named by their qualified path.
7//!
8//! Mirrors `js/src/translation/types.js`; the serialised form is the same JSON
9//! object (`{ "kind": "fixed", "bits": 32, "signed": true }`).
10
11use serde::{Deserialize, Serialize};
12
13use super::Span;
14
15/// A portable-core type, or a surface type reference before resolution.
16#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
17#[serde(tag = "kind", rename_all = "camelCase")]
18pub enum Type {
19    Nat,
20    Int,
21    Bool,
22    String,
23    Unit,
24    /// A JavaScript Number: an IEEE-754 binary64.
25    Float,
26    Fixed {
27        bits: u32,
28        signed: bool,
29    },
30    /// A resolved data type, named by its qualified path.
31    Data {
32        name: std::string::String,
33    },
34    /// A JavaScript array, which the portable core reads and never mutates.
35    Array {
36        element: Box<Self>,
37    },
38    /// A surface reference to a declared type, resolved by the checker.
39    Named {
40        path: Vec<std::string::String>,
41        #[serde(default, skip_serializing_if = "Option::is_none")]
42        span: Option<Span>,
43    },
44    /// The type of a numeral whose type the context has not fixed yet.
45    Literal,
46    /// A proof hypothesis bound by a case split (proof plans only).
47    Hypothesis,
48    /// The lines a program has printed, newest first: only the targets whose
49    /// programs are pure carry them, as a value (see `output`).
50    Output,
51}
52
53pub const NAT: Type = Type::Nat;
54pub const INT: Type = Type::Int;
55pub const BOOL: Type = Type::Bool;
56pub const STRING: Type = Type::String;
57pub const UNIT: Type = Type::Unit;
58pub const FLOAT: Type = Type::Float;
59
60#[must_use]
61pub const fn fixed(bits: u32, signed: bool) -> Type {
62    Type::Fixed { bits, signed }
63}
64
65#[must_use]
66pub fn array(element: Type) -> Type {
67    Type::Array {
68        element: Box::new(element),
69    }
70}
71
72#[must_use]
73pub fn data(name: impl Into<std::string::String>) -> Type {
74    Type::Data { name: name.into() }
75}
76
77impl Type {
78    /// The type's identity: `nat`, `i32`, `data:Tree`.
79    #[must_use]
80    pub fn key(&self) -> std::string::String {
81        match self {
82            Self::Fixed { bits, signed } => format!("{}{bits}", if *signed { 'i' } else { 'u' }),
83            Self::Data { name } => format!("data:{name}"),
84            Self::Array { element } => format!("array:{}", element.key()),
85            other => other.kind().to_owned(),
86        }
87    }
88
89    /// The `kind` discriminant as the JavaScript runtime spells it.
90    #[must_use]
91    pub const fn kind(&self) -> &'static str {
92        match self {
93            Self::Nat => "nat",
94            Self::Int => "int",
95            Self::Bool => "bool",
96            Self::String => "string",
97            Self::Unit => "unit",
98            Self::Float => "float",
99            Self::Fixed { .. } => "fixed",
100            Self::Data { .. } => "data",
101            Self::Array { .. } => "array",
102            Self::Named { .. } => "named",
103            Self::Literal => "literal",
104            Self::Hypothesis => "hypothesis",
105            Self::Output => "output",
106        }
107    }
108
109    #[must_use]
110    pub fn same(&self, other: &Self) -> bool {
111        self.key() == other.key()
112    }
113
114    #[must_use]
115    pub const fn is_numeric(&self) -> bool {
116        matches!(self, Self::Nat | Self::Int | Self::Fixed { .. })
117    }
118
119    #[must_use]
120    pub const fn is_float(&self) -> bool {
121        matches!(self, Self::Float)
122    }
123
124    /// True for the types `<` orders: the integers and Numbers.
125    #[must_use]
126    pub const fn is_ordered(&self) -> bool {
127        self.is_numeric() || self.is_float()
128    }
129
130    /// True when every value of the type is a non-negative integer.
131    #[must_use]
132    pub const fn is_natural(&self) -> bool {
133        matches!(self, Self::Nat | Self::Fixed { signed: false, .. })
134    }
135
136    #[must_use]
137    pub const fn is_literal(&self) -> bool {
138        matches!(self, Self::Literal)
139    }
140
141    /// The element type of an array.
142    #[must_use]
143    pub fn element(&self) -> Option<&Self> {
144        match self {
145            Self::Array { element } => Some(element),
146            _ => None,
147        }
148    }
149
150    /// The data type's qualified name.
151    #[must_use]
152    pub fn data_name(&self) -> Option<&str> {
153        match self {
154            Self::Data { name } => Some(name),
155            _ => None,
156        }
157    }
158}
159
160/// Inclusive bounds of a machine-integer type.
161#[must_use]
162pub fn fixed_bounds(bits: u32, signed: bool) -> (i128, u128) {
163    if signed {
164        let max = (1u128 << (bits - 1)) - 1;
165        let min = -i128::try_from(max).unwrap_or(i128::MAX) - 1;
166        (min, max)
167    } else if bits >= 128 {
168        (0, u128::MAX)
169    } else {
170        (0, (1u128 << bits) - 1)
171    }
172}
173
174/// `u8` … `i128`, `usize`, `isize` (the pointer-sized types are 64 bits).
175#[must_use]
176pub fn rust_fixed_type(name: &str) -> Option<Type> {
177    let signed = match name.as_bytes().first() {
178        Some(b'u') => false,
179        Some(b'i') => true,
180        _ => return None,
181    };
182    let bits = match &name[1..] {
183        "8" => 8,
184        "16" => 16,
185        "32" => 32,
186        "64" | "size" => 64,
187        "128" => 128,
188        _ => return None,
189    };
190    Some(fixed(bits, signed))
191}
meta_language/translation/types.rs

meta_language/translation/
types.rs
