[ fix #25 ] Generate Unit for One

rustdoc/katex-header.html

@@ -1,6 +1,16 @@
-<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css"    integrity="sha384-dbVIfZGuN1Yq7/1Ocstc1lUEm+AT+/rCkibIcC/OmWo5f0EA48Vf8CytHzGrSwbQ" crossorigin="anonymous">
-<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js"               integrity="sha384-2BKqo+exmr9su6dir+qCw08N2ZKRucY4PrGQPPWU1A7FtlCGjmEGFqXCv5nyM5Ij" crossorigin="anonymous"></script>
-<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/contrib/auto-render.min.js" integrity="sha384-kWPLUVMOks5AQFrykwIup5lo0m3iMkkHrD0uJ4H5cjeGihAutqP0yW0J6dpFiVkI" crossorigin="anonymous"></script>
+<noscript>This page requires javascript to work</noscript>
+<link rel="stylesheet"
+      href="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.css"
+      integrity="sha384-BdGj8xC2eZkQaxoQ8nSLefg4AV4/AwB3Fj+8SUSo7pnKP6Eoy18liIKTPn9oBYNG"
+      crossorigin="anonymous">
+<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/katex.min.js"
+        integrity="sha384-JiKN5O8x9Hhs/UE5cT5AAJqieYlOZbGT3CHws/y97o3ty4R7/O5poG9F3JoiOYw1"
+        crossorigin="anonymous"></script>
+<script defer
+        src="https://cdn.jsdelivr.net/npm/[email protected]/dist/contrib/auto-render.min.js"
+        integrity="sha384-kWPLUVMOks5AQFrykwIup5lo0m3iMkkHrD0uJ4H5cjeGihAutqP0yW0J6dpFiVkI"
+        crossorigin="anonymous"
+        onload="renderMathInElement(document.body);"></script>
 <script>
     document.addEventListener("DOMContentLoaded", function() {
         renderMathInElement(document.body, {
@@ -12,4 +22,5 @@
             ]
         });
     });
-</script>
+
+</script>

samples/basics/parse-only.out

@@ -1,3 +1,4 @@
 Parse successful.
 let a: b = c;
 
+

samples/basics/syntacic-sugar.out

@@ -5,4 +5,8 @@ let f: Π _: a. b = λ x. x;
 let p: Σ _: a. b = (0, 0);
 const infer_my_type = (1, 1);
 
+
+
+
+
 Type-Check successful.

samples/sum-split/bool.minitt

@@ -17,3 +17,15 @@ let and: bool -> bool -> bool = split
  | False => \lambda _. False
  };
 -- Nested functions
+
+let elimBool
+  : \Pi c : bool → Type
+  . \Pi _ : c False
+  . \Pi _ : c True
+  . \Pi b : bool
+  . c b
+
+  = λ c . λ h0 . λ h1 . split
+  { True => h1
+  | False => h0
+  };

src/check/expr.rs

@@ -100,7 +100,7 @@ pub fn check_infer(index: u32, mut tcs: TCS, expression: Expression) -> TCM<Valu
             let (left_level, new) = check_type(index, tcs, *input.expression.clone())?;
             tcs = new;
             let input_type = input.expression.eval(tcs.context());
-            let generated = generate_value(index);
+            let generated = generate_for(index, &input_type);
             let gamma = update_gamma(tcs.gamma, &input.pattern, input_type, generated)?;
             let (right_level, _) = check_type(index + 1, TCS::new(gamma, tcs.context), *output)?;
             // Does this need to depend on the level of the return type?
@@ -110,7 +110,7 @@ pub fn check_infer(index: u32, mut tcs: TCS, expression: Expression) -> TCM<Valu
             Lambda(pattern, Some(parameter_type), return_value) => {
                 let parameter_type = *parameter_type.internal;
                 tcs = check(index, tcs, *argument, parameter_type.clone())?;
-                let generated = generate_value(index + 1);
+                let generated = generate_for(index + 1, &parameter_type);
                 let tcs = tcs.update(pattern, parameter_type, generated)?;
                 check_infer(index + 1, tcs, *return_value)
             }
@@ -244,7 +244,7 @@ pub fn check(index: u32, mut tcs: TCS, expression: Expression, value: Value) ->
         (E::Void, _) => Ok(tcs),
         (E::Lambda(pattern, _, body), V::Pi(signature, closure)) => {
             let fake_tcs: TCS = tcs_borrow!(tcs);
-            let generated = generate_value(index);
+            let generated = generate_for(index, &*signature);
             let fake_tcs = fake_tcs.update(pattern, *signature, generated.clone())?;
             check(index + 1, fake_tcs, *body, closure.instantiate(generated))?;
             Ok(tcs)
@@ -378,12 +378,16 @@ pub fn check_telescoped(
 ) -> TCM<(Level, TCS)> {
     let (_, new) = check_type(index, tcs, *first.expression.clone())?;
     tcs = new;
-    let generated = generate_value(index);
-    let internal_tcs = tcs_borrow!(tcs).update(
-        first.pattern,
-        first.expression.eval(tcs.context()),
-        generated,
-    )?;
+    let ty = first.expression.eval(tcs.context());
+    let generated = generate_for(index, &ty);
+    let internal_tcs = tcs_borrow!(tcs).update(first.pattern, ty, generated)?;
     let (level, _) = check_type(index + 1, internal_tcs, second)?;
     Ok((level, tcs))
 }
+
+fn generate_for(index: u32, ty: &Value) -> Value {
+    match &ty {
+        Value::One => Value::Unit,
+        _ => generate_value(index),
+    }
+}