Skip to main content

logicaffeine_compile/analysis/
defined_real.rs

1//! Which functions may define a real number: `the real number whose digits in base 3 are f`, `the
2//! real number approximated by f`.
3//!
4//! A defined real reads its function only as a refinement needs it, and every tier reads it in a
5//! context of its own, at whatever moment a comparison, a floor or a printed digit asks. That is
6//! sound only for a function whose answer depends on its argument alone and whose call does nothing
7//! but answer. The phrase is the builtin `definedReal(kind, base, name, (n: Int) -> name(n))`, and
8//! every tier reads its four arguments as the phrase writes them, so a program is refused, before it
9//! runs, when it calls `definedReal` in any other form, and when a function it defines a real by:
10//!
11//! - is not one the program defines;
12//! - does not take exactly one `Int`;
13//! - declares an answer other than an `Int` (digits) or an `Int` or a `Rational` (approximations);
14//! - does more than answer — shows, reads or writes a file, sends, launches, chooses — or calls a
15//!   function that does ([`crate::optimize::effects`]);
16//! - or reads a variable of the program, itself or through a function it calls.
17
18use std::collections::HashSet;
19
20use crate::ast::stmt::{ClosureBody, Expr, Literal, Stmt, TypeExpr};
21use crate::intern::{Interner, Symbol};
22use crate::optimize::mentions::Mentions;
23use crate::optimize::writes::WriteSet;
24
25/// The first function the program defines a real number by that cannot define one, refused in
26/// words naming it; `Ok` when there is none.
27pub fn check(stmts: &[Stmt], interner: &Interner) -> Result<(), String> {
28    let Some(defined_real) = interner.lookup("definedReal") else {
29        return Ok(());
30    };
31    let walk = super::known_calls::harvest_calls(stmts);
32    let sites: Vec<_> = walk.calls.iter().filter(|c| c.function == defined_real).collect();
33    if sites.is_empty() {
34        return Ok(());
35    }
36    let functions: Vec<&Stmt> = stmts.iter().filter(|s| matches!(s, Stmt::FunctionDef { .. })).collect();
37    if functions
38        .iter()
39        .any(|s| matches!(s, Stmt::FunctionDef { name, .. } if *name == defined_real))
40    {
41        return Ok(());
42    }
43    let main: Vec<Stmt> = stmts
44        .iter()
45        .filter(|s| !matches!(s, Stmt::FunctionDef { .. }))
46        .cloned()
47        .collect();
48    let program_variables: HashSet<Symbol> = WriteSet::of_block(&main).declared().clone();
49    let effects = crate::optimize::effects::EffectEnv::from_stmts(stmts, interner);
50    for site in sites {
51        let Some(Phrase { kind, base, function }) = phrase(site.args, interner) else {
52            return Err("definedReal is written `the real number whose digits in base 10 are f` or `the real \
53                        number approximated by f`"
54                .to_string());
55        };
56        logicaffeine_base::exact_real::Definition::named(kind, base)?;
57        let name = interner.resolve(function);
58        let Some(Stmt::FunctionDef { params, return_type, .. }) = functions
59            .iter()
60            .find(|s| matches!(s, Stmt::FunctionDef { name, .. } if *name == function))
61            .copied()
62        else {
63            return Err(format!("{name} is no function this program defines"));
64        };
65        let takes_an_int = matches!(params.as_slice(), [(_, t)] if names(t, interner) == Some("Int"));
66        if !takes_an_int {
67            return Err(format!(
68                "{name} takes one Int to define a real number — the digit's place or the precision — and \
69                 it takes {}",
70                taken(params, interner)
71            ));
72        }
73        let digits = kind == "digits";
74        if let Some(answer) = return_type.and_then(|t| names(t, interner)) {
75            let answers = if digits { answer == "Int" } else { matches!(answer, "Int" | "Rational") };
76            if !answers {
77                return Err(format!(
78                    "{name} answers {answer}, and a real number is defined by {}",
79                    if digits { "whole digits" } else { "whole or rational answers" }
80                ));
81            }
82        }
83        if !effects.function_is_replayable(name) {
84            return Err(format!(
85                "{name} does more than answer, and a real number's function only computes its answer"
86            ));
87        }
88        if let Some((reader, variable)) = reads_a_variable(function, &functions, &program_variables) {
89            let variable = interner.resolve(variable);
90            let reader = interner.resolve(reader);
91            return Err(if reader == name {
92                format!("{name} reads `{variable}`, and a real number's function reads only its argument")
93            } else {
94                format!(
95                    "{name} reads `{variable}` through {reader}, and a real number's function reads only its \
96                     argument"
97                )
98            });
99        }
100    }
101    Ok(())
102}
103
104/// What a `definedReal` call says, read only from the form the phrase writes.
105struct Phrase<'i> {
106    kind: &'i str,
107    base: i64,
108    function: Symbol,
109}
110
111/// The phrase a `definedReal` call writes — its kind, its base, its function's name and the closure
112/// `(n: Int) -> name(n)` — or `None` for a call of any other form.
113fn phrase<'i>(args: &[&Expr], interner: &'i Interner) -> Option<Phrase<'i>> {
114    let [Expr::Literal(Literal::Text(kind)), Expr::Literal(Literal::Number(base)), Expr::Literal(Literal::Text(name)), Expr::Closure {
115        params,
116        body: ClosureBody::Expression(Expr::Call { function, args: read }),
117        return_type: None,
118    }] = args
119    else {
120        return None;
121    };
122    let [(index, index_type)] = params.as_slice() else {
123        return None;
124    };
125    let reads_its_index = matches!(read.as_slice(), [Expr::Identifier(i)] if i == index);
126    let kind = interner.resolve(*kind);
127    let named = interner.resolve(*name) == interner.resolve(*function);
128    (reads_its_index
129        && named
130        && names(index_type, interner) == Some("Int")
131        && matches!(kind, "digits" | "approximations"))
132    .then_some(Phrase {
133        kind,
134        base: *base,
135        function: *function,
136    })
137}
138
139/// A type written as a single name, like `Int` or `Rational`.
140fn names<'i>(t: &TypeExpr, interner: &'i Interner) -> Option<&'i str> {
141    match t {
142        TypeExpr::Primitive(s) | TypeExpr::Named(s) => Some(interner.resolve(*s)),
143        _ => None,
144    }
145}
146
147/// What a function takes, as the refusal says it.
148fn taken(params: &[(Symbol, &TypeExpr)], interner: &Interner) -> String {
149    match params {
150        [] => "nothing".to_string(),
151        [(_, t)] => format!("one {}", names(t, interner).unwrap_or("value of another type")),
152        more => format!("{} parameters", more.len()),
153    }
154}
155
156/// The first function reachable from `function` by calls that reads one of the program's own
157/// variables, with the variable.
158fn reads_a_variable(
159    function: Symbol,
160    functions: &[&Stmt],
161    program_variables: &HashSet<Symbol>,
162) -> Option<(Symbol, Symbol)> {
163    let mut seen: HashSet<Symbol> = HashSet::new();
164    let mut pending = vec![function];
165    while let Some(f) = pending.pop() {
166        if !seen.insert(f) {
167            continue;
168        }
169        let Some(Stmt::FunctionDef { params, body, .. }) =
170            functions.iter().find(|s| matches!(s, Stmt::FunctionDef { name, .. } if *name == f)).copied()
171        else {
172            continue;
173        };
174        let mut own: HashSet<Symbol> = params.iter().map(|(p, _)| *p).collect();
175        own.extend(WriteSet::of_block(body).declared().iter().copied());
176        let touched = Mentions::of_block(body);
177        if let Some(v) = touched
178            .symbols()
179            .find(|s| program_variables.contains(s) && !own.contains(s))
180        {
181            return Some((f, v));
182        }
183        for site in super::known_calls::harvest_calls(body).calls {
184            pending.push(site.function);
185        }
186    }
187    None
188}