CIC Textual Parser added to the repository.

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
new file mode 100644 (file)
index 0000000..844384f
--- /dev/null
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -0,0 +1,151 @@
+%{
+ open Cic;;
+ module U = UriManager;;
+
+ exception InvalidSuffix of string;;
+ exception InductiveTypeURIExpected;;
+ 
+ let uri_of_id_map = Hashtbl.create 53;;
+
+ let binders = ref [];;
+
+ let get_index_in_list e =
+  let rec aux i =
+   function
+      [] -> raise Not_found
+    | he::_ when he = e -> i
+    | _::tl -> aux (i+1) tl
+  in
+   aux 1
+;;
+%}
+%token <string> ID
+%token <int> META
+%token <int> NUM
+%token <UriManager.uri> CONURI
+%token <UriManager.uri * int> INDTYURI
+%token <UriManager.uri * int * int> INDCONURI
+%token ALIAS
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
+%token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE EOF
+%start main
+%type <Cic.term option> main
+%%
+main:
+   expr  { Some $1 }
+ | alias { None }
+ | EOF   { raise CicTextualParser0.Eof }
+;
+expr:
+   CONURI
+   { let uri = UriManager.string_of_uri $1 in
+     let suff = (String.sub uri (String.length uri - 3) 3) in
+      match suff with
+         "con" -> Const ($1,0)
+       | "var" -> Var $1
+       | _ -> raise (InvalidSuffix suff)
+   }
+ | INDTYURI { MutInd (fst $1, 0, snd $1) }
+ | INDCONURI
+   { let (uri,tyno,consno) = $1 in MutConstruct (uri, 0, tyno, consno) }
+ | ID
+   { try
+       Rel (get_index_in_list (Name $1) !binders)
+     with
+      Not_found ->
+       Hashtbl.find uri_of_id_map $1
+   }
+ | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
+    { MutCase (fst $5, 0, snd $5, $7, $3, $10) }
+ | CASE LPAREN expr COLON ID SEMICOLON expr RPAREN LCURLY branches RCURLY
+    { try
+       let _ = get_index_in_list (Name $5) !binders in
+        raise InductiveTypeURIExpected
+      with
+       Not_found ->
+        match Hashtbl.find uri_of_id_map $5 with
+           MutInd (uri,0,typeno) -> MutCase (uri, 0, typeno, $7, $3, $10)
+         | _ -> raise InductiveTypeURIExpected
+    }
+ | FIX ID LCURLY fixfuns RCURLY
+    { let fixfuns = $4 in
+       let idx =
+        let rec find idx =
+         function
+            [] -> raise Not_found
+          | (name,_,_,_)::_  when name = $2 -> idx
+          | _::tl -> find (idx+1) tl
+        in
+         find 0 fixfuns
+       in
+        Fix (idx,fixfuns)
+    }
+ | COFIX ID LCURLY cofixfuns RCURLY
+    { let cofixfuns = $4 in
+       let idx =
+        let rec find idx =
+         function
+            [] -> raise Not_found
+          | (name,_,_)::_  when name = $2 -> idx
+          | _::tl -> find (idx+1) tl
+        in
+         find 0 cofixfuns
+       in
+        CoFix (idx,cofixfuns)
+    }
+ | IMPLICIT { Implicit }
+ | SET { Sort Set }
+ | PROP { Sort Prop }
+ | TYPE { Sort Type }
+ | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
+ | META { Meta $1 }
+ | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
+ | pihead expr 
+    { binders := List.tl !binders ; Prod (fst $1, snd $1,$2) }
+ | lambdahead expr 
+    { binders := List.tl !binders ; Lambda (fst $1, snd $1,$2) }
+ | letinhead expr 
+    { binders := List.tl !binders ; LetIn (fst $1, snd $1,$2) }
+;
+fixfuns:
+   ID LPAREN NUM RPAREN COLON expr LETIN expr
+    { [$1,$3,$6,$8] }
+ | ID LPAREN NUM RPAREN COLON expr LETIN expr SEMICOLON fixfuns
+    { ($1,$3,$6,$8)::$10 }
+;
+cofixfuns:
+   ID COLON expr LETIN expr
+    { [$1,$3,$5] }
+ | ID COLON expr LETIN expr SEMICOLON cofixfuns
+    { ($1,$3,$5)::$7 }
+;
+pihead:
+  PROD ID COLON expr DOT
+   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
+;
+lambdahead:
+  LAMBDA ID COLON expr DOT
+   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
+;
+letinhead:
+  LAMBDA ID LETIN expr DOT
+   { binders := (Name $2)::!binders ; (Cic.Name $2, $4) }
+;
+branches:
+                            { [] }
+ | expr SEMICOLON branches  { $1::$3 }
+ | expr                     { [$1] }
+;
+exprlist:
+                  { [] }
+ | expr exprlist  { $1::$2 }
+;
+alias:
+   ALIAS ID CONURI
+    { Hashtbl.add uri_of_id_map $2 (Cic.Const ($3,0)) }
+ | ALIAS ID INDTYURI
+    { Hashtbl.add uri_of_id_map $2 (Cic.MutInd (fst $3, 0, snd $3)) }
+ | ALIAS ID INDCONURI
+    { let uri,indno,consno = $3 in
+       Hashtbl.add uri_of_id_map $2 (Cic.MutConstruct (uri, 0, indno ,consno))
+    }