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  | FIX ID LCURLY fixfuns RCURLY
  71     { let fixfuns = $4 in
  72        let idx =
  73         let rec find idx =
  74          function
  75             [] -> raise Not_found
  76           | (name,_,_,_)::_  when name = $2 -> idx
  77           | _::tl -> find (idx+1) tl
  78         in
  79          find 0 fixfuns
  80        in
  81         Fix (idx,fixfuns)
  82     }
  83  | COFIX ID LCURLY cofixfuns RCURLY
  84     { let cofixfuns = $4 in
  85        let idx =
  86         let rec find idx =
  87          function
  88             [] -> raise Not_found
  89           | (name,_,_)::_  when name = $2 -> idx
  90           | _::tl -> find (idx+1) tl
  91         in
  92          find 0 cofixfuns
  93        in
  94         CoFix (idx,cofixfuns)
  95     }
  96  | IMPLICIT { Implicit }
  97  | SET { Sort Set }
  98  | PROP { Sort Prop }
  99  | TYPE { Sort Type }
 100  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
 101  | META { Meta $1 }
 102  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
 103  | pihead expr
 104     { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) }
 105  | lambdahead expr
 106     { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) }
 107  | letinhead expr
 108     { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
 109 ;
 110 fixfuns:
 111    ID LPAREN NUM RPAREN COLON expr LETIN expr
 112     { [$1,$3,$6,$8] }
 113  | ID LPAREN NUM RPAREN COLON expr LETIN expr SEMICOLON fixfuns
 114     { ($1,$3,$6,$8)::$10 }
 115 ;
 116 cofixfuns:
 117    ID COLON expr LETIN expr
 118     { [$1,$3,$5] }
 119  | ID COLON expr LETIN expr SEMICOLON cofixfuns
 120     { ($1,$3,$5)::$7 }
 121 ;
 122 pihead:
 123   PROD ID COLON expr DOT
 124    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 125 ;
 126 lambdahead:
 127   LAMBDA ID COLON expr DOT
 128    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 129 ;
 130 letinhead:
 131   LAMBDA ID LETIN expr DOT
 132    { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
 133 ;
 134 branches:
 135                             { [] }
 136  | expr SEMICOLON branches  { $1::$3 }
 137  | expr                     { [$1] }
 138 ;
 139 exprlist:
 140                   { [] }
 141  | expr exprlist  { $1::$2 }
 142 ;
 143 alias:
 144    ALIAS ID CONURI
 145     { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }
 146  | ALIAS ID INDTYURI
 147     { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) }
 148  | ALIAS ID INDCONURI
 149     { let uri,indno,consno = $3 in
 150        Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno))
 151     }