Alice de Berny pushed to branch alice at Stefan / Typer

Commits: 7af89c25 by irradiee at 2020-07-17T15:50:19-04:00 add stats

- - - - - f807baf5 by irradiee at 2020-07-22T10:56:44-04:00 add stats on subst table

- - - - -

7 changed files:

- GNUmakefile - + profiling.txt - + samples/acctime.typer - src/REPL.ml - src/lexp.ml - src/util.ml - + stats.txt

Changes:

===================================== GNUmakefile ===================================== @@ -7,8 +7,12 @@ BUILDDIR := _build SRC_FILES := $(wildcard ./src/*.ml) CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) +TIME_FILE := ./samples/acctime.typer

-OBFLAGS = -tag debug -tag e -lib str -build-dir $(BUILDDIR) -pkg zarith +# camlLexp__hc / camlLexp__hc_eq / camlLexp_type__lexp_hash / camlSubst__subst_hash +MOTIF := camlSubst__hcsb_ + +OBFLAGS = -tag debug -tag e -lib str -build-dir $(BUILDDIR) -pkg zarith -pkg unix # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag e -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline @@ -22,6 +26,8 @@ OCAMLCP := ocamlcp OCAMLOPTP := ocamloptp OCAMLOPT := ocamlopt OCAMLDEP := ocamldep +GPROF := gprof +GREP := grep

OCAMLFLAGS := -I src SRC_NO_DEBUG := $(filter-out ./src/debug_util.ml, $(SRC_FILES)) @@ -85,7 +91,6 @@ install: tests

tests: tests-build tests-run

-# @TODO: delete test: $(OCAMLBUILD) tests/lexp_test.$(COMPILE_MODE) -I src $(OBFLAGS) @$(OCAMLBUILD) tests/utest_main.$(COMPILE_MODE) -I src $(OBFLAGS) @@ -130,22 +135,25 @@ profiling-cp: # ============================ # profiling bytecode # ============================ - ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith \ + ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith -package unix \ $(OCAMLFLAGS) str.cma -P f $(DEPSORT_FILES)

profiling-optp: # ============================ # profiling native # ============================ - ocamlfind $(OCAMLOPTP) -o profiling -linkpkg -package zarith \ + ocamlfind $(OCAMLOPTP) -o profiling -linkpkg -package zarith -package unix \ $(OCAMLFLAGS) str.cmxa -P f $(DEPSORT_FILES)

time: # ============================ # time native # ============================ - ocamlfind $(OCAMLOPT) -p -o profiling -linkpkg -package zarith \ + ocamlfind $(OCAMLOPT) -p -o profiling -linkpkg -package zarith -package unix \ $(OCAMLFLAGS) str.cmxa $(DEPSORT_FILES) + ./profiling --batch $(TIME_FILE) + $(GPROF) ./profiling >> profiling.txt + $(GREP) $(MOTIF) profiling.txt

# Clean up clean-profiling:

===================================== profiling.txt ===================================== The diff for this file was not included because it is too large.

===================================== samples/acctime.typer ===================================== @@ -0,0 +1,2159 @@ +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1)); + +accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; +accumulate = lambda (t : Type) ≡> + lambda (acc-op : (t -> t -> t)) -> + lambda (init : t) -> + lambda (list : List t) -> + case list + | cons hd tl => accumulate acc-op (acc-op init hd) tl + | nil => init; + + +map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; +map = lambda (a : Type) ≡> + lambda (b : Type) ≡> + lambda (list : List a) -> + lambda (f : a -> b) -> + case list + | cons hd tl => (cons (f hd) (map tl f)) + | nil => nil; + +list = (cons 1 (cons 2 (cons 3 (cons 4 nil)))); + +% main = accumulate _+_ 0 list; +% main = map list (lambda x -> (x + 1));

===================================== src/REPL.ml ===================================== @@ -203,7 +203,7 @@ let help_msg = %help (%h) : print help "

-let readfiles files (i, lctx, rctx) prt = +let readfiles_aux files (i, lctx, rctx) prt = (* Read specified files *) List.fold_left (fun (i, lctx, rctx) file ->

@@ -220,6 +220,10 @@ let readfiles files (i, lctx, rctx) prt = ) (i, lctx, rctx) files

+let readfiles files (i, lctx, rctx) prt = + let res = readfiles_aux files (i, lctx, rctx) prt in + res + (* Specials commands %[command-name] [args] *) let rec repl i clxp rctx = let repl = repl (i + 1) in @@ -230,8 +234,7 @@ let rec repl i clxp rctx = | "%help" | "%h" -> (print_string help_msg; repl clxp rctx) | "%calltrace" | "%ct" -> (print_eval_trace None; repl clxp rctx) | "%typertrace" | "%tt" -> (print_typer_trace None; repl clxp rctx) - | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table) !lshrct !nf_lshrct !Subst.sshrct !Subst.nf_sshrct) - | "%scollisions" | "%scl" -> (get_stats_hashtbl (Subst.WHCSB.stats Subst.hcsb_table) !lshrct !nf_lshrct !Subst.sshrct !Subst.nf_sshrct) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table) !lshrct !nf_lshrct)

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( @@ -247,7 +250,7 @@ let rec repl i clxp rctx = (time_process := true; let (i, clxp, rctx) = try - readfiles args (i, clxp, rctx) false + get_unix_stats_processtime (fun () -> (readfiles args (i, clxp, rctx) false)) with Log.Stop_Compilation msg -> (handle_stopped_compilation msg; (i,clxp,rctx)) in repl clxp rctx) @@ -319,11 +322,12 @@ let main () = if !time_process then let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + get_unix_stats_processtime (fun () -> (readfiles + (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch))) in (print_and_clear_log (); res) else let res = - readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + readfiles_aux (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in (print_and_clear_log (); res) with | Log.Stop_Compilation msg ->

===================================== src/lexp.ml ===================================== @@ -36,9 +36,10 @@ open Grammar (********************** Hash-consing **********************)

(** hash-consing test ** -* with: Hashtbl.hash - lexp'_hash -* median bucket length: 7 - 7 -* biggest bucket length: 205 - 22 *) +* with: Hashtbl.hash / lexp'_hash +* median bucket length: 7 / 7 +* biggest bucket length: 205 / 22 +* found/new lexp entries: - / 2 *)

let lexp_lexp' (e, h) = e

===================================== src/util.ml ===================================== @@ -126,7 +126,7 @@ let rec combine_hashes map = | [] -> 31 | e :: l -> combine_hash (e * 31) (combine_hashes l)

-let get_stats_hashtbl stats lshrct nf_lshrct sshrct nf_sshrct = +let get_stats_hashtbl stats lshrct nf_lshrct = let (tl, ne, sumb, smallb, medianb, bigb) = stats in Printf.printf "\n\ttable length: %i\n number of entries: %i\n @@ -134,8 +134,29 @@ let get_stats_hashtbl stats lshrct nf_lshrct sshrct nf_sshrct = smallest bucket length: %i\n median bucket length: %i\n biggest bucket length: %i\n - found/new lexp entries: %i\n - found/new subst entries: %i\n" - tl ne sumb smallb medianb bigb (lshrct / nf_lshrct) (sshrct / nf_sshrct) + found/new lexp entries: %i\n" + tl ne sumb smallb medianb bigb (lshrct / nf_lshrct)

let shrct_inc e acc = e := !e + acc + +let get_total_unix_stats_processtime (times : Unix.process_times) = + Printf.printf "\n\tUser time for the process: %f\n + System time for the process: %f\n + User time for the children processes: %f\n + System time for the children processes: %f\n" + times.tms_utime times.tms_stime times.tms_cutime times.tms_cstime + +let hc_total_time = ref 0.0 + +let inc_hc_total_time f = + let t = Unix.gettimeofday () in + let res = f () in (hc_total_time := + !hc_total_time +. Unix.gettimeofday () -. t; res) + +let get_unix_stats_processtime f = + let t = Unix.gettimeofday () in + let res = f () in (Printf.printf "\t(Unix) process time: %f\n" + (Unix.gettimeofday () -. t); res) + +let print_total_hctime hctime = + Printf.printf "\t(Unix) total hc time: %f\n" hctime

===================================== stats.txt ===================================== @@ -0,0 +1,111 @@ +## hash-consing lexp +# with subst hash table +with: Hashtbl.hash (on master branch) / lexp'_hash +median bucket length: 7 / 7 +biggest bucket length: 205 / 22 +found/new lexp entries: - / 2 + +# without subst hash table +with: lexp'_hash +median bucket length: 7 +biggest bucket length: 36 +found/new lexp entries: 3 + +## hash-consing subst + +with: subst'_hash +median bucket length: 7 +biggest bucket length: 22 +found/new subst entries: 7 + +## acctime.typer file with Unix.time (s) + +# on master branch +# average = 6.645643 + +6.627967 +6.612033 +6.668800 +6.604124 +6.574740 +6.608807 +6.609707 +6.603383 +6.879818 +6.903172 +6.624097 +6.590640 +6.625796 +6.589031 +6.586007 +6.667166 +6.594401 +6.651891 + +# on this branch +# with subst hash +# average = 7.738261 + +7.679965 +7.709951 +7.678673 +7.709191 +7.705138 +7.630524 +7.619517 +7.754700 +7.806102 +7.715318 +7.859585 +7.672065 +7.706296 +7.829695 +7.929891 +7.944672 +7.614767 +7.728893 +7.732013 + +# subst hash table without subst hash +# average = 7.620327 + +7.625761 +7.535479 +7.598095 +7.551590 +7.613274 +7.524923 +7.552562 +7.621846 +7.598882 +7.632416 +7.695533 +7.684801 +7.579720 +7.799411 +7.598517 +7.712421 + +# without subst hash table +# average = 5.829157 + +5.855567 +5.818960 +5.827624 +5.802086 +5.819951 +5.806960 +5.804491 +5.766256 +5.772987 +5.808192 +5.832567 +5.828493 +5.809422 +6.046799 +5.813889 +5.811058 +5.811843 +5.864935 +5.846754 +5.834313

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/47cb679f83f1c2d8964d7a8c07de4f03f...