From 3b944d15c80daa01baac262fdc29cc2207bf429b Mon Sep 17 00:00:00 2001 From: Michael Sippel Date: Mon, 2 Oct 2023 19:16:20 +0200 Subject: [PATCH] add more subtype test-cases & fix normalize in case of normalizing sub-ladders --- src/lnf.rs | 15 +++++++++++---- src/test/subtype.rs | 21 +++++++++++++++++++++ 2 files changed, 32 insertions(+), 4 deletions(-) diff --git a/src/lnf.rs b/src/lnf.rs index f8b3ad9..9e38aea 100644 --- a/src/lnf.rs +++ b/src/lnf.rs @@ -31,7 +31,16 @@ impl TypeTerm { match self { TypeTerm::Ladder(args) => { for x in args.into_iter() { - new_ladder.push(x.normalize()); + match x.normalize() { + TypeTerm::Ladder(gs) => { + for g in gs { + new_ladder.push(g); + } + } + g => { + new_ladder.push(g); + } + } } } @@ -102,9 +111,7 @@ impl TypeTerm { TypeTerm::Ladder( v ) => { v }, - _ => { - unreachable!(); - } + flat => vec![ flat ] } } } diff --git a/src/test/subtype.rs b/src/test/subtype.rs index 836b492..54ad397 100644 --- a/src/test/subtype.rs +++ b/src/test/subtype.rs @@ -72,5 +72,26 @@ fn test_syntactic_subtype() { ), Err(None) ); + + assert_eq!( + dict.parse("~ℕ").expect("parse error") + .is_syntactic_subtype_of( + &dict.parse("ℕ").expect("parse errror") + ), + Ok(1) + ); + + assert_eq!( + dict.parse(" + +~ℕ +~ +~< Seq ~ Char >" + ).expect("parse error") + .is_syntactic_subtype_of( + &dict.parse("").expect("parse errror") + ), + Ok(4) + ); }