Commit cf331208 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Allow idents to be meta arguments

parent 4e212696
......@@ -33,7 +33,7 @@ module type Printer = sig
val tprinter : ident_printer (* type symbols *)
val aprinter : ident_printer (* type variables *)
val sprinter : ident_printer (* variables and functions *)
val pprinter : ident_printer (* propoition names *)
val pprinter : ident_printer (* proposition names *)
val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
......@@ -556,6 +556,7 @@ let print_meta_arg_type fmt = function
| MTprsymbol -> fprintf fmt "[proposition]"
| MTstring -> fprintf fmt "[string]"
| MTint -> fprintf fmt "[integer]"
| MTident -> fprintf fmt "[identifier]"
let print_meta_arg fmt = function
| MAty ty -> fprintf fmt "type %a" print_ty ty; forget_tvs ()
......@@ -564,6 +565,7 @@ let print_meta_arg fmt = function
| MApr pr -> fprintf fmt "prop %a" print_pr pr
| MAstr s -> fprintf fmt "\"%s\"" s
| MAint i -> fprintf fmt "%d" i
| MAident i -> Ident.print_decoded fmt (id_unique sprinter i)
let print_qt fmt th =
if th.th_path = [] then print_th fmt th else
......
......@@ -83,6 +83,7 @@ type meta_arg_type =
| MTprsymbol
| MTstring
| MTint
| MTident
type meta_arg =
| MAty of ty
......@@ -91,6 +92,7 @@ type meta_arg =
| MApr of prsymbol
| MAstr of string
| MAint of int
| MAident of ident
type meta = {
meta_name : string;
......@@ -235,6 +237,7 @@ module Hstdecl = Hashcons.Make (struct
| MApr pr -> pr_hash pr
| MAstr s -> Hashtbl.hash s
| MAint i -> Hashtbl.hash i
| MAident i -> Ident.id_hash i
let hs_smap sm h =
Mts.fold hs_cl_ty sm.sm_ty
......@@ -409,8 +412,9 @@ let add_tdecl uc td = match td.td_node with
(** Declarations *)
let store_path, store_theory, restore_path =
let store_path, store_theory, restore_path, restore_theory =
let id_to_path = Wid.create 17 in
let id_to_th = Wid.create 17 in
let store_path uc path id =
(* this symbol already belongs to some theory *)
if Wid.mem id_to_path id then () else
......@@ -420,10 +424,16 @@ let store_path, store_theory, restore_path =
let store_theory th =
let id = th.th_name in
(* this symbol is already a theory *)
if Wid.mem id_to_path id then () else
Wid.set id_to_path id (th.th_path, id.id_string, []) in
if Wid.mem id_to_path id then () else begin
Wid.set id_to_path id (th.th_path, id.id_string, []);
Sid.iter (fun id -> Wid.set id_to_th id th) th.th_local;
Wid.set id_to_th id th;
end
in
let restore_path id = Wid.find id_to_path id in
store_path, store_theory, restore_path
let restore_theory id = Wid.find id_to_th id in
store_path, store_theory, restore_path, restore_theory
let close_theory uc =
let th = close_theory uc in
......@@ -862,6 +872,7 @@ let get_meta_arg_type = function
| MApr _ -> MTprsymbol
| MAstr _ -> MTstring
| MAint _ -> MTint
| MAident _ -> MTident
let create_meta m al =
let get_meta_arg at a =
......@@ -960,6 +971,7 @@ let print_meta_arg_type fmt = function
| MTprsymbol -> fprintf fmt "proposition"
| MTstring -> fprintf fmt "string"
| MTint -> fprintf fmt "int"
| MTident -> fprintf fmt "identifier"
let () = Exn_printer.register
begin fun fmt exn -> match exn with
......
......@@ -43,6 +43,7 @@ type meta_arg_type =
| MTprsymbol
| MTstring
| MTint
| MTident
type meta_arg =
| MAty of ty
......@@ -51,6 +52,7 @@ type meta_arg =
| MApr of prsymbol
| MAstr of string
| MAint of int
| MAident of ident
type meta = private {
meta_name : string;
......@@ -160,6 +162,8 @@ val restore_path : ident -> string list * string * string list
If [id] is a theory name, the third component is an empty list.
Raises [Not_found] if the ident was never declared in/as a theory. *)
val restore_theory : ident -> theory
(** {2 Declaration constructors} *)
val create_decl : decl -> tdecl
......
......@@ -388,6 +388,7 @@ meta_arg:
| AXIOM qualid { Max $2 }
| LEMMA qualid { Mlm $2 }
| GOAL qualid { Mgl $2 }
| VAL qualid { Mval $2 }
| STRING { Mstr $1 }
| INTEGER { Mint (Number.to_small_integer $1) }
......
......@@ -223,6 +223,7 @@ type metarg =
| Max of qualid
| Mlm of qualid
| Mgl of qualid
| Mval of qualid
| Mstr of string
| Mint of int
......
......@@ -509,6 +509,9 @@ let find_xsymbol muc q = find_xsymbol_ns (get_namespace muc) q
let find_itysymbol muc q = find_itysymbol_ns (get_namespace muc) q
let find_prog_symbol muc q = find_prog_symbol_ns (get_namespace muc) q
let find_rsymbol muc q =
find_qualid ~ty:Prog (fun rs -> rs.rs_name) ns_find_rs (get_namespace muc) q
let find_special muc test nm q =
match find_prog_symbol muc q with
| RS s when test s -> s
......@@ -1478,6 +1481,7 @@ let add_decl muc env file d =
| Ptree.Max q -> MApr (find_prop_of_kind Paxiom tuc q)
| Ptree.Mlm q -> MApr (find_prop_of_kind Plemma tuc q)
| Ptree.Mgl q -> MApr (find_prop_of_kind Pgoal tuc q)
| Ptree.Mval q -> MAident (find_rsymbol muc q).rs_name
| Ptree.Mstr s -> MAstr s
| Ptree.Mint i -> MAint i in
add_meta muc (lookup_meta id.id_str) (List.map convert al)
......
......@@ -370,6 +370,7 @@ let print_meta_arg fmt = function
| MApr pr -> fprintf fmt "prop %a" print_pr pr
| MAstr s -> fprintf fmt "\"%s\"" s
| MAint i -> fprintf fmt "%d" i
| MAident id -> fprintf fmt "%s" (id_unique iprinter id)
let print_qt fmt th =
if th.th_path = [] then print_th fmt th else
......
......@@ -629,6 +629,7 @@ module Checksum = struct
| Theory.MTprsymbol -> char b 'p'
| Theory.MTstring -> char b 's'
| Theory.MTint -> char b 'i'
| Theory.MTident -> char b 'd'
let meta b m =
string b m.Theory.meta_name;
......@@ -642,6 +643,7 @@ module Checksum = struct
| Theory.MApr pr -> char b 'p'; ident b pr.Decl.pr_name
| Theory.MAstr s -> char b 's'; string b s
| Theory.MAint i -> char b 'i'; int b i
| Theory.MAident i -> char b 'd'; ident b i
let tdecl b d = match d.Theory.td_node with
| Theory.Decl d -> decl b d
......
......@@ -158,7 +158,9 @@ let fold tenv taskpre task =
| MAls ls -> MAls (conv_ls tenv ud ls)
| MApr _ -> raise Exit
| MAstr _ as s -> s
| MAint _ as i -> i in
| MAint _ as i -> i
| MAident _ as i -> i
in
let arg = List.map map ml in
add_meta (decl_ud ud task) meta arg
with
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment