| `Exists -> "\\exists"
let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t)
+let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t)
let rec remove_level_info =
function
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
let instantiate21 idrefs env l1 =
- let rec subst_singleton env =
+ let rec subst_singleton pos env =
function
Ast.AttributedTerm (attr, t) ->
- Ast.AttributedTerm (attr, subst_singleton env t)
- | t -> CicNotationUtil.group (subst env t)
- and subst env = function
+ Ast.AttributedTerm (attr, subst_singleton pos env t)
+ | t -> CicNotationUtil.group (subst pos env t)
+ and subst pos env = function
| Ast.AttributedTerm (attr, t) as term ->
- subst env t
+ prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr);
+ subst pos env t
| Ast.Variable var ->
let name, expected_ty = CicNotationEnv.declaration_of_var var in
let ty, value =
(* following assertion should be a conditional that makes this
* instantiation fail *)
assert (CicNotationEnv.well_typed expected_ty value);
- [ CicNotationEnv.term_of_value value ]
- | Ast.Magic m -> subst_magic env m
+ [ add_pos_info pos (CicNotationEnv.term_of_value value) ]
+ | Ast.Magic m -> subst_magic pos env m
| Ast.Literal l as t ->
let t = add_idrefs idrefs t in
(match l with
| `Keyword k -> [ add_keyword_attrs t ]
| _ -> [ t ])
- | Ast.Layout l -> [ Ast.Layout (subst_layout env l) ]
- | t -> [ CicNotationUtil.visit_ast (subst_singleton env) t ]
- and subst_magic env = function
+ | Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
+ | t -> [ CicNotationUtil.visit_ast (subst_singleton pos env) t ]
+ and subst_magic pos env = function
| Ast.List0 (p, sep_opt)
| Ast.List1 (p, sep_opt) ->
let rec_decls = CicNotationEnv.declarations_of_term p in
| [] -> List.rev acc
| value_set :: [] ->
let env = CicNotationEnv.combine rec_decls value_set in
- instantiate_list (CicNotationUtil.group (subst env p) :: acc) []
+ instantiate_list (CicNotationUtil.group (subst pos env p) :: acc)
+ []
| value_set :: tl ->
let env = CicNotationEnv.combine rec_decls value_set in
- let terms = subst env p in
+ let terms = subst pos env p in
instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl
in
instantiate_list [] values
begin
match env with
| [] -> []
- | _ -> subst env p
+ | _ -> subst pos env p
end
| _ -> assert false (* impossible *)
- and subst_layout env = function
+ and subst_layout pos env = function
| Ast.Box (kind, tl) ->
- Ast.Box (kind, List.concat (List.map (subst env) tl))
- | l -> CicNotationUtil.visit_layout (subst_singleton env) l
+ let tl' = subst_children pos env tl in
+ Ast.Box (kind, List.concat tl')
+ | l -> CicNotationUtil.visit_layout (subst_singleton pos env) l
+ and subst_children pos env =
+ function
+ | [] -> []
+ | [ child ] ->
+ let pos' =
+ match pos with
+ | `Inner -> `Right
+ | `Left -> `Left
+ | `None -> assert false
+ | `Right -> `Right
+ in
+ [ subst pos' env child ]
+ | hd :: tl ->
+ let pos' =
+ match pos with
+ | `Inner -> `Inner
+ | `Left -> `Inner
+ | `None -> assert false
+ | `Right -> `Right
+ in
+ (subst pos env hd) :: subst_children pos' env tl
in
- subst_singleton env l1
+ subst_singleton `Left env l1
let rec pp_ast1 term =
let rec pp_value = function