Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 8e160ddb authored by Andrei Paskevich's avatar Andrei Paskevich

introduce [type oty = ty option] and some tools for it

parent c90575ec
......@@ -51,7 +51,7 @@ let create_vsymbol name ty = {
type lsymbol = {
ls_name : ident;
ls_args : ty list;
ls_value : ty option;
ls_value : oty;
}
module Lsym = WeakStructMake (struct
......@@ -78,10 +78,7 @@ let create_fsymbol nm al vl = create_lsymbol nm al (Some vl)
let create_psymbol nm al = create_lsymbol nm al (None)
let ls_ty_freevars ls =
let acc = match ls.ls_value with
| None -> Stv.empty
| Some ty -> ty_freevars Stv.empty ty
in
let acc = oty_freevars Stv.empty ls.ls_value in
List.fold_left ty_freevars acc ls.ls_args
(** Patterns *)
......@@ -905,41 +902,31 @@ let f_open_quant_cb fq =
(* constructors with type checking *)
let ls_arg_inst ls tl =
let mtch s ty t = ty_match s ty t.t_ty in
try List.fold_left2 mtch Mtv.empty ls.ls_args tl
with Invalid_argument _ -> raise (BadArity
(ls, List.length ls.ls_args, List.length tl))
let t_app_infer ls tl =
let s = ls_arg_inst ls tl in
match ls.ls_value with
| Some ty -> t_app ls tl (ty_inst s ty)
| None -> raise (FunctionSymbolExpected ls)
let ls_app_inst ls tl ty =
let s = match ls.ls_value, ty with
let s = ls_arg_inst ls tl in
match ls.ls_value, ty with
| Some _, None -> raise (PredicateSymbolExpected ls)
| None, Some _ -> raise (FunctionSymbolExpected ls)
| Some vty, Some ty -> ty_match Mtv.empty vty ty
| None, None -> Mtv.empty
in
let s =
let mtch s ty t = ty_match s ty t.t_ty in
try List.fold_left2 mtch s ls.ls_args tl
with Invalid_argument _ -> raise (BadArity
(ls, List.length ls.ls_args, List.length tl))
in
let add v acc = Mtv.add v (ty_inst s (ty_var v)) acc in
Stv.fold add (ls_ty_freevars ls) Mtv.empty
| Some vty, Some ty -> ty_match s vty ty
| None, None -> s
let fs_app_inst fs tl ty = ls_app_inst fs tl (Some ty)
let ps_app_inst ps tl = ls_app_inst ps tl None
let ps_app_inst ps tl = ls_app_inst ps tl (None)
let t_app fs tl ty = ignore (fs_app_inst fs tl ty); t_app fs tl ty
let f_app ps tl = ignore (ps_app_inst ps tl); f_app ps tl
let t_app_infer fs tl =
let mtch s ty t = ty_match s ty t.t_ty in
let s =
try List.fold_left2 mtch Mtv.empty fs.ls_args tl
with Invalid_argument _ -> raise (BadArity
(fs, List.length fs.ls_args, List.length tl))
in
let ty = match fs.ls_value with
| Some ty -> ty_inst s ty
| _ -> raise (FunctionSymbolExpected fs)
in
t_app fs tl ty
let f_app ps tl = ignore (ps_app_inst ps tl); f_app ps tl
exception EmptyCase
......
......@@ -237,3 +237,31 @@ let ty_tuple tyl = ty_app (ts_tuple (List.length tyl)) tyl
let is_ts_tuple ts = ts_equal ts (ts_tuple (List.length ts.ts_args))
(** {2 Operations on [ty option]} *)
type oty = ty option
exception UnexpectedProp
let oty_ty = function Some ty -> ty | None -> raise UnexpectedProp
let oty_prop = (=) None
let oty_value = (<>) None
let oty_equal = Util.option_eq ty_equal
let oty_hash = Util.option_apply 1 ty_hash
let oty_map = Util.option_map
let oty_iter = Util.option_iter
let oty_apply = Util.option_apply
let oty_fold = Util.option_fold
let oty_map_fold = Util.option_map_fold
let oty_match m o1 o2 = match o1,o2 with
| Some ty1, Some ty2 -> ty_match m ty1 ty2
| None, None -> m
| _ -> raise UnexpectedProp
let oty_inst m = Util.option_map (ty_inst m)
let oty_freevars = Util.option_fold ty_freevars
let oty_cons = Util.option_fold (fun tl t -> t::tl)
......@@ -119,3 +119,26 @@ val ty_tuple : ty list -> ty
val is_ts_tuple : tysymbol -> bool
(** {2 Operations on [ty option]} *)
type oty = ty option
exception UnexpectedProp
val oty_ty : oty -> ty
val oty_prop : oty -> bool
val oty_value : oty -> bool
val oty_equal : oty -> oty -> bool
val oty_hash : oty -> int
val oty_map : (ty -> ty) -> oty -> oty
val oty_iter : (ty -> unit) -> oty -> unit
val oty_apply : 'a -> (ty -> 'a) -> oty -> 'a
val oty_fold : ('a -> ty -> 'a) -> 'a -> oty -> 'a
val oty_map_fold : ('a -> ty -> 'a * ty) -> 'a -> oty -> 'a * oty
val oty_match : ty Mtv.t -> oty -> oty -> ty Mtv.t
val oty_inst : ty Mtv.t -> oty -> oty
val oty_freevars : Stv.t -> oty -> Stv.t
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