Minuska.builtin.list_model

From Minuska Require Import
    prelude
    spec
    model_functor
    list_signature
    model_algebra
    (* model_functor *)
.

Definition list_function_interp
    (InnerT : Type)
    (TermSymbol : Type)
    (NondetValue : Type)
    (Carrier : Type)
    (_WB : Injection bool Carrier)
    (_WI : Injection InnerT Carrier)
    (_WL : Injection (list InnerT) Carrier)
    (asi : Carrier -> option (InnerT))
    (asl : Carrier -> option (list InnerT))
:
    ListFunSymbol ->
    NondetValue ->
    list (@TermOver' TermSymbol Carrier) ->
    option (@TermOver' TermSymbol Carrier)
:=
    fun f nd args =>
    match f with
    | list_nil =>
        match args with
        | [] => Some (t_over (inject (list InnerT) Carrier []))
        | _ => None
        end
    | list_cons =>
        match args with
        | (t_over x1)::(t_over x2)::[] =>
            match (asi x1), (asl x2) with
            | Some v, Some l => Some (t_over (inject (list InnerT) Carrier (v::l)))
            | _, _ => None
            end
        | _ => None
        end
    | list_head =>
        match args with
        | (t_over x1)::[] =>
            match asl x1 with
            | Some [] => None
            | Some (h::_) => Some (t_over (inject InnerT Carrier h))
            | _ => None
            end
        | _ => None
        end
    | list_tail =>
        match args with
        | (t_over x1)::[] =>
            match asl x1 with
            | Some [] => None
            | Some (_::t) => Some (t_over (inject (list InnerT) Carrier t))
            | _ => None
            end
        | _ => None
        end
    | list_is_nil =>
        match args with
        | (t_over x1)::[] =>
            match (asl x1) with
            | Some l => Some (t_over (inject bool Carrier (bool_decide (l = []))))
            | _ => None
            end
        | _ => None
        end
    end
.

Definition list_predicate_interp
    (InnerT : Type)
    (TermSymbol : Type)
    (NondetValue : Type)
    (Carrier : Type)
    (_WB : Injection bool Carrier)
    (_WI : Injection InnerT Carrier)
    (_WL : Injection (list InnerT) Carrier)
    (asi : Carrier -> option (InnerT))
    (asl : Carrier -> option (list InnerT))
:
    ListPredSymbol ->
    NondetValue ->
    list (@TermOver' TermSymbol Carrier) ->
    option bool
:=
    fun p nd args =>
    match p with
    | list_is =>
        match args with
        | (t_over x1)::[] =>
            match (asl x1) with
            | Some _ => Some true
            | _ => Some false
            end
        | _ => None
        end
    end
.

Variant simple_list_carrier (Inner : Type) :=
| slc_inner (x : Inner)
| slc_list (l : list Inner)
.

#[local]
Instance simple_list_carrier__eqdec
    (Inner : Type)
    {_ : EqDecision Inner}
    : EqDecision (simple_list_carrier Inner)
.
Proof.
    ltac1:(solve_decision).
Defined.

#[local]
Program Instance simple_list_carrier__countable
    (Inner : Type)
    {_ : EqDecision Inner}
    {_ : Countable Inner}
    : Countable (simple_list_carrier Inner) := {|
    encode := fun slc =>
        stdpp.countable.encode (
            match slc with
            | slc_inner _ x => inl x
            | slc_list _ l => inr l
            end
        )
    ;
    decode := fun (p : positive) =>
        match (@stdpp.countable.decode (Inner+(list Inner)) _ _ p) with
        | Some (inl x) => Some (slc_inner _ x)
        | Some (inr l) => Some (slc_list _ l)
        | None => None
        end
|}.
Next Obligation.
    rewrite decode_encode.
        ltac1:(repeat case_match; simplify_eq/=);
        reflexivity.
Qed.
Fail Next Obligation.

(* 
    TODO: So far, the output algebra has only predicates and functions of list.
    We need to find a way to add there the original Fs and Ps back.
 *)
Program Definition list_wrapper
        (Vdeps Vours : Type)
        (NV Sy Fs Ps : Type)
        (M : RelaxedValueAlgebra Vdeps Vours NV Sy Fs Ps)
        :
        RelaxedValueAlgebra bool (simple_list_carrier Vours) NV Sy ListFunSymbol ListPredSymbol
:= {|
    rva_over :=
        fun
            (Carrier : Type)
            (inja : Injection (bool) Carrier)
            (injb : ReversibleInjection
                (simple_list_carrier Vours)
                Carrier
            )
        =>
        let asi := (fun c =>
            match (@ri_reverse _ _ injb) c with Some d => (
                match d with
                | slc_inner _ d' => Some d'
                | _ => None
                end
            )
            | None => None end
        ) in
        let asl := (fun c =>
            match (@ri_reverse _ _ injb) c with Some d => (
                match d with
                | slc_list _ d' => Some d'
                | _ => None
                end
            )
            | None => None end
        ) in
        let WL : Injection (list (Vours)) Carrier := {|
            inject := fun l => @inject _ _ (@ri_injection _ _ injb) (slc_list _ l)
        |} in
        let WI := {|
            inject := fun i => @inject _ _ (@ri_injection _ _ injb) (slc_inner _ i)
        |} in
        let WB := {|
            inject := fun b => @inject _ _ inja (b)
        |} in
        {|
            builtin_function_interp := fun (f : list_signature.ListFunSymbol) => list_function_interp Vours Sy NV Carrier WB WI WL asi asl f;
            builtin_predicate_interp := fun (p :list_signature.ListPredSymbol) => list_predicate_interp Vours Sy NV Carrier WB WI WL asi asl p;
        |}
|}
.
Next Obligation.
    apply inject_inj in H.
    ltac1:(injection H as H).
    exact H.
Qed.
Next Obligation.
    apply inject_inj in H.
    ltac1:(injection H as H).
    exact H.
Qed.
Next Obligation.
    apply (inj (inject bool Carrier)) in H.
    exact H.
Qed.
Fail Next Obligation.

About list_wrapper.