diff options
| -rw-r--r-- | contrib/xml/cic2Xml.ml | 2 | ||||
| -rw-r--r-- | contrib/xml/cic2acic.ml | 10 | ||||
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 3 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 27 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 16 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
6 files changed, 23 insertions, 37 deletions
diff --git a/contrib/xml/cic2Xml.ml b/contrib/xml/cic2Xml.ml index f04a03f9fd..08d3a85010 100644 --- a/contrib/xml/cic2Xml.ml +++ b/contrib/xml/cic2Xml.ml @@ -7,7 +7,7 @@ let print_xml_term ch env sigma cic = let seed = ref 0 in let acic = Cic2acic.acic_of_cic_context' true seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types [] + ids_to_father_ids ids_to_inner_sorts ids_to_inner_types env [] sigma (Unshare.unshare cic) None in let xml = Acic2Xml.print_term ids_to_inner_sorts acic in Xml.pp_ch xml ch diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 1a6cb9c811..c62db00bb1 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -349,7 +349,7 @@ let source_id_of_id id = "#source#" ^ id;; let acic_of_cic_context' computeinnertypes seed ids_to_terms constr_to_ids ids_to_father_ids ids_to_inner_sorts ids_to_inner_types - pvars ?(fake_dependent_products=false) env idrefs evar_map t expectedty + ?(fake_dependent_products=false) env idrefs evar_map t expectedty = let module D = DoubleTypeInference in let module E = Environ in @@ -541,6 +541,8 @@ print_endline "PASSATO" ; flush stdout ; add_inner_type fresh_id'' ; A.ARel (fresh_id'', n, List.nth idrefs (n-1), id) | T.Var id -> + let pvars = Termops.ids_of_named_context (E.named_context env) in + let pvars = List.map N.string_of_id pvars in let path = get_uri_of_var (N.string_of_id id) pvars in Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ; if is_a_Prop innersort && expected_available then @@ -827,6 +829,7 @@ print_endline "PASSATO" ; flush stdout ; aux computeinnertypes None [] env idrefs t ;; +(* Obsolete [HH 1/2009] let acic_of_cic_context metasenv context t = let ids_to_terms = Hashtbl.create 503 in let constr_to_ids = Acic.CicHash.create 503 in @@ -838,8 +841,9 @@ let acic_of_cic_context metasenv context t = ids_to_inner_sorts ids_to_inner_types metasenv context t, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types ;; +*) -let acic_object_of_cic_object pvars sigma obj = +let acic_object_of_cic_object sigma obj = let module A = Acic in let ids_to_terms = Hashtbl.create 503 in let constr_to_ids = Acic.CicHash.create 503 in @@ -853,7 +857,7 @@ let acic_object_of_cic_object pvars sigma obj = let seed = ref 0 in let acic_term_of_cic_term_context' = acic_of_cic_context' true seed ids_to_terms constr_to_ids ids_to_father_ids - ids_to_inner_sorts ids_to_inner_types pvars in + ids_to_inner_sorts ids_to_inner_types in (*CSC: is this the right env to use? Hhmmm. There is a problem: in *) (*CSC: Global.env () the object we are exporting is already defined, *) (*CSC: either in the environment or in the named context (in the case *) diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 26b1b0b760..a501fb6a63 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -31,7 +31,6 @@ let constr_to_xml obj sigma env = let ids_to_inner_sorts = Hashtbl.create 503 in let ids_to_inner_types = Hashtbl.create 503 in - let pvars = [] in (* named_context holds section variables and local variables *) let named_context = Environ.named_context env in (* real_named_context holds only the section variables *) @@ -54,7 +53,7 @@ let constr_to_xml obj sigma env = try let annobj = Cic2acic.acic_of_cic_context' false seed ids_to_terms constr_to_ids - ids_to_father_ids ids_to_inner_sorts ids_to_inner_types pvars rel_env + ids_to_father_ids ids_to_inner_sorts ids_to_inner_types rel_env idrefs sigma (Unshare.unshare obj') None in Acic2Xml.print_term ids_to_inner_sorts annobj diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 4ee97813bd..1ae1866144 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -79,15 +79,6 @@ let could_have_namesakes o sp = (* namesake = omonimo in italian *) | _ -> false (* uninteresting thing that won't be printed*) ;; - -(* A SIMPLE DATA STRUCTURE AND SOME FUNCTIONS TO MANAGE THE CURRENT *) -(* ENVIRONMENT (= [(name1,l1); ...;(namen,ln)] WHERE li IS THE LIST *) -(* OF VARIABLES DECLARED IN THE i-th SUPER-SECTION OF THE CURRENT *) -(* SECTION, WHOSE PATH IS namei *) - -let pvars = ref ([] : string list);; -let cumenv = ref Environ.empty_env;; - (* filter_params pvars hyps *) (* filters out from pvars (which is a list of lists) all the variables *) (* that does not belong to hyps (which is a simple list) *) @@ -120,22 +111,6 @@ type variables_type = | Assumption of string * Term.constr ;; -let add_to_pvars x = - let module E = Environ in - let v = - match x with - Definition (v, bod, typ) -> - cumenv := - E.push_named (Names.id_of_string v, Some bod, typ) !cumenv ; - v - | Assumption (v, typ) -> - cumenv := - E.push_named (Names.id_of_string v, None, typ) !cumenv ; - v - in - pvars := v::!pvars -;; - (* The computation is very inefficient, but we can't do anything *) (* better unless this function is reimplemented in the Declare *) (* module. *) @@ -231,7 +206,7 @@ let print_object uri obj sigma proof_tree_infos filename = ignore (Unix.system ("gzip " ^ fn' ^ ".xml")) in let (annobj,_,constr_to_ids,_,ids_to_inner_sorts,ids_to_inner_types,_,_) = - Cic2acic.acic_object_of_cic_object !pvars sigma obj in + Cic2acic.acic_object_of_cic_object sigma obj in let (xml, xml') = Acic2Xml.print_object uri ids_to_inner_sorts annobj in let xmltypes = Acic2Xml.print_inner_types uri ids_to_inner_sorts ids_to_inner_types in diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 5984f7415d..045c2ecca8 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -372,6 +372,16 @@ let process_chars bp c cs = | Some t -> (("", t), (bp, ep)) | None -> err (bp, ep) Undefined_token +let parse_after_dollar bp = + parser + | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] -> + ("METAIDENT", get_buff len) + | [< s >] -> + match lookup_utf8 s with + | Utf8Token (UnicodeLetter, n) -> + ("METAIDENT", get_buff (ident_tail (nstore n 0 s) s)) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars bp '$' s) + (* Parse what follows a dot *) let parse_after_dot bp c = parser @@ -399,10 +409,8 @@ let parse_after_qmark bp s = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$'; ' ('a'..'z' | 'A'..'Z' | '_' as c); - len = ident_tail (store 0 c) >] ep -> - comment_stop bp; - (("METAIDENT", get_buff len), (bp,ep)) + | [< ''$'; t = parse_after_dollar bp >] ep -> + comment_stop bp; (t, (ep, bp)) | [< ''.' as c; t = parse_after_dot bp c >] ep -> comment_stop bp; if Flags.do_beautify() & t=("",".") then between_com := true; diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 4b4abe63ad..234dd04c42 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -410,7 +410,7 @@ let is_operator s = let l = String.length s in l <> 0 & (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or - s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') + s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~' or s.[0] = '$') let is_prod_ident = function | Terminal s when is_letter s.[0] or s.[0] = '_' -> true |