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)
+ [] -> 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)
| Binding (name, StringType) :: tl ->
- prerr_endline "aux: string";
Gramext.action
(fun (v:string) ->
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)
| Binding (name, OptType t) :: tl ->
- prerr_endline "aux: opt";
Gramext.action
(fun (v:'a option) ->
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)
| Env _ :: tl ->
- prerr_endline "aux: env";
Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
(* LUCA: DEFCON 5 END *)
in
| 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 ->
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
| 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))