typage des quantificateurs

parent e65a815a
...@@ -298,31 +298,23 @@ let find_lsymbol_ns p ns = ...@@ -298,31 +298,23 @@ let find_lsymbol_ns p ns =
let find_lsymbol p th = let find_lsymbol p th =
find_lsymbol_ns p (get_namespace th) find_lsymbol_ns p (get_namespace th)
let specialize_fsymbol ~loc s = let specialize_lsymbol ~loc s =
let tl, t = match s.ls_value with let tl = s.ls_args in
| Some t -> s.ls_args, t let t = s.ls_value in
| _ -> assert false (* FIXME: is it right? *)
in
let env = Htv.create 17 in let env = Htv.create 17 in
s, List.map (specialize ~loc env) tl, specialize ?loc env t s, List.map (specialize ~loc env) tl, option_map (specialize ~loc env) t
let find_lsymbol {id=x; id_loc=loc} ns =
try Mnm.find x ns.ns_ls
with Not_found -> error ~loc (UnboundSymbol x)
let find_lsymbol_ns p ns =
find find_lsymbol p ns
let find_lsymbol p th = let specialize_fsymbol ~loc s =
find_lsymbol_ns p (get_namespace th) let s, tl, ty = specialize_lsymbol ~loc s in
match ty with
| None -> error ~loc TermExpected
| Some ty -> s, tl, ty
let specialize_psymbol ~loc s = let specialize_psymbol ~loc s =
let tl = match s.ls_value with let s, tl, ty = specialize_lsymbol ~loc s in
| None -> s.ls_args match ty with
| _ -> assert false (* FIXME: is it right? *) | None -> s, tl
in | Some _ -> error ~loc PredicateExpected
let env = Htv.create 17 in
s, List.map (specialize ~loc env) tl
(** Typing types *) (** Typing types *)
...@@ -461,6 +453,14 @@ let rec trigger_not_a_term_exn = function ...@@ -461,6 +453,14 @@ let rec trigger_not_a_term_exn = function
| Loc.Located (_, exn) -> trigger_not_a_term_exn exn | Loc.Located (_, exn) -> trigger_not_a_term_exn exn
| _ -> false | _ -> false
let check_linearity uqu =
let s = ref S.empty in
let check id =
if S.mem id.id !s then errorm ~loc:id.id_loc "duplicate variable %s" id.id;
s := S.add id.id !s
in
List.iter (fun (idl, _) -> List.iter check idl) uqu
let rec dterm env t = let rec dterm env t =
let n, ty = dterm_node t.pp_loc env t.pp_desc in let n, ty = dterm_node t.pp_loc env t.pp_desc in
{ dt_node = n; dt_ty = ty } { dt_node = n; dt_ty = ty }
...@@ -521,6 +521,7 @@ and dfmla env e = match e.pp_desc with ...@@ -521,6 +521,7 @@ and dfmla env e = match e.pp_desc with
| PPif (a, b, c) -> | PPif (a, b, c) ->
Fif (dfmla env a, dfmla env b, dfmla env c) Fif (dfmla env a, dfmla env b, dfmla env c)
| PPquant (q, uqu, trl, a) -> | PPquant (q, uqu, trl, a) ->
check_linearity uqu;
let uquant env (idl,ty) = let uquant env (idl,ty) =
let ty = dty env ty in let ty = dty env ty in
let env, idl = let env, idl =
......
...@@ -3,8 +3,8 @@ ...@@ -3,8 +3,8 @@
theory A theory A
use import prelude.Int use import prelude.Int
axiom A : logic p(int, int)
F : let x = 2+2 in G : x*x = 16 axiom A : forall x,y:int, z,t:real. x=x
end end
theory TreeForest theory TreeForest
......
...@@ -24,6 +24,8 @@ let map_fold_left f acc l = ...@@ -24,6 +24,8 @@ let map_fold_left f acc l =
let of_option = function Some v -> v | None -> assert false let of_option = function Some v -> v | None -> assert false
let option_map f = function None -> None | Some x -> Some (f x)
exception FoldSkip exception FoldSkip
let all_fn pr _ t = pr t || raise FoldSkip let all_fn pr _ t = pr t || raise FoldSkip
......
...@@ -19,6 +19,8 @@ val map_fold_left : ...@@ -19,6 +19,8 @@ val map_fold_left :
val of_option : 'a option -> 'a val of_option : 'a option -> 'a
val option_map : ('a -> 'b) -> 'a option -> 'b option
exception FoldSkip exception FoldSkip
val all_fn : ('a -> bool) -> 'b -> 'a -> bool val all_fn : ('a -> bool) -> 'b -> 'a -> bool
......
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