Commit c66c9c25 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

[Coq formalisation] [HUGE] Correct coercion

Coercion cannot be defined as a function, counterexamples added to
test.sigma.

We have to distinguish objects (ς-terms) and expressions (ς-terms with
explicit coercions).

In order to get an expression from an object, subtyping should be
reflexive, which is only the case for well-formed types (associations
lists without duplicates) so we add an invariant on types using a
Σ-type.

Because of these, reduction in Coq is very slow and Coq cannot check the
examples yet.
parent 81ce5cff
This diff is collapsed.
......@@ -2,7 +2,7 @@ open Parsetree
open Scoper
open Typer
let print_id out_fmter (Id i) = Format.fprintf out_fmter "%s" i
let print_id out_fmter (Id i) = Format.fprintf out_fmter "_%s" i
let print_cid out_fmter (Cid c) = Format.fprintf out_fmter "%s" c
let print_label out_fmter (Label l) = Format.fprintf out_fmter "\"%s\"" l
......@@ -17,7 +17,7 @@ let rec print_ty out_fmter = function
print_par_ty ty1
print_par_ty ty2
| Stbool ty ->
Format.fprintf out_fmter "@[<hov>Bool@ %a@]"
Format.fprintf out_fmter "@[<hov>BoolT@ %a@]"
print_par_ty ty
and print_ty_elem out_fmter (l, ty) =
Format.fprintf out_fmter "@[<hov>%a :@ %a@]"
......@@ -52,13 +52,13 @@ let rec print_term out_fmter : tterm -> unit = function
print_ty ty
print_par_term body
| Ttrue ty ->
Format.fprintf out_fmter "@[<hov>true@ %a@]"
Format.fprintf out_fmter "@[<hov>trueT@ %a@]"
print_par_ty ty
| Tfalse ty ->
Format.fprintf out_fmter "@[<hov>false@ %a@]"
Format.fprintf out_fmter "@[<hov>falseT@ %a@]"
print_par_ty ty
| Tif (b, t, e, _) ->
Format.fprintf out_fmter "@[<hov>IF@ %a@ THEN@ %a@ ELSE@ %a@]"
Format.fprintf out_fmter "@[<hov>ifT@ %a@ then@ %a@ else@ %a@]"
print_term b
print_term t
print_par_term e
......@@ -75,7 +75,7 @@ let rec print_term out_fmter : tterm -> unit = function
print_label l
print_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>coerce@ %a@ %a@ tt@ %a@]"
Format.fprintf out_fmter "@[<hov>coerce@ %a@ %a@ eq_refl@ %a@]"
print_par_ty ty1
print_par_ty ty2
print_par_term t
......@@ -121,7 +121,7 @@ Qed."
| Tconv (t1, t2, _) ->
Format.fprintf out_fmter "@[<h>Goal %a%%obj =@ %a%%obj@].
Proof.
reflexivity.
repeat (reduce_equality || simpl || apply f_equal).
Qed.
@\n"
print_par_term t1
......
......@@ -76,4 +76,16 @@ check (myCell.set 42).get = 42 : Nat.
print "\nChecking myCell.get = 0 : Nat.\n".
check myCell.get = 0 : Nat.
print "\nChecking that objects are not distinguishable after updates.\n".
type XY ::= [ x : Nat; y : Nat ].
type XYZ ::= [ x : Nat; y : Nat; z : Nat ].
let a : XY ::= [ x = ς(s : XYZ) s.y; y = ς(s : XYZ) 0; z = ς(s : XYZ) 0 ].
check (a.y := 42).x = 42 : Nat.
print "\nEnd of examples.\n".
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment