diff --git a/crates/kind-checker/src/compiler/mod.rs b/crates/kind-checker/src/compiler/mod.rs index 6c271c55..b5b68aa7 100644 --- a/crates/kind-checker/src/compiler/mod.rs +++ b/crates/kind-checker/src/compiler/mod.rs @@ -44,7 +44,7 @@ fn lift_spine(spine: Vec>) -> Vec> { if spine.len() > 16 { let mut start = spine[..2].to_vec(); start.push(Box::new(Term::Ctr { - name: format!("Kind.Term.args{}", spine.len() - 2), + name: format!("Apps.Kind.Term.args{}", spine.len() - 2), args: spine[2..].to_vec(), })); start @@ -101,7 +101,7 @@ fn range_to_num(lhs: bool, range: Range) -> Box { fn set_origin(ident: &Ident) -> Box { mk_lifted_ctr( - "Kind.Term.set_origin".to_owned(), + "Apps.Kind.Term.set_origin".to_owned(), vec![range_to_num(false, ident.range), mk_var(ident.to_str())], ) } @@ -114,8 +114,8 @@ fn lam(name: &Ident, body: Box) -> Box { } fn desugar_str(input: &str, range: Range) -> Box { - let nil = QualifiedIdent::new_static("String.nil", None, range); - let cons = QualifiedIdent::new_static("String.cons", None, range); + let nil = QualifiedIdent::new_static("Data.String.nil", None, range); + let cons = QualifiedIdent::new_static("Data.String.cons", None, range); input .chars() .rfold(desugared::Expr::ctr(range, nil, vec![]), |right, chr| { @@ -132,12 +132,12 @@ fn desugar_str(input: &str, range: Range) -> Box { fn codegen_str(input: &str) -> Box { input.chars().rfold( Box::new(Term::Ctr { - name: "String.nil".to_string(), + name: "Data.String.nil".to_string(), args: vec![], }), |right, chr| { Box::new(Term::Ctr { - name: "String.cons".to_string(), + name: "Data.String.cons".to_string(), args: vec![mk_u60(chr as u64), right], }) }, @@ -339,8 +339,8 @@ fn codegen_vec(exprs: T) -> Box where T: DoubleEndedIterator>, { - exprs.rfold(mk_ctr("List.nil".to_string(), vec![]), |left, right| { - mk_ctr("List.cons".to_string(), vec![right, left]) + exprs.rfold(mk_ctr("Data.List.nil".to_string(), vec![]), |left, right| { + mk_ctr("Data.List.cons".to_string(), vec![right, left]) }) } @@ -406,7 +406,7 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { rhs: codegen_expr(true, &rule.body), }); - if rule.name.to_string().as_str() == "HVM.log" { + if rule.name.to_string().as_str() == "Apps.HVM.log" { file.rules.push(lang::Rule { lhs: mk_ctr( TermTag::HoasF(rule.name.to_string()).to_string(), @@ -419,9 +419,9 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { ], ), rhs: mk_ctr( - "HVM.print".to_owned(), + "Apps.HVM.print".to_owned(), vec![ - mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), + mk_ctr("Apps.Kind.Term.show".to_owned(), vec![mk_var("log")]), mk_var("ret"), ], ), @@ -449,7 +449,7 @@ fn codegen_entry_rules( ) -> Box { if pats.is_empty() { mk_ctr( - "Kind.Rule.rhs".to_owned(), + "Apps.Kind.Rule.rhs".to_owned(), vec![mk_ctr( format!("QT{}", index), vec_preppend![ @@ -464,7 +464,7 @@ fn codegen_entry_rules( let expr = codegen_all_expr(true, false, count, false, pat); args.push(expr.clone()); mk_ctr( - "Kind.Rule.lhs".to_owned(), + "Apps.Kind.Rule.lhs".to_owned(), vec![ expr, codegen_entry_rules(count, index + 1, args, entry, &pats[1..]), @@ -476,7 +476,7 @@ fn codegen_entry_rules( fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.NameOf".to_owned(), + "Apps.Kind.Axiom.NameOf".to_owned(), vec![mk_ctr_name(&entry.name)], ), rhs: codegen_str(entry.name.to_string().as_str()), @@ -484,7 +484,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.OrigOf".to_owned(), + "Apps.Kind.Axiom.OrigOf".to_owned(), vec![mk_ctr_name(&entry.name)], ), rhs: range_to_num(false, entry.name.range), @@ -492,7 +492,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.HashOf".to_owned(), + "Apps.Kind.Axiom.HashOf".to_owned(), vec![mk_ctr_name(&entry.name)], ), rhs: mk_u60(fxhash::hash64(entry.name.to_string().as_str())), @@ -500,7 +500,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.TypeOf".to_owned(), + "Apps.Kind.Axiom.TypeOf".to_owned(), vec![mk_ctr_name(&entry.name)], ), rhs: codegen_type(&entry.args, &entry.typ), @@ -512,7 +512,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_lifted_ctr( - format!("Kind.Term.FN{}", entry.args.len()), + format!("Apps.Kind.Term.FN{}", entry.args.len()), vec_preppend![ mk_ctr_name(&entry.name), mk_var("orig"); @@ -561,7 +561,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.RuleOf".to_owned(), + "Apps.Kind.Axiom.RuleOf".to_owned(), vec![mk_ctr_name(&entry.name)], ), rhs: codegen_vec(rules), @@ -573,10 +573,10 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { if !entry.rules.is_empty() && !entry.rules[0].pats.is_empty() && !entry.attrs.partial && !entry.attrs.axiom { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.CoverCheck".to_owned(), + "Apps.Kind.Axiom.CoverCheck".to_owned(), vec![mk_ctr_name(&entry.name)], ), - rhs: mk_single_ctr("Bool.true".to_string()), + rhs: mk_single_ctr("Data.Bool.true".to_string()), }); } } @@ -584,15 +584,15 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { for family in book.families.values() { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.Family.Constructors".to_owned(), + "Apps.Kind.Axiom.Family.Constructors".to_owned(), vec![mk_ctr_name(&family.name)], ), - rhs: mk_ctr("Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]), + rhs: mk_ctr("Data.Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]), }); file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.Family.Params".to_owned(), + "Apps.Kind.Axiom.Family.Params".to_owned(), vec![mk_ctr_name(&family.name)], ), rhs: mk_u60(family.parameters.len() as u64), @@ -613,7 +613,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { let entry = book.entrs.get(constructor.to_str()).unwrap(); let mut maker = mk_ctr( - "Kind.Coverage.Maker.End".to_string(), + "Apps.Kind.Coverage.Maker.End".to_string(), vec![codegen_expr( false, &kind_tree::desugared::Expr::ctr( @@ -630,7 +630,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { for arg in entry.args[family.parameters.len()..].iter().rev() { maker = mk_ctr( - "Kind.Coverage.Maker.Cons".to_string(), + "Apps.Kind.Coverage.Maker.Cons".to_string(), vec![ range_to_num(false, arg.range), codegen_all_expr(false, false, &mut 0, false, &arg.typ), @@ -641,7 +641,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Coverage.Maker.Mk".to_owned(), + "Apps.Kind.Coverage.Maker.Mk".to_owned(), vec![ mk_ctr_name(constructor), mk_var("orig"), @@ -655,20 +655,20 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { ), ], ), - rhs: mk_ctr("Maybe.some".to_string(), vec![maker]), + rhs: mk_ctr("Data.Maybe.some".to_string(), vec![maker]), }); file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.Compare".to_owned(), + "Apps.Kind.Axiom.Compare".to_owned(), vec![mk_ctr_name(constructor), mk_ctr_name(constructor)], ), - rhs: mk_single_ctr("Bool.true".to_string()), + rhs: mk_single_ctr("Data.Bool.true".to_string()), }); file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.ArgsCount".to_owned(), + "Apps.Kind.Axiom.ArgsCount".to_owned(), vec![mk_ctr_name(constructor)], ), rhs: mk_u60(entry.args.len() as u64), @@ -676,10 +676,10 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) { file.rules.push(lang::Rule { lhs: mk_ctr( - "Kind.Axiom.Compare".to_owned(), + "Apps.Kind.Axiom.Compare".to_owned(), vec![mk_ctr_name(constructor), mk_ctr_name(constructor)], ), - rhs: mk_single_ctr("Bool.true".to_string()), + rhs: mk_single_ctr("Data.Bool.true".to_string()), }); } } @@ -694,7 +694,7 @@ pub fn codegen_book(book: &Book, check_coverage: bool, functions_to_check: Vec) -> fmt::Result { match self { - TermTag::Var => write!(f, "Kind.Term.var"), - TermTag::All => write!(f, "Kind.Term.all"), - TermTag::Lambda => write!(f, "Kind.Term.lam"), - TermTag::App => write!(f, "Kind.Term.app"), - TermTag::Fun(n) => write!(f, "Kind.Term.fn{}", n), - TermTag::Ctr(n) => write!(f, "Kind.Term.ct{}", n), - TermTag::Let => write!(f, "Kind.Term.let"), - TermTag::Ann => write!(f, "Kind.Term.ann"), - TermTag::Sub => write!(f, "Kind.Term.sub"), - TermTag::Typ => write!(f, "Kind.Term.typ"), - TermTag::U60 => write!(f, "Kind.Term.U60"), - TermTag::NUMU60 => write!(f, "Kind.Term.u60"), - TermTag::Binary => write!(f, "Kind.Term.op2"), - TermTag::Hole => write!(f, "Kind.Term.hol"), - TermTag::Hlp => write!(f, "Kind.Term.hlp"), + TermTag::Var => write!(f, "Apps.Kind.Term.var"), + TermTag::All => write!(f, "Apps.Kind.Term.all"), + TermTag::Lambda => write!(f, "Apps.Kind.Term.lam"), + TermTag::App => write!(f, "Apps.Kind.Term.app"), + TermTag::Fun(n) => write!(f, "Apps.Kind.Term.fn{}", n), + TermTag::Ctr(n) => write!(f, "Apps.Kind.Term.ct{}", n), + TermTag::Let => write!(f, "Apps.Kind.Term.let"), + TermTag::Ann => write!(f, "Apps.Kind.Term.ann"), + TermTag::Sub => write!(f, "Apps.Kind.Term.sub"), + TermTag::Typ => write!(f, "Apps.Kind.Term.typ"), + TermTag::U60 => write!(f, "Apps.Kind.Term.U60"), + TermTag::NUMU60 => write!(f, "Apps.Kind.Term.u60"), + TermTag::Binary => write!(f, "Apps.Kind.Term.op2"), + TermTag::Hole => write!(f, "Apps.Kind.Term.hol"), + TermTag::Hlp => write!(f, "Apps.Kind.Term.hlp"), TermTag::HoasF(name) => write!(f, "F${}", name), TermTag::HoasQ(name) => write!(f, "Q${}", name), } @@ -70,11 +70,11 @@ impl fmt::Display for TermTag { impl fmt::Display for EvalTag { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { match self { - EvalTag::Op => write!(f, "Kind.Term.eval_op"), - EvalTag::App => write!(f, "Kind.Term.eval_app"), - EvalTag::Let => write!(f, "Kind.Term.eval_let"), - EvalTag::Ann => write!(f, "Kind.Term.eval_ann"), - EvalTag::Sub => write!(f, "Kind.Term.eval_sub"), + EvalTag::Op => write!(f, "Apps.Kind.Term.eval_op"), + EvalTag::App => write!(f, "Apps.Kind.Term.eval_app"), + EvalTag::Let => write!(f, "Apps.Kind.Term.eval_let"), + EvalTag::Ann => write!(f, "Apps.Kind.Term.eval_ann"), + EvalTag::Sub => write!(f, "Apps.Kind.Term.eval_sub"), } } } @@ -83,21 +83,21 @@ impl fmt::Display for EvalTag { /// by the checker. pub fn operator_to_constructor<'a>(operator: Operator) -> &'a str { match operator { - Operator::Add => "Kind.Operator.add", - Operator::Sub => "Kind.Operator.sub", - Operator::Mul => "Kind.Operator.mul", - Operator::Div => "Kind.Operator.div", - Operator::Mod => "Kind.Operator.mod", - Operator::And => "Kind.Operator.and", - Operator::Xor => "Kind.Operator.xor", - Operator::Shl => "Kind.Operator.shl", - Operator::Shr => "Kind.Operator.shr", - Operator::Ltn => "Kind.Operator.ltn", - Operator::Lte => "Kind.Operator.lte", - Operator::Eql => "Kind.Operator.eql", - Operator::Gte => "Kind.Operator.gte", - Operator::Gtn => "Kind.Operator.gtn", - Operator::Neq => "Kind.Operator.neq", - Operator::Or => "Kind.Operator.or", + Operator::Add => "Apps.Kind.Operator.add", + Operator::Sub => "Apps.Kind.Operator.sub", + Operator::Mul => "Apps.Kind.Operator.mul", + Operator::Div => "Apps.Kind.Operator.div", + Operator::Mod => "Apps.Kind.Operator.mod", + Operator::And => "Apps.Kind.Operator.and", + Operator::Xor => "Apps.Kind.Operator.xor", + Operator::Shl => "Apps.Kind.Operator.shl", + Operator::Shr => "Apps.Kind.Operator.shr", + Operator::Ltn => "Apps.Kind.Operator.ltn", + Operator::Lte => "Apps.Kind.Operator.lte", + Operator::Eql => "Apps.Kind.Operator.eql", + Operator::Gte => "Apps.Kind.Operator.gte", + Operator::Gtn => "Apps.Kind.Operator.gtn", + Operator::Neq => "Apps.Kind.Operator.neq", + Operator::Or => "Apps.Kind.Operator.or", } } diff --git a/crates/kind-checker/src/lib.rs b/crates/kind-checker/src/lib.rs index 307b8127..eadfb587 100644 --- a/crates/kind-checker/src/lib.rs +++ b/crates/kind-checker/src/lib.rs @@ -110,7 +110,7 @@ pub fn eval_api(book: &Book) -> (String, u64) { runtime::link( &heap, 0, - runtime::Fun(*book.name_to_id.get("Kind.API.eval_main").unwrap(), 0), + runtime::Fun(*book.name_to_id.get("Apps.Kind.API.eval_main").unwrap(), 0), ); let host = 0; diff --git a/crates/kind-checker/src/report.rs b/crates/kind-checker/src/report.rs index 3fc892d1..a3dc7532 100644 --- a/crates/kind-checker/src/report.rs +++ b/crates/kind-checker/src/report.rs @@ -35,22 +35,22 @@ fn parse_num(term: &Term) -> Result { fn parse_op(term: &Term) -> Result { match term { Term::Ctr { name, args: _ } => match name.as_str() { - "Kind.Operator.add" => Ok(Operator::Add), - "Kind.Operator.sub" => Ok(Operator::Sub), - "Kind.Operator.mul" => Ok(Operator::Mul), - "Kind.Operator.div" => Ok(Operator::Div), - "Kind.Operator.mod" => Ok(Operator::Mod), - "Kind.Operator.and" => Ok(Operator::And), - "Kind.Operator.or" => Ok(Operator::Or), - "Kind.Operator.xor" => Ok(Operator::Xor), - "Kind.Operator.shl" => Ok(Operator::Shl), - "Kind.Operator.shr" => Ok(Operator::Shr), - "Kind.Operator.ltn" => Ok(Operator::Ltn), - "Kind.Operator.lte" => Ok(Operator::Lte), - "Kind.Operator.eql" => Ok(Operator::Eql), - "Kind.Operator.gte" => Ok(Operator::Gte), - "Kind.Operator.gtn" => Ok(Operator::Gtn), - "Kind.Operator.neq" => Ok(Operator::Neq), + "Apps.Kind.Operator.add" => Ok(Operator::Add), + "Apps.Kind.Operator.sub" => Ok(Operator::Sub), + "Apps.Kind.Operator.mul" => Ok(Operator::Mul), + "Apps.Kind.Operator.div" => Ok(Operator::Div), + "Apps.Kind.Operator.mod" => Ok(Operator::Mod), + "Apps.Kind.Operator.and" => Ok(Operator::And), + "Apps.Kind.Operator.or" => Ok(Operator::Or), + "Apps.Kind.Operator.xor" => Ok(Operator::Xor), + "Apps.Kind.Operator.shl" => Ok(Operator::Shl), + "Apps.Kind.Operator.shr" => Ok(Operator::Shr), + "Apps.Kind.Operator.ltn" => Ok(Operator::Ltn), + "Apps.Kind.Operator.lte" => Ok(Operator::Lte), + "Apps.Kind.Operator.eql" => Ok(Operator::Eql), + "Apps.Kind.Operator.gte" => Ok(Operator::Gte), + "Apps.Kind.Operator.gtn" => Ok(Operator::Gtn), + "Apps.Kind.Operator.neq" => Ok(Operator::Neq), _ => Err("Cannot recognized operator".to_string()), }, _ => Err("Error parsing operator".to_string()), @@ -91,44 +91,44 @@ fn parse_all_expr( ) -> Result, String> { match term { Term::Ctr { name, args } => match name.as_str() { - "Kind.Term.Quoted.all" => Ok(Expr::all( + "Apps.Kind.Term.Quoted.all" => Ok(Expr::all( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), parse_all_expr(names.clone(), &args[2])?, parse_all_expr(names, &args[3])?, false, // TODO: Fix )), - "Kind.Term.Quoted.lam" => Ok(Expr::lambda( + "Apps.Kind.Term.Quoted.lam" => Ok(Expr::lambda( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), parse_all_expr(names, &args[2])?, false, // TODO: Fix )), - "Kind.Term.Quoted.let" => Ok(Expr::let_( + "Apps.Kind.Term.Quoted.let" => Ok(Expr::let_( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), parse_all_expr(names.clone(), &args[2])?, parse_all_expr(names, &args[3])?, )), - "Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)), - "Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new( + "Apps.Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)), + "Apps.Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new( parse_name(&args[1])?, parse_orig(&args[0])?, ))), - "Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)), - "Kind.Term.Quoted.ann" => Ok(Expr::ann( + "Apps.Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)), + "Apps.Kind.Term.Quoted.ann" => Ok(Expr::ann( parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, parse_all_expr(names, &args[2])?, )), - "Kind.Term.Quoted.sub" => Ok(Expr::sub( + "Apps.Kind.Term.Quoted.sub" => Ok(Expr::sub( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), parse_num(&args[2])? as usize, parse_num(&args[3])? as usize, parse_all_expr(names, &args[4])?, )), - "Kind.Term.Quoted.app" => Ok(Expr::app( + "Apps.Kind.Term.Quoted.app" => Ok(Expr::app( parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, vec![desugared::AppBinding { @@ -136,7 +136,7 @@ fn parse_all_expr( erased: false, }], )), - "Kind.Term.Quoted.ctr" => { + "Apps.Kind.Term.Quoted.ctr" => { let name = parse_qualified(&args[0])?; let orig = parse_orig(&args[1])?; let mut res = Vec::new(); @@ -145,7 +145,7 @@ fn parse_all_expr( } Ok(Expr::ctr(orig, name, res)) } - "Kind.Term.Quoted.fun" => Ok(Expr::fun( + "Apps.Kind.Term.Quoted.fun" => Ok(Expr::fun( parse_orig(&args[1])?, parse_qualified(&args[0])?, { @@ -156,11 +156,11 @@ fn parse_all_expr( res }, )), - "Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))), - "Kind.Term.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)), - "Kind.Term.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)), + "Apps.Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))), + "Apps.Kind.Term.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)), + "Apps.Kind.Term.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: Change quoting to support floats - "Kind.Term.Quoted.op2" => Ok(Expr::binary( + "Apps.Kind.Term.Quoted.op2" => Ok(Expr::binary( parse_orig(&args[0])?, parse_op(&args[1])?, parse_all_expr(names.clone(), &args[2])?, @@ -181,9 +181,9 @@ fn parse_list(term: &Term) -> Result>, String> { loop { match cur { Term::Ctr { name, args } => { - if name == "List.nil" { + if name == "Data.List.nil" { break; - } else if name == "List.cons" { + } else if name == "Data.List.cons" { vec.push(args[0].clone()); cur = &args[1]; } else { @@ -199,10 +199,10 @@ fn parse_list(term: &Term) -> Result>, String> { /// Transforms a HVM quoted entry into a easy to manipulate structure. pub fn transform_entry(term: &Term) -> Result { match term { - Term::Ctr { name, args } if name == "Pair.new" => { + Term::Ctr { name, args } if name == "Data.Pair.new" => { let fst = parse_name(&args[0])?; match &*args[1] { - Term::Ctr { name, args } if name == "Pair.new" => { + Term::Ctr { name, args } if name == "Data.Pair.new" => { let snd = parse_expr(&args[0])?; let trd = parse_list(&args[1])?; let trd = trd.iter().flat_map(|x| parse_expr(x)).collect(); @@ -226,7 +226,7 @@ fn parse_type_error(expr: &Term) -> Result { let ctx = Context(entries.collect()); let orig = match_opt!(*args[1], Term::U6O { numb } => EncodedRange(numb).to_range())?; match name.as_str() { - "Kind.Error.Quoted.uncovered_pattern" => Ok(TypeDiagnostic::UncoveredPattern(ctx, orig, { + "Apps.Kind.Error.Quoted.uncovered_pattern" => Ok(TypeDiagnostic::UncoveredPattern(ctx, orig, { let args = parse_list(&args[2])?; let mut new_args = Vec::with_capacity(args.len()); for arg in &args { @@ -234,25 +234,25 @@ fn parse_type_error(expr: &Term) -> Result { } new_args })), - "Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)), - "Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)), - "Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)), - "Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)), - "Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase( + "Apps.Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)), + "Apps.Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)), + "Apps.Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)), + "Apps.Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)), + "Apps.Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase( ctx, orig, parse_all_expr(im_rc::HashMap::new(), &args[2])?, parse_all_expr(im_rc::HashMap::new(), &args[3])?, )), - "Kind.Error.Quoted.inspection" => Ok(TypeDiagnostic::Inspection( + "Apps.Kind.Error.Quoted.inspection" => Ok(TypeDiagnostic::Inspection( ctx, orig, parse_all_expr(im_rc::HashMap::new(), &args[2])?, )), - "Kind.Error.Quoted.too_many_arguments" => { + "Apps.Kind.Error.Quoted.too_many_arguments" => { Ok(TypeDiagnostic::TooManyArguments(ctx, orig)) } - "Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch( + "Apps.Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch( ctx, orig, parse_all_expr(im_rc::HashMap::new(), &args[2])?, diff --git a/crates/kind-derive/src/subst.rs b/crates/kind-derive/src/subst.rs index 654ed608..869ad5ff 100644 --- a/crates/kind-derive/src/subst.rs +++ b/crates/kind-derive/src/subst.rs @@ -214,7 +214,7 @@ impl<'a> Visitor for Subst<'a> { snd, } => { self.visit_qualified_ident(&mut QualifiedIdent::new_static( - "Sigma", None, expr.range, + "Data.Sigma", None, expr.range, )); self.visit_expr(fst); self.visit_expr(snd); @@ -225,7 +225,7 @@ impl<'a> Visitor for Subst<'a> { snd, } => { self.visit_qualified_ident(&mut QualifiedIdent::new_static( - "Sigma", None, expr.range, + "Data.Sigma", None, expr.range, )); self.visit_expr(fst); self.context_vars.push((ident.range, ident.to_string())); @@ -257,7 +257,7 @@ impl<'a> Visitor for Subst<'a> { } ExprKind::If { cond, then_, else_ } => { self.visit_qualified_ident(&mut QualifiedIdent::new_sugared( - "Bool", "if", expr.range, + "Data.Bool", "if", expr.range, )); self.visit_expr(cond); self.visit_expr(then_); @@ -265,17 +265,17 @@ impl<'a> Visitor for Subst<'a> { } ExprKind::Pair { fst, snd } => { self.visit_qualified_ident(&mut QualifiedIdent::new_sugared( - "Pair", "new", expr.range, + "Data.Pair", "new", expr.range, )); self.visit_expr(fst); self.visit_expr(snd); } ExprKind::List { args } => { self.visit_qualified_ident(&mut QualifiedIdent::new_sugared( - "List", "nil", expr.range, + "Data.List", "nil", expr.range, )); self.visit_qualified_ident(&mut QualifiedIdent::new_sugared( - "List", "cons", expr.range, + "Data.List", "cons", expr.range, )); visit_vec!(args.iter_mut(), arg => self.visit_expr(arg)); } diff --git a/crates/kind-parser/src/expr.rs b/crates/kind-parser/src/expr.rs index abdb8d03..b2446c0c 100644 --- a/crates/kind-parser/src/expr.rs +++ b/crates/kind-parser/src/expr.rs @@ -241,10 +241,10 @@ impl<'a> Parser<'a> { let id = self.parse_upper_id()?; let data = match id.to_string().as_str() { "Type" => ExprKind::Lit { lit: Literal::Type }, - "U60" => ExprKind::Lit { + "Data.U60" => ExprKind::Lit { lit: Literal::NumTypeU60, }, - "F60" => ExprKind::Lit { + "Data.F60" => ExprKind::Lit { lit: Literal::NumTypeF60, }, _ => ExprKind::Constr { @@ -263,10 +263,10 @@ impl<'a> Parser<'a> { let mut range = id.range; let data = match id.to_string().as_str() { "Type" => ExprKind::Lit { lit: Literal::Type }, - "U60" => ExprKind::Lit { + "Data.U60" => ExprKind::Lit { lit: Literal::NumTypeU60, }, - "F60" => ExprKind::Lit { + "Data.F60" => ExprKind::Lit { lit: Literal::NumTypeF60, }, _ => { diff --git a/crates/kind-pass/src/desugar/expr.rs b/crates/kind-pass/src/desugar/expr.rs index 9e4e95ff..b6a1bcde 100644 --- a/crates/kind-pass/src/desugar/expr.rs +++ b/crates/kind-pass/src/desugar/expr.rs @@ -24,8 +24,8 @@ impl<'a> DesugarState<'a> { ) -> Box { match literal { Literal::String(string) => { - if !self.check_implementation("String.cons", range, Sugar::String) - || !self.check_implementation("String.nil", range, Sugar::String) + if !self.check_implementation("Data.String.cons", range, Sugar::String) + || !self.check_implementation("Data.String.nil", range, Sugar::String) { return desugared::Expr::err(range); } @@ -37,7 +37,7 @@ impl<'a> DesugarState<'a> { Literal::NumTypeF60 => desugared::Expr::type_f60(range), Literal::NumU60(num) => desugared::Expr::num_u60(range, *num), Literal::Nat(num) => { - let list_ident = QualifiedIdent::new_static("Nat", None, range); + let list_ident = QualifiedIdent::new_static("Data.Nat", None, range); let cons_ident = list_ident.add_segment("succ"); let nil_ident = list_ident.add_segment("zero"); @@ -50,7 +50,7 @@ impl<'a> DesugarState<'a> { res } Literal::NumU120(num) => { - if !self.check_implementation("U120.new", range, Sugar::U120) { + if !self.check_implementation("Data.U120.new", range, Sugar::U120) { return desugared::Expr::err(range); } desugared::Expr::num_u120(range, *num) @@ -292,7 +292,7 @@ impl<'a> DesugarState<'a> { typ: &expr::Expr, body: &expr::Expr, ) -> Box { - let sigma = QualifiedIdent::new_static("Sigma", None, range); + let sigma = QualifiedIdent::new_static("Data.Sigma", None, range); if !self.check_implementation(sigma.to_str(), range, Sugar::Sigma) { return desugared::Expr::err(range); @@ -316,7 +316,7 @@ impl<'a> DesugarState<'a> { range: Range, expr: &[expr::Expr], ) -> Box { - let list_ident = QualifiedIdent::new_static("List", None, range); + let list_ident = QualifiedIdent::new_static("Data.List", None, range); let cons_ident = list_ident.add_segment("cons"); let nil_ident = list_ident.add_segment("nil"); @@ -345,7 +345,7 @@ impl<'a> DesugarState<'a> { if_: &expr::Expr, else_: &expr::Expr, ) -> Box { - let boolean = QualifiedIdent::new_static("Bool", None, range); + let boolean = QualifiedIdent::new_static("Data.Bool", None, range); let bool_if_ident = boolean.add_segment("if"); let bool_if = self.old_book.names.get(bool_if_ident.to_str()); @@ -419,7 +419,7 @@ impl<'a> DesugarState<'a> { fst: &expr::Expr, snd: &expr::Expr, ) -> Box { - let sigma_new = QualifiedIdent::new_sugared("Sigma", "new", range); + let sigma_new = QualifiedIdent::new_sugared("Data.Sigma", "new", range); if !self.check_implementation(sigma_new.to_str(), range, Sugar::Pair) { return desugared::Expr::err(range); diff --git a/crates/kind-pass/src/desugar/top_level.rs b/crates/kind-pass/src/desugar/top_level.rs index 1fbec32d..9406b4fa 100644 --- a/crates/kind-pass/src/desugar/top_level.rs +++ b/crates/kind-pass/src/desugar/top_level.rs @@ -223,7 +223,7 @@ impl<'a> DesugarState<'a> { fst: &concrete::pat::Pat, snd: &concrete::pat::Pat, ) -> Box { - let sigma_new = QualifiedIdent::new_static("Sigma", Some("new".to_string()), range); + let sigma_new = QualifiedIdent::new_static("Data.Sigma", Some("new".to_string()), range); let entry = self.old_book.entries.get(sigma_new.to_string().as_str()); if entry.is_none() { @@ -241,7 +241,7 @@ impl<'a> DesugarState<'a> { range: Range, expr: &[concrete::pat::Pat], ) -> Box { - let list_ident = QualifiedIdent::new_static("List", None, range); + let list_ident = QualifiedIdent::new_static("Data.List", None, range); let cons_ident = list_ident.add_segment("cons"); let nil_ident = list_ident.add_segment("nil"); diff --git a/crates/kind-pass/src/diagnostic.rs b/crates/kind-pass/src/diagnostic.rs index acfd6d80..fd089627 100644 --- a/crates/kind-pass/src/diagnostic.rs +++ b/crates/kind-pass/src/diagnostic.rs @@ -218,12 +218,12 @@ impl Diagnostic for PassDiagnostic { subtitles: vec![], hints: vec![match sugar { Sugar::DoNotation => "You must implement 'bind' and 'pure' for this type in order to use the do notation.".to_string(), - Sugar::List => "You must implement 'List', 'List.cons' and 'List.nil' for this type in order to use the list notation.".to_string(), - Sugar::Sigma => "You must implement 'Sigma' in order to use the sigma notation.".to_string(), - Sugar::Pair => "You must implement 'Sigma' and 'Sigma.new' in order to use the sigma notation.".to_string(), - Sugar::BoolIf => "You must implement 'Bool.if' in order to use the if notation.".to_string(), - Sugar::String => "You must implement 'String.cons' in order to use the string notation.".to_string(), - Sugar::U120 => "You must implement 'U120.new' in order to use the u120 notation.".to_string(), + Sugar::List => "You must implement 'Data.List', 'Data.List.cons' and 'Data.List.nil' for this type in order to use the list notation.".to_string(), + Sugar::Sigma => "You must implement 'Data.Sigma' in order to use the sigma notation.".to_string(), + Sugar::Pair => "You must implement 'Data.Sigma' and 'Data.Sigma.new' in order to use the sigma notation.".to_string(), + Sugar::BoolIf => "You must implement 'Data.Bool.if' in order to use the if notation.".to_string(), + Sugar::String => "You must implement 'Data.String.cons' in order to use the string notation.".to_string(), + Sugar::U120 => "You must implement 'Data.U120.new' in order to use the u120 notation.".to_string(), Sugar::Match(_) => "You must implement 'match' in order to use the match notation (or derive match with #derive[match]).".to_string(), Sugar::Mutter(typ) => format!("You must derive 'mutters' for '{}' in order to use this syntax", typ), Sugar::Getter(typ) => format!("You must derive 'getters' for '{}' in order to use this syntax", typ) diff --git a/crates/kind-pass/src/erasure/mod.rs b/crates/kind-pass/src/erasure/mod.rs index 493cd552..de3cf332 100644 --- a/crates/kind-pass/src/erasure/mod.rs +++ b/crates/kind-pass/src/erasure/mod.rs @@ -348,8 +348,8 @@ impl<'a> ErasureState<'a> { NumU60 { numb } => untyped::Expr::u60(expr.range, *numb), NumF60 { numb } => untyped::Expr::f60(expr.range, *numb), Str { val } => { - let nil = QualifiedIdent::new_static("String.nil", None, expr.range); - let cons = QualifiedIdent::new_static("String.cons", None, expr.range); + let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range); + let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range); self.connect_with(edge, &nil, relevance); self.connect_with(edge, &cons, relevance); @@ -491,8 +491,8 @@ impl<'a> ErasureState<'a> { NumU60 { numb } => untyped::Expr::u60(expr.range, *numb), NumF60 { numb } => untyped::Expr::f60(expr.range, *numb), Str { val } => { - let nil = QualifiedIdent::new_static("String.nil", None, expr.range); - let cons = QualifiedIdent::new_static("String.cons", None, expr.range); + let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range); + let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range); self.connect_with(edge, &nil, ambient); self.connect_with(edge, &cons, ambient); diff --git a/crates/kind-pass/src/unbound/mod.rs b/crates/kind-pass/src/unbound/mod.rs index 3e33306f..fca2f4f2 100644 --- a/crates/kind-pass/src/unbound/mod.rs +++ b/crates/kind-pass/src/unbound/mod.rs @@ -376,7 +376,7 @@ impl Visitor for UnboundCollector { match &mut pat.data { PatKind::Var(ident) => self.visit_pat_ident(ident), PatKind::Str(_) => { - let string = &mut QualifiedIdent::new_static("String", None, pat.range); + let string = &mut QualifiedIdent::new_static("Data.String", None, pat.range); self.visit_qualified_ident(&mut string.add_segment("cons").to_generated()); self.visit_qualified_ident(&mut string.add_segment("nil").to_generated()); } @@ -475,7 +475,7 @@ impl Visitor for UnboundCollector { use kind_tree::concrete::Literal::*; if let String(_) = lit { - let string = &mut QualifiedIdent::new_static("String", None, range); + let string = &mut QualifiedIdent::new_static("Data.String", None, range); self.visit_qualified_ident(&mut string.add_segment("cons").to_generated()); self.visit_qualified_ident(&mut string.add_segment("nil").to_generated()); } @@ -545,7 +545,7 @@ impl Visitor for UnboundCollector { snd, } => { self.visit_qualified_ident( - &mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(), + &mut QualifiedIdent::new_static("Data.Sigma", None, expr.range).to_generated(), ); self.visit_expr(fst); self.visit_expr(snd); @@ -556,7 +556,7 @@ impl Visitor for UnboundCollector { snd, } => { self.visit_qualified_ident( - &mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(), + &mut QualifiedIdent::new_static("Data.Sigma", None, expr.range).to_generated(), ); self.visit_expr(fst); self.context_vars.push((ident.range, ident.to_string())); @@ -587,20 +587,20 @@ impl Visitor for UnboundCollector { self.visit_sttm(sttm) } ExprKind::If { cond, then_, else_ } => { - let typ = QualifiedIdent::new_static("Bool", None, expr.range); + let typ = QualifiedIdent::new_static("Data.Bool", None, expr.range); self.visit_qualified_ident(&mut typ.add_segment("if").to_generated()); self.visit_expr(cond); self.visit_expr(then_); self.visit_expr(else_); } ExprKind::Pair { fst, snd } => { - let typ = QualifiedIdent::new_static("Pair", None, expr.range); + let typ = QualifiedIdent::new_static("Data.Pair", None, expr.range); self.visit_qualified_ident(&mut typ.add_segment("new").to_generated()); self.visit_expr(fst); self.visit_expr(snd); } ExprKind::List { args } => { - let mut typ = QualifiedIdent::new_static("List", None, expr.range); + let mut typ = QualifiedIdent::new_static("Data.List", None, expr.range); self.visit_qualified_ident(&mut typ); self.visit_qualified_ident(&mut typ.add_segment("nil").to_generated()); diff --git a/crates/kind-target-hvm/src/lib.rs b/crates/kind-target-hvm/src/lib.rs index e92a1d55..62817375 100644 --- a/crates/kind-target-hvm/src/lib.rs +++ b/crates/kind-target-hvm/src/lib.rs @@ -17,13 +17,13 @@ pub fn compile_book(book: untyped::Book, trace: bool) -> File { pub fn compile_str(val: &str) -> Box { let nil = Box::new(Term::Ctr { - name: String::from("String.nil"), + name: String::from("Data.String.nil"), args: vec![], }); let cons = |numb, next| { Box::new(Term::Ctr { - name: String::from("String.cons"), + name: String::from("Data.String.cons"), args: vec![Box::new(Term::U6O { numb }), next], }) }; @@ -105,7 +105,7 @@ fn compile_entry(file: &mut File, entry: Box, trace: bool) { args: args.clone(), }), rhs: Box::new(Term::Ctr { - name: "HVM.log".to_string(), + name: "Apps.HVM.log".to_string(), args: vec![ compile_str(entry.name.to_str()), Box::new(Term::Ctr { diff --git a/crates/kind-target-kdl/src/compile.rs b/crates/kind-target-kdl/src/compile.rs index 1bfc8ce4..d826407d 100644 --- a/crates/kind-target-kdl/src/compile.rs +++ b/crates/kind-target-kdl/src/compile.rs @@ -326,7 +326,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term { From::Ctr { name, args } => { // Convert U120 numbers into the native kindelia representation // Only possible if both U60s are U60 terms - if name.to_str() == "U120.new" { + if name.to_str() == "Data.U120.new" { if let (From::U60 { numb: hi }, From::U60 { numb: lo }) = (&args[0].data, &args[1].data) { @@ -344,97 +344,97 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term { // some numeric function applications // Add with no boundary check is just a normal add - "U60.add_unsafe" => To::Op2 { + "Data.U60.add_unsafe" => To::Op2 { oper: kdl::Oper::Add, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, // U60s are already stored in 120 bits - "U60.to_u120" => compile_expr(ctx, &args[0]), + "Data.U60.to_u120" => compile_expr(ctx, &args[0]), // Truncate to 60 bits - "U120.to_u60" => To::Op2 { + "Data.U120.to_u60" => To::Op2 { oper: kdl::Oper::And, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(To::Num { numb: U60_MAX }), }, // Compilation for U120 numeric operations - "U120.add" => To::Op2 { + "Data.U120.add" => To::Op2 { oper: kdl::Oper::Add, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.sub" => To::Op2 { + "Data.U120.sub" => To::Op2 { oper: kdl::Oper::Add, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.mul" => To::Op2 { + "Data.U120.mul" => To::Op2 { oper: kdl::Oper::Mul, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.div" => To::Op2 { + "Data.U120.div" => To::Op2 { oper: kdl::Oper::Div, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.mod" => To::Op2 { + "Data.U120.mod" => To::Op2 { oper: kdl::Oper::Mod, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_equal" => To::Op2 { + "Data.U120.num_equal" => To::Op2 { oper: kdl::Oper::Eql, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_not_equal" => To::Op2 { + "Data.U120.num_not_equal" => To::Op2 { oper: kdl::Oper::Neq, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.shift_left" => To::Op2 { + "Data.U120.shift_left" => To::Op2 { oper: kdl::Oper::Shl, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.shift_right" => To::Op2 { + "Data.U120.shift_right" => To::Op2 { oper: kdl::Oper::Shr, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_less_than" => To::Op2 { + "Data.U120.num_less_than" => To::Op2 { oper: kdl::Oper::Ltn, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_less_equal" => To::Op2 { + "Data.U120.num_less_equal" => To::Op2 { oper: kdl::Oper::Lte, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_greater_than" => To::Op2 { + "Data.U120.num_greater_than" => To::Op2 { oper: kdl::Oper::Gtn, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.num_greater_equal" => To::Op2 { + "Data.U120.num_greater_equal" => To::Op2 { oper: kdl::Oper::Gte, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.bitwise_and" => To::Op2 { + "Data.U120.bitwise_and" => To::Op2 { oper: kdl::Oper::And, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.bitwise_or" => To::Op2 { + "Data.U120.bitwise_or" => To::Op2 { oper: kdl::Oper::Or, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), }, - "U120.bitwise_xor" => To::Op2 { + "Data.U120.bitwise_xor" => To::Op2 { oper: kdl::Oper::Xor, val0: Box::new(compile_expr(ctx, &args[0])), val1: Box::new(compile_expr(ctx, &args[1])), @@ -455,11 +455,11 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term { } From::Str { val } => { let nil = kdl::Term::Ctr { - name: *ctx.kdl_names.get("String.nil").unwrap(), + name: *ctx.kdl_names.get("Data.String.nil").unwrap(), args: vec![], }; - let cons_name = *ctx.kdl_names.get("String.cons").unwrap(); + let cons_name = *ctx.kdl_names.get("Data.String.cons").unwrap(); let cons = |numb: u128, next| kdl::Term::Ctr { name: cons_name, @@ -494,7 +494,7 @@ pub fn compile_entry(ctx: &mut CompileCtx, entry: &untyped::Entry) { } } else { match entry.name.to_str() { - "U120.new" => compile_u120_new(ctx, entry), + "Data.U120.new" => compile_u120_new(ctx, entry), _ => compile_common_function(ctx, entry), } } diff --git a/crates/kind-tree/src/concrete/expr.rs b/crates/kind-tree/src/concrete/expr.rs index e6723dd1..69d3e673 100644 --- a/crates/kind-tree/src/concrete/expr.rs +++ b/crates/kind-tree/src/concrete/expr.rs @@ -397,8 +397,8 @@ impl Display for Literal { match self { Literal::Help(s) => write!(f, "?{}", s), Literal::Type => write!(f, "Type"), - Literal::NumTypeU60 => write!(f, "U60"), - Literal::NumTypeF60 => write!(f, "F60"), + Literal::NumTypeU60 => write!(f, "Data.U60"), + Literal::NumTypeF60 => write!(f, "Data.F60"), Literal::Char(c) => write!(f, "'{}'", c), Literal::NumU60(numb) => write!(f, "{}", numb), Literal::Nat(numb) => write!(f, "{}numb", numb), diff --git a/crates/kind-tree/src/desugared/mod.rs b/crates/kind-tree/src/desugared/mod.rs index a97bfebc..cbf55687 100644 --- a/crates/kind-tree/src/desugared/mod.rs +++ b/crates/kind-tree/src/desugared/mod.rs @@ -249,7 +249,7 @@ impl Expr { } pub fn num_u120(range: Range, numb: u128) -> Box { - let name = QualifiedIdent::new_static("U120.new", None, range); + let name = QualifiedIdent::new_static("Data.U120.new", None, range); let lo = Expr::num_u60(range, (numb & 0xFFFFFFFFFFFFFFF) as u64); let hi = Expr::num_u60(range, (numb >> 60) as u64); Box::new(Expr { @@ -402,8 +402,8 @@ impl Display for AppBinding { pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box], acc: u128) -> Option { match (name.to_str(), spine) { - ("Nat.zero", []) => Some(acc), - ("Nat.succ", [spine]) => match &spine.data { + ("Data.Nat.zero", []) => Some(acc), + ("Data.Nat.succ", [spine]) => match &spine.data { ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1), _ => None, }, @@ -416,8 +416,8 @@ impl Display for Expr { use ExprKind::*; match &self.data { Typ => write!(f, "Type"), - NumTypeU60 => write!(f, "U60"), - NumTypeF60 => write!(f, "F60"), + NumTypeU60 => write!(f, "Data.U60"), + NumTypeF60 => write!(f, "Data.F60"), Str { val } => write!(f, "\"{}\"", val), NumU60 { numb } => write!(f, "{}", numb), NumF60 { numb: _ } => todo!(),