;; Initial parts of lib/nat.scm

;; (load "~/git/minlog/init.scm")

(add-algs "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-var-name "n" "m" "l" (py "nat")) ;l instead of k, which will be an int

(define (make-numeric-term-wrt-nat n)
  (if (= n 0)
      (pt "Zero")
      (make-term-in-app-form
       (pt "Succ")
       (make-numeric-term-wrt-nat (- n 1)))))

(define NAT-NUMBERS #t)

(define (make-numeric-term x)
  (if NAT-NUMBERS
      (make-numeric-term-wrt-nat x)
      (make-numeric-term-wrt-pos x)))

(define (is-numeric-term? x)
  (if NAT-NUMBERS
      (is-numeric-term-wrt-nat? x)
      (is-numeric-term-wrt-pos? x)))

(define (numeric-term-to-number x)
  (if NAT-NUMBERS
      (numeric-term-wrt-nat-to-number x)
      (numeric-term-wrt-pos-to-number x)))

;; Tokens used by the parser.

(define (add-nat-tokens)
  (let* ((make-type-string
	  (lambda (type op-string type-strings)
	    (let* ((string (type-to-string type))
		   (l (string->list string)))
	      (if (member string type-strings)
		  (list->string (cons (char-upcase (car l)) (cdr l)))
		  (myerror op-string "unexpected type" type)))))
	 (tc ;term-creator
	  (lambda (op-string . type-strings)
	    (lambda (x y)
	      (let* ((type (term-to-type x))
		     (type-string
		      (make-type-string type op-string type-strings))
		     (internal-name (string-append type-string op-string)))
		(mk-term-in-app-form
		 (make-term-in-const-form
		  (pconst-name-to-pconst internal-name))
		 x y))))))
    (add-token "+" 'add-op (tc "Plus" "nat"))
    (add-token "*" 'mul-op (tc "Times" "nat"))
    (add-token "<" 'rel-op (tc "Lt" "nat"))
    (add-token "<=" 'rel-op (tc "Le" "nat"))
    (add-token "--" 'add-op (tc "Minus" "nat"))
    (add-token "max" 'mul-op (tc "Max" "nat"))
    (add-token "min" 'mul-op (tc "Min" "nat"))))

(add-nat-tokens)

;; (add-nat-display) updates DISPLAY-FUNCTIONS, so that it uses the
;; tokens introduced by (add-nat-tokens).

(define (add-nat-display)
  (let ((dc ;display-creator
	 (lambda (name display-string token-type)
	   (lambda (x)
	     (let ((op (term-in-app-form-to-final-op x))
		   (args (term-in-app-form-to-args x)))
	       (if (and (term-in-const-form? op)
			(string=? name (const-to-name
					(term-in-const-form-to-const op)))
			(= 2 (length args)))
		   (list token-type display-string
			 (term-to-token-tree (term-to-original (car args)))
			 (term-to-token-tree (term-to-original (cadr args))))
		   #f))))))
    (add-display (py "nat") (dc "NatPlus" "+" 'add-op))
    (add-display (py "nat") (dc "NatTimes" "*" 'mul-op))
    (add-display (py "boole") (dc "NatLt" "<" 'rel-op))
    (add-display (py "boole") (dc "NatLe" "<=" 'rel-op))
    (add-display (py "nat") (dc "NatMinus" "--" 'add-op))
    (add-display (py "nat") (dc "NatMax" "max" 'mul-op))
    (add-display (py "nat") (dc "NatMin" "min" 'mul-op))))

(add-nat-display)

;; End of initial parts of lib/nat.scm

;; Initial parts of lib/list.scm

(add-algs "list" 'prefix-typeop
	  '("list" "Nil")
	  '("alpha=>list=>list" "Cons"))

(add-var-name "x" (py "alpha"))
(add-var-name "xs" (py "list alpha"))

(add-token
 "::" 'pair-op
 (lambda (x y)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((const (constr-name-to-constr "Cons"))
	    (uninst-type (const-to-uninst-type const))
	    (patterns (arrow-form-to-arg-types uninst-type 2)) ;al, list al
	    (instances (map term-to-type (list x y))) ;e.g.  nat, list int
	    (type1 (car instances)) ;nat
	    (type2 (car (alg-form-to-types (cadr instances)))) ;int
	    (tsubst (cond ((type-le? type1 type2)
			   (make-subst (car patterns) type2))
			  ((type-le? type2 type1)
			   (make-subst (car patterns) type1))
			  (else (myerror "comparable types expected"
					 type1 type2)))))
       (const-substitute const tsubst #f)))
    x y)))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if
	  (and (term-in-const-form? op)
	       (string=? "Cons"
			 (const-to-name (term-in-const-form-to-const op)))
	       (= 2 (length args)))
	  (list 'pair-op  "::"
		(term-to-token-tree (car args))
		(term-to-token-tree (cadr args)))
	  #f))
       #f)))

;; The postfix-op ":" with "x:" for "x::(Nil rho)" needs a special
;; treatment with explicit uses of add-token and add-display.

(add-token
 ":" 'postfix-op
 (lambda (x)
   (mk-term-in-app-form
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Cons"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f)))
    x
    (make-term-in-const-form
     (let* ((constr (constr-name-to-constr "Nil"))
	    (tvars (const-to-tvars constr))
	    (subst (make-substitution tvars (list (term-to-type x)))))
       (const-substitute constr subst #f))))))

(add-display
 (py "list alpha")
 (lambda (x)
   (if (term-in-app-form? x)
       (let ((op (term-in-app-form-to-final-op x))
	     (args (term-in-app-form-to-args x)))
	 (if (and (term-in-const-form? op)
		  (string=? "Cons" (const-to-name
				    (term-in-const-form-to-const op)))
		  (= 2 (length args))
		  (term-in-const-form? (cadr args))
		  (string=? "Nil" (const-to-name
				   (term-in-const-form-to-const (cadr args)))))
	     (list 'postfix-op ":" (term-to-token-tree (car args)))
	     #f))
       #f)))

;; End of initial parts of lib/list.scm

;; Initial parts of lib/str.scm

(add-algs "str" 'prefix-typeop '("alpha=>str=>str" "SCons"))
(add-var-name "xstr" (py "str alpha"))
(add-infix-display-string "SCons" ":~:" 'pair-op) ;right associative

(pp (pt "x^1:~:x^2:~:x^3:~:xstr^"))

;; End of initial parts of lib/str.scm

;; Standard algebras

;; Be default we have the algebras unit boole yprod ysum uysum ysumu
;; We have added nat list str
;; We now add pos bin

(add-algs "pos" '("One" "pos") '("SZero" "pos=>pos") '("SOne" "pos=>pos"))
(add-var-name "p" "q" "r" (py "pos"))

(add-algs "bin" '("Lf" "bin") '("Br" "bin=>bin=>bin"))

(display-alg "unit" "boole" "nat" "pos" "bin")
(display-alg "list" "str")
(display-alg "yprod" "ysum" "uysum" "ysumu")

;; Program constants.

(add-program-constant "NatPlus" (py "nat=>nat=>nat"))
(add-program-constant "NatTimes" (py "nat=>nat=>nat"))
(add-program-constant "NatLe" (py "nat=>nat=>boole"))

;; Computation rules for the program constants.

;; For NatPlus
(add-computation-rules
 "n+0" "n"
 "n+Succ m" "Succ(n+m)")

;; For NatTimes
(add-computation-rules
 "n*0" "0"
 "n*Succ m" "(n*m)+n")

;; For NatLe
(add-computation-rules
 "0<=n" "True"
 "Succ n<=0" "False"
 "Succ n<=Succ m" "n<=m")

(display-pconst "NatPlus" "NatTimes" "NatLe")

;; The computation rules give rise to theorems, for instance

(pp "NatLe2CompRule")
;; all n^,m^ (Succ n^ <=Succ m^)eqd(n^ <=m^)

;; Here eqd denotes "Leibniz equality" between terms.  It will later
;; be defined as an "inductive predicate".

;; Types of recursion operators 

(pp (const-to-type (arrow-types-to-rec-const (py "boole=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "nat=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "pos=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "bin=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "list beta=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "beta ysum gamma=>alpha"))))
(pp (const-to-type (arrow-types-to-rec-const (py "beta yprod gamma=>alpha"))))

(pp (make-term-in-const-form (arrow-types-to-rec-const (py "bin=>alpha"))))

;; Definition of addition for nat using recursion

(pp (pt "(Rec nat=>nat)2 3([n,l](Succ l))"))
(pp (nt (pt "(Rec nat=>nat)2 3([n,l](Succ l))")))

;; Types of destructors

(pp (const-to-type (alg-to-destr-const (py "nat"))))
(pp (const-to-type (alg-to-destr-const (py "pos"))))
(pp (const-to-type (alg-to-destr-const (py "bin"))))
(pp (const-to-type (alg-to-destr-const (py "list alpha"))))
(pp (const-to-type (alg-to-destr-const (py "str alpha"))))

(pp (make-term-in-const-form (alg-to-destr-const (py "bin"))))