fixpoints

a bugfix
a test
an example (list/map.who)

Author: Johannes Kanig

list/map.who

@@ -1,4 +1,8 @@
-logic List.length ['a] : 'a list -> int
+fixpoint List.length ['a] (l : 'a list) : int =
+  match l with
+  | Nil -> 0
+  | Cons (x,xs) -> 1 + List.length xs
+  end
 
 let rec List.map ['a 'b||'e]
   (ia : <'e> -> 'a list -> prop) (ib : <'e> -> <'e> -> 'b list -> prop)
@@ -35,4 +39,4 @@ let test2 (l : int list) =
   let f ( _ : int) =
     {} r := !r + 1; !r { res : res = !!r /\ !!r = !!r@old + 1 } in
   List.map [{t}] ia ib f l
-  { res: l_incr res 1 (List.length res) }
+  { res: l_incr res 1 (List.length l) }

src/parser/recon.ml

@@ -172,12 +172,13 @@ let rec recon_decl x =
         let f =
           let v = mk_var_with_scheme false fix n (g,t) in
           var v (Ty.Generalize.to_inst g) l in
+        let e = subst n (fun _ -> f) e in
         let fapp = List.fold_left (fun acc t -> app acc t l) f tl in
         let def = eq fapp e l in
         List.fold_left (fun acc (x,t) -> sforall x t acc l) def acc in
       [
         Logic (n,(g,t));
-        Formula (Name.append n "def", form, `Assumed)
+        Formula (Name.append n "def", gen g form l, `Assumed)
       ]
 
   | I.Inductive (n,g,t,tel) ->

tests/good/parsing/fixpoint.expected

@@ -0,0 +1,9 @@
+type list ['a||] = | Nil | Cons of a* list[a] 
+logic +  : int -> int -> int
+logic = ['a||] : a -> a -> prop
+logic List_length ['a||] : list[a] -> int
+axiom List_lengthdef:
+  forall ['a||]. forall (l:list[a]).
+                 (List_length [a||] l) =
+                 (match l with Nil ->  0  | Cons(x,xs) ->
+                                1 + (List_length [a||] xs)  end ) 

tests/good/parsing/fixpoint.who

@@ -0,0 +1,13 @@
+type list['a] =
+| Nil
+| Cons of 'a * 'a list
+
+logic + : int -> int -> int
+
+logic = ['a] : 'a -> 'a -> prop
+
+fixpoint List.length ['a] (l : 'a list) : int =
+  match l with
+  | Nil -> 0
+  | Cons (x,xs) -> 1 + List.length xs
+  end