+let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ =
+ [],AutoTypes.cache_empty,AutoTypes.empty_universe
+;;
+
+(* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo
+ * la roba che non dipende da i *)
+let pi_of_ctx t i ctx =
+ let rec aux j = function
+ | [] -> t
+ | (Some (nam, Cic.Decl (term)))::tl -> Cic.Prod(nam,term,aux (j-1) tl)
+ | _ -> assert false (* not implemented *)
+ in
+ aux (List.length ctx-1) (List.rev ctx)
+;;
+
+let lambda_of_ctx t i ctx =
+ let rec aux j = function
+ | [] -> t
+ | (Some (nam, Cic.Decl (term)))::tl -> Cic.Lambda(nam,term,aux (j-1) tl)
+ | _ -> assert false (* not implemented *)
+ in
+ aux (List.length ctx -1) (List.rev ctx)
+;;
+
+let rec skip_lambda t l =
+ match t,l with
+ | Cic.Lambda (_,_,t), _::((_::_) as tl) -> skip_lambda t tl
+ | Cic.Lambda (_,_,t), _::[] -> t
+ | _ -> assert false
+;;
+
+let ty_of_eq = function
+ | Cic.Appl [Cic.MutInd (_, _, _); ty; _; _] -> ty
+ | _ -> assert false
+;;
+
+exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache
+
+let saturate_term context metasenv oldnewmeta term ?universe cache auto fast =
+ let head, metasenv, args, newmeta =
+ ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ in
+ let args_for_auto =
+ HExtlib.filter_map
+ (function
+ | Cic.Meta(i,_) ->
+ let _,_,mt = CicUtil.lookup_meta i metasenv in
+ let sort,u =
+ CicTypeChecker.type_of_aux' metasenv context mt
+ CicUniv.empty_ugraph
+ in
+ let b, _ =
+ CicReduction.are_convertible ~metasenv context
+ sort (Cic.Sort Cic.Prop) u
+ in
+ if b then Some i else None
+ (* maybe unif or conv should be used instead of = *)
+ | _ -> assert false)
+ args
+ in
+ let results,universe,cache =
+ if args_for_auto = [] then
+ let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+ [args,metasenv,newmetas,head,newmeta],universe,cache
+ else
+ let proof =
+ None,metasenv,term,term (* term non e' significativo *)
+ in
+ let flags =
+ if fast then
+ {AutoTypes.timeout = 1.0;maxwidth = 2;maxdepth = 2}
+ else
+ {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3}
+ in
+ match auto flags proof context ?universe cache args_for_auto with
+ | [],cache,universe -> raise (UnableToSaturate (Some universe,cache))
+ | substs,cache,universe ->
+ List.map
+ (fun subst ->
+ let metasenv =
+ CicMetaSubst.apply_subst_metasenv subst metasenv
+ in
+ let head = CicMetaSubst.apply_subst subst head in
+ let newmetas =
+ List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
+ in
+ let args = List.map (CicMetaSubst.apply_subst subst) args in
+ args,metasenv,newmetas,head,newmeta)
+ substs,
+ Some universe,cache
+ in
+ results,universe,cache
+;;
+
+let rec is_an_equality = function
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
+ when (LibraryObjects.is_eq_URI uri) -> true
+ | Cic.Prod (name, s, t) -> is_an_equality t
+ | _ -> false
+;;
+
+let build_equality_of_hypothesis index head args newmetas =
+ match head with
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
+ let p =
+ if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args)
+ in
+ debug_print
+ (lazy
+ (Printf.sprintf "OK: %s" (CicPp.ppterm p)));
+ let o = !Utils.compare_terms t1 t2 in
+ let stat = (ty,t1,t2,o) in
+ (* let w = compute_equality_weight stat in *)
+ let w = 0 in
+ let proof = Equality.Exact p in
+ Equality.mk_equality (w, proof, stat, newmetas)
+ | _ -> assert false
+;;
+
+let build_equality ty t1 t2 proof menv =
+ let o = !Utils.compare_terms t1 t2 in
+ let stat = (ty,t1,t2,o) in
+ let w = compute_equality_weight stat in
+ let proof = Equality.Exact proof in
+ Equality.mk_equality (w, proof, stat, menv)
+;;
+
+let find_equalities ?(auto = default_auto) context proof ?universe cache =
+ prerr_endline "find_equalities";