- (try
- fo_unif_l
- test_equality_only subst metasenv (lr1, lr2) ugraph
- with
- | UnificationFailure s
- | Uncertain s as exn ->
- (match l1, l2 with
- (* {{{ pullback *)
- | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
- (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
- CoercDb.is_a_coercion cc1 <> None &&
- CoercDb.is_a_coercion cc2 <> None &&
- not (UriManager.eq uri1 uri2) ->
-(*DEBUGGING ONLY:
-prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-*)
- let inner_coerced t =
- let t = CicMetaSubst.apply_subst subst t in
- let rec aux c x t =
- match t with
- | Cic.Appl l ->
- (match CoercGraph.coerced_arg l with
- | None -> c, x
- | Some (t,_) -> aux (List.hd l) t t)
- | _ -> c, x
- in
- aux (Cic.Implicit None) (Cic.Implicit None) t
- in
- let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
- let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
- let car1, car2 =
- match
- CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
- with
- | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
- | _ -> assert false
- in
- let head1_c, head2_c =
- match
- CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
- with
- | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
- | _ -> assert false
- in
- let unfold uri ens args =
- let o, _ =
- CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
- in
- assert (ens = []);
- match o with
- | Cic.Constant (_,Some bo,_,_,_) ->
- CicReduction.head_beta_reduce ~delta:false
- (Cic.Appl (bo::args))
- | _ -> assert false
- in
- let conclude subst metasenv ugraph last_tl1' last_tl2' =
- let subst',metasenv,ugraph =
-(*DEBUGGING ONLY:
-prerr_endline
- ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
- " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
-*)
- fo_unif_subst test_equality_only subst context
- metasenv last_tl1' last_tl2' ugraph
- in
- if subst = subst' then raise exn
- else
-(*DEBUGGING ONLY:
-let subst,metasenv,ugrph as res =
-*)
- fo_unif_subst test_equality_only subst' context
- metasenv (C.Appl l1) (C.Appl l2) ugraph
-(*DEBUGGING ONLY:
-in
-(prerr_endline
- (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
- " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
-res)
-*)
- in
- if CoercDb.eq_carr car1 car2 then
- match last_tl1,last_tl2 with
- | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
- | _, C.Meta _
- | C.Meta _, _ ->
- let subst,metasenv,ugraph =
- fo_unif_subst test_equality_only subst context
- metasenv last_tl1 last_tl2 ugraph
- in
- fo_unif_subst test_equality_only subst context
- metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
- | _ when CoercDb.eq_carr head1_c head2_c ->
- (* composite VS composition + metas avoiding
- * coercions not only in coerced position *)
- if c1 <> cc1 && c2 <> cc2 then
- conclude subst metasenv ugraph
- last_tl1 last_tl2
- else
- let l1, l2 =
- if c1 = cc1 then
- unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
- else
- Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
- in
- fo_unif_subst test_equality_only subst context
- metasenv l1 l2 ugraph
- | _ -> raise exn
- else
- let grow1 =
- match last_tl1 with Cic.Meta _ -> true | _ -> false in
- let grow2 =
- match last_tl2 with Cic.Meta _ -> true | _ -> false in
- if not (grow1 || grow2) then
- (* no flexible terminals -> no pullback, but
- * we still unify them, in some cases it helps *)
- conclude subst metasenv ugraph last_tl1 last_tl2
- else
- let meets =
- CoercGraph.meets
- metasenv subst context (grow1,car1) (grow2,car2)
- in
- (match meets with
- | [] -> raise exn
- | (carr,metasenv,to1,to2)::xxx ->
- warn_if_not_unique xxx to1 to2 carr car1 car2;
- let last_tl1',(subst,metasenv,ugraph) =
- match grow1,to1 with
- | true,Some (last,coerced) ->
- last,
- fo_unif_subst test_equality_only subst context
- metasenv coerced last_tl1 ugraph
- | _ -> last_tl1,(subst,metasenv,ugraph)
- in
- let last_tl2',(subst,metasenv,ugraph) =
- match grow2,to2 with
- | true,Some (last,coerced) ->
- last,
- fo_unif_subst test_equality_only subst context
- metasenv coerced last_tl2 ugraph
- | _ -> last_tl2,(subst,metasenv,ugraph)
- in
- conclude subst metasenv ugraph last_tl1' last_tl2')
- (* }}} pullback *)
- (* {{{ CSC: This is necessary because of the "elim H" tactic
- where the type of H is only reducible to an
- inductive type. This could be extended from inductive
- types to any rigid term. However, the code is
- duplicated in two places: inside applications and
- outside them. Probably it would be better to
- work with lambda-bar terms instead. *)
- | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
- | (_, Cic.MutInd _::_) ->
- let t1' = R.whd ~subst context t1 in
- (match t1' with
- C.Appl (C.MutInd _::_) ->
- fo_unif_subst test_equality_only
- subst context metasenv t1' t2 ugraph
- | _ -> raise (UnificationFailure (lazy "88")))
- | (Cic.MutInd _::_,_) ->
- let t2' = R.whd ~subst context t2 in
- (match t2' with
- C.Appl (C.MutInd _::_) ->
- fo_unif_subst test_equality_only
- subst context metasenv t1 t2' ugraph
- | _ -> raise
- (UnificationFailure
- (lazy ("not a mutind :"^
- CicMetaSubst.ppterm ~metasenv subst t2 ))))
- (* }}} elim H *)
- | _ -> raise exn)))
- | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
- let subst', metasenv',ugraph1 =
- fo_unif_subst test_equality_only subst context metasenv outt1 outt2
- ugraph in
- let subst'',metasenv'',ugraph2 =
- fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
- ugraph1 in
- (try
- List.fold_left2
- (fun (subst,metasenv,ugraph) t1 t2 ->
- fo_unif_subst
- test_equality_only subst context metasenv t1 t2 ugraph
- ) (subst'',metasenv'',ugraph2) pl1 pl2
+ let metasenv, subst =
+ instantiate rdb test_eq_only metasenv subst context j lj t2 true
+ in
+ (* We need to remove the out_scope_tags to avoid propagation of
+ them that triggers again the ad-hoc case *)
+ let subst =
+ List.map (fun (i,(tag,ctx,bo,ty)) ->
+ let tag =
+ List.filter
+ (function `InScope | `OutScope _ -> false | _ -> true) tag
+ in
+ i,(tag,ctx,bo,ty)
+ ) subst
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false))
+ | NCic.Meta (n, _), _ when is_locked n subst && swap ->
+ unify rdb test_eq_only metasenv subst context t2 t1 false
+
+ | t, C.Meta (n,lc) when List.mem_assoc n subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ unify rdb test_eq_only metasenv subst context t term swap
+ | C.Meta (n,_), _ when List.mem_assoc n subst ->
+ unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
+
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ unify rdb test_eq_only metasenv subst context t1
+ (mk_appl ~upto:(List.length args) term args) swap
+ | NCic.Appl (NCic.Meta (i,_)::_), _ when List.mem_assoc i subst ->
+ unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
+
+ | C.Meta (n,_), C.Meta (m,lc') when
+ let _,cc1,_ = NCicUtils.lookup_meta n metasenv in
+ let _,cc2,_ = NCicUtils.lookup_meta m metasenv in
+ (n < m && cc1 = cc2) ||
+ let len1 = List.length cc1 in
+ let len2 = List.length cc2 in
+ len2 < len1 && cc2 = fst (HExtlib.split_nth len2 cc1) ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)
+ | C.Meta (n,lc), C.Meta (m,lc') when
+ let _,_,tyn = NCicUtils.lookup_meta n metasenv in
+ let _,_,tym = NCicUtils.lookup_meta m metasenv in
+ let tyn = NCicSubstitution.subst_meta lc tyn in
+ let tym = NCicSubstitution.subst_meta lc tym in
+ match tyn,tym with
+ NCic.Sort NCic.Type u1, NCic.Sort NCic.Type u2 ->
+ NCicEnvironment.universe_lt u1 u2
+ | _,_ -> false ->
+ instantiate rdb test_eq_only metasenv subst context m lc'
+ (NCicReduction.head_beta_reduce ~subst t1) (not swap)
+ | C.Meta (n,lc), t ->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) swap
+ | t, C.Meta (n,lc) ->
+ instantiate rdb test_eq_only metasenv subst context n lc
+ (NCicReduction.head_beta_reduce ~subst t) (not swap)
+
+ (* higher order unification case *)
+ | NCic.Appl (NCic.Meta (i,l) as meta :: args), _ ->
+ (* this easy_case handles "(? ?) =?= (f a)", same number of
+ * args, preferring the instantiation "f" over "\_.f a" for the
+ * metavariable in head position. Since the arguments of the meta
+ * are flexible, delift would ignore them generating a constant
+ * function even in the easy case above *)
+ let easy_case =
+ match t2 with
+ | NCic.Appl (f :: f_args)
+ when
+ List.exists (NCicMetaSubst.is_flexible context ~subst) args ->
+ let mlen = List.length args in
+ let flen = List.length f_args in
+ let min_len = min mlen flen in
+ let mhe,margs = HExtlib.split_nth (mlen - min_len) args in
+ let fhe,fargs = HExtlib.split_nth (flen - min_len) f_args in
+ (try
+ Some (List.fold_left2
+ (fun (m, s) t1 t2 ->
+ unify rdb test_eq_only m s context t1 t2 swap
+ ) (metasenv,subst)
+ ((NCicUntrusted.mk_appl meta mhe)::margs)
+ ((NCicUntrusted.mk_appl f fhe)::fargs))
+ with UnificationFailure _ | Uncertain _ | KeepReducing _ ->
+ None)
+ | _ -> None
+ in
+ (match easy_case with
+ | Some ms -> ms
+ | None ->
+ (* This case handles "(?_f ..ti..) =?= t2", abstracting every
+ * non flexible ti (delift skips local context items that are
+ * flexible) from t2 in two steps:
+ * 1) ?_f := \..xi.. .?
+ * 2) ?_f ..ti.. =?= t2 --unif_machines-->
+ ?_f[..ti..] =?= t2 --instantiate-->
+ delift [..ti..] t2 *)
+ let metasenv, lambda_Mj =
+ lambda_intros rdb metasenv subst context (List.length args)
+ (NCicTypeChecker.typeof ~metasenv ~subst context meta)
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context
+ (C.Meta (i,l)) lambda_Mj swap
+ in
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context t1 t2 swap
+ in
+ (try
+ let name, ctx, term, ty = NCicUtils.lookup_subst i subst in
+ let term = eta_reduce subst term in
+ let subst = List.filter (fun (j,_) -> j <> i) subst in
+ metasenv, ((i, (name, ctx, term, ty)) :: subst)
+ with Not_found -> assert false))
+
+ | _, NCic.Appl (NCic.Meta (_,_) :: _) ->
+ unify rdb test_eq_only metasenv subst context t2 t1 (not swap)
+
+ (* processing this case here we avoid a useless small delta step *)
+ | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
+ when Ref.eq r1 r2 ->
+ let relevance = NCicEnvironment.get_relevance r1 in
+ let metasenv, subst, _ =
+ try
+ List.fold_left2
+ (fun (metasenv, subst, relevance) t1 t2 ->
+ let b, relevance =
+ match relevance with b::tl -> b,tl | _ -> true, [] in
+ let metasenv, subst =
+ try unify rdb test_eq_only metasenv subst context t1 t2
+ swap
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ metasenv, subst, relevance)
+ (metasenv, subst, relevance) tl1 tl2
+ with
+ Invalid_argument _ ->
+ raise (Uncertain (mk_msg metasenv subst context t1 t2))
+ | KeepReducing _ | KeepReducingThis _ -> assert false
+ in
+ metasenv, subst
+
+ | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
+ C.Match (ref2,outtype2,term2,pl2)) when Ref.eq ref1 ref2 ->
+ let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
+ let _,_,ty,_ = List.nth itl tyno in
+ let rec remove_prods ~subst context ty =
+ let ty = NCicReduction.whd ~subst context ty in
+ match ty with
+ | C.Sort _ -> ty
+ | C.Prod (name,so,ta) ->
+ remove_prods ~subst ((name,(C.Decl so))::context) ta
+ | _ -> assert false
+ in
+ let is_prop =
+ match remove_prods ~subst [] ty with
+ | C.Sort C.Prop -> true
+ | _ -> false
+ in
+ (* if not (Ref.eq ref1 ref2) then
+ raise (Uncertain (mk_msg metasenv subst context t1 t2))
+ else*)
+ let metasenv, subst =
+ unify rdb test_eq_only metasenv subst context outtype1 outtype2 swap in
+ let metasenv, subst =
+ try unify rdb test_eq_only metasenv subst context term1 term2 swap
+ with UnificationFailure _ | Uncertain _ when is_prop ->
+ metasenv, subst
+ in
+ (try
+ List.fold_left2
+ (fun (metasenv,subst) t1 t2 ->
+ unify rdb test_eq_only metasenv subst context t1 t2 swap)
+ (metasenv, subst) pl1 pl2
+ with Invalid_argument _ -> assert false)
+ | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+ | _ when norm1 && norm2 ->
+ if (could_reduce t1 || could_reduce t2) then
+ raise (Uncertain (mk_msg metasenv subst context t1 t2))
+ else
+ raise (UnificationFailure (mk_msg metasenv subst context t1 t2))
+ | _ -> raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+ (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
+ in
+ let fo_unif test_eq_only metasenv subst (norm1,t1 as nt1) (norm2,t2 as nt2)=
+ try fo_unif test_eq_only metasenv subst nt1 nt2
+ with
+ UnificationFailure _ | Uncertain _ when not norm1 || not norm2 ->
+ raise (KeepReducing (mk_msg metasenv subst context t1 t2))
+ in
+ let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) =
+ if NCicUntrusted.metas_of_term subst context t1 = [] &&
+ NCicUntrusted.metas_of_term subst context t2 = []
+ then None
+ else begin
+ (*D*) inside 'H'; try let rc =
+ pp(lazy ("\nProblema:\n" ^
+ ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^
+ ppterm ~metasenv ~subst ~context t2));
+ let candidates =
+ NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2
+ in
+ let rec cand_iter = function
+ | [] -> None (* raise exc *)
+ | (metasenv,(c1,c2),premises)::tl ->
+ pp (lazy ("\nProvo il candidato:\n" ^
+ String.concat "\n"
+ (List.map
+ (fun (a,b) ->
+ ppterm ~metasenv ~subst ~context a ^ " =?= " ^
+ ppterm ~metasenv ~subst ~context b) premises) ^
+ "\n-------------------------------------------\n"^
+ ppterm ~metasenv ~subst ~context c1 ^ " = " ^
+ ppterm ~metasenv ~subst ~context c2));
+ try
+ (*D*) inside 'K'; try let rc =
+ let metasenv,subst =
+ fo_unif test_eq_only metasenv subst mt1 (false,c1) in
+ let metasenv,subst =
+ fo_unif test_eq_only metasenv subst (false,c2) mt2 in
+ let metasenv,subst =
+ List.fold_left
+ (fun (metasenv, subst) (x,y) ->
+ unify rdb test_eq_only metasenv subst context x y false)
+ (metasenv, subst) (List.rev premises)
+ in
+ pp(lazy("FUNZIONA!"));
+ Some (metasenv, subst)
+ (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
+ with
+ KeepReducing _ | UnificationFailure _ | Uncertain _ -> cand_iter tl
+ | KeepReducingThis _ -> assert false
+ in
+ cand_iter candidates
+ (*D*) in outside None; rc with exn -> outside (Some exn); raise exn
+ end
+ in
+ let put_in_whd m1 m2 =
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
+ NCicReduction.reduce_machine ~delta:max_int ~subst context m2
+ in
+ let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) =
+ try fo_unif test_eq_only metasenv subst m1 m2
+ with
+ | UnificationFailure _ as exn -> raise exn
+ | KeepReducing _ | Uncertain _ as exn ->
+ let (t1,norm1 as tm1),(t2,norm2 as tm2) =
+ put_in_whd (0,[],t1,[]) (0,[],t2,[])
+ in
+ match
+ try_hints metasenv subst
+ (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+ with
+ | Some x -> x
+ | None ->
+ match exn with
+ | KeepReducing msg -> raise (KeepReducingThis (msg,tm1,tm2))
+ | Uncertain _ as exn -> raise exn
+ | _ -> assert false
+ in
+ let fo_unif_heads_and_cont_or_unwind_and_hints
+ test_eq_only metasenv subst m1 m2 cont hm1 hm2
+ =
+ let ms, continuation =
+ (* calling the continuation inside the outermost try is an option
+ and makes unification stronger, but looks not frequent to me
+ that heads unify but not the arguments and that an hints can fix
+ that *)
+ try fo_unif test_eq_only metasenv subst m1 m2, cont
+ with
+ | UnificationFailure _
+ | KeepReducing _ | Uncertain _ as exn ->
+ let (t1,norm1),(t2,norm2) = hm1, hm2 in
+ match
+ try_hints metasenv subst
+ (norm1,NCicReduction.unwind t1) (norm2,NCicReduction.unwind t2)
+ with
+ | Some x -> x, fun x -> x
+ | None ->
+ match exn with
+ | KeepReducing msg -> raise (KeepReducingThis (msg,hm1,hm2))
+ | UnificationFailure _ | Uncertain _ as exn -> raise exn
+ | _ -> assert false
+ in
+ continuation ms
+ in
+ let height_of = function
+ | NCic.Const (Ref.Ref (_,Ref.Def h))
+ | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
+ | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
+ | _ -> 0
+ in
+ let small_delta_step ~subst
+ ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
+ =
+ assert (not (norm1 && norm2));
+ if norm1 then
+ x1,NCicReduction.reduce_machine ~delta:0 ~subst context m2
+ else if norm2 then
+ NCicReduction.reduce_machine ~delta:0 ~subst context m1,x2
+ else
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
+ let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
+ NCicReduction.reduce_machine ~delta ~subst context m1,
+ NCicReduction.reduce_machine ~delta ~subst context m2
+ in
+ let rec unif_machines metasenv subst =
+ function
+ | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
+ (*D*) inside 'M'; try let rc =
+ pp (lazy("UM: " ^
+ ppterm ~metasenv ~subst ~context
+ (NCicReduction.unwind (k1,e1,t1,s1)) ^
+ " === " ^
+ ppterm ~metasenv ~subst ~context
+ (NCicReduction.unwind (k2,e2,t2,s2))));
+ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2));
+ let relevance = [] (* TO BE UNDERSTOOD
+ match t1 with
+ | C.Const r -> NCicEnvironment.get_relevance r
+ | _ -> [] *) in
+ let unif_from_stack (metasenv, subst) (t1, t2, b) =
+ try
+ let t1 = NCicReduction.from_stack ~delta:max_int t1 in
+ let t2 = NCicReduction.from_stack ~delta:max_int t2 in
+ unif_machines metasenv subst (put_in_whd t1 t2)
+ with UnificationFailure _ | Uncertain _ when not b ->
+ metasenv, subst
+ in
+ let rec check_stack l1 l2 r todo =
+ match l1,l2,r with
+ | x1::tl1, x2::tl2, r::tr-> check_stack tl1 tl2 tr ((x1,x2,r)::todo)
+ | x1::tl1, x2::tl2, []-> check_stack tl1 tl2 [] ((x1,x2,true)::todo)
+ | l1, l2, _ ->
+ NCicReduction.unwind (k1,e1,t1,List.rev l1),
+ NCicReduction.unwind (k2,e2,t2,List.rev l2),
+ todo
+ in
+ let check_stack l1 l2 r =
+ match t1, t2 with
+ | NCic.Meta _, _ | _, NCic.Meta _ ->
+ (NCicReduction.unwind (k1,e1,t1,s1)),
+ (NCicReduction.unwind (k2,e2,t2,s2)),[]
+ | _ -> check_stack l1 l2 r []
+ in
+ let hh1,hh2,todo = check_stack (List.rev s1) (List.rev s2) relevance in
+ try
+ fo_unif_heads_and_cont_or_unwind_and_hints
+ test_eq_only metasenv subst (norm1,hh1) (norm2,hh2)
+ (fun ms -> List.fold_left unif_from_stack ms todo)
+ m1 m2