helm/ocaml/cic_textual_parser/cicTextualParser.mly

   1 %{
   2  open Cic;;
   3  module U = UriManager;;
   4
   5  exception InvalidSuffix of string;;
   6  exception InductiveTypeURIExpected;;
   7
   8  let uri_of_id_map = Hashtbl.create 53;;
   9
  10  let binders = ref [];;
  11
  12  let get_index_in_list e =
  13   let rec aux i =
  14    function
  15       [] -> raise Not_found
  16     | he::_ when he = e -> i
  17     | _::tl -> aux (i+1) tl
  18   in
  19    aux 1
  20 ;;
  21 %}
  22 %token <string> ID
  23 %token <int> META
  24 %token <int> NUM
  25 %token <UriManager.uri> CONURI
  26 %token <UriManager.uri * int> INDTYURI
  27 %token <UriManager.uri * int * int> INDCONURI
  28 %token ALIAS
  29 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
  30 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE EOF
  31 %start main
  32 %type <Cic.term option> main
  33 %%
  34 main:
  35    expr  { Some $1 }
  36  | alias { None }
  37  | EOF   { raise CicTextualParser0.Eof }
  38 ;
  39 expr:
  40    CONURI
  41    { let uri = UriManager.string_of_uri $1 in
  42      let suff = (String.sub uri (String.length uri - 3) 3) in
  43       match suff with
  44          "con" -> Const ($1,0)
  45        | "var" -> Var $1
  46        | _ -> raise (InvalidSuffix suff)
  47    }
  48  | INDTYURI { MutInd (fst $1, 0, snd $1) }
  49  | INDCONURI
  50    { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) }
  51  | ID
  52    { try
  53        Rel (get_index_in_list (Name $1) !binders)
  54      with
  55       Not_found ->
  56        Hashtbl.find uri_of_id_map $1
  57    }
  58  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
  59     { MutCase (fst $5, 0, snd $5, $7, $3, $10) }
  60  | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
  61     { try
  62        let _ = get_index_in_list (Name $5) !binders in
  63         raise InductiveTypeURIExpected
  64       with
  65        Not_found ->
  66         match Hashtbl.find uri_of_id_map $5 with
  67            MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10)
  68          | _ -> raise InductiveTypeURIExpected
  69     }
  70  | fixheader LCURLY exprseplist RCURLY
  71     { let fixfunsdecls = snd $1 in
  72       let fixfunsbodies = $3 in
  73        let idx =
  74         let rec find idx =
  75          function
  76             [] -> raise Not_found
  77           | (name,_,_)::_  when name = (fst $1) -> idx
  78           | _::tl -> find (idx+1) tl
  79         in
  80          find 0 fixfunsdecls
  81        in
  82         let fixfuns =
  83          List.map2 (fun (name,recindex,ty) bo -> (name,recindex,ty,bo))
  84           fixfunsdecls fixfunsbodies
  85         in
  86          for i = 1 to List.length fixfuns do
  87           binders := List.tl !binders
  88          done ;
  89          Fix (idx,fixfuns)
  90     }
  91  | cofixheader LCURLY exprseplist RCURLY
  92     { let cofixfunsdecls = (snd $1) in
  93       let cofixfunsbodies = $3 in
  94        let idx =
  95         let rec find idx =
  96          function
  97             [] -> raise Not_found
  98           | (name,_)::_  when name = (fst $1) -> idx
  99           | _::tl -> find (idx+1) tl
 100         in
 101          find 0 cofixfunsdecls
 102        in
 103         let cofixfuns =
 104          List.map2 (fun (name,ty) bo -> (name,ty,bo))
 105           cofixfunsdecls cofixfunsbodies
 106         in
 107          for i = 1 to List.length cofixfuns do
 108           binders := List.tl !binders
 109          done ;
 110          CoFix (idx,cofixfuns)
 111     }
 112  | IMPLICIT { Implicit }
 113  | SET { Sort Set }
 114  | PROP { Sort Prop }
 115  | TYPE { Sort Type }
 116  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
 117  | META { Meta $1 }
 118  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 119  | pihead expr
 120     { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) }
 121  | lambdahead expr
 122     { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) }
 123  | letinhead expr
 124     { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
 125 ;
 126 fixheader:
 127    FIX ID LCURLY fixfunsdecl RCURLY
 128     { let bs = List.rev_map (function (name,_,_) -> Name name) $4 in
 129        binders := bs@(!binders) ;
 130        $2,$4
 131     }
 132 ;
 133 fixfunsdecl:
 134    ID LPAREN NUM RPAREN COLON expr
 135     { [$1,$3,$6] }
 136  | ID LPAREN NUM RPAREN COLON expr SEMICOLON fixfunsdecl
 137     { ($1,$3,$6)::$8 }
 138 ;
 139 cofixheader:
 140    COFIX ID LCURLY cofixfunsdecl RCURLY
 141     { let bs = List.rev_map (function (name,_) -> Name name) $4 in
 142        binders := bs@(!binders) ;
 143        $2,$4
 144     }
 145 ;
 146 cofixfunsdecl:
 147    ID COLON expr
 148     { [$1,$3] }
 149  | ID COLON expr SEMICOLON cofixfunsdecl
 150     { ($1,$3)::$5 }
 151 ;
 152 pihead:
 153   PROD ID COLON expr DOT
 154    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 155 ;
 156 lambdahead:
 157   LAMBDA ID COLON expr DOT
 158    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 159 ;
 160 letinhead:
 161   LAMBDA ID LETIN expr DOT
 162    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 163 ;
 164 branches:
 165                             { [] }
 166  | expr SEMICOLON branches  { $1::$3 }
 167  | expr                     { [$1] }
 168 ;
 169 exprlist:
 170                   { [] }
 171  | expr exprlist  { $1::$2 }
 172 ;
 173 exprseplist:
 174    expr                        { [$1] }
 175  | expr SEMICOLON exprseplist  { $1::$3 }
 176 ;
 177 alias:
 178    ALIAS ID CONURI
 179     { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }
 180  | ALIAS ID INDTYURI
 181     { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) }
 182  | ALIAS ID INDCONURI
 183     { let uri,indno,consno = $3 in
 184        Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno))
 185     }