%{
  open Symb
  open Alloyast
  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 <Symb.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 EXPECTS

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


%%

relation:
| relation0 { $1 }
;

relation_nl:
| relation0nl { $1 }
;

relation0:
| relation05 { $1 }
| relation0nl PLUS relation05 { `Plus (None, ($1, $3)) }
| relation0nl MOINS relation05 { `Moins (None, ($1, $3)) }
;

relation0nl:
| relation05nl { $1 }
| relation0nl PLUS relation05nl { `Plus (None, ($1, $3)) }
| relation0nl MOINS relation05nl { `Moins (None, ($1, $3)) }
;

relation05:
| relation1 { $1 }
// | relation05nl PLUSPLUS relation1 { `Plusplus (None, ($1, $3)) }
;

relation05nl:
| relation1nl { $1 }
// | relation05nl PLUSPLUS relation1nl { `Plusplus (None, ($1, $3)) }
;

relation1:
| relation2 { $1 }
| relation1nl INTER relation2 { `Inter (None, ($1, $3)) }
;

relation1nl:
| relation2nl { $1 }
| relation1nl INTER relation2nl { `Inter (None, ($1, $3)) }
;

relation2:
| relation3 { $1 }
| relation2nl FLECHE relation3 { `Fleche (None, ($1, $3)) }
;

relation2nl:
| relation3nl { $1 }
| relation2nl FLECHE relation3nl { `Fleche (None, ($1, $3)) }
;

relation3:
| relation4 { $1 }
| relation3nl CROCHETG relation CROCHETD { `Jointure (None, ($3, $1)) }
;

relation3nl:
| relation4nl { $1 }
| relation3nl CROCHETG relation CROCHETD { `Jointure (None, ($3, $1)) }
;

relation4:
| relation5 { $1 }
| relation4nl RESTD relation5 { `Restriction_droite (None, ($1, $3)) }
;

relation4nl:
| relation5nl { $1 }
| relation4nl RESTD relation5nl { `Restriction_droite (None, ($1, $3)) }
;

relation5:
| relation6 { $1 }
| relation5nl RESTG relation6 { `Restriction_gauche (None, ($1, $3)) }
;

relation5nl:
| relation6nl { $1 }
| relation5nl RESTG relation6nl { `Restriction_gauche (None, ($1, $3)) }
;

relation6:
| relation7 { $1 }
| relation6nl POINT relation7 { `Jointure (None, ($1, $3)) }
;

relation6nl:
| relation7nl { $1 }
| relation6nl POINT relation7nl { `Jointure (None, ($1, $3)) }
;

relation7:
| relation8 { $1 }
| TILDE relation7 { `Tilde $2 }
;

relation7nl:
| relation8nl { $1 }
| TILDE relation7nl { `Tilde $2 }
;

relation8:
| PARG relation PARD { $2 }
| IDENT arg_seq2 { `Fonction ($1, $2) }
| IDENT { `Variable $1 }
| UNIV { `Univ }
| IDEN { `Iden }
| NONE { `None }
| affectation BARRE relation { affecte_rel $1 $3 }
// | IF formule THEN relation ELSE relation {
//    `Si ($2, ($4, $6))
//  }
| error { parse_error "relation8" }
;

relation8nl:
| PARG relation PARD { $2 }
| IDENT arg_seq2 { `Fonction ($1, $2) }
| IDENT { `Variable $1 }
| UNIV { `Univ }
| IDEN { `Iden }
| NONE { `None }
| error { parse_error "relation8n1" }
;

affectation:
| LET affectation_liste { $2 }
;

affectation_liste:
| affectation_element { [ $1 ] }
| affectation_element VIRGULE affectation_liste { $1 :: $3 }
| error { parse_error "affectation_liste" }
;

affectation_element:
| IDENT EQ relation { ($1, $3) }
;

formule:
| formule0 { $1 }
;

formule0:
| formule1 { $1 }
| formule_disjonction { `Disjunction $1 }
;

formule0nl:
| formule1nl { $1 }
| formule_disjonction_nl { `Disjunction $1 }
;

formule_disjonction_nl:
| formule1nl OR formule1nl { [$1; $3] }
| formule1nl OR formule_disjonction_nl {$1::$3}
;

formule_disjonction:
| formule1nl OR formule1 { [$1; $3] }
| formule1nl OR formule_disjonction {$1::$3}
;

formule1:
| formule2 { $1 }
| formule2nl IMPLIES formule1 { implication $1 $3 }
//| 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 { implication $1 $3 }
// | formule2nl IMPLIES formule2nl els formule1nl { fun e -> si_formule ($1 e) ($3 e) ($5 e) }
;

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

formule2:
| formule3 { $1 }
| formule_conjonction { `Conjunction ($1) }
;

formule2nl:
| formule3nl { $1 }
| formule_conjonction_nl { `Conjunction ($1) }
;

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

formule_conjonction_nl:
| formule3nl AND formule3nl { [$1; $3]}
| formule3nl AND formule_conjonction_nl { ($1)::($3) }
;

formule3:
| formule4 { $1 }
| NOT formule3 { `Negation ($2 ) }
;

formule3nl:
| formule4nl { $1 }
| NOT formule3nl {  `Negation ($2 ) }
;

formule4:
| PARG formule PARD { $2 }
| formule_seq { $1 }
| IDENT arg_seq { `Predicate ($1, $2) }
| SOME relation { `Some $2 }
| NO relation { `No $2 }
| LONE relation { `Lone $2 }
| ONE relation { `One $2 }
| relation_nl IN relation { `In ($1, $3) }
// | relation_nl NOT IN relation { fun e -> negation (inclusion ($1 e) ($4 e)) }
| relation_nl EQ relation { `Equality ($1, $3) }
| ALL varlist_quant formule_corps { `Forall ($2, $3) }
| SOME varlist_quant formule_corps { `Exists ($2, $3) }
| NO varlist_quant formule_corps { `Negation (`Exists ($2, $3)) }
| affectation formule_corps { affecte_form $1 $2 }
//| error { parse_error "formule4" }
;

formule4nl:
| PARG formule PARD { $2 }
| formule_seq { $1 }
| IDENT arg_seq { `Predicate ($1, $2) }
| SOME relation { `Some $2 }
| NO relation { `No $2 }
| LONE relation { `Lone $2 }
| ONE relation { `One $2 }
| relation_nl IN relation { `In ($1, $3) }
// | relation_nl NOT IN relation { fun e -> negation (inclusion ($1 e) ($4 e)) }
| relation_nl EQ relation { `Equality ($1, $3) }
//| error { parse_error "formule4nl" }
; 

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

formule_seq:
| ACCG formule_liste ACCD { `Conjunction ($2 ) }
;

formule_liste:
| { [] }
| formule formule_liste { (($1 )::($2 )) }
;

varlist_quant:
| varlist_quant0 { fst $1 }
;

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

;

arg_seq:
| PARG PARD { [] }
| PARG arg_liste PARD { $2 }
;

arg_seq2:
| LT GT { [] }
| LT arg_liste GT { $2 }
;

arg_liste:
| relation { [$1 ] }
| relation VIRGULE arg_liste { (($1 )::($3 )) }
;

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

param_liste:
| param { let p, r = $1 in [p, r], r }
| param VIRGULE param_liste {
    let p, r = $1 and l, _ = $3 in ((p, r) :: l, r)
  }
| IDENT VIRGULE param_liste { let l, r = $3 in (($1, r) :: l, r) }
;

param:
// | IDENT DP IDENT { ($1, [$3]) }
| IDENT DP SET IDENT { ($1, (`Variable $4)) }
// | IDENT DP typefleche { ($1, $3) }
| IDENT DP relation { ($1, $3) }
;

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

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

reldef_liste:
| reldef { let r = $1 in [ r ], r }
| reldef VIRGULE reldef_liste { let r = $1 and l, _ = $3 in (r :: l, r) }
| IDENT VIRGULE reldef_liste { let l, r = $3 in {r with sigrel_name = $1}::l, r}
;

reldef:
| IDENT DP IDENT { {
    sigrel_name = $1;
    sigrel_function = true;
    sigrel_type = [$3];
  } }
| IDENT DP SET IDENT { {
    sigrel_name = $1;
    sigrel_function = false;
    sigrel_type = [$4];
  } }
| IDENT DP typefleche { {
    sigrel_name = $1;
    sigrel_function = false;
    sigrel_type = $3;
  } }
;

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

instruction:
| sigdecl IDENT reldef_seq { signature {
    sig_name = $2;
    sig_mult = $1;
    sig_type = None;
    sig_rels = $3;
  } }
| sigdecl IDENT EXTENDS IDENT reldef_seq { signature {
    sig_name = $2;
    sig_mult = $1;
    sig_type = Some (`Extends $4);
    sig_rels = $5;
  } }
| sigdecl IDENT IN relation reldef_seq { signature {
    sig_name = $2;
    sig_mult = $1;
    sig_type = Some (`In $4);
    sig_rels = $5;
  } }
| PRED IDENT param_seq formule_seq { predicat {
    corps_nom = $2;
    corps_param = $3;
    corps_corps = $4
  } }
| FUN IDENT param_seq DP set relation ACCG relation ACCD { fonction {
    corps_nom = $2;
    corps_param = $3;
    corps_corps = $8;
  } }
| FACT formule_seq { fait (nouveau_symbole "unnamed_fact", $2) }
| FACT IDENT formule_seq { fait ($2, $3) }
| ASSERT IDENT formule_seq { assertion ($2, $3) }
| check { fun e -> (
    prerr_endline "Check or run statement : ignored"; 
    e 
  ) } 
| OPEN chemin { process_module $2 }
| error { parse_error "instruction" }
; 

sigdecl:
| SIG { None }
| ABSTRACT SIG { Some `Abstract }
| ONE SIG { Some `One }
;

set:
| { () }
| SET { () }
;

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

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

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 { prerr_endline "Parsing complete." ; fun e -> $2 ($1 e) }
;