prima implementazione di demodulate, superposition_left e superposition_right

[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 b408e6e3bea60fdd718e5354691c987b875d8bd3..6bc494cdc5801be74a740972c16abf665dd60c9d 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -79,40 +79,30 @@ type binding =
 let make_action action bindings =
   let rec aux (vl : CicNotationEnv.t) =
     function
-      [] ->
-        prerr_endline "aux: make_action";
-        Gramext.action (fun (loc: location) -> action vl loc)
-    | NoBinding :: tl ->
-        prerr_endline "aux: none";
-        Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 2 BEGIN *)
+      [] -> Gramext.action (fun (loc: location) -> action vl loc)
+    | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
+    (* LUCA: DEFCON 5 BEGIN *)
     | Binding (name, TermType) :: tl ->
-        prerr_endline "aux: term";
         Gramext.action
-          (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl)
+          (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
     | Binding (name, StringType) :: tl ->
-        prerr_endline "aux: string";
         Gramext.action
           (fun (v:string) ->
-            aux ((name, (StringType, (StringValue v))) :: vl) tl)
+            aux ((name, (StringType, StringValue v)) :: vl) tl)
     | Binding (name, NumType) :: tl ->
-        prerr_endline "aux: num";
         Gramext.action
-          (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl)
+          (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
     | Binding (name, OptType t) :: tl ->
-        prerr_endline "aux: opt";
         Gramext.action
           (fun (v:'a option) ->
-            aux ((name, (OptType t, (OptValue v))) :: vl) tl)
+            aux ((name, (OptType t, OptValue v)) :: vl) tl)
     | Binding (name, ListType t) :: tl ->
-        prerr_endline "aux: list";
         Gramext.action
           (fun (v:'a list) ->
-            aux ((name, (ListType t, (ListValue v))) :: vl) tl)
+            aux ((name, (ListType t, ListValue v)) :: vl) tl)
     | Env _ :: tl ->
-        prerr_endline "aux: env";
         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 2 END *)
+    (* LUCA: DEFCON 5 END *)
   in
     aux [] (List.rev bindings)
 
@@ -172,9 +162,8 @@ let extract_term_production pattern =
     | List0 (p, _)
     | List1 (p, _) ->
         let p_bindings, p_atoms, p_names, p_action = inner_pattern p in
-        let env0 = List.map list_binding_of_name p_names in
+(*         let env0 = List.map list_binding_of_name p_names in
         let grow_env_entry env n v =
-          prerr_endline "grow_env_entry";
           List.map
             (function
               | (n', (ty, ListValue vl)) as entry ->
@@ -183,14 +172,12 @@ let extract_term_production pattern =
             env
         in
         let grow_env env_i env =
-          prerr_endline "grow_env";
           List.fold_left
             (fun env (n, (_, v)) -> grow_env_entry env n v)
             env env_i
-        in
+        in *)
         let action (env_list : CicNotationEnv.t list) (loc : location) =
-          prerr_endline "list action";
-          List.fold_right grow_env env_list env0
+          CicNotationEnv.coalesce_env p_names env_list
         in
         let g_symbol s =
           match magic with
@@ -257,10 +244,6 @@ let delete atoms = Grammar.delete_rule l2_pattern atoms
 
 (** {2 Grammar} *)
 
-let boxify = function
-  | [ a ] -> a
-  | l -> Layout (Box (H, l))
-
 let fold_binder binder pt_names body =
   let fold_cluster binder terms ty body =
     List.fold_right
@@ -342,7 +325,7 @@ EXTEND
           return_term loc (Layout (Box (V, p)))
       | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
       | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
-          return_term loc (boxify p)
+          return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->
           return_term loc (Variable (Ascription (p, id)))
       ]
@@ -510,8 +493,9 @@ EXTEND
     [ "90" NONA
       [ id = IDENT -> return_term loc (Ident (id, None))
       | id = IDENT; s = explicit_subst -> return_term loc (Ident (id, Some s))
+      | s = CSYMBOL -> return_term loc (Symbol (s, 0))
       | u = URI -> return_term loc (Uri (u, None))
-      | n = NUMBER -> prerr_endline "number"; return_term loc (Num (n, 0))
+      | n = NUMBER -> return_term loc (Num (n, 0))
       | IMPLICIT -> return_term loc (Implicit)
       | m = META -> return_term loc (Meta (int_of_string m, []))
       | m = META; s = meta_substs -> return_term loc (Meta (int_of_string m, s))
@@ -537,15 +521,15 @@ EXTEND
 (* }}} *)
 (* {{{ Grammar for interpretation, notation level 3 *)
   argument: [
-    [ id = IDENT -> IdentArg id
-    | SYMBOL <:unicode<eta>> (* η *); SYMBOL "."; a = SELF -> EtaArg (None, a)
-    | SYMBOL <:unicode<eta>> (* η *); id = IDENT; SYMBOL "."; a = SELF ->
-        EtaArg (Some id, a)
+    [ id = IDENT -> IdentArg (0, id)
+    | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
+      SYMBOL "."; id = IDENT ->
+        IdentArg (List.length l, id)
     ]
   ];
   level3_term: [
     [ u = URI -> UriPattern u
-    | a = argument -> ArgPattern a
+    | id = IDENT -> VarPattern id
     | SYMBOL "("; terms = LIST1 SELF; SYMBOL ")" ->
         (match terms with
         | [] -> assert false
@@ -572,8 +556,7 @@ EXTEND
     ]
   ];
   interpretation: [
-    [ s = SYMBOL; args = LIST1 argument; SYMBOL "=";
-      t = level3_term ->
+    [ s = CSYMBOL; args = LIST1 argument; SYMBOL "="; t = level3_term ->
         (s, args, t)
     ]
   ];