| 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";
- 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:env_type) -> aux (v @ vl) tl)
- (* LUCA: DEFCON 2 END *)
+ Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
+ (* LUCA: DEFCON 5 END *)
in
aux [] (List.rev bindings)
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
| 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
- let action (env_list : env_type list) (loc : location) =
- prerr_endline "list action";
- List.fold_right grow_env env_list env0
+ in *)
+ let action (env_list : CicNotationEnv.t list) (loc : location) =
+ CicNotationEnv.coalesce_env p_names env_list
in
let g_symbol s =
match magic with
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
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
(** {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
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)))
]
[ "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))
(* }}} *)
(* {{{ 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
[ 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";
- t = level3_term ->
- ()
+ [ s = CSYMBOL; 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)
]
];
(* }}} *)
projects / helm.git / blobdiff