* http://helm.cs.unibo.it/
*)
+open Printf
+
open CicNotationEnv
open CicNotationPt
-let meta_names_of term =
+(* 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 ()
| _ -> assert false
in
aux term ;
- !names
+ !names *)
let unopt_names names env =
let rec aux acc = function
| Ascription (term, name) -> assert false
and aux_magic env = function
| Default (some_pattern, none_pattern) ->
- (match meta_names_of some_pattern with
+ (match CicNotationUtil.names_of_term some_pattern with
| [] -> assert false (* some pattern must contain at least 1 name *)
| (name :: _) as names ->
(match lookup_value env name with
| Fold (`Left, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ List.filter ((<>) acc_name)
+ (CicNotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_left acc env' =
- prerr_endline "instantiate_fold_left";
match lookup_value env' name with
| ListValue (_ :: _) ->
instantiate_fold_left
| Fold (`Right, base_pattern, names, rec_pattern) ->
let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
let meta_names =
- List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+ List.filter ((<>) acc_name)
+ (CicNotationUtil.names_of_term rec_pattern)
in
(match meta_names with
| [] -> assert false (* as above *)
| (name :: _) as names ->
let rec instantiate_fold_right env' =
- prerr_endline "instantiate_fold_right";
match lookup_value env' name with
| ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
| _ -> assert false
in
instantiate_fold_right env)
+ | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t))
+ | Fail -> assert false
| _ -> assert false
in
aux env term
+let instantiate_appl_pattern env appl_pattern =
+ let lookup name =
+ try List.assoc name env
+ with Not_found ->
+ prerr_endline (sprintf "Name %s not found" name);
+ assert false
+ in
+ let rec aux = function
+ | UriPattern uri -> CicUtil.term_of_uri uri
+ | ImplicitPattern -> Cic.Implicit None
+ | VarPattern name -> lookup name
+ | ApplPattern terms -> Cic.Appl (List.map aux terms)
+ in
+ aux appl_pattern
+