From 02a3dcb1dd704140005219d897ec80c97db23b4e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Oct 2022 20:34:12 -0700 Subject: [PATCH] feat: hash for `LCNF.Code` --- src/Lean/Compiler/LCNF/CodeMap.lean | 46 +++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 src/Lean/Compiler/LCNF/CodeMap.lean diff --git a/src/Lean/Compiler/LCNF/CodeMap.lean b/src/Lean/Compiler/LCNF/CodeMap.lean new file mode 100644 index 0000000000..1a908c1b43 --- /dev/null +++ b/src/Lean/Compiler/LCNF/CodeMap.lean @@ -0,0 +1,46 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import Lean.Compiler.LCNF.Basic + +namespace Lean.Compiler.LCNF + +instance : Hashable Param where + hash p := mixHash (hash p.fvarId) (hash p.type) + +def hashParams (ps : Array Param) : UInt64 := + hash ps + +mutual +partial def hashAlt (alt : Alt) : UInt64 := + match alt with + | .alt ctorName ps k => mixHash (mixHash (hash ctorName) (hash ps)) (hashCode k) + | .default k => hashCode k + +partial def hashAlts (alts : Array Alt) : UInt64 := + alts.foldl (fun r a => mixHash r (hashAlt a)) 7 + +partial def hashCode (code : Code) : UInt64 := + match code with + | .let decl k => mixHash (mixHash (hash decl.fvarId) (hash decl.type)) (mixHash (hash decl.value) (hashCode k)) + | .fun decl k | .jp decl k => + mixHash (mixHash (mixHash (hash decl.fvarId) (hash decl.type)) (mixHash (hashCode decl.value) (hashCode k))) (hash decl.params) + | .return fvarId => hash fvarId + | .unreach type => hash type + | .jmp fvarId args => mixHash (hash fvarId) (hash args) + | .cases c => mixHash (mixHash (hash c.discr) (hash c.resultType)) (hashAlts c.alts) + +end + +instance : Hashable Code where + hash c := hashCode c + +/-- +Persistent hash map from `Code` to `α`. +Remark: consider using `normalizeFVarIds`. +-/ +abbrev PCodeHashMap (α : Type) := PHashMap Code α + +end Lean.Compiler.LCNF \ No newline at end of file