mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Prevent checker from fully evaluating top-level types
This commit is contained in:
parent
73e1e70785
commit
19fc3cbcbd
@ -1,6 +1,6 @@
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.2.66"
|
||||
version = "0.2.67"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
|
@ -910,7 +910,7 @@ Line = (String.cons 10 String.nil)
|
||||
(Infer (All orig name type body)) =
|
||||
ask dep = (Checker.bind Checker.get_depth)
|
||||
ask type_chk = (Checker.bind (Check type (Typ orig)))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var orig name dep)) (Typ orig)) name type []))
|
||||
ask body_chk = (Checker.bind (Checker.extended (Check (body (Var orig name dep)) (Typ orig)) name (Eval type) []))
|
||||
(Checker.done (Typ orig))
|
||||
|
||||
// Infers Lam
|
||||
@ -945,7 +945,7 @@ Line = (String.cons 10 String.nil)
|
||||
|
||||
// Infers Ct0
|
||||
(Infer (Ct0 ctid orig)) =
|
||||
(Checker.done (TypeOf ctid))
|
||||
(Checker.done (Eval (TypeOf ctid)))
|
||||
|
||||
// Infers Ct1
|
||||
(Infer (Ct1 ctid orig x0)) =
|
||||
@ -981,7 +981,7 @@ Line = (String.cons 10 String.nil)
|
||||
|
||||
// Infers Fn0
|
||||
(Infer (Fn0 ctid orig)) =
|
||||
(Checker.done (TypeOf ctid))
|
||||
(Checker.done (Eval (TypeOf ctid)))
|
||||
|
||||
// Infers Fn1
|
||||
(Infer (Fn1 ctid orig x0)) =
|
||||
@ -1566,7 +1566,7 @@ API.eval_main = (Text [
|
||||
let ruls = (RuleOf func)
|
||||
let type = (TypeOf func)
|
||||
let type_check = (Checker.run (Unify (Check type (Typ 0))) True)
|
||||
let rule_check = (API.check_function.rules ruls type)
|
||||
let rule_check = (API.check_function.rules ruls (Eval type))
|
||||
(List.cons type_check rule_check)
|
||||
|
||||
// Checks a function's rules
|
||||
|
@ -1738,9 +1738,9 @@ pub fn compile_entry(entry: &Entry) -> String {
|
||||
fn compile_type(args: &Vec<Box<Argument>>, tipo: &Box<Term>, index: usize) -> String {
|
||||
if index < args.len() {
|
||||
let arg = &args[index];
|
||||
format!("(All {} {} {} λ{} {})", 0, name_to_u64(&arg.name), compile_term(&arg.tipo, false, false), arg.name, compile_type(args, tipo, index + 1))
|
||||
format!("(All {} {} {} λ{} {})", 0, name_to_u64(&arg.name), compile_term(&arg.tipo, true, false), arg.name, compile_type(args, tipo, index + 1))
|
||||
} else {
|
||||
compile_term(tipo, false, false)
|
||||
compile_term(tipo, true, false)
|
||||
}
|
||||
}
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user