From: Enrico Tassi Date: Wed, 18 Jun 2008 15:03:32 +0000 (+0000) Subject: initial support for notation that specifies the precedence of term variables, that... X-Git-Tag: make_still_working~5016 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcf9a65332d321c25761207e2fb17110dbdc8241;p=helm.git initial support for notation that specifies the precedence of term variables, that allows to omit many useless parenthesis --- diff --git a/helm/software/components/acic_content/cicNotationEnv.ml b/helm/software/components/acic_content/cicNotationEnv.ml index 32d4f0df5..5a1c4c945 100644 --- a/helm/software/components/acic_content/cicNotationEnv.ml +++ b/helm/software/components/acic_content/cicNotationEnv.ml @@ -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 diff --git a/helm/software/components/acic_content/cicNotationEnv.mli b/helm/software/components/acic_content/cicNotationEnv.mli index d4f87097e..5d2bba6c7 100644 --- a/helm/software/components/acic_content/cicNotationEnv.mli +++ b/helm/software/components/acic_content/cicNotationEnv.mli @@ -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 diff --git a/helm/software/components/acic_content/cicNotationPp.ml b/helm/software/components/acic_content/cicNotationPp.ml index 6ea839ce3..7fbc9f492 100644 --- a/helm/software/components/acic_content/cicNotationPp.ml +++ b/helm/software/components/acic_content/cicNotationPp.ml @@ -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 diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index cc481ff0a..92d081fee 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -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 diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml index 51acf758f..d4a55b353 100644 --- a/helm/software/components/acic_content/cicNotationUtil.ml +++ b/helm/software/components/acic_content/cicNotationUtil.ml @@ -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 diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml index bae4a8f59..7690aeb9b 100644 --- a/helm/software/components/content_pres/cicNotationParser.ml +++ b/helm/software/components/content_pres/cicNotationParser.ml @@ -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." ] ]; diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml index 673df335f..a7bce6437 100644 --- a/helm/software/components/content_pres/cicNotationPres.ml +++ b/helm/software/components/content_pres/cicNotationPres.ml @@ -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 diff --git a/helm/software/components/content_pres/content2presMatcher.ml b/helm/software/components/content_pres/content2presMatcher.ml index 7e080ea69..bcb4257bf 100644 --- a/helm/software/components/content_pres/content2presMatcher.ml +++ b/helm/software/components/content_pres/content2presMatcher.ml @@ -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)) -> diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index e83fbc923..8f15664d0 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -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