| Env.OptType ty, Env.OptValue (Some v) ->
aux ((name, (ty, v)) :: acc) tl
| _ -> assert false)
- | _ :: tl -> aux acc tl
- (* some pattern may contain only meta names, thus we trash all others *)
+ | hd :: tl -> aux (hd :: acc) tl
| [] -> acc
in
aux [] env
new_name
in
let rec aux env term =
+(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
match term with
| Ast.AttributedTerm (_, term) -> aux env term
| Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
and aux_branch env (pattern, term) =
(aux_pattern env pattern, aux env term)
- and aux_pattern env (head, vars) =
- (head, List.map (aux_capture_var env) vars)
+ and aux_pattern env (head, hrefs, vars) =
+ (head, hrefs, List.map (aux_capture_var env) vars)
and aux_definition env (var, term, i) =
(aux_capture_var env var, aux env term, i)
and aux_substs env substs =
| Ast.Ascription (term, name) -> assert false
and aux_magic env = function
| Ast.Default (some_pattern, none_pattern) ->
- (match CicNotationUtil.names_of_term some_pattern with
+ let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
+ let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
+ let opt_names =
+ List.filter
+ (fun name -> not (List.mem name none_pattern_names))
+ some_pattern_names
+ in
+ (match opt_names with
| [] -> assert false (* some pattern must contain at least 1 name *)
| (name :: _) as names ->
(match Env.lookup_value env name with
*)
aux (unopt_names names env) some_pattern
| Env.OptValue None -> aux env none_pattern
- | _ -> assert false))
+ | _ ->
+ prerr_endline (sprintf
+ "lookup of %s in env %s did not return an optional value"
+ name (CicNotationPp.pp_env env));
+ assert false))
| Ast.Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =