Qcert.NRAEnv.Typing.TcNRAEnvInfer

Section TcNRAEnvInfer.

Type inference for NRA when given the type of the input

  Context {m:basic_model}.
  Context (τconstants:list (string ×rtype)).

  Fixpoint infer_cnraenv_type (e:cnraenv) (τenv τin:rtype) : option rtype :=
    match e with
      | ANID ⇒ Some τin
      | ANConst d ⇒ infer_data_type (normalize_data brand_relation_brands d)
      | ANBinop b op1 op2 ⇒
        let binf (τ₁ τ₂:rtype) := infer_binop_type b τ ₁ τ ₂ in
        olift2 binf (infer_cnraenv_type op1 τ env τin) (infer_cnraenv_type op2 τ env τin)
      | ANUnop u op1 ⇒
        let unf (τ₁:rtype) := infer_unop_type u τ ₁ in
        olift unf (infer_cnraenv_type op1 τ env τin)
      | ANMap op1 op2 ⇒
        let mapf (τ₁:rtype) :=
            olift (fun x ⇒ lift (fun y ⇒ Coll y) (infer_cnraenv_type op1 τ env x)) (tuncoll τ ₁)
        in
        olift mapf (infer_cnraenv_type op2 τ env τin)
      | ANMapConcat op1 op2 ⇒
        let mapconcatf (τ₁:list (string ×rtype)) :=
            match RecMaybe Closed τ ₁ with
              | None ⇒ None
              | Some τr₁ ⇒
                match olift (tmapConcatOutput τ ₁) (infer_cnraenv_type op1 τ env τr₁) with
                  | None ⇒ None
                  | Some τ₂ ⇒ Some (Coll τ₂)
                end
            end
        in
        olift mapconcatf (olift tmapConcatInput (infer_cnraenv_type op2 τ env τin))
      | ANProduct op1 op2 ⇒
        let mapconcatf (τ₁:list (string ×rtype)) :=
            match RecMaybe Closed τ ₁ with
              | None ⇒ None
              | Some τr₁ ⇒
                match olift (tmapConcatOutput τ ₁) (infer_cnraenv_type op2 τ env τin) with
                  | None ⇒ None
                  | Some τ₂ ⇒ Some (Coll τ₂)
                end
            end
        in
        olift mapconcatf (olift tmapConcatInput (infer_cnraenv_type op1 τ env τin))
      | ANSelect op1 op2 ⇒
        let selectf (τ₁:rtype) :=
            match tuncoll τ ₁ with
              | Some τ₁' ⇒
                match infer_cnraenv_type op1 τ env τ₁' with
                  | Some τ₂ ⇒
                    match `τ₂ with
                      | Bool₀ ⇒ Some (Coll τ₁')
                      | _ ⇒ None
                    end
                  | None ⇒ None
                end
              | None ⇒ None
            end
        in
        olift selectf (infer_cnraenv_type op2 τ env τin)
      | ANDefault op1 op2 ⇒
        match ((infer_cnraenv_type op1 τ env τin), (infer_cnraenv_type op2 τ env τin)) with
            | (Some τ₁', Some τ₂') ⇒
              match (tuncoll τ₁', tuncoll τ₂') with
                | (Some τ₁₀, Some τ₂₀) ⇒
                  if (`τ₁₀ == `τ₂₀) then Some τ₁' else None
                | _ ⇒ None
              end
            | (_, _) ⇒ None
        end
      | ANEither op1 op2 ⇒
        match tuneither τin with
        | Some (τl, τr) ⇒
          match ((infer_cnraenv_type op1 τ env τl), (infer_cnraenv_type op2 τ env τr)) with
          | (Some τ₁', Some τ₂') ⇒
            if (rtype_eq_dec τ₁' τ₂')
            then Some τ₁'
            else None
          | (_, _) ⇒ None
          end
        | _ ⇒ None
        end
      | ANEitherConcat op1 op2 ⇒
        match (infer_cnraenv_type op1 τ env τin, infer_cnraenv_type op2 τ env τ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
      | ANApp op1 op2 ⇒
        let appf (τ₁:rtype) := infer_cnraenv_type op1 τ env τ ₁ in
        olift appf (infer_cnraenv_type op2 τ env τin)
      | ANGetConstant s ⇒
        tdot τ constants s
      | ANEnv ⇒
        Some τ env
      | ANAppEnv op1 op2 ⇒
        let appf (τ₁:rtype) := infer_cnraenv_type op1 τ ₁ τin in
        olift appf (infer_cnraenv_type op2 τ env τin)
      | ANMapEnv op1 ⇒
        let mapf (τenv':rtype) :=
            lift Coll (infer_cnraenv_type op1 τ env' τin)
        in
        olift mapf (tuncoll τ env)
    end.

  Lemma infer_cnraenv_type_correct (τenv τin τout:rtype) (e:cnraenv) :
    infer_cnraenv_type e τ env τin = Some τ out →
    cnraenv_type τ constants e τ env τin τ out.

End TcNRAEnvInfer.