Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102/// Constructs that carry `Term.ctx` source-position wrappers in the places/// placement rule R3 leaves exposed, so the transparency oracle/// (`tools/debug_transparency_oracle.sh`) has something to check them on.////// Every term carries its position on every path (`parse_all_decls`,/// `lang/module.mo`). A wrapper must change what the compiler ANNOTATES and/// never what it DECIDES, and R3 keeps wrappers out of an application's HEAD/// but puts one on every ARGUMENT -- so argument-reading shape probes are/// the exposed surface. Not one file in `examples/` used `++` before this/// one, so that surface had no oracle coverage at all.////// **What this file proves, and what it does not.** It proves the oracle's/// actual property: for these shapes, a `--debug` build differs from a/// `--release` one only by `!dbg` annotations. It does NOT catch the/// carrier-inference gaps that motivated writing it -- verified, not/// assumed: with the `term_peel` removed from `infer_carrier_type` or from/// `term_matches_carrier` (`lang/scope.mo`), this file still compiles/// clean.////// The reason is worth knowing before writing another test like this. The/// type checker's own class-method resolution (`resolve_class_method`,/// `lang/typecheck/infer.mo`) is ctx-transparent for these shapes, and it/// runs first. The syntactic carrier-inference pass in `lang/scope.mo` is/// only load-bearing for a def whose ELABORATION failed, which/// `elaborate_module_decls_best_effort` swallows silently and which in/// practice needs the scale of the self-compile to happen at all. So:////// - the corpus is the gate for `named_call_fields_of` and/// `con_owner_name` (`slow_tests/codegen_named_call_*_tests.mo` and/// `typecheck_init_tests.mo` each caught one);/// - **the self-compile, in BOTH modes, is the only gate for the/// carrier-inference gaps.** `monad compile cli/src/main.mo` without/// `--release` is what found `Append.append`, and the `--release` one/// found `FromListLiteral.empty`.////// Each def below is still a shape a non-peeling probe reads:////// `concat_computed` a `++` whose LEFT operand is a CALL, not a literal/// -- the shape `infer_carrier_type`'s `Term.app` arm/// exists for./// `concat_local` `++` on a local whose carrier comes from its/// declared type, via `lookup_local_type`./// `list_and_lookup` a list literal desugars to `FromListLiteral.cons`//// `.empty`, which have no argument to infer from, so/// the CLASS DEFAULT carrier is the only source -- and/// a class param's default is lowered as a value, so/// it is itself wrapped./// `sum_of_call` a `match` whose scrutinee is a bare call, which is/// what `scrutinee_type_args` reads to enrich an arm's/// type environment.////// Keep it compiling in BOTH modes: the oracle SKIPs a file that fails/// either way, and a skipped case proves nothing.#![mote { name := "located_terms", deps := [init, std] }]open IO {println}use std::list {List.sum}/// `++` with a computed left operand.def concat_computed (x : I64) (suffix : String) : String := I64.to_string x ++ suffix/// `++` where the carrier comes from a local's declared type.def concat_local (a : String) : String := let b : String := "-" ++ a in b ++ "!"/// A list literal (class-default carrier) plus a fold over it.def list_and_lookup : I64 := let xs : List I64 := [1, 2, 3] in List.sum xs/// A `match` whose scrutinee is a bare call. `List.last` returns an/// `Option I64`, so the arm env has a concrete type arg to lose.def sum_of_call (xs : List I64) : I64 := match List.last xs { Option.some v => v + List.sum xs, Option.none => 0, }#[test]def test_concat_computed : Bool := String.beq (concat_computed 42 "x") "42x"#[test]def test_concat_local : Bool := String.beq (concat_local "a") "-a!"#[test]def test_list_and_lookup : Bool := list_and_lookup == 6#[test]def test_sum_of_call : Bool := sum_of_call ([4, 5] : List I64) == 14def main (args : List String) : IO Unit := do { println (concat_computed (list_and_lookup) " = sum"); println (concat_local "located"); println (I64.to_string (sum_of_call ([4, 5] : List I64)))}