multiple bindings inside OPT supported

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 09fd55b0d4bae7c890c6eb98599fbf6d3e9aa034..0c4ae0220719a998a664edb95b2e9b69f41f86e0 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -373,6 +373,11 @@ let term = Gramext.Sself
 
 type env_type = (string * (value_type * value)) list
 
+type binding =
+  | NoBinding
+  | Binding of string * value_type
+  | Env
+
 let rec pp_value =
   function
   | TermValue _ -> "@TERM@"
@@ -403,33 +408,36 @@ let make_action action bindings =
       [] ->
         prerr_endline "aux: make_action";
         Gramext.action (fun (loc: location) -> action vl loc)
-    | None :: tl ->
+    | NoBinding :: tl ->
         prerr_endline "aux: none";
         Gramext.action (fun _ -> aux vl tl)
     (* LUCA: DEFCON 3 BEGIN *)
-    | Some (name, TermType) :: tl ->
+    | Binding (name, TermType) :: tl ->
         prerr_endline "aux: term";
         Gramext.action
           (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl)
-    | Some (name, StringType) :: tl ->
+    | Binding (name, StringType) :: tl ->
         prerr_endline "aux: string";
         Gramext.action
           (fun (v:string) ->
             aux ((name, (StringType, (StringValue v))) :: vl) tl)
-    | Some (name, NumType) :: tl ->
+    | Binding (name, NumType) :: tl ->
         prerr_endline "aux: num";
         Gramext.action
           (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl)
-    | Some (name, OptType t) :: tl ->
+    | Binding (name, OptType t) :: tl ->
         prerr_endline "aux: opt";
         Gramext.action
           (fun (v:'a option) ->
             aux ((name, (OptType t, (OptValue v))) :: vl) tl)
-    | Some (name, ListType t) :: tl ->
+    | Binding (name, ListType t) :: tl ->
         prerr_endline "aux: list";
         Gramext.action
           (fun (v:'a list) ->
             aux ((name, (ListType t, (ListValue v))) :: vl) tl)
+    | Env :: tl ->
+        prerr_endline "aux: env";
+        Gramext.action (fun (v:env_type) -> aux (v @ vl) tl)
     (* LUCA: DEFCON 3 END *)
   in
     aux [] (List.rev bindings)
@@ -438,8 +446,8 @@ let flatten_opt =
   let rec aux acc =
     function
       [] -> List.rev acc
-    | None::tl -> aux acc tl
-    | Some hd::tl -> aux (hd::acc) tl
+    | (NoBinding | Env) :: tl -> aux acc tl
+    | Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
   in
   aux []
 
@@ -451,28 +459,30 @@ let extract_term_production pattern =
     | Magic m -> aux_magic m
     | Variable v -> aux_variable v
     | _ -> assert false
-  and aux_literal = function
-    | `Symbol s -> [None, symbol s]
-    | `Keyword s -> [None, ident s]
-    | `Number s -> [None, number s]
+  and aux_literal =
+    function
+    | `Symbol s -> [NoBinding, symbol s]
+    | `Keyword s -> [NoBinding, ident s]
+    | `Number s -> [NoBinding, number s]
   and aux_layout = function
-    | Sub (p1, p2) -> aux p1 @ [None, symbol "\\SUB"] @ aux p2
-    | Sup (p1, p2) -> aux p1 @ [None, symbol "\\SUP"] @ aux p2
-    | Below (p1, p2) -> aux p1 @ [None, symbol "\\BELOW"] @ aux p2
-    | Above (p1, p2) -> aux p1 @ [None, symbol "\\ABOVE"] @ aux p2
-    | Frac (p1, p2) -> aux p1 @ [None, symbol "\\FRAC"] @ aux p2
-    | Atop (p1, p2) -> aux p1 @ [None, symbol "\\ATOP"] @ aux p2
-    | Over (p1, p2) -> aux p1 @ [None, symbol "\\OVER"] @ aux p2
+    | Sub (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUB"] @ aux p2
+    | Sup (p1, p2) -> aux p1 @ [NoBinding, symbol "\\SUP"] @ aux p2
+    | Below (p1, p2) -> aux p1 @ [NoBinding, symbol "\\BELOW"] @ aux p2
+    | Above (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ABOVE"] @ aux p2
+    | Frac (p1, p2) -> aux p1 @ [NoBinding, symbol "\\FRAC"] @ aux p2
+    | Atop (p1, p2) -> aux p1 @ [NoBinding, symbol "\\ATOP"] @ aux p2
+    | Over (p1, p2) -> aux p1 @ [NoBinding, symbol "\\OVER"] @ aux p2
     | Root (p1, p2) ->
-        [None, symbol "\\ROOT"] @ aux p2 @ [None, symbol "\\OF"] @ aux p1
-    | Sqrt p -> [None, symbol "\\SQRT"] @ aux p
+        [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
+        @ aux p1
+    | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
     | Break -> []
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic = function
     | Opt p ->
         let p_bindings, p_atoms = List.split (aux p) in
         let p_names = flatten_opt p_bindings in
-        [ None,
+        [ Env,
           Gramext.srules
             [ [ Gramext.Sopt
                   (Gramext.srules
@@ -484,8 +494,12 @@ let extract_term_production pattern =
                         p_bindings)])],
               Gramext.action
                 (fun (env_opt : env_type option) (loc : location) ->
+                  Printf.printf "|p_names|=%d\n" (List.length p_names) ;
+                  flush stdout ;
                   match env_opt with
                     Some env ->
+                      Printf.printf "|env|=%d\n" (List.length env) ;
+                      flush stdout ;
                       prerr_endline "opt action (Some _)";
                       List.map
                         (fun (name, (typ, v)) ->
@@ -498,10 +512,11 @@ let extract_term_production pattern =
                           (name, (OptType typ, OptValue None)))
                         p_names) ]]
     | _ -> assert false
-  and aux_variable = function
-    | NumVar s -> [Some (s, NumType), number ""]
-    | TermVar s -> [Some (s, TermType), term]
-    | IdentVar s -> [Some (s, StringType), ident ""]
+  and aux_variable =
+    function
+    | NumVar s -> [Binding (s, NumType), number ""]
+    | TermVar s -> [Binding (s, TermType), term]
+    | IdentVar s -> [Binding (s, StringType), ident ""]
     | Ascription (p, s) -> assert false (* TODO *)
     | FreshVar _ -> assert false
   in

diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli
index 32ba0a318acff4c93b0692cd7cecc598149ac6df..ef6aa482c30fe8633a7057673253a9fd1b2f00f9 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.mli
+++ b/helm/ocaml/cic_notation/cicNotationParser.mli
@@ -55,6 +55,8 @@ val delete: rule_id -> unit
 (** {2 Debugging} *)
 
 val pp_env: env_type -> string
+val pp_value: CicNotationPt.value -> string
+val pp_value_type: CicNotationPt.value_type -> string
 
   (** print "level2_pattern" entry on stdout, flushing afterwards *)
 val print_l2_pattern: unit -> unit

diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml
index c068491a38898c07e5c7fc1f89c263f9d2b688ba..a8e2c45b0c6231901e2ce4fe131146609ad7cfd8 100644 (file)
--- a/helm/ocaml/cic_notation/test_parser.ml
+++ b/helm/ocaml/cic_notation/test_parser.ml
@@ -41,7 +41,12 @@ let _ =
       CicNotationParser.extend ~precedence:50 ~associativity:Gramext.LeftA
         (P.Layout (P.Box (P.H,
           [ P.Literal (`Symbol "+");
-            P.Magic (P.Opt (P.Variable (P.TermVar "ugo"))) ]
+            P.Magic (P.Opt (P.Layout (P.Box (P.H,
+              [ P.Variable (P.TermVar "ugo");
+                P.Literal (`Symbol "+");
+                P.Variable (P.TermVar "pino")
+              ]))));
+          ]
 (*           [ P.Variable (P.TermVar "a");
             P.Literal (`Symbol "+");
             P.Variable (P.TermVar "b");
@@ -52,10 +57,12 @@ let _ =
           prerr_endline "reducing rule" ;
           prerr_endline (sprintf "env = [ %s ]" (CicNotationParser.pp_env env));
 (*           match env with
-          [(x, (_, P.OptValue v))] ->
+          [(_, (_, P.OptValue v))] ->
               begin
                 match v with
-                Some _ -> Printf.printf "Ugo c'e'? %s\n" x; flush stdout
+                | Some x ->
+                    printf "Ugo c'e'? %s\n" (CicNotationParser.pp_value x);
+                    flush stdout
                 | None  -> prerr_endline "nooooo"
               end
            | _ -> assert false *)