]> matita.cs.unibo.it Git - helm.git/commitdiff
initial support for notation that specifies the precedence of term variables, that...
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 18 Jun 2008 15:03:32 +0000 (15:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 18 Jun 2008 15:03:32 +0000 (15:03 +0000)
helm/software/components/acic_content/cicNotationEnv.ml
helm/software/components/acic_content/cicNotationEnv.mli
helm/software/components/acic_content/cicNotationPp.ml
helm/software/components/acic_content/cicNotationPt.ml
helm/software/components/acic_content/cicNotationUtil.ml
helm/software/components/content_pres/cicNotationParser.ml
helm/software/components/content_pres/cicNotationPres.ml
helm/software/components/content_pres/content2presMatcher.ml
helm/software/components/content_pres/termContentPres.ml

index 32d4f0df5e699043505022a31d48d3baa91a7d82..5a1c4c9458d1f216ba047643e380349b4bdaec81 100644 (file)
@@ -35,7 +35,7 @@ type value =
   | ListValue of value list
 
 type value_type =
-  | TermType
+  | TermType of (int * Gramext.g_assoc) option
   | StringType
   | NumType
   | OptType of value_type
@@ -98,7 +98,7 @@ let list_declaration (n, ty) = (n, ListType ty)
 let declaration_of_var = function
   | Ast.NumVar s -> s, NumType
   | Ast.IdentVar s -> s, StringType
-  | Ast.TermVar s -> s, TermType
+  | Ast.TermVar (s,l) -> s, TermType l
   | _ -> assert false
 
 let value_of_term = function
@@ -114,7 +114,7 @@ let term_of_value = function
 
 let rec well_typed ty value =
   match ty, value with
-  | TermType, TermValue _
+  | TermType _, TermValue _
   | StringType, StringValue _
   | OptType _, OptValue None
   | NumType, NumValue _ -> true
index d4f87097e2fa2c50d86a56b6b55d985e2a72032c..5d2bba6c7dee698db593da7980cdc78afdb9e488 100644 (file)
@@ -33,7 +33,7 @@ type value =
   | ListValue of value list
 
 type value_type =
-  | TermType
+  | TermType of (int * Gramext.g_assoc) option
   | StringType
   | NumType
   | OptType of value_type
index 6ea839ce322afff694ad1af077b2253a31730aba..7fbc9f492225c1db508e1241c73eddcf81e6f07c 100644 (file)
@@ -56,9 +56,9 @@ let pp_literal =
 
 let pp_assoc =
   function
-  | Gramext.NonA -> "NonA"
-  | Gramext.LeftA -> "LeftA"
-  | Gramext.RightA -> "RightA"
+  | Gramext.NonA -> "N"
+  | Gramext.LeftA -> "L"
+  | Gramext.RightA -> "R"
 
 let pp_pos =
   function
@@ -256,7 +256,8 @@ and pp_sep_opt = function
 and pp_variable = function
   | Ast.NumVar s -> "number " ^ s
   | Ast.IdentVar s -> "ident " ^ s
-  | Ast.TermVar s -> "term " ^ s
+  | Ast.TermVar (s,None) -> s
+  | Ast.TermVar (s,Some (l,a)) -> "term " ^string_of_int l ^ " " ^ pp_assoc a ^ " " ^ s
   | Ast.Ascription (t, n) -> assert false
   | Ast.FreshVar n -> "fresh " ^ n
 
@@ -333,7 +334,8 @@ let rec pp_value = function
 
 let rec pp_value_type =
   function
-  | Env.TermType -> "Term"
+  | Env.TermType None -> "Term"
+  | Env.TermType (Some (l,a)) -> "Term "^string_of_int l ^ " " ^ pp_assoc a 
   | Env.StringType -> "String"
   | Env.NumType -> "Number"
   | Env.OptType t -> "Maybe " ^ pp_value_type t
index cc481ff0a913e9129d5ce78dc6b7456e0ad8f449..92d081fee84096994b39d788de5bd52bb8fecf20 100644 (file)
@@ -63,7 +63,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 2
+let magic = 3
 
 type term =
   (* CIC AST *)
@@ -145,7 +145,7 @@ and pattern_variable =
   (* level 1 and 2 variables *)
   | NumVar of string
   | IdentVar of string
-  | TermVar of string
+  | TermVar of string * (int * Gramext.g_assoc) option
 
   (* level 1 variables *)
   | Ascription of term * string
index 51acf758f080d427cb43ff4370a00b0c63eba833..d4a55b353adf41221cd44958e294c6ef38ee59a9 100644 (file)
@@ -136,7 +136,7 @@ let names_of_term t =
   let aux = function
     | Ast.NumVar s
     | Ast.IdentVar s
-    | Ast.TermVar s -> s
+    | Ast.TermVar (s,_) -> s
     | _ -> assert false
   in
     List.map aux (variables_of_term t)
@@ -229,7 +229,7 @@ let meta_names_of_term term =
   and aux_variable = function
     | Ast.NumVar name -> add_name name
     | Ast.IdentVar name -> add_name name
-    | Ast.TermVar name -> add_name name
+    | Ast.TermVar (name,_) -> add_name name
     | Ast.FreshVar _ -> ()
     | Ast.Ascription _ -> assert false
   and aux_magic = function
index bae4a8f593628821b0f8d1181563aa7e496222b8..7690aeb9b7464ffaae36a13b6c918acbe93fa268 100644 (file)
@@ -57,11 +57,26 @@ let int_of_string s =
 
 (** {2 Grammar extension} *)
 
+let level_of precedence associativity =
+  if precedence < min_precedence || precedence > max_precedence then
+    raise (Level_not_found precedence);
+  let assoc_string = 
+    match associativity with
+    | Gramext.NonA -> "N"
+    | Gramext.LeftA -> "L"
+    | Gramext.RightA -> "R"
+  in
+  string_of_int precedence ^ assoc_string
+
 let gram_symbol s = Gramext.Stoken ("SYMBOL", s)
 let gram_ident s = Gramext.Stoken ("IDENT", s)
 let gram_number s = Gramext.Stoken ("NUMBER", s)
 let gram_keyword s = Gramext.Stoken ("", s)
-let gram_term = Gramext.Sself
+let gram_term = function
+  | None -> Gramext.Sself
+  | Some (precedence, associativity) ->
+      Gramext.Snterml (Grammar.Entry.obj (term: 'a Grammar.Entry.e),level_of precedence associativity)
+;;
 
 let gram_of_literal =
   function
@@ -80,10 +95,10 @@ let make_action action bindings =
       [] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
     | NoBinding :: tl -> Gramext.action (fun _ -> aux vl tl)
     (* LUCA: DEFCON 3 BEGIN *)
-    | Binding (name, Env.TermType) :: tl ->
+    | Binding (name, Env.TermType l) :: tl ->
         Gramext.action
           (fun (v:Ast.term) ->
-            aux ((name, (Env.TermType, Env.TermValue v))::vl) tl)
+            aux ((name, (Env.TermType l, Env.TermValue v))::vl) tl)
     | Binding (name, Env.StringType) :: tl ->
         Gramext.action
           (fun (v:string) ->
@@ -198,7 +213,8 @@ let extract_term_production pattern =
   and aux_variable =
     function
     | Ast.NumVar s -> [Binding (s, Env.NumType), gram_number ""]
-    | Ast.TermVar s -> [Binding (s, Env.TermType), gram_term]
+    | Ast.TermVar (s,level) -> 
+        [Binding (s, Env.TermType level), gram_term level]
     | Ast.IdentVar s -> [Binding (s, Env.StringType), gram_ident ""]
     | Ast.Ascription (p, s) -> assert false (* TODO *)
     | Ast.FreshVar _ -> assert false
@@ -213,17 +229,6 @@ let extract_term_production pattern =
   in
   aux pattern
 
-let level_of precedence associativity =
-  if precedence < min_precedence || precedence > max_precedence then
-    raise (Level_not_found precedence);
-  let assoc_string =
-    match associativity with
-    | Gramext.NonA -> "N"
-    | Gramext.LeftA -> "L"
-    | Gramext.RightA -> "R"
-  in
-  string_of_int precedence ^ assoc_string
-
 type rule_id = Grammar.token Gramext.g_symbol list
 
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
@@ -334,8 +339,15 @@ EXTEND
     | "opt";   p = l1_simple_pattern -> Ast.Opt p
     ]
   ];
+  l1_associativity : [
+   [ IDENT "L" -> Gramext.LeftA
+   | IDENT "N" -> Gramext.NonA
+   | IDENT "R" -> Gramext.RightA
+   ]
+  ];
   l1_pattern_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; assoc = l1_associativity ; id = IDENT -> 
+        Ast.TermVar (id, Some (int_of_string precedence,assoc))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     ]
@@ -375,7 +387,7 @@ EXTEND
           return_term loc (CicNotationUtil.group p)
       ]
     | "simple" NONA
-      [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar i))
+      [ i = IDENT -> return_term loc (Ast.Variable (Ast.TermVar (i,None)))
       | m = l1_magic_pattern -> return_term loc (Ast.Magic m)
       | v = l1_pattern_variable -> return_term loc (Ast.Variable v)
       | l = literal -> return_term loc (Ast.Literal l)
@@ -387,13 +399,20 @@ EXTEND
 (* {{{ Grammar for ast magics, notation level 2 *)
 EXTEND
   GLOBAL: level2_meta;
+  l2_associativity : [
+   [ IDENT "L" -> Gramext.LeftA
+   | IDENT "N" -> Gramext.NonA
+   | IDENT "R" -> Gramext.RightA
+   ]
+  ];
   l2_variable: [
-    [ "term"; id = IDENT -> Ast.TermVar id
+    [ "term"; precedence = NUMBER; assoc = l2_associativity; id = IDENT -> 
+        Ast.TermVar (id,Some (int_of_string precedence, assoc))
     | "number"; id = IDENT -> Ast.NumVar id
     | "ident"; id = IDENT -> Ast.IdentVar id
     | "fresh"; id = IDENT -> Ast.FreshVar id
-    | "anonymous" -> Ast.TermVar "_"
-    | id = IDENT -> Ast.TermVar id
+    | "anonymous" -> Ast.TermVar ("_",None)
+    | id = IDENT -> Ast.TermVar (id,None)
     ]
   ];
   l2_magic: [
@@ -481,7 +500,7 @@ EXTEND
         let meta = !parse_level2_meta_ref (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
-        | Ast.Variable (Ast.TermVar "_") -> [Ast.Ident ("_", None)], None
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
@@ -492,7 +511,7 @@ EXTEND
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar "_") -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
         | _ -> failwith "Invalid index name."
     ]
   ];
index 673df335f224d4db81427637f1c185bb31e2a9bb..a7bce6437520b8c36361deac9e29e6fe225cf5e8 100644 (file)
@@ -197,7 +197,7 @@ let add_parens child_prec child_assoc child_pos curr_prec t =
           child_assoc = Gramext.RightA &&
           child_pos <> `Right))
   then begin (* parens should be added *)
-(*     prerr_endline "adding parens!"; *)
+(*      prerr_endline "adding parens!";  *)
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
@@ -324,7 +324,8 @@ let render ids_to_uris ?(prec=(-1)) =
         assert false
   and aux_attributes xmlattrs mathonly xref pos prec t =
     let reset = ref false in
-    let new_level = ref None in
+    let inferred_level = ref None in
+    let expected_level = ref None in
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
     let new_pos = ref pos in
@@ -337,14 +338,21 @@ let render ids_to_uris ?(prec=(-1)) =
           | `Raw _ -> ()
           | `Level (-1, _) -> reset := true
           | `Level (child_prec, child_assoc) ->
-              new_level := Some (child_prec, child_assoc)
+              assert (!expected_level = None);
+              expected_level := !inferred_level;
+              inferred_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 !new_pos prec t
+          let prec = 
+            match !expected_level with
+            | None -> prec
+            | Some (prec, _) -> prec
+          in
+          (match !inferred_level with
+          | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t 
           | Some (child_prec, child_assoc) ->
               let t' = 
                 aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
index 7e080ea6956a901180b40f719be98753af00267a..bcb4257bfda353f4f0ba7fe010d3590da5ca674b 100644 (file)
@@ -73,7 +73,7 @@ struct
     let add_magic m =
       let name = Util.fresh_name () in
       magic_map := (name, m) :: !magic_map;
-      Ast.Variable (Ast.TermVar name)
+      Ast.Variable (Ast.TermVar (name,None))
     in
     let rec aux = function
       | Ast.AttributedTerm (_, t) -> assert false
@@ -91,8 +91,8 @@ struct
       List.map2
         (fun p t ->
           match p, t with
-            Ast.Variable (Ast.TermVar name), _ ->
-              name, (Env.TermType, Env.TermValue t)
+          | Ast.Variable (Ast.TermVar (name,l)), _ ->
+              name, (Env.TermType l, Env.TermValue t)
           | Ast.Variable (Ast.NumVar name), (Ast.Num (s, _)) ->
               name, (Env.NumType, Env.NumValue s)
           | Ast.Variable (Ast.IdentVar name), (Ast.Ident (s, None)) ->
index e83fbc92373f8e8b137d730851bc1e75e166e673..8f15664d0342fb7bdeb1b5131863e90f97d577bd 100644 (file)
@@ -330,7 +330,14 @@ let instantiate21 idrefs env l1 =
         (* following assertion should be a conditional that makes this
          * instantiation fail *)
         assert (CicNotationEnv.well_typed expected_ty value);
-        [ add_pos_info pos (CicNotationEnv.term_of_value value) ]
+        let value = CicNotationEnv.term_of_value value in
+        let value = 
+          match expected_ty with
+          | Env.TermType (Some l) -> 
+              Ast.AttributedTerm (`Level l,value) 
+          | _ -> value
+        in
+        [ add_pos_info pos value ]
     | Ast.Magic m -> subst_magic pos env m
     | Ast.Literal l as t ->
         let t = add_idrefs idrefs t in
@@ -545,7 +552,7 @@ let instantiate_level2 env term =
       new_name
   in
   let rec aux env term =
-(*     prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
+(*    prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
     match term with
     | Ast.AttributedTerm (_, term) -> aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
@@ -596,7 +603,10 @@ let instantiate_level2 env term =
   and aux_variable env = function
     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
     | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
-    | Ast.TermVar name -> Env.lookup_term env name
+    | Ast.TermVar (name,None) -> 
+        Env.lookup_term env name
+    | Ast.TermVar (name,Some l) -> 
+        Ast.AttributedTerm (`Level l,Env.lookup_term env name)
     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
     | Ast.Ascription (term, name) -> assert false
   and aux_magic env = function
@@ -637,7 +647,7 @@ let instantiate_level2 env term =
               | Env.ListValue (_ :: _) ->
                   instantiate_fold_left 
                     (let acc_binding =
-                      acc_name, (Env.TermType, Env.TermValue acc)
+                      acc_name, (Env.TermType None, Env.TermValue acc)
                      in
                      aux (acc_binding :: head_names names env') rec_pattern)
                     (tail_names names env')
@@ -659,7 +669,7 @@ let instantiate_level2 env term =
               | Env.ListValue (_ :: _) ->
                   let acc = instantiate_fold_right (tail_names names env') in
                   let acc_binding =
-                    acc_name, (Env.TermType, Env.TermValue acc)
+                    acc_name, (Env.TermType None, Env.TermValue acc)
                   in
                   aux (acc_binding :: head_names names env') rec_pattern
               | Env.ListValue [] -> aux env base_pattern