... suite:
let type_eq = mkBuiltin ((dloc, "Eq"), type_eq_type) -let eq_refl =
+(* FIXME: Is this the best way to do this? Originally, I wanted to
define this in Typer and then reference it from OCaml code.- *)
Comme discuté, c'est possible que ce soit le mieux qu'on puisse faire pour l'instant, en effet :-( Quoique... voir ci-dessous.
+(* Defining the following:
- typecons Interval i0 i1
- *)
+let type_interval = mkInductive (dsinfo, (dloc, "Interval"), [],
List.fold_left (fun m name -> SMap.add name [] m)SMap.empty["i0"; "i1"])
SVP évite de dépasser les 80 colonnes (e.g. ajoute un line-break juste avant le `=`).
+let eq_eq =
- (* Variables for the type level, type and the function (I -> ?A) *)
- let lv = (dsinfo, Some "l") in
- let tv = (dsinfo, Some "t") in
- let fv = (dsinfo, Some "f") in
- mkBuiltin ((dloc, "Eq.eq"),
mkArrow (dsinfo, Aerasable, lv,type_level,mkArrow (dsinfo, Aerasable, tv,mkSort (dsinfo, Stype (mkVar (lv, 0))),mkArrow (dsinfo, Anormal, fv,mkArrow (dsinfo, Aerasable, (dsinfo, None),type_interval,mkVar (tv, 1)),mkCall (dsinfo, type_eq,[Aerasable, mkVar (lv, 2);Aerasable, mkVar (tv, 1);Anormal, mkCall (dsinfo, mkVar (fv, 0),[Aerasable, interval_i0]);Anormal, mkCall (dsinfo, mkVar (fv, 0),
Hmm... je cois qu'on faisait déjà ça pour `eq_refl` (où "ça", c'est de définir le builtin à double: une fois ici en OCaml et une fois en Typer. C'est redondant et en plus je ne suis pas sûr si le code vérifie que les deux types sont égaux).
Je pense qu'on aurait intérêt à utiliser un predef ici. Je vois que `eq_refl` était utilisé dans `opslexp.ml` et que maintenant tu utilises `eq_eq` au même endroit, donc on en a besoin tôt (avant de finir de lire `builtins.typer`), mais on devrait pouvoir utiliser un hack comme celui que j'utilise pour `Macro` (c.f. la définition de `predef_map` où je mets une version dummy de `Macro`), du moins tant qu'on utilise pas *vraiment* `eq_eq` dans `builtins.typer`.
C'est probablement vrai pour `Eq_uneq` aussi.
(* easier to debug with type annotations *) type env_elem = (vname * varbind * ltype) diff --git a/src/env.ml b/src/env.ml index f60f0f3..77e3cb4 100644 --- a/src/env.ml +++ b/src/env.ml @@ -63,6 +63,7 @@ type value_type = | Vref of (value_type ref) | Velabctx of DB.elab_context | Varray of (value_type array)
- | Veq of value_type (* TODO: Do I need a runtime value of an equality proof? *)
Notre printer devrait prendre non seulement une `value_type` en argument, mais aussi son `ltype` (ou au moins la version `elexp` de son `ltype`), par exemple pour correctement imprimer une valeur de type `τ₁ ≡> τ₂` 🙂. Donc nos preuves d'égalité n'ont pas besoin d'être représentées par des valeurs qui disent "je suis une preuve d'égalité".
Ceci dit, c'est OK d'ajouter `Veq` pour l'instant (la performance ne nous préoccupe pas vraiment et ça peut faciliter le debugging).
- | Veq v -> let v' = value_string v in
v' ^ " = " ^ v' (* FIXME: Is this always correct? *)
What do you mean by "correct"? What kind of problem are you worried about?
+let eq_eq loc _ vs = match vs with
- | [v] -> Veq v
- | _ -> error loc "Eq_eq takes a single value as argument"
+let eq_uneq loc _ vs = match vs with
- | [_x; _y; Veq v] -> v
- | _ -> error loc "Eq_uneq takes 3 arguments"
Hmm... now I realize we do have a real problem:
If the `f` arg to `Eq_eq` is erased, then `eq_uneq` cannot return it, really. Because at run time, we can't extract that from the equality proof if it's erased.
So, instead of something like
Eq_uneq : Eq ?x ?y → (I ≡> τ);
we'd need something like:
Eq_uneq : Eq ?x ?y → ((f : I ≡> τ) ≡> ?α) → α
I.e. a kind of "let" version of "uneq" so we can mark the `f` erased. But that doesn't work for `eq_uneq_whnf` any more :-(
Hmm....
So we have to keep the `f` argument of `Eq_eq` as non-erased, indeed!!
diff --git a/src/opslexp.ml b/src/opslexp.ml index b18a7ea..d08d170 100644
....la suite au prochain épisode,
Stefan