include "basics/types.ma".
include "basics/logic.ma".
include "basics/lists/list.ma".
include "common/PreIdentifiers.ma".
include "basics/russell.ma".
include "utilities/monad.ma".
include "utilities/option.ma".

(* * Error reporting and the error monad. *)

(* * * Representation of error messages. *)

(* * Compile-time errors produce an error message, represented in Coq
  as a list of either substrings or positive numbers encoding
  a source-level identifier (see module AST). *)

inductive errcode: Type[0] :=
  | MSG: String → errcode
  | CTX: ∀tag:String. identifier tag → errcode.

definition errmsg: Type[0] ≝ list errcode.

definition msg : String → errmsg ≝ λs. [MSG s].

(* * * The error monad *)

(* * Compilation functions that can fail have return type [res A].
  The return value is either [OK res] to indicate success,
  or [Error msg] to indicate failure. *)

(* Paolo: not using except for backward compatbility
  (would break Error ? msg) *)

inductive res (A: Type[0]) : Type[0] ≝
| OK: A → res A
| Error: errmsg → res A.

(*Implicit Arguments Error [A].*)

definition Res ≝ MakeMonadProps
  (* the monad *)
  res
  (* return *)
  (λX.OK X)
  (* bind *)
  (λX,Y,m,f. match m with [ OK x ⇒ f x | Error msg ⇒ Error ? msg])
  ????.
//
[(* bind_ret *)
 #X*normalize //
|(* bind_bind *)
 #X#Y#Z*normalize //
| normalize #X #Y * normalize /2/
]
qed.

include "hints_declaration.ma".
alias symbol "hint_decl" (instance 1) = "hint_decl_Type1".
unification hint 0 ≔ X;
N ≟ max_def Res
(*---------------*) ⊢
res X ≡ monad N X
.

(*(* Dependent pair version. *)
notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ mk_Sig ${ident v} ${ident p} ⇒ ${e'} ]) }.

lemma Prod_extensionality:
  ∀a, b: Type[0].
  ∀p: a × b.
    p = 〈fst … p, snd … p〉.
  #a #b #p //
qed.

definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
λA,B,C,P,e,f.
  match e with
  [ OK v ⇒ match v with [ mk_Sig v' p ⇒ f (fst … v') (snd … v') ? ]
  | Error msg ⇒ Error ? msg
  ].
  <(Prod_extensionality A B v')
  assumption
qed.

notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).*)

lemma bind_inversion:
  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
  (f »= g = return y) →
  ∃x. (f = return x) ∧ (g x = return y).
#A #B #f #g #y cases f normalize 
[ #a #e %{a} /2 by conj/
| #m #H destruct (H)
] qed.

lemma bind2_inversion:
  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: A → B → res C. ∀z: C.
  m_bind2 ???? f g = return z →
  ∃x. ∃y. f = return 〈x, y〉 ∧ g x y = return z.
#A #B #C #f #g #z cases f normalize
[ * #a #b normalize #e %{a} %{b} /2 by conj/
| #m #H destruct (H)
] qed. 

(*
Open Local Scope error_monad_scope.*)

(*
lemma mmap_inversion:
  ∀A, B: Type[0]. ∀f: A -> res B. ∀l: list A. ∀l': list B.
  mmap A B f l = OK ? l' →
  list_forall2 (fun x y => f x = OK y) l l'.
Proof.
  induction l; simpl; intros.
  inversion_clear H. constructor.
  destruct (bind_inversion _ _ H) as [hd' [P Q]].
  destruct (bind_inversion _ _ Q) as [tl' [R S]].
  inversion_clear S.
  constructor. auto. auto. 
Qed.
*)

(* A monadic fold_lefti *)
let rec mfold_left_i_aux (A: Type[0]) (B: Type[0])
                        (f: nat → A → B → res A) (x: res A) (i: nat) (l: list B) on l ≝
  match l with
    [ nil ⇒ x
    | cons hd tl ⇒
       ! x ← x ;
       mfold_left_i_aux A B f (f i x hd) (S i) tl
    ].

definition mfold_left_i ≝ λA,B,f,x. mfold_left_i_aux A B f x O.


(* A monadic fold_left2 *)

axiom WrongLength: String.

let rec mfold_left2
  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → res A) (accu: res A)
  (left: list B) (right: list C) on left: res A ≝
  match left with
  [ nil ⇒
    match right with
    [ nil ⇒ accu
    | cons hd tl ⇒ Error ? (msg WrongLength)
    ]
  | cons hd tl ⇒
    match right with
    [ nil ⇒ Error ? (msg WrongLength)
    | cons hd' tl' ⇒
       ! accu ← accu;
       mfold_left2 … f (f accu hd hd') tl tl'
    ]
  ].

(*
(** * Reasoning over monadic computations *)

(** The [monadInv H] tactic below simplifies hypotheses of the form
<<
        H: (do x <- a; b) = OK res
>>
    By definition of the bind operation, both computations [a] and
    [b] must succeed for their composition to succeed.  The tactic
    therefore generates the following hypotheses:

         x: ...
        H1: a = OK x
        H2: b x = OK res
*)

Ltac monadInv1 H :=
  match type of H with
  | (OK _ = OK _) =>
      inversion H; clear H; try subst
  | (Error _ = OK _) =>
      discriminate
  | (bind ?F ?G = OK ?X) =>
      let x := fresh "x" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind_inversion F G H) as [x [EQ1 EQ2]];
      clear H;
      try (monadInv1 EQ2))))
  | (bind2 ?F ?G = OK ?X) =>
      let x1 := fresh "x" in (
      let x2 := fresh "x" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
      destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
      clear H;
      try (monadInv1 EQ2)))))
  | (mmap ?F ?L = OK ?M) =>
      generalize (mmap_inversion F L H); intro
  end.

Ltac monadInv H :=
  match type of H with
  | (OK _ = OK _) => monadInv1 H
  | (Error _ = OK _) => monadInv1 H
  | (bind ?F ?G = OK ?X) => monadInv1 H
  | (bind2 ?F ?G = OK ?X) => monadInv1 H
  | (?F _ _ _ _ _ _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  | (?F _ = OK _) => 
      ((progress simpl in H) || unfold F in H); monadInv1 H
  end.
*)


definition opt_to_res ≝ λA.λmsg.λv:option A. match v with [ None ⇒ Error A msg | Some v ⇒ OK A v ].
lemma opt_OK: ∀A,m,P,e.
  (∀v. e = Some ? v → P v) →
  match opt_to_res A m e with [ Error _ ⇒ True | OK v ⇒ P v ].
#A #m #P #e elim e; /2/;
qed.

lemma opt_eq_from_res : ∀T,m,e,v.
  opt_to_res T m e = return v →
  e = Some T v.
#T #m * [ #v #E normalize in E; destruct | #e' #v #E normalize in E; destruct % ]
qed.

coercion opt_eq_from_res :
  ∀T,m,e,v. ∀E:opt_to_res T m e = return v. e = Some T v ≝ opt_eq_from_res
  on _E:eq (res ?) ?? to eq (option ?) ??.

(* A variation of bind and its notation that provides an equality proof for
   later use. *)

definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
  match f return λx. f = x → ? with
  [ OK x ⇒ g x
  | Error msg ⇒ λ_. Error ? msg
  ] (refl ? f).

notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 48 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.

definition bind2_eq ≝ λA,B,C:Type[0]. λf: res (A×B). λg: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C.
  match f return λx. f = x → ? with
  [ OK x ⇒ match x return λx. f = OK ? x → ? with [ mk_Prod a b ⇒ g a b ]
  | Error msg ⇒ λ_. Error ? msg
  ] (refl ? f).

notation > "vbox('do' 〈ident v1, ident v2〉 'as' ident E ← e; break e')" with precedence 48 for @{ bind2_eq ??? ${e} (λ${ident v1}.λ${ident v2}.λ${ident E}.${e'})}.

definition res_to_opt : ∀A:Type[0]. res A → option A ≝
 λA.λv. match v with [ Error _ ⇒ None ? | OK v ⇒ Some … v].

(* aliases for backward compatibility *)
definition bind ≝ m_bind Res.
definition bind2 ≝ m_bind2 Res.
definition bind3 ≝ m_bind3 Res.
definition mmap ≝ m_list_map Res.
definition mmap_sigma ≝ m_list_map_sigma Res.