X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=5c5db75b4bb88f93ef54640b0952e77067338567;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=18259a00441873ea85ea755e3a06e891de291872;hpb=fecaa410b6226e8614cfef78d0f952e3c676c06e;p=helm.git diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml index 18259a004..5c5db75b4 100644 --- a/helm/software/components/cic_proof_checking/cicReduction.ml +++ b/helm/software/components/cic_proof_checking/cicReduction.ml @@ -34,6 +34,37 @@ exception ReferenceToVariable;; exception ReferenceToCurrentProof;; exception ReferenceToInductiveDefinition;; +let ndebug = ref false;; +let indent = ref "";; +let times = ref [];; +let pp s = + if !ndebug then + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; +let inside c = + if !ndebug then + begin + let time1 = Unix.gettimeofday () in + indent := !indent ^ String.make 1 c; + times := time1 :: !times; + prerr_endline ("{{{" ^ !indent ^ " ") + end +;; +let outside ok = + if !ndebug then + begin + let time2 = Unix.gettimeofday () in + let time1 = + match !times with time1::tl -> times := tl; time1 | [] -> assert false in + prerr_endline ("}}} " ^ string_of_float (time2 -. time1)); + if not ok then prerr_endline "exception raised!"; + try + indent := String.sub !indent 0 (String.length !indent -1) + with + Invalid_argument _ -> indent := "??"; () + end +;; + let debug = false let profile = false let debug_print s = if debug then prerr_endline (Lazy.force s) @@ -55,8 +86,14 @@ module type Strategy = type env_term type ens_term type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list - val to_env : config -> env_term - val to_ens : config -> ens_term + val to_env : + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> + config -> env_term + val to_ens : + reduce: (config -> config) -> + unwind: (config -> Cic.term) -> + config -> ens_term val from_stack : stack_term -> config val from_stack_list_for_unwind : unwind: (config -> Cic.term) -> @@ -106,7 +143,30 @@ module CallByValueByNameForUnwind = end ;; +module CallByValueByNameForUnwind' = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *) + and env_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *) + and ens_term = config lazy_t * Cic.term lazy_t (* cbv, cbn *) + + let to_env ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let to_ens ~reduce ~unwind c = lazy (reduce c),lazy (unwind c) + let from_stack (c,_) = Lazy.force c + let from_stack_list_for_unwind ~unwind l = List.map (function (_,c) -> Lazy.force c) l + let from_env (c,_) = Lazy.force c + let from_ens (c,_) = Lazy.force c + let from_env_for_unwind ~unwind (_,c) = Lazy.force c + let from_ens_for_unwind ~unwind (_,c) = Lazy.force c + let stack_to_env ~reduce ~unwind config = config + let compute_to_env ~reduce ~unwind k e ens t = + lazy (reduce (k,e,ens,t,[])), lazy (unwind (k,e,ens,t,[])) + let compute_to_stack ~reduce ~unwind config = lazy (reduce config), lazy (unwind config) + end +;; + +(* Old Machine module CallByNameStrategy = struct type stack_term = Cic.term @@ -126,6 +186,28 @@ module CallByNameStrategy = let compute_to_env ~reduce ~unwind k e ens t = unwind k e ens t end ;; +*) + +module CallByNameStrategy = + struct + type config = int * env_term list * ens_term Cic.explicit_named_substitution * Cic.term * stack_term list + and stack_term = config + and env_term = config + and ens_term = config + + let to_env c = c + let to_ens c = c + let from_stack config = config + let from_stack_list_for_unwind ~unwind l = List.map unwind l + let from_env c = c + let from_ens c = c + let from_env_for_unwind ~unwind c = unwind c + let from_ens_for_unwind ~unwind c = unwind c + let stack_to_env ~reduce ~unwind config = 0,[],[],unwind config,[] + let compute_to_env ~reduce ~unwind k e ens t = k,e,ens,t,[] + let compute_to_stack ~reduce ~unwind config = config + end +;; module CallByValueStrategy = struct @@ -400,7 +482,8 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, | C.Cast (te,ty) -> C.Cast (unwind_aux m te, unwind_aux m ty) (*CSC ???*) | C.Prod (n,s,t) -> C.Prod (n, unwind_aux m s, unwind_aux (m + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, unwind_aux m s, unwind_aux (m + 1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t) + | C.LetIn (n,s,ty,t) -> + C.LetIn (n, unwind_aux m s, unwind_aux m ty, unwind_aux (m + 1) t) | C.Appl l -> C.Appl (List.map (unwind_aux m) l) | C.Const (uri,exp_named_subst) -> let params = @@ -471,31 +554,7 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, in C.CoFix (i, substitutedfl) and substaux_in_exp_named_subst params exp_named_subst' m = - (*CSC: Idea di Andrea di ordinare compatibilmente con l'ordine dei params - let ens' = - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (*CSC: qui liftiamo tutti gli ens anche se magari me ne servono la meta'!!! *) - List.map (function (uri,t) -> uri, CicSubstitution.lift m t) ens - in - let rec filter_and_lift = - function - [] -> [] - | uri::tl -> - let r = filter_and_lift tl in - (try - (uri,(List.assq uri ens'))::r - with - Not_found -> r - ) - in - filter_and_lift params - *) - - (*CSC: invece di concatenare sarebbe meglio rispettare l'ordine dei params *) - (*CSC: e' vero???? una veloce prova non sembra confermare la teoria *) - - (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) - (*CSC: codice altamente inefficiente *) + (*CSC: codice copiato e modificato dalla cicSubstitution.subst_vars *) let rec filter_and_lift already_instantiated = function [] -> [] @@ -510,18 +569,24 @@ debug_print (lazy ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri, (uri,CicSubstitution.lift m (RS.from_ens_for_unwind ~unwind t)) :: (filter_and_lift (uri::already_instantiated) tl) | _::tl -> filter_and_lift already_instantiated tl -(* - | (uri,_)::tl -> -debug_print (lazy ("---- SKIPPO " ^ UriManager.string_of_uri uri)) ; -if List.for_all (function (uri',_) -> not (UriManager.eq uri uri')) -exp_named_subst' then debug_print (lazy "---- OK1") ; -debug_print (lazy ("++++ uri " ^ UriManager.string_of_uri uri ^ " not in " ^ String.concat " ; " (List.map UriManager.string_of_uri params))) ; -if List.mem uri params then debug_print (lazy "---- OK2") ; - filter_and_lift tl -*) in - List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ - (filter_and_lift [] (List.rev ens)) + let res = + List.map (function (uri,t) -> uri, unwind_aux m t) exp_named_subst' @ + (filter_and_lift [] (List.rev ens)) + in + let rec reorder = + function + [] -> [] + | uri::tl -> + let he = + try + [uri,List.assoc uri res] + with + Not_found -> [] + in + he@reorder tl + in + reorder params in unwind_aux m t @@ -545,19 +610,21 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function (k, e, _, C.Rel n, s) as config -> let config' = - try - Some (RS.from_env (List.nth e (n-1))) - with - Failure _ -> - try - begin - match List.nth context (n - 1 - k) with - None -> assert false - | Some (_,C.Decl _) -> None - | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) - end - with - Failure _ -> None + if not delta then None + else + try + Some (RS.from_env (List.nth e (n-1))) + with + Failure _ -> + try + begin + match List.nth context (n - 1 - k) with + None -> assert false + | Some (_,C.Decl _) -> None + | Some (_,C.Def (x,_)) -> Some (0,[],[],S.lift (n - k) x,[]) + end + with + Failure _ -> None in (match config' with Some (k',e',ens',t',s') -> reduce (k',e',ens',t',s'@s) @@ -592,7 +659,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (_, _, _, C.Lambda _, []) as config -> config | (k, e, ens, C.Lambda (_,_,t), p::s) -> reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s) - | (k, e, ens, C.LetIn (_,m,t), s) -> + | (k, e, ens, C.LetIn (_,m,_,t), s) -> let m' = RS.compute_to_env ~reduce ~unwind k e ens m in reduce (k+1, m'::e, ens, t, s) | (_, _, _, C.Appl [], _) -> assert false @@ -641,14 +708,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; (k', e', ens', C.MutConstruct (_,_,j,_), []) -> reduce (k, e, ens, (List.nth pl (j-1)), s) | (k', e', ens', C.MutConstruct (_,_,j,_), s') -> - let (arity, r) = + let r = let o,_ = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind in match o with - C.InductiveDefinition (s,ingredients,r,_) -> - let (_,_,arity,_) = List.nth s i in - (arity,r) + C.InductiveDefinition (_,_,r,_) -> r | _ -> raise WrongUriToInductiveDefinition in let ts = @@ -691,12 +756,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let leng = List.length fl in let new_env = let counter = ref 0 in - let rec build_env e = - if !counter = leng then e + let rec build_env e' = + if !counter = leng then e' else (incr counter ; build_env - ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e)) + ((RS.to_env ~reduce ~unwind (k,e,ens,C.Fix (!counter -1, fl),[]))::e')) in build_env e in @@ -717,7 +782,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; function [] -> ens | (uri,t)::tl -> - push_exp_named_subst k e ((uri,RS.to_ens (k,e,ens,t,[]))::ens) tl + push_exp_named_subst k e ((uri,RS.to_ens ~reduce ~unwind (k,e,ens,t,[]))::ens) tl in reduce ;; @@ -746,8 +811,11 @@ module R = Reduction ClosuresOnStackByValueFromEnvOrEnsByNameOnConstantsStrategy;; OK 58.094s module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);; OK 58.127s *) -module R = Reduction(CallByValueByNameForUnwind);; +(*module R = Reduction(CallByValueByNameForUnwind);;*) +module RS = CallByValueByNameForUnwind';; +(*module R = Reduction(CallByNameStrategy);;*) (*module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;*) +module R = Reduction(RS);; module U = UriManager;; let whd = R.whd @@ -766,8 +834,11 @@ let (===) x y = (* t1, t2 must be well-typed *) let are_convertible whd ?(subst=[]) ?(metasenv=[]) = + let heuristic = ref true in let rec aux test_equality_only context t1 t2 ugraph = - let aux2 test_equality_only t1 t2 ugraph = + (*D*)inside 'B'; try let rc = + pp (lazy (CicPp.ppterm t1 ^ " vs " ^ CicPp.ppterm t2)); + let rec aux2 test_equality_only t1 t2 ugraph = (* this trivial euristic cuts down the total time of about five times ;-) *) (* this because most of the time t1 and t2 are "sintactically" the same *) @@ -811,15 +882,36 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = if b2 then true,ugraph1 else false,ugraph else false,ugraph - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only -> - true,(CicUniv.add_eq t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> - true,(CicUniv.add_ge t2 t1 ugraph) - (* TASSI: CONSTRAINTS *) - | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph - (* TASSI: CONSTRAINTS *) + | C.Meta (n1,l1), _ -> + (try + let _,term,_ = CicUtil.lookup_subst n1 subst in + let term' = CicSubstitution.subst_meta l1 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t2); +*) + aux test_equality_only context term' t2 ugraph + with CicUtil.Subst_not_found _ -> false,ugraph) + | _, C.Meta (n2,l2) -> + (try + let _,term,_ = CicUtil.lookup_subst n2 subst in + let term' = CicSubstitution.subst_meta l2 term in +(* +prerr_endline ("%?: " ^ CicPp.ppterm t1 ^ " <==> " ^ CicPp.ppterm t2); +prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1); +*) + aux test_equality_only context t1 term' ugraph + with CicUtil.Subst_not_found _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when test_equality_only -> + (try true,(CicUniv.add_eq t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) + when not test_equality_only -> + (try true,(CicUniv.add_ge t2 t1 ugraph) + with CicUniv.UniverseInconsistency _ -> false,ugraph) + | (C.Sort s1, C.Sort (C.Type _)) + | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> let b',ugraph' = aux true context s1 s2 ugraph in @@ -829,27 +921,36 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = else false,ugraph | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) -> - let b',ugraph' = aux test_equality_only context s1 s2 ugraph in + let b',ugraph' = aux true context s1 s2 ugraph in if b' then aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2 ugraph' else false,ugraph - | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) -> + | (C.LetIn (name1,s1,ty1,t1), C.LetIn(_,s2,ty2,t2)) -> let b',ugraph' = aux test_equality_only context s1 s2 ugraph in if b' then - aux test_equality_only - ((Some (name1, (C.Def (s1,None))))::context) t1 t2 ugraph' + let b',ugraph = aux test_equality_only context ty1 ty2 ugraph in + if b' then + aux test_equality_only + ((Some (name1, (C.Def (s1,ty1))))::context) t1 t2 ugraph' + else + false,ugraph else false,ugraph | (C.Appl l1, C.Appl l2) -> + let b, ugraph = + aux test_equality_only context (List.hd l1) (List.hd l2) ugraph + in + if not b then false, ugraph + else (try List.fold_right2 (fun x y (b,ugraph) -> if b then - aux test_equality_only context x y ugraph + aux true context x y ugraph else - false,ugraph) l1 l2 (true,ugraph) + false,ugraph) (List.tl l1) (List.tl l2) (true,ugraph) with Invalid_argument _ -> false,ugraph ) @@ -912,7 +1013,7 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = let b'',ugraph''=aux test_equality_only context outtype1 outtype2 ugraph in if b'' then - let b''',ugraph'''= aux test_equality_only context + let b''',ugraph'''= aux true context term1 term2 ugraph'' in List.fold_right2 (fun x y (b,ugraph) -> @@ -926,8 +1027,12 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = else false,ugraph | (C.Fix (i1,fl1), C.Fix (i2,fl2)) -> - let tys = - List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 + let tys,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 in if i1 = i2 then List.fold_right2 @@ -945,9 +1050,13 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = else false,ugraph | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) -> - let tys = - List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1 - in + let tys,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) fl1 + in if i1 = i2 then List.fold_right2 (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) -> @@ -963,16 +1072,70 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[]) = fl1 fl2 (true,ugraph) else false,ugraph - | (C.Cast _, _) | (_, C.Cast _) + | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph + | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (_,_) -> false,ugraph end in + let res = + if !heuristic then + aux2 test_equality_only t1 t2 ugraph + else + false,ugraph + in + if fst res = true then + res + else +begin +(*if !heuristic then prerr_endline ("NON FACILE: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) + (* heuristic := false; *) debug t1 [t2] "PREWHD"; +(*prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2);*) +(* +prerr_endline ("PREWHD: " ^ CicPp.ppterm t1 ^ " <===> " ^ CicPp.ppterm t2); let t1' = whd ?delta:(Some true) ?subst:(Some subst) context t1 in let t2' = whd ?delta:(Some true) ?subst:(Some subst) context t2 in debug t1' [t2'] "POSTWHD"; +*) +let rec convert_machines test_equality_only ugraph = + function + [] -> true,ugraph + | ((k1,env1,ens1,h1,s1),(k2,env2,ens2,h2,s2))::tl -> + let (b,ugraph) as res = + aux2 test_equality_only + (R.unwind (k1,env1,ens1,h1,[])) (R.unwind (k2,env2,ens2,h2,[])) ugraph + in + if b then + let problems = + try + Some + (List.combine + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s1) + (List.map + (fun si-> R.reduce ~delta:false ~subst context(RS.from_stack si)) + s2) + @ tl) + with + Invalid_argument _ -> None + in + match problems with + None -> false,ugraph + | Some problems -> convert_machines true ugraph problems + else + res +in + convert_machines test_equality_only ugraph + [R.reduce ~delta:true ~subst context (0,[],[],t1,[]), + R.reduce ~delta:true ~subst context (0,[],[],t2,[])] +(*prerr_endline ("POSTWH: " ^ CicPp.ppterm t1' ^ " <===> " ^ CicPp.ppterm t2');*) +(* aux2 test_equality_only t1' t2' ugraph +*) +end + (*D*)in outside true; rc with exc -> outside false; raise exc in aux false (*c t1 t2 ugraph *) ;; @@ -1031,7 +1194,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = | C.Lambda (n,s,t) -> let s' = aux ctx s in C.Lambda (n, s', aux ((decl n s')::ctx) t) - | C.LetIn (n,s,t) -> + | C.LetIn (n,s,_,t) -> (* the term is already in weak head normal form *) assert false | C.Appl (h::l) -> C.Appl (h::(List.map (aux ctx) l)) @@ -1057,18 +1220,61 @@ let normalize ?delta ?subst ctx term = (* performs an head beta/cast reduction *) -let rec head_beta_reduce = - function - (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - let he''' = - match he'' with - Cic.Appl l -> Cic.Appl (l@tl') - | _ -> Cic.Appl (he''::tl') +let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t = + match upto with + 0 -> t + | n -> + match t with + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + else + let he''' = + match he'' with + Cic.Appl l -> Cic.Appl (l@tl') + | _ -> Cic.Appl (he''::tl') + in + head_beta_reduce ~delta ~upto:(upto - 1) he''' + | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te + | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition + in + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~upto + ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl))) + | Cic.Const (uri,ens) as t when delta=true -> + let bo = + match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with + Cic.Constant (_,bo,_,_,_) -> bo + | Cic.Variable _ -> raise ReferenceToVariable + | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo + | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition in - head_beta_reduce he''' - | Cic.Cast (te,_) -> head_beta_reduce te - | t -> t + (match bo with + None -> t + | Some bo -> + head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo)) + | t -> t + +(* +let are_convertible ?subst ?metasenv context t1 t2 ugraph = + let before = Unix.gettimeofday () in + let res = are_convertible ?subst ?metasenv context t1 t2 ugraph in + let after = Unix.gettimeofday () in + let diff = after -. before in + if diff > 0.1 then + begin + let nc = List.map (function None -> None | Some (n,_) -> Some n) context in + prerr_endline + ("\n#(" ^ string_of_float diff ^ "):\n" ^ CicPp.pp t1 nc ^ "\n<=>\n" ^ CicPp.pp t2 nc); + end; + res +*)