From 56cfc3d275d99cd4c96b79bfe6c004b9da3dde62 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Tue, 10 Dec 2013 15:09:59 +0100 Subject: [PATCH] Extraction of List. append, reverse, length new theory HdTlNoOpt --- drivers/ocaml.drv | 13 +++++++++++++ theories/list.why | 16 +++++++++++++++- 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/drivers/ocaml.drv b/drivers/ocaml.drv index 126a04ad0..37d2a5e0a 100644 --- a/drivers/ocaml.drv +++ b/drivers/ocaml.drv @@ -38,6 +38,19 @@ theory list.List syntax function Cons "((%1) :: (%2))" end +theory list.Length + syntax function length "(List.length (%1))" +end + +theory list.Append + syntax function (++) "(List.append (%1) (%2))" +end + +theory list.Reverse + syntax function reverse "(List.rev (%1))" +end + + (* WhyML *) diff --git a/theories/list.why b/theories/list.why index 5a8c72dd6..afebed0c5 100644 --- a/theories/list.why +++ b/theories/list.why @@ -77,7 +77,7 @@ theory NthNoOpt use export List use import int.Int - function nth (n: int) (l: list 'a) : 'a + function nth (n: int) (l: list 'a) : 'a axiom nth_cons_0: forall x:'a, r:list 'a. nth 0 (Cons x r) = x axiom nth_cons_n: forall x:'a, r:list 'a, n:int. @@ -121,6 +121,20 @@ theory HdTl end +theory HdTlNoOpt + + use export List + + function hd (l: list 'a) : 'a + + axiom hd_cons: forall x:'a, r:list 'a. hd (Cons x r) = x + + function tl (l: list 'a) : list 'a + + axiom tl_cons: forall x:'a, r:list 'a. tl (Cons x r) = r + +end + (** {2 Relation between head, tail, and nth} *) theory NthHdTl -- GitLab