From Coq Require Import Strings.String.
Require Import terms.
Require Import subst.
Require Import equiv.
Require Import subtype.
Require Import context.

(* Given a context, there is a morphism path from τ to τ' *)
Reserved Notation "Γ '|-' σ '~>' τ" (at level 101, σ at next level, τ at next level).

Inductive morphism_path : context -> type_term -> type_term -> Prop :=
  | M_Sub : forall Γ τ τ',
    (τ :<= τ') ->
    (Γ |- τ ~> τ')

  | M_Single : forall Γ h τ τ',
    (context_contains Γ h (type_morph τ τ')) ->
    (Γ |- τ ~> τ')

  | M_Chain : forall Γ τ τ' τ'',
    (Γ |- τ ~> τ') ->
    (Γ |- τ' ~> τ'') ->
    (Γ |- τ ~> τ'')

  | M_Lift : forall Γ σ τ τ',
    (Γ |- τ ~> τ') ->
    (Γ |- (type_ladder σ τ) ~> (type_ladder σ τ'))

  | M_MapSeq : forall Γ τ τ',
    (Γ |- τ ~> τ') ->
    (Γ |- (type_spec (type_id "Seq") τ) ~> (type_spec (type_id "Seq") τ'))

where "Γ '|-' s '~>' t" := (morphism_path Γ s t).


Inductive translate_morphism_path : context -> type_term -> type_term -> expr_term -> Prop :=
  | Translate_Subtype : forall Γ τ τ',
    (τ :<= τ') ->
    (translate_morphism_path Γ τ τ'
        (expr_morph "x" τ (expr_var "x")))

  | Translate_Lift : forall Γ σ τ τ' m,
    (Γ |- τ ~> τ') ->
    (translate_morphism_path Γ τ τ' m) ->
    (translate_morphism_path Γ (type_ladder σ τ) (type_ladder σ τ')
        (expr_morph "x" (type_ladder σ τ)
          (expr_ascend σ (expr_app m (expr_descend τ (expr_var "x"))))))

  | Translate_Single : forall Γ h τ τ',
    (context_contains Γ h (type_morph τ τ')) ->
    (translate_morphism_path Γ τ τ' (expr_var h))

  | Translate_Chain : forall Γ τ τ' τ'' m1 m2,
    (translate_morphism_path Γ τ τ' m1) -> 
    (translate_morphism_path Γ τ' τ'' m2) ->
    (translate_morphism_path Γ τ τ''
      (expr_morph "x" τ (expr_app m2 (expr_app m1 (expr_var "x")))))

  | Translate_MapSeq : forall Γ τ τ' m,
    (translate_morphism_path Γ τ τ' m) ->
    (translate_morphism_path Γ
      (type_spec (type_id "Seq") τ)
      (type_spec (type_id "Seq") τ')
      (expr_morph "xs"
        (type_spec (type_id "Seq") τ)
        (expr_app (expr_app (expr_ty_app (expr_ty_app
          (expr_var "map") τ) τ') m)
          (expr_var "xs"))))
.


Example morphism_paths :
  (ctx_assign "degrees-to-turns" [< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]
    (ctx_assign "turns-to-radians" [< $"Angle"$~$"Turns"$~$"ℝ"$ ->morph $"Angle"$~$"Radians"$~$"ℝ"$ >]
      ctx_empty))

  |- [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Degrees"$~$"ℝ"$> >]
  ~> [< <$"Seq"$ $"Hue"$~$"Angle"$~$"Radians"$~$"ℝ"$> >]
.
Proof.
  intros.
  apply M_MapSeq.
  apply M_Lift.
  apply M_Chain with (τ':=[<$"Angle"$~$"Turns"$~$"ℝ"$>]).
  apply M_Single with (h:="degrees-to-turns"%string).
  apply C_take.
  
  apply M_Single with (h:="turns-to-radians"%string).
  apply C_shuffle.
  apply C_take.
Qed.