Qcert.NRA.Lang.NRA
Nested Relational Algebra
By convention, "static" parameters come first, followed by
dependent operators. This allows for instanciation on those
parameters
Context {fruntime:foreign_runtime}.
Inductive nra : Set :=
| AID : nra
| AConst : data → nra
| ABinop : binOp → nra → nra → nra
| AUnop : unaryOp → nra → nra
| AMap : nra → nra → nra
| AMapConcat : nra → nra → nra
| AProduct : nra → nra → nra
| ASelect : nra → nra → nra
| ADefault : nra → nra → nra
| AEither : nra → nra → nra
| AEitherConcat : nra → nra → nra
| AApp : nra → nra → nra
.
Global Instance nra_eqdec : EqDec nra eq.
NRA Semantics
Context (h:list(string×string)).
Fixpoint nra_eval (op:nra) (x:data) : option data :=
match op with
| AID ⇒ Some x
| AConst rd ⇒ Some (normalize_data h rd)
| ABinop bop op1 op2 ⇒
olift2 (fun d1 d2 ⇒ fun_of_binop h bop d1 d2) (nra_eval op1 x) (nra_eval op2 x)
| AUnop uop op1 ⇒
olift (fun d1 ⇒ fun_of_unaryop h uop d1) (nra_eval op1 x)
| AMap op1 op2 ⇒
let aux_map d :=
lift_oncoll (fun c1 ⇒ lift dcoll (rmap (nra_eval op1) c1)) d
in olift aux_map (nra_eval op2 x)
| AMapConcat op1 op2 ⇒
let aux_mapconcat d :=
lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (nra_eval op1) c1)) d
in olift aux_mapconcat (nra_eval op2 x)
| AProduct op1 op2 ⇒
let aux_product d :=
lift_oncoll (fun c1 ⇒ lift dcoll (rmap_concat (fun _ ⇒ nra_eval op2 x) c1)) d
in olift aux_product (nra_eval op1 x)
| ASelect op1 op2 ⇒
let pred x' :=
match nra_eval op1 x' with
| Some (dbool b) ⇒ Some b
| _ ⇒ None
end
in
let aux_select d :=
lift_oncoll (fun c1 ⇒ lift dcoll (lift_filter pred c1)) d
in
olift aux_select (nra_eval op2 x)
| ADefault op1 op2 ⇒
olift (fun d1 ⇒ match d1 with
| dcoll nil ⇒ nra_eval op2 x
| _ ⇒ Some d1
end) (nra_eval op1 x)
| AEither opl opr ⇒
match x with
| dleft dl ⇒ nra_eval opl dl
| dright dr ⇒ nra_eval opr dr
| _ ⇒ None
end
| AEitherConcat op1 op2 ⇒
match nra_eval op1 x, nra_eval op2 x with
| Some (dleft (drec l)), Some (drec t) ⇒
Some (dleft (drec (rec_concat_sort l t)))
| Some (dright (drec r)), Some (drec t) ⇒
Some (dright (drec (rec_concat_sort r t)))
| _, _ ⇒ None
end
| AApp op1 op2 ⇒
olift (fun d ⇒ (nra_eval op1 d)) (nra_eval op2 x)
end.
Lemma data_normalized_orecconcat {x y z}:
orecconcat x y = Some z →
data_normalized h x → data_normalized h y →
data_normalized h z.
Lemma nra_eval_normalized {op:nra} {d:data} {o} :
nra_eval op d = Some o →
data_normalized h d →
data_normalized h o.
End NRA.
Nraebraic plan application