Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Decoupled ImplItemKind.class_instance_to_doc() #431

Merged
merged 6 commits into from
Dec 22, 2023
Merged

Decoupled ImplItemKind.class_instance_to_doc() #431

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ff5fbd7
Decoupled `ImplItemKind.class_instance_to_doc`
InfiniteEchoes Dec 21, 2023
bac3360
Applied `justname` to further reduce code
InfiniteEchoes Dec 21, 2023
64ea8fc
Deleted comment
InfiniteEchoes Dec 21, 2023
b9faab2
cargo fmt
InfiniteEchoes Dec 21, 2023
5736344
Update snapshot
InfiniteEchoes Dec 21, 2023
8490e0f
Fixed bug and updated python script
InfiniteEchoes Dec 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion CoqOfRust/make_and_detect_warnings.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
from subprocess import Popen, PIPE
import threading
import sys

global lines
lines = []
Expand Down Expand Up @@ -66,7 +67,7 @@ def check_warnings():
print("Checking warnings...")
for line in errorlines:
if line.startswith("Warning: "):
print("Warnings detected from coqc. Abort.")
print("Warnings detected from coqc. Abort.", file=sys.err)
exit(1)
print("Check complete, no warnings detected")

Expand Down
30 changes: 21 additions & 9 deletions lib/src/coq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -690,16 +690,19 @@ impl<'a> Instance<'a> {
concat([
nest([
nest([
text("Global Instance"),
line(),
text("Global Instance "),
text(self.name.to_owned()),
optional_insert(
self.parameters.is_empty(),
concat([
line(),
intersperse(self.parameters.iter().map(|p| p.to_doc()), [line()]),
]),
),
optional_insert(self.parameters.is_empty(), {
let non_empty_params: Vec<_> =
self.parameters.iter().filter(|p| !p.is_empty()).collect();
optional_insert(
non_empty_params.is_empty(),
concat([
line(),
intersperse(non_empty_params.iter().map(|p| p.to_doc()), [line()]),
]),
)
}),
]),
text(" :"),
line(),
Expand Down Expand Up @@ -1020,6 +1023,15 @@ impl<'a> Field<'a> {
}

impl<'a> ArgDecl<'a> {
pub(crate) fn is_empty(&self) -> bool {
match self.decl.to_owned() {
ArgDeclVar::Simple { idents, .. } => idents.is_empty(),
ArgDeclVar::Generalized { .. } => false, // ty would always be exist
ArgDeclVar::Traits { traits } => traits.is_empty(),
ArgDeclVar::Destructured { .. } => false,
}
}

/// produces a new coq argument
pub(crate) fn new(decl: &ArgDeclVar<'a>, kind: ArgSpecKind) -> Self {
ArgDecl {
Expand Down
115 changes: 46 additions & 69 deletions lib/src/top_level.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1539,77 +1539,54 @@ impl FunDefinition {
}

impl ImplItemKind {
fn class_instance_to_doc<'a>(
fn class_instance_to_coq<'a>(
instance_prefix: &'a str,
name: &'a str,
ty_params: Option<&'a [String]>,
where_predicates: Option<&'a [Rc<WherePredicate>]>,
class_name: &'a str,
method_name: &'a str,
) -> Doc<'a> {
group([
nest([
nest([
text("Global Instance "),
text(format!("{instance_prefix}_{name}")),
// Type parameters a, b, c... compiles to {a b c ... : Set}
match ty_params {
None | Some([]) => nil(),
Some(ty_params) => concat([
line(),
coq::ArgDecl::of_ty_params(ty_params, coq::ArgSpecKind::Implicit)
.to_doc(),
]),
},
// where predicates types
match where_predicates {
None | Some([]) => nil(),
Some(where_predicates) => concat([
line(),
WherePredicate::vec_to_coq(where_predicates).to_doc(),
]),
},
text(" :"),
]),
line(),
nest([
text(class_name),
line(),
text(format!("\"{name}\"")),
text(" := {"),
]),
]),
nest([
hardline(),
nest([
text(method_name),
line(),
text(":="),
line(),
{
let body = coq::Expression::just_name(name);
match ty_params {
None => body,
Some(ty_params) => body.apply_many_args(
&ty_params
.iter()
.map(|ty_param| {
(
Some(ty_param.to_owned()),
coq::Expression::just_name(ty_param),
)
})
.collect::<Vec<_>>(),
),
}
.to_doc(false)
},
text(";"),
]),
]),
hardline(),
text("}."),
])
) -> coq::TopLevelItem<'a> {
// Type parameters a, b, c... compiles to {a b c ... : Set}
let ty_params_arg = coq::ArgDecl::of_ty_params(
match ty_params {
None | Some([]) => &[],
Some(ty_params) => ty_params,
},
coq::ArgSpecKind::Implicit,
);
// where predicates types
let where_predicates = match where_predicates {
None | Some([]) => WherePredicate::vec_to_coq(&[]),
Some(where_predicates) => WherePredicate::vec_to_coq(where_predicates),
};

let body = coq::Expression::just_name(name);
let entry = match ty_params {
None => body,
Some(ty_params) => body.apply_many_args(
&ty_params
.iter()
.map(|ty_param| {
(
Some(ty_param.to_owned()),
coq::Expression::just_name(ty_param),
)
})
.collect::<Vec<_>>(),
),
};

coq::TopLevelItem::Instance(coq::Instance::new(
&format!("{instance_prefix}_{name}"),
&[ty_params_arg, where_predicates],
coq::Expression::just_name(class_name)
.apply(&coq::Expression::just_name(format!("\"{name}\"").as_str())),
&coq::Expression::Record {
fields: vec![coq::Field::new(&Path::new(&[method_name]), &[], &entry)],
},
vec![],
))
}

fn to_coq<'a>(&'a self, name: &'a str) -> coq::TopLevel<'a> {
Expand Down Expand Up @@ -1645,26 +1622,26 @@ impl ImplItemKind {
)),
},
coq::TopLevelItem::Line,
coq::TopLevelItem::Code(Self::class_instance_to_doc(
Self::class_instance_to_coq(
"AssociatedFunction",
name,
None,
None,
"Notations.DoubleColon Self",
"Notations.double_colon",
)),
),
])]),
ImplItemKind::Definition { definition, .. } => coq::TopLevel::new(&[
coq::TopLevelItem::Code(definition.to_doc(name, None)),
coq::TopLevelItem::Line,
coq::TopLevelItem::Code(Self::class_instance_to_doc(
Self::class_instance_to_coq(
"AssociatedFunction",
name,
Some(&definition.ty_params),
Some(&definition.where_predicates),
"Notations.DoubleColon Self",
"Notations.double_colon",
)),
),
]),
ImplItemKind::Type { ty } => {
coq::TopLevel::new(&[coq::TopLevelItem::Definition(coq::Definition::new(
Expand Down
Loading