]> matita.cs.unibo.it Git - helm.git/commitdiff
changed precedence/associativeness handling: relative position of children wrt its...
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 27 Sep 2005 16:37:13 +0000 (16:37 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 27 Sep 2005 16:37:13 +0000 (16:37 +0000)
helm/ocaml/cic_notation/cicNotationPres.ml
helm/ocaml/cic_notation/cicNotationPt.ml
helm/ocaml/cic_notation/cicNotationRew.ml

index f838521b231333ededbac6cd0f5feaba502335d3..bed2cdd4d1296638be09f7380c43d1cc41543d32 100644 (file)
@@ -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
index 1dc6349309cc68429a0596ef73af821a976766ad..d889b0981432ba0d7df18189190639e76306b2ab 100644 (file)
@@ -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 *)
index b1892e64a1973fe767afb237c7285d931f5d1e95..4a02c8fff2affac5115259a96257184cbf25c847 100644 (file)
@@ -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