fixed a finalization issue for connections closed twice

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 056e595e7ed8b8fc5eaf3867a47a1072e53058f9..4a21e10b5a9e6334ce022bbb430b6ba6739fb08f 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -25,12 +25,14 @@
 
 open Printf
 
+module Ast = CicNotationPt
+
 let grammar = CicNotationParser.level2_ast_grammar
 
 let term = CicNotationParser.term
 let statement = Grammar.Entry.create grammar "statement"
 
-let add_raw_attribute ~text t = CicNotationPt.AttributedTerm (`Raw text, t)
+let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 
 let default_precedence = 50
 let default_associativity = Gramext.NonA
@@ -40,7 +42,7 @@ EXTEND
   arg: [
    [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],CicNotationPt.Implicit
+   | name = IDENT -> [name],Ast.Implicit
    ]
   ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
@@ -52,23 +54,25 @@ EXTEND
     [ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
   ];
   reduction_kind: [
-    [ IDENT "reduce" -> `Reduce
+    [ IDENT "normalize" -> `Normalize
+    | IDENT "reduce" -> `Reduce
     | IDENT "simplify" -> `Simpl
-    | IDENT "whd" -> `Whd 
-    | IDENT "normalize" -> `Normalize ]
+    | IDENT "unfold"; t = OPT term -> `Unfold t
+    | IDENT "whd" -> `Whd ]
   ];
   sequent_pattern_spec: [
    [ hyp_paths =
       LIST0
        [ id = IDENT ;
          path = OPT [SYMBOL ":" ; path = term -> path ] ->
-         (id,match path with Some p -> p | None -> CicNotationPt.UserInput) ]
+         (id,match path with Some p -> p | None -> Ast.UserInput) ]
        SEP SYMBOL ";";
      goal_path = OPT [ SYMBOL <:unicode<vdash>>; term = term -> term ] ->
       let goal_path =
-       match goal_path with
-          None -> CicNotationPt.UserInput
-        | Some goal_path -> goal_path
+       match goal_path, hyp_paths with
+          None, [] -> Ast.UserInput
+        | None, _::_ -> Ast.Implicit
+        | Some goal_path, _ -> goal_path
       in
        hyp_paths,goal_path
    ]
@@ -85,12 +89,12 @@ EXTEND
         ] ->
          let wanted,hyp_paths,goal_path =
           match wanted_and_sps with
-             wanted,None -> wanted, [], CicNotationPt.UserInput
+             wanted,None -> wanted, [], Ast.UserInput
            | wanted,Some (hyp_paths,goal_path) -> wanted,hyp_paths,goal_path
          in
           wanted, hyp_paths, goal_path ] ->
       match res with
-         None -> None,[],CicNotationPt.UserInput
+         None -> None,[],Ast.UserInput
        | Some ps -> ps]
   ];
   direction: [
@@ -348,10 +352,10 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> CicNotationPt.IdentArg (0, id)
+    [ id = IDENT -> Ast.IdentArg (0, id)
     | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
       SYMBOL "."; id = IDENT ->
-        CicNotationPt.IdentArg (List.length l, id)
+        Ast.IdentArg (List.length l, id)
     ]
   ];
   associativity: [
@@ -364,7 +368,7 @@ EXTEND
     [ "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
   ];
   notation: [
-    [ s = QSTRING;
+    [ dir = OPT direction; s = QSTRING;
       assoc = OPT associativity; prec = OPT precedence;
       IDENT "for";
       p2 = 
@@ -385,24 +389,26 @@ EXTEND
             | None -> default_precedence
             | Some prec -> prec
           in
-          (add_raw_attribute ~text:s
-            (CicNotationParser.parse_level1_pattern (Stream.of_string s)),
-           assoc, prec, p2)
+          let p1 =
+            add_raw_attribute ~text:s
+              (CicNotationParser.parse_level1_pattern (Stream.of_string s))
+          in
+          (dir, p1, assoc, prec, p2)
     ]
   ];
   level3_term: [
-    [ u = URI -> CicNotationPt.UriPattern (UriManager.uri_of_string u)
-    | id = IDENT -> CicNotationPt.VarPattern id
-    | SYMBOL "_" -> CicNotationPt.ImplicitPattern
+    [ u = URI -> Ast.UriPattern (UriManager.uri_of_string u)
+    | id = IDENT -> Ast.VarPattern id
+    | SYMBOL "_" -> Ast.ImplicitPattern
     | LPAREN; terms = LIST1 SELF; RPAREN ->
         (match terms with
         | [] -> assert false
         | [term] -> term
-        | terms -> CicNotationPt.ApplPattern terms)
+        | terms -> Ast.ApplPattern terms)
     ]
   ];
   interpretation: [
-    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
+    [ s = CSYMBOL; args = LIST0 argument; SYMBOL "="; t = level3_term ->
         (s, args, t)
     ]
   ];
@@ -415,26 +421,26 @@ EXTEND
       typ = term; SYMBOL <:unicode<def>> ; newname = IDENT ->
         GrafiteAst.Obj (loc, 
           GrafiteAst.Theorem 
-            (`Variant,name,typ,Some (CicNotationPt.Ident (newname, None))))
+            (`Variant,name,typ,Some (Ast.Ident (newname, None))))
     | flavour = theorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc,GrafiteAst.Theorem (flavour, name, typ, body))
     | flavour = theorem_flavour; name = IDENT;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         GrafiteAst.Obj (loc,
-          GrafiteAst.Theorem (flavour, name, CicNotationPt.Implicit, body))
+          GrafiteAst.Theorem (flavour, name, Ast.Implicit, body))
     | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((CicNotationPt.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((CicNotationPt.Ident (name, None), None),_,_) :: _ ->
-                name, CicNotationPt.Implicit
+            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
+            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+                name, Ast.Implicit
             | _ -> assert false 
           in
-          let body = CicNotationPt.Ident (name,None) in
+          let body = Ast.Ident (name,None) in
           GrafiteAst.Obj (loc,GrafiteAst.Theorem(`Definition, name, ty,
-            Some (CicNotationPt.LetRec (ind_kind, defs, body))))
+            Some (Ast.LetRec (ind_kind, defs, body))))
     | [ IDENT "inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
@@ -446,9 +452,9 @@ EXTEND
         in
         GrafiteAst.Obj (loc,GrafiteAst.Inductive (params, ind_types))
     | IDENT "coercion" ; name = IDENT -> 
-        GrafiteAst.Coercion (loc, CicNotationPt.Ident (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Ident (name,Some []))
     | IDENT "coercion" ; name = URI -> 
-        GrafiteAst.Coercion (loc, CicNotationPt.Uri (name,Some []))
+        GrafiteAst.Coercion (loc, Ast.Uri (name,Some []))
     | IDENT "alias" ; spec = alias_spec ->
         GrafiteAst.Alias (loc, spec)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
@@ -458,8 +464,8 @@ EXTEND
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
-    | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
-        GrafiteAst.Notation (loc, l1, assoc, prec, l2)
+    | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
+        GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
     | IDENT "interpretation"; id = QSTRING;
       (symbol, args, l3) = interpretation ->
         GrafiteAst.Interpretation (loc, id, (symbol, args), l3)