change Subsmap to map to Partial.Expr (#362)

Signed-off-by: Craig Disselkoen <[email protected]>

cedar-lean/Cedar/Partial/Request.lean

@@ -71,18 +71,18 @@ open Cedar.Data
 open Cedar.Spec (EntityUID)
 
 /--
-  Given a map of unknown-name to value, substitute the unknown in `UidOrUnknown`
-  if possible. If the `UidOrUnknown` is already known, or it's an unknown that doesn't
-  have a mapping in `subsmap`, return it unchanged.
+  Given a `Subsmap`, substitute the unknown in `UidOrUnknown` if possible. If
+  the `UidOrUnknown` is already known, or it's an unknown that doesn't have a
+  mapping in `subsmap`, return it unchanged.
 
   Returns `none` if the substitution is invalid -- e.g., if trying to substitute
   a non-`EntityUID` into `UidOrUnknown`.
 -/
 def UidOrUnknown.subst (subsmap : Subsmap) : UidOrUnknown → Option UidOrUnknown
   | .known uid => some (.known uid)
   | .unknown unk => match subsmap.m.find? unk with
-    | some (.value (.prim (.entityUID uid))) => some (.known uid)
-    | some (.residual (.unknown unk')) => some (.unknown unk') -- substituting an unknown with another unknown, we'll allow it
+    | some (.lit (.entityUID uid)) => some (.known uid)
+    | some (.unknown unk') => some (.unknown unk') -- substituting an unknown with another unknown, we'll allow it
     | none => some (.unknown unk) -- no substitution available, return `unk` unchanged
     | _ => none -- substitution is not for a literal UID or literal unknown. Not valid, return none
 

cedar-lean/Cedar/Partial/Value.lean

@@ -39,10 +39,11 @@ instance : Coe Spec.Value Partial.Value where
   coe := Partial.Value.value
 
 /--
-  Defines a mapping from unknowns to values, for use in a substitution.
+  Defines a mapping from unknowns to the `Partial.Expr`s to replace them with
+  during a substitution.
 -/
 structure Subsmap where
-  m : Map Unknown Partial.Value
+  m : Map Unknown Partial.Expr
 
 /--
   Given a map of unknown-name to value, substitute all unknowns with the
@@ -66,7 +67,7 @@ def Expr.subst (subsmap : Subsmap) : Partial.Expr → Partial.Expr
   | .record pairs => .record (pairs.attach₂.map λ ⟨(k, v), _⟩ => (k, v.subst subsmap))
   | .call xfn xs => .call xfn (xs.map₁ λ ⟨x, _⟩ => x.subst subsmap)
   | .unknown u => match subsmap.m.find? u with
-    | some val => val.asPartialExpr
+    | some x => x
     | none => .unknown u -- no substitution available
 
 /--