From dfdff98e4417bae54fcf31d49c8a4d718c4487c2 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 27 Sep 2005 16:37:13 +0000 Subject: [PATCH] changed precedence/associativeness handling: relative position of children wrt its (box-)parent is now statically computed starting from the level1 pattern --- helm/ocaml/cic_notation/cicNotationPres.ml | 57 ++++++++++----------- helm/ocaml/cic_notation/cicNotationPt.ml | 3 ++ helm/ocaml/cic_notation/cicNotationRew.ml | 59 +++++++++++++++------- 3 files changed, 71 insertions(+), 48 deletions(-) diff --git a/helm/ocaml/cic_notation/cicNotationPres.ml b/helm/ocaml/cic_notation/cicNotationPres.ml index f838521b2..bed2cdd4d 100644 --- a/helm/ocaml/cic_notation/cicNotationPres.ml +++ b/helm/ocaml/cic_notation/cicNotationPres.ml @@ -148,13 +148,6 @@ let pp_assoc = | 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 _ @@ -304,6 +297,7 @@ let render ids_to_uris = 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) -> @@ -313,16 +307,17 @@ let render ids_to_uris = | `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 = @@ -374,30 +369,30 @@ let render ids_to_uris = | (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 diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml index 1dc634930..d889b0981 100644 --- a/helm/ocaml/cic_notation/cicNotationPt.ml +++ b/helm/ocaml/cic_notation/cicNotationPt.ml @@ -41,10 +41,13 @@ let fail floc msg = type href = UriManager.uri +type child_pos = [ `None | `Left | `Right | `Inner ] + type term_attribute = [ `Loc of location (* source file location *) | `IdRef of string (* ACic pointer *) | `Level of int * Gramext.g_assoc (* precedence, associativity *) + | `ChildPos of child_pos (* position of l1 pattern variables *) | `XmlAttrs of (string option * string * string) list (* list of XML attributes: namespace, name, value *) | `Raw of string (* unparsed version *) diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml index b1892e64a..4a02c8fff 100644 --- a/helm/ocaml/cic_notation/cicNotationRew.ml +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -73,6 +73,7 @@ let resolve_binder = function | `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 @@ -426,14 +427,15 @@ let add_idrefs = 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 = @@ -447,16 +449,16 @@ let instantiate21 idrefs env l1 = (* 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 @@ -473,10 +475,11 @@ let instantiate21 idrefs env l1 = | [] -> 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 @@ -496,15 +499,37 @@ let instantiate21 idrefs env l1 = 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 -- 2.39.2