diff --git a/src/Lean/Elab/ComputedFields.lean b/src/Lean/Elab/ComputedFields.lean index ee47507ff8..dcd7b9d462 100644 --- a/src/Lean/Elab/ComputedFields.lean +++ b/src/Lean/Elab/ComputedFields.lean @@ -135,6 +135,9 @@ def overrideComputedFields : M Unit := do let {name, levelParams, ctors, compFields, compFieldVars, lparams, params, indices, val ..} ← read withLocalDeclD `x (mkAppN (mkConst (name ++ `_impl) lparams) (params ++ indices)) fun xImpl => do for cfn in compFields, cf in compFieldVars do + if isExtern (← getEnv) cfn then + compileDecls [cfn] + continue let cases ← ctors.toArray.mapM fun ctor => do forallTelescope (← inferType (mkAppN (mkConst ctor lparams) params)) fun fields _ => do if ← isScalarField ctor then @@ -199,5 +202,6 @@ def setComputedFields (computedFields : Array (Name × Array Name)) : MetaM Unit for ctor in ind.ctors do toCompile := toCompile.push (ctor ++ `_override) for fieldName in computedFields do - toCompile := toCompile.push <| fieldName ++ `_override + unless isExtern (← getEnv) fieldName do + toCompile := toCompile.push <| fieldName ++ `_override compileDecls toCompile.toList diff --git a/tests/compiler/computedFieldsExtern.lean b/tests/compiler/computedFieldsExtern.lean new file mode 100644 index 0000000000..4e9f8bf2aa --- /dev/null +++ b/tests/compiler/computedFieldsExtern.lean @@ -0,0 +1,12 @@ +inductive Exp + | var (i : Nat) + | app (a b : Exp) +with + @[extern c inline "(lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*)) + 40)"] + hash : Exp → UInt64 + | .var i => Hashable.hash i + | .app a b => a.hash + b.hash + +def main : IO Unit := do + -- should be 30 + 3*40 = 150 + IO.println <| Exp.hash (.app (.var 10) (.var 20)) diff --git a/tests/compiler/computedFieldsExtern.lean.expected.out b/tests/compiler/computedFieldsExtern.lean.expected.out new file mode 100644 index 0000000000..fa8f08cb6f --- /dev/null +++ b/tests/compiler/computedFieldsExtern.lean.expected.out @@ -0,0 +1 @@ +150 diff --git a/tests/compiler/computedFieldsExtern.lean.no_interpreter b/tests/compiler/computedFieldsExtern.lean.no_interpreter new file mode 100644 index 0000000000..e69de29bb2