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.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139use lang::types { Attribute, Decl, Def, Identifier, InductConstructor, Inductive, LocalScope, LocalVar, ModulePath, NamePath, NameRef, Param, Scope, ScopeData, ScopeDef, ScopeError, TypeConstraint, hole, package_private, sort_n,}use lib::scope { build_scope_from_decls, resolve_def_in_scope_by_name, scope_find_inductive, scope_resolve_name,}// --- Helpers ---def empty_local_scope : LocalScope := let empty_vars : List LocalVar := List.empty in let empty_parent : Option LocalScope := Option.none in { vars := empty_vars, parent := empty_parent }def test_module_path : ModulePath := let test_id : Identifier := Identifier.id "Test" in let empty_id_list : List Identifier := List.cons test_id List.empty in ModulePath.mp empty_id_listdef make_scope (sd : ScopeData) : Scope := let path : ModulePath := test_module_path in let empty_parent : Option Scope := Option.none in { module_id := path, scope := sd, parent := empty_parent, incomplete_match_ok := false }/// A one-segment DECL name -- the shape `Def.name`, `Inductive.name`,/// `InductConstructor.name` and the name arguments of/// `scope_find_inductive`/`resolve_def_in_scope_by_name` all take.def name_to_npath (i : Identifier) : NamePath := let empty_id_list : List Identifier := List.empty in NamePath.npath (List.cons i empty_id_list)// Typed empty lists to avoid forall inference issuesdef empty_decls_list : List Decl := List.emptydef empty_constraints : List TypeConstraint := List.emptydef empty_attrs : List Attribute := List.emptydef empty_params : List Param := List.emptydef empty_constructors : List InductConstructor := List.empty// --- Test: Empty module has builtins ---#[test]def test_parse_empty_has_builtins : Bool := let path : ModulePath := test_module_path in let sd : ScopeData := build_scope_from_decls path empty_decls_list in let scope : Scope := make_scope sd in let type_ref : NameRef := NameRef.nid (Identifier.id "Type") in let locals : LocalScope := empty_local_scope in match scope_resolve_name type_ref scope locals { ok _ => true, err _ => false }// --- Test: Build scope with a manually constructed def ---#[test]def test_scope_def_resolves : Bool := let path : ModulePath := test_module_path in let defname : NamePath := name_to_npath (Identifier.id "add") in let def_decl : Def := Def.mk defname (sort_n 1) Term.hole empty_constraints empty_attrs Visibility.package_private List.empty in let decl_list : List Decl := List.cons (Decl.def_d def_decl) empty_decls_list in let sd : ScopeData := build_scope_from_decls path decl_list in let scope : Scope := make_scope sd in let add_ref : NameRef := NameRef.nid (Identifier.id "add") in let locals : LocalScope := empty_local_scope in match scope_resolve_name add_ref scope locals { ok _ => true, err _ => false }// --- Test: Build scope with a manually constructed inductive ---#[test]def test_scope_inductive_found : Bool := let path : ModulePath := test_module_path in let color_path : NamePath := name_to_npath (Identifier.id "Color") in let red_con_name : NamePath := name_to_npath (Identifier.id "red") in let red_con : InductConstructor := InductConstructor.mk red_con_name empty_params Term.hole in let constructors : List InductConstructor := List.cons red_con empty_constructors in let ind : Inductive := Inductive.mk color_path empty_params (sort_n 1) constructors empty_attrs Visibility.package_private in let decl_list : List Decl := List.cons (Decl.inductive_d ind) empty_decls_list in let sd : ScopeData := build_scope_from_decls path decl_list in let scope : Scope := make_scope sd in match scope_find_inductive color_path scope { ok _ => true, err _ => false }// --- Test: Constructor resolves as def ---#[test]def test_scope_constructor_resolves : Bool := let path : ModulePath := test_module_path in let color_path : NamePath := name_to_npath (Identifier.id "Color") in let red_con_name : NamePath := name_to_npath (Identifier.id "red") in let red_con : InductConstructor := InductConstructor.mk red_con_name empty_params Term.hole in let constructors : List InductConstructor := List.cons red_con empty_constructors in let ind : Inductive := Inductive.mk color_path empty_params (sort_n 1) constructors empty_attrs Visibility.package_private in let decl_list : List Decl := List.cons (Decl.inductive_d ind) empty_decls_list in let sd : ScopeData := build_scope_from_decls path decl_list in let scope : Scope := make_scope sd in let red_ref : NameRef := NameRef.nid (Identifier.id "red") in let locals : LocalScope := empty_local_scope in match scope_resolve_name red_ref scope locals { ok _ => true, err _ => false }// --- Test: Unknown name does not resolve ---#[test]def test_scope_unknown_name_fails : Bool := let path : ModulePath := test_module_path in let sd : ScopeData := build_scope_from_decls path empty_decls_list in let scope : Scope := make_scope sd in let y_ref : NameRef := NameRef.nid (Identifier.id "y") in let locals : LocalScope := empty_local_scope in match scope_resolve_name y_ref scope locals { ok _ => false, err _ => true }// --- Test: Builtins present (Type resolution) ---#[test]def test_builtin_type_resolves : Bool := let path : ModulePath := test_module_path in let sd : ScopeData := build_scope_from_decls path empty_decls_list in let scope : Scope := make_scope sd in let type_name : NamePath := name_to_npath (Identifier.id "Type") in let result : Result ScopeError ScopeDef := resolve_def_in_scope_by_name type_name scope in match result { ok _ => true, err _ => false }