let _,_,mt = CicUtil.lookup_meta i metasenv in
let sort,u =
CicTypeChecker.type_of_aux' metasenv context mt
let _,_,mt = CicUtil.lookup_meta i metasenv in
let sort,u =
CicTypeChecker.type_of_aux' metasenv context mt
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty)
in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty)
let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
Saturation.simplify_equalities bag eq_uri env units
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
let _,_,mt = CicUtil.lookup_meta i metasenv in
let sort,u =
CicTypeChecker.type_of_aux' metasenv context mt
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty) else None)
equations in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty) else None)
equations in
in
let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
let goal_arity = count_prods context ty in
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;;
(****************** AUTO ********************)
let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
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 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 _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
let _,context,ty = CicUtil.lookup_meta g metasenv in
try
let sort,u = typeof ~subst metasenv context ty ugraph in
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 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
type subst = Cic.substitution
type goal = ProofEngineTypes.goal * int * AutoTypes.sort
let candidate_no = ref 0;;
type subst = Cic.substitution
type goal = ProofEngineTypes.goal * int * AutoTypes.sort
let candidate_no = ref 0;;
type cache = AutoCache.cache
type tables =
Saturation.active_table * Saturation.passive_table * Equality.equality_bag
type cache = AutoCache.cache
type tables =
Saturation.active_table * Saturation.passive_table * Equality.equality_bag
(* the status exported to the external observer *)
type auto_status =
(* context, (goal,candidate) list, and_list, history *)
(* the status exported to the external observer *)
type auto_status =
(* context, (goal,candidate) list, and_list, history *)
- Cic.context * (int * Cic.term * bool * int * (int * Cic.term) list) list *
- (int * Cic.term * int) list * Cic.term list
+ Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
+ (int * Cic.term * int) list * Cic.term Lazy.t list
| None -> Printf.sprintf "D(%d, _, %d)" gi d
in
let string_of_s m su k (ci,ct) gi =
| None -> Printf.sprintf "D(%d, _, %d)" gi d
in
let string_of_s m su k (ci,ct) gi =
- Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp ct) ci
+ Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
- None,metasenv,subst ,Cic.Meta(goalno,mk_irl context),goalty, []
+ None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
let open_goals = order_new_goals metasenv subst open_goals ppterm in
let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
incr candidate_no;
let open_goals = order_new_goals metasenv subst open_goals ppterm in
let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
incr candidate_no;
- Some ((!candidate_no,cand),metasenv,subst,open_goals), tables , maxmeta
+ Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
with
| ProofEngineTypes.Fail s -> None,tables, maxm
| CicUnification.Uncertain s -> None,tables, maxm
with
| ProofEngineTypes.Fail s -> None,tables, maxm
| CicUnification.Uncertain s -> None,tables, maxm
(* we demodulate using both actives passives *)
List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
in
(* we demodulate using both actives passives *)
List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
in
match Indexing.solve_demodulating bag env table initgoal steps with
| Some (proof, metasenv, newty) ->
let refl =
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
in
let changed,(newproof,newmetasenv, newty) =
Indexing.demodulation_goal bag