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

Decide subtyping for generated coq terms.

parent 93984d51
...@@ -20,6 +20,20 @@ Defined. ...@@ -20,6 +20,20 @@ Defined.
Inductive Istrue : bool -> Prop := Inductive Istrue : bool -> Prop :=
| Istrue_true : Istrue true. | Istrue_true : Istrue true.
Lemma Istrue_eq b : b = true -> Istrue b.
Proof.
intro e.
rewrite e.
exact Istrue_true.
Defined.
Lemma Istrue_eq_inv b : Istrue b -> b = true.
Proof.
intro e.
inversion e.
reflexivity.
Defined.
Definition isProp A := forall x y : A, x = y. Definition isProp A := forall x y : A, x = y.
Module String_dec. Module String_dec.
...@@ -214,7 +228,7 @@ Section subtyping. ...@@ -214,7 +228,7 @@ Section subtyping.
Proof. Proof.
decide equality. decide equality.
apply string_dec. apply string_dec.
Qed. Defined.
(* Definition of the subtyping relation: A <: B if B is a subset of A. *) (* Definition of the subtyping relation: A <: B if B is a subset of A. *)
Fixpoint Subtype A B {struct B} : Type := Fixpoint Subtype A B {struct B} : Type :=
...@@ -253,6 +267,25 @@ Section subtyping. ...@@ -253,6 +267,25 @@ Section subtyping.
assumption. assumption.
Defined. Defined.
Fixpoint subtype_dec (A B : type) : bool.
Proof.
destruct B as [ | l B1 B2 ].
- exact true.
- case_eq (mem l (domain A)).
+ intro H.
apply Istrue_eq in H.
apply mem_pos in H.
case (type_dec (assoc A l H) B1); intro.
* exact (subtype_dec A B2).
* exact false.
+ intro; exact false.
Defined.
Definition subtype_dec_correct A B : Istrue (subtype_dec A B) -> A <: B.
Proof.
admit.
Qed.
Fixpoint domain_subtype {A} {B} : Fixpoint domain_subtype {A} {B} :
A <: B -> domain B domain A. A <: B -> domain B domain A.
Proof. Proof.
...@@ -593,12 +626,10 @@ Definition lmeth_meth A (lm : Lmethod A) : Method A ((A ⊙ (lmeth_label A lm)) ...@@ -593,12 +626,10 @@ Definition lmeth_meth A (lm : Lmethod A) : Method A ((A ⊙ (lmeth_label A lm))
assumption. assumption.
Defined. Defined.
Definition pocons_3 A (lm : Lmethod A) Definition pocons_3 {A} (lm : Lmethod A) (a : Expr A) : Expr A :=
(a : Expr A) :
Expr A :=
update (lmeth_label A lm) a (lmeth_H A lm) (lmeth_meth A lm). update (lmeth_label A lm) a (lmeth_H A lm) (lmeth_meth A lm).
Notation "[ m1 ; .. ; mn ]" := (pocons_3 _ m1%meth (.. (pocons_3 _ mn%meth (init _ Istrue_true)) .. )) : object_scope. Notation "[ m1 ; .. ; mn ]" := (pocons_3 m1%meth (.. (pocons_3 mn%meth (init _ Istrue_true)) .. )) : object_scope.
Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope. Notation "[[ l = 'ς' ( x ) m ; p ]]" := (pocons l (Make_meth (fun x => m)) p) (at level 50) : object_scope.
...@@ -613,10 +644,10 @@ Section examples. ...@@ -613,10 +644,10 @@ Section examples.
Definition init_bool A : Expr (BoolT A) := init (BoolT A) Istrue_true. Definition init_bool A : Expr (BoolT A) := init (BoolT A) Istrue_true.
Definition trueT A : Expr (BoolT A) := Definition trueT A : Expr (BoolT A) :=
pocons_3 _ ("if" = ς(x !: BoolT A) (x # "then"))%meth (init_bool A). pocons_3 ("if" = ς(x !: BoolT A) (x # "then"))%meth (init_bool A).
Definition falseT A : Expr (BoolT A) := Definition falseT A : Expr (BoolT A) :=
pocons_3 _ ("if" = ς(x !: BoolT A) (x # "else"))%meth (init_bool A). pocons_3 ("if" = ς(x !: BoolT A) (x # "else"))%meth (init_bool A).
Definition Ifthenelse A b (t e : Expr A) : Expr A := Definition Ifthenelse A b (t e : Expr A) : Expr A :=
(((b##"then" ς(x !: BoolT A) t)##"else" ς(x !: BoolT A) e)#"if")%obj. (((b##"then" ς(x !: BoolT A) t)##"else" ς(x !: BoolT A) e)#"if")%obj.
...@@ -629,7 +660,7 @@ Section examples. ...@@ -629,7 +660,7 @@ Section examples.
Definition init_arr A B := init (Arrow A B) Istrue_true. Definition init_arr A B := init (Arrow A B) Istrue_true.
Definition Lambda A B (f : Expr A -> Expr B) : Expr (Arrow A B) := Definition Lambda A B (f : Expr A -> Expr B) : Expr (Arrow A B) :=
pocons_3 _ ("val" = ς(x !: Arrow A B) (f (x#"arg")))%meth (init_arr A B). pocons_3 ("val" = ς(x !: Arrow A B) (f (x#"arg")))%meth (init_arr A B).
Definition App A B (f : Expr (Arrow A B)) (a : Expr A) : Expr B := Definition App A B (f : Expr (Arrow A B)) (a : Expr A) : Expr B :=
((f##"arg" ς(x !: Arrow A B) a)#"val")%obj. ((f##"arg" ς(x !: Arrow A B) a)#"val")%obj.
......
...@@ -22,7 +22,7 @@ let rec print_ty out_fmter = function ...@@ -22,7 +22,7 @@ let rec print_ty out_fmter = function
and print_ty_elem out_fmter (l, ty) = and print_ty_elem out_fmter (l, ty) =
Format.fprintf out_fmter "@[<hov>%a :@ %a@]" Format.fprintf out_fmter "@[<hov>%a :@ %a@]"
print_label l print_label l
print_ty ty print_par_ty ty
and print_ty_elems out_fmter = function and print_ty_elems out_fmter = function
| [] -> () | [] -> ()
| [ el ] -> print_ty_elem out_fmter el | [ el ] -> print_ty_elem out_fmter el
...@@ -62,9 +62,9 @@ let rec print_term out_fmter : tterm -> unit = function ...@@ -62,9 +62,9 @@ let rec print_term out_fmter : tterm -> unit = function
print_term b print_term b
print_term t print_term t
print_par_term e print_par_term e
| Tobj (ll, _) -> | Tobj (ll, ty) ->
Format.fprintf out_fmter "[@[<hov>%a@]]" Format.fprintf out_fmter "@[<hov>%a@]"
print_obj_elems ll (print_obj_elems ty) ll
| Tsel (t, l, _) -> | Tsel (t, l, _) ->
Format.fprintf out_fmter "@[<hov>%a#%a@]" Format.fprintf out_fmter "@[<hov>%a#%a@]"
print_par_term t print_par_term t
...@@ -75,26 +75,29 @@ let rec print_term out_fmter : tterm -> unit = function ...@@ -75,26 +75,29 @@ let rec print_term out_fmter : tterm -> unit = function
print_label l print_label l
print_meth m print_meth m
| Tcast (t, ty1, ty2) -> | Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[<hov>coerce@ %a@ %a@ eq_refl@ %a@]" Format.fprintf out_fmter "@[<hov>Ecoerce@ %a@ %a@ %a@ (subtype_dec_correct@ %a@ %a@ Istrue_true)@]"
print_par_ty ty1
print_par_ty ty2 print_par_ty ty2
print_par_ty ty1
print_par_term t print_par_term t
print_par_ty ty1
print_par_ty ty2
and print_par_term out_fmter = function and print_par_term out_fmter = function
| Tvar _ | Tconst _ | Tpar _ | Tobj _ as t -> print_term out_fmter t | Tvar _ | Tconst _ | Tpar _ | Tobj _ as t -> print_term out_fmter t
| t -> | t ->
Format.fprintf out_fmter "(%a)" Format.fprintf out_fmter "(%a)"
print_term t print_term t
and print_obj_elem out_fmter (l, m) = and print_obj_elem out_fmter (l, m) =
Format.fprintf out_fmter "@[<hov>%a =@ %a@]" Format.fprintf out_fmter "(@[<hov>%a =@ %a@])%%meth"
print_label l print_label l
print_meth m print_meth m
and print_obj_elems out_fmter = function and print_obj_elems ty out_fmter = function
| [] -> () | [] ->
| [el] -> print_obj_elem out_fmter el Format.fprintf out_fmter "(init@ %a@ Istrue_true)"
print_par_ty ty
| el :: els -> | el :: els ->
Format.fprintf out_fmter "%a;@ %a" Format.fprintf out_fmter "(pocons_3@ %a@ %a)"
print_obj_elem el print_obj_elem el
print_obj_elems els (print_obj_elems ty) els
and print_meth out_fmter (Tmeth (x, ty, body, _)) = and print_meth out_fmter (Tmeth (x, ty, body, _)) =
Format.fprintf out_fmter "@[<h>ς(%a !: %a)%a@]" Format.fprintf out_fmter "@[<h>ς(%a !: %a)%a@]"
print_id x print_id x
...@@ -107,15 +110,16 @@ let rec print_line out_fmter = function ...@@ -107,15 +110,16 @@ let rec print_line out_fmter = function
print_cid cid print_cid cid
print_par_ty ty print_par_ty ty
| Tvardef (id, ty, def) -> | Tvardef (id, ty, def) ->
Format.fprintf out_fmter "@[<h>Definition %a :@ Obj %a :=@ %a%%obj.@]@\n" Format.fprintf out_fmter "@[<h>Definition %a :@ Expr %a :=@ %a%%obj.@]@\n"
print_id id print_id id
print_par_ty ty print_par_ty ty
print_par_term def print_par_term def
| Tcheck (t, ty) -> | Tcheck (t, ty) ->
Format.fprintf out_fmter "@[<h>Goal Obj %a@]. Format.fprintf out_fmter "@[<h>Goal Expr %a@].
Proof. Proof.
exact %a%%obj. exact %a%%obj.
Qed." Qed.
"
print_par_ty ty print_par_ty ty
print_par_term t print_par_term t
| Tconv (t1, t2, ty) -> | Tconv (t1, t2, ty) ->
......
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