module Ast = CicNotationPt
module Env = CicNotationEnv
-(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
- * be removes as soon as we believe implementation are equivalent *)
-(* let meta_names_of term =
- let rec names = ref [] in
- let add_name n =
- if List.mem n !names then ()
- else names := n :: !names
- in
- let rec aux = function
- | AttributedTerm (_, term) -> aux term
- | Appl terms -> List.iter aux terms
- | Binder (_, _, body) -> aux body
- | Case (term, indty, outty_opt, patterns) ->
- aux term ;
- aux_opt outty_opt ;
- List.iter aux_branch patterns
- | LetIn (_, t1, t2) ->
- aux t1 ;
- aux t2
- | LetRec (_, definitions, body) ->
- List.iter aux_definition definitions ;
- aux body
- | Uri (_, Some substs) -> aux_substs substs
- | Ident (_, Some substs) -> aux_substs substs
- | Meta (_, substs) -> aux_meta_substs substs
-
- | Implicit
- | Ident _
- | Num _
- | Sort _
- | Symbol _
- | Uri _
- | UserInput -> ()
-
- | Magic magic -> aux_magic magic
- | Variable var -> aux_variable var
-
- | _ -> assert false
- and aux_opt = function
- | Some term -> aux term
- | None -> ()
- and aux_capture_var (_, ty_opt) = aux_opt ty_opt
- and aux_branch (pattern, term) =
- aux_pattern pattern ;
- aux term
- and aux_pattern (head, vars) =
- List.iter aux_capture_var vars
- and aux_definition (var, term, i) =
- aux_capture_var var ;
- aux term
- and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
- and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
- and aux_variable = function
- | NumVar name -> add_name name
- | IdentVar name -> add_name name
- | TermVar name -> add_name name
- | FreshVar _ -> ()
- | Ascription _ -> assert false
- and aux_magic = function
- | Default (t1, t2)
- | Fold (_, t1, _, t2) ->
- aux t1 ;
- aux t2
- | _ -> assert false
- in
- aux term ;
- !names *)
-
let unopt_names names env =
let rec aux acc = function
| (name, (ty, v)) :: tl when List.mem name names ->
| 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 =