Skip to content

GitLab

Commit 67aa9dcd authored by Lennard Gäher's avatar Lennard Gäher
Browse files

upd frontend

parent 05e3c269
Hide whitespace changes
Inline Side-by-side
rr_frontend/Cargo.lock
View file @ 67aa9dcd
......@@ -203,11 +203,10 @@ dependencies = [
"env_logger",
"lazy_static",
"log",
"proc-macro2",
"regex",
"rustc-hash",
"serde 1.0.130",
"syn",
"unicode-xid 0.0.4",
]
[[package]]
......@@ -354,7 +353,7 @@ version = "1.0.29"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "b9f5105d4fdaab20335ca9565e106a5d9b82b6219b5ba735731124ac6711d23d"
dependencies = [
"unicode-xid",
"unicode-xid 0.2.2",
]
[[package]]
......@@ -513,7 +512,7 @@ checksum = "d010a1623fbd906d51d650a9916aaefc05ffa0e4053ff7fe601167f3e715d194"
dependencies = [
"proc-macro2",
"quote",
"unicode-xid",
"unicode-xid 0.2.2",
]
[[package]]
......@@ -564,6 +563,12 @@ version = "0.1.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "3ed742d4ea2bd1176e236172c8429aaf54486e7ac098db29ffe6529e0ce50973"
[[package]]
name = "unicode-xid"
version = "0.0.4"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "8c1f860d7d29cf02cb2f3f359fd35991af3d30bac52c57d265a3c461074cb4dc"
[[package]]
name = "unicode-xid"
version = "0.2.2"
......
rr_frontend/RefinedRust.toml 0 → 100644
View file @ 67aa9dcd
dump_borrowck_info=true
output_dir="./output"
rr_frontend/SPEC_FORMAT.md 0 → 100644
View file @ 67aa9dcd
| Keyword | Purpose | Properties | Example |
--------------------------------------------------------------------------------------------
| `params` | specify Coq-level parameters | multiple | `#[rr:params("n" : "Z", b : "bool")]` |
| `param` | specify Coq-level parameters | multiple | `#[rr:param("n" : "Z")]` |
| `args` | specify argument types | single | `#[rr::args("n" @ "int i32", "b" @ "boolean"]` |
| `returns` | specify return type | single | `#[rr::returns("42" @ "int i32")]` |
| `requires` | specify a precondition | multiple | `#[rr:requires("⌜i > 42⌝")]` |
| `ensures` | specify a postcondition | multiple | `#[rr::ensures("⌜x > y⌝")]` |
| `exists` | specify an existential for the postco | multiple | `#[rr::exists("x" : "Z")]` |
rr_frontend/translation/Cargo.toml
View file @ 67aa9dcd
......@@ -14,8 +14,9 @@ serde = "1.0.130"
csv = "1.1"
config = "0.11"
lazy_static = "1.4.0"
syn = { version = "1.0.80", features = ["full", "parsing"] }
proc-macro2 = "1.0"
#syn = { version = "1.0.80", features = ["full", "parsing"] }
#proc-macro2 = "1.0"
unicode-xid = "0.0.4"
analysis = { path = "../analysis" }
......
rr_frontend/translation/src/caesium/mod.rs
View file @ 67aa9dcd
......@@ -38,7 +38,7 @@ impl CaesiumLiteral {
format!("i2v ({}) {}", i.as_str(), it.caesium_fmt().as_str())
};
let format_bool = |i: String| {
format!("i2v (Z_of_bool {}) {}", i.as_str(), (CaesiumIntType::CaesiumU8).caesium_fmt().as_str())
format!("i2v (Z_of_bool {}) {}", i.as_str(), (BOOL_REPR).caesium_fmt().as_str())
};
match self {
Self::LitI8(i) => format_int(i.to_string(), CaesiumIntType::CaesiumI8),
......@@ -62,12 +62,12 @@ impl CaesiumLiteral {
* Caesium expressions
*/
pub enum CaesiumExpr {
Var(String),
Var(String),
/// a Coq-level parameter with a given Coq name
MetaParam(String),
Literal(CaesiumLiteral),
UnOp{
o : CaesiumUnop,
o : CaesiumUnop,
ot : CaesiumOpType,
e : Box<CaesiumExpr>,
},
......@@ -114,6 +114,12 @@ pub enum CaesiumExpr {
ly: CaesiumStructLayout,
name: String,
},
Annot {
a: CaesiumAnnotation,
e: Box<CaesiumExpr>
},
DropE(Box<CaesiumExpr>),
BoxE(CaesiumLayout),
}
impl CaesiumExpr {
......@@ -155,7 +161,6 @@ impl CaesiumExpr {
Self::Borrow{lft, bk, e} => {
let formatted_bk = bk.caesium_fmt();
let formatted_e = e.caesium_fmt();
// TODO: needs lifetime info
format!("&ref{{ {}, \"{}\" }} ({})", formatted_bk, lft, formatted_e)
},
Self::AddressOf{mt, e} => {
......@@ -175,7 +180,18 @@ impl CaesiumExpr {
let formatted_ly = ly.caesium_fmt();
format!("{} at{{ {} }} \"{}\"", formatted_e, formatted_ly, name)
},
Self::Annot{a, e} => {
let formatted_e = e.caesium_fmt();
format!("AnnotExpr {} ({}) ({})", a.needs_laters(), a, formatted_e)
},
Self::BoxE(ly) => {
let formatted_ly = ly.caesium_fmt();
format!("box{{{}}}", formatted_ly)
},
Self::DropE(e) => {
let formatted_e = e.caesium_fmt();
format!("drop ({})", formatted_e)
}
// TODO
_ => format!(""),
}
......@@ -213,8 +229,14 @@ impl CaesiumBorKind {
}
pub enum CaesiumAnnotation {
/// Start a lifetime as a sublifetime of the intersection of a few other lifetimes
StartLft(CaesiumLft, Vec<CaesiumLft>),
/// End this lifetime
EndLft(CaesiumLft),
/// Extend this lifetime by making the directly owned part static
ExtendLft(CaesiumLft),
/// Shorten the lifetime of an object to the intersection of the given lifetimes
ShortenLft(Vec<CaesiumLft>),
}
impl fmt::Display for CaesiumAnnotation {
fn fmt(&self, f : &mut fmt::Formatter<'_>) -> fmt::Result {
......@@ -234,11 +256,36 @@ impl fmt::Display for CaesiumAnnotation {
},
Self::EndLft(l) => {
write!(f, "EndLftAnnot \"{}\"", l)
},
Self::ExtendLft(l) => {
write!(f, "ExtendLftAnnot \"{}\"", l)
},
Self::ShortenLft(sup) => {
write!(f, "ShortenLftAnnot [")?;
let mut need_sep = false;
for s in sup.iter() {
if need_sep {
write!(f, ", ")?;
}
write!(f, "\"{}\"", s)?;
need_sep = true;
}
write!(f, "]")
}
}
}
}
impl CaesiumAnnotation {
pub(crate) fn needs_laters(&self) -> u32 {
match self {
Self::ShortenLft{..} => 0,
_ => 0,
}
}
}
type CaesiumBlockLabel = String;
pub enum CaesiumStmt {
......@@ -290,23 +337,23 @@ impl CaesiumStmt {
format!("{}Return ({})", ind, formatted_e)
},
CaesiumStmt::Assign{ot, e1, e2, s} => {
let formatted_s = s.caesium_fmt(indent);
let formatted_s = s.caesium_fmt(indent);
let formatted_e1 = e1.caesium_fmt();
let formatted_e2 = e2.caesium_fmt();
let formatted_ot = ot.caesium_fmt();
format!("{}{} <-{{ {} }} {};\n{}",
ind,
formatted_e1.as_str(),
format!("{}{} <-{{ {} }} {};\n{}",
ind,
formatted_e1.as_str(),
formatted_ot.as_str(),
formatted_e2.as_str(),
formatted_e2.as_str(),
formatted_s.as_str())
},
CaesiumStmt::ExprS{e, s} => {
let formatted_e = e.caesium_fmt();
let formatted_s = s.caesium_fmt(indent);
format!("{}{};\n{}",
ind,
ind,
formatted_e.as_str(),
formatted_s.as_str())
},
......@@ -333,7 +380,7 @@ pub enum CaesiumUnop {
}
impl CaesiumUnop {
fn caesium_fmt(&self, ot: &CaesiumOpType) -> String {
match self {
match self {
Self::NegOp => format!("−{{ {} }}", ot.caesium_fmt()),
// TODO: don't actually use that on the Caesium side currently
Self::NotOp => format!("!!{{ {} }}", ot.caesium_fmt()),
......@@ -344,29 +391,29 @@ impl CaesiumUnop {
pub enum CaesiumBinop {
//arithmetic
AddOp,
SubOp,
MulOp,
DivOp,
ModOp,
AddOp,
SubOp,
MulOp,
DivOp,
ModOp,
// logical
AndOp,
OrOp,
//bitwise
BitAndOp,
BitOrOp,
BitXorOp,
BitAndOp,
BitOrOp,
BitXorOp,
ShlOp,
ShrOp,
ShrOp,
// comparison
EqOp,
NeOp,
LtOp,
GtOp,
LeOp,
GeOp,
NeOp,
LtOp,
GtOp,
LeOp,
GeOp,
// pointer operations
PtrOffsetOp(CaesiumLayout),
PtrOffsetOp(CaesiumLayout),
PtrNegOffsetOp(CaesiumLayout),
PtrDiffOp(CaesiumLayout)
}
......@@ -375,7 +422,7 @@ impl CaesiumBinop {
let rt = String::with_capacity(20);
let format_prim = |st:&str| format!("{}{{ {} , {} }}", st, ot1.caesium_fmt(), ot2.caesium_fmt());
let format_bool = |st:&str| format!("{}{{ {} , {} , {} }}", st, ot1.caesium_fmt(), ot2.caesium_fmt(), (CaesiumIntType::CaesiumU8).caesium_fmt());
let format_bool = |st:&str| format!("{}{{ {} , {} , {} }}", st, ot1.caesium_fmt(), ot2.caesium_fmt(), (BOOL_REPR).caesium_fmt());
match self {
......@@ -466,11 +513,13 @@ impl CaesiumIntType {
}
}
// Notes on ADT representation:
pub static BOOL_REPR: CaesiumIntType = CaesiumIntType::CaesiumI8;
// Notes on ADT representation:
// - Rust structs have a single variant with several fields. This is directly accomodated by
// Caesium structs.
// - Rust enums are more complicated. Need one field for the discriminant.
// Then, essentially, a union of several structs?.
// Then, essentially, a union of several structs?.
// TODO: think more about the correct model for this.
// - Rust unions seem relatively straightforward based on Caesium unions.
// - Rust tuple structs should just compile down to tuples aka structs
......@@ -488,7 +537,7 @@ impl CaesiumStructLayout {
}
// struct itself needs to have size divisible by alignment
offset % self.alignment() == 0
}
}
/// Make a struct layout by correctly padding a given prototypical layout.
pub fn make_layout(prely: Vec<(String, CaesiumLayout)>) -> Self {
......@@ -558,8 +607,8 @@ pub enum CaesiumLayout {
// size 1, similar to u8/i8
BoolLayout,
// always 4 bytes
CharLayout,
// guaranteed to have size 0 and alignment 1.
CharLayout,
// guaranteed to have size 0 and alignment 1.
// TODO: Could alternatively represent this as a struct instead? an empty struct has the
// same representation, essentially
UnitLayout,
......@@ -571,8 +620,9 @@ pub enum CaesiumLayout {
impl CaesiumLayout {
pub fn into_caesium_op_type(self) -> CaesiumOpType {
match self {
//Self::PtrLayout => CaesiumOpType::PtrOp,
//Self::IntLayout(it) => CaesiumOpType::IntOp(it),
Self::PtrLayout => CaesiumOpType::PtrOp,
Self::IntLayout(it) => CaesiumOpType::IntOp(it),
Self::BoolLayout => CaesiumOpType::IntOp(BOOL_REPR),
// TODO: handle structs?
layout => CaesiumOpType::UntypedOp(layout),
}
......@@ -582,11 +632,11 @@ impl CaesiumLayout {
match self {
Self::PtrLayout => "void*".to_string(),
Self::IntLayout(it) => format!("it_layout {}", it.caesium_fmt().as_str()),
Self::BoolLayout => format!("it_layout {}", (CaesiumIntType::CaesiumU8).caesium_fmt().as_str()),
Self::BoolLayout => format!("it_layout {}", BOOL_REPR.caesium_fmt().as_str()),
// TODO
Self::CharLayout => format!("char_layout"),
// TODO
Self::UnitLayout => format!("unit_layout"),
Self::UnitLayout => format!("(layout_of unit_layout)"),
//TODO
Self::StructLayout(ly) => format!("struct_layout"),
// TODO
......@@ -622,13 +672,13 @@ impl CaesiumLayout {
pub enum CaesiumOpType {
IntOp(CaesiumIntType),
PtrOp,
StructOp(CaesiumStructLayout),
StructOp(CaesiumStructLayout),
UntypedOp(CaesiumLayout),
}
impl CaesiumOpType {
fn caesium_fmt(&self) -> String {
match self {
Self::IntOp(it) => format!("IntOp {}", it.caesium_fmt().as_str()),
Self::IntOp(it) => format!("IntOp {}", it.caesium_fmt().as_str()),
Self::PtrOp => "PtrOp".to_string(),
// TODO
Self::StructOp(ly) => "StructOp TODO TODO".to_string(),
......@@ -645,10 +695,22 @@ pub struct CaesiumFunctionCode {
stack_layout: CaesiumStackMap,
basic_blocks: HashMap<String, CaesiumStmt>,
/// Coq parameters that the function is parameterized over
/// Coq parameters that the function is parameterized over
required_parameters: Vec<(CoqName, CoqType)>,
}
fn make_map_string(sep0: &str, sep: &str, els: Vec<(String, String)>) -> String {
let mut out = String::with_capacity(100);
for (key, value) in els.iter() {
out.push_str(sep);
out.push_str(format!("<[\"{}\" :={}{}{}]>%E $", key, sep0, value, sep).as_str());
}
out.push_str(sep);
out.push_str("∅");
out
}
impl CaesiumFunctionCode {
const initial_bb: &'static str = "_bb0";
pub fn caesium_fmt(&self) -> String {
......@@ -679,18 +741,8 @@ impl CaesiumFunctionCode {
let mut formatted_locals = String::with_capacity(100);
formatted_locals.push_str(format!("{}f_local_vars := {}", make_indent(1), format_stack_layout(self.stack_layout.iter_locals()).as_str()).as_str());
let mut formatted_bb = String::with_capacity(1000);
formatted_bb.push_str(format!("{}f_code :=", make_indent(1).as_str()).as_str());
for (name, bb) in self.basic_blocks.iter() {
formatted_bb.push_str("\n");
formatted_bb.push_str(make_indent(2).as_str());
let printed_stmt = bb.caesium_fmt(3);
formatted_bb.push_str(format!("<[\"{}\" :=\n{}\n{}]>%E $", name, printed_stmt, make_indent(2).as_str()).as_str());
}
formatted_bb.push_str("\n");
formatted_bb.push_str(make_indent(2).as_str());
formatted_bb.push_str("∅");
let formatted_bb = make_map_string("\n", format!("\n{}", make_indent(2).as_str()).as_str(),
self.basic_blocks.iter().map(|(name, bb)| (name.to_string(), bb.caesium_fmt(3))).collect());
if self.basic_blocks.len() < 1 {
panic!("CaesiumFunction has no basic block");
......@@ -704,15 +756,20 @@ impl CaesiumFunctionCode {
formatted_params.push_str(format!("({}, : {})", name, ty).as_str());
}
format!("Definition {} {} : function := {{|\n{};\n{};\n{};\n{};\n|}}",
format!("Definition {}_def {} : function := {{|\n{};\n{};\n{}f_code := {};\n{};\n|}}.",
self.name.as_str(),
formatted_params.as_str(),
formatted_args.as_str(),
formatted_locals.as_str(),
make_indent(1).as_str(),
formatted_bb.as_str(),
formatted_init.as_str())
}
/// Get the number of arguments of the function.
pub fn get_argument_count(&self) -> usize {
self.stack_layout.iter_args().len()
}
}
......@@ -732,8 +789,8 @@ impl CaesiumStackMap {
let mut names = HashSet::new();
CaesiumStackMap {
arg_map,
CaesiumStackMap {
arg_map,
local_map,
used_names: names,
}
......@@ -792,10 +849,10 @@ pub struct CaesiumFunctionCodeBuilder {
impl CaesiumFunctionCodeBuilder {
pub fn new() -> CaesiumFunctionCodeBuilder {
CaesiumFunctionCodeBuilder {
stack_layout: CaesiumStackMap::new(),
stack_layout: CaesiumStackMap::new(),
basic_blocks: HashMap::new(),
}
}
......@@ -819,7 +876,7 @@ impl CaesiumFunctionCodeBuilder {
let cont_stmt = CaesiumStmt::Annot {
a: CaesiumAnnotation::StartLft(format!("{}", lft), outliving),
s: Box::new(bb0),
};
};
self.basic_blocks.insert(CaesiumFunctionCode::initial_bb.to_string(), cont_stmt);
}
}
......@@ -831,6 +888,92 @@ pub struct CaesiumFunction {
pub spec: CaesiumFunctionSpec,
}
impl CaesiumFunction {
/// Get the name of the function.
pub fn name(&self) -> &str {
&self.code.name
}
pub fn generate_proof(&self) -> String {
let mut out = String::with_capacity(100);
let indent0 = make_indent(2);
let indent = indent0.as_str();
out.push_str(format!("\
Lemma {}_proof {} (π : thread_id) :\n\
{}⊢ typed_function π {}_def type_of_{}.\n\
Proof.\n",
self.name(), self.spec.coq_context.join(" "), indent, self.name(), self.name()).as_str());
// generate intro pattern for params
let mut ip_params = String::with_capacity(100);
let params = &self.spec.decomposed_params;
if params.len() >0 {
// product is left-associative
for _ in 0 .. params.len() - 1 {
ip_params.push_str("[ ");
}
let mut p_count = 0;
for (n, _) in params {
if p_count > 1 {
ip_params.push_str(" ]");
}
ip_params.push_str(" ");
p_count += 1;
ip_params.push_str(format!("{}", n).as_str());
}
if p_count > 1 {
ip_params.push_str(" ]");
}
}
else {
// no params, but still need to provide something to catch the unit
// (and no empty intropatterns are allowed)
ip_params.push_str("?");
}
out.push_str(format!("{}iStartProof.\n", indent).as_str());
out.push_str(format!("{}start_function \"{}\" ( {} ).\n", indent, self.name(), ip_params.as_str()).as_str());
// intro stack locations
out.push_str(format!("{}intros", indent).as_str());
for (arg, _) in self.code.stack_layout.arg_map.iter() {
out.push_str(" arg_");
out.push_str(arg.as_str());
}
for (local, _) in self.code.stack_layout.local_map.iter() {
out.push_str(" local_");
out.push_str(local.as_str());
}
out.push_str(".\n");
// destruct function parameters
out.push_str(format!("{}prepare_parameters (", indent).as_str());
for (n, _) in params {
out.push_str(" ");
out.push_str(format!("{}", n).as_str());
}
out.push_str(" ).\n");
// initialize lifetimes
let formatted_lifetimes = make_map_string(" ", " ", self.spec.decomposed_params.iter().filter_map(|(n, t)| if t.eq(&CoqType::Lft) { Some ((n.to_string(), n.to_string())) } else { None }).collect());
out.push_str(format!("{}init_lfts ({} ).\n", indent, formatted_lifetimes.as_str()).as_str());
// TODO: split blocks
out.push_str(format!("{}repeat liRStep; liShow.\n", indent).as_str());
out.push_str(format!("{}Unshelve. all: li_unshelve_sidecond; sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.\n", indent).as_str());
// TODO custom tactics specified in annotations
out.push_str(format!("{}Unshelve. all: try done; try apply: inhabitant; print_remaining_shelved_goal \"{}\".\n", indent, self.name()).as_str());
out.push_str("Qed.\n");
out
}
}
/// A CaesiumFunctionBuilder allows to incrementally construct the functions's code and the spec
/// at the same time. It ensures that both definitions line up in the right way (for instance, by
/// ensuring that other functions are linked up in a consistent way).
......@@ -867,12 +1010,12 @@ impl CaesiumFunctionBuilder {
/// Require refinements by a given CoqType to be available.
/// It does not matter when a type is registered via this function.
fn require_rfn_type(&mut self, t: CoqType) {
self.rfn_types.push(t);
self.rfn_types.push(t);
}
/// Adds a lifetime parameter to the function.
fn add_universal_lifetime(&mut self, lft: CaesiumLft) -> Result<(), String> {
self.spec.add_coq_param(CoqName::Named(lft), CoqType::Lft, false)
pub fn add_universal_lifetime(&mut self, lft: CaesiumLft) -> Result<(), String> {
self.spec.add_param(CoqName::Named(lft), CoqType::Lft)
}
}
......@@ -887,9 +1030,9 @@ impl Into<CaesiumFunction> for CaesiumFunctionBuilder {
required_parameters: fn_loc_parameters,
};
// push required parameters to the spec builder
// push required parameters to the spec builder
for t in self.rfn_types.iter() {
//TODO will need more elaborate scheme to insert the right place_rfn things
//TODO will need more elaborate scheme to insert the right place_rfn things
self.spec.add_unnamed_coq_param(CoqType::Literal(format!("ghost_varG Σ {}", t)), true);
}
let spec = self.spec.into_function_spec(&self.function_name);
......
rr_frontend/translation/src/caesium/specs.rs
View file @ 67aa9dcd
......@@ -2,7 +2,7 @@ use std::collections::HashSet;
use std::fmt::{Formatter, Display};
use std::fmt as fmt;
#[derive(Clone)]
#[derive(Clone, Debug)]
pub enum IPropConj {
Literal(String),
}
......@@ -15,7 +15,7 @@ impl Display for IPropConj {
}
}
#[derive(Clone)]
#[derive(Clone, Debug)]
/// Encodes a RR type with an accompanying refinement.
pub enum CaesiumTypeWithRef {
/// refinement + type
......@@ -28,12 +28,12 @@ impl Display for CaesiumTypeWithRef {
match self {
Self::Literal(rfn, t) => write!(f, "{} @ {}", rfn, t),
// TODO might need fix to rename unit
Self::Unit => write!(f, ".@ unit"),
Self::Unit => write!(f, "() @ unit_t"),
}
}
}
#[derive(Clone)]
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum CoqType {
Literal(String),
/// Coq type `lft`
......@@ -51,7 +51,7 @@ impl Display for CoqType {
}
}
#[derive(Clone)]
#[derive(Clone, Debug)]
pub enum CoqName {