Lem code generation
I have created a simple program in Lem.
open import Pervasives
type myList 'a =
| Nil
| Cons of 'a * (myList 'a)
let isNil (l : myList 'a) : bool =
match l with
| Nil -> true
end
let rec myMap (f : 'a -> 'b) (l : myList 'a) : myList 'b =
match l with
| Nil -> Nil
| (Cons x xs) -> Cons (f x) (myMap f xs)
end
The generated Coq code looks like this:
(* Generated by Lem from test.lem. *)
Require Import Arith.
Require Import Bool.
Require Import List.
Require Import String.
Require Import Program.Wf.
Require Import coqharness.
Open Scope nat_scope.
Open Scope string_scope.
Require Import lem_pervasives.
Require Export lem_pervasives.
Inductive myList (a : Type) : Type :=
| Nil: myList a
| Cons: a -> (myList a) -> myList a.
Definition myList_default{a: Type} : myList a := Nil.
Definition isNil {a : Type} (l : myList a) : bool :=
match ( l) with | Nil => true | Cons _ _ =>
bool_default (* Incomplete Pattern at File \"test.lem\", line 8, character 3 to line 10, character 5 *)
end.
Program Fixpoint myMap {a b : Type} (f : b -> a) (l : myList b) : myList a:=
match ( l) with
| Nil => Nil
|( Cons x xs) => Cons (f x) (myMap f xs)
end.
There are a few issues with this code, most likely because Lem supports only Coq 8.4.
- A load path needs to be added to import the Coq libraries that Lem comes with.
- The Coq library imports are missing a
Lem
prefix, e.g.Require Import Lem.lem_pervasives
. - Coq complains about missing type arguments for
Nil
andCons
. - There are some redundant spaces or missing line breaks and the code layout in general isn't as good as I would have expected.
If I don't want to be restricted to Coq 8.4, I would probably need to modify the generated code or add this functionality to Lem. Since the recent development regarding Lem and the Coq translation doesn't seem very active, this is probably rather difficult.
Edited by Niels Bunkenburg