Commit 3185e298 authored by MARCHE Claude's avatar MARCHE Claude

solved configure pb with manager

parent 510df77f
......@@ -306,6 +306,7 @@ dnl AC_SUBST(OCAMLWEB)
AC_SUBST(CAMLP5O)
AC_SUBST(enable_ide)
AC_SUBST(enable_proof_manager)
AC_SUBST(enable_plugins)
AC_SUBST(DYNLINK)
......
......@@ -23,16 +23,24 @@ open Theory
type env
val env_tag : env -> int
type retrieve_theory = env -> string list -> theory Mnm.t
val create_env : retrieve_theory -> env
(** ??? *)
exception TheoryNotFound of string list * string
val find_theory : env -> string list -> string -> theory
(** [find_theory e p n] finds the theory named [p.n] in environment
[e]
@raises [TheoryNotFound p n] if theory not present in env [e]
*)
val env_tag : env -> int
exception TheoryNotFound of string list * string
(** Parsers *)
......
......@@ -480,8 +480,31 @@ let gando = function
(* recognition of a Gappa predicate *)
let is_le_num _id = assert false
(* true when id is <= on R or Z *)
let prelude_to_load = ref true
let dummy_symbol = (Obj.magic 0 : Term.lsymbol)
let symbol_le_int = ref dummy_symbol
let symbol_le_real = ref dummy_symbol
let load_prelude (drv : Driver.driver_query) =
if !prelude_to_load then
begin
let env = Driver.query_env drv in
let int_theory = Env.find_theory env ["int"] "Int" in
let real_theory = Env.find_theory env ["real"] "Real" in
symbol_le_int :=
Theory.ns_find_ls int_theory.Theory.th_export ["infix <="];
symbol_le_real :=
Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
prelude_to_load := false;
end
(* true when id is <= on R or Z *)
let is_le_num id =
ls_equal id !symbol_le_int
|| ls_equal id !symbol_le_real
let is_ge_num _id = assert false
(* true when id is >= on R or Z *)
......@@ -667,16 +690,8 @@ let process_goal _g = assert false
*)
let print_decl drv _fmt d = match d.d_node with
| Dtype _dl ->
assert false
(*
print_list_opt newline (print_type_decl drv) fmt dl
*)
| Dlogic _dl ->
assert false
(*
print_list_opt newline (print_logic_decl drv) fmt dl
*)
| Dtype _dl -> false
| Dlogic _dl -> false
| Dind _ -> unsupportedDecl d
"gappa: inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
......@@ -705,6 +720,7 @@ let print_task drv fmt task =
let () = register_printer "gappa"
(fun drv fmt task ->
load_prelude drv;
(*
forget_all ident_printer;
*)
......
......@@ -83,8 +83,8 @@ module Utils = struct
let const x _ = x
let map_keys m = Mty.fold (fun key value acc -> key::acc) m []
let map_values m = Mty.fold (fun key value acc -> value::acc) m []
let map_keys m = Mty.fold (fun key _value acc -> key::acc) m []
let map_values m = Mty.fold (fun _key value acc -> value::acc) m []
end
......@@ -132,7 +132,7 @@ module Prelude = struct
(** [find_matching_vars tblT varM args_ty args_vars] matches [args_ty]
against [args_vars] to deduce a mapping from [args_vars] to lsymbols
through [tblT] and [varM] *)
let find_matching_vars tblT varM args_ty args_vars =
let find_matching_vars _tblT varM args_ty args_vars =
let tv_to_ty = Mtv.empty in
let mapping = List.fold_left2 ty_match tv_to_ty args_ty args_vars in
let tv_to_lsymbol = Mtv.empty in (* result mapping *)
......
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