(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2025 --  Inria - CNRS - Paris-Saclay University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(********************************************************************)

%{
  open Why3
  open Ptree
  open Mc_ast

  exception Unsupported of string

  let () = Exn_printer.register (fun fmt exn -> match exn with
    | Error -> Format.pp_print_string fmt "syntax error"
    | Unsupported s -> Format.fprintf fmt "unsupported feature: %s" s
    | _ -> raise exn)

  let floc s e = Loc.extract (s,e)
  let mk_id id s e = { id_str = id; id_ats = []; id_loc = floc s e }
  let mk_pat  d s e = { pat_desc  = d; pat_loc  = floc s e }
  let mk_term d s e = { term_desc = d; term_loc = floc s e }
  let mk_expr loc d = { expr_desc = d; expr_loc = loc }
  let mk_stmt loc d = { stmt_desc = d; stmt_loc = loc }
  let postop op loc = { id_str = "__post" ^ op; id_ats = []; id_loc = loc }
  let preop op loc = { id_str = "__pre" ^ op; id_ats = []; id_loc = loc }
  let arrpostop op loc = { id_str = "__arrpost" ^ op; id_ats=[]; id_loc = loc }
  let arrpreop op loc = { id_str = "__arrpre" ^ op; id_ats=[]; id_loc = loc }
  let assignop loc op =
    { id_str = Ident.op_infix op; id_ats = []; id_loc = loc }
  let arr_assignop loc op =
    let s = match op with
      | "+=" -> "__array_add"
      | "-=" -> "__array_sub"
      | "*=" -> "__array_mul"
      | "/=" -> "__array_div"
      | s -> raise (Unsupported ("no such operator " ^ s)) in
    { id_str = s; id_ats = []; id_loc = loc }

  let variant_union v1 v2 = match v1, v2 with
    | _, [] -> v1
    | [], _ -> v2
    | _, ({term_loc = loc},_)::_ -> Loc.errorm ~loc
        "multiple `variant' clauses are not allowed"

  let get_op s e = Qident (mk_id (Ident.op_get "") s e)
  let upd_op s e = Qident (mk_id (Ident.op_update "") s e)

  let empty_spec = {
    sp_pre     = [];    sp_post    = [];  sp_xpost  = [];
    sp_reads   = [];    sp_writes  = [];  sp_alias  = [];
    sp_variant = [];
    sp_checkrw = false; sp_diverge = false; sp_partial = false;
  }

  let spec_union s1 s2 = {
    sp_pre     = s1.sp_pre @ s2.sp_pre;
    sp_post    = s1.sp_post @ s2.sp_post;
    sp_xpost   = s1.sp_xpost @ s2.sp_xpost;
    sp_reads   = s1.sp_reads @ s2.sp_reads;
    sp_writes  = s1.sp_writes @ s2.sp_writes;
    sp_alias   = s1.sp_alias @ s2.sp_alias;
    sp_variant = variant_union s1.sp_variant s2.sp_variant;
    sp_checkrw = s1.sp_checkrw || s2.sp_checkrw;
    sp_diverge = s1.sp_diverge || s2.sp_diverge;
    sp_partial = s1.sp_partial || s2.sp_partial;
  }

  let type_int s e = PTtyapp (Qident (mk_id "int" s e), [])
  let type_array s e =
    let array = Qdot (Qident (mk_id "Array" s e), mk_id "array" s e) in
    PTtyapp (array, [type_int s e])

%}

%token <string> INCLUDE
%token <string> INTEGER
%token <string> STRING
%token <Mc_ast.binop> CMP
%token <string> IDENT
%token IF ELSE RETURN WHILE FOR AND OR NOT
%token BREAK
%token EOF
%token LEFTPAR RIGHTPAR LEFTSQ RIGHTSQ COMMA EQUAL SEMICOLON LBRC RBRC
%token PLUS MINUS TIMES DIV MOD
%token VOID INT
%token PLUSPLUS MINUSMINUS PLUSEQUAL MINUSEQUAL TIMESEQUAL DIVEQUAL
%token AMPERSAND SCANF
(* annotations *)
%token LEMMA AXIOM GOAL COLON
%token INVARIANT VARIANT ASSUME ASSERT CHECK REQUIRES ENSURES LABEL
%token FUNCTION PREDICATE TRUE FALSE
%token ARROW LARROW LRARROW FORALL EXISTS DOT THEN LET IN OLD AT

(* precedences *)

%nonassoc IN
%nonassoc no_else
%nonassoc DOT ELSE
%right ARROW LRARROW
%right OR
%right AND
%nonassoc NOT
%right CMP
%left PLUS MINUS
%left TIMES DIV MOD
%nonassoc unary_minus prec_prefix_op

%start file
(* Transformations entries *)
%start <Why3.Ptree.term> term_eof
%start <Why3.Ptree.term list> term_comma_list_eof
%start <Why3.Ptree.ident list> ident_comma_list_eof

%type <Mc_ast.file> file
%type <Mc_ast.stmt> stmt

%%

file:
| dl=decl* EOF
    { dl }
;

decl:
| include_ { $1 }
| def      { $1 }
| func     { $1 }
| prop     { $1 }

include_:
| f=INCLUDE
  { Dinclude (mk_id f $startpos $endpos) }

func:
| FUNCTION INT id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
  SEMICOLON
  { Dlogic (Some Tint, id, l, None) }
| FUNCTION INT id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
  EQUAL t=term SEMICOLON
  { Dlogic (Some Tint, id, l, Some t) }
| PREDICATE id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
  SEMICOLON
 { Dlogic (None, id, l, None) }
| PREDICATE id=ident LEFTPAR l=separated_list(COMMA, param) RIGHTPAR
  EQUAL t=term SEMICOLON
 { Dlogic (None, id, l, Some t) }

prop:
| LEMMA id=ident COLON t=term SEMICOLON
  { Dprop (Decl.Plemma, id, t) }
| AXIOM id=ident COLON t=term SEMICOLON
  { Dprop (Decl.Paxiom, id, t) }
| GOAL id=ident COLON t=term SEMICOLON
  { Dprop (Decl.Pgoal, id, t) }

def:
| ty=return_type f=ident LEFTPAR x=separated_list(COMMA, param) RIGHTPAR
  sbl=block_with_spec
    { let s, bl = sbl in Dfun (ty, f, x, s, bl) }
;

block_with_spec:
| s=non_empty_spec  bl=block
   { s, bl }
| LBRC s=spec l=list(stmt) RBRC
   { s, mk_stmt (floc $startpos $endpos) (Sblock l) }
;

return_type:
| VOID { Tvoid }
| INT  { Tint }
;

param:
| INT id=ident
   { Tint, id }
| INT id=ident LEFTSQ RIGHTSQ
   { Tarray, id }
;

spec:
| (* epsilon *)  { empty_spec }
| non_empty_spec { $1 }
;

non_empty_spec:
| single_spec                { $1 }
| single_spec non_empty_spec { spec_union $1 $2 }
;

single_spec:
| REQUIRES t=term SEMICOLON
    { { empty_spec with sp_pre = [t] } }
| ENSURES e=ensures SEMICOLON
    { { empty_spec with sp_post = [floc $startpos(e) $endpos(e), e] } }
| variant
    { { empty_spec with sp_variant = $1 } }

ensures:
| term
    { let id = mk_id "result" $startpos $endpos in
      [mk_pat (Pvar id) $startpos $endpos, $1] }

expr:
| d = expr_desc
   { mk_expr (floc $startpos $endpos) d }
;

expr_desc:
| c = INTEGER
    { Eint c }
| s = STRING
    { Estring s }
| id = ident
    { Eident id }
| id=ident op=incdec
    { let loc = floc $startpos $endpos in
      Ecall (postop op loc, [mk_expr loc (Eaddr id)]) }
| op=incdec id=ident
    { let loc = floc $startpos $endpos in
      Ecall (preop op loc, [mk_expr loc (Eaddr id)]) }
| id=ident LEFTSQ e2 = expr RIGHTSQ
    { Eget (mk_expr (floc $startpos(id) $endpos(id)) (Eident id), e2) }
| id=ident LEFTSQ e2 = expr RIGHTSQ op=incdec
    { let loc = floc $startpos $endpos in
      let e1 = mk_expr (floc $startpos(id) $endpos(id)) (Eident id) in
      Ecall (arrpostop op loc, [e1; e2]) }
| op=incdec id=ident LEFTSQ e2 = expr RIGHTSQ
    { let loc = floc $startpos $endpos in
      let e1 = mk_expr (floc $startpos(id) $endpos(id)) (Eident id) in
      Ecall (arrpreop op loc, [e1; e2]) }
| MINUS e1 = expr %prec unary_minus
    { Eunop (Uneg, e1) }
| NOT e1 = expr
    { Eunop (Unot, e1) }
| e1 = expr o = binop e2 = expr
    { Ebinop (o, e1, e2) }
| f = ident LEFTPAR e = separated_list(COMMA, expr) RIGHTPAR
    { Ecall (f, e) }
| SCANF LEFTPAR s=STRING COMMA AMPERSAND id=ident RIGHTPAR
    { if s <> "%d" then raise (Unsupported "scanf is limited to \"%d\"");
      let id = mk_expr (floc $startpos $endpos) (Eaddr id) in
      Ecall (mk_id "scanf" $startpos $endpos, [id]) }
| LEFTPAR e = expr RIGHTPAR
   { e.expr_desc }
;

incdec:
| PLUSPLUS   { "inc" }
| MINUSMINUS { "dec" }
;

%inline binop:
| PLUS  { Badd }
| MINUS { Bsub }
| TIMES { Bmul }
| DIV   { Bdiv }
| MOD   { Bmod }
| c=CMP { c    }
| AND   { Band }
| OR    { Bor  }
;

located(X):
| X { mk_stmt (floc $startpos $endpos) $1 }
;

stmt:
| simple_stmt { $1 }
| block       { $1 }
;

block:
| located(block_desc) { $1 }
;

block_desc:
| LBRC l = list(stmt) RBRC { Sblock l }
;

loop_body:
| a=loop_annotation  s=simple_stmt
  { a, s }
| LBRC a=loop_annotation l=list(stmt) RBRC
  { a, mk_stmt (floc $startpos $endpos) (Sblock l) }
| a=non_empty_loop_annotation LBRC l=list(stmt) RBRC
  { a, mk_stmt (floc $startpos $endpos) (Sblock l) }

loop_annotation:
| (* epsilon *)
    { [], [] }
| non_empty_loop_annotation
   { $1 }
;

non_empty_loop_annotation:
| invariant loop_annotation
    { let (i, v) = $2 in ($1::i, v) }
| variant loop_annotation
    { let (i, v) = $2 in (i, variant_union $1 v) }

invariant:
| INVARIANT i=term SEMICOLON { i }

variant:
| VARIANT l=comma_list1(term) SEMICOLON { List.map (fun t -> t, None) l }

simple_stmt: located(simple_stmt_desc) { $1 };

simple_stmt_desc:
| SEMICOLON
    { Sskip }
| RETURN e = expr SEMICOLON
    { Sreturn e }
| INT id=ident SEMICOLON
    { let any_int = mk_id "any_int" $startpos $endpos in
      let loc = floc $startpos $endpos in
      let e = mk_expr loc (Ecall (any_int, [mk_expr loc Eunit])) in
      Svar (Tint, id, e) }
| INT id=ident LEFTSQ e=expr RIGHTSQ SEMICOLON
    { let alloc_array = mk_id "alloc_array" $startpos $endpos in
      let loc = floc $startpos $endpos in
      let e = mk_expr loc (Ecall (alloc_array, [e])) in
      Svar (Tarray, id, e) }
| k=assertion_kind t = term SEMICOLON
    { Sassert (k, t) }
| BREAK SEMICOLON
    { Sbreak }
| LABEL id=ident SEMICOLON
    { Slabel id }
| IF LEFTPAR c = expr RIGHTPAR s1 = stmt %prec no_else
    { Sif (c, s1, mk_stmt (floc $startpos $endpos) Sskip) }
| IF LEFTPAR c = expr RIGHTPAR s1 = stmt ELSE s2=stmt
    { Sif (c, s1, s2) }
| WHILE LEFTPAR e=expr RIGHTPAR b=loop_body
    { let iv, l = b in Swhile (e, iv, l) }
| FOR LEFTPAR e1=expr_stmt SEMICOLON e=expr SEMICOLON e2=expr_stmt
  RIGHTPAR b=loop_body
   { let loc = floc $startpos $endpos in
     let iv, l = b in
     Sblock [e1;
             mk_stmt loc (Swhile (e, iv, mk_stmt loc (Sblock [l; e2])))]
   }
| s=expr_stmt_desc SEMICOLON
   { s }
;

expr_stmt: located(expr_stmt_desc) { $1 };

expr_stmt_desc:
| INT id=ident EQUAL e = expr
    { Svar (Tint, id, e) }
| id = ident EQUAL e = expr
    { Sassign (id, e) }
| id = ident op=assignop e = expr
    { let loc = floc $startpos $endpos in
      let id = mk_expr loc (Eaddr id) in
      Seval (mk_expr loc (Ecall (assignop loc op, [id; e]))) }
| id=ident LEFTSQ e2 = expr RIGHTSQ EQUAL e3 = expr
    { let e1 = mk_expr (floc $startpos(id) $endpos(id)) (Eident id) in
      Sset (e1, e2, e3) }
| id=ident LEFTSQ e2 = expr RIGHTSQ op=assignop e3 = expr
    { let loc = floc $startpos $endpos in
      let e1 = mk_expr (floc $startpos(id) $endpos(id)) (Eident id) in
      Seval (mk_expr loc (Ecall (arr_assignop loc op, [e1; e2; e3]))) }
| e = expr
    { Seval e }
;

assignop:
| PLUSEQUAL  { "+=" }
| MINUSEQUAL { "-=" }
| TIMESEQUAL { "*=" }
| DIVEQUAL   { "/=" }
;

assertion_kind:
| ASSERT  { Expr.Assert }
| ASSUME  { Expr.Assume }
| CHECK   { Expr.Check }

ident:
  id = IDENT { mk_id id $startpos $endpos }
;

/* logic */

mk_term(X): d = X { mk_term d $startpos $endpos }

term: t = mk_term(term_) { t }

term_:
| term_arg_
    { match $1 with (* break the infix relation chain *)
      | Tinfix (l,o,r) -> Tinnfix (l,o,r)
      | Tbinop (l,o,r) -> Tbinnop (l,o,r)
      | d -> d }
| NOT term
    { Tnot $2 }
| OLD LEFTPAR t=term RIGHTPAR
    { Tat (t, mk_id Dexpr.old_label $startpos($1) $endpos($1)) }
| AT LEFTPAR t=term COMMA l=ident RIGHTPAR
    { Tat (t, l) }
| o = prefix_op ; t = term %prec prec_prefix_op
    { Tidapp (Qident o, [t]) }
| l = term ; o = bin_op ; r = term
    { Tbinop (l, o, r) }
| l = term ; o = infix_op_1 ; r = term
    { Tinfix (l, o, r) }
| l = term ; o = infix_op_234 ; r = term
    { Tidapp (Qident o, [l; r]) }
| IF term THEN term ELSE term
    { Tif ($2, $4, $6) }
| LET id=ident EQUAL t1=term IN t2=term
    { Tlet (id, t1, t2) }
| q=quant l=comma_list1(binder) DOT t=term
    { let var (id, ty) = id.id_loc, Some id, false, Some ty in
      Tquant (q, List.map var l, [], t) }
| id=ident LEFTPAR l=separated_list(COMMA, term) RIGHTPAR
    { Tidapp (Qident id, l) }

quant:
| FORALL  { Dterm.DTforall }
| EXISTS  { Dterm.DTexists }

binder:
| id=ident                { id, type_int   $startpos $endpos }
| id=ident LEFTSQ RIGHTSQ { id, type_array $startpos $endpos }

term_arg: mk_term(term_arg_) { $1 }

term_arg_:
| ident       { Tident (Qident $1) }
| INTEGER     { Tconst (Constant.ConstInt Number.(int_literal ILitDec ~neg:false $1)) }
| TRUE        { Ttrue }
| FALSE       { Tfalse }
| term_sub_                 { $1 }

term_sub_:
| LEFTPAR term RIGHTPAR                             { $2.term_desc }
| term_arg LEFTSQ term RIGHTSQ
    { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
| term_arg LEFTSQ term LARROW term RIGHTSQ
    { Tidapp (upd_op $startpos($2) $endpos($2), [$1;$3;$5]) }

%inline bin_op:
| ARROW   { Dterm.DTimplies }
| LRARROW { Dterm.DTiff }
| OR      { Dterm.DTor }
| AND     { Dterm.DTand }

%inline infix_op_1:
| c=CMP  { let op = match c with
          | Beq  -> "="
          | Bneq -> "<>"
          | Blt  -> "<"
          | Ble  -> "<="
          | Bgt  -> ">"
          | Bge  -> ">="
          | Badd|Bsub|Bmul|Bdiv|Bmod|Band|Bor -> assert false in
           mk_id (Ident.op_infix op) $startpos $endpos }

%inline prefix_op:
| MINUS { mk_id (Ident.op_prefix "-")  $startpos $endpos }

%inline infix_op_234:
| DIV    { mk_id "div" $startpos $endpos }
| MOD    { mk_id "mod" $startpos $endpos }
| PLUS   { mk_id (Ident.op_infix "+") $startpos $endpos }
| MINUS  { mk_id (Ident.op_infix "-") $startpos $endpos }
| TIMES  { mk_id (Ident.op_infix "*") $startpos $endpos }

comma_list1(X):
| separated_nonempty_list(COMMA, X) { $1 }

(* parsing of a single term *)
term_eof:
| term EOF { $1 }

ident_comma_list_eof:
| comma_list1(ident) EOF { $1 }

term_comma_list_eof:
| comma_list1(term) EOF { $1 }