| Gramext.RightA -> "RightA"
| Gramext.NonA -> "NonA"
-let pp_pos =
- function
- `None -> "`None"
- | `Left -> "`Left"
- | `Right -> "`Right"
- | `Inner -> "`Inner"
-
let is_atomic t =
let rec aux_mpres = function
| Mpres.Mi _
let new_level = ref None in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
+ let new_pos = ref pos in
let rec aux_attribute =
function
| A.AttributedTerm (attr, t) ->
| `Level (child_prec, child_assoc) ->
new_level := Some (child_prec, child_assoc)
| `IdRef xref -> new_xref := xref :: !new_xref
+ | `ChildPos pos -> new_pos := pos
| `XmlAttrs attrs -> new_xmlattrs := attrs @ !new_xmlattrs);
aux_attribute t
| t ->
(match !new_level with
- | None -> aux !new_xmlattrs mathonly new_xref pos prec t
+ | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
| Some (child_prec, child_assoc) ->
let t' =
- aux !new_xmlattrs mathonly new_xref pos child_prec t
+ aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
in
- add_parens child_prec child_assoc pos prec t')
+ add_parens child_prec child_assoc !new_pos prec t')
in
aux_attribute t
and aux_literal xmlattrs xref prec l =
| (A.Layout A.Break) :: tl ->
aux_list first (List.rev acc :: clusters) [] tl
| [hd] ->
- let pos' =
- if first then
- pos
- else
- match pos with
- `None -> `Right
- | `Inner -> `Inner
- | `Right -> `Right
- | `Left -> `Inner
- in
+(* let pos' =
+ if first then
+ pos
+ else
+ match pos with
+ `None -> `Right
+ | `Inner -> `Inner
+ | `Right -> `Right
+ | `Left -> `Inner
+ in *)
aux_list false clusters
- (aux [] mathonly xref pos' prec hd :: acc) []
+ (aux [] mathonly xref pos prec hd :: acc) []
| hd :: tl ->
- let pos' =
- match pos, first with
- `None, true -> `Left
- | `None, false -> `Inner
- | `Left, true -> `Left
- | `Left, false -> `Inner
- | `Right, _ -> `Inner
- | `Inner, _ -> `Inner
- in
+(* let pos' =
+ match pos, first with
+ `None, true -> `Left
+ | `None, false -> `Inner
+ | `Left, true -> `Left
+ | `Left, false -> `Inner
+ | `Right, _ -> `Inner
+ | `Inner, _ -> `Inner
+ in *)
aux_list false clusters
- (aux [] mathonly xref pos' prec hd :: acc) tl
+ (aux [] mathonly xref pos prec hd :: acc) tl
in
aux_list true [] []
in
| `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
projects / helm.git / commitdiff