Support inheritance (#459)

### Changes
- Change naming scheme so the name `$heap` is always used as the heap to
read/assign to in the body. For read-only procedures, `$heap` is the
input parameter as well as the one to read. For read/write procedures,
`$heap` is the out parameter and `$heap_in` the input one.
- Add a `Map.const` function to the Core factory
- Add datatypes to Laurel, to support a more incremental translation to
Core
- During translation, introduce a `Field` datatype that has a
constructor for each user defined field.
- During translation, introduce a `UserType` datatype that has a
constructor for each user defined type.
- Support composites that have fields with the same name but different
types
- Move the handling of `new` from HeapParameterization to a new pass
`TypeHierarchy`, that also handles `<value> as <Type>` and `<value> is
<Type>`.

### Testing
- Add a test `sameFieldNameDifferentType` to the mutable fields test
file
- Added a test file related to inheritance

Author: keyboardDrummer

Strata/Languages/Core/Factory.lean

@@ -220,6 +220,21 @@ def reNoneFunc : WFLFunc CoreLParams :=
 def polyOldFunc : WFLFunc CoreLParams :=
   polyUneval "old" ["a"] [("x", mty[%a])] mty[%a]
 
+/- A constant `Map` constructor with type `∀k, v. v → Map k v`.
+   `Map.const(d)` returns a map where every key maps to the value `d`. -/
+def mapConstFunc : WFLFunc CoreLParams :=
+  polyUneval "Map.const" ["k", "v"]
+    [("d", mty[%v])]
+    (mapTy mty[%k] mty[%v])
+    (axioms := [
+      ToCoreIdent esM[∀ (%v): -- %1 d
+          (∀ (%k): -- %0 kk
+            {(((~select : (Map %k %v) → %k → %v)
+                ((~Map.const : %v → (Map %k %v)) %1)) %0)}
+            (((~select : (Map %k %v) → %k → %v)
+                ((~Map.const : %v → (Map %k %v)) %1)) %0) == %1)]
+    ])
+
 /- A `Map` selection function with type `∀k, v. Map k v → k → v`. -/
 def mapSelectFunc : WFLFunc CoreLParams :=
   polyUneval "select" ["k", "v"]
@@ -359,6 +374,7 @@ def WFFactory : Lambda.WFLFactory CoreLParams :=
 
   polyOldFunc,
 
+  mapConstFunc,
   mapSelectFunc,
   mapUpdateFunc,
 
@@ -464,6 +480,7 @@ def reInterOp : Expression.Expr := reInterFunc.opExpr
 def reCompOp : Expression.Expr := reCompFunc.opExpr
 def reNoneOp : Expression.Expr := reNoneFunc.opExpr
 def polyOldOp : Expression.Expr := polyOldFunc.opExpr
+def mapConstOp : Expression.Expr := mapConstFunc.opExpr
 def mapSelectOp : Expression.Expr := mapSelectFunc.opExpr
 def mapUpdateOp : Expression.Expr := mapUpdateFunc.opExpr
 

Strata/Languages/Laurel/CorePrelude.lean

@@ -28,9 +28,15 @@ def corePreludeDDM :=
 #strata
 program Core;
 
-// Abstract types for the heap model
+// Field and TypeTag are declared as an opaque type for DDM resolution to pass; the Laurel translator
+// replaces them with datatypes that contain one constructor for each field and composite type
 type Field;
-type Composite := int;
+type TypeTag;
+
+// Composite is a datatype with a reference (int) and a runtime type tag
+datatype Composite () {
+  MkComposite(ref: int, typeTag: TypeTag)
+};
 
 // Tagged union for field values
 datatype Box () {

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -206,6 +206,14 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.new, #[nameArg] =>
       let name ← translateIdent nameArg
       return mkStmtExprMd (.New name) md
+    | q`Laurel.isType, #[targetArg, typeNameArg] =>
+      let target ← translateStmtExpr targetArg
+      let typeName ← translateIdent typeNameArg
+      return mkStmtExprMd (.IsType target (mkHighTypeMd (.UserDefined typeName) md)) md
+    | q`Laurel.asType, #[targetArg, typeNameArg] =>
+      let target ← translateStmtExpr targetArg
+      let typeName ← translateIdent typeNameArg
+      return mkStmtExprMd (.AsType target (mkHighTypeMd (.UserDefined typeName) md)) md
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee.val with
@@ -230,7 +238,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExprMd := do
     | q`Laurel.fieldAccess, #[objArg, fieldArg] =>
       let obj ← translateStmtExpr objArg
       let field ← translateIdent fieldArg
-      return mkStmtExprMd (.FieldSelect obj field) md
+      let fieldMd ← getArgMetaData fieldArg
+      return mkStmtExprMd (.FieldSelect obj field) fieldMd
     | q`Laurel.while, #[condArg, invSeqArg, bodyArg] =>
       let cond ← translateStmtExpr condArg
       let invariants ← match invSeqArg with
@@ -400,12 +409,21 @@ def parseComposite (arg : Arg) : TransM TypeDefinition := do
   let .op op := arg
     | TransM.error s!"parseComposite expects operation"
   match op.name, op.args with
-  | q`Laurel.composite, #[nameArg, fieldsArg] =>
+  | q`Laurel.composite, #[nameArg, extendsArg, fieldsArg] =>
     let name ← translateIdent nameArg
+    let extending ← match extendsArg with
+      | .option _ (some (.op extendsOp)) => match extendsOp.name, extendsOp.args with
+        | q`Laurel.optionalExtends, #[parentsArg] =>
+          match parentsArg with
+          | .seq _ .comma args => args.toList.mapM translateIdent
+          | singleArg => do let parent ← translateIdent singleArg; pure [parent]
+        | _, _ => TransM.error s!"Expected optionalExtends operation, got {repr extendsOp.name}"
+      | .option _ none => pure []
+      | _ => TransM.error s!"Expected optionalExtends, got {repr extendsArg}"
     let fields ← match fieldsArg with
       | .seq _ _ args => args.toList.mapM parseField
       | _ => pure []
-    return .Composite { name := name, extending := [], fields := fields, instanceProcedures := [] }
+    return .Composite { name := name, extending := extending, fields := fields, instanceProcedures := [] }
   | _, _ =>
     TransM.error s!"parseComposite expects composite, got {repr op.name}"
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -94,8 +94,16 @@ category Field;
 op mutableField (name: Ident, fieldType: LaurelType): Field => "var " name ":" fieldType;
 op immutableField (name: Ident, fieldType: LaurelType): Field => name ":" fieldType;
 
+// Type checking and casting
+op isType (target: StmtExpr, typeName: Ident): StmtExpr => @[prec(40)] target " is " typeName;
+op asType (target: StmtExpr, typeName: Ident): StmtExpr => @[prec(40)] target " as " typeName;
+
+// Composite types with optional extends
+category OptionalExtends;
+op optionalExtends(parents: CommaSepBy Ident): OptionalExtends => "extends " parents;
+
 category Composite;
-op composite (name: Ident, fields: Seq Field): Composite => "composite " name "{" fields "}";
+op composite (name: Ident, extending: Option OptionalExtends, fields: Seq Field): Composite => "composite " name extending "{" fields "}";
 
 // Procedures
 category OptionalReturnType;