diff options
Diffstat (limited to 'src/checker_signature.rs')
| -rw-r--r-- | src/checker_signature.rs | 74 |
1 files changed, 55 insertions, 19 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index beb0af6..2888568 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -24,8 +24,27 @@ impl CheckerState { Ok(Param { set, name: canon }) }) .collect::<Result<Vec<_>, _>>()?; - let codomain = Box::new(ctx.check_signature(codomain)?); - Ok(Signature::Ext { params, codomain }) + let codomain = ctx.check_signature(codomain)?; + + let result = if let Signature::Ext { + params: inner, + codomain: deep, + } = codomain + { + let mut merged = params.clone(); + merged.extend(inner.iter().cloned()); + Signature::Ext { + params: merged, + codomain: deep, + } + } else { + Signature::Ext { + params, + codomain: Box::new(codomain), + } + }; + + Ok(result) } Signature::Theory(fields) => { let mut ctx = self.clone(); @@ -36,10 +55,7 @@ impl CheckerState { ctx.add_instance(name.clone(), InstanceValue::Hypothetical, signature.clone())?; // And lo, the special case, our chosen canonical form if signature == Signature::Set { - ctx.add_set( - name.clone(), - Set::ClaimedSet(Instance::Var(name.clone())).into(), - )?; + ctx.add_set(name.clone(), Set::ClaimedSet(Instance::Var(name.clone())))?; } new_fields.push(Field { name: name.clone(), @@ -153,7 +169,7 @@ impl CheckerState { if f_s == Signature::Set { ctx.add_set( f_n.clone(), - Set::ClaimedSet(Instance::Var(f_n.clone())).into(), + Set::ClaimedSet(Instance::Var(f_n.clone())), )?; } @@ -316,12 +332,37 @@ impl CheckerState { params: inst_params, body, } => { + if inst_params.is_empty() { + return Err(CheckerError::Unimplemented( + "for instance with empty params".to_string(), + )); + } + + // deal with left-nesting + let mut ctx = self.clone(); + for Param { name, set } in inst_params { + ctx.make_element_binding(name.clone(), set.clone())?; + } + let body = ctx.check_instance(body, None)?; + let (inst_params, body) = if let Instance::For { + params: inner_params, + body: inner_body, + } = body + { + let mut merged = inst_params.clone(); + merged.extend(inner_params.clone()); + (merged, *inner_body) + } else { + (inst_params.clone(), body) + }; + if let Some(signature) = signature { if inst_params.is_empty() { return Err(CheckerError::Unimplemented( "instance for with empty params".to_string(), )); }; + let Signature::Ext { params: sig_params, codomain, @@ -339,11 +380,13 @@ impl CheckerState { claimed: signature.clone(), }); }; + if sig_params.is_empty() { return Err(CheckerError::Unimplemented( "extension signature with empty params".to_string(), )); } + if sig_params.len() != inst_params.len() { return Err(CheckerError::InstanceDoesNotBelong { instance: instance.clone(), @@ -365,7 +408,7 @@ impl CheckerState { set: set_s, }, )| { - let inst_s = ctx.check_set(inst_s)?; + let inst_s = ctx.check_set(&inst_s)?; let set_s = ctx.check_set(set_s)?; if !ctx.equal(&inst_s, &set_s) { return Err(CheckerError::InstanceDoesNotBelong{ @@ -387,7 +430,7 @@ impl CheckerState { }, ) .collect::<Result<Vec<_>, _>>()?; - let body = ctx.check_instance(body, Some(&*codomain))?; + let body = ctx.check_instance(&body, Some(&*codomain))?; Ok(Instance::For { body: Box::new(body), params: inst_params, @@ -405,7 +448,7 @@ impl CheckerState { }) }) .collect::<Result<Vec<_>, _>>()?; - let body = ctx.check_instance(body, None)?; + let body = ctx.check_instance(&body, None)?; Ok(Instance::For { params: inst_params, body: Box::new(body), @@ -416,18 +459,11 @@ impl CheckerState { instance: inner, args, } => { - // this is the only time that we ever call check_instance with - // signature = None, and in this mode all we want is to put - // inner into a canonical form pushing stuck terms to the leaves - // and simplifying everything else. let subject = self.check_instance(inner, None)?; - // the whole game here is to make sure that we have no left // nesting, and that we're fully evaluated. If that's true then - // we don't need to come up with signatures for partial - // application. The parser already enforces this, but the - // cunning user may supply ASTs directly so we do this here as - // well. + // structural equality is much more powerful, and partial + // application is simpler. let (subject, args) = match subject { Instance::App { instance: inner_inner, |