Skip to content

[michocoq] Fix a bug related to lambdas as part of data

Raphaël Cauderlier requested to merge rafoo@fix_untyped_syntax into dev

Fix isuue #63.

In the concrete syntax, lambdas were only correctly handled by the typer when they appeared at the topmost position in a value (so for example PUSH (lambda nat int) { PUSH int -1; ADD } was accepted but PUSH (pair nat (lambda nat int)) (Pair 0 { PUSH int -1; ADD }) was not). This restriction simplified the mutual dependencies of conversion functions because in the general case data, instructions, and instruction sequences are mutually recursive.

In this commit, we bite the mutual dependency bullet to fix the bug.

Edited by Raphaël Cauderlier

Merge request reports