/*        Hierarchy Builder: algebraic hierarchies made easy
    This software is released under the terms of the MIT license              */

% This file contains proxies for the API to write into the Coq state (eg add
% an inductive, set implicit arguments...). This has two purposes:
% - give nicer error messages
% - we want to be able to log to a file all these actions (WIP), this file is
%   were logging takes place. Hence we never call, say, coq.evn.add-* directly,
%   but always via this proxy

namespace log.coq {

pred arguments.set-implicit i:gref, i:list (list implicit_kind).
arguments.set-implicit GR I :-  std.do! [
  coq.arguments.set-implicit GR I,
  if (@local!) (Local = tt) (Local = ff),
  log.private.log-vernac (log.private.coq.vernac.implicit Local {coq.gref->id GR} I),
].

pred env.add-location i:gref.
env.add-location GR :-
  if (get-option "elpi.loc" Loc) % remove when coq-elpi > 1.9
     (acc-clause library (decl-location GR Loc))
     true.

pred strategy.set i:list constant, i:conversion_strategy.
strategy.set CL S :-
  coq.strategy.set CL S,
  log.private.log-vernac (log.private.coq.vernac.strategy CL S).

pred env.add-const-noimplicits i:id, i:term, i:term, i:opaque?, o:constant.
env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [
  if (not(ground_term Ty ; ground_term Bo))
    (coq.error "HB: cannot infer some information in" Name
               ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
    true,
  avoid-name-collision Name Name1,
  coq.env.add-const Name1 Bo Ty Opaque C,
  env.add-location (const C),
  if (var Ty) (Ty? = none) (Ty? = some Ty),
  log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
  @local! => arguments.set-implicit (const C) [[]],
].

pred env.add-const i:id, i:term, i:term, i:opaque?, o:constant.
env.add-const Name Bo Ty Opaque C :- std.do! [
  if (not(ground_term Ty ; ground_term Bo))
    (coq.error "HB: cannot infer some information in" Name
               ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
    true,
  avoid-name-collision Name Name1,
  coq.env.add-const Name1 Bo Ty Opaque C,
  env.add-location (const C),
  if (var Ty) (Ty? = none) (Ty? = some Ty),
  log.private.log-vernac (log.private.coq.vernac.definition Name1 Ty? Bo),
].

pred env.add-const-noimplicits-failondup i:id, i:term, i:term, i:opaque?, o:constant.
env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
  if (not(ground_term Ty ; ground_term Bo))
    (coq.error "HB: cannot infer some information in" Name
               ":" {coq.term->string Ty} ":=" {coq.term->string Bo})
    true,
  coq.env.add-const Name Bo Ty Opaque C,
  env.add-location (const C),
  if (var Ty) (Ty? = none) (Ty? = some Ty),
  log.private.log-vernac (log.private.coq.vernac.definition Name Ty? Bo),
  @local! => arguments.set-implicit (const C) [[]],
].

pred env.add-parameter i:id, i:term, o:constant.
env.add-parameter ID Ty C :- std.do! [
  @global! => coq.env.add-axiom ID Ty C,
  log.private.log-vernac (log.private.coq.vernac.parameter ID Ty),
].

pred env.add-indt i:indt-decl, o:inductive.
env.add-indt Decl I :- std.do! [
  if (not(coq.ground-indt-decl? Decl))
    (coq.error "HB: cannot infer some information in" {coq.indt-decl->string Decl})
    true,
  coq.env.add-indt Decl I,
  (coq.env.record? I P ; P = ff),
  log.private.log-vernac (log.private.coq.vernac.inductive Decl P),
  env.add-location (indt I),

  % copy the current value of implicit arguments
  coq.env.indt I _ _ _ _ KS _,
  log.private.log-implicits-of ff (indt I),
  std.forall KS (k\ env.add-location (indc k), log.private.log-implicits-of ff (indc k)),
  std.forall {coq.env.projections I}
    (p\ sigma c\ if (p = some c) (env.add-location (const c), log.private.log-implicits-of ff (const c)) true),
].

pred env.begin-module i:id, i:option (pair modtypath id).
env.begin-module Name none :- std.do! [
  coq.env.begin-module Name none,
  log.private.log-vernac (log.private.coq.vernac.begin-module Name none),
].
env.begin-module Name (some (pr Sig SigName)) :- std.do! [
  coq.env.begin-module Name (some Sig),
  log.private.log-vernac (log.private.coq.vernac.begin-module Name (some SigName)),
].

pred env.begin-module-type i:id.
env.begin-module-type Name :- std.do! [
  coq.env.begin-module-type Name,
  log.private.log-vernac (log.private.coq.vernac.begin-module-type Name),
].

pred env.end-module-name i:id, o:modpath.
env.end-module-name Name M :- std.do! [
  coq.env.end-module M,
  log.private.log-vernac (log.private.coq.vernac.end-module Name),
].
pred env.end-module-type-name i:id, o:modtypath.
env.end-module-type-name Name M :- std.do! [
  coq.env.end-module-type M,
  log.private.log-vernac (log.private.coq.vernac.end-module-type Name),
].

pred env.begin-section i:id.
env.begin-section Name :- std.do! [
  coq.env.begin-section Name,
  log.private.log-vernac (log.private.coq.vernac.begin-section Name),
].

pred env.end-section-name i:id.
env.end-section-name Name :- std.do! [
  coq.env.end-section,
  log.private.log-vernac (log.private.coq.vernac.end-section Name),
].

pred notation.add-abbreviation i:id, i:int, i:term, i:bool, o:abbreviation.
notation.add-abbreviation Name NArgs Body OnlyParsing O :- std.do! [
  coq.notation.add-abbreviation Name NArgs Body OnlyParsing O,
  log.private.log-vernac (log.private.coq.vernac.abbreviation Name NArgs Body),
].

pred env.export-module i:id, i:modpath.
env.export-module MPNice M :- std.do! [
  coq.env.export-module M,
  log.private.log-vernac (log.private.coq.vernac.export-module MPNice),
].

pred env.import-module i:id, i:modpath.
env.import-module MPNice M :- std.do! [
  coq.env.import-module M,
  log.private.log-vernac (log.private.coq.vernac.import-module MPNice),
].

pred coercion.declare i:coercion.
coercion.declare C :- std.do! [
  @global! => @reversible! => coq.coercion.declare C,
  C = coercion GR _ SRCGR TGTCL,
  coq.gref->id GR Name,
  log.private.log-vernac (log.private.coq.vernac.coercion Name SRCGR TGTCL),
]. 


}

% Since CS.foo is not a valid predicate name we can't use it
% in the namespace, so we just define it here with the full name
pred log.coq.CS.declare-instance i:constant.
log.coq.CS.declare-instance C  :- std.do! [
  if (@local!) (Local = tt) (Local = ff),
  coq.CS.declare-instance (const C),
  coq.gref->id (const C) Id,
  std.last {coq.gref->path (const C)} M,
  std.last {coq.env.current-path} M1,
  if (M = M1) (Name = Id) (Name is M ^ "." ^ Id),
  log.private.log-vernac (log.private.coq.vernac.canonical Name Local),
].

pred log.coq.check i:term, o:term, o:term, o:diagnostic.
log.coq.check Skel Ty T D :- std.do! [
  coq.elaborate-skeleton Skel Ty T D,
  if (get-option "fail" tt) (Fail = tt) (Fail = ff),
  log.private.log-vernac (log.private.coq.vernac.check Skel Fail),
].

pred refine i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics
pred log.refine i:term, i:goal, o:list sealed-goal.
log.refine T G GL :- std.do! [
  refine T G GL,
  G = goal _ _ _ Solution _,
  log.private.log-tactic Solution,
].
pred refine.no_check i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics
pred log.refine.no_check i:term, i:goal, o:list sealed-goal.
log.refine.no_check T G GL :- std.do! [
  refine.no_check T G GL,
  G = goal _ _ _ Solution _,
  log.private.log-tactic Solution,
].


namespace log.private {

%%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred log-implicits-of i:bool, i:gref.
log-implicits-of Local GR :-
  coq.arguments.implicit GR I,
  if (std.forall I (i\ std.forall i (x\ x = explicit))) (IMP = [[]]) (IMP = I),
  log.private.log-vernac (log.private.coq.vernac.implicit Local {coq.gref->id GR} IMP).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Coq document

% This is a very minimalistic AST to represent a Coq document equipped with
% pretty printing facilities.
%
% When "complete enough" this should be moved to coq-elpi proper.

kind coq.vernac type.
type coq.vernac.begin-module  string -> option string       -> coq.vernac.
type coq.vernac.end-module    string                        -> coq.vernac.
type coq.vernac.begin-module-type string                    -> coq.vernac.
type coq.vernac.end-module-type   string                    -> coq.vernac.
type coq.vernac.begin-section string                        -> coq.vernac.
type coq.vernac.end-section   string                        -> coq.vernac.
type coq.vernac.import-module string                        -> coq.vernac.
type coq.vernac.export-module string                        -> coq.vernac.
type coq.vernac.definition    string -> option term -> term -> coq.vernac.
type coq.vernac.variable      string -> term                -> coq.vernac.
type coq.vernac.parameter     string -> term                -> coq.vernac.
type coq.vernac.inductive     indt-decl -> bool             -> coq.vernac.
type coq.vernac.abbreviation  string -> int -> term         -> coq.vernac.
type coq.vernac.notation      string -> int -> term         -> coq.vernac.
type coq.vernac.coercion      string -> gref -> class       -> coq.vernac.
type coq.vernac.canonical     string -> bool                -> coq.vernac.
type coq.vernac.implicit      bool -> string -> list (list implicit_kind)  -> coq.vernac.
type coq.vernac.comment       A                             -> coq.vernac.
type coq.vernac.check         term -> bool                  -> coq.vernac.
type coq.vernac.strategy      list constant -> conversion_strategy -> coq.vernac.

}

pred with-logging i:prop.
pred log.private.log-vernac i:log.private.coq.vernac.
pred log.private.log-tactic i:term.

/*        Hierarchy Builder: algebraic hierarchies made easy
    This software is released under the terms of the MIT license              */

% implementation of logging and vernac printing

with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !,
  get-option "elpi.loc" Loc,
  loc.fields Loc FILE Start Stop _ _,
  LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop},
  FILENAME is FILE ^ ".hb",
  open_append FILENAME OC1,
  std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1,
  output OC1 PATCH1,
  close_out OC1,
  (log.private.logger L NICE => P),
  log.private.logger-close L,
  std.intersperse coq.pp.spc L PP,
  coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S,
  open_append FILENAME OC2,
  output OC2 S,
  close_out OC2.
with-logging P :- (get-option "log" tt, NICE = tt ; get-option "log.raw" tt, NICE = ff), !,
  (log.private.logger L NICE => P),
  log.private.logger-close L,
  std.intersperse coq.pp.spc L PP,
  coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S,
  coq.say "(* \n" S "\n*)".
with-logging P :- P.

log.private.log-vernac V :- log.private.logger L Nice, !,
  if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]),
  log.private.logger-extend L {PPALL => log.private.coq.vernac->pp [V]}.
log.private.log-vernac _.

log.private.log-tactic P :- log.private.logger L Nice, !,
  if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]),
  log.private.logger-extend L {PPALL => @holes! => coq.term->pp P}.
log.private.log-tactic _.

% The main entry point to print vernacular commands is coq.vernac->pp

shorten log.private.coq.vernac.{ begin-module , end-module , begin-section, end-section }.
shorten log.private.coq.vernac.{ begin-module-type , end-module-type }.
shorten log.private.coq.vernac.{ import-module , export-module }.
shorten log.private.coq.vernac.{ definition , variable , comment , check }.
shorten log.private.coq.{ vernac.inductive , vernac.implicit , vernac.parameter }.
shorten log.private.coq.vernac.{ canonical , abbreviation , notation , coercion , strategy }.
shorten log.private.{ coq.vernac }.
shorten coq.pp.{ box , h , spc , v , str , hv , hov, glue, brk }.

namespace log.private {

pred logger o:list coq.pp, o:bool.

pred logger-extend i:list coq.pp, i:coq.pp.
logger-extend [] _ :- coq.error "HB: logger was closed".
logger-extend (uvar as X) V :- X = [V|FRESH_].
logger-extend [_|XS] V :- logger-extend XS V.

pred logger-close i:list coq.pp.
logger-close (uvar as X) :- X = [].
logger-close [_|XS] :- logger-close XS.

pred coq.vernac->pp i:list coq.vernac, o:coq.pp.
coq.vernac->pp L (box (v 0) L2) :-
  std.map L coq.vernac->pp1 L1,
  std.intersperse spc L1 L2.

pred coq.vernac->pp1 i:coq.vernac, o:coq.pp.
coq.vernac->pp1 (begin-module Name none) PP :-
  PP = box h [str "Module ", str Name, str "."].
coq.vernac->pp1 (begin-module Name (some TyName)) PP :-
  PP = box h [str "Module ", str Name, str " : ", str TyName, str "."].
coq.vernac->pp1 (end-module Name) PP :-
  PP = box h [str "End ", str Name, str "."].
coq.vernac->pp1 (begin-module-type Name) PP :-
  PP = box h [str "Module Type ", str Name, str "."].
coq.vernac->pp1 (end-module-type Name) PP :-
  PP = box h [str "End ", str Name, str "."].
coq.vernac->pp1 (begin-section Name) PP :-
  PP = box h [str "Section ", str Name, str "."].
coq.vernac->pp1 (end-section Name) PP :-
  PP = box h [str "End ", str Name, str "."].
coq.vernac->pp1 (definition Name none Body) PP :-
  PP = box (hv 2) [str "Definition ", str Name, str " :=", spc, B, str "."],
  coq.term->pp Body B.
coq.vernac->pp1 (definition Name (some Ty) Body) PP :-
  PP = box (hv 2) [str "Definition ", str Name, str " : ", T, str " :=", spc, B, str "."],
  coq.term->pp Ty T,
  coq.term->pp Body B.
coq.vernac->pp1 (variable Name Ty) (box (hv 2) [box h [str "Variable ", str Name, str " :"], spc, TY, str "."]) :-
  coq.term->pp Ty TY.
coq.vernac->pp1 (vernac.parameter Name Ty) (box (hv 2) [box h [str "Parameter ", str Name, str " :"], spc, TY, str "."]) :-
  coq.term->pp Ty TY.
coq.vernac->pp1 (import-module Name) (box h [str "Import ", str Name, str "."]).
coq.vernac->pp1 (export-module Name) (box h [str "Export ", str Name, str "."]).
coq.vernac->pp1 (notation KM NParams Term) (box (hv 2) [box h [str "Notation \"'",str KM,str"' "|StrParams], str "\" := (", spc, B, str ") (at level 1)."]) :- !,
  coq.vernac->ppabbrterm NParams Term StrParams B.
coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notation ",str Name|StrParams], str " := (", spc, B, str ")."]) :-
  coq.vernac->ppabbrterm NParams Term StrParams B.
coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :-
  local->locality Local Locality.
coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :-
  coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC},
  if2 (TGT = sortclass) (T = "Sortclass")
      (TGT = funclass)  (T = "Funclass")
                        (TGT = grefclass GR, coq.gref->path GR GRP, std.string.concat "." {std.take-last 2 GRP} T', T is T' ^ "." ^ {coq.gref->id GR}).
coq.vernac->pp1 (vernac.inductive I Primitive) (glue [str Start, PP, str Stop]) :-
  coq.vernac->ppinductive I [] PP,
  if (Primitive = tt)
     (Start = "Set Primitive Projections. ", Stop = "Unset Primitive Projections. ")
     (Start = "", Stop = "").
coq.vernac->pp1 (vernac.implicit Local Name [[]]) (box h [Locality, str "Arguments ", str Name, str " : clear implicits."]) :- local->locality Local Locality.
coq.vernac->pp1 (vernac.implicit Local Name [L]) (box h [Locality, str "Arguments ", str Name, spc, glue PP, str "."]) :-
  local->locality Local Locality,
  std.map L coq.vernac->ppimparg PP1,
  std.intersperse spc PP1 PP.
coq.vernac->pp1 (comment A) (box (hov 2) [str"(*", str S, str"*)"]) :-
  std.any->string A S.
coq.vernac->pp1 (check T Fail) (box (hov 2) [Failure, str"Check", spc, PPT, str"."]) :-
  (@holes! => coq.term->pp T PPT),
  fail->failure Fail Failure.
coq.vernac->pp1 (strategy L opaque) (box (hov 2) [str"Strategy opaque [", glue PPL , str"]."]) :-
  std.map L (c\r\sigma id\coq.gref->id (const c) id, r = str id) LID, std.intersperse spc LID PPL.
coq.vernac->pp1 (strategy L expand) (box (hov 2) [str"Strategy expand [", glue PPL , str"]."]) :-
  std.map L (c\r\sigma id\coq.gref->id (const c) id, r = str id) LID, std.intersperse spc LID PPL.
coq.vernac->pp1 (strategy L (level N)) (box (hov 2) [str"Strategy ",str NPP,str" [", glue PPL , str"]."]) :-
  std.any->string N NPP,
  std.map L (c\r\sigma id\coq.gref->id (const c) id, r = str id) LID, std.intersperse spc LID PPL.

pred local->locality i:bool, o:coq.pp.
local->locality tt (str "Local ").
local->locality ff (str "Global ").

pred fail->failure i:bool, o:coq.pp.
fail->failure tt (str "Fail ").
fail->failure ff (str "").

pred coq.vernac->ppimparg i:implicit_kind, o:coq.pp.
coq.vernac->ppimparg explicit (str "_").
coq.vernac->ppimparg maximal  (str "{_}").
coq.vernac->ppimparg implicit (str "[_]").

pred coq.vernac->ppinductive i:indt-decl, i:list (pair implicit_kind term), o:coq.pp.
coq.vernac->ppinductive (parameter ID IMPL TY I) Acc R :-
  @pi-parameter ID TY p\ coq.vernac->ppinductive (I p) [pr IMPL p|Acc] R.
coq.vernac->ppinductive (record ID SORT KID RD) ParamsRev (box (v 0) [Hack1, PP, Hack2]) :-
  PP = (box (hov 0) [
         box (hov 0) [str "Record", spc, str ID, brk 1 4, glue ParamsPP,
                      str " : ", SortPP, brk 1 2, str":= ", str KID],
         brk 1 2,
         box (hv 2) [str"{", spc, glue FieldsPP, str"}"],
         str"."]),
  Hack1 = glue [str "Section ", str ID, str ".", spc,
                str "Local Unset Implicit Arguments.", spc],
  Hack2 = glue [spc, str "End ", str ID, str".", spc],
  std.rev ParamsRev Params,
  coq.vernac->ppinductiveparams Params ParamsPP,
  coq.term->pp SORT SortPP,
  coq.vernac->pprecordfields RD FieldsPP.
coq.vernac->ppinductive (inductive ID IsInd Arity Ks) ParamsRev PP :-
  PP = (box (hov 0) [
         str CO,str "Inductive", spc,
         box (hov 0) [
           str ID, brk 1 4, glue ParamsPP, ArityPP, str " :="],
         brk 0 2,
         box (hv 2) [str"  ", glue KsPp],
         str "."]),
  std.rev ParamsRev Params,
  coq.vernac->ppinductiveparams Params ParamsPP,
  std.map Params snd ParamsAsArgs,
  if (IsInd = tt) (CO = "") (CO = "Co"),
  coq.arity->pp Arity ArityPP,
  @pi-inductive ID Arity x\
    coq.mk-app x ParamsAsArgs (X x),
    coq.vernac->ppinductiveconstructor (Ks (X x)) KsPp.

pred coq.vernac->ppinductiveconstructor i:list indc-decl, o:list coq.pp.
coq.vernac->ppinductiveconstructor [] [].
coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :-
  PP = [str ID,{coq.arity->pp Arity},SEP|Rest],
  if (Ks = []) (SEP = str"") (SEP = glue [brk 1 0, str "| "]),
  coq.vernac->ppinductiveconstructor Ks Rest.

pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp.
coq.vernac->ppinductiveparams [] [].
coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :-
  PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest],
  coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY,
  if2 (Imp = explicit) (A = "(", B = ")")
      (Imp = maximal)  (A = "{", B = "}")
                       (A = "[", B = "]"),
  coq.vernac->ppinductiveparams Rest PPRest.

pred coq.vernac->pprecordfields i:record-decl, o:list coq.pp. 
coq.vernac->pprecordfields end-record [].
coq.vernac->pprecordfields (field _ ID TY F) [ str ID, str " : ", TYPP, str ";", spc|FPP] :- % TODO attributes
  coq.term->pp TY TYPP,
  @pi-parameter ID TY p\ coq.vernac->pprecordfields (F p) FPP.

pred coq.vernac->ppabbrterm i:int, i:term, o:list coq.pp, o:coq.pp.
coq.vernac->ppabbrterm 0 T [] B :- !, @holes! => coq.term->pp T B.
coq.vernac->ppabbrterm N (fun _ _ F) [spc,str ID|StrParams] B :-
  ID is "X" ^ {std.any->string N},
  coq.id->name ID Name,
  M is N - 1,
  @pi-decl Name (sort prop) x\ coq.vernac->ppabbrterm M (F x) StrParams B.

}