open CicNotationPt
- (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name =
- let index = ref ~-1 in
- fun () ->
- incr index;
- "fresh" ^ string_of_int !index
-
(* let meta_names_of term = *)
(* let rec names = ref [] in *)
(* let add_name n = *)
Binder (kind, aux_capture_variable var, k body)
| Case (term, indtype, typ, patterns) ->
Case (k term, indtype, aux_opt typ, aux_patterns patterns)
+ | Cast (t1, t2) -> Cast (k t1, k t2)
| LetIn (var, t1, t2) -> LetIn (aux_capture_variable var, k t1, k t2)
| LetRec (kind, definitions, term) ->
let definitions =
| [ a ] -> a
| l -> Layout (Box ((H, false, false), l))
+let unboxify = function
+ | Layout (Box ((H, false, false), [ a ])) -> a
+ | l -> l
+
let group = function
| [ a ] -> a
| l -> Layout (Group l)
in
aux []
-let dress sauce =
+let dress ~sep:sauce =
let rec aux =
function
| [] -> []
in
aux
+let dressn ~sep:sauces =
+ let rec aux =
+ function
+ | [] -> []
+ | [hd] -> [hd]
+ | hd :: tl -> hd :: sauces @ aux tl
+ in
+ aux
+
let find_appl_pattern_uris ap =
let rec aux acc =
function
- | GrafiteAst.UriPattern uri ->
+ | UriPattern uri ->
(try
ignore (List.find (fun uri' -> UriManager.eq uri uri') acc);
acc
with Not_found -> uri :: acc)
- | GrafiteAst.VarPattern _ -> acc
- | GrafiteAst.ApplPattern apl -> List.fold_left aux acc apl
+ | ImplicitPattern
+ | VarPattern _ -> acc
+ | ApplPattern apl -> List.fold_left aux acc apl
in
aux [] ap
Magic (If (_, Magic Fail, t)) -> find_branch t
| Magic (If (_, t, _)) -> find_branch t
| t -> t
+
+let cic_name_of_name = function
+ | CicNotationPt.Ident ("_", None) -> Cic.Anonymous
+ | CicNotationPt.Ident (name, None) -> Cic.Name name
+ | _ -> assert false
+
+let name_of_cic_name =
+ let add_dummy_xref t = CicNotationPt.AttributedTerm (`IdRef "", t) in
+ function
+ | Cic.Name s -> add_dummy_xref (CicNotationPt.Ident (s, None))
+ | Cic.Anonymous -> add_dummy_xref (CicNotationPt.Ident ("_", None))
+
+let fresh_index = ref ~-1
+
+type notation_id = int
+
+let fresh_id () =
+ incr fresh_index;
+ !fresh_index
+
+ (* TODO ensure that names generated by fresh_var do not clash with user's *)
+let fresh_name () = "fresh" ^ string_of_int (fresh_id ())
+