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

Use more projections in Coq encoding.

parent c2ba58de
......@@ -541,7 +541,23 @@ Section objects.
(* An expression of pretype B is an object of pretype A <: B coerced to pretype B. *)
Definition Expr (B : type) := sigT (fun A => ((Obj A) * (A <: B))%type).
Definition expr_type {B : type} (e : Expr B) : type.
Proof.
destruct e as (A, _).
exact A.
Defined.
Definition expr_obj {B : type} (e : Expr B) : Obj (expr_type e).
Proof.
destruct e as (A, (a, st)).
unfold expr_type.
assumption.
Defined.
Definition expr_st {B : type} (e : Expr B) : (expr_type e) <: B.
Proof.
destruct e as (A, (a, st)).
unfold expr_type.
assumption.
Defined.
Definition Obj_to_expr {A} : Obj A -> Expr A.
Proof.
exists A.
......@@ -622,10 +638,10 @@ Section semantics.
Defined.
Definition select l {A} (e : Expr A) (H : l (domain A)) : Expr (assoc A l).
destruct e as (A', (a', st)).
rewrite <- (preassoc_subtype_wf A' A l st H).
exact (Eval_meth (preselect l a' (predomain_subtype l st H))
(Obj_to_expr a')).
(* destruct e as (A', (a', st)). *)
rewrite <- (preassoc_subtype_wf (expr_type e) A l (expr_st e) H).
exact (Eval_meth (preselect l (expr_obj e) (predomain_subtype l (expr_st e) H))
(Obj_to_expr (expr_obj e))).
Defined.
Fixpoint preupdate_cons l {A} {f} {l2} {d} (po : Preobj A f (cons l2 d))
......@@ -659,18 +675,18 @@ Section semantics.
Definition update l A (e : Expr A) (m : Method A (assoc A l)) (H : l domain A) : Expr A.
Proof.
destruct e as (A', (a', st)).
exists A'.
(* destruct e as (A', (a', st)). *)
exists (expr_type e).
split.
- apply (obj_update l a').
- apply (obj_update l (expr_obj e)).
apply Make_meth.
intro self.
rewrite (preassoc_subtype_wf A' A l st H).
rewrite (preassoc_subtype_wf (expr_type e) A l (expr_st e) H).
apply (Eval_meth m).
apply (coerce st).
apply (coerce (expr_st e)).
exact self.
exact (predomain_subtype l st H).
- assumption.
exact (predomain_subtype l (expr_st e) H).
- exact (expr_st e).
Defined.
(* Specification of select: *)
......@@ -784,12 +800,23 @@ Section init.
End init.
(* Definition of objects without respecting the order of labels given by the pretype. *)
Definition lmeth_label A (lm : Lmethod A) :=
let (l, _) := lm in l.
Definition lmeth_meth A (lm : Lmethod A) : Method A (A (lmeth_label A lm)).
destruct lm as (l, (H, m)).
unfold lmeth_label.
assumption.
Defined.
Definition lmeth_H A (lm : Lmethod A) : (lmeth_label A lm) domain A.
destruct lm as (l, (H, m)).
unfold lmeth_label.
assumption.
Defined.
Definition pocons_3 A (lm : Lmethod A)
(a : Expr A) :
Expr A :=
let (l, Hm) := lm in
let (H, m) := Hm in
update l A a m H.
update (lmeth_label A lm) A a (lmeth_meth A lm) (lmeth_H A lm).
Notation "[ m1 ; .. ; mn ]" := (pocons_3 _ m1%meth (.. (pocons_3 _ mn%meth (init _)) .. )) : object_scope.
......
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