Qcert.NRA.Typing.TNRAInfer

Section TNRAInfer.

Type inference for NRA when given the type of the input

  Section aux.
    Context {fdata:foreign_data}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.

    Definition tmapConcatInput (τ₁: rtype) : option (list (string ×rtype)).

    Definition tmapConcatOutput (τ₁ : list (string ×rtype)) (τ₂: rtype) : option rtype.

  End aux.

  Context {m:basic_model}.

  Fixpoint infer_nra_type (e:nra) (τin:rtype) : option rtype :=
    match e with
      | AID ⇒ Some τin
      | AConst d ⇒ infer_data_type (normalize_data brand_relation_brands d)
      | ABinop b op1 op2 ⇒
        let binf (τ₁ τ₂:rtype) := infer_binop_type b τ ₁ τ ₂ in
        olift2 binf (infer_nra_type op1 τin) (infer_nra_type op2 τin)
      | AUnop u op1 ⇒
        let unf (τ₁:rtype) := infer_unop_type u τ ₁ in
        olift unf (infer_nra_type op1 τin)
      | AMap op1 op2 ⇒
        let mapf (τ₁:rtype) :=
            olift (fun x ⇒ lift (fun y ⇒ Coll y) (infer_nra_type op1 x)) (tuncoll τ ₁)
        in
        olift mapf (infer_nra_type op2 τin)
      | AMapConcat op1 op2 ⇒
        let mapconcatf (τ₁:list (string ×rtype)) :=
            match RecMaybe Closed τ ₁ with
              | None ⇒ None
              | Some τr₁ ⇒
                match olift (tmapConcatOutput τ ₁) (infer_nra_type op1 τr₁) with
                  | None ⇒ None
                  | Some τ₂ ⇒ Some (Coll τ₂)
                end
            end
        in
        olift mapconcatf (olift tmapConcatInput (infer_nra_type op2 τin))
      | AProduct op1 op2 ⇒
        let mapconcatf (τ₁:list (string ×rtype)) :=
            match RecMaybe Closed τ ₁ with
              | None ⇒ None
              | Some τr₁ ⇒
                match olift (tmapConcatOutput τ ₁) (infer_nra_type op2 τin) with
                  | None ⇒ None
                  | Some τ₂ ⇒ Some (Coll τ₂)
                end
            end
        in
        olift mapconcatf (olift tmapConcatInput (infer_nra_type op1 τin))
      | ASelect op1 op2 ⇒
        let selectf (τ₁:rtype) :=
            match tuncoll τ ₁ with
              | Some τ₁' ⇒
                match infer_nra_type op1 τ₁' with
                  | Some τ₂ ⇒
                    match `τ₂ with
                      | Bool₀ ⇒ Some (Coll τ₁')
                      | _ ⇒ None
                    end
                  | None ⇒ None
                end
              | None ⇒ None
            end
        in
        olift selectf (infer_nra_type op2 τin)
      | ADefault op1 op2 ⇒
        match ((infer_nra_type op1 τin), (infer_nra_type op2 τin)) with
            | (Some τ₁', Some τ₂') ⇒
              match (tuncoll τ₁', tuncoll τ₂') with
                | (Some τ₁₀, Some τ₂₀) ⇒
                  if (`τ₁₀ == `τ₂₀) then Some τ₁' else None
                | _ ⇒ None
              end
            | (_, _) ⇒ None
        end
      | AEither op1 op2 ⇒
        match tuneither τin with
        | Some (τl, τr) ⇒
          match ((infer_nra_type op1 τl), (infer_nra_type op2 τr)) with
          | (Some τ₁', Some τ₂') ⇒
            if (rtype_eq_dec τ₁' τ₂')
            then Some τ₁'
            else None
          | (_, _) ⇒ None
          end
        | _ ⇒ None
        end
      | AEitherConcat op1 op2 ⇒
        match (infer_nra_type op1 τin, infer_nra_type op2 τin) with
        | (Some τeither, Some τrecplus) ⇒
          match tuneither τeither with
          | Some (τl, τr) ⇒
            match (trecConcat τl τrecplus, trecConcat τr τrecplus) with
            | (Some τrecl, Some τrecr) ⇒
              Some (Either τrecl τrecr)
            | (_, _) ⇒ None
            end
          | None ⇒ None
          end
        | (_, _) ⇒ None
        end
      | AApp op1 op2 ⇒
        let appf (τ₁:rtype) := infer_nra_type op1 τ ₁ in
        olift appf (infer_nra_type op2 τin)
    end.

  Lemma infer_nra_type_correct (τin τout:rtype) (e:nra) :
    infer_nra_type e τin = Some τ out →
    nra_type e τin τ out.

End TNRAInfer.