;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; 2013-06-12.  listrev.scm.  Example for translation into Haskell.

; (load "~/minlogsvn/init.scm")

;; Loading libraries for nat and list
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(libload "list.scm")
(set! COMMENT-FLAG #t)

;; (add-alg "nat"
;;          '("Zero" "nat")
;;          '("Succ" "nat=>nat"))

;; (add-alg "list"
;; 	    '("Nil" "list")
;; 	    '("Cons" "alpha=>list=>list"))

;; preparing variables
(remove-var-name "n" "m" "k")
(add-var-name "x" "y" "n" "m" "k" (py "nat"))
(add-var-name "v" "w" "u" (py "list nat"))

; inductively defined predicate A (see the slide)
(add-ids
 (list (list "A" (make-arity (py "list nat") (py "list nat") (py "list nat"))))
 '("all v^ A(Nil nat)v^ v^" "InitA")
 '("all u^,v^,w^,x^(A u^ v^ w^ -> A(x^ ::u^)v^(x^ ::w^))" "GenA"))

;; (display-idpc "A")

;; LA
(set-goal "all v,u ex w A u v w")
(assume "v")
(ind)
;; Base
(ex-intro (pt "v"))
(use "InitA")
;; Step
(assume "x" "u" "IHu")
(by-assume "IHu" "w" "wProp")
(ex-intro (pt "x::w"))
(use "GenA")
(use "wProp")
;; Proof finished.
(save "LA")

; inductive predicate R (see the slide)
(add-ids
 (list (list "R" (make-arity (py "list nat") (py "list nat"))))
 '("R(Nil nat)(Nil nat)" "InitR")
 '("all v^,w^,w^1,x^(R v^ w^ -> A w^(x^ :)w^1 -> R(x^ ::v^)w^1)" "GenR"))

;; (display-idpc "R")

;; LR
; using the lemma LA
(set-goal "all v ex w R v w")
(ind)
;; Base
(ex-intro (pt "(Nil nat)"))
(use "InitR")
;; Step
(assume "x" "v" "IHv")
(by-assume "IHv" "w" "wProp")
(assert "ex w1 A w(x:)w1")
(use "LA")
(assume "ExHyp")
(by-assume "ExHyp" "w1" "w1Prop")
(ex-intro (pt "w1"))
(use "GenR" (pt "w"))
(use "wProp")
(use "w1Prop")
;; Proof finished.
(save "LR")

; extracting a program form the proof
(define eterm (proof-to-extracted-term (theorem-name-to-proof "LR")))

;; tell Minlog to use computatinal content from propositions
(animate "LR")
(animate "LA")

;; printing the extracted term (see the slide)
(pp (nt eterm))

(display-pconst "cLR" "cLA")

;; cLR
;;   comprules
;; 	cLR	[v0](Rec list nat=>list nat)v0(Nil nat)([x1,v2]cLA x1:)
;; cLA
;;   comprules
;; 	cLA	[v0,v1](Rec list nat=>list nat)v1 v0([x2,v3](Cons nat)x2)

(terms-to-haskell-program "listrev.hs"
			  (list (list (pt "cLR") "rev")
				(list (pt "cLA") "apd")))

;; module Main where

;; import Data.List

;; ----- Algebras ------------------

;; type Nat = Integer

;; ----- Recursion operators -------

;; listRec :: ([alpha] -> (alpha186 -> ((alpha -> ([alpha] -> (alpha186 -> alpha186))) -> alpha186)))
;; listRec [] a f = a
;; listRec (b : z) a f = (((f b) z) (listRec z a f))

;; ----- Program constants ---------

;; cLA :: ([Nat] -> ([Nat] -> [Nat]))
;; cLA = (\ v0 -> (\ v1 -> (listRec v1 v0 (\ x2 -> (\ v3 -> (:) x2)))))

;; cLR :: ([Nat] -> [Nat])
;; cLR = (\ v0 -> (listRec v0 [] (\ x1 -> (\ v2 -> (cLA (x1 : []))))))

;; ---------------------------------

;; clr :: ([Nat] -> [Nat])
;; clr = cLR

;; cla :: ([Nat] -> ([Nat] -> [Nat]))
;; cla = cLA

;; ---------------------------------

;; main :: IO ()
;; main = putStrLn ""

;; To run:
;; 1.  Type ghci listrev.hs in terminal.
;; 2.  On prompt *Main> type clr [2,3,4]
;; 3.  Obtain result [4,3,2]