%{
  open Fol
  let parse_error s =
    let st = Parsing.symbol_start_pos ()
    and en = Parsing.symbol_end_pos ()  in
    failwith ("Syntax error at surat " ^ string_of_int st.Lexing.pos_lnum ^ ":" ^ string_of_int (st.Lexing.pos_cnum - st.Lexing.pos_bol) ^ " - " ^ string_of_int en.Lexing.pos_lnum ^ ":" ^ string_of_int (en.Lexing.pos_cnum - en.Lexing.pos_bol) ^ " : " ^ s)
    
%}

%token <Fol.ident> IDENT

%token PLUS MOINS PLUSPLUS INTER FLECHE CROCHETG CROCHETD RESTD RESTG POINT TILDE PARG PARD UNIV IDEN NONE BARRE IF THEN ELSE LET VIRGULE EQ OR IMPLIES AND NOT SOME NO LONE ONE IN ALL ACCG ACCD DP SET DIV SIG ABSTRACT EXTENDS PRED FUN FACT ASSERT CHECK RUN OPEN MODULE EXACTLY FOR BUT INT LT GT EOF

%type <(token Fol.env -> token Fol.env)> modul
%start modul


%%

relation:
| relation0 { $1 }
;

relation_nl:
| relation0nl { $1 }
;

relation0:
| relation05 { $1 }
| relation0nl PLUS relation05 { fun e -> plus ($1 e) ($3 e) }
| relation0nl MOINS relation05 { fun e -> moins ($1 e) ($3 e) }
;

relation0nl:
| relation05nl { $1 }
| relation0nl PLUS relation05nl { fun e -> plus ($1 e) ($3 e) }
| relation0nl MOINS relation05nl { fun e -> moins ($1 e) ($3 e) }
;

relation05:
| relation1 { $1 }
| relation05nl PLUSPLUS relation1 { fun e -> plusplus ($1 e) ($3 e) }
;

relation05nl:
| relation1nl { $1 }
| relation05nl PLUSPLUS relation1nl { fun e -> plusplus ($1 e) ($3 e) }
;

relation1:
| relation2 { $1 }
| relation1nl INTER relation2 { fun e -> inter ($1 e) ($3 e) }
;

relation1nl:
| relation2nl { $1 }
| relation1nl INTER relation2nl { fun e -> inter ($1 e) ($3 e) }
;

relation2:
| relation3 { $1 }
| relation2nl FLECHE relation3 { fun e -> fleche ($1 e) ($3 e) }
;

relation2nl:
| relation3nl { $1 }
| relation2nl FLECHE relation3nl { fun e -> fleche ($1 e) ($3 e) }
;

relation3:
| relation4 { $1 }
| relation3nl CROCHETG relation CROCHETD { fun e -> jointure ($3 e) ($1 e) }
;

relation3nl:
| relation4nl { $1 }
| relation3nl CROCHETG relation CROCHETD { fun e -> jointure ($3 e) ($1 e) }
;

relation4:
| relation5 { $1 }
| relation4nl RESTD relation5 { fun e -> restriction_droite ($1 e) ($3 e) }
;

relation4nl:
| relation5nl { $1 }
| relation4nl RESTD relation5nl { fun e -> restriction_droite ($1 e) ($3 e) }
;

relation5:
| relation6 { $1 }
| relation5nl RESTG relation6 { fun e -> restriction_gauche ($1 e) ($3 e) }
;

relation5nl:
| relation6nl { $1 }
| relation5nl RESTG relation6nl { fun e -> restriction_gauche ($1 e) ($3 e) }
;

relation6:
| relation7 { $1 }
| relation6nl POINT relation7 { fun e -> jointure ($1 e) ($3 e) }
;

relation6nl:
| relation7nl { $1 }
| relation6nl POINT relation7nl { fun e -> jointure ($1 e) ($3 e) }
;

relation7:
| relation8 { $1 }
| TILDE relation7 { fun e -> tilde ($2 e) }
;

relation7nl:
| relation8nl { $1 }
| TILDE relation7nl { fun e -> tilde ($2 e) }
;

relation8:
| PARG relation PARD { $2 }
| IDENT arg_seq2 { fun e -> appel_fonction $1 ($2 e) e }
| IDENT { appel_relation $1 }
| UNIV { fun _ -> univ }
| IDEN { fun _ -> iden }
| NONE { fun _ -> none }
| affectation BARRE relation { fun e -> $3 ($1 e) }
| IF formule THEN relation ELSE relation { fun e -> si_relation ($2 e) ($4 e) ($6 e) }
| error { parse_error "relation8" }
;

relation8nl:
| PARG relation PARD { $2 }
| IDENT arg_seq2 { fun e -> appel_fonction $1 ($2 e) e }
| IDENT { appel_relation $1 }
| UNIV { fun _ -> univ }
| IDEN { fun _ -> iden }
| NONE { fun _ -> none }
| error { parse_error "relation8n1" }
;

affectation:
| LET affectation_liste { $2 }
;

affectation_liste:
| affectation_element { $1 }
| affectation_element VIRGULE affectation_liste {
    fun e -> $3 ($1 e)
  }
| error { parse_error "affectation_liste" }
;

affectation_element:
| IDENT EQ relation {
    fun e -> { e with
      env_rels = (fun nom -> if nom = $1 then Some ($3 e) else e.env_rels nom)
      }
  }
;

formule:
| formule0 { $1 }
;

formule0:
| formule1 { $1 }
| formule_disjonction { fun e -> `Disjunction ($1 e) }
;

formule0nl:
| formule1nl { $1 }
| formule_disjonction_nl { fun e -> `Disjunction ($1 e) }
;

formule_disjonction_nl:
| formule1nl OR formule1nl { fun e -> [$1 e; $3 e] }
| formule1nl OR formule_disjonction_nl {fun e -> (($1 e)::($3 e))}
;

formule_disjonction:
| formule1nl OR formule1 { fun e -> [$1 e; $3 e] }
| formule1nl OR formule_disjonction {fun e -> (($1 e)::($3 e))}
;

formule1:
| formule2 { $1 }
| formule2nl IMPLIES formule1 { fun e -> implication ($1 e) ($3 e) }
//| formule2nl IMPLIES formule2nl els formule1 { fun e -> `Conjunction [
//    implication ($1 e) ($3 e);
//    implication (`Negation ($1 e)) ($5 e);
//  ]}
;

formule1nl:
| formule2nl { $1 }
| formule2nl IMPLIES formule1nl { fun e -> implication ($1 e) ($3 e) }
// | formule2nl IMPLIES formule2nl els formule1nl { fun e -> si_formule ($1 e) ($3 e) ($5 e) }
;

els:
| ELSE { () }
| VIRGULE { () }
;

formule2:
| formule3 { $1 }
| formule_conjonction { fun e -> `Conjunction ($1 e) }
;

formule2nl:
| formule3nl { $1 }
| formule_conjonction_nl { fun e -> `Conjunction ($1 e) }
;

formule_conjonction:
| formule3nl AND formule3 { fun e -> [$1 e; $3 e]}
| formule3nl AND formule_conjonction { fun e -> (($1 e)::($3 e)) }
;

formule_conjonction_nl:
| formule3nl AND formule3nl { fun e -> [$1 e; $3 e]}
| formule3nl AND formule_conjonction_nl { fun e -> (($1 e)::($3 e)) }
;

formule3:
| formule4 { $1 }
| NOT formule3 { fun e -> `Negation ($2 e) }
;

formule3nl:
| formule4nl { $1 }
| NOT formule3nl { fun e -> `Negation ($2 e) }
;

formule4:
| PARG formule PARD { $2 }
| formule_seq { $1 }
| IDENT arg_seq { fun e -> appel_predicat $1 ($2 e) e }
| SOME relation { fun e -> mult_some ($2 e) }
| NO relation { fun e -> mult_no ($2 e) }
| LONE relation { fun e -> mult_lone ($2 e) }
| ONE relation { fun e -> mult_one ($2 e) }
| relation_nl IN relation { fun e -> inclusion ($1 e) ($3 e) }
// | relation_nl NOT IN relation { fun e -> negation (inclusion ($1 e) ($4 e)) }
| relation_nl EQ relation { fun e -> egalite ($1 e) ($3 e) }
| ALL varlist_quant formule_corps { fun e -> quant_forall ($2 e) $3 e }
| SOME varlist_quant formule_corps { fun e -> quant_exists ($2 e) $3 e }
| NO varlist_quant formule_corps { fun e -> `Negation (quant_exists ($2 e) $3 e) }
| affectation formule_corps { fun e -> $2 ($1 e) }
//| error { parse_error "formule4" }
;

formule4nl:
| PARG formule PARD { $2 }
| formule_seq { $1 }
| IDENT arg_seq { fun e -> appel_predicat $1 ($2 e) e }
| SOME relation_nl { fun e -> mult_some ($2 e) }
| NO relation_nl { fun e -> mult_no ($2 e) }
| LONE relation_nl { fun e -> mult_lone ($2 e) }
| ONE relation_nl { fun e -> mult_one ($2 e) }
| relation_nl IN relation_nl { fun e -> inclusion ($1 e) ($3 e) }
// | relation_nl NOT IN relation_nl { fun e -> negation (inclusion ($1 e) ($4 e)) }
| relation_nl EQ relation_nl { fun e -> egalite ($1 e) ($3 e) }
//| error { parse_error "formule4nl" }
; 

formule_corps:
| BARRE formule { $2 }
| formule_seq { $1 }
;

formule_seq:
| ACCG formule_liste ACCD { fun e -> `Conjunction ($2 e) }
;

formule_liste:
| { fun _ -> [] }
| formule formule_liste { fun e -> (($1 e)::($2 e)) }
;

varlist_quant:
| varlist_quant0 { fun e -> fst ($1 e) }
;

varlist_quant0:
| IDENT DP relation { fun e -> let r = $3 e in ([ $1, r ], r) }
| IDENT DP relation VIRGULE varlist_quant0 { fun e ->
    let r = $3 e in (($1, r)::(fst ($5 e)) ,r)
  }
| IDENT VIRGULE varlist_quant0 { fun e ->
    let l, r = $3 e in (($1, r)::l, r)
  }
//| IDENT PV varlist_quant0 {
//    let l, r = $3 e in (($1, r)::l, r)
//  }

;

arg_seq:
| PARG PARD { fun _ -> [] }
| PARG arg_liste PARD { $2 }
;

arg_seq2:
| LT GT { fun _ -> [] }
| LT arg_liste GT { $2 }
;

arg_liste:
| relation { fun e -> [$1 e] }
| relation VIRGULE arg_liste { fun e -> (($1 e)::($3 e)) }
;

param_seq:
| PARG PARD { [] }
| PARG param_liste PARD { $2 }
;

param_liste:
| param { [$1] }
| param VIRGULE param_liste { $1 :: $3 }
| IDENT VIRGULE param_liste { $1 :: $3 }
;

param:
| IDENT DP IDENT { $1 }
| IDENT DP SET IDENT { $1 }
| IDENT DP typefleche { $1 }
;

typefleche:
| IDENT FLECHE IDENT { [$1; $3] }
| IDENT FLECHE typefleche { $1 :: $3 }
;

reldef_seq:
| ACCG reldef_liste ACCD { fst $2 }
;

reldef_liste:
| { ([], []), ([], false) }
| reldef { let (id, ty) as rel, est_fonct = $1 in (([rel], (if est_fonct then [id] else [])), (ty, est_fonct)) }
| IDENT VIRGULE reldef_liste {
    let (rels, foncts), ((dernier_type, est_fonct) as c) = $3 in
    (($1, dernier_type)::rels, if est_fonct then $1::foncts else foncts),
    c
  }
| reldef VIRGULE reldef_liste {
    let (rels, foncts), _ = $3 in
    let (((id, ty) as rel), est_fonct) = $1 in
    ((rel::rels, if est_fonct then id::foncts else foncts), (ty, est_fonct))
  }
;

reldef:
| IDENT DP IDENT { (($1, [$3]), true) }
| IDENT DP SET IDENT { (($1, [$4]), false) }
| IDENT DP typefleche { (($1, $3), false) }
;

chemin:
| IDENT DIV chemin { let queue, nom = $3 in ($1 :: queue, nom) }
| IDENT { [], $1 }
;

instruction:
| ABSTRACT SIG IDENT reldef_seq { sig_master $3 true $4 }
| ABSTRACT SIG IDENT EXTENDS IDENT reldef_seq { sig_extends $3 $5 true $6 }
| SIG IDENT reldef_seq { sig_master $2 false $3 }
| SIG IDENT EXTENDS IDENT reldef_seq { sig_extends $2 $4 false $5 }
| SIG IDENT IN relation reldef_seq { fun e -> sig_in $2 ($4 e) $5 e }
| PRED IDENT param_seq formule_seq { predicat $2 $3 $4 }
| FUN IDENT param_seq DP relation ACCG relation ACCD { fonction $2 $3 $7 }
| FACT formule_seq { axiome "<unnamed fact>" $2 }
| FACT IDENT formule_seq { axiome $2 $3 }
| ASSERT IDENT formule_seq { theoreme $2 $3 }
| check { fun e -> (
    prerr_endline "Check or run statement : ignored"; 
    e 
  ) } 
| OPEN chemin { process_module $2 }
| error { parse_error "instruction" }
; 

check_mot:
| CHECK { () }
| RUN { () }
;

check:
| check_mot IDENT { () }
| check_mot IDENT FOR scope { () }
;

scope:
| INT { () }
| INT BUT scope_precis { () }
| scope_precis { () }
;

scope_precis:
| scope_precis_elem { () }
| scope_precis_elem VIRGULE scope_precis { () }
;

scope_precis_elem:
| INT IDENT { () }
| EXACTLY INT IDENT { () }
;

modul0:
| { fun e -> (
    prerr_endline "Reached end of file";
    e) }
| instruction  modul0 { fun e -> $2 ($1 e) }
//| instruction { $1 }
;

moduledecl:
| MODULE chemin {
    let _, nom = $2 in
    fun e -> (
    prerr_endline ("Module: " ^ nom);
    {e with env_modulenames = nom :: e.env_modulenames}
  ) }
;

modul:
| moduledecl modul0 EOF { fun e -> $2 ($1 e) }
;