(* Sigmtch.sml *)

open List Fnlib Mixture Const Prim Lambda Globals Units Types;
open Front Back Emit_phr;

(* Signature matching *)

fun lookupSig_TyEnv (sign : CSig) id =
  Hasht.find (#uTyEnv sign) id
  handle Subscript =>
    (msgIBlock 0;
     errPrompt "Type "; msgString id;
     msgString
       " is specified in the signature but not defined in the unit body";
     msgEOL();
     msgEBlock();
     raise Toplevel)
;

fun lookupSig_VarEnv (sign : CSig) id =
  Hasht.find (#uVarEnv sign) id
  handle Subscript =>
    (msgIBlock 0;
     errPrompt "Value "; msgString id;
     msgString
       " is specified in the signature but not defined in the unit body";
     msgEOL();
     msgEBlock();
     raise Toplevel)
;

fun lookupSig_cBas (sign : CSig) id =
  Hasht.find (#uConBasis sign) id
  handle Subscript =>
    (msgIBlock 0;
     errPrompt "Value "; msgString id;
     msgString
       " is specified in the signature but not defined in the unit body";
     msgEOL();
     msgEBlock();
     raise Toplevel)
;

fun errorImplMismatch id =
(
  msgIBlock 0;
  errPrompt "Mismatch between the specification of the value ";
  msgString id; msgEOL();
  errPrompt "in the signature and its implementation in the unit body";
  msgEOL();
  msgEBlock();
  raise Toplevel
);

fun errorConImplMismatch id =
(
  msgIBlock 0;
  errPrompt "Mismatch between the specification of the value constructor ";
  msgString id; msgEOL();
  errPrompt "in the signature and its implementation in the unit body";
  msgEOL();
  msgEBlock();
  raise Toplevel
);

fun errorExConImplMismatch id =
(
  msgIBlock 0;
  errPrompt "Mismatch between the specification of the exception constructor ";
  msgString id; msgEOL();
  errPrompt "in the signature and its implementation in the unit body";
  msgEOL();
  msgEBlock();
  raise Toplevel
);

fun mkTypeFcnOfTyName (tn : TyName) =
  let val vs = newTypeVars (#tnArity (!(#info tn))) in
    TYPEts(vs, type_con (map TypeOfTypeVar vs) tn)
  end
;

fun applyRea (tyname : TyName) ts =
  case #tnStr(!(#info tyname)) of
      NILts => type_con ts tyname
    | TYPEts(pars, body) => fatalError "applyRea"
    | DATATYPEts _ => type_con ts tyname
    | REAts tn =>
        let val arity = List.length ts
            val {info=ref{tnArity, tnStr, ...}, ...} = tn
        in
          if tnArity <> arity then
            fatalError "applyRea"
          else ();
          case tnStr of
              NILts => type_con ts tn
            | TYPEts(pars, body) =>
                type_subst (zip2 pars ts) body
            | DATATYPEts _ => type_con ts tn
            | REAts _ => fatalError "applyRea"
        end
;

fun expandRea UE tau =
  case normType tau of
    VARt var =>
      (lookup var UE
       handle Subscript => fatalError "expandRea: Unknown variable")
  | ARROWt(t,t') =>
      ARROWt(expandRea UE t, expandRea UE t')
  | CONt(ts, tn) =>
      applyRea tn (map (expandRea UE) ts)
  | RECt rt =>
      let val {fields=fs, rho=rho} = !rt in
        RECt (ref{fields=map_fields (expandRea UE) fs, rho=rho})
      end
;

fun newParTypeVar () =
  mkTypeVar false false false 0
;

fun newHardTypeVar () =
  let val tv = mkTypeVar false false false 0 in
    setTvKind tv (Explicit "");
    tv
  end;

fun isTypeFcnEqu vs' tau' vs tau =
  let val ts = map (fn _ => TypeOfTypeVar(newHardTypeVar())) vs
      val UE = zip2 vs ts
      val tau0 = expandRea UE tau
      val UE' = zip2 vs' ts
      val tau'0 = type_subst UE' tau'
  in
    (unify tau'0 tau0; true)
    handle Unify _ => false
  end
;

fun matchDatatype (tyname : TyName) (CE : ConEnv) (CE' : ConEnv) =
  let val domCE  = map (fn gci => #id(#qualid gci)) CE
      val domCE' = map (fn gci => #id(#qualid gci)) CE'
  in
    (* domCE' is non-empty, because `abstype' is not allowed *)
    (* in signatures, and "primitive" types are represented  *)
    (* as NILts. *)
    if domCE <> domCE' then (
      msgIBlock 0;
      errPrompt "Realization mismatch: variant type constructor ";
      msgString (#id (#qualid tyname)); msgEOL();
      errPrompt "has specification and realization that differ"; msgEOL();
      errPrompt "in the names and/or the order of value constructors";
      msgEOL();
      msgEBlock();
      raise Toplevel)
    else ();
    (* We don't have to compare the types of constructors here, *)
    (* because they will be compared as values. Note that all *)
    (* constructors are visible, for redefining values in signatures *)
    (* is not allowed. *)
    ()
  end;

fun refresh0HardTypeVar (var : TypeVar) =
  let val {tvEqu, tvImp, ...} = !var
      val tv = mkTypeVar tvEqu tvImp false 0
  in
    setTvKind tv (Explicit "");
    tv
  end;

fun refresh0TypeVar (var : TypeVar) =
  let val {tvEqu, tvImp, ...} = !var
  in
    mkTypeVar tvEqu tvImp false 0
  end;

fun matchTypeSchemes id infSc specSc =
  let
    val TypeScheme{tscParameters=vs, tscBody=tau} = specSc
    val ts = map (fn v => TypeOfTypeVar(refresh0HardTypeVar v)) vs
    val UE = zip2 vs ts
    val tau0 = expandRea UE tau
    val TypeScheme{tscParameters=vs', tscBody=tau'} = infSc
    val ts' = map (fn v => TypeOfTypeVar(refresh0TypeVar v)) vs'
    val UE' = zip2 vs' ts'
    val tau'0 = type_subst UE' tau'
  in
    unify tau'0 tau0
    handle Unify _ =>
      (let
         val ts = map TypeOfTypeVar vs
         val UE = zip2 vs ts
         val tau0 = expandRea UE tau
       in
         msgIBlock 0;
         errPrompt "Type mismatch: value identifier "; msgString id;
         msgString " in the signature has type"; msgEOL();
         errPrompt "  "; printType tau0; msgEOL();
         errPrompt "whereas its implementation in the unit's body has type";
         msgEOL();
         errPrompt "  "; printScheme infSc; msgEOL();
         msgEBlock();
         raise Toplevel
       end)
  end;

fun realizeTyName (infTyName : TyName) (specTyName : TyName) =
  let val {info=ref infInfo, ...} = infTyName
      val {info=ref specInfo, qualid={id, ...}} = specTyName
  in
    if #tnArity specInfo  <> #tnArity infInfo then (
      msgIBlock 0;
      errPrompt "Arity mismatch: type constructor ";
      msgString id; msgString " is specified as having arity ";
      msgInt (#tnArity specInfo); msgEOL();
      errPrompt "but declared as having arity ";
      msgInt (#tnArity infInfo); msgString " in the unit's body";
      msgEOL();
      msgEBlock();
      raise Toplevel)
    else ();
    case #tnEqu specInfo of
        REFequ =>
          if #tnEqu infInfo <> REFequ then (
            msgIBlock 0;
            errPrompt "Type constructor "; msgString id;
            msgString " is specified as `prim_EQtype',";
            msgEOL();
            errPrompt "but isn't realized as a `prim_EQtype'";
            msgEOL();
            msgEBlock();
            raise Toplevel)
          else ()
      | TRUEequ =>
          if #tnEqu infInfo = FALSEequ then (
            msgIBlock 0;
            errPrompt "Type constructor "; msgString id;
            msgString " is specified as admitting equality,";
            msgEOL();
            errPrompt "but its realization doesn't admit equality";
            msgEOL();
            msgEBlock();
            raise Toplevel)
          else ()
      | FALSEequ =>
          ();
    case #tnStr specInfo of
        NILts => setTnStr (#info specTyName) (REAts infTyName)
      | TYPEts _ => ()
      | DATATYPEts _ => ()
      | REAts _ => fatalError "realizeTyName"
  end;

fun checkRealization (inferredSig : CSig) (specSig : CSig)
                     (infTyName : TyName) (specTyName : TyName) =
  let val {info=ref infInfo, ...} = infTyName
      val {info=ref specInfo, qualid={id, ...}} = specTyName
  in
    case #tnStr specInfo of
        NILts => fatalError "checkRealization"
      | TYPEts(vs, tau) =>
          (case #tnStr infInfo of
               NILts =>
                 (msgIBlock 0;
                  errPrompt "Realization mismatch: type constructor ";
                  msgString id; msgString " is specified"; msgEOL();
                  errPrompt "as a type abbreviation,"; msgEOL();
                  errPrompt "but implemented as a primitive type"; msgEOL();
                  msgEBlock();
                  raise Toplevel)
             | TYPEts(vs', tau') =>
                 if not(isTypeFcnEqu vs' tau' vs tau) then (
                   msgIBlock 0;
                   errPrompt "Realization mismatch: type constructor ";
                   msgString id; msgString " is bound"; msgEOL();
                   errPrompt "to non-equivalent type abbreviations"; msgEOL();
                   errPrompt "in the signature and in the unit body"; msgEOL();
                   msgEBlock();
                   raise Toplevel)
                 else ()
             | DATATYPEts _ =>
                 (msgIBlock 0;
                  errPrompt "Realization mismatch: type constructor ";
                  msgString id; msgString " is specified"; msgEOL();
                  errPrompt "as a type abbreviation,"; msgEOL();
                  errPrompt "but implemented as a variant type"; msgEOL();
                  msgEBlock();
                  raise Toplevel)
             | REAts tn' => fatalError "checkRealization")
      | DATATYPEts dt =>
          let val CE = findConstructors specSig dt in
            case #tnStr infInfo of
                NILts =>
                  (msgIBlock 0;
                   errPrompt "Realization mismatch: type constructor ";
                   msgString id;
                   msgString " is specified as a variant type,"; msgEOL();
                   errPrompt "but implemented as a primitive type"; msgEOL();
                   msgEBlock();
                   raise Toplevel)
              | TYPEts(vs', tau') =>
                  (msgIBlock 0;
                   errPrompt "Realization mismatch: type constructor ";
                   msgString id;
                   msgString " is specified as a variant type,"; msgEOL();
                   errPrompt "but implemented as a type abbreviation"; msgEOL();
                   msgEBlock();
                   raise Toplevel)
              | DATATYPEts dt' =>
                  let val CE' = findConstructors inferredSig dt'
                  in matchDatatype specTyName CE CE' end
              | REAts tn' => fatalError "checkRealization"
          end
      | REAts _ => ()
  end;

fun exportValAsVal os (infStatus : ConStatus) (specStatus : ConStatus) =
  let val lam =
    Lprim(Pset_global (#qualid specStatus, 0),
            [Lprim(Pget_global (#qualid infStatus, 0), [])])
  in emit_phrase os (compileLambda true lam) end
;

fun exportPrimAsVal os (pi : PrimInfo) (specStatus : ConStatus) =
  let val lam =
    Lprim(Pset_global (#qualid specStatus, 0), [trPrimVar (#primOp pi)])
  in emit_phrase os (compileLambda true lam) end
;

fun exportConAsVal os (ci : ConInfo) (specStatus : ConStatus) =
  let val lam =
    Lprim(Pset_global (#qualid specStatus, 0), [trConVar ci])
  in emit_phrase os (compileLambda true lam) end
;

fun exportExConAsVal os (ei : ExConInfo) (specStatus : ConStatus) =
  let val lam =
    Lprim(Pset_global (#qualid specStatus, 0), [trTopExConVar ei])
  in emit_phrase os (compileLambda true lam) end
;

fun checkHomeUnits infQual specQual id thing =
  if specQual <> infQual then (
    msgIBlock 0;
    errPrompt "Specified signature expects the ";
    msgString thing; msgString " ";
    msgString id; msgString " to be defined"; msgEOL();
    errPrompt "in the unit "; msgString specQual;
    msgString " but it is defined in the unit ";
    msgString infQual; msgEOL();
    msgEBlock();
    raise Toplevel)
  else ();
;

fun matchIdStatus os infStatus specStatus =
  let val {qualid=infQualid, info=infInfo} = infStatus
      val {qualid=specQualid, info=specInfo} = specStatus
      val {qual=infQual, ...} = infQualid
      val {qual=specQual, id=id} = specQualid
  in
    case specInfo of
        VARname ovltype =>
          (* checkHomeUnits infQual specQual id "value"; *)
          (case infInfo of
               VARname ovltype' =>
                 (if ovltype <> ovltype' then errorImplMismatch id
                  else ();
                  if specQual <> infQual then
                    exportValAsVal os infStatus specStatus
                  else ())
             | PRIMname pi' =>
                   exportPrimAsVal os pi' specStatus
             | CONname ci' =>
                   exportConAsVal os ci' specStatus
             | EXNname ei' =>
                   exportExConAsVal os ei' specStatus
             | REFname => errorImplMismatch id)
      | PRIMname pi =>
          (* checkHomeUnits infQual specQual id "prim_value"; *)
          (case infInfo of
               VARname ovltype' => errorImplMismatch id
             | PRIMname pi'=>
                 if pi <> pi' then errorImplMismatch id else ()
             | CONname ci' => errorImplMismatch id
             | EXNname ei' => errorImplMismatch id
             | REFname => errorImplMismatch id)
      | CONname ci =>
          (* checkHomeUnits infQual specQual id "value constructor"; *)
          (case infInfo of
               VARname ovltype' => errorImplMismatch id
             | PRIMname pi' => errorImplMismatch id
             | CONname ci' =>
                 if #conArity(!ci) <> #conArity(!ci')
                 orelse #conIsGreedy(!ci) <> #conIsGreedy(!ci')
                 orelse #conTag(!ci) <> #conTag(!ci')
                 orelse #conSpan(!ci) <> #conSpan(!ci')
                 then errorConImplMismatch id
                 else ()
             | EXNname ei' => errorImplMismatch id
             | REFname => errorImplMismatch id)
      | EXNname ei =>
          (checkHomeUnits infQual specQual id "exception";
           case infInfo of
               VARname ovltype' => errorImplMismatch id
             | PRIMname pi' => errorImplMismatch id
             | CONname ci' => errorImplMismatch id
             | EXNname ei' =>
                 if #exconArity(!ei) <> #exconArity(!ei')
                 orelse #exconIsGreedy(!ei) <> #exconIsGreedy(!ei')
                 then errorExConImplMismatch id
                 else ()
             | REFname => errorImplMismatch id)
      | REFname =>
          (case infInfo of
               VARname ovltype' => errorImplMismatch id
             | PRIMname pi' => errorImplMismatch id
             | CONname ci' => errorImplMismatch id
             | EXNname ei' => errorImplMismatch id
             | REFname => ())
  end
;

fun matchStamps (inferredSig : CSig) (specSig : CSig) =
  Hasht.apply
    (fn uname => fn stamp =>
      let val stamp' = Hasht.find (#uMentions inferredSig) uname in
        if stamp' <> stamp then (
          msgIBlock 0;
          errPrompt "The signature of "; msgString uname;
          msgString " has changed, while "; msgString (#uName specSig);
          msgString ".sig depends on it."; msgEOL();
          errPrompt "Please, recompile "; msgString (#uName specSig);
          msgString ".sig, before compiling "; msgString (#uName specSig);
          msgString ".sml."; msgEOL();
          msgEBlock();
          raise Toplevel)
        else ()
      end
      handle Subscript => ())
    (#uMentions specSig)
;

fun matchSignature os (inferredSig : CSig) (specSig : CSig) =
(
  (* Matching stamps of mentioned signatures *)
  matchStamps inferredSig specSig;
  (* Type realization. *)
  Hasht.apply (fn id => fn specTyName =>
      realizeTyName (lookupSig_TyEnv inferredSig id) specTyName)
    (#uTyEnv specSig);
  Hasht.apply (fn id => fn specTyName =>
      checkRealization inferredSig specSig
                       (lookupSig_TyEnv inferredSig id) specTyName)
    (#uTyEnv specSig);
  (* Matching value types *)
  Hasht.apply (fn id => fn specSc =>
      matchTypeSchemes id (lookupSig_VarEnv inferredSig id) specSc)
    (#uVarEnv specSig);
  (* Status matching. *)
  (* This may cause some code to be generated, *)
  (* if a primitive function or a value constructor is *)
  (* exported as a value. *)
  Hasht.apply (fn id => fn specStatus =>
      matchIdStatus os (lookupSig_cBas inferredSig id) specStatus)
    (#uConBasis specSig)
);