snapshot (first version with [apparently] working mappings between level

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

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index c7cc77be0a5f37b0978cdd817f4e239c1e46ce52..b408e6e3bea60fdd718e5354691c987b875d8bd3 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -77,7 +77,7 @@ type binding =
   | Env of (string * value_type) list
 
 let make_action action bindings =
-  let rec aux (vl : env_type) =
+  let rec aux (vl : CicNotationEnv.t) =
     function
       [] ->
         prerr_endline "aux: make_action";
@@ -111,7 +111,7 @@ let make_action action bindings =
             aux ((name, (ListType t, (ListValue v))) :: vl) tl)
     | Env _ :: tl ->
         prerr_endline "aux: env";
-        Gramext.action (fun (v:env_type) -> aux (v @ vl) tl)
+        Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
     (* LUCA: DEFCON 2 END *)
   in
     aux [] (List.rev bindings)
@@ -160,7 +160,7 @@ let extract_term_production pattern =
     match magic with
     | Opt p ->
         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-        let action (env_opt : env_type option) (loc : location) =
+        let action (env_opt : CicNotationEnv.t option) (loc : location) =
           match env_opt with
           | Some env -> List.map opt_binding_some env
           | None -> List.map opt_binding_of_name p_names
@@ -188,7 +188,7 @@ let extract_term_production pattern =
             (fun env (n, (_, v)) -> grow_env_entry env n v)
             env env_i
         in
-        let action (env_list : env_type list) (loc : location) =
+        let action (env_list : CicNotationEnv.t list) (loc : location) =
           prerr_endline "list action";
           List.fold_right grow_env env_list env0
         in
@@ -217,7 +217,8 @@ let extract_term_production pattern =
     let p_names = flatten_opt p_bindings in
     let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in
     let action =
-      make_action (fun (env : env_type) (loc : location) -> prerr_endline "inner action"; env) p_bindings
+      make_action (fun (env : CicNotationEnv.t) (loc : location) -> env)
+        p_bindings
     in
     p_bindings, p_atoms, p_names, action
   in
@@ -247,7 +248,7 @@ let extend level1_pattern ?(precedence = default_precedence)
           associativity,
           [ p_atoms, 
             (make_action
-              (fun (env: env_type) (loc: location) -> (action env loc))
+              (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc))
               p_bindings) ]]]
   in
   p_atoms
@@ -564,25 +565,27 @@ EXTEND
     [ IDENT "with"; IDENT "precedence"; n = NUMBER -> int_of_string n ]
   ];
   notation: [
-    [ IDENT "notation";
-      p1 = level1_pattern;
+    [ p1 = level1_pattern;
       assoc = OPT associativity; prec = OPT precedence;
       IDENT "for"; p2 = level2_pattern ->
         (p1, assoc, prec, p2)
     ]
   ];
   interpretation: [
-    [ IDENT "interpretation"; s = SYMBOL; args = LIST1 argument; IDENT "as";
+    [ s = SYMBOL; args = LIST1 argument; SYMBOL "=";
       t = level3_term ->
-        ()
+        (s, args, t)
     ]
   ];
 (* }}} *)
 (* {{{ Top-level phrases *)
   phrase: [
     [ IDENT "print"; p2 = level2_pattern; SYMBOL "." -> Print p2
-    | (l1, assoc, prec, l2) = notation; SYMBOL "." ->
+    | IDENT "notation"; (l1, assoc, prec, l2) = notation; SYMBOL "." ->
         Notation (l1, assoc, prec, l2)
+    | IDENT "interpretation"; (symbol, args, l3) = interpretation; SYMBOL "." ->
+        Interpretation ((symbol, args), l3)
+    | IDENT "render"; u = URI; SYMBOL "." -> Render (UriManager.uri_of_string u)
     ]
   ];
 (* }}} *)