diff options
| -rw-r--r-- | src/coq/Semantics.v | 16 | ||||
| -rw-r--r-- | src/coq/Syntax.v | 2 |
2 files changed, 17 insertions, 1 deletions
diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v index 2022ec94..19c67a05 100644 --- a/src/coq/Semantics.v +++ b/src/coq/Semantics.v @@ -209,5 +209,21 @@ Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t := | right _ => fun x => x end ((eDen e1) n) + | Concat c1 c2 e1 e2 => fun n => + match (cDen c1) n as D return match D with + | None => unit + | Some T => T + end + -> match (match D with + | None => (cDen c2) n + | v => v + end) with + | None => unit + | Some T => T + end with + | None => fun _ => (eDen e2) n + | _ => fun x => x + end ((eDen e1) n) + | _ => cheat _ end. diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v index 13b7e9de..b19a790e 100644 --- a/src/coq/Syntax.v +++ b/src/coq/Syntax.v @@ -187,6 +187,6 @@ Section vars. | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _))) | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c') - | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) + | Concat : forall c1 c2, exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2)) | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c). End vars. |