From cff2b4c05ce05f40625656722b57a943001a37cc Mon Sep 17 00:00:00 2001 From: brendanzab Date: Thu, 10 Nov 2022 16:29:38 +1100 Subject: [PATCH] Switch to an explicitly typed core language --- fathom/src/core.rs | 51 +-- fathom/src/core/pretty.rs | 41 +- fathom/src/core/semantics.rs | 37 +- fathom/src/surface/distillation.rs | 57 +-- fathom/src/surface/elaboration.rs | 50 ++- fathom/src/surface/elaboration/unification.rs | 29 +- formats/gif.snap | 2 +- formats/opentype.snap | 290 ++++++------ formats/unwrap-none.snap | 3 +- tests/cmd/fathom-norm.md | 2 +- tests/fail/elaboration/block-comment.snap | 2 +- .../mismatch/match-equation-body-exprs.snap | 2 +- .../unsolved/fun-literal-param-type.snap | 2 +- .../fun-literal-placeholder-body-type.snap | 2 +- ...l-identity-mono-input-ann-placeholder.snap | 2 +- ...-literal-identity-mono-input-ann-type.snap | 2 +- .../ann/fun-literal-identity-mono.snap | 2 +- ...teral-identity-poly-input-placeholder.snap | 2 +- .../ann/fun-literal-identity-poly-sugar.snap | 2 +- .../ann/fun-literal-identity-poly.snap | 2 +- .../fun-literal-placeholder-body-type.snap | 2 +- tests/succeed/bin-ops.snap | 12 +- tests/succeed/distillation/fresh-names.snap | 12 +- tests/succeed/equality.snap | 52 +-- tests/succeed/format-cond/simple.snap | 4 +- tests/succeed/format-overlap/dependent.snap | 13 +- .../format-overlap/field-refinements.snap | 4 +- tests/succeed/format-overlap/numbers.snap | 4 +- .../format-record/computed-fields.snap | 10 +- .../format-record/field-refinements.snap | 5 +- .../succeed/format-record/pair-dependent.snap | 4 +- tests/succeed/format-record/pair.snap | 2 +- tests/succeed/format-repr/coercions.snap | 5 +- tests/succeed/format-repr/pair-dependent.snap | 6 +- tests/succeed/format-repr/primitives.snap | 81 ++-- tests/succeed/format-repr/record.snap | 6 +- tests/succeed/format-repr/unit-literal.snap | 6 +- .../succeed/fun-elim/ann-identity-mono-0.snap | 2 +- .../succeed/fun-elim/ann-identity-mono-1.snap | 2 +- .../succeed/fun-elim/ann-identity-mono-2.snap | 2 +- .../succeed/fun-elim/ann-identity-poly-0.snap | 2 +- .../succeed/fun-elim/ann-identity-poly-1.snap | 2 +- tests/succeed/fun-elim/identity-mono-0.snap | 2 +- tests/succeed/fun-elim/identity-mono-1.snap | 2 +- tests/succeed/fun-literal/identity-mono.snap | 2 +- .../fun-literal/identity-poly-sugar.snap | 2 +- tests/succeed/fun-literal/identity-poly.snap | 2 +- tests/succeed/hole/hole-1.snap | 2 +- tests/succeed/if-then-else/pretty.snap | 6 +- tests/succeed/implicit-args/generalize.snap | 7 +- tests/succeed/implicit-args/insert-args.snap | 8 +- tests/succeed/implicit-args/specialize.snap | 21 +- tests/succeed/let/id-type.snap | 5 +- tests/succeed/let/identity-placeholders.snap | 8 +- tests/succeed/let/identity.snap | 8 +- .../succeed/let/let-def-placeholder-ann.snap | 2 +- tests/succeed/let/let-def-placeholder.snap | 2 +- tests/succeed/match/check-const-1.snap | 2 +- tests/succeed/match/check-const-2.snap | 2 +- tests/succeed/match/check-const-bool.snap | 2 +- .../succeed/match/check-const-redundant.snap | 2 +- .../succeed/match/check-simple-redundant.snap | 2 +- tests/succeed/match/check-simple.snap | 2 +- tests/succeed/match/synth-const-1.snap | 2 +- tests/succeed/match/synth-const-2.snap | 2 +- .../succeed/match/synth-simple-redundant.snap | 2 +- tests/succeed/match/synth-simple.snap | 2 +- tests/succeed/numeric-literal/styled.snap | 11 +- tests/succeed/ops-sugar.snap | 164 +++---- tests/succeed/prelude.snap | 111 +++-- tests/succeed/primitive-ops.snap | 16 +- tests/succeed/primitives.snap | 414 +++++++++--------- tests/succeed/raw-identifiers.snap | 2 +- tests/succeed/record-type/generic-pair.snap | 4 +- tests/succeed/record-type/generic-point.snap | 4 +- .../record-type/generic-singleton.snap | 4 +- tests/succeed/record-type/generic-triple.snap | 21 +- tests/succeed/stress.snap | 391 ++++++++++------- tests/succeed/tuple/check-format.snap | 10 +- tests/succeed/tuple/check-term.snap | 12 +- tests/succeed/tuple/check-universe.snap | 10 +- tests/succeed/tuple/generic-pair.snap | 4 +- tests/succeed/tuple/generic-triple.snap | 9 +- tests/succeed/tuple/synth.snap | 10 +- 84 files changed, 1096 insertions(+), 1020 deletions(-) diff --git a/fathom/src/core.rs b/fathom/src/core.rs index 11920930b..a6c71ba6f 100644 --- a/fathom/src/core.rs +++ b/fathom/src/core.rs @@ -140,15 +140,12 @@ pub enum Term<'arena> { // - https://lib.rs/crates/smallbitvec // - https://lib.rs/crates/bit-vec InsertedMeta(Span, Level, &'arena [LocalInfo]), - /// Annotated expressions. - Ann(Span, &'arena Term<'arena>, &'arena Term<'arena>), /// Let expressions. Let( Span, Option, &'arena Term<'arena>, &'arena Term<'arena>, - &'arena Term<'arena>, ), /// The type of types. @@ -167,7 +164,13 @@ pub enum Term<'arena> { /// Function literals. /// /// Also known as: lambda expressions, anonymous functions. - FunLit(Span, Plicity, Option, &'arena Term<'arena>), + FunLit( + Span, + Plicity, + Option, + &'arena Term<'arena>, + &'arena Term<'arena>, + ), /// Function applications. FunApp(Span, Plicity, &'arena Term<'arena>, &'arena Term<'arena>), @@ -208,26 +211,25 @@ impl<'arena> Term<'arena> { /// Get the source span of the term. pub fn span(&self) -> Span { match self { - Term::ItemVar(span, _) - | Term::LocalVar(span, _) - | Term::MetaVar(span, _) - | Term::InsertedMeta(span, _, _) - | Term::Ann(span, _, _) - | Term::Let(span, _, _, _, _) + Term::ItemVar(span, ..) + | Term::LocalVar(span, ..) + | Term::MetaVar(span, ..) + | Term::InsertedMeta(span, ..) + | Term::Let(span, ..) | Term::Universe(span) | Term::FunType(span, ..) | Term::FunLit(span, ..) | Term::FunApp(span, ..) - | Term::RecordType(span, _, _) - | Term::RecordLit(span, _, _) - | Term::RecordProj(span, _, _) + | Term::RecordType(span, ..) + | Term::RecordLit(span, ..) + | Term::RecordProj(span, ..) | Term::ArrayLit(span, _) - | Term::FormatRecord(span, _, _) - | Term::FormatCond(span, _, _, _) - | Term::FormatOverlap(span, _, _) - | Term::Prim(span, _) - | Term::ConstLit(span, _) - | Term::ConstMatch(span, _, _, _) => *span, + | Term::FormatRecord(span, ..) + | Term::FormatCond(span, ..) + | Term::FormatOverlap(span, ..) + | Term::Prim(span, ..) + | Term::ConstLit(span, ..) + | Term::ConstMatch(span, ..) => *span, } } @@ -242,16 +244,15 @@ impl<'arena> Term<'arena> { | Term::Prim(_, _) | Term::ConstLit(_, _) => false, - Term::Ann(_, expr, r#type) => expr.binds_local(var) || r#type.binds_local(var), - Term::Let(_, _, def_type, def_expr, body_expr) => { - def_type.binds_local(var) - || def_expr.binds_local(var) - || body_expr.binds_local(var.prev()) + Term::Let(_, _, def_expr, body_expr) => { + def_expr.binds_local(var) || body_expr.binds_local(var.prev()) } Term::FunType(.., param_type, body_type) => { param_type.binds_local(var) || body_type.binds_local(var.prev()) } - Term::FunLit(.., body_expr) => body_expr.binds_local(var.prev()), + Term::FunLit(.., param_type, body_expr) => { + param_type.binds_local(var) || body_expr.binds_local(var.prev()) + } Term::FunApp(.., head_expr, arg_expr) => { head_expr.binds_local(var) || arg_expr.binds_local(var) } diff --git a/fathom/src/core/pretty.rs b/fathom/src/core/pretty.rs index eb29956bb..65da06c0c 100644 --- a/fathom/src/core/pretty.rs +++ b/fathom/src/core/pretty.rs @@ -137,26 +137,13 @@ impl<'interner, 'arena> Context<'interner> { Term::InsertedMeta(_, level, info) => { RcDoc::text(format!("InsertedMeta({level:?}, {info:?})")) } - Term::Ann(_, expr, r#type) => self.paren( - prec > Prec::Top, - RcDoc::concat([ - RcDoc::concat([ - self.term_prec(Prec::Let, expr), - RcDoc::space(), - RcDoc::text(":"), - ]) - .group(), - RcDoc::softline(), - self.term_prec(Prec::Top, r#type), - ]), - ), - Term::Let(_, def_pattern, def_type, def_expr, body_expr) => self.paren( + Term::Let(_, def_pattern, def_expr, body_expr) => self.paren( prec > Prec::Let, RcDoc::concat([ RcDoc::concat([ RcDoc::text("let"), RcDoc::space(), - self.ann_pattern(Prec::Top, *def_pattern, def_type), + self.pattern(*def_pattern), RcDoc::space(), RcDoc::text("="), RcDoc::softline(), @@ -201,17 +188,29 @@ impl<'interner, 'arena> Context<'interner> { self.term_prec(Prec::Fun, body_type), ]), ), - Term::FunLit(_, plicity, param_name, body_expr) => self.paren( + Term::FunLit(_, plicity, param_name, param_type, body_expr) => self.paren( prec > Prec::Fun, RcDoc::concat([ RcDoc::concat([ RcDoc::text("fun"), RcDoc::space(), - self.plicity(*plicity), - match param_name { - Some(name) => self.string_id(*name), - None => RcDoc::text("_"), - }, + self.paren( + prec > Prec::Top, + RcDoc::concat([ + RcDoc::concat([ + self.plicity(*plicity), + match param_name { + Some(name) => self.string_id(*name), + None => RcDoc::text("_"), + }, + RcDoc::space(), + RcDoc::text(":"), + ]) + .group(), + RcDoc::softline(), + self.term_prec(Prec::Top, param_type), + ]), + ), RcDoc::space(), RcDoc::text("=>"), ]) diff --git a/fathom/src/core/semantics.rs b/fathom/src/core/semantics.rs index 8623e5aaf..87c8e5652 100644 --- a/fathom/src/core/semantics.rs +++ b/fathom/src/core/semantics.rs @@ -30,7 +30,7 @@ pub enum Value<'arena> { /// Dependent function types. FunType(Plicity, Option, ArcValue<'arena>, Closure<'arena>), /// Function literals. - FunLit(Plicity, Option, Closure<'arena>), + FunLit(Plicity, Option, ArcValue<'arena>, Closure<'arena>), /// Record types. RecordType(&'arena [StringId], Telescope<'arena>), @@ -298,8 +298,7 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { let head_expr = self.eval(&Term::MetaVar(*span, *var)); self.apply_local_infos(head_expr, local_infos) } - Term::Ann(span, expr, _) => Spanned::merge(*span, self.eval(expr)), - Term::Let(span, _, _, def_expr, body_expr) => { + Term::Let(span, _, def_expr, body_expr) => { let def_expr = self.eval(def_expr); self.local_exprs.push(def_expr); let body_expr = self.eval(body_expr); @@ -318,11 +317,12 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Closure::new(self.local_exprs.clone(), body_type), )), ), - Term::FunLit(span, plicity, param_name, body_expr) => Spanned::new( + Term::FunLit(span, plicity, param_name, param_type, body_expr) => Spanned::new( *span, Arc::new(Value::FunLit( *plicity, *param_name, + self.eval(param_type), Closure::new(self.local_exprs.clone(), body_expr), )), ), @@ -521,7 +521,7 @@ impl<'arena, 'env> ElimEnv<'arena, 'env> { ) -> ArcValue<'arena> { match Arc::make_mut(&mut head_expr) { // Beta-reduction - Value::FunLit(fun_plicity, _, body_expr) => { + Value::FunLit(fun_plicity, _, _, body_expr) => { assert_eq!(arg_plicity, *fun_plicity, "Plicities must be equal"); // FIXME: use span from head/arg exprs? self.apply_closure(body_expr, arg_expr) @@ -722,10 +722,11 @@ impl<'in_arena, 'env> QuoteEnv<'in_arena, 'env> { scope.to_scope(self.quote(scope, param_type)), self.quote_closure(scope, body_type), ), - Value::FunLit(plicity, param_name, body_expr) => Term::FunLit( + Value::FunLit(plicity, param_name, param_type, body_expr) => Term::FunLit( span, *plicity, *param_name, + scope.to_scope(self.quote(scope, param_type)), self.quote_closure(scope, body_expr), ), @@ -874,15 +875,9 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { Term::InsertedMeta(*span, *var, infos) } }, - Term::Ann(span, expr, r#type) => Term::Ann( - *span, - scope.to_scope(self.unfold_metas(scope, expr)), - scope.to_scope(self.unfold_metas(scope, r#type)), - ), - Term::Let(span, def_name, def_type, def_expr, body_expr) => Term::Let( + Term::Let(span, def_name, def_expr, body_expr) => Term::Let( *span, *def_name, - scope.to_scope(self.unfold_metas(scope, def_type)), scope.to_scope(self.unfold_metas(scope, def_expr)), self.unfold_bound_metas(scope, body_expr), ), @@ -896,10 +891,11 @@ impl<'arena, 'env> EvalEnv<'arena, 'env> { scope.to_scope(self.unfold_metas(scope, param_type)), self.unfold_bound_metas(scope, body_type), ), - Term::FunLit(span, plicity, param_name, body_expr) => Term::FunLit( + Term::FunLit(span, plicity, param_name, param_type, body_expr) => Term::FunLit( *span, *plicity, *param_name, + scope.to_scope(self.unfold_metas(scope, param_type)), self.unfold_bound_metas(scope, body_expr), ), @@ -1117,13 +1113,18 @@ impl<'arena, 'env> ConversionEnv<'arena, 'env> { && self.is_equal(param_type0, param_type1) && self.is_equal_closures(body_type0, body_type1) } - (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) => { - plicity0 == plicity1 && self.is_equal_closures(body_expr0, body_expr1) + ( + Value::FunLit(plicity0, _, param_type0, body_expr0), + Value::FunLit(plicity1, _, param_type1, body_expr1), + ) => { + plicity0 == plicity1 + && self.is_equal(param_type0, param_type1) + && self.is_equal_closures(body_expr0, body_expr1) } - (Value::FunLit(plicity, _, body_expr), _) => { + (Value::FunLit(plicity, .., body_expr), _) => { self.is_equal_fun_lit(*plicity, body_expr, &value1) } - (_, Value::FunLit(plicity, _, body_expr)) => { + (_, Value::FunLit(plicity, .., body_expr)) => { self.is_equal_fun_lit(*plicity, body_expr, &value0) } diff --git a/fathom/src/surface/distillation.rs b/fathom/src/surface/distillation.rs index e85eafe4a..3966faa9e 100644 --- a/fathom/src/surface/distillation.rs +++ b/fathom/src/surface/distillation.rs @@ -276,14 +276,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { fn check_prec(&mut self, prec: Prec, core_term: &core::Term<'_>) -> Term<'arena, ()> { match core_term { - core::Term::Ann(_span, expr, _) => { - // Avoid adding extraneous type annotations! - self.check_prec(prec, expr) - } - core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => { - let def_type = self.check_prec(Prec::Top, def_type); - let def_expr = self.check_prec(Prec::Let, def_expr); - + core::Term::Let(_, def_name, def_expr, body_expr) => { + let def_expr = self.check_prec(Prec::Top, def_expr); let def_name = self.freshen_name(*def_name, body_expr); let def_name = self.push_local(def_name); let def_pattern = name_to_pattern(def_name); @@ -295,7 +289,7 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { Term::Let( (), def_pattern, - Some(self.scope.to_scope(def_type)), + None, self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), ), @@ -303,21 +297,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { } core::Term::FunLit(..) => { let initial_local_len = self.local_len(); + let mut params = Vec::new(); let mut body_expr = core_term; - while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr { - let param_name = self.freshen_name(*param_name, next_body_expr); - params.push((*plicity, self.push_local(param_name))); + + while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr { + let r#type = self.check(r#type); + let name = self.freshen_name(*name, next_body_expr); + params.push((*plicity, self.push_local(name), r#type)); body_expr = next_body_expr; } let body_expr = self.check_prec(Prec::Let, body_expr); self.truncate_local(initial_local_len); - let params = params.into_iter().map(|(plicity, name)| Param { + let params = params.into_iter().map(|(plicity, name, r#type)| Param { plicity, pattern: name_to_pattern(name), - r#type: None, + r#type: Some(r#type), }); self.paren( @@ -492,21 +489,11 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { self.paren(prec > Prec::App, Term::App((), head_expr, args.into())) } } - core::Term::Ann(_span, expr, r#type) => { - let expr = self.check_prec(Prec::Let, expr); - let r#type = self.check_prec(Prec::Top, r#type); - - self.paren( - prec > Prec::Top, - Term::Ann((), self.scope.to_scope(expr), self.scope.to_scope(r#type)), - ) - } - core::Term::Let(_span, def_name, def_type, def_expr, body_expr) => { - let def_type = self.check_prec(Prec::Top, def_type); - let def_expr = self.check_prec(Prec::Let, def_expr); - + core::Term::Let(_, def_name, def_expr, body_expr) => { + let def_expr = self.check_prec(Prec::Top, def_expr); let def_name = self.freshen_name(*def_name, body_expr); let def_name = self.push_local(def_name); + let def_pattern = name_to_pattern(def_name); let body_expr = self.synth_prec(Prec::Let, body_expr); self.pop_local(); @@ -514,8 +501,8 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { prec > Prec::Let, Term::Let( (), - name_to_pattern(def_name), - Some(self.scope.to_scope(def_type)), + def_pattern, + None, self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), ), @@ -581,22 +568,24 @@ impl<'interner, 'arena, 'env> Context<'interner, 'arena, 'env> { } core::Term::FunLit(..) => { let initial_local_len = self.local_len(); + let mut params = Vec::new(); let mut body_expr = core_term; - while let core::Term::FunLit(_, plicity, param_name, next_body_expr) = body_expr { - let param_name = self.freshen_name(*param_name, next_body_expr); - params.push((*plicity, self.push_local(param_name))); + while let core::Term::FunLit(_, plicity, name, r#type, next_body_expr) = body_expr { + let r#type = self.check(r#type); + let name = self.freshen_name(*name, next_body_expr); + params.push((*plicity, self.push_local(name), r#type)); body_expr = next_body_expr; } let body_expr = self.synth_prec(Prec::Let, body_expr); self.truncate_local(initial_local_len); - let params = params.into_iter().map(|(plicity, name)| Param { + let params = params.into_iter().map(|(plicity, name, r#type)| Param { plicity, pattern: name_to_pattern(name), - r#type: None, + r#type: Some(r#type), }); self.paren( diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 712f419d1..47c19b09c 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -921,7 +921,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { match r#type { None => { let (pattern, type_value) = self.synth_pattern(pattern); - let r#type = self.quote_env().quote(self.scope, &type_value); + let r#type = self.quote_env().quote(self.scope, &type_value); // FIXME: don't quote in let elaboration (pattern, r#type, type_value) } Some(r#type) => { @@ -1014,7 +1014,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { match (surface_term, expected_type.as_ref()) { (Term::Paren(_, term), _) => self.check(term, &expected_type), (Term::Let(_, def_pattern, def_type, def_expr, body_expr), _) => { - let (def_pattern, def_type, def_type_value) = + let (def_pattern, _, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); let def_expr = self.check(def_expr, &def_type_value); let def_expr_value = self.eval_env().eval(&def_expr); @@ -1026,7 +1026,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> { core::Term::Let( file_range.into(), def_name, - self.scope.to_scope(def_type), self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), ) @@ -1344,7 +1343,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { ) -> (core::Term<'arena>, ArcValue<'arena>) { let (term, r#type) = self.synth(surface_term); match term { - core::Term::FunLit(_, Plicity::Implicit, _, _) => (term, r#type), + core::Term::FunLit(_, Plicity::Implicit, ..) => (term, r#type), term => self.insert_implicit_apps(surface_term.range(), term, r#type), } } @@ -1410,18 +1409,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> { Term::Ann(_, expr, r#type) => { let r#type = self.check(r#type, &self.universe.clone()); let type_value = self.eval_env().eval(&r#type); - let expr = self.check(expr, &type_value); - let ann_expr = core::Term::Ann( - file_range.into(), - self.scope.to_scope(expr), - self.scope.to_scope(r#type), - ); - - (ann_expr, type_value) + (self.check(expr, &type_value), type_value) } Term::Let(_, def_pattern, def_type, def_expr, body_expr) => { - let (def_pattern, def_type, def_type_value) = + let (def_pattern, _, def_type_value) = self.synth_ann_pattern(def_pattern, *def_type); let def_expr = self.check(def_expr, &def_type_value); let def_expr_value = self.eval_env().eval(&def_expr); @@ -1433,7 +1425,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> { let let_expr = core::Term::Let( file_range.into(), def_name, - self.scope.to_scope(def_type), self.scope.to_scope(def_expr), self.scope.to_scope(body_expr), ); @@ -1783,16 +1774,18 @@ impl<'interner, 'arena> Context<'interner, 'arena> { Some((param, next_params)) => { let body_type = self.elim_env().force(expected_type); match body_type.as_ref() { - Value::FunType(param_plicity, _, param_type, next_body_type) + Value::FunType(param_plicity, _, param_type_value, next_body_type) if param.plicity == *param_plicity => { let range = ByteRange::merge(param.pattern.range(), body_expr.range()); let pattern = self.check_ann_pattern( ¶m.pattern, param.r#type.as_ref(), - param_type, + param_type_value, ); - let (name, arg_expr) = self.push_local_param(pattern, param_type.clone()); + let param_type = self.quote_env().quote(self.scope, param_type_value); + let (name, arg_expr) = + self.push_local_param(pattern, param_type_value.clone()); let body_type = self.elim_env().apply_closure(next_body_type, arg_expr); let body_expr = @@ -1803,22 +1796,31 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.file_range(range).into(), param.plicity, name, + self.scope.to_scope(param_type), self.scope.to_scope(body_expr), ) } // If an implicit function is expected, try to generalize the // function literal by wrapping it in an implicit function - Value::FunType(Plicity::Implicit, param_name, param_type, next_body_type) - if param.plicity == Plicity::Explicit => - { - let arg_expr = self.local_env.push_param(*param_name, param_type.clone()); + Value::FunType( + Plicity::Implicit, + param_name, + param_type_value, + next_body_type, + ) if param.plicity == Plicity::Explicit => { + let param_type = self.quote_env().quote(self.scope, param_type_value); + let arg_expr = self + .local_env + .push_param(*param_name, param_type_value.clone()); let body_type = self.elim_env().apply_closure(next_body_type, arg_expr); let body_expr = self.check_fun_lit(range, params, body_expr, &body_type); self.local_env.pop(); + core::Term::FunLit( file_range.into(), Plicity::Implicit, *param_name, + self.scope.to_scope(param_type), self.scope.to_scope(body_expr), ) } @@ -1881,17 +1883,19 @@ impl<'interner, 'arena> Context<'interner, 'arena> { _ => ByteRange::merge(param_range, body_expr.range()), }; + let r#type = self.scope.to_scope(r#type); fun_lit = core::Term::FunLit( self.file_range(range).into(), plicity, name, + r#type, self.scope.to_scope(fun_lit), ); fun_type = core::Term::FunType( Span::Empty, plicity, name, - self.scope.to_scope(r#type), + r#type, self.scope.to_scope(fun_type), ); } @@ -2210,7 +2214,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> { let def_name = Some(name); let def_expr = self.eval_env().eval(match_info.scrutinee.expr); let def_type_value = match_info.scrutinee.r#type.clone(); - let def_type = self.quote_env().quote(self.scope, &def_type_value); self.local_env.push_def(def_name, def_expr, def_type_value); let body_expr = self.check(body_expr, &match_info.expected_type); @@ -2221,7 +2224,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> { core::Term::Let( Span::merge(&range.into(), &body_expr.span()), def_name, - self.scope.to_scope(def_type), match_info.scrutinee.expr, self.scope.to_scope(body_expr), ) diff --git a/fathom/src/surface/elaboration/unification.rs b/fathom/src/surface/elaboration/unification.rs index ae9e47ee2..f10f86f97 100644 --- a/fathom/src/surface/elaboration/unification.rs +++ b/fathom/src/surface/elaboration/unification.rs @@ -23,10 +23,9 @@ use crate::alloc::SliceVec; use crate::core::semantics::{ self, ArcValue, Branches, Closure, Elim, Head, SplitBranches, Telescope, Value, }; -use crate::core::{Prim, Term}; +use crate::core::{Plicity, Prim, Term}; use crate::env::{EnvLen, Index, Level, SharedEnv, SliceEnv, UniqueEnv}; -use crate::source::{Spanned, StringId}; -use crate::surface::Plicity; +use crate::source::{Span, Spanned, StringId}; /// Errors encountered during unification. /// @@ -238,15 +237,17 @@ impl<'arena, 'env> Context<'arena, 'env> { self.unify(param_type0, param_type1)?; self.unify_closures(body_type0, body_type1) } - (Value::FunLit(plicity0, _, body_expr0), Value::FunLit(plicity1, _, body_expr1)) - if plicity0 == plicity1 => - { + ( + Value::FunLit(plicity0, _, param_type0, body_expr0), + Value::FunLit(plicity1, _, param_type1, body_expr1), + ) if plicity0 == plicity1 => { + self.unify(param_type0, param_type1)?; self.unify_closures(body_expr0, body_expr1) } - (Value::FunLit(plicity, _, body_expr), _) => { + (Value::FunLit(plicity, .., body_expr), _) => { self.unify_fun_lit(*plicity, body_expr, &value1) } - (_, Value::FunLit(plicity, _, body_expr)) => { + (_, Value::FunLit(plicity, .., body_expr)) => { self.unify_fun_lit(*plicity, body_expr, &value0) } @@ -517,9 +518,15 @@ impl<'arena, 'env> Context<'arena, 'env> { /// Wrap a `term` in [function literals][Term::FunLit] that /// correspond to the given `spine`. fn fun_intros(&self, spine: &[Elim<'arena>], term: Term<'arena>) -> Term<'arena> { + // These functions literals should be eliminated after the metavariables + // have been unfolded, so just use error sentinels to avoid having to + // look up the corresponding type annotation for each parameter. + const PARAM_TYPE: Term<'static> = Term::Prim(Span::Empty, Prim::ReportedError); + + let span = term.span(); spine.iter().fold(term, |term, elim| match elim { Elim::FunApp(plicity, _) => { - Term::FunLit(term.span(), *plicity, None, self.scope.to_scope(term)) + Term::FunLit(span, *plicity, None, &PARAM_TYPE, self.scope.to_scope(term)) } Elim::RecordProj(_) | Elim::ConstMatch(_) => { unreachable!("should have been caught by `init_renaming`") @@ -615,13 +622,15 @@ impl<'arena, 'env> Context<'arena, 'env> { self.scope.to_scope(body_type), )) } - Value::FunLit(plicity, param_name, body_expr) => { + Value::FunLit(plicity, param_name, param_type, body_expr) => { + let param_type = self.rename(meta_var, param_type)?; let body_expr = self.rename_closure(meta_var, body_expr)?; Ok(Term::FunLit( span, *plicity, *param_name, + self.scope.to_scope(param_type), self.scope.to_scope(body_expr), )) } diff --git a/formats/gif.snap b/formats/gif.snap index 422a9e181..9025f5f77 100644 --- a/formats/gif.snap +++ b/formats/gif.snap @@ -11,7 +11,7 @@ def header : Format = { version <- repeat_len8 3 u8, }; def color_table_entry : Format = { red <- u8, green <- u8, blue <- u8 }; -def global_color_table : U16 -> Format = fun len => { +def global_color_table : U16 -> Format = fun (len : U16) => { entries <- repeat_len16 len color_table_entry, }; def main : Format = { header <- header, screen <- logical_screen_descriptor }; diff --git a/formats/opentype.snap b/formats/opentype.snap index 9596e81c9..08d256440 100644 --- a/formats/opentype.snap +++ b/formats/opentype.snap @@ -16,42 +16,55 @@ def find_table : fun (@num_tables : U16) -> Array16 num_tables { checksum : U32, offset : U32, length : U32, -} = fun @num_tables table_records table_id => array16_find @num_tables @{ +} = fun (@num_tables : U16) (table_records : +Array16 num_tables (Repr table_record)) (table_id : +Repr tag) => array16_find @num_tables @{ table_id : U32, checksum : U32, offset : U32, length : U32, -} (fun table_record => table_record.table_id == table_id) table_records; +} (fun (table_record : { + table_id : U32, + checksum : U32, + offset : U32, + length : U32, +}) => table_record.table_id == table_id) table_records; def link_table : Pos -> { table_id : U32, checksum : U32, offset : U32, length : U32, -} -> Format -> Format = -fun file_start table_record table_format => link (file_start + table_record.offset) (limit32 table_record.length table_format); +} -> Format -> Format = fun (file_start : Pos) (table_record : +Repr table_record) (table_format : +Format) => link (file_start + table_record.offset) (limit32 table_record.length table_format); def platform_id : Format = u16be; -def encoding_id : Repr platform_id -> Format = fun platform => u16be; +def encoding_id : Repr platform_id -> Format = fun (platform : +Repr platform_id) => u16be; def empty : Format = (); -def offset32 : Pos -> Format -> Format = fun base format => { +def offset32 : Pos -> Format -> Format = fun (base : Pos) (format : Format) => { offset <- u32be, link <- match offset { 0 => empty, _ => link (base + offset) format }, }; def language_id : Format = u16be; -def cmap_language_id : Repr platform_id -> Format = fun platform => language_id; +def cmap_language_id : Repr platform_id -> Format = fun (platform : +Repr platform_id) => language_id; def small_glyph_id : Format = u8; -def cmap_subtable_format0 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format0 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { length <- u16be, language <- cmap_language_id platform, glyph_id_array <- repeat_len16 256 small_glyph_id, }; -def cmap_subtable_format2 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format2 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { length <- u16be, language <- cmap_language_id platform, sub_header_keys <- repeat_len16 256 u16be, }; -def reserved : fun (format : Format) -> Repr format -> Format = -fun format default => format; -def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => { +def reserved : fun (format : Format) -> Repr format -> Format = fun (format : +Format) (default : Repr format) => format; +def cmap_subtable_format4 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { length <- u16be, language <- cmap_language_id platform, seg_count_x2 <- u16be, @@ -65,7 +78,8 @@ def cmap_subtable_format4 : Repr platform_id -> Format = fun platform => { id_delta <- repeat_len16 seg_count s16be, id_range_offsets <- repeat_len16 seg_count u16be, }; -def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format6 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { length <- u16be, language <- cmap_language_id platform, first_code <- u16be, @@ -73,14 +87,15 @@ def cmap_subtable_format6 : Repr platform_id -> Format = fun platform => { glyph_id_array <- repeat_len16 entry_count u16be, }; def language_id32 : Format = u32be; -def cmap_language_id32 : Repr platform_id -> Format = -fun platform => language_id32; +def cmap_language_id32 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => language_id32; def sequential_map_group : Format = { start_char_code <- u32be, end_char_code <- u32be, start_glyph_id <- u32be, }; -def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format8 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -88,7 +103,8 @@ def cmap_subtable_format8 : Repr platform_id -> Format = fun platform => { num_groups <- u32be, groups <- repeat_len32 num_groups sequential_map_group, }; -def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format10 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -96,7 +112,8 @@ def cmap_subtable_format10 : Repr platform_id -> Format = fun platform => { num_chars <- u32be, glyph_id_array <- repeat_len32 num_chars u16be, }; -def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format12 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -104,7 +121,8 @@ def cmap_subtable_format12 : Repr platform_id -> Format = fun platform => { groups <- repeat_len32 num_groups sequential_map_group, }; def constant_map_group : Format = sequential_map_group; -def cmap_subtable_format13 : Repr platform_id -> Format = fun platform => { +def cmap_subtable_format13 : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { _reserved <- reserved u16be 0, length <- u32be, language <- cmap_language_id32 platform, @@ -125,19 +143,20 @@ def non_default_uvs_table : Format = { num_uvs_mappings <- u32be, uvs_mappings <- repeat_len32 num_uvs_mappings uvs_mapping, }; -def variation_selector : Pos -> Format = fun table_start => { +def variation_selector : Pos -> Format = fun (table_start : Pos) => { var_selector <- u24be, default_uvs_offset <- offset32 table_start default_uvs_table, non_default_uvs_offset <- offset32 table_start non_default_uvs_table, }; -def cmap_subtable_format14 : Repr platform_id -> Pos -> Format = -fun platform table_start => { +def cmap_subtable_format14 : Repr platform_id -> Pos -> Format = fun (platform : +Repr platform_id) (table_start : Pos) => { length <- u32be, num_var_selector_records <- u32be, var_selector <- repeat_len32 num_var_selector_records (variation_selector table_start), }; def unknown_table : Format = (); -def cmap_subtable : Repr platform_id -> Format = fun platform => { +def cmap_subtable : Repr platform_id -> Format = fun (platform : +Repr platform_id) => { table_start <- stream_pos, format <- u16be, data <- match format { @@ -153,7 +172,7 @@ def cmap_subtable : Repr platform_id -> Format = fun platform => { _ => unknown_table, }, }; -def encoding_record : Pos -> Format = fun table_start => { +def encoding_record : Pos -> Format = fun (table_start : Pos) => { platform <- platform_id, encoding <- encoding_id platform, subtable_offset <- offset32 table_start (cmap_subtable platform), @@ -166,8 +185,8 @@ def cmap_table : Format = { }; def fixed : Format = u32be; def long_date_time : Format = s64be; -def deprecated : fun (format : Format) -> Repr format -> Format = -fun format default => format; +def deprecated : fun (format : Format) -> Repr format -> Format = fun (format : +Format) (default : Repr format) => format; def head_table : Format = { major_version <- u16be where major_version == (1 : U16), minor_version <- u16be, @@ -237,16 +256,16 @@ def long_horizontal_metric : Format = { advance_width <- u16be, left_side_bearing <- s16be, }; -def htmx_table : U16 -> U16 -> Format = -fun number_of_long_horizontal_metrics num_glyphs => { +def htmx_table : U16 -> U16 -> Format = fun (number_of_long_horizontal_metrics : +U16) (num_glyphs : U16) => { h_metrics <- repeat_len16 number_of_long_horizontal_metrics long_horizontal_metric, left_side_bearings <- repeat_len16 (num_glyphs - number_of_long_horizontal_metrics) s16be, }; -def offset16 : Pos -> Format -> Format = fun base format => { +def offset16 : Pos -> Format -> Format = fun (base : Pos) (format : Format) => { offset <- u16be, link <- match offset { 0 => empty, _ => link (base + offset) format }, }; -def name_record : Pos -> Format = fun storage_start => { +def name_record : Pos -> Format = fun (storage_start : Pos) => { platform <- platform_id, encoding <- encoding_id platform, language <- language_id, @@ -254,11 +273,11 @@ def name_record : Pos -> Format = fun storage_start => { length <- u16be, offset <- offset16 storage_start (repeat_len16 length u8), }; -def lang_tag_record : Pos -> Format = fun storage_start => { +def lang_tag_record : Pos -> Format = fun (storage_start : Pos) => { length <- u16be, offset <- offset16 storage_start (repeat_len16 length u8), }; -def name_version_1 : Pos -> Format = fun storage_start => { +def name_version_1 : Pos -> Format = fun (storage_start : Pos) => { lang_tag_count <- u16be, lang_tag_records <- repeat_len16 lang_tag_count (lang_tag_record storage_start), }; @@ -299,7 +318,7 @@ def os2_version_5 : Format = { usLowerOpticalPointSize <- u16be, usUpperOpticalPointSize <- u16be, }; -def os2_table : U32 -> Format = fun table_length => { +def os2_table : U32 -> Format = fun (table_length : U32) => { version <- u16be, x_avg_char_width <- s16be, us_weight_class <- u16be, @@ -367,8 +386,10 @@ def glyph_header : Format = { x_max <- s16be, y_max <- s16be, }; -def args_are_signed : U16 -> Bool = fun flags => u16_and flags 0x2 != (0 : U16); -def arg_format : U16 -> Format = fun flags => if u16_and flags 0x1 != (0 : U16) +def args_are_signed : U16 -> Bool = fun (flags : +U16) => u16_and flags 0x2 != (0 : U16); +def arg_format : U16 -> Format = fun (flags : +U16) => if u16_and flags 0x1 != (0 : U16) then if args_are_signed flags then s16be else u16be else if args_are_signed flags then s8 else u8; @@ -378,7 +399,7 @@ def composite_glyph : Format = { argument1 <- arg_format flags, argument2 <- arg_format flags, }; -def simple_glyph : U16 -> Format = fun number_of_contours => { +def simple_glyph : U16 -> Format = fun (number_of_contours : U16) => { end_pts_of_contours <- repeat_len16 number_of_contours u16be, instruction_length <- u16be, instructions <- repeat_len16 instruction_length u8, @@ -392,10 +413,11 @@ def glyph : Format = { then composite_glyph else simple_glyph (s16_unsigned_abs header.number_of_contours), }; -def glyf_table : U16 -> Format = fun num_glyphs => { +def glyf_table : U16 -> Format = fun (num_glyphs : U16) => { glyphs <- repeat_len16 num_glyphs glyph, }; -def loca_table : U16 -> S16 -> Format = fun num_glyphs index_to_loc_format => { +def loca_table : U16 -> S16 -> Format = fun (num_glyphs : +U16) (index_to_loc_format : S16) => { offsets <- match index_to_loc_format { 0 => repeat_len16 (num_glyphs + (1 : U16)) u16be, 1 => repeat_len16 (num_glyphs + (1 : U16)) u32be, @@ -407,7 +429,7 @@ def coverage_format_1 : Format = { glyph_count <- u16be, glyph_array <- repeat_len16 glyph_count u16be, }; -def coverage_format_2 : Format = let range_record : Format = { +def coverage_format_2 : Format = let range_record = { start_glyph_id <- u16be, end_glyph_id <- u16be, start_coverage_index <- u16be, @@ -435,7 +457,7 @@ def class_def_format_1 : Format = { glyph_count <- u16be, class_value_array <- repeat_len16 glyph_count u16be, }; -def class_def_format_2 : Format = let class_range_record : Format = { +def class_def_format_2 : Format = let class_range_record = { start_glyph_id <- u16be, end_glyph_id <- u16be, class <- u16be, @@ -452,7 +474,7 @@ def class_def : Format = { _ => unknown_table, }, }; -def attach_list : Format = let attach_point_table : Format = { +def attach_list : Format = let attach_point_table = { point_count <- u16be, point_indices <- repeat_len16 point_count u16be, }; @@ -462,22 +484,22 @@ def attach_list : Format = let attach_point_table : Format = { glyph_count <- u16be, attach_point_offsets <- repeat_len16 glyph_count (offset16 table_start attach_point_table), }; -def device_table : Format = let u16_div_ceil : U16 -> U16 -> U16 = -fun numerator denominator => let quotient : U16 = numerator / denominator; +def device_table : Format = let u16_div_ceil = fun (numerator : +U16) (denominator : U16) => let quotient = numerator / denominator; if (quotient * denominator) < numerator then quotient + (1 : U16) else quotient; -let delta_bits : U16 -> U16 -> U16 = -fun delta_format num_sizes => match delta_format { +let delta_bits = fun (delta_format : U16) (num_sizes : +U16) => match delta_format { 0x1 => num_sizes * (2 : U16), 0x2 => num_sizes * (4 : U16), 0x3 => num_sizes * (8 : U16), _ => 0, }; -let num_sizes : U16 -> U16 -> U16 = fun start end => end - start + (1 : U16); +let num_sizes = fun (start : U16) (end : U16) => end - start + (1 : U16); { start_size <- u16be, end_size <- u16be, delta_format <- u16be, - delta_values <- let delta_bits : U16 = + delta_values <- let delta_bits = delta_bits delta_format (num_sizes start_size end_size); repeat_len16 (u16_div_ceil delta_bits 16) u16be, }; @@ -495,11 +517,9 @@ def device_or_variation_index_table : Format = overlap { _ => unknown_table, }, }; -def caret_value : Format = let caret_value_format_1 : Format = { - coordinate <- s16be, -}; -let caret_value_format_2 : Format = { caret_value_point_index <- u16be }; -let caret_value_format_3 : Pos -> Format = fun table_start => { +def caret_value : Format = let caret_value_format_1 = { coordinate <- s16be }; +let caret_value_format_2 = { caret_value_point_index <- u16be }; +let caret_value_format_3 = fun (table_start : Pos) => { coordinate <- s16be, table <- offset16 table_start device_or_variation_index_table, }; @@ -524,11 +544,9 @@ def lig_caret_list : Format = { lig_glyph_count <- u16be, lig_glyph_offsets <- repeat_len16 lig_glyph_count (offset16 table_start lig_glyph), }; -def gdef_table : Format = let gdef_header_version_1_2 : Pos -> Format = -fun gdef_start => { - mark_glyph_sets_def <- offset16 gdef_start mark_glyph_sets, -}; -let gdef_header_version_1_3 : Pos -> Format = fun gdef_start => { +def gdef_table : Format = let gdef_header_version_1_2 = fun (gdef_start : +Pos) => { mark_glyph_sets_def <- offset16 gdef_start mark_glyph_sets }; +let gdef_header_version_1_3 = fun (gdef_start : Pos) => { item_var_store <- u32be, }; { @@ -553,7 +571,7 @@ def lang_sys : Format = { feature_index_count <- u16be, feature_indices <- repeat_len16 feature_index_count u16be, }; -def lang_sys_record : Pos -> Format = fun script_start => { +def lang_sys_record : Pos -> Format = fun (script_start : Pos) => { lang_sys_tag <- tag, lang_sys <- offset16 script_start lang_sys, }; @@ -563,8 +581,8 @@ def script_table : Format = { lang_sys_count <- u16be, lang_sys_records <- repeat_len16 lang_sys_count (lang_sys_record table_start), }; -def script_list : Format = let script_record : Pos -> Format = -fun script_list_start => { +def script_list : Format = let script_record = fun (script_list_start : +Pos) => { script_tag <- tag, script <- offset16 script_list_start script_table, }; @@ -579,8 +597,8 @@ def feature_table : Format = { lookup_index_count <- u16be, lookup_list_indices <- repeat_len16 lookup_index_count u16be, }; -def feature_list : Format = let feature_record : Pos -> Format = -fun feature_list_start => { +def feature_list : Format = let feature_record = fun (feature_list_start : +Pos) => { feature_tag <- tag, feature <- offset16 feature_list_start feature_table, }; @@ -605,7 +623,7 @@ def single_substitution : Format = { _ => unknown_table, }, }; -def multiple_substitution : Format = let sequence_table : Format = { +def multiple_substitution : Format = let sequence_table = { glyph_count <- u16be, substitute_glyph_ids <- repeat_len16 glyph_count u16be, }; @@ -621,7 +639,7 @@ def multiple_substitution : Format = let sequence_table : Format = { _ => unknown_table, }, }; -def alternate_substitution : Format = let alternate_set : Format = { +def alternate_substitution : Format = let alternate_set = { glyph_count <- u16be, alternate_glyph_ids <- repeat_len16 glyph_count u16be, }; @@ -637,12 +655,12 @@ def alternate_substitution : Format = let alternate_set : Format = { _ => unknown_table, }, }; -def ligature_substitution : Format = let ligature_table : Format = { +def ligature_substitution : Format = let ligature_table = { ligature_glyph <- u16be, component_count <- u16be, component_glyph_ids <- repeat_len16 (component_count - (1 : U16)) u16be, }; -let ligature_set : Format = { +let ligature_set = { table_start <- stream_pos, ligature_count <- u16be, ligatures <- repeat_len16 ligature_count (offset16 table_start ligature_table), @@ -663,13 +681,13 @@ def sequence_lookup_record : Format = { sequence_index <- u16be, lookup_list_index <- u16be, }; -def sequence_context_format1 : Format = let sequence_rule : Format = { +def sequence_context_format1 : Format = let sequence_rule = { glyph_count <- u16be, seq_lookup_count <- u16be, input_sequence <- repeat_len16 (glyph_count - (1 : U16)) u16be, seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, }; -let sequence_rule_set : Format = { +let sequence_rule_set = { table_start <- stream_pos, seq_rule_count <- u16be, seq_rules <- repeat_len16 seq_rule_count (offset16 table_start sequence_rule), @@ -680,13 +698,13 @@ let sequence_rule_set : Format = { seq_rule_set_count <- u16be, seq_rule_sets <- repeat_len16 seq_rule_set_count (offset16 table_start sequence_rule_set), }; -def sequence_context_format2 : Format = let class_sequence_rule : Format = { +def sequence_context_format2 : Format = let class_sequence_rule = { glyph_count <- u16be, seq_lookup_count <- u16be, input_sequence <- repeat_len16 (glyph_count - (1 : U16)) u16be, seqLookupRecords <- repeat_len16 seq_lookup_count sequence_lookup_record, }; -let class_sequence_rule_set : Format = { +let class_sequence_rule_set = { table_start <- stream_pos, class_seq_rule_count <- u16be, class_seq_rules <- repeat_len16 class_seq_rule_count (offset16 table_start class_sequence_rule), @@ -726,7 +744,7 @@ def chained_sequence_context : Format = { }; def chained_contexts_substitution : Format = chained_sequence_context; def reverse_chaining_contextual_single_substitution : Format = -let reverse_chain_single_subst_format1 : Format = { +let reverse_chain_single_subst_format1 = { table_start <- stream_pos, coverage <- offset16 table_start coverage_table, backtrack_glyph_count <- u16be, @@ -743,7 +761,7 @@ let reverse_chain_single_subst_format1 : Format = { _ => unknown_table, }, }; -def extension_substitution : Format = let extension_subst_format1 : Format = { +def extension_substitution : Format = let extension_subst_format1 = { table_start <- stream_pos, extension_lookup_type <- u16be, extension_subtable <- match extension_lookup_type { @@ -765,17 +783,17 @@ def extension_substitution : Format = let extension_subst_format1 : Format = { _ => unknown_table, }, }; -def value_record : Pos -> U16 -> Format = -fun table_start flags => let X_PLACEMENT : U16 = 0x1; -let Y_PLACEMENT : U16 = 0x2; -let X_ADVANCE : U16 = 0x4; -let Y_ADVANCE : U16 = 0x8; -let X_PLACEMENT_DEVICE : U16 = 0x10; -let Y_PLACEMENT_DEVICE : U16 = 0x20; -let X_ADVANCE_DEVICE : U16 = 0x40; -let Y_ADVANCE_DEVICE : U16 = 0x80; -let optional_field : U16 -> Format -> Format = -fun field format => if u16_and flags field != (0 : U16) then format else empty; +def value_record : Pos -> U16 -> Format = fun (table_start : Pos) (flags : +U16) => let X_PLACEMENT = 0x1; +let Y_PLACEMENT = 0x2; +let X_ADVANCE = 0x4; +let Y_ADVANCE = 0x8; +let X_PLACEMENT_DEVICE = 0x10; +let Y_PLACEMENT_DEVICE = 0x20; +let X_ADVANCE_DEVICE = 0x40; +let Y_ADVANCE_DEVICE = 0x80; +let optional_field = fun (field : U16) (format : +Format) => if u16_and flags field != (0 : U16) then format else empty; { x_placement <- optional_field X_PLACEMENT s16be, y_placement <- optional_field Y_PLACEMENT s16be, @@ -786,13 +804,13 @@ fun field format => if u16_and flags field != (0 : U16) then format else empty; x_adv_device_offset <- optional_field X_ADVANCE_DEVICE (offset16 table_start device_or_variation_index_table), y_adv_device_offset <- optional_field Y_ADVANCE_DEVICE (offset16 table_start device_or_variation_index_table), }; -def single_adjustment : Format = let single_pos_format1 : Pos -> Format = -fun table_start => { +def single_adjustment : Format = let single_pos_format1 = fun (table_start : +Pos) => { coverage_offset <- offset16 table_start coverage_table, value_format <- u16be, value_record <- value_record table_start value_format, }; -let single_pos_format2 : Pos -> Format = fun table_start => { +let single_pos_format2 = fun (table_start : Pos) => { coverage_offset <- offset16 table_start coverage_table, value_format <- u16be, value_count <- u16be, @@ -807,38 +825,38 @@ let single_pos_format2 : Pos -> Format = fun table_start => { _ => unknown_table, }, }; -def optional_value_record : Pos -> U16 -> Format = -fun table_start flags => if flags == (0 : U16) +def optional_value_record : Pos -> U16 -> Format = fun (table_start : +Pos) (flags : U16) => if flags == (0 : U16) then empty else value_record table_start flags; -def pair_adjustment : Format = let pair_value_record : Pos -> U16 -> U16 -> -Format = fun table_start value_format1 value_format2 => { +def pair_adjustment : Format = let pair_value_record = fun (table_start : +Pos) (value_format1 : U16) (value_format2 : U16) => { second_glyph <- u16be, value_record1 <- optional_value_record table_start value_format1, value_record2 <- optional_value_record table_start value_format2, }; -let pair_set : U16 -> U16 -> Format = fun value_format1 value_format2 => { +let pair_set = fun (value_format1 : U16) (value_format2 : U16) => { table_start <- stream_pos, pair_value_count <- u16be, pair_value_records <- repeat_len16 pair_value_count (pair_value_record table_start value_format1 value_format2), }; -let pair_pos_format1 : Pos -> Format = fun table_start => { +let pair_pos_format1 = fun (table_start : Pos) => { coverage <- offset16 table_start coverage_table, value_format1 <- u16be, value_format2 <- u16be, pair_set_count <- u16be, pair_sets <- repeat_len16 pair_set_count (offset16 table_start (pair_set value_format1 value_format2)), }; -let class2_record : Pos -> U16 -> U16 -> Format = -fun table_start value_format1 value_format2 => { +let class2_record = fun (table_start : Pos) (value_format1 : +U16) (value_format2 : U16) => { value_record1 <- optional_value_record table_start value_format1, value_record2 <- optional_value_record table_start value_format2, }; -let class1_record : Pos -> U16 -> U16 -> U16 -> Format = -fun table_start class2_count value_format1 value_format2 => { +let class1_record = fun (table_start : Pos) (class2_count : +U16) (value_format1 : U16) (value_format2 : U16) => { class2_records <- repeat_len16 class2_count (class2_record table_start value_format1 value_format2), }; -let pair_pos_format2 : Pos -> Format = fun pair_pos_start => { +let pair_pos_format2 = fun (pair_pos_start : Pos) => { coverage <- offset16 pair_pos_start coverage_table, value_format1 <- u16be, value_format2 <- u16be, @@ -876,12 +894,12 @@ def anchor_table : Format = { _ => unknown_table, }, }; -def cursive_attachment : Format = let entry_exit_record : Pos -> Format = -fun table_start => { +def cursive_attachment : Format = let entry_exit_record = fun (table_start : +Pos) => { entry_anchor <- offset16 table_start anchor_table, exit_anchor <- offset16 table_start anchor_table, }; -let cursive_pos_format1 : Pos -> Format = fun table_start => { +let cursive_pos_format1 = fun (table_start : Pos) => { coverage <- offset16 table_start coverage_table, entry_exit_count <- u16be, entry_exit_record <- repeat_len16 entry_exit_count (entry_exit_record table_start), @@ -894,8 +912,7 @@ let cursive_pos_format1 : Pos -> Format = fun table_start => { _ => unknown_table, }, }; -def mark_array_table : Format = let mark_record : Pos -> Format = -fun table_start => { +def mark_array_table : Format = let mark_record = fun (table_start : Pos) => { mark_class <- u16be, mark_anchor_offset <- offset16 table_start anchor_table, }; @@ -904,16 +921,15 @@ fun table_start => { mark_count <- u16be, mark_records <- repeat_len16 mark_count (mark_record table_start), }; -def mark_to_base_attachment : Format = let base_record : Pos -> U16 -> Format = -fun table_start mark_class_count => { +def mark_to_base_attachment : Format = let base_record = fun (table_start : +Pos) (mark_class_count : U16) => { base_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), }; -let base_array_table : Pos -> U16 -> Format = -fun table_start mark_class_count => { +let base_array_table = fun (table_start : Pos) (mark_class_count : U16) => { base_count <- u16be, base_records <- repeat_len16 base_count (base_record table_start mark_class_count), }; -let mark_base_pos_format1 : Pos -> Format = fun table_start => { +let mark_base_pos_format1 = fun (table_start : Pos) => { mark_coverage <- offset16 table_start coverage_table, base_coverage <- offset16 table_start coverage_table, mark_class_count <- u16be, @@ -928,21 +944,19 @@ let mark_base_pos_format1 : Pos -> Format = fun table_start => { _ => unknown_table, }, }; -def mark_to_ligature_attachment : Format = let component_record : Pos -> U16 -> -Format = fun table_start mark_class_count => { +def mark_to_ligature_attachment : Format = let component_record = +fun (table_start : Pos) (mark_class_count : U16) => { ligature_anchors <- repeat_len16 mark_class_count (offset16 table_start anchor_table), }; -let ligature_attach : Pos -> U16 -> Format = -fun table_start mark_class_count => { +let ligature_attach = fun (table_start : Pos) (mark_class_count : U16) => { component_count <- u16be, component_records <- repeat_len16 component_count (component_record table_start mark_class_count), }; -let ligature_array : Pos -> U16 -> Format = -fun table_start mark_class_count => { +let ligature_array = fun (table_start : Pos) (mark_class_count : U16) => { ligature_count <- u16be, ligature_attaches <- repeat_len16 ligature_count (offset16 table_start (ligature_attach table_start mark_class_count)), }; -let mark_lig_pos_format1 : Pos -> Format = fun table_start => { +let mark_lig_pos_format1 = fun (table_start : Pos) => { mark_coverage <- offset16 table_start coverage_table, ligature_coverage <- offset16 table_start coverage_table, mark_class_count <- u16be, @@ -960,7 +974,7 @@ let mark_lig_pos_format1 : Pos -> Format = fun table_start => { def mark_to_mark_attachment : Format = mark_to_base_attachment; def contextual_positioning : Format = sequence_context; def chained_contexts_positioning : Format = chained_sequence_context; -def extension_positioning : Format = let extension_pos_format1 : Format = { +def extension_positioning : Format = let extension_pos_format1 = { table_start <- stream_pos, extension_lookup_type <- u16be, extension_subtable <- match extension_lookup_type { @@ -982,9 +996,9 @@ def extension_positioning : Format = let extension_pos_format1 : Format = { _ => unknown_table, }, }; -def lookup_table : U32 -> Format = fun tag => let USE_MARK_FILTERING_SET : U16 = -0x10; -let lookup_subtable : U32 -> U16 -> Format = fun tag lookup_type => match tag { +def lookup_table : U32 -> Format = fun (tag : +U32) => let USE_MARK_FILTERING_SET = 0x10; +let lookup_subtable = fun (tag : U32) (lookup_type : U16) => match tag { "GPOS" => match lookup_type { 1 => single_adjustment, 2 => pair_adjustment, @@ -1021,12 +1035,12 @@ let lookup_subtable : U32 -> U16 -> Format = fun tag lookup_type => match tag { then u16be else empty, }; -def lookup_list : U32 -> Format = fun tag => { +def lookup_list : U32 -> Format = fun (tag : U32) => { table_start <- stream_pos, lookup_count <- u16be, lookups <- repeat_len16 lookup_count (offset16 table_start (lookup_table tag)), }; -def layout_table : U32 -> Format = fun tag => { +def layout_table : U32 -> Format = fun (tag : U32) => { table_start <- stream_pos, major_version <- u16be where major_version == (1 : U16), minor_version <- u16be, @@ -1038,7 +1052,7 @@ def gpos_table : Format = layout_table "GPOS"; def gsub_table : Format = layout_table "GSUB"; def jstf_table : Format = unknown_table; def math_table : Format = unknown_table; -def table_directory : Pos -> Format = fun file_start => { +def table_directory : Pos -> Format = fun (file_start : Pos) => { sfnt_version <- u32be where bool_or (sfnt_version == (0x10000 : U32)) (sfnt_version == ("OTTO" : U32)), num_tables <- u16be, @@ -1046,8 +1060,8 @@ def table_directory : Pos -> Format = fun file_start => { entry_selector <- u16be, range_shift <- u16be, table_records <- repeat_len16 num_tables table_record, - table_links <- let required_table : U32 -> Format -> Format = - fun table_id table_format => { + table_links <- let required_table = fun (table_id : + Repr tag) (table_format : Format) => { table_record <- unwrap @{ table_id : U32, checksum : U32, @@ -1056,8 +1070,8 @@ def table_directory : Pos -> Format = fun file_start => { } (find_table @num_tables table_records table_id), link <- link_table file_start table_record table_format, }; - let required_table_with_len : U32 -> (U32 -> Format) -> Format = - fun table_id table_format => { + let required_table_with_len = fun (table_id : Repr tag) (table_format : U32 + -> Format) => { table_record <- unwrap @{ table_id : U32, checksum : U32, @@ -1066,13 +1080,18 @@ def table_directory : Pos -> Format = fun file_start => { } (find_table @num_tables table_records table_id), link <- link_table file_start table_record (table_format table_record.length), }; - let optional_table : U32 -> Format -> Format = - fun table_id table_format => option_fold @{ + let optional_table = fun (table_id : Repr tag) (table_format : + Format) => option_fold @{ + table_id : U32, + checksum : U32, + offset : U32, + length : U32, + } @Format () (fun (record : { table_id : U32, checksum : U32, offset : U32, length : U32, - } @Format () (fun record => link_table file_start record table_format) (find_table @num_tables table_records table_id); + }) => link_table file_start record table_format) (find_table @num_tables table_records table_id); { cmap <- required_table "cmap" cmap_table, head <- required_table "head" head_table, @@ -1243,12 +1262,12 @@ def table_directory : Pos -> Format = fun file_start => { vmtx <- optional_table "vmtx" unknown_table, }, }; -def ttc_header : Pos -> Format = fun start => let ttc_header1 : Pos -> Format = -fun start => { +def ttc_header : Pos -> Format = fun (start : Pos) => let ttc_header1 = +fun (start : Pos) => { num_fonts <- u32be, table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), }; -let ttc_header2 : Pos -> Format = fun start => { +let ttc_header2 = fun (start : Pos) => { num_fonts <- u32be, table_directories <- repeat_len32 num_fonts (offset32 start (table_directory start)), dsig_tag <- u32be, @@ -1278,8 +1297,7 @@ def main : Format = { }, }; def f2dot14 : Format = s16be; -def chained_sequence_context_format_1 : Format = let chained_sequence_rule : -Format = { +def chained_sequence_context_format_1 : Format = let chained_sequence_rule = { backtrack_glyph_count <- u16be, backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, input_glyph_count <- u16be, @@ -1289,7 +1307,7 @@ Format = { seq_lookup_count <- u16be, seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, }; -let chained_sequence_rule_set : Format = { +let chained_sequence_rule_set = { table_start <- stream_pos, chained_seq_rule_count <- u16be, chained_seq_rules <- repeat_len16 chained_seq_rule_count (offset16 table_start chained_sequence_rule), @@ -1301,7 +1319,7 @@ let chained_sequence_rule_set : Format = { chained_seq_rule_sets <- repeat_len16 chained_seq_rule_set_count (offset16 table_start chained_sequence_rule_set), }; def chained_sequence_context_format_2 : Format = -let chained_class_sequence_rule : Format = { +let chained_class_sequence_rule = { backtrack_glyph_count <- u16be, backtrack_sequence <- repeat_len16 backtrack_glyph_count u16be, input_glyph_count <- u16be, @@ -1311,7 +1329,7 @@ let chained_class_sequence_rule : Format = { seq_lookup_count <- u16be, seq_lookup_records <- repeat_len16 seq_lookup_count sequence_lookup_record, }; -let chained_class_sequence_rule_set : Format = { +let chained_class_sequence_rule_set = { table_start <- stream_pos, chained_class_seq_rule_count <- u16be, chained_class_seq_rules <- repeat_len16 chained_class_seq_rule_count (offset16 table_start chained_class_sequence_rule), diff --git a/formats/unwrap-none.snap b/formats/unwrap-none.snap index f12ac67f3..bed39b2c5 100644 --- a/formats/unwrap-none.snap +++ b/formats/unwrap-none.snap @@ -1,7 +1,8 @@ stdout = ''' def main : Format = { let ary : Array16 3 U16 = [1, 2, 3], - x <- unwrap @U16 (array16_find @3 @U16 (fun el => el == (4 : U16)) ary), + x <- unwrap @U16 (array16_find @3 @U16 (fun (el : U16) => el == (4 : + U16)) ary), }; ''' stderr = '' diff --git a/tests/cmd/fathom-norm.md b/tests/cmd/fathom-norm.md index b178144a4..1f2324d63 100644 --- a/tests/cmd/fathom-norm.md +++ b/tests/cmd/fathom-norm.md @@ -40,7 +40,7 @@ Terms can be normalised with `--term` ```console $ fathom norm --term tests/succeed/fun-elim/ann-identity-poly-1.fathom -fun a => a : Type -> Type +fun (a : Type) => a : Type -> Type ``` diff --git a/tests/fail/elaboration/block-comment.snap b/tests/fail/elaboration/block-comment.snap index 75e75c878..4f5c96033 100644 --- a/tests/fail/elaboration/block-comment.snap +++ b/tests/fail/elaboration/block-comment.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : Bool = false; () : () +let x = false; () : () ''' stderr = '' diff --git a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap index e408c537b..141170f36 100644 --- a/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap +++ b/tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.snap @@ -16,7 +16,7 @@ error: mismatched types ┌─ tests/fail/elaboration/unification/mismatch/match-equation-body-exprs.fathom:5:10 │ 5 │ _ => 4 : U64, - │ ^^^^^^^ type mismatch, expected `U32`, found `U64` + │ ^ type mismatch, expected `U32`, found `U64` │ = expected `U32` found `U64` diff --git a/tests/fail/elaboration/unsolved/fun-literal-param-type.snap b/tests/fail/elaboration/unsolved/fun-literal-param-type.snap index 7b651e95c..3f5c8e48f 100644 --- a/tests/fail/elaboration/unsolved/fun-literal-param-type.snap +++ b/tests/fail/elaboration/unsolved/fun-literal-param-type.snap @@ -1,5 +1,5 @@ stdout = ''' -fun a => a : ?0 -> ?0 +fun (a : ?0) => a : ?0 -> ?0 ''' stderr = ''' error: failed to infer named pattern type diff --git a/tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.snap b/tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.snap index 63800ddf1..8168f5129 100644 --- a/tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.snap +++ b/tests/fail/elaboration/unsolved/fun-literal-placeholder-body-type.snap @@ -1,5 +1,5 @@ stdout = ''' -fun A a b => a : fun (A : Type) -> ?2 A -> A -> ?2 A +fun (A : Type) (a : ?2 A) (b : A) => a : fun (A : Type) -> ?2 A -> A -> ?2 A ''' stderr = ''' error: failed to infer named pattern type diff --git a/tests/succeed/ann/fun-literal-identity-mono-input-ann-placeholder.snap b/tests/succeed/ann/fun-literal-identity-mono-input-ann-placeholder.snap index d2bd245b3..684f68bc1 100644 --- a/tests/succeed/ann/fun-literal-identity-mono-input-ann-placeholder.snap +++ b/tests/succeed/ann/fun-literal-identity-mono-input-ann-placeholder.snap @@ -1,4 +1,4 @@ stdout = ''' -fun a => a : Type -> Type +fun (a : Type) => a : Type -> Type ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-identity-mono-input-ann-type.snap b/tests/succeed/ann/fun-literal-identity-mono-input-ann-type.snap index d2bd245b3..684f68bc1 100644 --- a/tests/succeed/ann/fun-literal-identity-mono-input-ann-type.snap +++ b/tests/succeed/ann/fun-literal-identity-mono-input-ann-type.snap @@ -1,4 +1,4 @@ stdout = ''' -fun a => a : Type -> Type +fun (a : Type) => a : Type -> Type ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-identity-mono.snap b/tests/succeed/ann/fun-literal-identity-mono.snap index d2bd245b3..684f68bc1 100644 --- a/tests/succeed/ann/fun-literal-identity-mono.snap +++ b/tests/succeed/ann/fun-literal-identity-mono.snap @@ -1,4 +1,4 @@ stdout = ''' -fun a => a : Type -> Type +fun (a : Type) => a : Type -> Type ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-identity-poly-input-placeholder.snap b/tests/succeed/ann/fun-literal-identity-poly-input-placeholder.snap index e5d47a791..77a3079c8 100644 --- a/tests/succeed/ann/fun-literal-identity-poly-input-placeholder.snap +++ b/tests/succeed/ann/fun-literal-identity-poly-input-placeholder.snap @@ -1,4 +1,4 @@ stdout = ''' -fun _ a => a : fun (A : Type) -> A -> A +fun (a : Type) (a : a) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-identity-poly-sugar.snap b/tests/succeed/ann/fun-literal-identity-poly-sugar.snap index 97b34df95..776aa4093 100644 --- a/tests/succeed/ann/fun-literal-identity-poly-sugar.snap +++ b/tests/succeed/ann/fun-literal-identity-poly-sugar.snap @@ -1,4 +1,4 @@ stdout = ''' -fun A a => a : fun (A : Type) -> A -> A +fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-identity-poly.snap b/tests/succeed/ann/fun-literal-identity-poly.snap index 97b34df95..776aa4093 100644 --- a/tests/succeed/ann/fun-literal-identity-poly.snap +++ b/tests/succeed/ann/fun-literal-identity-poly.snap @@ -1,4 +1,4 @@ stdout = ''' -fun A a => a : fun (A : Type) -> A -> A +fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/ann/fun-literal-placeholder-body-type.snap b/tests/succeed/ann/fun-literal-placeholder-body-type.snap index 97b34df95..776aa4093 100644 --- a/tests/succeed/ann/fun-literal-placeholder-body-type.snap +++ b/tests/succeed/ann/fun-literal-placeholder-body-type.snap @@ -1,4 +1,4 @@ stdout = ''' -fun A a => a : fun (A : Type) -> A -> A +fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/bin-ops.snap b/tests/succeed/bin-ops.snap index ff3bf27b2..361097dda 100644 --- a/tests/succeed/bin-ops.snap +++ b/tests/succeed/bin-ops.snap @@ -1,20 +1,20 @@ stdout = ''' -let device_table : Format = let u16_div_ceil : U16 -> U16 -> U16 = -fun numerator denominator => let quotient : U16 = numerator / denominator; +let device_table = let u16_div_ceil = fun (numerator : U16) (denominator : +U16) => let quotient = numerator / denominator; if (quotient * denominator) < numerator then quotient + (1 : U16) else quotient; -let delta_bits : U16 -> U16 -> U16 = -fun delta_format num_sizes => match delta_format { +let delta_bits = fun (delta_format : U16) (num_sizes : +U16) => match delta_format { 0x1 => num_sizes * (2 : U16), 0x2 => num_sizes * (4 : U16), 0x3 => num_sizes * (8 : U16), _ => 0, }; -let num_sizes : U16 -> U16 -> U16 = fun start end => end - start + (1 : U16); +let num_sizes = fun (start : U16) (end : U16) => end - start + (1 : U16); { start_size <- u16be, end_size <- u16be, delta_format <- u16be, - delta_values <- let delta_bits : U16 = + delta_values <- let delta_bits = delta_bits delta_format (num_sizes start_size end_size); repeat_len16 (u16_div_ceil delta_bits 16) u16be, }; diff --git a/tests/succeed/distillation/fresh-names.snap b/tests/succeed/distillation/fresh-names.snap index b605ed185..e3df4b1aa 100644 --- a/tests/succeed/distillation/fresh-names.snap +++ b/tests/succeed/distillation/fresh-names.snap @@ -1,12 +1,12 @@ stdout = ''' def a : () = (); -def const1 : fun (@A : Type) (@B : Type) -> A -> B -> A = -fun @b @c x y => let x1 : b = x; -let y1 : c = y; +def const1 : fun (@A : Type) (@B : Type) -> A -> B -> A = fun (@b : Type) (@c : +Type) (x : b) (y : c) => let x1 = x; +let y1 = y; x; -def const2 : fun (@A : Type) (@B : Type) -> A -> B -> A = let b : () = (); -fun @c @d x y => let x1 : c = x; -let y1 : d = y; +def const2 : fun (@A : Type) (@B : Type) -> A -> B -> A = let b = (); +fun (@c : Type) (@d : Type) (x : c) (y : d) => let x1 = x; +let y1 = y; x; ''' stderr = '' diff --git a/tests/succeed/equality.snap b/tests/succeed/equality.snap index 9ab405c21..47b4fd314 100644 --- a/tests/succeed/equality.snap +++ b/tests/succeed/equality.snap @@ -1,38 +1,34 @@ stdout = ''' -let id : fun (A : Type) -> A -> A = fun A a => a; -let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A -> -Type) -> P a0 -> P a1; -let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a); -let fun_eta_left : fun (f : Type -> Type) -> Eq (Type -> -Type) f (fun x => f x) = fun f => refl (Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type) -> Eq (Type -> -Type) (fun x => f x) f = fun f => refl (Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) f (fun x => f x) = fun f => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x => f x) f = fun f => refl (Type -> Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) f (fun x y => f x y) = fun f => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x y => f x y) f = fun f => refl (Type -> Type -> Type) f; -let fun_eta_left : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x => f x) (fun x y => f x y) = fun f => refl (Type -> Type -> +let id = fun (A : Type) (a : A) => a; +let Eq = fun (A : Type) (a0 : A) (a1 : A) => fun (P : A -> Type) -> P a0 -> +P a1; +let refl = fun (A : Type) (a : A) (P : A -> Type) => id (P a); +let fun_eta_left = fun (f : Type -> Type) => refl (Type -> Type) f; +let fun_eta_right = fun (f : Type -> Type) => refl (Type -> Type) f; +let fun_eta_left = fun (f : Type -> Type -> Type) => refl (Type -> Type -> Type) f; -let fun_eta_right : fun (f : Type -> Type -> Type) -> Eq (Type -> Type -> -Type) (fun x y => f x y) (fun x => f x) = fun f => refl (Type -> Type -> +let fun_eta_right = fun (f : Type -> Type -> Type) => refl (Type -> Type -> Type) f; -let record_eta_left : fun (r : { x : Type, y : Type }) -> Eq { +let fun_eta_left = fun (f : Type -> Type -> Type) => refl (Type -> Type -> +Type) f; +let fun_eta_right = fun (f : Type -> Type -> Type) => refl (Type -> Type -> +Type) f; +let fun_eta_left = fun (f : Type -> Type -> Type) => refl (Type -> Type -> +Type) f; +let fun_eta_right = fun (f : Type -> Type -> Type) => refl (Type -> Type -> +Type) f; +let record_eta_left = fun (r : { x : Type, y : Type }) => refl { x : Type, y : Type, -} r { x = r.x, y = r.y } = fun r => refl { x : Type, y : Type } r; -let record_eta_right : fun (r : { x : Type, y : Type }) -> Eq { +} r; +let record_eta_right = fun (r : { x : Type, y : Type }) => refl { x : Type, y : Type, -} { x = r.x, y = r.y } r = fun r => refl { x : Type, y : Type } r; -let four_chars : Eq U32 "beng" 1650814567 = refl U32 "beng"; -let three_chars : Eq U32 "BEN " 1111838240 = refl U32 "BEN "; -let foo : U32 -> U32 = fun x => match x { 1 => 0, x => x }; -let eq_foo : Eq (U32 -> U32) foo foo = refl (U32 -> U32) (fun a => match a { +} r; +let four_chars = refl U32 "beng"; +let three_chars = refl U32 "BEN "; +let foo = fun (x : U32) => match x { 1 => 0, x => x }; +let eq_foo = refl (U32 -> U32) (fun (a : reported_error) => match a { 1 => 0, x => x, }); diff --git a/tests/succeed/format-cond/simple.snap b/tests/succeed/format-cond/simple.snap index b2cff4c88..783cb10da 100644 --- a/tests/succeed/format-cond/simple.snap +++ b/tests/succeed/format-cond/simple.snap @@ -1,8 +1,8 @@ stdout = ''' -let format : Format = { +let format = { sfnt_version <- { version <- u32be | version == (0xffff : U32) }, }; -let _ : Repr format -> { sfnt_version : Repr u32be } = fun x => x; +let _ = fun (x : { sfnt_version : U32 }) => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-overlap/dependent.snap b/tests/succeed/format-overlap/dependent.snap index 0f017d55c..8f794dcc4 100644 --- a/tests/succeed/format-overlap/dependent.snap +++ b/tests/succeed/format-overlap/dependent.snap @@ -1,17 +1,14 @@ stdout = ''' -let record0 : Format = { length <- u8 }; -let record1 : U8 -> Format = fun length => { +let record0 = { length <- u8 }; +let record1 = fun (length : U8) => { _length <- u8, data <- repeat_len8 length u8, }; -let silly : Format = overlap { - record0 <- record0, - record1 <- record1 record0.length, -}; -let _ : Repr silly -> { +let silly = overlap { record0 <- record0, record1 <- record1 record0.length }; +let _ = fun (silly : { record0 : { length : U8 }, record1 : { _length : U8, data : Array8 record0.length U8 }, -} = fun silly => silly; +}) => silly; () : () ''' stderr = '' diff --git a/tests/succeed/format-overlap/field-refinements.snap b/tests/succeed/format-overlap/field-refinements.snap index 4c883bfc5..5614d7ea9 100644 --- a/tests/succeed/format-overlap/field-refinements.snap +++ b/tests/succeed/format-overlap/field-refinements.snap @@ -1,6 +1,6 @@ stdout = ''' -let number : Format = overlap { u <- u32be where u >= (2 : U32), s <- s32be }; -let _ : Repr number -> { u : U32, s : S32 } = fun n => n; +let number = overlap { u <- u32be where u >= (2 : U32), s <- s32be }; +let _ = fun (n : { u : U32, s : S32 }) => n; () : () ''' stderr = '' diff --git a/tests/succeed/format-overlap/numbers.snap b/tests/succeed/format-overlap/numbers.snap index 2c0e3d9de..b7a1aa9e5 100644 --- a/tests/succeed/format-overlap/numbers.snap +++ b/tests/succeed/format-overlap/numbers.snap @@ -1,6 +1,6 @@ stdout = ''' -let number : Format = overlap { u <- u32be, s <- s32be }; -let _ : Repr number -> { u : U32, s : S32 } = fun n => n; +let number = overlap { u <- u32be, s <- s32be }; +let _ = fun (n : { u : U32, s : S32 }) => n; () : () ''' stderr = '' diff --git a/tests/succeed/format-record/computed-fields.snap b/tests/succeed/format-record/computed-fields.snap index fdf12baa8..ca4477f64 100644 --- a/tests/succeed/format-record/computed-fields.snap +++ b/tests/succeed/format-record/computed-fields.snap @@ -1,18 +1,18 @@ stdout = ''' -let format : Format = { +let format = { seg_count_x2 <- u16be, let seg_count : U16 = seg_count_x2 / (2 : U16), start_code <- repeat_len16 seg_count u16be, id_delta <- repeat_len16 seg_count s16be, }; -let _ : Repr format -> { +let _ = fun (x : { seg_count_x2 : U16, seg_count : U16, start_code : Array16 seg_count U16, id_delta : Array16 seg_count S16, -} = fun x => x; -let format : Format = { let x : U32 = 256 }; -let _ : Repr format -> { x : U32 } = fun x => x; +}) => x; +let format = { let x : U32 = 256 }; +let _ = fun (x : { x : U32 }) => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-record/field-refinements.snap b/tests/succeed/format-record/field-refinements.snap index e53127fb2..51df3e97d 100644 --- a/tests/succeed/format-record/field-refinements.snap +++ b/tests/succeed/format-record/field-refinements.snap @@ -1,11 +1,10 @@ stdout = ''' -let format : Format = { +let format = { magic <- u64le where magic == (0xffffffffffff00 : U64), len <- u8 where len <= (16 : U8), data <- repeat_len8 len u8, }; -let _ : Repr format -> { magic : U64, len : U8, data : Array8 len U8 } = -fun x => x; +let _ = fun (x : { magic : U64, len : U8, data : Array8 len U8 }) => x; () : () ''' stderr = '' diff --git a/tests/succeed/format-record/pair-dependent.snap b/tests/succeed/format-record/pair-dependent.snap index 388dc6a4b..0503a1385 100644 --- a/tests/succeed/format-record/pair-dependent.snap +++ b/tests/succeed/format-record/pair-dependent.snap @@ -1,6 +1,6 @@ stdout = ''' -let repeat_len32 : U32 -> Format -> Format = fun len Elem => Elem; -let pair : Format = { len <- u32be, data <- repeat_len32 len u32be }; +let repeat_len32 = fun (len : U32) (Elem : Format) => Elem; +let pair = { len <- u32be, data <- repeat_len32 len u32be }; pair : Format ''' stderr = '' diff --git a/tests/succeed/format-record/pair.snap b/tests/succeed/format-record/pair.snap index 387cad5db..4b66abaf5 100644 --- a/tests/succeed/format-record/pair.snap +++ b/tests/succeed/format-record/pair.snap @@ -1,4 +1,4 @@ stdout = ''' -let pair : Format = { fst <- u32be, snd <- u32be }; pair : Format +let pair = { fst <- u32be, snd <- u32be }; pair : Format ''' stderr = '' diff --git a/tests/succeed/format-repr/coercions.snap b/tests/succeed/format-repr/coercions.snap index 13608b9e2..727d6c719 100644 --- a/tests/succeed/format-repr/coercions.snap +++ b/tests/succeed/format-repr/coercions.snap @@ -1,7 +1,4 @@ stdout = ''' -let num : Format = s32be; -let x : Repr num = 3; -let Point : Type = { x : Repr num, y : Repr num }; -x : S32 +let num = s32be; let x = 3; let Point = { x : Repr num, y : Repr num }; x : S32 ''' stderr = '' diff --git a/tests/succeed/format-repr/pair-dependent.snap b/tests/succeed/format-repr/pair-dependent.snap index 50345c9f8..027bd4000 100644 --- a/tests/succeed/format-repr/pair-dependent.snap +++ b/tests/succeed/format-repr/pair-dependent.snap @@ -1,7 +1,7 @@ stdout = ''' -let repeat_len32 : U32 -> Format -> Format = fun len Elem => Elem; -let pair : Format = { len <- u32be, data <- repeat_len32 len u32be }; -let test_pair : Repr pair -> { len : U32, data : U32 } = fun p => p; +let repeat_len32 = fun (len : U32) (Elem : Format) => Elem; +let pair = { len <- u32be, data <- repeat_len32 len u32be }; +let test_pair = fun (p : { len : U32, data : U32 }) => p; pair : Format ''' stderr = '' diff --git a/tests/succeed/format-repr/primitives.snap b/tests/succeed/format-repr/primitives.snap index 27f7d8e68..173fa1ab0 100644 --- a/tests/succeed/format-repr/primitives.snap +++ b/tests/succeed/format-repr/primitives.snap @@ -1,49 +1,40 @@ stdout = ''' -let test_u8_repr : Repr u8 -> U8 = fun x => x; -let test_u16be_repr : Repr u16be -> U16 = fun x => x; -let test_u16le_repr : Repr u16le -> U16 = fun x => x; -let test_u32be_repr : Repr u32be -> U32 = fun x => x; -let test_u32le_repr : Repr u32le -> U32 = fun x => x; -let test_u64be_repr : Repr u64be -> U64 = fun x => x; -let test_u64le_repr : Repr u64le -> U64 = fun x => x; -let test_s8_repr : Repr s8 -> S8 = fun x => x; -let test_s16be_repr : Repr s16be -> S16 = fun x => x; -let test_s16le_repr : Repr s16le -> S16 = fun x => x; -let test_s32be_repr : Repr s32be -> S32 = fun x => x; -let test_s32le_repr : Repr s32le -> S32 = fun x => x; -let test_s64be_repr : Repr s64be -> S64 = fun x => x; -let test_s64le_repr : Repr s64le -> S64 = fun x => x; -let test_f32be_repr : Repr f32be -> F32 = fun x => x; -let test_f32le_repr : Repr f32le -> F32 = fun x => x; -let test_f64be_repr : Repr f64be -> F64 = fun x => x; -let test_f64le_repr : Repr f64le -> F64 = fun x => x; -let test_repeat_len8 : fun (n : U8) (f : Format) -> Repr (repeat_len8 n f) -> -Array8 n (Repr f) = fun _ _ x => x; -let test_repeat_len16 : fun (n : U16) (f : Format) -> Repr (repeat_len16 n f) -> -Array16 n (Repr f) = fun _ _ x => x; -let test_repeat_len32 : fun (n : U32) (f : Format) -> Repr (repeat_len32 n f) -> -Array32 n (Repr f) = fun _ _ x => x; -let test_repeat_len64 : fun (n : U64) (f : Format) -> Repr (repeat_len64 n f) -> -Array64 n (Repr f) = fun _ _ x => x; -let test_repeat_until_end : fun (f : Format) -> Repr (repeat_until_end f) -> -Array (Repr f) = fun _ x => x; -let test_limit8 : fun (n : U8) (f : Format) -> Repr (limit8 n f) -> Repr f = -fun _ _ x => x; -let test_limit16 : fun (n : U16) (f : Format) -> Repr (limit16 n f) -> Repr f = -fun _ _ x => x; -let test_limit32 : fun (n : U32) (f : Format) -> Repr (limit32 n f) -> Repr f = -fun _ _ x => x; -let test_limit64 : fun (n : U64) (f : Format) -> Repr (limit64 n f) -> Repr f = -fun _ _ x => x; -let test_link : fun (pos : Pos) (f : Format) -> Repr (link pos f) -> Ref f = -fun _ _ x => x; -let test_deref : fun (f : Format) (ref : Ref f) -> Repr (deref @f ref) -> -Repr f = fun _ _ x => x; -let test_stream_pos : Repr stream_pos -> Pos = fun x => x; -let test_succeed : Repr (succeed @S32 42) -> S32 = fun x => x; -let test_fail : Repr fail -> Void = fun x => x; -let test_unwrap : fun (A : Type) (opt_a : Option A) -> Repr (unwrap @A opt_a) -> -A = fun _ _ x => x; +let test_u8_repr = fun (x : U8) => x; +let test_u16be_repr = fun (x : U16) => x; +let test_u16le_repr = fun (x : U16) => x; +let test_u32be_repr = fun (x : U32) => x; +let test_u32le_repr = fun (x : U32) => x; +let test_u64be_repr = fun (x : U64) => x; +let test_u64le_repr = fun (x : U64) => x; +let test_s8_repr = fun (x : S8) => x; +let test_s16be_repr = fun (x : S16) => x; +let test_s16le_repr = fun (x : S16) => x; +let test_s32be_repr = fun (x : S32) => x; +let test_s32le_repr = fun (x : S32) => x; +let test_s64be_repr = fun (x : S64) => x; +let test_s64le_repr = fun (x : S64) => x; +let test_f32be_repr = fun (x : F32) => x; +let test_f32le_repr = fun (x : F32) => x; +let test_f64be_repr = fun (x : F64) => x; +let test_f64le_repr = fun (x : F64) => x; +let test_repeat_len8 = fun (a : U8) (b : Format) (x : Array8 a (Repr b)) => x; +let test_repeat_len16 = fun (a : U16) (b : Format) (x : +Array16 a (Repr b)) => x; +let test_repeat_len32 = fun (a : U32) (b : Format) (x : +Array32 a (Repr b)) => x; +let test_repeat_len64 = fun (a : U64) (b : Format) (x : +Array64 a (Repr b)) => x; +let test_repeat_until_end = fun (a : Format) (x : Array (Repr a)) => x; +let test_limit8 = fun (_ : U8) (a : Format) (x : Repr a) => x; +let test_limit16 = fun (_ : U16) (a : Format) (x : Repr a) => x; +let test_limit32 = fun (_ : U32) (a : Format) (x : Repr a) => x; +let test_limit64 = fun (_ : U64) (a : Format) (x : Repr a) => x; +let test_link = fun (_ : Pos) (a : Format) (x : Ref a) => x; +let test_deref = fun (a : Format) (_ : Ref a) (x : Repr a) => x; +let test_stream_pos = fun (x : Pos) => x; +let test_succeed = fun (x : S32) => x; +let test_fail = fun (x : Void) => x; +let test_unwrap = fun (a : Type) (_ : Option a) (x : a) => x; Type : Type ''' stderr = '' diff --git a/tests/succeed/format-repr/record.snap b/tests/succeed/format-repr/record.snap index f86b823cc..950af12ce 100644 --- a/tests/succeed/format-repr/record.snap +++ b/tests/succeed/format-repr/record.snap @@ -1,7 +1,7 @@ stdout = ''' -let pair : Format = { fst <- u32be, snd <- u32be }; -let test_pair : Repr pair -> { fst : U32, snd : U32 } = fun p => p; -let test_pair : Repr pair -> { fst : U32, snd : U32 } = fun p => { +let pair = { fst <- u32be, snd <- u32be }; +let test_pair = fun (p : { fst : U32, snd : U32 }) => p; +let test_pair = fun (p : { fst : U32, snd : U32 }) => { fst = p.fst, snd = p.snd, }; diff --git a/tests/succeed/format-repr/unit-literal.snap b/tests/succeed/format-repr/unit-literal.snap index da0d2f6d4..48b7952f1 100644 --- a/tests/succeed/format-repr/unit-literal.snap +++ b/tests/succeed/format-repr/unit-literal.snap @@ -1,7 +1,7 @@ stdout = ''' -let unit : Format = (); -let test_unit : Repr unit -> () = fun p => p; -let test_unit : Repr unit -> () = fun p => (); +let unit = (); +let test_unit = fun (p : ()) => p; +let test_unit = fun (p : ()) => (); unit : Format ''' stderr = '' diff --git a/tests/succeed/fun-elim/ann-identity-mono-0.snap b/tests/succeed/fun-elim/ann-identity-mono-0.snap index f965ee9b0..a5ceb7d58 100644 --- a/tests/succeed/fun-elim/ann-identity-mono-0.snap +++ b/tests/succeed/fun-elim/ann-identity-mono-0.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun a => a : Type -> Type) Type : Type +(fun (a : Type) => a) Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/ann-identity-mono-1.snap b/tests/succeed/fun-elim/ann-identity-mono-1.snap index 2d2879e4e..2219c114d 100644 --- a/tests/succeed/fun-elim/ann-identity-mono-1.snap +++ b/tests/succeed/fun-elim/ann-identity-mono-1.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun a => a : (Type -> Type) -> Type -> Type) (fun a => a) Type : Type +(fun (a : Type -> Type) => a) (fun (a : Type) => a) Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/ann-identity-mono-2.snap b/tests/succeed/fun-elim/ann-identity-mono-2.snap index 2d2879e4e..2219c114d 100644 --- a/tests/succeed/fun-elim/ann-identity-mono-2.snap +++ b/tests/succeed/fun-elim/ann-identity-mono-2.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun a => a : (Type -> Type) -> Type -> Type) (fun a => a) Type : Type +(fun (a : Type -> Type) => a) (fun (a : Type) => a) Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/ann-identity-poly-0.snap b/tests/succeed/fun-elim/ann-identity-poly-0.snap index 0bbfc9f5b..ebee6317c 100644 --- a/tests/succeed/fun-elim/ann-identity-poly-0.snap +++ b/tests/succeed/fun-elim/ann-identity-poly-0.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun A a => a : fun (A : Type) -> A -> A) Type Type : Type +(fun (A : Type) (a : A) => a) Type Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/ann-identity-poly-1.snap b/tests/succeed/fun-elim/ann-identity-poly-1.snap index d3bacde42..bf0d438fd 100644 --- a/tests/succeed/fun-elim/ann-identity-poly-1.snap +++ b/tests/succeed/fun-elim/ann-identity-poly-1.snap @@ -1,5 +1,5 @@ stdout = ''' -(fun A a => a : fun (A : Type) -> A -> A) (Type -> Type) (fun a => a) : Type -> +(fun (A : Type) (a : A) => a) (Type -> Type) (fun (a : Type) => a) : Type -> Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/identity-mono-0.snap b/tests/succeed/fun-elim/identity-mono-0.snap index 210a12da2..a5ceb7d58 100644 --- a/tests/succeed/fun-elim/identity-mono-0.snap +++ b/tests/succeed/fun-elim/identity-mono-0.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun a => a) Type : Type +(fun (a : Type) => a) Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-elim/identity-mono-1.snap b/tests/succeed/fun-elim/identity-mono-1.snap index 5292e4489..2219c114d 100644 --- a/tests/succeed/fun-elim/identity-mono-1.snap +++ b/tests/succeed/fun-elim/identity-mono-1.snap @@ -1,4 +1,4 @@ stdout = ''' -(fun a => a) (fun a => a) Type : Type +(fun (a : Type -> Type) => a) (fun (a : Type) => a) Type : Type ''' stderr = '' diff --git a/tests/succeed/fun-literal/identity-mono.snap b/tests/succeed/fun-literal/identity-mono.snap index d2bd245b3..684f68bc1 100644 --- a/tests/succeed/fun-literal/identity-mono.snap +++ b/tests/succeed/fun-literal/identity-mono.snap @@ -1,4 +1,4 @@ stdout = ''' -fun a => a : Type -> Type +fun (a : Type) => a : Type -> Type ''' stderr = '' diff --git a/tests/succeed/fun-literal/identity-poly-sugar.snap b/tests/succeed/fun-literal/identity-poly-sugar.snap index 97b34df95..776aa4093 100644 --- a/tests/succeed/fun-literal/identity-poly-sugar.snap +++ b/tests/succeed/fun-literal/identity-poly-sugar.snap @@ -1,4 +1,4 @@ stdout = ''' -fun A a => a : fun (A : Type) -> A -> A +fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/fun-literal/identity-poly.snap b/tests/succeed/fun-literal/identity-poly.snap index 97b34df95..776aa4093 100644 --- a/tests/succeed/fun-literal/identity-poly.snap +++ b/tests/succeed/fun-literal/identity-poly.snap @@ -1,4 +1,4 @@ stdout = ''' -fun A a => a : fun (A : Type) -> A -> A +fun (A : Type) (a : A) => a : fun (A : Type) -> A -> A ''' stderr = '' diff --git a/tests/succeed/hole/hole-1.snap b/tests/succeed/hole/hole-1.snap index a70d1d6a5..5ea57dc49 100644 --- a/tests/succeed/hole/hole-1.snap +++ b/tests/succeed/hole/hole-1.snap @@ -1,5 +1,5 @@ stdout = ''' -(fun a => a : Type -> Type) Type : Type +(fun (a : Type) => a) Type : Type ''' stderr = ''' note: solution found for hole `?fun_type` diff --git a/tests/succeed/if-then-else/pretty.snap b/tests/succeed/if-then-else/pretty.snap index acf50489b..99550097a 100644 --- a/tests/succeed/if-then-else/pretty.snap +++ b/tests/succeed/if-then-else/pretty.snap @@ -1,10 +1,10 @@ stdout = ''' -let _ : U32 = if false then 1 else 0; -let _ : U32 = if (if false then true else false) +let _ = if false then 1 else 0; +let _ = if (if false then true else false) then if true then 0 else 1 else if false then 2 else 3; -let _ : U32 = if false +let _ = if false then 0 else if false then 0 else if false then 0 diff --git a/tests/succeed/implicit-args/generalize.snap b/tests/succeed/implicit-args/generalize.snap index e6d072754..e8d8a098a 100644 --- a/tests/succeed/implicit-args/generalize.snap +++ b/tests/succeed/implicit-args/generalize.snap @@ -1,8 +1,7 @@ stdout = ''' -let id : fun (@A : Type) -> A -> A = fun @A a => a; -let always : fun (@A : Type) (@B : Type) -> A -> B -> A = fun @A @B a b => a; -let apply : fun (@A : Type) (@B : Type) -> (A -> B) -> A -> B = -fun @A @B f x => f x; +let id = fun (@A : Type) (a : A) => a; +let always = fun (@A : Type) (@B : Type) (a : A) (b : B) => a; +let apply = fun (@A : Type) (@B : Type) (f : A -> B) (x : A) => f x; () : () ''' stderr = '' diff --git a/tests/succeed/implicit-args/insert-args.snap b/tests/succeed/implicit-args/insert-args.snap index d1888f6a8..e1f875093 100644 --- a/tests/succeed/implicit-args/insert-args.snap +++ b/tests/succeed/implicit-args/insert-args.snap @@ -1,8 +1,8 @@ stdout = ''' -let id : fun (@A : Type) -> A -> A = fun @A a => a; -let always : fun (@A : Type) (@B : Type) -> A -> B -> A = fun @A @B a b => a; -let _ : Bool = id @Bool false; -let _ : U32 = always @U32 @Bool 0 false; +let id = fun (@A : Type) (a : A) => a; +let always = fun (@A : Type) (@B : Type) (a : A) (b : B) => a; +let _ = id @Bool false; +let _ = always @U32 @Bool 0 false; () : () ''' stderr = '' diff --git a/tests/succeed/implicit-args/specialize.snap b/tests/succeed/implicit-args/specialize.snap index ddc19804c..b28494f74 100644 --- a/tests/succeed/implicit-args/specialize.snap +++ b/tests/succeed/implicit-args/specialize.snap @@ -1,15 +1,14 @@ stdout = ''' -let id : fun (@A : Type) -> A -> A = fun @A a => a; -let always : fun (@A : Type) (@B : Type) -> A -> B -> A = fun @A @B a b => a; -let apply : fun (@A : Type) (@B : Type) -> (A -> B) -> A -> B = -fun @A @B f x => f x; -let _ : fun (@A : Type) -> A -> A = id; -let _ : fun (@A : Type) (@B : Type) -> A -> B -> A = always; -let _ : fun (@A : Type) (@B : Type) -> (A -> B) -> A -> B = apply; -let _ : Bool -> Bool = id @Bool; -let _ : Bool -> U32 -> Bool = always @Bool @U32; -let _ : (Bool -> U32) -> Bool -> U32 = apply @Bool @U32; -let _ : Bool = apply @U32 @Bool (always @Bool @U32 false) 0; +let id = fun (@A : Type) (a : A) => a; +let always = fun (@A : Type) (@B : Type) (a : A) (b : B) => a; +let apply = fun (@A : Type) (@B : Type) (f : A -> B) (x : A) => f x; +let _ = id; +let _ = always; +let _ = apply; +let _ = id @Bool; +let _ = always @Bool @U32; +let _ = apply @Bool @U32; +let _ = apply @U32 @Bool (always @Bool @U32 false) 0; () : () ''' stderr = '' diff --git a/tests/succeed/let/id-type.snap b/tests/succeed/let/id-type.snap index c40f34eee..540055f77 100644 --- a/tests/succeed/let/id-type.snap +++ b/tests/succeed/let/id-type.snap @@ -1,6 +1,5 @@ stdout = ''' -let Id : Type -> Type = fun A => A; -let test_id : fun (A : Type) -> Id A -> A = fun A a => a; -Type : Type +let Id = fun (A : Type) => A; let test_id = fun (A : Type) (a : A) => a; Type : +Type ''' stderr = '' diff --git a/tests/succeed/let/identity-placeholders.snap b/tests/succeed/let/identity-placeholders.snap index 0a610ea65..61a573ebf 100644 --- a/tests/succeed/let/identity-placeholders.snap +++ b/tests/succeed/let/identity-placeholders.snap @@ -1,8 +1,8 @@ stdout = ''' -let id : fun (A : Type) -> A -> A = fun A a => a; -let test_id_check0 : Type -> Type = id Type; -let test_id_check1 : Type = id Type Type; -let test_id_synth : Type = id Type Type; +let id = fun (A : Type) (a : A) => a; +let test_id_check0 = id Type; +let test_id_check1 = id Type Type; +let test_id_synth = id Type Type; Type : Type ''' stderr = '' diff --git a/tests/succeed/let/identity.snap b/tests/succeed/let/identity.snap index 0a610ea65..61a573ebf 100644 --- a/tests/succeed/let/identity.snap +++ b/tests/succeed/let/identity.snap @@ -1,8 +1,8 @@ stdout = ''' -let id : fun (A : Type) -> A -> A = fun A a => a; -let test_id_check0 : Type -> Type = id Type; -let test_id_check1 : Type = id Type Type; -let test_id_synth : Type = id Type Type; +let id = fun (A : Type) (a : A) => a; +let test_id_check0 = id Type; +let test_id_check1 = id Type Type; +let test_id_synth = id Type Type; Type : Type ''' stderr = '' diff --git a/tests/succeed/let/let-def-placeholder-ann.snap b/tests/succeed/let/let-def-placeholder-ann.snap index db3411b51..ce3cb6cca 100644 --- a/tests/succeed/let/let-def-placeholder-ann.snap +++ b/tests/succeed/let/let-def-placeholder-ann.snap @@ -1,4 +1,4 @@ stdout = ''' -let _ : Type = Type; Type : Type +let _ = Type; Type : Type ''' stderr = '' diff --git a/tests/succeed/let/let-def-placeholder.snap b/tests/succeed/let/let-def-placeholder.snap index db3411b51..ce3cb6cca 100644 --- a/tests/succeed/let/let-def-placeholder.snap +++ b/tests/succeed/let/let-def-placeholder.snap @@ -1,4 +1,4 @@ stdout = ''' -let _ : Type = Type; Type : Type +let _ = Type; Type : Type ''' stderr = '' diff --git a/tests/succeed/match/check-const-1.snap b/tests/succeed/match/check-const-1.snap index ec77653c8..77325315a 100644 --- a/tests/succeed/match/check-const-1.snap +++ b/tests/succeed/match/check-const-1.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, x => x } : U8 +let x = 3; match x { 1 => 0, x => x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-2.snap b/tests/succeed/match/check-const-2.snap index 2023e6468..779b078f7 100644 --- a/tests/succeed/match/check-const-2.snap +++ b/tests/succeed/match/check-const-2.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8 +let x = 3; match x { 1 => 0, 3 => 7, x => x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-bool.snap b/tests/succeed/match/check-const-bool.snap index 7699f35d0..d5ad6dc2a 100644 --- a/tests/succeed/match/check-const-bool.snap +++ b/tests/succeed/match/check-const-bool.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : Bool = false; if x then 1 else 0 : U8 +let x = false; if x then 1 else 0 : U8 ''' stderr = '' diff --git a/tests/succeed/match/check-const-redundant.snap b/tests/succeed/match/check-const-redundant.snap index c1ccc9013..5061f3391 100644 --- a/tests/succeed/match/check-const-redundant.snap +++ b/tests/succeed/match/check-const-redundant.snap @@ -1,5 +1,5 @@ stdout = ''' -let x : U8 = 3; match x { 1 => 0, 3 => 7, x => x } : U8 +let x = 3; match x { 1 => 0, 3 => 7, x => x } : U8 ''' stderr = ''' warning: unreachable pattern diff --git a/tests/succeed/match/check-simple-redundant.snap b/tests/succeed/match/check-simple-redundant.snap index 013396d87..e7079959d 100644 --- a/tests/succeed/match/check-simple-redundant.snap +++ b/tests/succeed/match/check-simple-redundant.snap @@ -1,5 +1,5 @@ stdout = ''' -let x : U8 = 3; 3 : U32 +let x = 3; 3 : U32 ''' stderr = ''' warning: unreachable pattern diff --git a/tests/succeed/match/check-simple.snap b/tests/succeed/match/check-simple.snap index 45f233853..b79dad576 100644 --- a/tests/succeed/match/check-simple.snap +++ b/tests/succeed/match/check-simple.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; 3 : U32 +let x = 3; 3 : U32 ''' stderr = '' diff --git a/tests/succeed/match/synth-const-1.snap b/tests/succeed/match/synth-const-1.snap index 098d6b2df..69a82d084 100644 --- a/tests/succeed/match/synth-const-1.snap +++ b/tests/succeed/match/synth-const-1.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => x, x => x } : U8 +let x = 3; match x { 1 => x, x => x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/synth-const-2.snap b/tests/succeed/match/synth-const-2.snap index 38aaac02b..d8e59e5eb 100644 --- a/tests/succeed/match/synth-const-2.snap +++ b/tests/succeed/match/synth-const-2.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; match x { 1 => x, 3 => x, x => x } : U8 +let x = 3; match x { 1 => x, 3 => x, x => x } : U8 ''' stderr = '' diff --git a/tests/succeed/match/synth-simple-redundant.snap b/tests/succeed/match/synth-simple-redundant.snap index 513fcab7c..03f6fed65 100644 --- a/tests/succeed/match/synth-simple-redundant.snap +++ b/tests/succeed/match/synth-simple-redundant.snap @@ -1,5 +1,5 @@ stdout = ''' -let x : U8 = 3; x : U8 +let x = 3; x : U8 ''' stderr = ''' warning: unreachable pattern diff --git a/tests/succeed/match/synth-simple.snap b/tests/succeed/match/synth-simple.snap index 6e26ddc52..01ad8a156 100644 --- a/tests/succeed/match/synth-simple.snap +++ b/tests/succeed/match/synth-simple.snap @@ -1,4 +1,4 @@ stdout = ''' -let x : U8 = 3; x : U8 +let x = 3; x : U8 ''' stderr = '' diff --git a/tests/succeed/numeric-literal/styled.snap b/tests/succeed/numeric-literal/styled.snap index 1f0c9a2d9..63de44f60 100644 --- a/tests/succeed/numeric-literal/styled.snap +++ b/tests/succeed/numeric-literal/styled.snap @@ -1,12 +1,7 @@ stdout = ''' -let x : U32 = 4660; -let _ : U16 = match x { - 0b1111 => 0b10, - 0x1234 => 0b1, - "head" => 0b100, - _ => 0xffff, -}; -let beef : U16 = 0xbeef; +let x = 4660; +let _ = match x { 0b1111 => 0b10, 0x1234 => 0b1, "head" => 0b100, _ => 0xffff }; +let beef = 0xbeef; Void : Type ''' stderr = '' diff --git a/tests/succeed/ops-sugar.snap b/tests/succeed/ops-sugar.snap index 4eb8af92b..794cef695 100644 --- a/tests/succeed/ops-sugar.snap +++ b/tests/succeed/ops-sugar.snap @@ -1,86 +1,86 @@ stdout = ''' -let test : U8 = (1 : U8) * (2 : U8); -let test : U16 = (1 : U16) * (2 : U16); -let test : U32 = (1 : U32) * (2 : U32); -let test : U64 = (1 : U64) * (2 : U64); -let test : S8 = (1 : S8) * (2 : S8); -let test : S16 = (1 : S16) * (2 : S16); -let test : S32 = (1 : S32) * (2 : S32); -let test : S64 = (1 : S64) * (2 : S64); -let test : U8 = (1 : U8) / (2 : U8); -let test : U16 = (1 : U16) / (2 : U16); -let test : U32 = (1 : U32) / (2 : U32); -let test : U64 = (1 : U64) / (2 : U64); -let test : S8 = (1 : S8) / (2 : S8); -let test : S16 = (1 : S16) / (2 : S16); -let test : S32 = (1 : S32) / (2 : S32); -let test : S64 = (1 : S64) / (2 : S64); -let test : U8 = (1 : U8) + (2 : U8); -let test : U16 = (1 : U16) + (2 : U16); -let test : U32 = (1 : U32) + (2 : U32); -let test : U64 = (1 : U64) + (2 : U64); -let test : S8 = (1 : S8) + (2 : S8); -let test : S16 = (1 : S16) + (2 : S16); -let test : S32 = (1 : S32) + (2 : S32); -let test : S64 = (1 : S64) + (2 : S64); -let test : U8 = (2 : U8) - (1 : U8); -let test : U16 = (2 : U16) - (1 : U16); -let test : U32 = (2 : U32) - (1 : U32); -let test : U64 = (2 : U64) - (1 : U64); -let test : S8 = (1 : S8) - (2 : S8); -let test : S16 = (1 : S16) - (2 : S16); -let test : S32 = (1 : S32) - (2 : S32); -let test : S64 = (1 : S64) - (2 : S64); -let test : Bool = true == false; -let test : Bool = (1 : U8) == (2 : U8); -let test : Bool = (1 : U16) == (2 : U16); -let test : Bool = (1 : U32) == (2 : U32); -let test : Bool = (1 : U64) == (2 : U64); -let test : Bool = (1 : S8) == (2 : S8); -let test : Bool = (1 : S16) == (2 : S16); -let test : Bool = (1 : S32) == (2 : S32); -let test : Bool = (1 : S64) == (2 : S64); -let test : Bool = true != false; -let test : Bool = (1 : U8) != (2 : U8); -let test : Bool = (1 : U16) != (2 : U16); -let test : Bool = (1 : U32) != (2 : U32); -let test : Bool = (1 : U64) != (2 : U64); -let test : Bool = (1 : S8) != (2 : S8); -let test : Bool = (1 : S16) != (2 : S16); -let test : Bool = (1 : S32) != (2 : S32); -let test : Bool = (1 : S64) != (2 : S64); -let test : Bool = (1 : U8) < (2 : U8); -let test : Bool = (1 : U16) < (2 : U16); -let test : Bool = (1 : U32) < (2 : U32); -let test : Bool = (1 : U64) < (2 : U64); -let test : Bool = (1 : S8) < (2 : S8); -let test : Bool = (1 : S16) < (2 : S16); -let test : Bool = (1 : S32) < (2 : S32); -let test : Bool = (1 : S64) < (2 : S64); -let test : Bool = (1 : U8) <= (2 : U8); -let test : Bool = (1 : U16) <= (2 : U16); -let test : Bool = (1 : U32) <= (2 : U32); -let test : Bool = (1 : U64) <= (2 : U64); -let test : Bool = (1 : S8) <= (2 : S8); -let test : Bool = (1 : S16) <= (2 : S16); -let test : Bool = (1 : S32) <= (2 : S32); -let test : Bool = (1 : S64) <= (2 : S64); -let test : Bool = (1 : U8) > (2 : U8); -let test : Bool = (1 : U16) > (2 : U16); -let test : Bool = (1 : U32) > (2 : U32); -let test : Bool = (1 : U64) > (2 : U64); -let test : Bool = (1 : S8) > (2 : S8); -let test : Bool = (1 : S16) > (2 : S16); -let test : Bool = (1 : S32) > (2 : S32); -let test : Bool = (1 : S64) > (2 : S64); -let test : Bool = (1 : U8) >= (2 : U8); -let test : Bool = (1 : U16) >= (2 : U16); -let test : Bool = (1 : U32) >= (2 : U32); -let test : Bool = (1 : U64) >= (2 : U64); -let test : Bool = (1 : S8) >= (2 : S8); -let test : Bool = (1 : S16) >= (2 : S16); -let test : Bool = (1 : S32) >= (2 : S32); -let test : Bool = (1 : S64) >= (2 : S64); +let test = (1 : U8) * (2 : U8); +let test = (1 : U16) * (2 : U16); +let test = (1 : U32) * (2 : U32); +let test = (1 : U64) * (2 : U64); +let test = (1 : S8) * (2 : S8); +let test = (1 : S16) * (2 : S16); +let test = (1 : S32) * (2 : S32); +let test = (1 : S64) * (2 : S64); +let test = (1 : U8) / (2 : U8); +let test = (1 : U16) / (2 : U16); +let test = (1 : U32) / (2 : U32); +let test = (1 : U64) / (2 : U64); +let test = (1 : S8) / (2 : S8); +let test = (1 : S16) / (2 : S16); +let test = (1 : S32) / (2 : S32); +let test = (1 : S64) / (2 : S64); +let test = (1 : U8) + (2 : U8); +let test = (1 : U16) + (2 : U16); +let test = (1 : U32) + (2 : U32); +let test = (1 : U64) + (2 : U64); +let test = (1 : S8) + (2 : S8); +let test = (1 : S16) + (2 : S16); +let test = (1 : S32) + (2 : S32); +let test = (1 : S64) + (2 : S64); +let test = (2 : U8) - (1 : U8); +let test = (2 : U16) - (1 : U16); +let test = (2 : U32) - (1 : U32); +let test = (2 : U64) - (1 : U64); +let test = (1 : S8) - (2 : S8); +let test = (1 : S16) - (2 : S16); +let test = (1 : S32) - (2 : S32); +let test = (1 : S64) - (2 : S64); +let test = true == false; +let test = (1 : U8) == (2 : U8); +let test = (1 : U16) == (2 : U16); +let test = (1 : U32) == (2 : U32); +let test = (1 : U64) == (2 : U64); +let test = (1 : S8) == (2 : S8); +let test = (1 : S16) == (2 : S16); +let test = (1 : S32) == (2 : S32); +let test = (1 : S64) == (2 : S64); +let test = true != false; +let test = (1 : U8) != (2 : U8); +let test = (1 : U16) != (2 : U16); +let test = (1 : U32) != (2 : U32); +let test = (1 : U64) != (2 : U64); +let test = (1 : S8) != (2 : S8); +let test = (1 : S16) != (2 : S16); +let test = (1 : S32) != (2 : S32); +let test = (1 : S64) != (2 : S64); +let test = (1 : U8) < (2 : U8); +let test = (1 : U16) < (2 : U16); +let test = (1 : U32) < (2 : U32); +let test = (1 : U64) < (2 : U64); +let test = (1 : S8) < (2 : S8); +let test = (1 : S16) < (2 : S16); +let test = (1 : S32) < (2 : S32); +let test = (1 : S64) < (2 : S64); +let test = (1 : U8) <= (2 : U8); +let test = (1 : U16) <= (2 : U16); +let test = (1 : U32) <= (2 : U32); +let test = (1 : U64) <= (2 : U64); +let test = (1 : S8) <= (2 : S8); +let test = (1 : S16) <= (2 : S16); +let test = (1 : S32) <= (2 : S32); +let test = (1 : S64) <= (2 : S64); +let test = (1 : U8) > (2 : U8); +let test = (1 : U16) > (2 : U16); +let test = (1 : U32) > (2 : U32); +let test = (1 : U64) > (2 : U64); +let test = (1 : S8) > (2 : S8); +let test = (1 : S16) > (2 : S16); +let test = (1 : S32) > (2 : S32); +let test = (1 : S64) > (2 : S64); +let test = (1 : U8) >= (2 : U8); +let test = (1 : U16) >= (2 : U16); +let test = (1 : U32) >= (2 : U32); +let test = (1 : U64) >= (2 : U64); +let test = (1 : S8) >= (2 : S8); +let test = (1 : S16) >= (2 : S16); +let test = (1 : S32) >= (2 : S32); +let test = (1 : S64) >= (2 : S64); Type : Type ''' stderr = '' diff --git a/tests/succeed/prelude.snap b/tests/succeed/prelude.snap index 0775b8d3b..0d4d8528c 100644 --- a/tests/succeed/prelude.snap +++ b/tests/succeed/prelude.snap @@ -1,51 +1,68 @@ stdout = ''' -let id : fun (A : Type) -> A -> A = fun _ a => a; -let always : fun (A : Type) (B : Type) -> A -> B -> A = fun _ _ a _ => a; -let compose : fun (A : Type) (B : Type) (C : Type) -> (A -> B) -> (B -> C) -> A --> C = fun _ _ _ ab bc a => bc (ab a); -let Nat : Type = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; -let zero : Nat = fun Nat succ zero => zero; -let succ : Nat -> Nat = fun prev Nat succ zero => succ (prev Nat succ zero); -let add : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); -let mul : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; -let List : Type -> Type = fun Elem => fun (List : Type) -> List -> (Elem -> List --> List) -> List; -let nil : fun (Elem : Type) -> List Elem = fun Elem List nil cons => nil; -let cons : fun (Elem : Type) -> Elem -> List Elem -> List Elem = -fun Elem head tail List nil cons => cons head (tail List nil cons); -let Vec : Type -> Nat -> Type = fun Elem len => fun (Vec : Nat -> Type) -> -Vec zero -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem --> Vec len -> Vec (succ len)) -> Vec len; -let vnil : fun (Elem : Type) -> Vec Elem zero = fun Elem Vec nil cons => nil; -let vcons : fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) -> Elem -> Vec Elem len -> Vec Elem (succ len) = -fun Elem len head tail Vec nil cons => cons len head (tail Vec nil cons); -let Void : Type = fun (Void : Type) -> Void; -let absurd : fun (A : Type) -> Void -> A = fun A void => void A; -let Unit : Type = fun (Unit : Type) -> Unit -> Unit; -let unit : Unit = fun Unit unit => unit; -let Eq : fun (A : Type) -> A -> A -> Type = fun A a0 a1 => fun (P : A -> -Type) -> P a0 -> P a1; -let refl : fun (A : Type) (a : A) -> Eq A a a = fun A a P => id (P a); -let trans : fun (A : Type) (a0 : A) (a1 : A) (a2 : A) -> Eq A a0 a1 -> -Eq A a1 a2 -> Eq A a0 a2 = -fun _ a0 a1 a2 p0 p1 P => compose (P a0) (P a1) (P a2) (p0 P) (p1 P); -let sym : fun (A : Type) (a0 : A) (a1 : A) -> Eq A a0 a1 -> Eq A a1 a0 = -fun a a0 a1 p => p (fun a1 => Eq a a1 a0) (refl a a0); -let id_apply_type : Type = (fun a => a) Type; -let list1 : List Bool = cons Bool (id Bool true) (nil Bool); -let five : Nat = succ (succ (succ (succ (succ zero)))); -let ten : Nat = add five five; -let hundred : Nat = mul ten ten; -let thousand : Nat = mul ten hundred; -let eq_test : Eq (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) hundred hundred = refl (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))); -let eq_id_apply_type : Eq Type ((fun a => a) Type) Type = refl Type Type; -let eq_id_apply_true : Eq Bool ((fun a => a) true) true = refl Bool true; -let eq_id_apply_false : Eq Bool ((fun a => a) false) false = refl Bool false; +let id = fun (a : Type) (a : a) => a; +let always = fun (a : Type) (b : Type) (a : a) (_ : b) => a; +let compose = fun (a : Type) (b : Type) (c : Type) (ab : a -> b) (bc : b -> +c) (a : a) => bc (ab a); +let Nat = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; +let zero = fun (Nat : Type) (succ : Nat -> Nat) (zero : Nat) => zero; +let succ = fun (prev : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : +Type) (succ : Nat -> Nat) (zero : Nat) => succ (prev Nat succ zero); +let add = fun (n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (n1 : +fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => n0 Nat succ (n1 Nat succ zero); +let mul = fun (n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (n1 : +fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => n0 Nat (n1 Nat succ) zero; +let List = fun (Elem : Type) => fun (List : Type) -> List -> (Elem -> List -> +List) -> List; +let nil = fun (Elem : Type) (List : Type) (nil : List) (cons : Elem -> List -> +List) => nil; +let cons = fun (Elem : Type) (head : Elem) (tail : fun (List : Type) -> List -> +(Elem -> List -> List) -> List) (List : Type) (nil : List) (cons : Elem -> List +-> List) => cons head (tail List nil cons); +let Vec = fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) => fun (Vec : Nat -> Type) -> Vec zero -> (fun (len : fun (Nat : Type) -> +(Nat -> Nat) -> Nat -> Nat) -> Elem -> Vec len -> Vec (succ len)) -> Vec len; +let vnil = fun (Elem : Type) (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Type) (nil : Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => zero)) (cons : fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => succ (len Nat succ zero))) => nil; +let vcons = fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) (head : Elem) (tail : fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat) -> Type) -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => zero) -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => succ (len Nat succ zero))) -> Vec len) (Vec : (fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Type) (nil : Vec (fun (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => zero)) (cons : fun (len : fun (Nat : Type) -> (Nat -> Nat) +-> Nat -> Nat) -> Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> +Nat) (zero : +Nat) => succ (len Nat succ zero))) => cons len head (tail Vec nil cons); +let Void = fun (Void : Type) -> Void; +let absurd = fun (A : Type) (void : fun (Void : Type) -> Void) => void A; +let Unit = fun (Unit : Type) -> Unit -> Unit; +let unit = fun (Unit : Type) (unit : Unit) => unit; +let Eq = fun (A : Type) (a0 : A) (a1 : A) => fun (P : A -> Type) -> P a0 -> +P a1; +let refl = fun (A : Type) (a : A) (P : A -> Type) => id (P a); +let trans = fun (a : Type) (a0 : a) (a1 : a) (a2 : a) (p0 : fun (P : a -> +Type) -> P a0 -> P a1) (p1 : fun (P : a -> Type) -> P a1 -> P a2) (P : a -> +Type) => compose (P a0) (P a1) (P a2) (p0 P) (p1 P); +let sym = fun (a : Type) (a0 : a) (a1 : a) (p : fun (P : a -> Type) -> P a0 -> +P a1) => p (fun (a1 : a) => Eq a a1 a0) (refl a a0); +let id_apply_type = (fun (a : Type) => a) Type; +let list1 = cons Bool (id Bool true) (nil Bool); +let five = succ (succ (succ (succ (succ zero)))); +let ten = add five five; +let hundred = mul ten ten; +let thousand = mul ten hundred; +let eq_test = refl (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : +reported_error) (a : reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))); +let eq_id_apply_type = refl Type Type; +let eq_id_apply_true = refl Bool true; +let eq_id_apply_false = refl Bool false; Type : Type ''' stderr = '' diff --git a/tests/succeed/primitive-ops.snap b/tests/succeed/primitive-ops.snap index d1994c908..5491d08c3 100644 --- a/tests/succeed/primitive-ops.snap +++ b/tests/succeed/primitive-ops.snap @@ -1,12 +1,12 @@ stdout = ''' -let test : Array8 ((1 : U8) + (2 : U8)) () -> Array8 3 () = fun x => x; -let test : Array16 ((1 : U16) + (2 : U16)) () -> Array16 3 () = fun x => x; -let test : Array32 ((1 : U32) + (2 : U32)) () -> Array32 3 () = fun x => x; -let test : Array64 ((1 : U64) + (2 : U64)) () -> Array64 3 () = fun x => x; -let test : Array8 ((3 : U8) - (1 : U8)) () -> Array8 2 () = fun x => x; -let test : Array16 ((3 : U16) - (1 : U16)) () -> Array16 2 () = fun x => x; -let test : Array32 ((3 : U32) - (1 : U32)) () -> Array32 2 () = fun x => x; -let test : Array64 ((3 : U64) - (1 : U64)) () -> Array64 2 () = fun x => x; +let test = fun (x : Array8 3 ()) => x; +let test = fun (x : Array16 3 ()) => x; +let test = fun (x : Array32 3 ()) => x; +let test = fun (x : Array64 3 ()) => x; +let test = fun (x : Array8 2 ()) => x; +let test = fun (x : Array16 2 ()) => x; +let test = fun (x : Array32 2 ()) => x; +let test = fun (x : Array64 2 ()) => x; Type : Type ''' stderr = '' diff --git a/tests/succeed/primitives.snap b/tests/succeed/primitives.snap index d3d8a8525..d82fec60f 100644 --- a/tests/succeed/primitives.snap +++ b/tests/succeed/primitives.snap @@ -1,215 +1,207 @@ stdout = ''' -let _ : Type = Void; -let _ : Type = Bool; -let _ : Type = U8; -let _ : Type = U16; -let _ : Type = U32; -let _ : Type = U64; -let _ : Type = S8; -let _ : Type = S16; -let _ : Type = S32; -let _ : Type = S64; -let _ : Type = F32; -let _ : Type = F64; -let _ : Type -> Type = Option; -let _ : Type -> Type = Array; -let _ : U8 -> Type -> Type = Array8; -let _ : U16 -> Type -> Type = Array16; -let _ : U32 -> Type -> Type = Array32; -let _ : U64 -> Type -> Type = Array64; -let _ : Type = Pos; -let _ : Format -> Type = Ref; -let _ : U8 = 1; -let _ : U16 = 1; -let _ : U32 = 1; -let _ : U64 = 1; -let _ : S8 = 1; -let _ : S16 = 1; -let _ : S32 = 1; -let _ : S64 = 1; -let _ : F32 = 1; -let _ : F64 = 1; -let _ : Type = Format; -let _ : Format = u8; -let _ : Format = u16be; -let _ : Format = u16le; -let _ : Format = u32be; -let _ : Format = u32le; -let _ : Format = u64be; -let _ : Format = u64le; -let _ : Format = s8; -let _ : Format = s16be; -let _ : Format = s16le; -let _ : Format = s32be; -let _ : Format = s32le; -let _ : Format = s64be; -let _ : Format = s64le; -let _ : Format = f32be; -let _ : Format = f32le; -let _ : Format = f64be; -let _ : Format = f64le; -let _ : U8 -> Format -> Format = repeat_len8; -let _ : U16 -> Format -> Format = repeat_len16; -let _ : U32 -> Format -> Format = repeat_len32; -let _ : U64 -> Format -> Format = repeat_len64; -let _ : Format -> Format = repeat_until_end; -let _ : U8 -> Format -> Format = repeat_len8; -let _ : U16 -> Format -> Format = repeat_len16; -let _ : U32 -> Format -> Format = repeat_len32; -let _ : U64 -> Format -> Format = repeat_len64; -let _ : Pos -> Format -> Format = link; -let _ : fun (@f : Format) -> Ref f -> Format = deref; -let _ : Format = stream_pos; -let _ : fun (@A : Type) -> A -> Format = succeed; -let _ : Format = fail; -let _ : fun (@A : Type) -> Option A -> Format = unwrap; -let _ : Format -> Type = Repr; -let _ : fun (@A : Type) -> Void -> A = absurd; -let _ : Bool -> Bool -> Bool = bool_eq; -let _ : Bool -> Bool -> Bool = bool_neq; -let _ : Bool -> Bool = bool_not; -let _ : Bool -> Bool -> Bool = bool_and; -let _ : Bool -> Bool -> Bool = bool_or; -let _ : Bool -> Bool -> Bool = bool_xor; -let _ : U8 -> U8 -> Bool = u8_eq; -let _ : U8 -> U8 -> Bool = u8_neq; -let _ : U8 -> U8 -> Bool = u8_gt; -let _ : U8 -> U8 -> Bool = u8_lt; -let _ : U8 -> U8 -> Bool = u8_gte; -let _ : U8 -> U8 -> Bool = u8_lte; -let _ : U8 -> U8 -> U8 = u8_add; -let _ : U8 -> U8 -> U8 = u8_sub; -let _ : U8 -> U8 -> U8 = u8_mul; -let _ : U8 -> U8 -> U8 = u8_div; -let _ : U8 -> U8 = u8_not; -let _ : U8 -> U8 -> U8 = u8_shl; -let _ : U8 -> U8 -> U8 = u8_shr; -let _ : U8 -> U8 -> U8 = u8_and; -let _ : U8 -> U8 -> U8 = u8_or; -let _ : U8 -> U8 -> U8 = u8_xor; -let _ : U16 -> U16 -> Bool = u16_eq; -let _ : U16 -> U16 -> Bool = u16_neq; -let _ : U16 -> U16 -> Bool = u16_gt; -let _ : U16 -> U16 -> Bool = u16_lt; -let _ : U16 -> U16 -> Bool = u16_gte; -let _ : U16 -> U16 -> Bool = u16_lte; -let _ : U16 -> U16 -> U16 = u16_add; -let _ : U16 -> U16 -> U16 = u16_sub; -let _ : U16 -> U16 -> U16 = u16_mul; -let _ : U16 -> U16 -> U16 = u16_div; -let _ : U16 -> U16 = u16_not; -let _ : U16 -> U8 -> U16 = u16_shl; -let _ : U16 -> U8 -> U16 = u16_shr; -let _ : U16 -> U16 -> U16 = u16_and; -let _ : U16 -> U16 -> U16 = u16_or; -let _ : U16 -> U16 -> U16 = u16_xor; -let _ : U32 -> U32 -> Bool = u32_eq; -let _ : U32 -> U32 -> Bool = u32_neq; -let _ : U32 -> U32 -> Bool = u32_gt; -let _ : U32 -> U32 -> Bool = u32_lt; -let _ : U32 -> U32 -> Bool = u32_gte; -let _ : U32 -> U32 -> Bool = u32_lte; -let _ : U32 -> U32 -> U32 = u32_add; -let _ : U32 -> U32 -> U32 = u32_sub; -let _ : U32 -> U32 -> U32 = u32_mul; -let _ : U32 -> U32 -> U32 = u32_div; -let _ : U32 -> U32 = u32_not; -let _ : U32 -> U8 -> U32 = u32_shl; -let _ : U32 -> U8 -> U32 = u32_shr; -let _ : U32 -> U32 -> U32 = u32_and; -let _ : U32 -> U32 -> U32 = u32_or; -let _ : U32 -> U32 -> U32 = u32_xor; -let _ : U64 -> U64 -> Bool = u64_eq; -let _ : U64 -> U64 -> Bool = u64_neq; -let _ : U64 -> U64 -> Bool = u64_gt; -let _ : U64 -> U64 -> Bool = u64_lt; -let _ : U64 -> U64 -> Bool = u64_gte; -let _ : U64 -> U64 -> Bool = u64_lte; -let _ : U64 -> U64 -> U64 = u64_add; -let _ : U64 -> U64 -> U64 = u64_sub; -let _ : U64 -> U64 -> U64 = u64_mul; -let _ : U64 -> U64 -> U64 = u64_div; -let _ : U64 -> U64 = u64_not; -let _ : U64 -> U8 -> U64 = u64_shl; -let _ : U64 -> U8 -> U64 = u64_shr; -let _ : U64 -> U64 -> U64 = u64_and; -let _ : U64 -> U64 -> U64 = u64_or; -let _ : U64 -> U64 -> U64 = u64_xor; -let _ : S8 -> S8 -> Bool = s8_eq; -let _ : S8 -> S8 -> Bool = s8_neq; -let _ : S8 -> S8 -> Bool = s8_gt; -let _ : S8 -> S8 -> Bool = s8_lt; -let _ : S8 -> S8 -> Bool = s8_gte; -let _ : S8 -> S8 -> Bool = s8_lte; -let _ : S8 -> S8 = s8_neg; -let _ : S8 -> S8 -> S8 = s8_add; -let _ : S8 -> S8 -> S8 = s8_sub; -let _ : S8 -> S8 -> S8 = s8_mul; -let _ : S8 -> S8 -> S8 = s8_div; -let _ : S8 -> S8 = s8_abs; -let _ : S8 -> U8 = s8_unsigned_abs; -let _ : S16 -> S16 -> Bool = s16_eq; -let _ : S16 -> S16 -> Bool = s16_neq; -let _ : S16 -> S16 -> Bool = s16_gt; -let _ : S16 -> S16 -> Bool = s16_lt; -let _ : S16 -> S16 -> Bool = s16_gte; -let _ : S16 -> S16 -> Bool = s16_lte; -let _ : S16 -> S16 = s16_neg; -let _ : S16 -> S16 -> S16 = s16_add; -let _ : S16 -> S16 -> S16 = s16_sub; -let _ : S16 -> S16 -> S16 = s16_mul; -let _ : S16 -> S16 -> S16 = s16_div; -let _ : S16 -> S16 = s16_abs; -let _ : S16 -> U16 = s16_unsigned_abs; -let _ : S32 -> S32 -> Bool = s32_eq; -let _ : S32 -> S32 -> Bool = s32_neq; -let _ : S32 -> S32 -> Bool = s32_gt; -let _ : S32 -> S32 -> Bool = s32_lt; -let _ : S32 -> S32 -> Bool = s32_gte; -let _ : S32 -> S32 -> Bool = s32_lte; -let _ : S32 -> S32 = s32_neg; -let _ : S32 -> S32 -> S32 = s32_add; -let _ : S32 -> S32 -> S32 = s32_sub; -let _ : S32 -> S32 -> S32 = s32_mul; -let _ : S32 -> S32 -> S32 = s32_div; -let _ : S32 -> S32 = s32_abs; -let _ : S32 -> U32 = s32_unsigned_abs; -let _ : S64 -> S64 -> Bool = s64_eq; -let _ : S64 -> S64 -> Bool = s64_neq; -let _ : S64 -> S64 -> Bool = s64_gt; -let _ : S64 -> S64 -> Bool = s64_lt; -let _ : S64 -> S64 -> Bool = s64_gte; -let _ : S64 -> S64 -> Bool = s64_lte; -let _ : S64 -> S64 = s64_neg; -let _ : S64 -> S64 -> S64 = s64_add; -let _ : S64 -> S64 -> S64 = s64_sub; -let _ : S64 -> S64 -> S64 = s64_mul; -let _ : S64 -> S64 -> S64 = s64_div; -let _ : S64 -> S64 = s64_abs; -let _ : S64 -> U64 = s64_unsigned_abs; -let _ : fun (@A : Type) -> A -> Option A = some; -let _ : fun (@A : Type) -> Option A = none; -let _ : fun (@A : Type) (@B : Type) -> B -> (A -> B) -> Option A -> B = -option_fold; -let _ : fun (@len : U8) (@A : Type) -> (A -> Bool) -> Array8 len A -> Option A = -array8_find; -let _ : fun (@len : U16) (@A : Type) -> (A -> Bool) -> Array16 len A -> -Option A = array16_find; -let _ : fun (@len : U32) (@A : Type) -> (A -> Bool) -> Array32 len A -> -Option A = array32_find; -let _ : fun (@len : U64) (@A : Type) -> (A -> Bool) -> Array64 len A -> -Option A = array64_find; -let _ : fun (@len : U8) (@A : Type) -> U8 -> Array8 len A -> A = array8_index; -let _ : fun (@len : U16) (@A : Type) -> U16 -> Array16 len A -> A = -array16_index; -let _ : fun (@len : U32) (@A : Type) -> U32 -> Array32 len A -> A = -array32_index; -let _ : fun (@len : U64) (@A : Type) -> U64 -> Array64 len A -> A = -array64_index; -let _ : Pos -> U8 -> Pos = pos_add_u8; -let _ : Pos -> U16 -> Pos = pos_add_u16; -let _ : Pos -> U32 -> Pos = pos_add_u32; -let _ : Pos -> U64 -> Pos = pos_add_u64; +let _ = Void; +let _ = Bool; +let _ = U8; +let _ = U16; +let _ = U32; +let _ = U64; +let _ = S8; +let _ = S16; +let _ = S32; +let _ = S64; +let _ = F32; +let _ = F64; +let _ = Option; +let _ = Array; +let _ = Array8; +let _ = Array16; +let _ = Array32; +let _ = Array64; +let _ = Pos; +let _ = Ref; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = 1; +let _ = Format; +let _ = u8; +let _ = u16be; +let _ = u16le; +let _ = u32be; +let _ = u32le; +let _ = u64be; +let _ = u64le; +let _ = s8; +let _ = s16be; +let _ = s16le; +let _ = s32be; +let _ = s32le; +let _ = s64be; +let _ = s64le; +let _ = f32be; +let _ = f32le; +let _ = f64be; +let _ = f64le; +let _ = repeat_len8; +let _ = repeat_len16; +let _ = repeat_len32; +let _ = repeat_len64; +let _ = repeat_until_end; +let _ = repeat_len8; +let _ = repeat_len16; +let _ = repeat_len32; +let _ = repeat_len64; +let _ = link; +let _ = deref; +let _ = stream_pos; +let _ = succeed; +let _ = fail; +let _ = unwrap; +let _ = Repr; +let _ = absurd; +let _ = bool_eq; +let _ = bool_neq; +let _ = bool_not; +let _ = bool_and; +let _ = bool_or; +let _ = bool_xor; +let _ = u8_eq; +let _ = u8_neq; +let _ = u8_gt; +let _ = u8_lt; +let _ = u8_gte; +let _ = u8_lte; +let _ = u8_add; +let _ = u8_sub; +let _ = u8_mul; +let _ = u8_div; +let _ = u8_not; +let _ = u8_shl; +let _ = u8_shr; +let _ = u8_and; +let _ = u8_or; +let _ = u8_xor; +let _ = u16_eq; +let _ = u16_neq; +let _ = u16_gt; +let _ = u16_lt; +let _ = u16_gte; +let _ = u16_lte; +let _ = u16_add; +let _ = u16_sub; +let _ = u16_mul; +let _ = u16_div; +let _ = u16_not; +let _ = u16_shl; +let _ = u16_shr; +let _ = u16_and; +let _ = u16_or; +let _ = u16_xor; +let _ = u32_eq; +let _ = u32_neq; +let _ = u32_gt; +let _ = u32_lt; +let _ = u32_gte; +let _ = u32_lte; +let _ = u32_add; +let _ = u32_sub; +let _ = u32_mul; +let _ = u32_div; +let _ = u32_not; +let _ = u32_shl; +let _ = u32_shr; +let _ = u32_and; +let _ = u32_or; +let _ = u32_xor; +let _ = u64_eq; +let _ = u64_neq; +let _ = u64_gt; +let _ = u64_lt; +let _ = u64_gte; +let _ = u64_lte; +let _ = u64_add; +let _ = u64_sub; +let _ = u64_mul; +let _ = u64_div; +let _ = u64_not; +let _ = u64_shl; +let _ = u64_shr; +let _ = u64_and; +let _ = u64_or; +let _ = u64_xor; +let _ = s8_eq; +let _ = s8_neq; +let _ = s8_gt; +let _ = s8_lt; +let _ = s8_gte; +let _ = s8_lte; +let _ = s8_neg; +let _ = s8_add; +let _ = s8_sub; +let _ = s8_mul; +let _ = s8_div; +let _ = s8_abs; +let _ = s8_unsigned_abs; +let _ = s16_eq; +let _ = s16_neq; +let _ = s16_gt; +let _ = s16_lt; +let _ = s16_gte; +let _ = s16_lte; +let _ = s16_neg; +let _ = s16_add; +let _ = s16_sub; +let _ = s16_mul; +let _ = s16_div; +let _ = s16_abs; +let _ = s16_unsigned_abs; +let _ = s32_eq; +let _ = s32_neq; +let _ = s32_gt; +let _ = s32_lt; +let _ = s32_gte; +let _ = s32_lte; +let _ = s32_neg; +let _ = s32_add; +let _ = s32_sub; +let _ = s32_mul; +let _ = s32_div; +let _ = s32_abs; +let _ = s32_unsigned_abs; +let _ = s64_eq; +let _ = s64_neq; +let _ = s64_gt; +let _ = s64_lt; +let _ = s64_gte; +let _ = s64_lte; +let _ = s64_neg; +let _ = s64_add; +let _ = s64_sub; +let _ = s64_mul; +let _ = s64_div; +let _ = s64_abs; +let _ = s64_unsigned_abs; +let _ = some; +let _ = none; +let _ = option_fold; +let _ = array8_find; +let _ = array16_find; +let _ = array32_find; +let _ = array64_find; +let _ = array8_index; +let _ = array16_index; +let _ = array32_index; +let _ = array64_index; +let _ = pos_add_u8; +let _ = pos_add_u16; +let _ = pos_add_u32; +let _ = pos_add_u64; Type : Type ''' stderr = '' diff --git a/tests/succeed/raw-identifiers.snap b/tests/succeed/raw-identifiers.snap index 729c6c5c1..6cbbabae8 100644 --- a/tests/succeed/raw-identifiers.snap +++ b/tests/succeed/raw-identifiers.snap @@ -1,4 +1,4 @@ stdout = ''' -let r#def : Bool = false; let foo : Bool = r#def; foo : Bool +let r#def = false; let foo = r#def; foo : Bool ''' stderr = '' diff --git a/tests/succeed/record-type/generic-pair.snap b/tests/succeed/record-type/generic-pair.snap index bc481921a..d8e2728c7 100644 --- a/tests/succeed/record-type/generic-pair.snap +++ b/tests/succeed/record-type/generic-pair.snap @@ -1,6 +1,6 @@ stdout = ''' -let fst : fun (A : Type) (B : Type) -> { x : A, y : B } -> A = fun A B p => p.x; -let snd : fun (A : Type) (B : Type) -> { x : A, y : B } -> B = fun A B p => p.y; +let fst = fun (A : Type) (B : Type) (p : { x : A, y : B }) => p.x; +let snd = fun (A : Type) (B : Type) (p : { x : A, y : B }) => p.y; () : () ''' stderr = '' diff --git a/tests/succeed/record-type/generic-point.snap b/tests/succeed/record-type/generic-point.snap index cf67a8938..30fb486a9 100644 --- a/tests/succeed/record-type/generic-point.snap +++ b/tests/succeed/record-type/generic-point.snap @@ -1,6 +1,6 @@ stdout = ''' -let Point : Type -> Type = fun A => { x : A, y : A }; -let test_point : fun (A : Type) -> Point A -> { x : A, y : A } = fun A p => p; +let Point = fun (A : Type) => { x : A, y : A }; +let test_point = fun (A : Type) (p : { x : A, y : A }) => p; Type : Type ''' stderr = '' diff --git a/tests/succeed/record-type/generic-singleton.snap b/tests/succeed/record-type/generic-singleton.snap index df5327e5f..b3613a32f 100644 --- a/tests/succeed/record-type/generic-singleton.snap +++ b/tests/succeed/record-type/generic-singleton.snap @@ -1,6 +1,6 @@ stdout = ''' -let Singleton : Type -> Type = fun A => { x : A }; -let test_point : fun (A : Type) -> Singleton A -> { x : A } = fun A p => p; +let Singleton = fun (A : Type) => { x : A }; +let test_point = fun (A : Type) (p : { x : A }) => p; Type : Type ''' stderr = '' diff --git a/tests/succeed/record-type/generic-triple.snap b/tests/succeed/record-type/generic-triple.snap index 4095a0489..449d9f608 100644 --- a/tests/succeed/record-type/generic-triple.snap +++ b/tests/succeed/record-type/generic-triple.snap @@ -1,10 +1,19 @@ stdout = ''' -let get1 : fun (A : Type) (B : Type) (C : Type) -> { x : A, y : B, z : C } -> -A = fun A B C p => p.x; -let get2 : fun (A : Type) (B : Type) (C : Type) -> { x : A, y : B, z : C } -> -B = fun A B C p => p.y; -let get3 : fun (A : Type) (B : Type) (C : Type) -> { x : A, y : B, z : C } -> -C = fun A B C p => p.z; +let get1 = fun (A : Type) (B : Type) (C : Type) (p : { + x : A, + y : B, + z : C, +}) => p.x; +let get2 = fun (A : Type) (B : Type) (C : Type) (p : { + x : A, + y : B, + z : C, +}) => p.y; +let get3 = fun (A : Type) (B : Type) (C : Type) (p : { + x : A, + y : B, + z : C, +}) => p.z; () : () ''' stderr = '' diff --git a/tests/succeed/stress.snap b/tests/succeed/stress.snap index 303161fb1..3ed0342ce 100644 --- a/tests/succeed/stress.snap +++ b/tests/succeed/stress.snap @@ -1,6 +1,6 @@ stdout = ''' -let id : fun (A : Type) -> A -> A = fun A a => a; -let id_test : fun (A : Type) -> A -> A = id (fun (A : Type) -> A -> +let id = fun (A : Type) (a : A) => a; +let id_test = id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : @@ -65,165 +65,234 @@ A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> -A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id (fun (A : -Type) -> A -> A) id; -let Nat : Type = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; -let zero : Nat = fun Nat succ zero => zero; -let succ : Nat -> Nat = fun prev Nat succ zero => succ (prev Nat succ zero); -let add : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat succ (n1 Nat succ zero); -let mul : Nat -> Nat -> Nat = -fun n0 n1 Nat succ zero => n0 Nat (n1 Nat succ) zero; -let n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = zero; -let n1 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n0; -let n2 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n1; -let n3 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n2; -let n4 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n3; -let n5 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n4; -let n6 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n5; -let n7 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n6; -let n8 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n7; -let n9 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n8; -let n10 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = succ n9; -let n3000 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat = -mul n10 (mul n10 (mul n10 n3)); -let Vec : Type -> Nat -> Type = fun Elem len => fun (Vec : Nat -> Type) -> -Vec zero -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> Elem --> Vec len -> Vec (succ len)) -> Vec len; -let vnil : fun (Elem : Type) -> Vec Elem zero = fun Elem Vec nil cons => nil; -let vcons : fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) -> Elem -> Vec Elem len -> Vec Elem (succ len) = -fun Elem len head tail Vec nil cons => cons len head (tail Vec nil cons); -let vec1 : fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> -Type) -> Vec (fun Nat succ zero => zero) -> (fun (len : fun (Nat : Type) -> (Nat --> Nat) -> Nat -> Nat) -> (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> -Vec len -> Vec (fun Nat succ zero => succ (len Nat succ zero))) -> -Vec (fun Nat succ zero => succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) = -vcons (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a (a b))))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a (a b)))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a (a b))))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a (a b)))))))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a (a b))))))) zero (vcons (fun (Nat : Type) -> -(Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a (a b)))))) zero (vcons (fun (Nat : Type) -> -(Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a (a (a b))))) zero (vcons (fun (Nat : Type) -> (Nat -> -Nat) -> Nat -> Nat) (fun _ a b => a (a (a (a b)))) zero (vcons (fun (Nat : -Type) -> (Nat -> Nat) -> Nat -> -Nat) (fun _ a b => a (a (a b))) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) -> -Nat -> Nat) (fun _ a b => a (a b)) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) --> Nat -> Nat) (fun _ a b => a b) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) --> Nat -> Nat) (fun _ _ a => a) zero (vnil (fun (Nat : Type) -> (Nat -> Nat) -> -Nat -> Nat))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))); +A) id (fun (A : Type) -> A -> A) id (fun (A : Type) -> A -> A) id; +let Nat = fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat; +let zero = fun (Nat : Type) (succ : Nat -> Nat) (zero : Nat) => zero; +let succ = fun (prev : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : +Type) (succ : Nat -> Nat) (zero : Nat) => succ (prev Nat succ zero); +let add = fun (n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (n1 : +fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => n0 Nat succ (n1 Nat succ zero); +let mul = fun (n0 : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (n1 : +fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => n0 Nat (n1 Nat succ) zero; +let n0 = zero; +let n1 = succ n0; +let n2 = succ n1; +let n3 = succ n2; +let n4 = succ n3; +let n5 = succ n4; +let n6 = succ n5; +let n7 = succ n6; +let n8 = succ n7; +let n9 = succ n8; +let n10 = succ n9; +let n3000 = mul n10 (mul n10 (mul n10 n3)); +let Vec = fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) => fun (Vec : Nat -> Type) -> Vec zero -> (fun (len : fun (Nat : Type) -> +(Nat -> Nat) -> Nat -> Nat) -> Elem -> Vec len -> Vec (succ len)) -> Vec len; +let vnil = fun (Elem : Type) (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Type) (nil : Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => zero)) (cons : fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) -> Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => succ (len Nat succ zero))) => nil; +let vcons = fun (Elem : Type) (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) (head : Elem) (tail : fun (Vec : (fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat) -> Type) -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => zero) -> (fun (len : fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) -> +Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> Nat) (zero : +Nat) => succ (len Nat succ zero))) -> Vec len) (Vec : (fun (Nat : Type) -> (Nat +-> Nat) -> Nat -> Nat) -> Type) (nil : Vec (fun (Nat : Type) (succ : Nat -> +Nat) (zero : Nat) => zero)) (cons : fun (len : fun (Nat : Type) -> (Nat -> Nat) +-> Nat -> Nat) -> Elem -> Vec len -> Vec (fun (Nat : Type) (succ : Nat -> +Nat) (zero : +Nat) => succ (len Nat succ zero))) => cons len head (tail Vec nil cons); +let vec1 = vcons (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : +reported_error) (a : reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a (a b))))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a (a b)))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a (a b))))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a (a b)))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a (a b))))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a (a b)))))))) zero (vcons (fun (Nat : +Type) -> (Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : +reported_error) (b : +reported_error) => a (a (a (a (a (a (a b))))))) zero (vcons (fun (Nat : Type) -> +(Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a (a (a (a (a (a b)))))) zero (vcons (fun (Nat : Type) -> +(Nat -> Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a (a (a (a (a b))))) zero (vcons (fun (Nat : Type) -> (Nat -> +Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a (a (a (a b)))) zero (vcons (fun (Nat : Type) -> (Nat -> +Nat) -> Nat -> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a (a (a b))) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) -> +Nat -> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a (a b)) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) -> Nat +-> Nat) (fun (_ : reported_error) (a : reported_error) (b : +reported_error) => a b) zero (vcons (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat) (fun (_ : reported_error) (_ : reported_error) (a : +reported_error) => a) zero (vnil (fun (Nat : Type) -> (Nat -> Nat) -> Nat -> +Nat))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))); Type : Type ''' stderr = '' diff --git a/tests/succeed/tuple/check-format.snap b/tests/succeed/tuple/check-format.snap index 854a2e530..4b1891f63 100644 --- a/tests/succeed/tuple/check-format.snap +++ b/tests/succeed/tuple/check-format.snap @@ -1,9 +1,9 @@ stdout = ''' -let Unit : Format = (); -let Paren : Format = u8; -let Single : Format = (u8,); -let Pair : Format = (u8, u8); -let Triple : Format = (u8, u8, u8); +let Unit = (); +let Paren = u8; +let Single = (u8,); +let Pair = (u8, u8); +let Triple = (u8, u8, u8); Unit : Format ''' stderr = '' diff --git a/tests/succeed/tuple/check-term.snap b/tests/succeed/tuple/check-term.snap index c2ecc8ef3..083b73564 100644 --- a/tests/succeed/tuple/check-term.snap +++ b/tests/succeed/tuple/check-term.snap @@ -1,10 +1,10 @@ stdout = ''' -let Triple : Type = (U16, U16, U16); -let Point : Type = { x : U16, y : U16, z : U16 }; -let Any : Type = { A : Type, a : A }; -let triple : Triple = (0, 1, 2); -let point : Point = { x = 0, y = 1, z = 2 }; -let any : Any = { A = Bool, a = false }; +let Triple = (U16, U16, U16); +let Point = { x : U16, y : U16, z : U16 }; +let Any = { A : Type, a : A }; +let triple = (0, 1, 2); +let point = { x = 0, y = 1, z = 2 }; +let any = { A = Bool, a = false }; () : () ''' stderr = '' diff --git a/tests/succeed/tuple/check-universe.snap b/tests/succeed/tuple/check-universe.snap index 77a87be47..cf047505f 100644 --- a/tests/succeed/tuple/check-universe.snap +++ b/tests/succeed/tuple/check-universe.snap @@ -1,9 +1,9 @@ stdout = ''' -let Unit : Type = (); -let Paren : Type = Bool; -let Single : Type = (Bool,); -let Pair : Type = (Bool, U8); -let Triple : Type = (Bool, U8, U16); +let Unit = (); +let Paren = Bool; +let Single = (Bool,); +let Pair = (Bool, U8); +let Triple = (Bool, U8, U16); Unit : Type ''' stderr = '' diff --git a/tests/succeed/tuple/generic-pair.snap b/tests/succeed/tuple/generic-pair.snap index d08f0bdce..b44bd14f5 100644 --- a/tests/succeed/tuple/generic-pair.snap +++ b/tests/succeed/tuple/generic-pair.snap @@ -1,6 +1,6 @@ stdout = ''' -let fst : fun (A : Type) (B : Type) -> (A, B) -> A = fun A B p => p._0; -let snd : fun (A : Type) (B : Type) -> (A, B) -> B = fun A B p => p._1; +let fst = fun (A : Type) (B : Type) (p : (A, B)) => p._0; +let snd = fun (A : Type) (B : Type) (p : (A, B)) => p._1; () : () ''' stderr = '' diff --git a/tests/succeed/tuple/generic-triple.snap b/tests/succeed/tuple/generic-triple.snap index d8db3c0dc..8be156d2b 100644 --- a/tests/succeed/tuple/generic-triple.snap +++ b/tests/succeed/tuple/generic-triple.snap @@ -1,10 +1,7 @@ stdout = ''' -let get1 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> A = -fun A B C p => p._0; -let get2 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> B = -fun A B C p => p._1; -let get3 : fun (A : Type) (B : Type) (C : Type) -> (A, B, C) -> C = -fun A B C p => p._2; +let get1 = fun (A : Type) (B : Type) (C : Type) (p : (A, B, C)) => p._0; +let get2 = fun (A : Type) (B : Type) (C : Type) (p : (A, B, C)) => p._1; +let get3 = fun (A : Type) (B : Type) (C : Type) (p : (A, B, C)) => p._2; () : () ''' stderr = '' diff --git a/tests/succeed/tuple/synth.snap b/tests/succeed/tuple/synth.snap index 8b7178b67..1d9eafc2b 100644 --- a/tests/succeed/tuple/synth.snap +++ b/tests/succeed/tuple/synth.snap @@ -1,9 +1,9 @@ stdout = ''' -let unit : () = (); -let paren : Bool = false; -let single : (Bool,) = (false,); -let pair : (Bool, Bool) = (false, true); -let triple : (Bool, Bool, Bool) = (false, true, false); +let unit = (); +let paren = false; +let single = (false,); +let pair = (false, true); +let triple = (false, true, false); () : () ''' stderr = ''