/* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 */

%{
 open Cic;;
 module U = UriManager;;

 exception InvalidSuffix of string;;
 exception InductiveTypeURIExpected;;
 exception UnknownIdentifier of string;;
 exception ExplicitNamedSubstitutionAppliedToRel;;
 exception TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable;;
 
 (* merge removing duplicates of two lists free of duplicates *)
 let union dom1 dom2 =
  let rec filter =
   function
      [] -> []
    | he::tl ->
       if List.mem he dom1 then filter tl else he::(filter tl)
  in
   dom1 @ (filter dom2)
 ;;

 let get_index_in_list e =
  let rec aux i =
   function
      [] -> raise Not_found
    | (Some he)::_ when he = e -> i
    | _::tl -> aux (i+1) tl
  in
   aux 1
 ;;

 (* Returns the first meta whose number is above the *)
 (* number of the higher meta.                       *)
 (*CSC: cut&pasted from proofEngine.ml *)
 let new_meta () =
  let rec aux =
   function
      None,[] -> 1
    | Some n,[] -> n
    | None,(n,_,_)::tl -> aux (Some n,tl)
    | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  in
   1 + aux (None,!TexCicTextualParser0.metasenv)
 ;;

 (* identity_relocation_list_for_metavariable i canonical_context         *)
 (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
 (* where n = List.length [canonical_context]                             *)
 (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
 (*CSC: cut&pasted from proofEngine.ml *)
 let identity_relocation_list_for_metavariable canonical_context =
  let canonical_context_length = List.length canonical_context in
   let rec aux =
    function
       (_,[]) -> []
     | (n,None::tl) -> None::(aux ((n+1),tl))
     | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
   in
    aux (1,canonical_context)
 ;;

 let deoptionize_exp_named_subst =
  function
     None -> [], (function _ -> [])
   | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
 ;;

 let term_of_con_uri uri exp_named_subst =
  Const (uri,exp_named_subst)
 ;;

 let term_of_var_uri uri exp_named_subst =
  Var (uri,exp_named_subst)
 ;;

 let term_of_indty_uri (uri,tyno) exp_named_subst =
  MutInd (uri, tyno, exp_named_subst)
 ;;

 let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
  MutConstruct (uri, tyno, consno, exp_named_subst)
 ;;

 let term_of_uri uri =
  match uri with
     CicTextualParser0.ConUri uri ->
      term_of_con_uri uri
   | CicTextualParser0.VarUri uri ->
      term_of_var_uri uri
   | CicTextualParser0.IndTyUri (uri,tyno) ->
      term_of_indty_uri (uri,tyno) 
   | CicTextualParser0.IndConUri (uri,tyno,consno) ->
      term_of_indcon_uri (uri,tyno,consno)
 ;;

 let var_uri_of_id id interp =
  let module CTP0 = CicTextualParser0 in
   match interp (CicTextualParser0.Id id) with
      None -> raise (UnknownIdentifier id)
    | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
    | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
 ;;

 let indty_uri_of_id id interp =
  let module CTP0 = CicTextualParser0 in
   match interp (CicTextualParser0.Id id) with
      None -> raise (UnknownIdentifier id)
    | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
    | Some _ -> raise InductiveTypeURIExpected
 ;;

 let mk_implicit () =
  let newmeta = new_meta () in
   let new_canonical_context = [] in
    let irl =
     identity_relocation_list_for_metavariable new_canonical_context
    in
     TexCicTextualParser0.metasenv :=
      [newmeta, new_canonical_context, Sort Type ;
       newmeta+1, new_canonical_context, Meta (newmeta,irl);
       newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
      ] @ !TexCicTextualParser0.metasenv ;
     [], function _ -> Meta (newmeta+2,irl)
 ;;
%}
%token <string> ID
%token <int> META
%token <int> NUM
%token <UriManager.uri> CONURI
%token <UriManager.uri> VARURI
%token <UriManager.uri * int> INDTYURI
%token <UriManager.uri * int * int> INDCONURI
%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
%token DOLLAR
%token PLUS MINUS TIMES EQ
%right ARROW
%right EQ
%right PLUS MINUS
%right TIMES
%start main
%type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
%%
main:
 | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
 | DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
 | DOLLAR DOLLAR DOLLAR DOLLAR EOF {raise CicTextualParser0.Eof }
 | expr EOF { $1 }
 | DOLLAR expr DOLLAR EOF { $2 }
 | DOLLAR DOLLAR expr DOLLAR DOLLAR EOF { $3 }
 | expr SEMICOLON { $1 } /*  FG: to read several terms in a row
                          *  Do we need to clear some static variables? 
			  */
;
expr2:
   NUM
   { [], function interp ->
      let rec cic_int_of_int =
       function
          0 ->
           Cic.MutConstruct
            (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
             0,1,[])
        | n ->
          Cic.Appl
           [ Cic.MutConstruct
              (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
               0,2,[]) ;
             cic_int_of_int (n - 1)
           ]
      in
       cic_int_of_int $1
   }
 | expr2 PLUS expr2
   { let dom1,mk_expr1 = $1 in
     let dom2,mk_expr2 = $3 in
      let dom = union dom1 dom2 in
       dom, function interp ->
        Cic.Appl
         [Cic.Const
           (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
          (mk_expr1 interp) ;
          (mk_expr2 interp)
         ]
   }
 | expr2 MINUS expr2
   { let dom1,mk_expr1 = $1 in
     let dom2,mk_expr2 = $3 in
      let dom = union dom1 dom2 in
       dom, function interp ->
        Cic.Appl
         [Cic.Const
           (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
          (mk_expr1 interp) ;
          (mk_expr2 interp)
         ]
   }
 | expr2 TIMES expr2
   { let dom1,mk_expr1 = $1 in
     let dom2,mk_expr2 = $3 in
      let dom = union dom1 dom2 in
       dom, function interp ->
        Cic.Appl
         [Cic.Const
           (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
          (mk_expr1 interp) ;
          (mk_expr2 interp)
         ]
   }
 | expr2 EQ expr2
   { let dom1,mk_expr1 = $1 in
     let dom2,mk_expr2 = $3 in
     let dom3,mk_expr3 = mk_implicit () in
      let dom = union dom1 (union dom2 dom3) in
       dom, function interp ->
        Cic.Appl
         [Cic.MutInd
           (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
          (mk_expr3 interp) ;
          (mk_expr1 interp) ;
          (mk_expr2 interp)
         ]
   }
 | CONURI exp_named_subst
   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
      dom, function interp -> term_of_con_uri $1 (mk_exp_named_subst interp)
   }
 | VARURI exp_named_subst
   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
      dom, function interp -> term_of_var_uri $1 (mk_exp_named_subst interp)
   }
 | INDTYURI exp_named_subst
   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
      dom, function interp -> term_of_indty_uri $1 (mk_exp_named_subst interp)
   }
 | INDCONURI exp_named_subst
   { let dom,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
      dom, function interp -> term_of_indcon_uri $1 (mk_exp_named_subst interp)
   }
 | ID exp_named_subst
   { try
      let res =
       Rel (get_index_in_list (Name $1) !TexCicTextualParser0.binders)
      in
       (match $2 with
           None -> ([], function _ -> res)
         | Some _ -> raise (ExplicitNamedSubstitutionAppliedToRel)
       )
     with
      Not_found ->
       let dom1,mk_exp_named_subst = deoptionize_exp_named_subst $2 in
        let dom = union dom1 [CicTextualParser0.Id $1] in
         dom,
          function interp ->
           match interp (CicTextualParser0.Id $1) with
	      None  -> raise (UnknownIdentifier $1)
	    | Some (CicTextualParser0.Uri uri) ->
               term_of_uri uri (mk_exp_named_subst interp)
            | Some CicTextualParser0.Implicit ->
               (*CSC: not very clean; to maximize code reusage *)
               snd (mk_implicit ()) ""
            | Some (CicTextualParser0.Term mk_term) ->
               (mk_term interp)
   }
 | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
    { let dom1,mk_expr1 = $3 in
      let dom2,mk_expr2 = $7 in
      let dom3,mk_expr3 = $10 in
       let dom = union dom1 (union dom2 dom3) in
        dom,
        function interp ->
         MutCase
          (fst $5,snd $5,(mk_expr2 interp),(mk_expr1 interp),(mk_expr3 interp))
    }
 | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
    { let dom1,mk_expr1 = $3 in
      let dom2,mk_expr2 = $7 in
      let dom3,mk_expr3 = $10 in
       let dom =
        union [CicTextualParser0.Id $5] (union dom1 (union dom2 dom3))
       in
        dom,
        function interp ->
         let uri,typeno = indty_uri_of_id $5 interp in
          MutCase
           (uri,typeno,(mk_expr2 interp),(mk_expr1 interp),
             (mk_expr3 interp))
    }
 | fixheader LCURLY exprseplist RCURLY
    { let dom1,foo,ids_and_indexes,mk_types = $1 in
      let dom2,mk_exprseplist = $3 in
       let dom = union dom1 dom2 in
        for i = 1 to List.length ids_and_indexes do
         TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders
        done ;
        dom,
         function interp ->
          let types = mk_types interp in
          let fixfunsbodies = (mk_exprseplist interp) in
           let idx =
            let rec find idx =
             function
                [] -> raise Not_found
              | (name,_)::_  when name = foo -> idx
              | _::tl -> find (idx+1) tl
            in
             find 0 ids_and_indexes
           in
            let fixfuns =
             List.map2 (fun ((name,recindex),ty) bo -> (name,recindex,ty,bo))
              (List.combine ids_and_indexes types) fixfunsbodies
            in
             Fix (idx,fixfuns)
    }
 | cofixheader LCURLY exprseplist RCURLY
    { let dom1,foo,ids,mk_types = $1 in
      let dom2,mk_exprseplist = $3 in
       let dom = union dom1 dom2 in
        dom,
         function interp ->
          let types = mk_types interp in
          let fixfunsbodies = (mk_exprseplist interp) in
           let idx =
            let rec find idx =
             function
                [] -> raise Not_found
              | name::_  when name = foo -> idx
              | _::tl -> find (idx+1) tl
            in
             find 0 ids
           in
            let fixfuns =
             List.map2 (fun (name,ty) bo -> (name,ty,bo))
              (List.combine ids types) fixfunsbodies
            in
             for i = 1 to List.length fixfuns do
              TexCicTextualParser0.binders :=
               List.tl !TexCicTextualParser0.binders
             done ;
             CoFix (idx,fixfuns)
    }
 | IMPLICIT
    { mk_implicit () }
 | SET  { [], function _ -> Sort Set }
 | PROP { [], function _ -> Sort Prop }
 | TYPE { [], function _ -> Sort Type }
 | LPAREN expr CAST expr RPAREN
    { let dom1,mk_expr1 = $2 in
      let dom2,mk_expr2 = $4 in
       let dom = union dom1 dom2 in
        dom, function interp -> Cast ((mk_expr1 interp),(mk_expr2 interp))
    }
 | META LBRACKET substitutionlist RBRACKET
    { let dom,mk_substitutionlist = $3 in
       dom, function interp -> Meta ($1, mk_substitutionlist interp)
    } 
 | LPAREN expr exprlist RPAREN
    { let length,dom2,mk_exprlist = $3 in
       match length with
          0 -> $2
        | _ ->
          let dom1,mk_expr1 = $2 in
           let dom = union dom1 dom2 in
            dom,
             function interp ->
              Appl ((mk_expr1 interp)::(mk_exprlist interp))
    }
;
exp_named_subst :
    { None }
 | LCURLY named_substs RCURLY
    { Some $2 }
;
named_substs :
   VARURI LETIN expr2
    { let dom,mk_expr = $3 in
       dom, function interp -> [$1, mk_expr interp] }
 | ID LETIN expr2
    { let dom1,mk_expr = $3 in
       let dom = union [CicTextualParser0.Id $1] dom1 in
        dom, function interp -> [var_uri_of_id $1 interp, mk_expr interp] }
 | VARURI LETIN expr2 SEMICOLON named_substs
    { let dom1,mk_expr = $3 in
      let dom2,mk_named_substs = $5 in
       let dom = union dom1 dom2 in
        dom, function interp -> ($1, mk_expr interp)::(mk_named_substs interp)
    }
 | ID LETIN expr2 SEMICOLON named_substs
    { let dom1,mk_expr = $3 in
      let dom2,mk_named_substs = $5 in
       let dom = union [CicTextualParser0.Id $1] (union dom1 dom2) in
        dom,
         function interp ->
          (var_uri_of_id $1 interp, mk_expr interp)::(mk_named_substs interp)
    }
;
expr :
   pihead expr
    { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
      let dom1,mk_expr1 = snd $1 in
      let dom2,mk_expr2 = $2 in
       let dom = union dom1 dom2 in
        dom, function interp -> Prod (fst $1, mk_expr1 interp, mk_expr2 interp)
    }
 | lambdahead expr
    { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
      let dom1,mk_expr1 = snd $1 in
      let dom2,mk_expr2 = $2 in
       let dom = union dom1 dom2 in
        dom,function interp -> Lambda (fst $1, mk_expr1 interp, mk_expr2 interp)
    }
 | letinhead expr
    { TexCicTextualParser0.binders := List.tl !TexCicTextualParser0.binders ;
      let dom1,mk_expr1 = snd $1 in
      let dom2,mk_expr2 = $2 in
       let dom = union dom1 dom2 in
        dom, function interp -> LetIn (fst $1, mk_expr1 interp, mk_expr2 interp)
    }
 | expr2
    { $1 }
;
fixheader:
   FIX ID LCURLY fixfunsdecl RCURLY
    { let dom,ids_and_indexes,mk_types = $4 in
       let bs =
        List.rev_map (function (name,_) -> Some (Name name)) ids_and_indexes
       in
        TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
        dom, $2, ids_and_indexes, mk_types
    }
;
fixfunsdecl:
   ID LPAREN NUM RPAREN COLON expr
    { let dom,mk_expr = $6 in
       dom, [$1,$3], function interp -> [mk_expr interp]
    }
 | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
    { let dom1,mk_expr = $6 in
      let dom2,ids_and_indexes,mk_types = $8 in
       let dom = union dom1 dom2 in
        dom, ($1,$3)::ids_and_indexes,
         function interp -> (mk_expr interp)::(mk_types interp)
    }
;
cofixheader:
   COFIX ID LCURLY cofixfunsdecl RCURLY
    { let dom,ids,mk_types = $4 in
       let bs =
        List.rev_map (function name -> Some (Name name)) ids
       in
        TexCicTextualParser0.binders := bs@(!TexCicTextualParser0.binders) ;
        dom, $2, ids, mk_types
    }
;
cofixfunsdecl:
   ID COLON expr
    { let dom,mk_expr = $3 in
       dom, [$1], function interp -> [mk_expr interp]
    }
 | ID COLON expr SEMICOLON cofixfunsdecl
    { let dom1,mk_expr = $3 in
      let dom2,ids,mk_types = $5 in
       let dom = union dom1 dom2 in
        dom, $1::ids,
         function interp -> (mk_expr interp)::(mk_types interp)
    }
;
pihead:
   PROD ID COLON expr DOT
    { TexCicTextualParser0.binders :=
       (Some (Name $2))::!TexCicTextualParser0.binders;
      let dom,mk_expr = $4 in
       Cic.Name $2, (dom, function interp -> mk_expr interp)
    }
 | expr2 ARROW
   { TexCicTextualParser0.binders :=
      (Some Anonymous)::!TexCicTextualParser0.binders ;
     let dom,mk_expr = $1 in
      Anonymous, (dom, function interp -> mk_expr interp)
   }
 | PROD ID DOT
    { TexCicTextualParser0.binders :=
       (Some (Name $2))::!TexCicTextualParser0.binders;
      let newmeta = new_meta () in
       let new_canonical_context = [] in
        let irl =
         identity_relocation_list_for_metavariable new_canonical_context
        in
         TexCicTextualParser0.metasenv :=
          [newmeta, new_canonical_context, Sort Type ;
           newmeta+1, new_canonical_context, Meta (newmeta,irl)
          ] @ !TexCicTextualParser0.metasenv ;
         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
    }
;
lambdahead:
   LAMBDA ID COLON expr DOT
    { TexCicTextualParser0.binders :=
       (Some (Name $2))::!TexCicTextualParser0.binders;
      let dom,mk_expr = $4 in
       Cic.Name $2, (dom, function interp -> mk_expr interp)
    }
 | LAMBDA ID DOT
    { TexCicTextualParser0.binders :=
       (Some (Name $2))::!TexCicTextualParser0.binders;
      let newmeta = new_meta () in
       let new_canonical_context = [] in
        let irl =
         identity_relocation_list_for_metavariable new_canonical_context
        in
         TexCicTextualParser0.metasenv :=
          [newmeta, new_canonical_context, Sort Type ;
           newmeta+1, new_canonical_context, Meta (newmeta,irl)
          ] @ !TexCicTextualParser0.metasenv ;
         Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
    }
;
letinhead:
  LAMBDA ID LETIN expr DOT
   { TexCicTextualParser0.binders :=
      (Some (Name $2))::!TexCicTextualParser0.binders ;
     let dom,mk_expr = $4 in
      Cic.Name $2, (dom, function interp -> mk_expr interp)
   }
;
branches:
    { [], function _ -> [] }
 | expr SEMICOLON branches
    { let dom1,mk_expr = $1 in
      let dom2,mk_branches = $3 in
       let dom = union dom1 dom2 in
        dom, function interp -> (mk_expr interp)::(mk_branches interp)
    }
 | expr
    { let dom,mk_expr = $1 in
       dom, function interp -> [mk_expr interp]
    }
;
exprlist:
    
    { 0, [], function _ -> [] }
 | expr exprlist
    { let dom1,mk_expr = $1 in
      let length,dom2,mk_exprlist = $2 in
       let dom = union dom1 dom2 in
        length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
    }
;
exprseplist:
   expr
    { let dom,mk_expr = $1 in
       dom, function interp -> [mk_expr interp]
    }
 | expr SEMICOLON exprseplist
    { let dom1,mk_expr = $1 in
      let dom2,mk_exprseplist = $3 in
       let dom = union dom1 dom2 in
        dom, function interp -> (mk_expr interp)::(mk_exprseplist interp)
    }
;
substitutionlist:
    { [], function _ -> [] }
 | expr SEMICOLON substitutionlist
    { let dom1,mk_expr = $1 in
      let dom2,mk_substitutionlist = $3 in
       let dom = union dom1 dom2 in
        dom,
         function interp ->(Some (mk_expr interp))::(mk_substitutionlist interp)
    }
 | NONE SEMICOLON substitutionlist
    { let dom,mk_exprsubstitutionlist = $3 in
       dom, function interp -> None::(mk_exprsubstitutionlist interp)
    }