[DRAFT] Dead sam/memoization

Strata/DL/Lambda/Factory.lean

@@ -29,13 +29,16 @@ open Std (ToFormat Format format)
 
 open LTy.Syntax
 
-variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier]
+variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier] [Hashable Identifier]
 
 /--
 A signature is a map from variable identifiers to types.
 -/
 abbrev Signature (Identifier : Type) (Ty : Type) := Map Identifier Ty
 
+instance [Hashable Identifier] [Hashable Ty] : Hashable (Signature Identifier Ty) where
+  hash s := hash s
+
 def Signature.format (ty : Signature Identifier Ty) [Std.ToFormat Ty] : Std.Format :=
   match ty with
   | [] => ""
@@ -45,6 +48,9 @@ def Signature.format (ty : Signature Identifier Ty) [Std.ToFormat Ty] : Std.Form
 
 abbrev LMonoTySignature := Signature Identifier LMonoTy
 
+instance [Hashable Identifier] [Hashable LMonoTy]: Hashable (Signature Identifier LMonoTy) where
+  hash s := hash s
+
 abbrev LTySignature := Signature Identifier LTy
 
 
@@ -90,6 +96,12 @@ structure LFunc (Identifier : Type) where
   denote   : Option ((LExpr Identifier) → List (LExpr Identifier) → (LExpr Identifier)) := .none
   axioms   : List (LExpr Identifier) := []  -- For axiomatic definitions
 
+instance : Hashable (LFunc Identifier) where
+  hash f := hash (f.name, f.typeArgs, f.inputs, f.output, f.body, f.attr, f.axioms)
+
+instance : BEq (LFunc Identifier) where
+  beq a b := a.name == b.name && a.typeArgs == b.typeArgs && a.inputs == b.inputs && a.output == b.output && a.body == b.body && a.attr == b.attr && a.axioms == b.axioms
+
 instance : Inhabited (LFunc Identifier) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }
 
@@ -146,7 +158,14 @@ Identifier)` -- lambdas are our only tool. `Factory` gives us a way to add
 support for concrete/symbolic evaluation and type checking for `FunFactory`
 functions without actually modifying any core logic or the ASTs.
 -/
-def Factory := Array (LFunc Identifier)
+abbrev Factory := Array (LFunc Identifier)
+
+instance [Hashable Identifier] : Hashable (@Factory Identifier) where
+   hash a := hash (a : Array (LFunc Identifier))
+
+instance [BEq Identifier] : BEq (@Factory Identifier) where
+  beq a b := a == b
+
 
 def Factory.default : @Factory Identifier := #[]
 

Strata/DL/Lambda/LExpr.lean

@@ -22,7 +22,7 @@ open Std (ToFormat Format format)
 inductive QuantifierKind
   | all
   | exist
-  deriving Repr, DecidableEq
+  deriving Repr, DecidableEq, Hashable
 
 /--
 Lambda Expressions with Quantifiers.
@@ -57,7 +57,7 @@ inductive LExpr (Identifier : Type) : Type where
   | ite     (c t e : LExpr Identifier)
   /-- `.eq e1 e2`: equality expression. -/
   | eq      (e1 e2 : LExpr Identifier)
-  deriving Repr, DecidableEq
+  deriving Repr, DecidableEq, Hashable
 
 def LExpr.all {Identifier : Type} := @LExpr.quant Identifier .all
 def LExpr.exist {Identifier : Type} := @LExpr.quant Identifier .exist