in
let rec aux t =
NotationUtil.visit_ast
+ ~clear_interpretation:true
~map_xref_option:(fun _ -> None)
~map_case_indty:(fun _ -> None)
~map_case_outtype:(fun _ _ -> None)
(* Debugging only *)
(*CSC: new NCicPp.status is the best I can do now *)
- let string_of_term = NotationPp.pp_term (new NCicPp.status)
- let string_of_pattern = NotationPp.pp_term (new NCicPp.status)
+ (*WR: can't guess a user id so I must use None *)
+ let string_of_term = NotationPp.pp_term (new NCicPp.status None)
+ let string_of_pattern = NotationPp.pp_term (new NCicPp.status None)
end
module M = PatternMatcher.Matcher (Pattern21)
name, (Env.TermType l, Env.TermValue t)
| Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
name, (Env.NumType, Env.NumValue s)
- | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
+ | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, `Ambiguous)) ->
name, (Env.StringType, Env.StringValue (Env.Ident s))
| _ -> assert false)
pl tl
let env'' = Env.remove_name env' acc_name in
match aux acc with
| None -> aux_base term
- | Some (base_env, ctors', rec_envl) ->
- let ctors'' = ctors' @ ctors in
+ | Some (base_env, ctors_acc, rec_envl) ->
+ let ctors'' = ctors' @ ctors_acc (* @ ctors *)in
Some (base_env, ctors'',env'' :: rec_envl)
end
in
match aux term with
| None -> None
- | Some (base_env, ctors, rec_envl) ->
+ | Some (base_env, ctors_term, rec_envl) ->
let env' =
base_env @ Env.coalesce_env p_rec_decls rec_envl @ env
(* @ env LUCA!!! *)
in
- Some (env', ctors))
+ Some (env', ctors_term @ ctors))
| Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
let p_some_decls = Env.declarations_of_term p_some in