let debug_print s =
if debug then prerr_endline (Lazy.force s);;
+let is_propositional context sort =
+ match CicReduction.whd context sort with
+ | Cic.Sort Cic.Prop
+ | Cic.Sort (Cic.CProp _) -> true
+ | _-> false
+;;
+
+
type auto_params = Cic.term list * (string * string) list
let elems = ref [] ;;
let terms = List.map CicUtil.term_of_uri univ in
List.map
(fun t ->
- (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)))
+ (t,fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph)))
terms
let find_context_theorems context metasenv =
let _,_,mt = CicUtil.lookup_meta i metasenv in
let sort,u =
CicTypeChecker.type_of_aux' metasenv context mt
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
- let b, _ =
- CicReduction.are_convertible ~metasenv context
- sort (Cic.Sort Cic.Prop) u
- in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
let only signature context metasenv t =
try
let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
(fun t ->
let ty,_ =
CicTypeChecker.type_of_aux'
- metasenv context t CicUniv.empty_ugraph
+ metasenv context t CicUniv.oblivion_ugraph
in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty)
in
(* SIMPLIFICATION STEP
let equalities =
- let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let env = (metasenv, context, CicUniv.oblivion_ugraph) in
let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
Saturation.simplify_equalities bag eq_uri env units
in
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
+ CicUniv.oblivion_ugraph
in
- if b then Some i else None
+ if is_propositional context sort then Some i else None
| _ -> assert false)
args
in
HExtlib.filter_map
(fun t ->
let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty) else None)
equations in
in
let metasenv' = metasenv@newmetasenvfragment in
let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
in
let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
let goal_arity = count_prods context ty in
(****************** AUTO ********************)
let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
-let ugraph = CicUniv.empty_ugraph;;
+let ugraph = CicUniv.oblivion_ugraph;;
let typeof = CicTypeChecker.type_of_aux';;
let ppterm ctx t =
let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
CicPp.pp t names
;;
let is_in_prop context subst metasenv ty =
- let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
- fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
+ let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
+ is_propositional context sort
;;
let assert_proof_is_valid proof metasenv context goalty =
if debug then
begin
- let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+ let ty,u = typeof metasenv context proof CicUniv.oblivion_ugraph in
let b,_ = CicReduction.are_convertible context ty goalty u in
if not b then
begin
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
- let b,_ =
- CicReduction.are_convertible
- ~subst ~metasenv context sort (Cic.Sort Cic.Prop) u in
- b
+ is_propositional context sort
with
| CicTypeChecker.AssertFailure s
| CicTypeChecker.TypeCheckerFailure s ->
let order_new_goals metasenv subst open_goals ppterm =
let prop,rest = split_goals_in_prop metasenv subst open_goals in
let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in
+ let closed_type, open_type = split_goals_with_metas metasenv subst rest in
let open_goals =
- (List.map (fun x -> x,P) (closed_prop @ open_prop))
+ (List.map (fun x -> x,P) (open_prop @ closed_prop))
@
- (List.map (fun x -> x,T) rest)
+ (List.map (fun x -> x,T) (open_type @ closed_type))
in
let tys =
List.map
(* we demodulate using both actives passives *)
List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
in
- let env = metasenv,context,CicUniv.empty_ugraph in
+ let env = metasenv,context,CicUniv.oblivion_ugraph in
match Indexing.solve_demodulating bag env table initgoal steps with
| Some (proof, metasenv, newty) ->
let refl =
in
let changed,(newproof,newmetasenv, newty) =
Indexing.demodulation_goal bag
- (metasenv,context,CicUniv.empty_ugraph) table initgoal
+ (metasenv,context,CicUniv.oblivion_ugraph) table initgoal
in
if changed then
begin