Alice de Berny pushed to branch alice at Stefan / Typer

Commits: 028fb86e by irradiee at 2020-07-24T09:11:53-04:00 remove susbt hash table

- - - - - af983619 by irradiee at 2020-07-31T09:11:10-04:00 remove lexp_type & clean code

- - - - -

19 changed files:

- GNUmakefile - − profiling.txt - − samples/acctime.typer - src/REPL.ml - src/builtin.ml - src/debruijn.ml - src/debug_util.ml - src/elab.ml - src/elexp.ml - src/env.ml - src/eval.ml - src/inverse_subst.ml - src/lexp.ml - − src/lexp_type.ml - src/opslexp.ml - src/subst.ml - src/unification.ml - src/util.ml - − stats.txt

Changes:

===================================== GNUmakefile ===================================== @@ -4,15 +4,15 @@ OCAMLBUILD=ocamlbuild

BUILDDIR := _build

+OCAMLCP := ocamlcp +OCAMLOPT := ocamlopt +OCAMLDEP := ocamldep + SRC_FILES := $(wildcard ./src/*.ml) -CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo) TEST_FILES := $(wildcard ./tests/*_test.ml) -TIME_FILE := ./samples/acctime.typer - -# camlLexp__hc / camlLexp__hc_eq / camlLexp_type__lexp_hash / camlSubst__subst_hash -MOTIF := camlSubst__hcsb_ +DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG))

-OBFLAGS = -tag debug -tag e -lib str -build-dir $(BUILDDIR) -pkg zarith -pkg unix +OBFLAGS = -tag debug -tag e -lib str -build-dir $(BUILDDIR) -pkg zarith # OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str # OBFLAGS_DEBUG := -tag debug -tag e -tag "warn(+20)" # OBFLAGS_RELEASE := -tag unsafe -tag inline @@ -22,17 +22,6 @@ COMPILE_MODE = byte # DEBUG ?= 1 # VERBOSE ?= 1

-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)) -DEPSORT_FILES := $(shell ocamldep -sort -I src $(SRC_NO_DEBUG)) - all: typer debug tests-build

# ifeq ($(OS), Windows_NT) @@ -136,24 +125,14 @@ profiling-cp: # profiling bytecode # ============================ ocamlfind $(OCAMLCP) -o profiling -linkpkg -package zarith -package unix \ - $(OCAMLFLAGS) str.cma -P f $(DEPSORT_FILES) + -I src str.cma -P f $(DEPSORT_FILES)

profiling-optp: # ============================ # profiling native # ============================ 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 -package unix \ - $(OCAMLFLAGS) str.cmxa $(DEPSORT_FILES) - ./profiling --batch $(TIME_FILE) - $(GPROF) ./profiling >> profiling.txt - $(GREP) $(MOTIF) profiling.txt + -I src str.cmxa -P f $(DEPSORT_FILES)

# Clean up clean-profiling:

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

===================================== samples/acctime.typer deleted ===================================== @@ -1,2159 +0,0 @@ -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 ===================================== @@ -44,7 +44,7 @@ open Prelexer open Lexer open Sexp open Pexp -open Lexp_type + open Lexp

open Eval @@ -203,9 +203,10 @@ let help_msg = %help (%h) : print help "

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

(if prt then ( print_string " In["; ralign_print_int i 2; print_string "] >> "; @@ -220,9 +221,6 @@ let readfiles_aux 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 = @@ -234,7 +232,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) + | "%lcollisions" | "%cl" -> (get_stats_hashtbl (WHC.stats hc_table))

(* command with arguments *) | _ when (ipt.[0] = '%' && ipt.[1] != ' ') -> ( @@ -244,16 +242,9 @@ let rec repl i clxp rctx = try readfiles args (i, clxp, rctx) false with Log.Stop_Compilation msg -> - (handle_stopped_compilation msg; (i,clxp,rctx)) in - repl clxp rctx - | "%readfiletime"::args -> - (time_process := true; - let (i, clxp, rctx) = - try - 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) + (handle_stopped_compilation msg; (i,clxp,rctx)) + in + repl clxp rctx; | "%who"::args | "%w"::args -> ( let _ = match args with | ["all"] -> dump_rte_ctx rctx @@ -295,7 +286,6 @@ let arg_defs = [ ("--verbosity", Arg.String Log.set_typer_log_level_str, "Set the logging level"); ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity"); - ("--time", Arg.Set time_process, "Get time for process"); (* ("--debug", Arg.Set arg_debug, "Print the Elexp representation") *) (*"-I", Arg.String (fun f -> searchpath := f::!searchpath), @@ -319,16 +309,9 @@ let main () =

let (i, ectx, rctx) = ( try - if !time_process - then - let res = - 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_aux (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in - (print_and_clear_log (); res) + let res = + readfiles (List.rev !arg_files) (1, ectx, rctx) (not !arg_batch) in + print_and_clear_log (); res with | Log.Stop_Compilation msg -> handle_stopped_compilation msg; exit 1

===================================== src/builtin.ml ===================================== @@ -57,7 +57,7 @@ open Util

open Sexp (* Integer/Float *) open Pexp (* arg_kind *) -open Lexp_type + module OL = Opslexp open Lexp

===================================== src/debruijn.ml ===================================== @@ -36,7 +36,7 @@ module Str = Str

open Util

-open Lexp_type + open Lexp

module M = Myers

===================================== src/debug_util.ml ===================================== @@ -37,7 +37,7 @@ open Debug (* ASTs *) open Sexp open Pexp -open Lexp_type + open Lexp

(* AST reader *)

===================================== src/elab.ml ===================================== @@ -45,7 +45,7 @@ open Lexer

open Sexp open Pexp -open Lexp_type + open Lexp

open Env @@ -395,23 +395,23 @@ let rec meta_to_var ids (e : lexp) = *)

(* `o` is the binding offset until the root. *) - let rec adjust_subst o (s : subst) = match S.subst_subst' s with - | Identity n + let rec adjust_subst o (s : subst) = match s with + | S.Identity n -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.hcsb (Identity (n + count)) + S.Identity (n + count) else - S.hcsb (Identity n) - | Cons (e, s', n) + S.Identity n + | S.Cons (e, s', n) -> let o' = o - n in if o' < 0 then (* This metavar's original context is outside of our scope * (case (B) above), so don't let it refer to the new vars. *) - S.hcsb (Cons (e, s', n + count)) + S.Cons (e, s', n + count) else - S.hcsb (Cons (loop o' e, adjust_subst o' s', n)) + S.Cons (loop o' e, adjust_subst o' s', n)

(* `o` is the binding depth at which we are relative to the "root" * of the expression (i.e. where the new vars will be inserted). *)

===================================== src/elexp.ml ===================================== @@ -35,7 +35,6 @@ open Sexp (* Sexp type *) open Pexp (* Anormal *)

module U = Util -module LT = Lexp_type module L = Lexp

type vname = U.vname @@ -78,7 +77,7 @@ type elexp =

(* A Type expression. There's no useful operation we can apply to it, * but they can appear in the code. *) - | Type of LT.lexp + | Type of L.lexp

let rec elexp_location e = match e with

===================================== src/env.ml ===================================== @@ -36,7 +36,6 @@ open Sexp

open Elexp module M = Myers -module LT = Lexp_type module L = Lexp module BI = Z (* Was Big_int *) module DB = Debruijn @@ -59,7 +58,7 @@ type value_type = | Vsexp of sexp (* Values passed to macros. *) (* Unable to eval during macro expansion, only throw if the value is used *) | Vundefined - | Vtype of LT.lexp (* The lexp value can't be trusted. *) + | Vtype of L.lexp (* The lexp value can't be trusted. *) | Vin of in_channel | Vout of out_channel | Vcommand of (unit -> value_type) @@ -242,7 +241,7 @@ let print_rte_ctx_n (ctx: runtime_env) start =

(* Only print user defined variables *) let print_rte_ctx ctx = - print_rte_ctx_n ctx (!LT.builtin_size) + print_rte_ctx_n ctx (!L.builtin_size)

(* Dump the whole context *) let dump_rte_ctx ctx =

===================================== src/eval.ml ===================================== @@ -35,7 +35,7 @@ open Fmt

open Sexp open Pexp (* Arg_kind *) -open Lexp_type + open Lexp (* Varbind *)

open Elexp

===================================== src/inverse_subst.ml ===================================== @@ -39,7 +39,7 @@ this program. If not, see http://www.gnu.org/licenses/. *) * So either left or right inverse can be used! *)

-open Lexp_type + open Lexp open Util module S = Subst @@ -69,7 +69,7 @@ let transfo (s: subst) : substIR option = let shiftVar (var: lexp) (offset: int): int = indexOf (mkSusp var (S.shift offset)) (* Helper : shift the index of a var *) in - match S.subst_subst' s with + match s with | Cons ((Var _ as v, h), s, o) -> let off_acc = off_acc + o in (match transfo s off_acc (idx + 1) imp_cnt with @@ -146,7 +146,7 @@ let fill (l: (int * int) list) (nbVar: int) (shift: int): subst option =

let is_identity (s : subst) = let rec is_identity (s : subst) acc = - match S.subst_subst' s with + match s with | Cons((Var(_, idx), _), s1, 0) when idx = acc -> is_identity s1 (acc + 1) | Identity o -> acc = o | _ -> S.identity_p s @@ -182,7 +182,7 @@ let inverse (s: subst) : subst option = (* Returns false if the application of the inverse substitution is not * possible. This happens when the substitution replaces some variables * with non-variables, in which case the "inverse" is ambiguous. *) -let rec invertible (s: subst) : bool = match S.subst_subst' s with +let rec invertible (s: subst) : bool = match s with | Identity _ -> true | Cons (e, s, _) -> (let e' = lexp_lexp' e in @@ -194,7 +194,7 @@ exception Ambiguous

(* Lookup variable i in s⁻¹ *) let rec lookup_inv_subst (i : db_index) (s : subst) : db_index - = match S.subst_subst' s with + = match s with | (Identity o | Cons (_, _, o)) when i < o -> raise Not_invertible | Identity o -> i - o | Cons ((Var (_, i'), _), s, o) when i' = i - o @@ -240,7 +240,7 @@ let shift_inv_subst n s * One way to do it is to compute s⁻¹ and then pass it to `compose`. * But we can try and do it more directly. *) -let rec compose_inv_subst (s' : subst) (s : subst) = match S.subst_subst' s' with +let rec compose_inv_subst (s' : subst) (s : subst) = match s' with | Cons (e, s', o) -> let s = shift_inv_subst o s in (* FIXME: Why don't we ever return a Shift? *)

===================================== src/lexp.ml ===================================== @@ -20,19 +20,154 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-(* open Unify *) -module S = Subst - +module U = Util +module L = List +module SMap = U.SMap open Fmt

open Sexp open Pexp

-open Lexp_type - open Myers open Grammar

+(* open Unify *) +module S = Subst + +type vname = U.vname +type vref = U.vref +type meta_id = int (* Identifier of a meta variable. *) + +type label = symbol + +type attribute_key = (int * string) (* rev_dbi * Var name *) +module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) + +(*************** Elaboration to Lexp *********************) + +(* The scoping of `Let` is tricky: + * + * Since it's a recursive let, the definition part of each binding is + * valid in the "final" scope which includes all the new bindings. + * + * But the type of each binding is not defined in that same scope. Instead + * it's defined in the scope of all the previous bindings. + * + * For exemple the type of the second binding of such a Let is defined in + * the scope of the surrounded context extended with the first binding. + * And the type of the 3rd binding is defined in the scope of the + * surrounded context extended with the first and the second bindings. *) + +type ltype = lexp + and subst = lexp S.subst + and lexp = int * lexp' + and lexp' = + | Imm of sexp (* Used for strings, ... *) + | SortLevel of sort_level + | Sort of U.location * sort + | Builtin of symbol * ltype * lexp AttributeMap.t option + | Var of vref + | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) + (* This "Let" allows recursion. *) + | Let of U.location * (vname * lexp * ltype) list * lexp + | Arrow of arg_kind * vname * ltype * U.location * ltype + | Lambda of arg_kind * vname * ltype * lexp + | Call of lexp * (arg_kind * lexp) list (* Curried call. *) + | Inductive of U.location * label + * ((arg_kind * vname * ltype) list) (* formal Args *) + * ((arg_kind * vname * ltype) list) SMap.t + | Cons of lexp * symbol (* = Type info * ctor_name *) + | Case of U.location * lexp + * ltype (* The type of the return value of all branches *) + * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (vname * lexp) option (* Default. *) + (* The `subst` will be applied to the the metavar's value when it + * gets instantiated. *) + | Metavar of meta_id * subst * vname + (* (* For logical metavars, there's no substitution. *) + * | Metavar of (U.location * string) * metakind * metavar ref + * and metavar = + * (* An uninstantiated var, along with a venv (stipulating over which vars + * * it should be closed), and its type. + * * If its type is not given, it implies its type should be a sort. *) + * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level + * | MetaSet of lexp + * and metakind = + * | MetaGraft of subst + * (* Forward reference or Free var: Not known yet, but not instantiable by + * * unification. *) + * | MetaFoF + * and subst = lexp VMap.t *) + (* + * The PTS I'm imagining looks like: + * + * S = { TypeLevel, TypeOmega, Type ℓ } + * A = { Level : TypeLevel, Z : Level, S : Level → Level, + * Type : (ℓ : Level) → Type (S ℓ) } + * R = { (TypeLevel, Type ℓ, TypeOmega), + * (TypeLevel, TypeOmega, TypeOmega), + * (Type ℓ, TypeOmega, TypeOmega), + * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } + *) + and sort = + | Stype of lexp + | StypeOmega + | StypeLevel + and sort_level = + | SLz + | SLsucc of lexp + | SLlub of lexp * lexp + +type varbind = + | Variable + | ForwardRef + | LetDef of U.db_offset * lexp + +(* For metavariables, we give each metavar a (hopefully) unique integer + * and then we store its corresponding info into the `metavar_table` + * global map. + * + * Instead of this single ref-cell holding an IntMap, we could use many + * ref-cells, and do away with the unique integer. The reasons why we + * do it this way are: + * - for printing purposes, we want to have a printable unique identifier + * for each metavar. OCaml does not offer any way to turn a ref-cell + * into some kind of printable identifier (can't get a hash of the address, + * no `eq` hash-tables, ...). + * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: + * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique + * integer in order to produce a hash anyway (and we'd have to write the hash + * function by hand, tho that might be a good idea anyway). + *) + +(* Scope level is used to detect "out of scope" metavars. + * See http://okmij.org/ftp/ML/generalization.html + * The ctx_length keeps track of the length of the lctx in which the + * metavar is meant to be defined. *) +type scope_level = int +type ctx_length = int + +type metavar_info = + | MVal of lexp (* Exp to which the var is instantiated. *) + | MVar of scope_level (* Outermost scope in which the var appears. *) + * ltype (* Expected type. *) + (* We'd like to keep the lexp_content in which the type is to be + * understood, but lexp_context is not yet defined here, + * so we just keep the length of the lexp_context. *) + * ctx_length +type meta_subst = metavar_info U.IMap.t + +let dummy_scope_level = 0 +let impossible = Imm Sexp.dummy_epsilon + +let builtin_size = ref 0 + +let metavar_table = ref (U.IMap.empty : meta_subst) +let metavar_lookup (id : meta_id) : metavar_info + = try U.IMap.find id (!metavar_table) + with Not_found + -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!" + (********************** Hash-consing **********************)

(** hash-consing test ** @@ -41,10 +176,12 @@ open Grammar * biggest bucket length: 205 / 22 * found/new lexp entries: - / 2 *)

-let lexp_lexp' (e, h) = e +let lexp_lexp' (h, e) = e +let lexp_hash (h, e) = h

-let lexp'_hash (expr : lexp') = - match expr with +(* hash lexp using combine_hash (lxor) with hash of sub-lexp *) +let lexp'_hash (lp : lexp') = + match lp with | Imm s -> U.combine_hash 1 (Hashtbl.hash s) | SortLevel l -> U.combine_hash 2 @@ -93,14 +230,16 @@ let lexp'_hash (expr : lexp') = | _ -> 0)))) | Metavar (id, s, v) -> U.combine_hash 12 (U.combine_hash id - (U.combine_hash (S.subst_hash s) (Hashtbl.hash v))) + (U.combine_hash (Hashtbl.hash s) (Hashtbl.hash v))) | Call (e, args) -> U.combine_hash 13 (U.combine_hash (lexp_hash e) (U.combine_hashes (List.map (fun e -> let (ak, lp) = e in (U.combine_hash (Hashtbl.hash ak) (lexp_hash lp))) args))) | Susp (lp, subst) - -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (S.subst_hash subst)) + -> U.combine_hash 14 (U.combine_hash (lexp_hash lp) (Hashtbl.hash subst))

+(* equality function for hash table + * using physical eq for sub-lexp and compare for subst *) let hc_eq e1 e2 = e1 == e2 || match (lexp_lexp' e1, lexp_lexp' e2) with @@ -117,7 +256,7 @@ let hc_eq e1 e2 = | (Sort (_, Stype e1), Sort (_, Stype e2)) -> e1 == e2 | (Builtin ((_, name1), _, _), Builtin ((_, name2), _, _)) -> name1 = name2 | (Var (_, i1), Var (_, i2)) -> i1 = i2 - | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && s1 == s2 + | (Susp (e1, s1), Susp (e2, s2)) -> e1 == e2 && compare s1 s2 = 0 | (Let (_, defs1, e1), Let (_, defs2, e2)) -> e1 == e2 && List.for_all2 (fun (_, e1, t1) (_, e2, t2) -> t1 == t2 && e1 == e2) defs1 defs2 @@ -143,30 +282,19 @@ let hc_eq e1 e2 = | (Some (_, e1), Some (_, e2)) -> e1 == e2 | _ -> def1 = def2) | (Metavar (i1, s1, _), Metavar (i2, s2, _)) - -> i1 = i2 && s1 == s2 + -> i1 = i2 && compare s1 s2 = 0 | _ -> false

module WHC = Weak.Make (struct type t = lexp - (* Using (=) instead of `compare` results - * in an *enormous* slowdown. Apparently - * `compare` checks == before recursing - * but (=) doesn't? *) - let equal x y = hc_eq x y - let hash = lexp_hash - end) - -(* counter for lexp found in WHC *) -let lshrct = ref 0 - -(* counter for lexp not found in WHC *) -let nf_lshrct = ref 0 + let equal x y = hc_eq x y + let hash = lexp_hash + end)

let hc_table : WHC.t = WHC.create 1000

let hc (s : lexp') : lexp = - let lp = (s, lexp'_hash s) in - try let lp' = WHC.find hc_table lp in (U.shrct_inc lshrct 1; lp') - with Not_found -> (U.shrct_inc nf_lshrct 1; WHC.add hc_table lp; lp) + let lp = (s, lexp'_hash s) in + WHC.merge hc_table lp

let impossible = hc (Imm Sexp.dummy_epsilon)

@@ -618,7 +746,7 @@ let rec lexp_unparse lxp = (* FIXME: ¡Unify lexp_print and lexp_string! *) and lexp_string lxp = sexp_string (lexp_unparse lxp)

-and subst_string s = match S.subst_subst' s with +and subst_string s = match s with | Identity o -> "↑" ^ string_of_int o | Cons (l, s, 0) -> lexp_name l ^ " · " ^ subst_string s | Cons (l, s, o) @@ -998,7 +1126,7 @@ let rec eq e1 e2 =

and subst_eq s1 s2 = s1 == s2 || - match (S.subst_subst' s1, S.subst_subst' s2) with + match (s1, s2) with | (Identity o1, Identity o2) -> o1 = o2 | (Cons (e1, s1, o1), Cons (e2, s2, o2)) -> if o1 = o2 then

===================================== src/lexp_type.ml deleted ===================================== @@ -1,195 +0,0 @@ -(* lexp_type.ml --- Lambda-expressions: the core language. - -Copyright (C) 2011-2020 Free Software Foundation, Inc. - -Author: Stefan Monnier monnier@iro.umontreal.ca -Keywords: languages, lisp, dependent types. - -This file is part of Typer. - -Typer is free software; you can redistribute it and/or modify it under the -terms of the GNU General Public License as published by the Free Software -Foundation, either version 3 of the License, or (at your option) any -later version. - -Typer is distributed in the hope that it will be useful, but WITHOUT ANY -WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS -FOR A PARTICULAR PURPOSE. See the GNU General Public License for -more details. - -You should have received a copy of the GNU General Public License along with -this program. If not, see http://www.gnu.org/licenses/. *) - -module U = Util -module L = List -module SMap = U.SMap - - -open Sexp -open Pexp - - -type vname = U.vname -type vref = U.vref -type meta_id = int (* Identifier of a meta variable. *) - -type label = symbol - -type attribute_key = (int * string) (* rev_dbi * Var name *) -module AttributeMap = Map.Make (struct type t = attribute_key let compare = compare end) - -(*************** Elaboration to Lexp *********************) - -(* The scoping of `Let` is tricky: - * - * Since it's a recursive let, the definition part of each binding is - * valid in the "final" scope which includes all the new bindings. - * - * But the type of each binding is not defined in that same scope. Instead - * it's defined in the scope of all the previous bindings. - * - * For exemple the type of the second binding of such a Let is defined in - * the scope of the surrounded context extended with the first binding. - * And the type of the 3rd binding is defined in the scope of the - * surrounded context extended with the first and the second bindings. *) - -type ltype = lexp - and lexp = lexp' * int - and lexp' = - | Imm of sexp (* Used for strings, ... *) - | SortLevel of sort_level - | Sort of U.location * sort - | Builtin of symbol * ltype * lexp AttributeMap.t option - | Var of vref - | Susp of lexp * subst (* Lazy explicit substitution: e[σ]. *) - (* This "Let" allows recursion. *) - | Let of U.location * (vname * lexp * ltype) list * lexp - | Arrow of arg_kind * vname * ltype * U.location * ltype - | Lambda of arg_kind * vname * ltype * lexp - | Call of lexp * (arg_kind * lexp) list (* Curried call. *) - | Inductive of U.location * label - * ((arg_kind * vname * ltype) list) (* formal Args *) - * ((arg_kind * vname * ltype) list) SMap.t - | Cons of lexp * symbol (* = Type info * ctor_name *) - | Case of U.location * lexp - * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t - * (vname * lexp) option (* Default. *) - (* The `subst` will be applied to the the metavar's value when it - * gets instantiated. *) - | Metavar of meta_id * subst * vname - (* (* For logical metavars, there's no substitution. *) - * | Metavar of (U.location * string) * metakind * metavar ref - * and metavar = - * (* An uninstantiated var, along with a venv (stipulating over which vars - * * it should be closed), and its type. - * * If its type is not given, it implies its type should be a sort. *) - * | MetaUnset of (lexp option * lexp) VMap.t * ltype option * scope_level - * | MetaSet of lexp - * and metakind = - * | MetaGraft of subst - * (* Forward reference or Free var: Not known yet, but not instantiable by - * * unification. *) - * | MetaFoF - * and subst = lexp VMap.t *) - (* - * The PTS I'm imagining looks like: - * - * S = { TypeLevel, TypeOmega, Type ℓ } - * A = { Level : TypeLevel, Z : Level, S : Level → Level, - * Type : (ℓ : Level) → Type (S ℓ) } - * R = { (TypeLevel, Type ℓ, TypeOmega), - * (TypeLevel, TypeOmega, TypeOmega), - * (Type ℓ, TypeOmega, TypeOmega), - * (Type ℓ₁, Type ℓ₂, Type (max l₁ l₂) } - *) -and sort = - | Stype of lexp - | StypeOmega - | StypeLevel -and sort_level = - | SLz - | SLsucc of lexp - | SLlub of lexp * lexp - -(* We define here substitutions which take a variable within a source context -* Δₛ and should return an expression valid in target context Δₜ. -* -* The current implementation only handles a very limited subset of such -* substitutions. One of the many limitations is that we can only encode -* substitutions which map variables to variables. -*) - -and db_index = int (* DeBruijn index. *) -and db_offset = int (* DeBruijn index offset. *) - -(* Substitution, i.e. a mapping from db_index to lexp *) -(* @TODO: change Cons name *) -and subst = subst' * int - and subst' = - | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) - | Cons of lexp * subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) - (* Myers's extra pointers down the list: - * * int * lexp subst * db_offset *) -(* Lift (n,m) increases indices≥N by M. - * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination - * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) - (* | Lift of db_index * db_offset *) - -(* Build Myers's "stack" element. *) -(* let mkCons e s o = match s with -* | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 -* -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) -* | _ -> Cons (e, s, o, 1, s, o) *) - - -type varbind = - | Variable - | ForwardRef - | LetDef of U.db_offset * lexp - -let lexp_hash (e, h) = h - -(* For metavariables, we give each metavar a (hopefully) unique integer - * and then we store its corresponding info into the `metavar_table` - * global map. - * - * Instead of this single ref-cell holding an IntMap, we could use many - * ref-cells, and do away with the unique integer. The reasons why we - * do it this way are: - * - for printing purposes, we want to have a printable unique identifier - * for each metavar. OCaml does not offer any way to turn a ref-cell - * into some kind of printable identifier (can't get a hash of the address, - * no `eq` hash-tables, ...). - * - Hashtbl.hash as well as `compare` happily follow ref-cell indirections: - * `compare (ref 0) (ref 0)` tells us they're equal! So we need the unique - * integer in order to produce a hash anyway (and we'd have to write the hash - * function by hand, tho that might be a good idea anyway). - *) - -(* Scope level is used to detect "out of scope" metavars. - * See http://okmij.org/ftp/ML/generalization.html - * The ctx_length keeps track of the length of the lctx in which the - * metavar is meant to be defined. *) -type scope_level = int -type ctx_length = int - -type metavar_info = - | MVal of lexp (* Exp to which the var is instantiated. *) - | MVar of scope_level (* Outermost scope in which the var appears. *) - * ltype (* Expected type. *) - (* We'd like to keep the lexp_content in which the type is to be - * understood, but lexp_context is not yet defined here, - * so we just keep the length of the lexp_context. *) - * ctx_length -type meta_subst = metavar_info U.IMap.t - -let dummy_scope_level = 0 - -let builtin_size = ref 0 - -let metavar_table = ref (U.IMap.empty : meta_subst) -let metavar_lookup (id : meta_id) : metavar_info - = try U.IMap.find id (!metavar_table) - with Not_found - -> Log.log_fatal ~section:"LEXP" "metavar lookup failure!"

===================================== src/opslexp.ml ===================================== @@ -30,7 +30,7 @@ module P = Pexp (* open Grammar *) open Lexp module E = Elexp -open Lexp_type + module L = Lexp module M = Myers

===================================== src/subst.ml ===================================== @@ -20,7 +20,6 @@ You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

module U = Util -open Lexp_type

(* Implementation of the subsitution calculus. * @@ -104,58 +103,43 @@ open Lexp_type * *)

-(********************** Hash-consing **********************) - -(** hash-consing test ** - * with: subst'_hash - * median bucket length: 7 - * biggest bucket length: 22 - * found/new subst entries: 7 *) - -let subst_hash (s, h) = h -let subst_subst' (s, h) = s - -(* counter for subst found in WHCSB *) -let sshrct = ref 0 - -(* counter for subst not found in WHCSB *) -let nf_sshrct = ref 0 - -let hcsb_eq sb1 sb2 = - sb1 == sb2 || - match (subst_subst' sb1, subst_subst' sb2) with - | (Identity off1, Identity off2) -> off1 = off2 - | (Cons (lp1, lps1, off1), Cons (lp2, lps2, off2)) - -> lp1 == lp2 && lps1 == lps2 && off1 = off2 - | _ -> false - -let subst'_hash (sb : subst') : int = - match sb with - | Identity off - -> U.combine_hash 1 (Hashtbl.hash off) - | Cons (lp, sb, off) - -> U.combine_hash 2 - (U.combine_hash (U.combine_hash - (lexp_hash lp) (subst_hash sb)) (Hashtbl.hash off)) - -module WHCSB = Weak.Make (struct type t = subst - let equal x y = hcsb_eq x y - let hash = subst_hash - end) - -let hcsb_table : WHCSB.t = WHCSB.create 1000 +(* We define here substitutions which take a variable within a source context + * Δₛ and should return an expression valid in target context Δₜ. + * + * The current implementation only handles a very limited subset of such + * substitutions. One of the many limitations is that we can only encode + * substitutions which map variables to variables. + *)

-let hcsb (s : subst') : subst = - let sb = (s, subst'_hash s) in - try let sb' = WHCSB.find hcsb_table sb in (U.shrct_inc sshrct 1; sb') - with Not_found -> (U.shrct_inc nf_sshrct 1; WHCSB.add hcsb_table sb; sb) +type db_index = int (* DeBruijn index. *) +type db_offset = int (* DeBruijn index offset. *) + +(* Substitution, i.e. a mapping from db_index to 'a + * In practice, 'a is always lexp, but we keep it as a parameter: + * - for better modularity of the code. + * - to break a mutual dependency between the Lexp and the Subst modules. *) +type 'a subst = (* lexp subst *) + | Identity of db_offset (* Identity o ≡ id ∘ ↑ₒ *) + | Cons of 'a * 'a subst * db_offset (* Cons (e, s, o) ≡ (e · s) ∘ ↑ₒ *) + (* Myers's extra pointers down the list: + * * int * 'a subst * db_offset *) +(* Lift (n,m) increases indices≥N by M. + * IOW, it takes variables from a source context Δₛ₁Δₛ₂ to a destination + * context Δₛ₁ΔₜΔₛ₂ where Δₛ₂ has size N and Δₜ has size M. *) + (* | Lift of db_index * db_offset *) + +(* Build Myers's "stack" element. *) +(* let mkCons e s o = match s with + * | Cons (_, _, _, sk1, Cons (_, _, _, sk2, s2, o2), o1) when sk1 >= sk2 + * -> Cons (e, s, o, sk1 + sk2 + 1, s2, o1 + o2 + o) + * | _ -> Cons (e, s, o, 1, s, o) *)

(* Apply a substitution to a single variable. *) let lookup (mkVar : 'b -> db_index -> 'a) (mkShift: 'a -> db_offset -> 'a) - (s: subst) (l : 'b) (v:db_index) : 'a = - let rec lookup' (o:db_offset) (s: subst) (v:db_index) : 'a = - match subst_subst' s with + (s: 'a subst) (l : 'b) (v:db_index) : 'a = + let rec lookup' (o:db_offset) (s: 'a subst) (v:db_index) : 'a = + match s with | Identity o' -> mkVar l (v + o + o') (* Use Myers's fastlane when applicable: * | Cons (_, _, _, sk, s, o') when v >= sk -> lookup' (o + o') s (v - sk) *) @@ -164,49 +148,48 @@ let lookup (mkVar : 'b -> db_index -> 'a) else mkShift e o in lookup' 0 s v

-(* ici *) let mkShift s (m:db_offset) = if m>0 then - match subst_subst' s with Identity o -> hcsb (Identity (o + m)) - | Cons (e, s, o) -> hcsb (Cons (e, s, o + m)) + match s with Identity o -> Identity (o + m) + | Cons (e, s, o) -> Cons (e, s, o + m) else s

(* A substitution which adds M to every deBruijn index. * I.e. one that takes variables from a context Δₛ to an extended * context ΔₛΔₜ where Δₜ has size M. *) -let shift (m:db_offset) : subst = hcsb (Identity m) +let shift (m:db_offset) = Identity m

(* Return a substitution which replaces #0 with `e` and then applies `s` * to the rest. *) -let cons e s : subst = hcsb (Cons (e, s, 0)) +let cons e s = Cons (e, s, 0)

(* The trivial substitution which doesn't do anything. *) -let identity = hcsb (Identity 0) +let identity = Identity 0

(* Test if a substitution is trivial. The "_p" stands for "predicate". *) -let identity_p s = match subst_subst' s with | Identity o -> o = 0 | _ -> false +let identity_p s = match s with | Identity o -> o = 0 | _ -> false

(* Compose two substitutions. This implements the merging rules. * Returns s₁ ∘ s₂ (i.e. s₁ is applied before s₂) *) -let compose (mkSusp : 'a -> subst -> 'a) - (s1: subst) (s2: subst) : subst = +let compose (mkSusp : 'a -> 'a subst -> 'a) + (s1: 'a subst) (s2: 'a subst) : 'a subst = (* There is a bit of flexibility in what we return, in the sense * that some shifts can be pushed more or less down. Here we * want the shifts to float as far outside as possible. *) - let rec compose' (s1: subst) (s2: subst) : subst = - match subst_subst' s1 with + let rec compose' (s1: 'a subst) (s2: 'a subst) : 'a subst = + match s1 with | Identity o1 - -> let rec compose_id o1 s o = match subst_subst' s with - | Identity o2 -> hcsb (Identity (o + o1 + o2)) + -> let rec compose_id o1 s o = match s with + | Identity o2 -> Identity (o + o1 + o2) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_id (o1 - sk2) s2' (o + o2') *) if o1 > 0 then compose_id (o1 - 1) s2 (o + o2) - else hcsb (Cons (e2, s2, o + o2)) + else Cons (e2, s2, o + o2) in compose_id o1 s2 0 | Cons (e1, s1, o1) - -> let rec compose_cons o1 s o = match subst_subst' s with - | Identity o2 -> hcsb (Cons (e1, s1, o + o1 + o2)) + -> let rec compose_cons o1 s o = match s with + | Identity o2 -> Cons (e1, s1, o + o1 + o2) | Cons (e2, s2, o2) (* , sk2, s2', o2' *) -> (* Myers's fastlane: * if o1 >= sk2 then compose_cons (o1 - sk1) s2' (o + o2') *) @@ -214,7 +197,7 @@ let compose (mkSusp : 'a -> subst -> 'a) else (* Pull out o2's shift and compose the two Cons. *) let s' = cons e2 s2 in - hcsb (Cons (mkSusp e1 s', compose' s1 s', o + o2)) + Cons (mkSusp e1 s', compose' s1 s', o + o2) in compose_cons o1 s2 0 in compose' s1 s2

@@ -222,7 +205,7 @@ let compose (mkSusp : 'a -> subst -> 'a) * I.e. take a substitution from Δs to Δₜ and return a substitution * from Δs,x to Δₜ,x. * Also known as `lift`. *) -let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:subst) = +let sink (mkVar : 'b -> db_index -> 'a) (l:'b) (s:'a subst) = cons (mkVar l 0) (mkShift s 1)

(* Return a substitution which replaces #0 with `e`. *)

===================================== src/unification.ml ===================================== @@ -19,7 +19,7 @@ more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/. *)

-open Lexp_type + open Lexp

(* open Sexp *) @@ -134,41 +134,41 @@ let occurs_in (id: meta_id) (e : lexp) : bool = match metavar_lookup id with *) let common_subset ctx (s1 : subst) (s2 : subst) = let rec loop (s1 : subst) (s2 : subst) o1 o2 o = - match (S.subst_subst' s1, S.subst_subst' s2) with - | (Cons (le1, s1', o1'), Cons (le2, s2', o2')) + match (s1, s2) with + | (S.Cons (le1, s1', o1'), S.Cons (le2, s2', o2')) -> let o1 = o1 + o1' in let o2 = o2 + o2' in (* FIXME: We should check if le1 and le2 are *unifiable* instead! *) if not (le1 = impossible || le1 = impossible) && OL.conv_p ctx (mkSusp le1 (S.shift o1)) (mkSusp le2 (S.shift o2)) then match loop s1' s2' o1 o2 1 with - | (Identity 1, _) -> S.hcsb (Identity o) (* Optimization! *) - | (sb, _) as s' -> S.hcsb (Cons (mkVar ((lexp_location le1, None), 0), - s', o)) + | S.Identity 1 -> S.Identity o (* Optimization! *) + | s' -> S.Cons (mkVar ((lexp_location le1, None), 0), + s', o) else loop s1' s2' o1 o2 (o + 1) (* If one of them reached `Identity`, unroll it, knowing that * * Identity 0 = #0 · #1 · #2 ... = #0 · (Identity 1) *) - | (Cons _, Identity o2') - -> loop s1 (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), - S.hcsb (Identity 1), o2'))) + | (S.Cons _, S.Identity o2') + -> loop s1 (S.Cons (mkVar ((U.dummy_location, None), 0), + S.Identity 1, o2')) o1 o2 o - | (Identity o1', Cons _) - -> loop (S.hcsb (Cons (mkVar ((U.dummy_location, None), 0), - S.hcsb (Identity 1), o1'))) + | (S.Identity o1', S.Cons _) + -> loop (S.Cons (mkVar ((U.dummy_location, None), 0), + S.Identity 1, o1')) s2 o1 o2 o - | (Identity o1', Identity o2') + | (S.Identity o1', S.Identity o2') -> assert (o1 + o1' = o2 + o2'); - S.hcsb (Identity o) + S.Identity o in loop s1 s2 0 0 0

(* Return the number of vars difference between input and output context. * * Could be returned directly by `common_subset`, but it's pretty easy to * compute it here instead. *) -let rec s_offset (s : subst) = match S.subst_subst' s with - | Identity o -> o - | Cons (_, s', o) -> o - 1 + s_offset s' +let rec s_offset (s : subst) = match s with + | S.Identity o -> o + | S.Cons (_, s', o) -> o - 1 + s_offset s'

(************************** Top level unify **********************************)

@@ -313,7 +313,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) | Metavar (idx2, s2, name) -> if idx = idx2 then match common_subset ctx s1 s2 with - | (Identity 0, _) -> [] (* Optimization! *) + | S.Identity 0 -> [] (* Optimization! *) (* ¡ s1 != s2 ! * Create a new metavar that can only refer to those vars * which are mapped identically by `s1` and `s2` @@ -321,7 +321,7 @@ and unify_metavar ctx idx s1 (lxp1: lexp) (lxp2: lexp) * This metavar doesn't necessarily live exactly in `ctx` * nor even a proper prefix of it, tho :-( !! *) - | (sb, _) as s -> + | s -> (* print_string "Metavar idx-idx s1!=s2\n"; *) assert (not (OL.conv_p ctx lxp1 lxp2)); match (Inverse_subst.inverse s,

===================================== src/util.ml ===================================== @@ -121,42 +121,17 @@ let option_map (fn : 'a -> 'b) (opt : 'a option) : 'b option =

let combine_hash e1 e2 = (e1 * 31) lxor e2

-let rec combine_hashes map = - match map with +let rec combine_hashes li = + match li with | [] -> 31 | e :: l -> combine_hash (e * 31) (combine_hashes l)

-let get_stats_hashtbl stats lshrct nf_lshrct = +let get_stats_hashtbl stats = let (tl, ne, sumb, smallb, medianb, bigb) = stats in Printf.printf "\n\ttable length: %i\n number of entries: %i\n sum of bucket lengths: %i\n smallest bucket length: %i\n median bucket length: %i\n - biggest bucket length: %i\n - 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 + biggest bucket length: %i\n" + tl ne sumb smallb medianb bigb

===================================== stats.txt deleted ===================================== @@ -1,111 +0,0 @@ -## 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/f807baf505996160fcc627eaaaead3329...