nachivpn

module STLCBetaWHNF where

open import Data.Sum
open import Data.Unit using (⊤ ; tt)
open import Data.Product

--------------------
-- Term syntax, etc.
--------------------

nachivpn

Master's Courses

• Types for Proofs and Programs (Chalmers/GU, LP1): https://chalmers.instructure.com/courses/7445
• Formal Methods in Software Development (Chalmers/GU, LP1): https://chalmers.instructure.com/courses/7577
• Category Theory (Chalmers/GU, LP2): https://wiki.portal.chalmers.se/cse/pmwiki.php/ProgLog/CTFP20
• Introduction to set theory (GU, LP1): https://www.gu.se/en/study-gothenburg/introduction-to-set-theory-log010
• Logical theory (GU, LP1-2): https://www.gu.se/en/study-gothenburg/logical-theory-log111
• Modal Logic (GU, LP2): https://www.gu.se/en/study-gothenburg/modal-logic-log131
• Proof theory (GU, LP3): https://www.gu.se/en/study-gothenburg/proof-theory-log221

nachivpn

¬[_] : ∀ {a b : Name} → Dec (a ≡ b) → Set
¬[ (yes x₁) ] = ⊥
¬[ (no x₁) ] = ⊤

data _,_∈x_ (n : Name) (p : Pointer) : Env → Set where
  zero : ∀ {xs}            → n , p ∈x ((n , p) ∷ xs)
  suc  : ∀ {n' : Name}  { p' : Pointer} {xs} {pr : ¬[  n == n'  ]}
    → n , p ∈x xs → n , p ∈x ((n' , p') ∷ xs)
    
private

nachivpn

-- scope sensitive belongs
-- Unlike ∈, it does not allow scope insensitive proof of belongs
_∈s_ : (Name × Pointer) → Env → Set
(n , p) ∈s [] = ⊥
(n , p) ∈s ((n' , p') ∷ ρ') with n ==n n' | p ==n p'
... | false | _     = ( n , p ) ∈s ρ'
... | _     | false = ⊥
... | true  | true  = ⊤

private

nachivpn

public final static class Left<LL, LR> extends Either<LL, LR>{
    LL l;
    public Left(LL l) {
        this.l = l;
    }
    @Override
    public <T> T match(Function<LL, T> a, Function<LR, T> b) {
        return a.apply(l);
    }
    @Override

nachivpn

public static void main(String args[]){
	//bike product
	Map<String,List<String>> productDetails = new HashMap<>();
	List<String> bikeComponentNames = new ArrayList<>();
	bikeComponentNames.add("wheel");
	bikeComponentNames.add("wheel");
	bikeComponentNames.add("frame");
	productDetails.put("bike", bikeComponentNames);

	//componets

nachivpn

Map<String,Component> components;
public List<String> getComponentNames(String product){
  return productDetails.get(product);
}
//given a product, return the sum of prices of it's components
//if anything fails, return that specific exception
public Either<Exception,Double> getProductPrice(String product){
	return getComponentNames(product)
		.stream()
			//from product name string, get componenet as Either<Exception,Component>

nachivpn

//return component price from Either<Exception, Component>, but if any step fails, return exception which occured
public Either<Exception,Double> getComponentPrice(Either<Exception, Component> response){
	return response
			//extract component id
		.fmap(result -> result.getId())
			//find price
		.bind(this::findOriginalPrice)
			//apply discount if applicable
		.fmap(this::discountedPrice);
}

nachivpn

Double discount;
//apply discount to a given price and return discounted price
public Double discountedPrice(Double originalPrice){
	Optional<Double> optionalDiscount = Optional.ofNullable(discount);
	return optionalDiscount
		.map(discount -> originalPrice - originalPrice * discount)
		.orElse(originalPrice);
}

nachivpn

//return the price of component in Either<Exception, Component> if price is available, else return exception
public Either<Exception,Double> getComponentPrice(Either<Exception, Component> response){
    return response.bind(result -> findOriginalPrice(result.getId()));
}