(* we assume an `input` variable holding the input,
             an `offset` (mutable) variable holding the current index within the input,
             the `parsers` dictionary of parsing functions for all the user-defined peg used.
   the result of a parsing expression is:
   - an expression holding the value part of the result
   - mutation of the offset variable to advance what we're looking at
   - a new dictionary with any extra needed parsers *)

gen_parse_js : [A]peg A -> map string string (* input parser dictionary *) ->
                           map string string (* output parser dictionary *) ->
                           string (* result expression *) -> prop.

quote_string_js : string -> string -> prop.
quote_term_js : [A]reified A -> string -> prop.

quote_string_js S Res :- tostring S Res.

gen_parse_js anychar Dict Dict Result :-
  expansion.str
  `(offset < input.length
     ? (JSON.stringify(input[offset++]))
     : null)`
  Result.

gen_parse_js (charclass S) Dict Dict Result :-
  quote_string_js S S_js,
  expansion.str
  `((offset < input.length && ${S_js}.includes(input[offset]))
     ? JSON.stringify(input[offset++])
     : null)`
  Result.

gen_parse_js (exact S) Dict Dict Result :-
  if (refl.isconst S) then quote_string_js S S_js
  else (reify S S_R, quote_term_js S_R S_js', expansion.str `JSON.parse(\`${S_js'}\`)` S_js),
  expansion.str
  `(input.startsWith(${S_js}, offset)
    ? (offset += ${S_js}.length, JSON.stringify(${S_js}))
    : null)`
  Result.

gen_parse_js (neg P) Dict Dict' Result :-
  gen_parse_js P Dict Dict' Code,
  expansion.str
  `(yield* (function*() {
     const keepOffset = offset;
     const result = ${Code};
     offset = keepOffset;
     return (result === null ? "unit" : null);
  })())`
  Result.

gen_parse_js (lookahead P) Dict Dict' Result :-
  gen_parse_js P Dict Dict' Code,
  expansion.str
  `(yield* (function*() {
     const keepOffset = offset;
     const result = ${Code};
     offset = keepOffset;
     return (result === null ? null : "unit");
  })())`
  Result.

gen_parse_js empty Dict Dict Result :-
  expansion.str `"unit"` Result.

gen_parse_js void Dict Dict "null".

(* now on to the more difficult ones *)

quote_parse_res_js : [A]A -> string -> prop.

parse_res_counter : fluid int.
`( fluid.set parse_res_counter 0 ).

gen_parse_js (bind (P : peg A) (F : A -> peg B)) Dict Dict'' Result :-
  gen_parse_js P Dict Dict' Code,
  fluid.get parse_res_counter I,
  tostring I IS,
  expansion.str `result_${IS}` Name,
  fluid.inc parse_res_counter {prop|
    (a:A -> quote_parse_res_js a Name ->
      (gen_parse_js (F a) Dict' Dict'' Code')) |},
  expansion.str
  `(yield* (function*() {
     const keepOffset = offset;
     const ${Name} = ${Code};
     if (${Name} === null) {
       offset = keepOffset;
       return null;
     } else {
       const result = ${Code'};
       if (result === null) {
         offset = keepOffset;
         return null;
       } else return result;
     }
   })())`
  Result.

gen_parse_js (seq A B) Dict Dict'' Result :-
  gen_parse_js A Dict Dict' CodeA,
  gen_parse_js B Dict' Dict'' CodeB,
  expansion.str
  `(yield* (function*() {
     const keepOffset = offset;
     const result = ${CodeA};
     if (result === null) {
       offset = keepOffset;
       return null;
     } else {
       const result = ${CodeB};
       if (result === null) {
         offset = keepOffset;
         return null;
       } else return result;
     }
   })())`
  Result.

gen_parse_js (choices PS) Dict Dict' Result :-
  foldl (pfun cur p next => [DictCur CodeCur DictNext CodeNext CodeP]
    eq cur (DictCur, CodeCur),
    eq next (DictNext, CodeNext),
    gen_parse_js p DictCur DictNext CodeP,
    expansion.str
    `${CodeCur}
     {
       offset = keepOffset;
       const result = ${CodeP};
       if (result !== null) return result;
     }`
    CodeNext) (Dict, "") PS (Dict', Blocks),
  expansion.str
  `(yield* (function*() {
     const keepOffset = offset;
     ${Blocks}
     offset = keepOffset;
     return null;
   })())`
  Result.

gen_parse_js (many P) Dict Dict' Result :-
  gen_parse_js P Dict Dict' Code,
  expansion.str
  `(yield* (function*() {
     let result = [];
     while (true) {
       const current = ${Code};
       if (current === null) break;
       else result.push(current);
     }
     return \`[\${result.join(", ")}]\`;
   })())`
  Result.

gen_parse_js (assume Clause P) Dict Dict' Result :-
  assume Clause (gen_parse_js P Dict Dict' Result).

quote_terms_js : [A B]reified_args A B -> string -> prop.

quote_terms_js X Result
  when refl.isunif X, log_error X `Uninstantiated reified arguments`.

quote_terms_js [] "".
quote_terms_js (Head :: Tail) Result :-
  quote_term_js Head HeadS,
  quote_terms_js Tail TailS,
  expansion.str ` ${HeadS}${TailS}` Result.

quote_paren_term_js : string -> string -> string -> prop.

quote_paren_term_js HeadS ArgsS Result :-
  if (eq ArgsS "")
  then eq Result HeadS
  else expansion.str `(${HeadS}${ArgsS})` Result.

quote_term_js (reified.term Head Args) Result :-
  tostring_qualified Head HeadS,
  quote_terms_js Args ArgsS,
  quote_paren_term_js HeadS ArgsS Result.

quote_term_js (reified.const (S : string)) S_js :-
  quote_string_js S S_quoted,
  string.explode S_quoted S_quoted',
  map (pfun char res =>
    if eq char "\\"
    then eq res "\\\\"
    else (if eq char "`"
    then eq res "\\`"
    else eq res char)) S_quoted' S_quoted'',
  string.explode S_js S_quoted''.

quote_term_js (reified.const (I : int)) I_js :-
  tostring I I_js.

(* here we need to antiquote the result of `P` *)
quote_term_js (reified.nvar P Args) Result :-
  quote_parse_res_js P PRes,
  quote_terms_js Args ArgsS,
  expansion.str `\${${PRes}}` HeadS,
  quote_paren_term_js HeadS ArgsS Result.

quote_var_js : [A]A -> string -> prop.

quote_var_counter : fluid int.
`( fluid.set quote_var_counter 0 ).

quote_term_js (reified.bvar X Args) Result :-
  quote_var_js X Var,
  quote_terms_js Args ArgsS,
  quote_paren_term_js Var ArgsS Result.

quote_term_js (reified.lambda (F : A -> B)) Result :-
  fluid.get quote_var_counter I,
  tostring I VarI,
  expansion.str `x_${VarI}` Var,
  fluid.inc quote_var_counter {prop|
  (x:A -> quote_var_js x Var -> (
     quote_term_js (F x) Body,
     (* TODO: investigate if it's better to add this always. *)
     if (refl.monotyp x, refl.typstring x Typ) then
       expansion.str `(${Var}: ${Typ})` Binder
     else
       eq Var Binder)) |},
  expansion.str `(fun ${Binder} => ${Body})` Result.

(* TODO: decide if and how unification variables will be supported. *)

gen_parse_js (action X) Dict Dict Result :-
  reify X X_Reified,
  quote_term_js X_Reified X_js,
  expansion.str `\`${X_js}\`` Result.

key_of_var : [A] peg A -> string -> prop.
key_of : [A] peg A -> string -> prop.

key_of P Key :-
  if (key_of_var P Key) then success
  else (reify P P_R, quote_term_js P_R Key).

gather_used_results, gather_used_results_aux : [A] set string -> A -> set string -> prop.

gather_used_results S R S' :-
  demand.case_otherwise (gather_used_results_aux S R S')
                        (generic.fold @gather_used_results S R S').

gather_used_results_aux S X S' when refl.isnvar X, quote_parse_res_js X PRes :-
  set.ccons PRes S S'.

quote_used_results_js : [A] peg A -> string -> prop.
quote_used_results_js P DictKeys :-
  gather_used_results [] P UsedResultsSet,
  if (eq UsedResultsSet []) then eq DictKeys ""
  else (
    set.to_list UsedResultsSet UsedResults,
    map (pfun x => eq [",", x]) UsedResults UsedResults',
    concat UsedResults' (_ :: UsedResults''),
    string.concat UsedResults'' DictKeys
  ).

(* external parsers are defined using `extern_def` rules.
   the parser should be of the form `(input: string, offset: int) => { result: ?string, newOffset: int }`
*)

gen_parse_js P Dict Dict' Result
  when not(builtin P), not(refl.isunif P), external P, key_of P Key :-
  quote_used_results_js P Args_js,
  quote_string_js Key Parser_key,
  if (map.find Dict Key _)
  then (eq Dict' Dict)
  else (
  get_external_peg_definition P Code,
  eq Dict' ((Key, Expr) :: Dict),
  expansion.str
    `(function*(args) {
      const { ${Args_js} } = args;
      const memoEntry = \`${Key}\`;
      const historyEntry = \`${Key}:\${offset}\`;
      const keepOffset = offset;
      if (history.includes(historyEntry)) {
        throw new Error(\`left recursion found: adding \${historyEntry} to \${history}\`);
      }
      if (memoEntry in memoize && memoize[memoEntry][keepOffset] !== undefined) {
        const { result, newOffset } = memoize[memoEntry][keepOffset];
        offset = newOffset;
        return result;
      } else {
        let historyCopy = history.slice();
        history.push(historyEntry);
        const data = (function (input, offset) { return (${Code})(input, offset); })(input, offset);
        if (data.result !== null) offset = data.newOffset;
        if (!(memoEntry in memoize)) memoize[memoEntry] = {};
        memoize[memoEntry][keepOffset] = {
          result: data.result,
          newOffset: data.result === null ? keepOffset : data.newOffset
         };
        history = historyCopy;
        return data.result;
      }
     })`
     Expr),
  expansion.str
  `yield { parser: ${Parser_key}, args: { ${Args_js} } }`
  Result.

gen_parse_js P Dict Dict' Result
  when not(builtin P), not(refl.isunif P), inline P, not(external P) :-
  get_peg_definition P P',
  gen_parse_js P' Dict Dict' Result.

gen_parse_js P Dict DictRes Result
  when not(builtin P), not(refl.isunif P), not(inline P), not(external P) :-
  key_of P Key,
  quote_used_results_js P Args_js,
  quote_string_js Key Parser_key,
  if (map.find Dict Key _)
  then (eq DictRes Dict)
  else (
    get_peg_definition P P',
    eq Dict' ((Key, Expr) :: Dict),
    gen_parse_js P' Dict' DictRes Code,
    expansion.str
    `(function*(args) {
      const { ${Args_js} } = args;
      const memoEntry = \`${Key}\`;
      const historyEntry = \`${Key}:\${offset}\`;
      const keepOffset = offset;
      if (history.includes(historyEntry)) {
        throw new Error(\`left recursion found: adding \${historyEntry} to \${history}\`);
      }
      if (memoEntry in memoize && memoize[memoEntry][keepOffset] !== undefined) {
        const { result, newOffset } = memoize[memoEntry][keepOffset];
        offset = newOffset;
        return result;
      } else {
        let historyCopy = history.slice();
        history.push(historyEntry);
        const result = ${Code};
        if (result === null) offset = keepOffset;
        if (!(memoEntry in memoize)) memoize[memoEntry] = {};
        memoize[memoEntry][keepOffset] = { result, newOffset: offset };
        history = historyCopy;
        return result;
      }
     })`
     Expr
  ),
  expansion.str
  `yield { parser: ${Parser_key}, args: { ${Args_js} } }`
  Result.

gen_dictionary_js_aux : map string string -> string -> prop.
gen_dictionary_js : map string string -> string -> prop.

gen_dictionary_js_aux Map "" when map.empty Map.

gen_dictionary_js_aux Map Result when map.headtail Map Key Value_js Map' :-
  gen_dictionary_js_aux Map' Result',
  quote_string_js Key Key_js,
  expansion.str
  `${Key_js}: ${Value_js},
   ${Result'}`
  Result.

gen_dictionary_js Map Result :-
  gen_dictionary_js_aux Map Entries_js,
  expansion.str `{
    ${Entries_js}
  }` Result.

(* Since every Makam type is encoded as a string while in JavaScript parsing land,
   this is a cast to make sure that we can quote the result of a parse inside
   an expansion, regardless of its type. *)
result : [A]A -> string.

(* Similarly, if the result (represented as a string) makes sense in JavaScript as a term,
   then we can use `jsresult` to parse it into a JavaScript value. For example, this
   would convert a quoted string into a string and a quoted number into a number. *)
jsresult : [A]A -> string.

quote_expansion_js : list (reified string) -> list (reified string) -> prop.

quote_expansion_js [] [].

quote_expansion_js (HD :: TL) (reified.const (S' : string) :: TL') :-
  if (eq HD (reified.const (S : string))) then
    (eq S' S)
  else
    (if (eq HD (reified.term result [X]))
     then (quote_term_js X HD', expansion.str `\`${HD'}\`` S')
     else (if (eq HD (reified.term jsresult [X]))
     then (quote_term_js X HD', expansion.str `JSON.parse(\`${HD'}\`)` S')
     else (quote_term_js HD HD', expansion.str `\`${HD'}\`` S'))),
  quote_expansion_js TL TL'.

gen_parse_js Eval Dict Dict Result
  when (eq Eval (eval (expansion X)); eq Eval (eval _ (expansion X))) :-
  map reify X X_Reified,
  quote_expansion_js X_Reified X_Reified',
  map reflect X_Reified' X',
  expansion.str (expansion X') X_js,
  expansion.str `(function(){${X_js}})()` Result.

gen_toplevel_parser_js : [A] peg A -> string -> prop.
gen_toplevel_parser_js P Function_js :-
  gen_parse_js P [] Dict Code,
  gen_dictionary_js Dict Dict_js,
  expansion.str
  `(function (input, startOffset) {
      let offset = startOffset;
      const parsers = ${Dict_js};
      const memoize = {};
      let history = [];
      const firstGen = (function*() { return ${Code}; })();
      const recurseOrResult = [ { gen: firstGen, val: firstGen.next() } ];
      let lastRes;
      while (recurseOrResult.length > 0) {
        const { gen: genTop, val: valTop } = recurseOrResult[recurseOrResult.length-1];
        if (valTop.done) {
          lastRes = valTop.value;
          recurseOrResult.pop();
          if (recurseOrResult.length > 0) {
            const { gen, val } = recurseOrResult[recurseOrResult.length - 1];
            recurseOrResult[recurseOrResult.length - 1] = { gen, val: gen.next(lastRes) };
          }
        } else {
          const nextGen = parsers[valTop.value.parser](valTop.value.args);
          recurseOrResult.push( {gen: nextGen, val: nextGen.next() } );
        }
      }
      if (lastRes === null) {
        return { result: null, newOffset: startOffset };
      } else {
        return { result: lastRes, newOffset: offset };
      }
   })`
   Function_js.

eval_parser_js : [A] peg A -> string -> string -> (A * string) -> prop.

eval_parser_js P Function_js Input Result :-
  quote_string_js Input Input_js,
  expansion.str
  `(function(){
      const input = ${Input_js};
      const { result, newOffset } = ${Function_js}(input, 0);
      if (result === null) return "none";
      else return \`some( \${result}, \${JSON.stringify(input.substr(newOffset))} )\`;
  })();`
  FinalCode,
  js.eval FinalCode ResultS,
  refl.fromstring ResultS (some Result).

generated_toplevel_parser_js : [A] string -> peg A -> string -> prop.

gen_toplevel_parser_js_cached : [A] peg A -> string -> prop.
gen_toplevel_parser_js_cached P Code :-
  persistent_cache.predicate (gen_toplevel_parser_js P) Code.

def_toplevel_parser_js : [A]peg A -> cmd -> prop.
def_toplevel_parser_js P (cmd_newclause (clause (generated_toplevel_parser_js Typ P Code) success)) :-
  (* this does not play well with polymorphism, so we require a monomorphic type.
     we can have different instantiations of the same polymorphic constant though,
     hence we store a representation of the type as part of the cached predicate. *)
  refl.monotyp P, refl.typstring P Typ,
  gen_toplevel_parser_js_cached P Code.

def_parser_js : [A]peg A -> peg A -> cmd -> prop.
def_parser_js P P' (cmd_many [ cmd_newclause (clause (external P) success),
                               cmd_newclause (clause (extern_def P Code) success) ]) :-
  refl.monotyp P, refl.typstring P Typ,
  gen_toplevel_parser_js_cached P' Code.

parse_opt : [A] peg A -> string -> (A * string) -> prop.

parse_opt P Input Result :-
  if (refl.isunif(P)) then
    (locget P Loc,
     tostring Loc LocS,
     print_string `-- At ${LocS}, using parse_opt with uninstantiated PEG.\n`,
     failure)
  else success,
  if (refl.monotyp P, refl.typstring P Typ, generated_toplevel_parser_js Typ P Function_js)
  then success
  else gen_toplevel_parser_js P Function_js,
  eval_parser_js P Function_js Input Result.


%extend peg_list.
mapi_aux : [AS](int -> A -> prop) -> int -> peg_list AS -> list A -> prop.
mapi : [AS](int -> A -> prop) -> peg_list AS -> list A -> prop.
assume_many : [AS]forall A (peg A -> B -> prop) -> peg_list AS -> list B -> prop -> prop.

mapi_aux P I [] [].
mapi_aux P I (HD :: TL) (HD' :: TL') :-
  P I HD', plus I 1 I', mapi_aux P I' TL TL'.

mapi P X Y :- mapi_aux P 0 X Y.

assume_many P [] [] Q :- Q.
assume_many P (HD :: TL) (HD' :: TL') Q :- instantiate P P', (P' HD HD' -> assume_many P TL TL' Q).
%end.

gen_parse_js (letrec DefsBody) Dict Dict' Code :-
  map.raw_length Dict I0,
  peg_list.open DefsBody (pfun ps defsBody => [Defs Body]
    eq defsBody (Defs, Body),
    peg_list.mapi (pfun i res => [I0S IS]
      (tostring I0 I0S, tostring i IS,
       expansion.str `~rec_${I0S}_${IS}` res)) Defs Keys,
    peg_list.assume_many @rule ps Defs (
      peg_list.assume_many @key_of_var ps Keys (
        gen_parse_js Body Dict Dict' Code))).