diff --git a/Cargo.lock b/Cargo.lock index 7efe2d92..07b7149d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -51,11 +51,12 @@ version = "0.1.0" dependencies = [ "base64", "failure", - "frunk", + "frunk_core", "itertools", "lazy_static", "nom", "petgraph", + "serde", "sha2", "strum", "strum_macros", @@ -69,7 +70,7 @@ name = "aris-auto-grader" version = "0.1.0" dependencies = [ "aris", - "frunk", + "frunk_core", ] [[package]] @@ -85,16 +86,27 @@ name = "aris-java" version = "0.1.0" dependencies = [ "aris", - "frunk", + "frunk_core", "jni", ] +[[package]] +name = "aris-js" +version = "0.1.0" +dependencies = [ + "aris", + "frunk_core", + "js-sys", + "serde-wasm-bindgen", + "wasm-bindgen", +] + [[package]] name = "aris-web-app" version = "0.1.0" dependencies = [ "aris", - "frunk", + "frunk_core", "gloo", "js-sys", "strum", @@ -362,70 +374,13 @@ version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" -[[package]] -name = "frunk" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8313555ac9fdcbe88b502fbd5b9f7de3270654635444d8279242613ad3fdc41e" -dependencies = [ - "frunk_core", - "frunk_derives", - "frunk_proc_macros", -] - [[package]] name = "frunk_core" version = "0.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "26c09b4b25ef220d9b6ac31dc0bb3479fccdf539598893f1cbf27d5a5bc324b5" - -[[package]] -name = "frunk_derives" -version = "0.2.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04a917380b97872efb7a5e560cbd67f6234c90133a60a8a17aa3b053b95d103f" -dependencies = [ - "frunk_core", - "frunk_proc_macro_helpers", - "quote 0.6.13", - "syn 0.15.44", -] - -[[package]] -name = "frunk_proc_macro_helpers" -version = "0.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "127176d3c96d6a9011bdb87194bd06b6f01c2524070a61669ad600cb4f3f08f6" -dependencies = [ - "frunk_core", - "quote 0.6.13", - "syn 0.15.44", -] - -[[package]] -name = "frunk_proc_macros" -version = "0.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46a82ea7fce299f0f0f78233cdf373425b13fa9c2b04df42d2bd3187d2cfe4fb" dependencies = [ - "frunk_core", - "frunk_proc_macros_impl", - "proc-macro-hack", - "quote 0.6.13", - "syn 0.15.44", -] - -[[package]] -name = "frunk_proc_macros_impl" -version = "0.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "98e073845f3791501385f17aa96d03527d982a9483013706684c86450c4fe3d0" -dependencies = [ - "frunk_core", - "frunk_proc_macro_helpers", - "proc-macro-hack", - "quote 0.6.13", - "syn 0.15.44", + "serde", ] [[package]] @@ -697,9 +652,9 @@ checksum = "8eaf4bc02d17cbdd7ff4c7438cafcdf7fb9a4613313ad11b4f8fefe7d3fa0130" [[package]] name = "js-sys" -version = "0.3.40" +version = "0.3.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ce10c23ad2ea25ceca0093bd3192229da4c5b3c0f2de499c1ecac0d98d452177" +checksum = "c4b9172132a62451e56142bff9afc91c8e4a4500aa5b847da36815b63bfda916" dependencies = [ "wasm-bindgen", ] @@ -1065,6 +1020,18 @@ dependencies = [ "serde_derive", ] +[[package]] +name = "serde-wasm-bindgen" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7ee6f12f7ed0e7ad2e55200da37dbabc2cadeb942355c5b629aa3771f5ac5636" +dependencies = [ + "fnv", + "js-sys", + "serde", + "wasm-bindgen", +] + [[package]] name = "serde_derive" version = "1.0.114" @@ -1078,9 +1045,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.55" +version = "1.0.56" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec2c5d7e739bc07a3e73381a39d61fdb5f671c60c1df26a130690665803d8226" +checksum = "3433e879a558dde8b5e8feb2a04899cf34fdde1fafb894687e52105fc1162ac3" dependencies = [ "itoa", "ryu", @@ -1409,19 +1376,21 @@ checksum = "cccddf32554fecc6acb585f82a32a72e28b48f8c4c1883ddfeeeaa96f7d8e519" [[package]] name = "wasm-bindgen" -version = "0.2.63" +version = "0.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c2dc4aa152834bc334f506c1a06b866416a8b6697d5c9f75b9a689c8486def0" +checksum = "6a634620115e4a229108b71bde263bb4220c483b3f07f5ba514ee8d15064c4c2" dependencies = [ "cfg-if", + "serde", + "serde_json", "wasm-bindgen-macro", ] [[package]] name = "wasm-bindgen-backend" -version = "0.2.63" +version = "0.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ded84f06e0ed21499f6184df0e0cb3494727b0c5da89534e0fcc55c51d812101" +checksum = "3e53963b583d18a5aa3aaae4b4c1cb535218246131ba22a71f05b518098571df" dependencies = [ "bumpalo", "lazy_static", @@ -1446,9 +1415,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.63" +version = "0.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "838e423688dac18d73e31edce74ddfac468e37b1506ad163ffaf0a46f703ffe3" +checksum = "3fcfd5ef6eec85623b4c6e844293d4516470d8f19cd72d0d12246017eb9060b8" dependencies = [ "quote 1.0.7", "wasm-bindgen-macro-support", @@ -1456,9 +1425,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.63" +version = "0.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3156052d8ec77142051a533cdd686cba889537b213f948cd1d20869926e68e92" +checksum = "9adff9ee0e94b926ca81b57f57f86d5545cdcb1d259e21ec9bdd95b901754c75" dependencies = [ "proc-macro2 1.0.18", "quote 1.0.7", @@ -1469,9 +1438,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.63" +version = "0.2.64" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c9ba19973a58daf4db6f352eda73dc0e289493cd29fb2632eb172085b6521acd" +checksum = "7f7b90ea6c632dd06fd765d44542e234d5e63d9bb917ecd64d79778a13bd79ae" [[package]] name = "web-sys" diff --git a/Cargo.toml b/Cargo.toml index 1bfc1b7d..33f5c59f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,4 +6,5 @@ members = [ "auto-grader", "bindings/c", "bindings/java", + "bindings/js", ] diff --git a/aris/Cargo.toml b/aris/Cargo.toml index 8da3ae1f..e14c30b1 100644 --- a/aris/Cargo.toml +++ b/aris/Cargo.toml @@ -14,9 +14,10 @@ sha2 = "0.8.1" varisat = "0.2.1" xml-rs = "0.8.0" itertools = "0.9.0" -frunk = "0.2.2" +frunk_core = { version = "0.2.2", features = ["serde"] } strum = "0.18.0" strum_macros = "0.18.0" +serde = { version = "^1.0", features = ["derive"] } [build-dependencies] version_check = "0.9" diff --git a/aris/src/expression.rs b/aris/src/expression.rs index 1388ea64..4a2902ea 100644 --- a/aris/src/expression.rs +++ b/aris/src/expression.rs @@ -62,34 +62,38 @@ assert_eq!(does_it_have_any_ands(&expr2), true); assert_eq!(does_it_have_any_ands(&expr3), false); ``` */ + use super::*; + use std::collections::{HashSet, HashMap}; use std::collections::BTreeSet; use std::mem; use std::ops::Not; use itertools::Itertools; +use serde::Deserialize; +use serde::Serialize; /// Symbol for unary operations -#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd, Serialize, Deserialize)] #[repr(C)] pub enum USymbol { Not } /// Symbol for binary operations -#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd, Serialize, Deserialize)] #[repr(C)] pub enum BSymbol { Implies, Plus, Mult } /// Symbol for associative binary operations -#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd, Serialize, Deserialize)] #[repr(C)] pub enum ASymbol { And, Or, Bicon, Equiv } /// Symbol for quantifiers -#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd, Serialize, Deserialize)] #[repr(C)] pub enum QSymbol { Forall, Exists } /// aris::expression::Expr is the core AST (Abstract Syntax Tree) type for representing logical expressions. /// For most of the recursive cases, it uses symbols so that code can work on the shape of e.g. a binary operation without worrying about which binary operation it is. -#[derive(Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd)] +#[derive(Clone, Debug, PartialEq, Eq, Hash, Ord, PartialOrd, Serialize, Deserialize)] #[repr(C)] pub enum Expr { Contradiction, diff --git a/aris/src/lib.rs b/aris/src/lib.rs index 92757d50..372db107 100644 --- a/aris/src/lib.rs +++ b/aris/src/lib.rs @@ -1,4 +1,4 @@ -#[macro_use] extern crate frunk; +#[macro_use] extern crate frunk_core; #[macro_use] extern crate nom; #[macro_use] extern crate lazy_static; diff --git a/aris/src/proofs.rs b/aris/src/proofs.rs index fe8bfba4..4e6048a5 100644 --- a/aris/src/proofs.rs +++ b/aris/src/proofs.rs @@ -27,7 +27,7 @@ The test running apparatus expects you to return the proof, a list of line refer ## Parsing XML into a PooledProof ``` -#[macro_use] extern crate frunk; +#[macro_use] extern crate frunk_core; use aris::expression::Expr; use aris::proofs::xml_interop::proof_from_xml; let data = &include_bytes!("../../example-proofs/propositional_logic_arguments_for_proofs_ii_problem_10.bram")[..]; @@ -54,8 +54,8 @@ ASCII art proof: Code that builds the proof generically and then instantiates it: ``` -#[macro_use] extern crate frunk; -use frunk::Coproduct; +#[macro_use] extern crate frunk_core; +use frunk_core::coproduct::Coproduct; use aris::expression::Expr; use aris::proofs::{Proof, Justification, pooledproof::PooledProof}; use aris::rules::RuleM; @@ -85,8 +85,8 @@ let concrete_proof = contraposition_demo::

(); # Mutating existing lines of a proof ``` -#[macro_use] extern crate frunk; -use frunk::Coproduct; +#[macro_use] extern crate frunk_core; +use frunk_core::coproduct::Coproduct; use aris::expression::Expr; use aris::parser::parse_unwrap as p; use aris::proofs::{Proof, Justification, pooledproof::PooledProof}; @@ -115,7 +115,7 @@ The subproof pointer in `with_mut_subproof`, if returned directly, could be inva This is prevented by the fact that the lifetime parameter of the subproof reference cannot occur in A: ```compile_fail,E0495 -#[macro_use] extern crate frunk; +#[macro_use] extern crate frunk_core; use aris::proofs::{Proof, pooledproof::PooledProof}; use aris::expression::Expr; fn should_fail_with_lifetime_error() { @@ -129,12 +129,16 @@ This is a similar trick to the rank-2 type of `runST` in Haskell used to prevent */ use super::*; -use frunk::coproduct::*; + use std::collections::HashSet; use std::fmt::{Display, Formatter}; use std::hash::Hash; use std::ops::Range; +use frunk_core::coproduct::*; +use serde::Deserialize; +use serde::Serialize; + #[cfg(test)] mod proof_tests; @@ -262,7 +266,7 @@ pub trait Proof: Sized { ret } fn transitive_dependencies(&self, line: PJRef) -> HashSet> { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; // TODO: cycle detection let mut stack: Vec> = vec![pj_to_pjs::(line)]; let mut result = HashSet::new(); @@ -303,7 +307,7 @@ pub trait Proof: Sized { // 3) if r2 is a subproof reference, r1 must be outside r2's subproof // we compute the set of lines satisfying these properties by walking backwards starting from the subproof that r1 is in, adding lines that respect these rules fn aux(top: &P, sr: Option, r: &PJSRef

, deps: &mut HashSet>, sdeps: &mut HashSet) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; let prf = sr.and_then(|sr| Some((sr.clone(), top.lookup_subproof(&sr)?))); match prf { Some((sr, sub)) => { @@ -354,7 +358,7 @@ pub trait Proof: Sized { /// A Justification struct represents a step in the proof. /// It contains an expression, a rule indicating why that expression is justified, and references to previous lines/subproofs for validating the rule. -#[derive(Clone, Debug, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)] pub struct Justification(pub T, pub Rule, pub Vec, pub Vec); impl Justification { @@ -365,7 +369,7 @@ impl Justification { pub trait JustificationExprDisplay { fn fmt_expr(&self, fmt: &mut Formatter) -> std::fmt::Result; } impl JustificationExprDisplay for Expr { fn fmt_expr(&self, fmt: &mut Formatter) -> std::fmt::Result { write!(fmt, "{}", self) } } -impl JustificationExprDisplay for frunk::HCons { fn fmt_expr(&self, fmt: &mut Formatter) -> std::fmt::Result { write!(fmt, "{}", self.head) } } +impl JustificationExprDisplay for frunk_core::hlist::HCons { fn fmt_expr(&self, fmt: &mut Formatter) -> std::fmt::Result { write!(fmt, "{}", self.head) } } impl DisplayIndented for Justification { fn display_indented(&self, fmt: &mut Formatter, indent: usize, linecount: &mut usize) -> std::result::Result<(), std::fmt::Error> { diff --git a/aris/src/proofs/java_shallow_proof.rs b/aris/src/proofs/java_shallow_proof.rs index 27e22727..a5875f86 100644 --- a/aris/src/proofs/java_shallow_proof.rs +++ b/aris/src/proofs/java_shallow_proof.rs @@ -1,5 +1,5 @@ use super::*; -use frunk::Coproduct; +use frunk_core::coproduct::Coproduct; #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub struct JavaShallowProof(pub Vec); @@ -61,7 +61,7 @@ impl Proof for JavaShallowProof { } fn parent_of_line(&self, _: &PJSRef) -> Option { unimplemented!() } fn verify_line(&self, r: &PJRef) -> Result<(), ProofCheckError, Self::SubproofReference>> { - use self::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; match self.lookup_pj(r) { None => Err(ProofCheckError::LineDoesNotExist(r.clone())), Some(Inl(_)) => Ok(()), // premises are always valid diff --git a/aris/src/proofs/lined_proof.rs b/aris/src/proofs/lined_proof.rs index a2f9296e..169e476b 100644 --- a/aris/src/proofs/lined_proof.rs +++ b/aris/src/proofs/lined_proof.rs @@ -76,7 +76,7 @@ impl LinedProof

where PJRef

: Debug, P::SubproofReference: } pub fn from_proof(p: P) -> Self { fn aux(p: &P::Subproof, ret: &mut LinedProof

, current_sub: Option) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; for prem in p.premises() { let e = p.lookup_premise(&prem).unwrap(); ret.lines.push(Line::new(format!("{}", e), true, Inl(prem), current_sub.clone())); @@ -101,7 +101,7 @@ impl LinedProof

where PJRef

: Debug, P::SubproofReference: ret } pub fn add_line(&mut self, i: usize, is_premise: bool, subproof_level: usize) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; println!("add_line {:?} {:?} {:?}", i, is_premise, subproof_level); let const_true = Expr::Tautology; let line: Option> = self.lines.get(i).cloned(); diff --git a/aris/src/proofs/pooledproof.rs b/aris/src/proofs/pooledproof.rs index 0cdbc931..3d5c1ecb 100644 --- a/aris/src/proofs/pooledproof.rs +++ b/aris/src/proofs/pooledproof.rs @@ -101,18 +101,23 @@ These illustrations are less verbose than the `Debug` rendering of an actual `Po ### Parse trees `AST("forall x, p(x)")` will be rendered as the actual AST `Quantifier { symbol: Forall, name: "x", body: Apply { func: Var { name: "p" }, args: [Var { name: "x" }] } }`. ### Coproducts -Various parts of `PooledProof` use `frunk::Coproduct` to create subtypes of the union of `{PremKey, JustKey, SubKey}` to get more precise typing guarantees. This manifests as occurrences of `{Inl,Inr}`. +Various parts of `PooledProof` use `frunk_core::coproduct::Coproduct` to create subtypes of the union of `{PremKey, JustKey, SubKey}` to get more precise typing guarantees. This manifests as occurrences of `{Inl,Inr}`. ### Vec vs ZipperVec While the `[]`s in the `Justification`s are actually `Vec`s and will be that simple in the `Debug` rendering, `premise_list` and `line_list` are `ZipperVec`s for performance, and so the `Debug` rendering reveals where the cursor (roughly, last insertion point) is. */ use super::*; -use frunk::hlist::HCons; +use frunk_core::hlist::HCons; use std::collections::BTreeMap; -#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct PremKey(usize); -#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct JustKey(usize); -#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] pub struct SubKey(usize); +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +pub struct PremKey(usize); + +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +pub struct JustKey(usize); + +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +pub struct SubKey(usize); type PooledRef = Coprod!(PremKey, JustKey); @@ -121,7 +126,7 @@ pub struct Pools { prem_map: BTreeMap, just_map: BTreeMap>, sub_map: BTreeMap>, - containing_subproof: BTreeMap>>, SubKey>, + containing_subproof: BTreeMap>>, SubKey>, } impl Pools { @@ -153,7 +158,7 @@ impl Pools { result } fn remove_line(&mut self, idx: &Coprod!(PremKey, JustKey)) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; match idx { Inl(prem) => self.remove_premise(prem), Inr(Inl(just)) => self.remove_step(just), @@ -161,7 +166,7 @@ impl Pools { } } fn remove_line_helper(&mut self, idx: &Coprod!(PremKey, JustKey, SubKey)) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; let just_map = std::mem::replace(&mut self.just_map, BTreeMap::new()); self.just_map = just_map.into_iter().map(|(k, Justification(expr, rule, deps, sdeps))| { let (new_deps, new_sdeps) = match idx { @@ -191,7 +196,7 @@ impl Pools { self.remove_line_helper(&Coproduct::inject(*idx)); } fn remove_subproof(&mut self, idx: &SubKey) { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; if let Some(sub) = self.sub_map.remove(idx) { for prem in sub.premise_list.iter() { self.remove_premise(prem); @@ -222,7 +227,7 @@ pub struct PooledProof { pub struct PooledSubproof { pools: *mut Pools, premise_list: ZipperVec, - line_list: ZipperVec>>, + line_list: ZipperVec>>, } impl PooledSubproof { diff --git a/aris/src/proofs/proof_tests.rs b/aris/src/proofs/proof_tests.rs index 271c173c..03a1d700 100644 --- a/aris/src/proofs/proof_tests.rs +++ b/aris/src/proofs/proof_tests.rs @@ -1,10 +1,14 @@ #![deny(unused_variables, dead_code)] use super::*; + use std::fmt::Debug; -fn coproduct_inject(to_insert: T) -> frunk::Coproduct - where frunk::Coproduct: frunk::coproduct::CoprodInjector { - frunk::Coproduct::inject(to_insert) +use frunk_core::coproduct::Coproduct; +use frunk_core::coproduct::CoprodInjector; + +fn coproduct_inject(to_insert: T) -> Coproduct + where Coproduct: CoprodInjector { + Coproduct::inject(to_insert) } fn run_test (P, Vec>, Vec>)>(f: F) where PJRef

: Debug, P::SubproofReference: Debug { diff --git a/aris/src/proofs/treeproof.rs b/aris/src/proofs/treeproof.rs index 6a13e097..13f9026a 100644 --- a/aris/src/proofs/treeproof.rs +++ b/aris/src/proofs/treeproof.rs @@ -1,5 +1,5 @@ use super::*; -use frunk::coproduct::{Coproduct, CNil}; +use frunk_core::coproduct::{Coproduct, CNil}; //use std::rc::{Rc, Weak}; #[derive(Clone, PartialEq, Eq, Hash)] diff --git a/aris/src/proofs/treeproof_tests.rs b/aris/src/proofs/treeproof_tests.rs index 8e1a064f..ae67bbef 100644 --- a/aris/src/proofs/treeproof_tests.rs +++ b/aris/src/proofs/treeproof_tests.rs @@ -3,7 +3,7 @@ use super::treeproof::*; #[test] fn demo_prettyprinting() { - use frunk::Coproduct::Inl; + use frunk_core::coproduct::Coproduct::Inl; use parser::parse_unwrap as p; let proof1 = TreeProof(TreeSubproof { premises: vec![((),p("A")), ((),p("B"))], diff --git a/aris/src/proofs/xml_interop.rs b/aris/src/proofs/xml_interop.rs index a3f338b7..da15a7cb 100644 --- a/aris/src/proofs/xml_interop.rs +++ b/aris/src/proofs/xml_interop.rs @@ -174,7 +174,7 @@ pub fn xml_from_proof_and_metadata(prf: &P, meta: &ProofMeta state.linenum += 1; } for step in prf.lines() { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; match step { Inl(jr) => { state.deps_map.insert(Coproduct::inject(jr), state.linenum); @@ -201,7 +201,7 @@ pub fn xml_from_proof_and_metadata(prf: &P, meta: &ProofMeta ew.write(XmlEvent::end_element())?; } for step in prf.lines() { - use frunk::Coproduct::{Inl, Inr}; + use frunk_core::coproduct::Coproduct::{Inl, Inr}; match step { Inl(jr) => { let just = prf.lookup_step(&jr).unwrap(); diff --git a/aris/src/rules.rs b/aris/src/rules.rs index 2e950e25..93ef3fbd 100644 --- a/aris/src/rules.rs +++ b/aris/src/rules.rs @@ -7,7 +7,7 @@ Rules are split into different enums both for based on what type of rule they ar This allows metadata to be defined only once for certain classes of rules (e.g. `Equivalence`s always take 1 plain dep and 0 subdeps). -The `SharedChecks` wrapper and `frunk::Coproduct` tie the different enums together into `Rule`. +The `SharedChecks` wrapper and `frunk_core::coproduct::Coproduct` tie the different enums together into `Rule`. `SharedChecks`'s `RuleT` instance enforces common requirements based on the inner type's metadata (mostly number of dependencies. @@ -51,15 +51,20 @@ Adding the tests and implementing the rule can be interleaved; it's convenient t - if default metadata applies to all rules of the type, add those (e.g. `Equivalence`) - if default metadata doesn't apply to all rules of the type, add an empty match block (e.g. `PrepositionalInference`) */ + use super::*; use proofs::PJRef; + use std::collections::{HashMap, HashSet}; use std::iter::FromIterator; -use frunk::Coproduct::{self, Inl, Inr}; + +use frunk_core::coproduct::Coproduct::{self, Inl, Inr}; use petgraph::algo::tarjan_scc; use petgraph::graphmap::DiGraphMap; +use serde::Deserialize; +use serde::Serialize; -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum PrepositionalInference { Reit, AndIntro, AndElim, @@ -71,48 +76,47 @@ pub enum PrepositionalInference { EquivalenceIntro, EquivalenceElim, } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum PredicateInference { ForallIntro, ForallElim, ExistsIntro, ExistsElim, } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum Equivalence { DeMorgan, Association, Commutation, Idempotence, Distribution, DoubleNegation, Complement, Identity, Annihilation, Inverse, Absorption, Reduction, Adjacency } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum ConditionalEquivalence { Complement, Identity, Annihilation, Implication, BiImplication, Contraposition, Currying, ConditionalDistribution, ConditionalReduction, KnightsAndKnaves, ConditionalIdempotence, BiconditionalNegation, BiconditionalSubstitution } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum RedundantPrepositionalInference { ModusTollens, HypotheticalSyllogism, ExcludedMiddle, ConstructiveDilemma } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum AutomationRelatedRules { AsymmetricTautology, Resolution, TautologicalConsequence, } -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub enum QuantifierEquivalence { QuantifierNegation, NullQuantification, ReplacingBoundVars, SwappingQuantifiers, AristoteleanSquare, QuantifierDistribution, PrenexLaws } - /// The RuleT instance for SharedChecks does checking that is common to all the rules; /// it should always be the outermost constructor of the Rule type alias. -#[derive(Clone, Copy, Debug, PartialEq, Eq)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)] pub struct SharedChecks(T); pub type Rule = SharedChecks RuleT for Coproduct { match self { Inl(x) => x.check(p, expr, deps, sdeps), Inr(x) => x.check(p, expr, deps, sdeps), } } } -impl RuleT for frunk::coproduct::CNil { +impl RuleT for frunk_core::coproduct::CNil { fn get_name(&self) -> String { match *self {} } fn get_classifications(&self) -> HashSet { match *self {} } fn num_deps(&self) -> Option { match *self {} } @@ -1127,7 +1131,7 @@ fn either_orderResult, ProofChe pub enum ProofCheckError { LineDoesNotExist(R), SubproofDoesNotExist(S), - ReferencesLaterLine(R, Coproduct>), + ReferencesLaterLine(R, Coproduct>), IncorrectDepCount(Vec, usize), IncorrectSubDepCount(Vec, usize), DepOfWrongForm(Expr, Expr), diff --git a/aris/src/solver_integration/solver.rs b/aris/src/solver_integration/solver.rs index fb236c5d..380881c5 100644 --- a/aris/src/solver_integration/solver.rs +++ b/aris/src/solver_integration/solver.rs @@ -1,4 +1,4 @@ -use frunk::Coproduct; +use frunk_core::coproduct::Coproduct; use varisat::{Lit, checker::{ProofProcessor, CheckedProofStep}}; use crate::proofs::{Proof, Justification, PJRef}; use crate::expression::{Expr, ASymbol, USymbol}; diff --git a/auto-grader/Cargo.toml b/auto-grader/Cargo.toml index b1be337c..261eb318 100644 --- a/auto-grader/Cargo.toml +++ b/auto-grader/Cargo.toml @@ -6,4 +6,4 @@ edition = "2018" [dependencies] aris = { path = "../aris" } -frunk = "0.2.2" +frunk_core = "0.2.2" diff --git a/auto-grader/src/main.rs b/auto-grader/src/main.rs index e6e012ef..7da77324 100644 --- a/auto-grader/src/main.rs +++ b/auto-grader/src/main.rs @@ -2,8 +2,8 @@ extern crate aris; // This file builds the headless version of Aris, // meant for verifying proofs submitted on Submitty. -#[macro_use] extern crate frunk; -use frunk::Coproduct; +#[macro_use] extern crate frunk_core; +use frunk_core::coproduct::Coproduct; use std::env; use std::path::Path; @@ -20,7 +20,7 @@ use aris::proofs::lined_proof::LinedProof; fn validate_recursive(proof: &P, line: PJRef

) -> Result<(), (PJRef

, ProofCheckError, P::SubproofReference>)> where PJRef

:Debug, P::SubproofReference:Debug { use ProofCheckError::*; - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; let mut q = vec![line]; // lookup returns either expr or Justification. if it returns the expr, it's done. diff --git a/bindings/java/Cargo.toml b/bindings/java/Cargo.toml index 303f0cea..73d1772c 100644 --- a/bindings/java/Cargo.toml +++ b/bindings/java/Cargo.toml @@ -10,4 +10,4 @@ crate-type = ["cdylib"] [dependencies] aris = { path = "../../aris" } jni = "0.10.2" -frunk = "0.2.2" +frunk_core = "0.2.2" diff --git a/bindings/java/src/java_proof.rs b/bindings/java/src/java_proof.rs index df908d90..39ba62b2 100644 --- a/bindings/java/src/java_proof.rs +++ b/bindings/java/src/java_proof.rs @@ -5,7 +5,7 @@ use aris::proofs::Proof; use aris::proofs::lined_proof::LinedProof; use aris::proofs::pooledproof::PooledProof; -use frunk::Hlist; +use frunk_core::Hlist; #[no_mangle] #[allow(non_snake_case)] diff --git a/bindings/java/src/java_rule.rs b/bindings/java/src/java_rule.rs index 08a2316b..636f07d3 100644 --- a/bindings/java/src/java_rule.rs +++ b/bindings/java/src/java_rule.rs @@ -5,6 +5,8 @@ use aris::rules::RuleClassification; use aris::rules::RuleM; use aris::rules::RuleT; +use frunk_core::coproduct::Coproduct; + #[no_mangle] #[allow(non_snake_case)] pub extern "system" fn Java_edu_rpi_aris_rules_Rule_fromRule(env: JNIEnv, _: JObject, rule: JObject) -> jobject { @@ -130,7 +132,7 @@ pub extern "system" fn Java_edu_rpi_aris_rules_Rule_verifyClaim(env: JNIEnv, rul } sdeps.push(sdep); } else { - deps.push(frunk::Coproduct::Inl(jobject_to_expr(env, env.call_method(prem, "getPremise", "()Ledu/rpi/aris/ast/Expression;", &[])?.l()?)?)); + deps.push(Coproduct::Inl(jobject_to_expr(env, env.call_method(prem, "getPremise", "()Ledu/rpi/aris/ast/Expression;", &[])?.l()?)?)); } } println!("Rule::verifyClaim deps: {:?} {:?}", deps, sdeps); diff --git a/bindings/js/Cargo.toml b/bindings/js/Cargo.toml new file mode 100644 index 00000000..774ae86d --- /dev/null +++ b/bindings/js/Cargo.toml @@ -0,0 +1,19 @@ +[package] +name = "aris-js" +version = "0.1.0" +authors = ["Benjamin Levy "] +edition = "2018" + +[lib] +crate-type = ["cdylib"] + +[dependencies] +aris = { path = "../../aris" } +wasm-bindgen = { version = "0.2.64", features = ["serde-serialize"] } +frunk_core = "0.2.2" +js-sys = "0.3.41" + +# This crate allows propagating `serde` errors with the `?` operator, which is +# safer than `wasm_bindgen::UnwrapThrowExt`, because `UnwrapThrowExt` doesn't +# run destructors and can cause memory leaks. +serde-wasm-bindgen = "0.1.3" \ No newline at end of file diff --git a/bindings/js/src/expression.rs b/bindings/js/src/expression.rs new file mode 100644 index 00000000..82410bad --- /dev/null +++ b/bindings/js/src/expression.rs @@ -0,0 +1,32 @@ +use crate::JsResult; + +use aris::expression::Expr; + +use std::collections::HashSet; + +use serde_wasm_bindgen::from_value; +use serde_wasm_bindgen::to_value; +use wasm_bindgen::prelude::*; + +#[wasm_bindgen] +pub fn freevars(expr: JsValue) -> JsResult { + let expr: Expr = from_value(expr)?; + let vars = aris::expression::freevars(&expr); + let vars = to_value(&vars)?; + Ok(vars) +} + +#[wasm_bindgen] +pub fn gensym(orig: &str, avoid: JsValue) -> JsResult { + let avoid: HashSet = from_value(avoid)?; + Ok(aris::expression::gensym(orig, &avoid)) +} + +#[wasm_bindgen] +pub fn subst(expr: JsValue, to_replace: &str, with: JsValue) -> JsResult { + let expr: Expr = from_value(expr)?; + let with: Expr = from_value(with)?; + let ret = aris::expression::subst(&expr, to_replace, with); + let ret = to_value(&ret)?; + Ok(ret) +} diff --git a/bindings/js/src/lib.rs b/bindings/js/src/lib.rs new file mode 100644 index 00000000..88b4e6b1 --- /dev/null +++ b/bindings/js/src/lib.rs @@ -0,0 +1,7 @@ +use wasm_bindgen::prelude::*; + +pub mod expression; +pub mod parser; +pub mod proofs; + +pub type JsResult = Result; diff --git a/bindings/js/src/parser.rs b/bindings/js/src/parser.rs new file mode 100644 index 00000000..0fd90033 --- /dev/null +++ b/bindings/js/src/parser.rs @@ -0,0 +1,16 @@ +use crate::JsResult; + +use serde_wasm_bindgen::to_value; +use wasm_bindgen::prelude::*; + +#[wasm_bindgen] +pub fn parse(input: &str) -> JsResult { + let ret = aris::parser::parse(input).ok_or("aris: parse error")?; + let ret = to_value(&ret)?; + Ok(ret) +} + +#[wasm_bindgen] +pub fn prettify_expr(s: &str) -> String { + aris::parser::prettify_expr(s) +} diff --git a/bindings/js/src/proofs.rs b/bindings/js/src/proofs.rs new file mode 100644 index 00000000..c0624d9d --- /dev/null +++ b/bindings/js/src/proofs.rs @@ -0,0 +1,315 @@ +use crate::JsResult; + +use aris::expression::Expr; +use aris::proofs::pooledproof::JustKey; +use aris::proofs::pooledproof::PremKey; +use aris::proofs::pooledproof::SubKey; +use aris::proofs::JSRef; +use aris::proofs::Justification; +use aris::proofs::PJRef; +use aris::proofs::PJSRef; +use aris::proofs::Proof as ProofT; + +use std::collections::HashSet; + +use frunk_core::Coprod; +use frunk_core::Hlist; +use serde_wasm_bindgen::from_value; +use serde_wasm_bindgen::to_value; +use wasm_bindgen::prelude::*; + +type P = aris::proofs::pooledproof::PooledProof; +type SP = aris::proofs::pooledproof::PooledSubproof; + +#[wasm_bindgen] +pub struct Proof(P); + +#[wasm_bindgen] +impl Proof { + pub fn new() -> Self { + Self(P::new()) + } + + pub fn top_level_proof(&self) -> Subproof { + Subproof(self.0.top_level_proof().clone()) + } + + pub fn lookup_premise(&self, r: JsValue) -> JsResult { + let r: PremKey = from_value(r)?; + let ret = self + .0 + .lookup_premise(&r) + .ok_or("aris: failed looking up premise")?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_step(&self, r: JsValue) -> JsResult { + let r: JustKey = from_value(r)?; + let ret = self + .0 + .lookup_step(&r) + .ok_or("aris: failed looking up step")?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_subproof(&self, r: JsValue) -> JsResult { + let r: SubKey = from_value(r)?; + let ret = self + .0 + .lookup_subproof(&r) + .ok_or("aris: failed looking up subproof")?; + Ok(Subproof(ret)) + } + + pub fn with_premise(&mut self, r: JsValue, f: js_sys::Function) -> JsResult { + let r: PremKey = from_value(r)?; + let f = |expr: &mut Expr| -> JsResult { + let expr = to_value(&expr)?; + f.call1(&JsValue::NULL, &expr) + }; + let ret = self.0.with_mut_premise(&r, f); + let ret = ret.ok_or("aris: premise not found")?; + ret + } + + pub fn with_step(&mut self, r: JsValue, f: js_sys::Function) -> JsResult { + let r: JustKey = from_value(r)?; + let f = |just: &mut Justification, SubKey>| -> JsResult { + let just = to_value(&just)?; + f.call1(&JsValue::NULL, &just) + }; + let ret = self.0.with_mut_step(&r, f); + let ret = ret.ok_or("aris: step not found")?; + ret + } + + pub fn with_subproof(&mut self, r: JsValue, f: js_sys::Function) -> JsResult { + let r: SubKey = from_value(r)?; + let f = |subproof: &mut SP| -> JsResult { + let subproof = Subproof(subproof.clone()); + let subproof = JsValue::from(subproof); + f.call1(&JsValue::NULL, &subproof) + }; + let ret = self.0.with_mut_subproof(&r, f); + let ret = ret.ok_or("aris: step not found")?; + ret + } + + pub fn add_premise(&mut self, expr: JsValue) -> JsResult { + let expr: Expr = from_value(expr)?; + let ret = self.0.add_premise(expr); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn add_subproof(&mut self) -> JsResult { + let ret = self.0.add_subproof(); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn add_step(&mut self, just: JsValue) -> JsResult { + let just: Justification, SubKey> = from_value(just)?; + let ret = self.0.add_step(just); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn add_premise_relative( + &mut self, + expr: JsValue, + r: JsValue, + after: bool, + ) -> JsResult { + let expr: Expr = from_value(expr)?; + let r: PremKey = from_value(r)?; + let ret = self.0.add_premise_relative(expr, &r, after); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn add_subproof_relative(&mut self, r: JsValue, after: bool) -> JsResult { + let r: JSRef

= from_value(r)?; + let ret = self.0.add_subproof_relative(&r, after); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn add_step_relative( + &mut self, + just: JsValue, + r: JsValue, + after: bool, + ) -> JsResult { + let just: Justification, SubKey> = from_value(just)?; + let r: JSRef

= from_value(r)?; + let ret = self.0.add_step_relative(just, &r, after); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn remove_line(&mut self, r: JsValue) -> JsResult<()> { + let r: PJRef

= from_value(r)?; + self.0.remove_line(&r); + Ok(()) + } + + pub fn remove_subproof(&mut self, r: JsValue) -> JsResult<()> { + let r: SubKey = from_value(r)?; + self.0.remove_subproof(&r); + Ok(()) + } + + pub fn premises(&self) -> JsResult> { + let ret = self + .0 + .premises() + .into_iter() + .map(|prem_key: PremKey| to_value(&prem_key)) + .collect::, _>>()?; + Ok(ret) + } + + pub fn lines(&self) -> JsResult> { + let ret = self + .0 + .lines() + .into_iter() + .map(|js_ref: JSRef

| to_value(&js_ref)) + .collect::, _>>()?; + Ok(ret) + } + + pub fn parent_of_line(&self, r: JsValue) -> JsResult { + let r: PJSRef

= from_value(r)?; + let ret = self.0.parent_of_line(&r); + let ret = ret.ok_or("aris: failed getting parent of line")?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn verify_line(&self, r: JsValue) -> JsResult<()> { + let r: PJRef

= from_value(r)?; + self.0.verify_line(&r).map_err(|err| err.to_string())?; + Ok(()) + } + + pub fn lookup_expr(&self, r: JsValue) -> JsResult { + let r: PJRef

= from_value(r)?; + let ret = self + .0 + .lookup_expr(&r) + .ok_or("aris: failed looking up expression")?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_expr_or_die(&self, r: JsValue) -> JsResult { + let r: PJRef

= from_value(r)?; + let ret = self + .0 + .lookup_expr_or_die(&r) + .map_err(|err| err.to_string())?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_premise_or_die(&self, r: JsValue) -> JsResult { + let r: PremKey = from_value(r)?; + let ret = self + .0 + .lookup_premise_or_die(&r) + .map_err(|err| err.to_string())?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_justification_or_die(&self, r: JsValue) -> JsResult { + let r: JustKey = from_value(r)?; + let ret = self + .0 + .lookup_justification_or_die(&r) + .map_err(|err| err.to_string())?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_pj(&self, r: JsValue) -> JsResult { + let r: PJRef

= from_value(r)?; + let ret = self + .0 + .lookup_pj(&r) + .ok_or("aris: failed looking up premise or justification")?; + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn lookup_subproof_or_die(&self, r: JsValue) -> JsResult { + let r: SubKey = from_value(r)?; + let ret = self + .0 + .lookup_subproof_or_die(&r) + .map_err(|err| err.to_string())?; + Ok(Subproof(ret)) + } + + pub fn direct_lines(&self) -> JsResult> { + let ret = self + .0 + .direct_lines() + .into_iter() + .map(|just_key: JustKey| to_value(&just_key)) + .collect::, _>>()?; + Ok(ret) + } + + pub fn exprs(&self) -> JsResult> { + let ret = self + .0 + .exprs() + .into_iter() + .map(|pj_ref: PJRef

| to_value(&pj_ref)) + .collect::, _>>()?; + Ok(ret) + } + + pub fn contained_justifications(&self, include_premises: bool) -> JsResult { + let ret = self.0.contained_justifications(include_premises); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn transitive_dependencies(&self, line: JsValue) -> JsResult { + let line: PJRef

= from_value(line)?; + let ret = self.0.transitive_dependencies(line); + let ret = to_value(&ret)?; + Ok(ret) + } + + pub fn depth_of_line(&self, r: JsValue) -> JsResult { + let r: PJSRef

= from_value(r)?; + let ret = self.0.depth_of_line(&r); + Ok(ret) + } + + pub fn possible_deps_for_line(&self, r: JsValue) -> JsResult { + let r: PJRef

= from_value(r)?; + let mut deps = HashSet::new(); + let mut sdeps = HashSet::new(); + self.0.possible_deps_for_line(&r, &mut deps, &mut sdeps); + let ret = to_value(&(deps, sdeps))?; + Ok(ret) + } + + pub fn can_reference_dep(&self, r1: JsValue, r2: JsValue) -> JsResult { + let r1: PJRef

= from_value(r1)?; + let r2: Coprod![PJRef

, SubKey] = from_value(r2)?; + let ret = self.0.can_reference_dep(&r1, &r2); + Ok(ret) + } +} + +#[wasm_bindgen] +pub struct Subproof(SP); diff --git a/web-app/Cargo.toml b/web-app/Cargo.toml index 77725616..0ee0057a 100644 --- a/web-app/Cargo.toml +++ b/web-app/Cargo.toml @@ -12,7 +12,7 @@ wasm-bindgen = "^0.2" wee_alloc = "0.4" js-sys = "0.3" web-sys = { version = "0.3", features = ["HtmlAnchorElement"] } -frunk = "0.2.2" +frunk_core = "0.2.2" strum = "0.18.0" [lib] diff --git a/web-app/src/components/proof_widget.rs b/web-app/src/components/proof_widget.rs index 4f805228..4cf6e070 100644 --- a/web-app/src/components/proof_widget.rs +++ b/web-app/src/components/proof_widget.rs @@ -18,8 +18,8 @@ use std::collections::BTreeSet; use std::fmt; use std::mem; -use frunk::Coprod; -use frunk::Coproduct; +use frunk_core::Coprod; +use frunk_core::coproduct::Coproduct; use strum::IntoEnumIterator; use yew::prelude::*; @@ -51,7 +51,7 @@ pub enum LineActionKind { Delete { what: LAKItem }, SetRule { rule: Rule }, Select, - ToggleDependency { dep: frunk::Coproduct, frunk::Coproduct<

::SubproofReference, frunk::coproduct::CNil>> }, + ToggleDependency { dep: Coprod![PJRef

,

::SubproofReference] }, } pub enum ProofWidgetMsg { @@ -87,7 +87,7 @@ impl ProofWidget { None => "".to_string(), }; if let Some(selected_line) = self.selected_line { - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; if let Inr(Inl(_)) = selected_line { let dep = proofref.clone(); let selected_line_ = selected_line.clone(); @@ -256,8 +256,8 @@ impl ProofWidget { } } fn render_proof_line(&self, line: usize, depth: usize, proofref: PJRef

, edge_decoration: &str) -> Html { - use frunk::Coproduct::{Inl, Inr}; - let line_num_dep_checkbox = self.render_line_num_dep_checkbox(Some(line), frunk::Coproduct::inject(proofref.clone())); + use Coproduct::{Inl, Inr}; + let line_num_dep_checkbox = self.render_line_num_dep_checkbox(Some(line), Coproduct::inject(proofref.clone())); let mut indentation = yew::virtual_dom::VList::new(); for _ in 0..depth { //indentation.add_child(html! { {"-"}}); @@ -422,7 +422,7 @@ impl ProofWidget { *line += 1; } let dep_checkbox = match sref { - Some(sr) => self.render_line_num_dep_checkbox(None, frunk::Coproduct::inject(sr)), + Some(sr) => self.render_line_num_dep_checkbox(None, Coproduct::inject(sr)), None => yew::virtual_dom::VNode::from(yew::virtual_dom::VList::new()), }; let mut spacer = yew::virtual_dom::VList::new(); @@ -440,7 +440,7 @@ impl ProofWidget { output.push((spacer, false)); let prf_lines = prf.lines(); for (i, lineref) in prf_lines.iter().enumerate() { - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; let edge_decoration = if i == prf_lines.len()-1 { box_chars::UP_RIGHT } else { box_chars::VERT }.to_string(); match lineref { Inl(r) => { output.push((self.render_proof_line(*line, *depth, Coproduct::inject(r.clone()), &edge_decoration), false)); *line += 1; }, @@ -477,7 +477,7 @@ impl ProofWidget { } fn may_remove_line(prf: &P, proofref: &PJRef

) -> bool { - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; let is_premise = match prf.lookup_pj(proofref) { Some(Inl(_)) => true, Some(Inr(Inl(_))) => false, @@ -546,7 +546,7 @@ impl Component for ProofWidget { self.preblob += &format!("{:?}\n", msg); ret = true; } - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; match msg { ProofWidgetMsg::Nop => {}, ProofWidgetMsg::LineChanged(r, input) => { diff --git a/web-app/src/proof_ui_data.rs b/web-app/src/proof_ui_data.rs index 9161550c..e74d6da1 100644 --- a/web-app/src/proof_ui_data.rs +++ b/web-app/src/proof_ui_data.rs @@ -6,7 +6,7 @@ use aris::proofs::Proof; use std::collections::HashMap; -use frunk::Coproduct; +use frunk_core::coproduct::Coproduct; pub struct ProofUiData { pub ref_to_line_depth: HashMap, (usize, usize)>, @@ -31,7 +31,7 @@ impl ProofUiData

{ fn initialize_inputs(prf: &P) -> HashMap, String> { fn aux(p: &

::Subproof, out: &mut HashMap, String>) { - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; for line in p .premises() .into_iter() diff --git a/web-app/src/util.rs b/web-app/src/util.rs index 6d6a2a9c..caa2250e 100644 --- a/web-app/src/util.rs +++ b/web-app/src/util.rs @@ -5,8 +5,8 @@ use aris::proofs::Proof; use std::collections::HashMap; -use frunk::Coproduct; -use frunk::Hlist; +use frunk_core::coproduct::Coproduct; +use frunk_core::Hlist; // yew doesn't seem to allow Components to be generic over , so fix a proof type P at the module level pub type P = PooledProof; @@ -22,7 +22,7 @@ pub fn calculate_lineinfo( *line += 1; } for lineref in prf.lines() { - use frunk::Coproduct::{Inl, Inr}; + use Coproduct::{Inl, Inr}; match lineref { Inl(r) => { output.insert(Coproduct::inject(r), (*line, *depth));