if sort = `Prop then
let inductive_types =
(let o,_ =
- CicEnvironment.get_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
in
match o with
| Cic.InductiveDefinition (l,_,_,_) -> l
else raise Not_a_proof
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
let inductive_types,noparams =
- (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
let ind_str = (prefix ^ ".ind") in
let ind_uri = UriManager.uri_of_string ind_str in
let inductive_types,noparams =
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
match o with
| Cic.InductiveDefinition (l,_,n,_) -> (l,n)
| _ -> assert false
}
let get_types uri =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno
| _ -> assert false
*)
let get_type msg st bo =
try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+ let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
ty
with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
let get_ind_names uri tno =
try
- let ts = match E.get_obj Un.empty_ugraph uri with
+ let ts = match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (ts, _, _, _), _ -> ts
| _ -> assert false
in
aux [] c
let elim_inferred_type context goal arg using cpattern =
- let metasenv, ugraph = [], Un.empty_ugraph in
+ let metasenv, ugraph = [], Un.oblivion_ugraph in
let ety, _ugraph = TC.type_of_aux' metasenv context using ugraph in
let _splits, args_no = PEH.split_with_whd (context, ety) in
let _metasenv, predicate, _arg, actual_args = PT.mk_predicate_for_elim
let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
with e ->
Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
raise e
let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+ try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
with e ->
Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
let is_atomic t = not (is_not_atomic t)
let get_ind_type uri tyno =
- match E.get_obj Un.empty_ugraph uri with
+ match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
| _ -> assert false
let get_type msg c bo =
try
- let ty, _ = TC.type_of_aux' [] c bo Un.empty_ugraph in
+ let ty, _ = TC.type_of_aux' [] c bo Un.oblivion_ugraph in
ty
with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
let xxx_type_of_aux' m c t =
let res,_ =
try
- CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph
with
| CicTypeChecker.AssertFailure _
| CicTypeChecker.TypeCheckerFailure _ ->
- Cic.Sort Cic.Prop, CicUniv.empty_ugraph
+ Cic.Sort Cic.Prop, CicUniv.oblivion_ugraph
in
res
;;
let xxx_type_of_aux' m c t =
try
- Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
+ Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.oblivion_ugraph))
with
| CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
;;
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked constant")
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
| CicEnvironment.UncheckedObj (C.Variable _,_) ->
raise (NotWellTyped "Reference to an unchecked variable")
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked inductive type")
let module R = CicReduction in
let module U = UriManager in
let cobj =
- match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
+ match CicEnvironment.is_type_checked CicUniv.oblivion_ugraph uri with
CicEnvironment.CheckedObj (cobj,_) -> cobj
| CicEnvironment.UncheckedObj (uobj,_) ->
raise (NotWellTyped "Reference to an unchecked constructor")
let (cl,parsno) =
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
match obj with
let uris_and_types =
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
let params = CicUtil.params_of_obj obj in
(function uri ->
let obj,_ =
try
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
with Not_found -> assert false
in
match obj with
let tl' = List.map (eta_fix' context) tl in
let ty,_ =
CicTypeChecker.type_of_aux' metasenv context he
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
fix_according_to_type ty (eta_fix' context he) tl'
(*
let term' = eta_fix' context term in
let patterns' = List.map (eta_fix' context) patterns in
let inductive_types,noparams =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> assert false
| Cic.Variable _ -> assert false
else
let term_type,_ =
CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
(match term_type with
C.Appl (hd::params) ->
(fun newsubst (uri,t) ->
let t' = eta_fix' context t in
let ty =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
Cic.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars newsubst ty
raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
) branches
else
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
Cic.InductiveDefinition (il,_,leftsno,_) ->
let _,_,_,cl =
try
(try
match cic with
| Cic.Const (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Const (uri, mk_subst uris)
| Cic.Var (uri, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.Var (uri, mk_subst uris)
| Cic.MutInd (uri, i, []) ->
(try
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutInd (uri, i, mk_subst uris)
with
(*here the explicit_named_substituion is assumed to be of length 0 *)
Cic.MutInd (uri,i,[]))
| Cic.MutConstruct (uri, i, j, []) ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let uris = CicUtil.params_of_obj o in
Cic.MutConstruct (uri, i, j, mk_subst uris)
| Cic.Meta _ | Cic.Implicit _ as t ->
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
let disambiguate_thing ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
(thing_txt,thing_txt_prefix_len,thing)
=
failwith "Disambiguate: circular dependency"
let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
- ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+ ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
(text,prefix_len,term)
=
let term =
(if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
| C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
let nparams =
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (_,_,nparams,_) -> nparams
| _ -> assert false in
let hes = pp ~in_type he context in
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
qualified_name_of_uri current_module_uri
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
if patterns = [] then "assert false"
else
(let connames_and_argsno, go_up, go_pu, go_down, go_nwod =
- (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,paramsno,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
let rc =
(let candidate,ugraph5,metasenv,subst =
let exp_name_subst, metasenv =
let o,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri
in
let uris = CicUtil.params_of_obj o in
List.fold_right (
metasenv,ugraph,substituted_tys
let typecheck metasenv uri obj ~localization_tbl =
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
(* CSC: ugly code. Here I need to retrieve in advance the loc of bo
(fun arity (c,saturations) ->
let ty,_ =
CicTypeChecker.type_of_aux' ~subst metasenv context c
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let _,metasenv,args,lastmeta =
TermUtil.saturate_term ~delta:false freshmeta metasenv context ty arity in
let irl =
| Cic.Appl (he::_) -> CicUtil.uri_of_term he
| _ -> CicUtil.uri_of_term t
in
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.Constant (_,_, _, _, attrs),_ ->
List.exists (function `Class (`Coercion _) -> true | _ -> false) attrs
| _ -> false
| _ -> 0
in
let uri = CicUtil.uri_of_term c in
- match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
| Cic.Constant (_, _, ty, _, _) -> count_pi ty
| _ -> assert false
in
let is_a_coercion uri =
try
let obj,_ =
- CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
try
match List.find
let t = CicUtil.term_of_uri u in
let ty',g =
CicTypeChecker.type_of_aux'
- metasenv' [] t CicUniv.empty_ugraph
+ metasenv' [] t CicUniv.oblivion_ugraph
in
fst(CicReduction.are_convertible [] ty' ty g))
similar
let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
let add_to_universe (universe,status) uri =
let term = CicUtil.term_of_uri uri in
- let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
(* prop filtering
- let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
+ let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.oblivion_ugraph in
prerr_endline (CicPp.ppterm term);
prerr_endline (CicPp.ppterm sort);
let tkeys =
let add_aliases_for_objs =
List.fold_left
(fun status uri ->
- let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
add_aliases_for_object status uri obj)
module OrderedId =
let elim_of ~sort uri typeno =
counter := ~-1;
- let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+ let (obj, univ) = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
match obj with
| Cic.InductiveDefinition (indTypes, params, leftno, _) ->
let (name, inductive, ty, constructors) =
*)
let (computed_type, ugraph) =
try
- CicTypeChecker.type_of_aux' [] [] eliminator_body CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' [] [] eliminator_body
+ CicUniv.oblivion_ugraph
with CicTypeChecker.TypeCheckerFailure msg ->
raise (Elim_failure (lazy (sprintf
"type checker failure while type checking:\n%s\nerror:\n%s"
let projections_of uri field_names =
let buri = UriManager.buri_of_uri uri in
- let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let obj,ugraph = CicEnvironment.get_cooked_obj CicUniv.oblivion_ugraph uri in
match obj with
Cic.InductiveDefinition ([_,_,sort,[_,ty]],params,paramsno,_) ->
assert (params = []); (* general case not implemented *)
List.iter remove_single_obj !uris;
raise exn
in
- let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+ let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
match obj with
| Cic.InductiveDefinition (indTypes, _, _, _) ->
let counter = ref 0 in
=
let coer_ty,_ =
let coer = CicUtil.term_of_uri uri in
- CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph
in
(* we have to get the source and the tgt type uri
* in Coq syntax we have already their names, but
(fun (uri, name, bo) (_name, coercion, arity) ->
let saturations = 0 in
try
- let ty, ugraph =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
let attrs = [`Class `Projection; `Generated] in
let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
add_single_obj uri obj refinement_toolkit;
List.flatten
(List.map
(fun uri ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
projections_of (CicUtil.projections_of_record o uri))
uris)
in
| _ -> assert false
let var_has_body uri =
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| Cic.Variable (_, Some body, _, _, _), _ -> true
| _ -> false
List.length (List.filter (non var_has_body) params)
let rec compute_var pos uri =
- let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.Variable (_, Some _, _, _, _) -> S.empty
| Cic.Variable (_, None, ty, params, _) ->
| _ -> assert false
let compute_obj uri =
- let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
| Cic.Variable (_, body, ty, params, _)
| Cic.Constant (_, body, ty, params, _) ->
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
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
+ CicUniv.oblivion_ugraph
in
let b, _ =
CicReduction.are_convertible ~metasenv context
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
+ let sort,u = typeof ~subst metasenv context ty CicUniv.oblivion_ugraph in
fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
;;
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
(* 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
let o,univ = build_obj t univ arityres in
(o,saturationsres,arityres),univ
| _ -> assert false
- ) (first_step, CicUniv.empty_ugraph) tl
+ ) (first_step, CicUniv.oblivion_ugraph) tl
in
let name_src = CoercDb.name_of_carr src in
let name_tgt = CoercDb.name_of_carr tgt in
Cic.MutInd (uri,0,[]), Cic.Const (LibraryObjects.trans_eq_URI ~eq:uri,[])
in
let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.oblivion_ugraph in
let just' =
match just with
`Auto (univ, params) ->
let mk_branches_and_outtype turi typeno consno context args =
(* a list of "True" except for the element in position consno which
* is "False" *)
- match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+ match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_) ->
let _,_,rty,constructor_list = List.nth ind_type_list typeno in
let false_constr_id,_ = List.nth constructor_list (consno - 1) in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
- CTC.type_of_aux' metasenv context term CU.empty_ugraph
+ CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
in
match termty with
| C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
debug_print (lazy ("\nclear di: " ^ pp context term));
debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
let g () = if first_time then raise exn_nothingtodo else T.id_tac in
* del costruttore *)
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
let termty,_ =
- CTC.type_of_aux' metasenv context term CU.empty_ugraph
+ CTC.type_of_aux' metasenv context term CU.oblivion_ugraph
in
debug_print (lazy ("\ninjection su : " ^ pp context termty));
match termty with (* an equality *)
List.nth applist1 (pred i),List.nth applist2 (pred i),consno2
| _ -> assert false
in
- let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
+ let tty',_ = CTC.type_of_aux' metasenv context t1' CU.oblivion_ugraph in
let patterns,outtype =
- match fst (CicEnvironment.get_obj CU.empty_ugraph turi) with
+ match fst (CicEnvironment.get_obj CU.oblivion_ugraph turi) with
| C.InductiveDefinition (ind_type_list,_,paramsno,_)->
let left_params, right_params = HExtlib.split_nth paramsno params in
let _,_,_,constructor_list = List.nth ind_type_list typeno in
let go_on =
try
let _,g = CTC.type_of_aux' metasenv context cutted
- CU.empty_ugraph
+ CU.oblivion_ugraph
in
let _,g = CTC.type_of_aux' metasenv context changed g in
fst (CR.are_convertible ~metasenv context t1' changed g)
let (proof, goal) = status in
let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
debug_print (lazy ("\nsubst " ^ (match direction with `LeftToRight -> "->" | `RightToLeft -> "<-") ^ " di: " ^ pp context term));
let tactic = match where with
| None ->
let rec destruct ~first_time lterm =
let are_convertible hd1 hd2 metasenv context =
- fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
+ fst (CR.are_convertible ~metasenv context hd1 hd2 CU.oblivion_ugraph)
in
let recur = destruct ~first_time:false in
let destruct status =
let (proof, goal) = status in
let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let term, metasenv, _ugraph = lterm context metasenv CU.empty_ugraph in
+ let term, metasenv, _ugraph = lterm context metasenv CU.oblivion_ugraph in
let tactic = if not (first_time || exists context term) then T.id_tac else begin
debug_print (lazy ("\ndestruct di: " ^ pp context term));
debug_print (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
- let termty,_ = CTC.type_of_aux' metasenv context term CU.empty_ugraph in
+ let termty,_ = CTC.type_of_aux' metasenv context term CU.oblivion_ugraph in
debug_print (lazy ("\ndestruct su: " ^ pp context termty));
let mk_lterm term c m ug =
let distance = List.length c - List.length context in
let premise_pattern what = None, [what, C.Implicit (Some `Hole)], None
let get_inductive_def uri =
- match E.get_obj Un.empty_ugraph uri with
+ match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ ->
lpsno, tys
| _ -> assert false
let _, psno = PEH.split_with_whd ([], arity) in
let not_relation = (lpsno = psno) in
let not_recursive = is_not_recursive uri tyno tys in
- let ty_ty, _ = TC.type_of_aux' metasenv context t Un.empty_ugraph in
+ let ty_ty, _ = TC.type_of_aux' metasenv context t Un.oblivion_ugraph in
let sort = match PEH.split_with_whd (context, ty_ty) with
| (_, C.Sort sort) ::_ , _ -> CicPp.ppsort sort
| (_, C.Meta _) :: _, _ -> CicPp.ppsort (C.Type (Un.fresh ()))
in
let ty_eq,ugraph =
CicTypeChecker.type_of_aux' metasenv context equality
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let (ty_eq,metasenv',arguments,fresh_meta) =
TermUtil.saturate_term
(ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in
in
let context_len = List.length context in
let subst,metasenv,u,_,selected_terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
let with_what, metasenv, u = with_what context metasenv u in
let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =
CicTypeChecker.type_of_aux'
- metasenv context with_what CicUniv.empty_ugraph in
+ metasenv context with_what CicUniv.oblivion_ugraph in
let whats =
match selected_terms_with_context with
[] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
(lazy "Replace: one of the selected terms is not closed")) in
let ty_of_t_in_context,u = (* TASSI: FIXME *)
CicTypeChecker.type_of_aux' metasenv context t_in_context
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
let b,u = CicReduction.are_convertible ~metasenv context
ty_of_with_what ty_of_t_in_context u in
if b then
let lapply_tac (proof, goal) =
let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
+ let lemma, _ = TC.type_of_aux' metasenv context what U.oblivion_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
let metasenv, metas, conts = strip_prods metasenv context ?how_many to_what lemma in
let conclusion =
| Some uri -> uri
in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
- let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let uri = baseuri_of_term termty in
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let (_,_,typeno,_) =
match termty with
C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
let parameters_tys =
(List.map
(fun t -> (
- match (T.type_of_aux' metasenv context t CicUniv.empty_ugraph) with
+ match (T.type_of_aux' metasenv context t CicUniv.oblivion_ugraph) with
(term,graph) -> term))
parameters)
in
(*DEBUG*) debug_print (lazy ("private inversion: term before refinement: " ^
CicPp.ppterm t));
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
(*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: "
^ CicPp.ppterm ref_t));
(*DEBUG*) debug_print (lazy ("inversion begins"));
let _,metasenv,_subst,_,_, _ = proof in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
- let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let uri, typeno =
match termty with
| Cic.MutInd (uri,typeno,_)
| _ -> assert false
in
(* let uri = baseuri_of_term termty in *)
- let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
let name,nleft,arity,cons_list =
match obj with
Cic.InductiveDefinition (tys,_,nleft,_) ->
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
let (t1,metasenv,_subst,t3,t4, attrs) = proof in
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
let proof3,gl3 =
debug_print
(lazy ("theorem prima di refine: " ^ (CicPp.ppterm theorem)));
let (ref_theorem,_,metasenv,_) = CicRefine.type_of_aux' [] [] theorem
- CicUniv.empty_ugraph in
+ CicUniv.oblivion_ugraph in
(*DEBUG*) debug_print
(lazy ("theorem dopo refine: " ^ (CicPp.ppterm ref_theorem)));
let buri = UriManager.buri_of_uri uri in
try
let ty,_ =
CicTypeChecker.type_of_aux'
- metasenv current_ctx t CicUniv.empty_ugraph
+ metasenv current_ctx t CicUniv.oblivion_ugraph
in
let sort,_ =
CicTypeChecker.type_of_aux'
- metasenv current_ctx ty CicUniv.empty_ugraph
+ metasenv current_ctx ty CicUniv.oblivion_ugraph
in
let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
match sort with
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
- CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph
in
let ty_sort2,_ =
- CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph
in
let prop1 =
let b,_ =
CicReduction.are_convertible
- ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
+ ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph
in
if b then 0
else 1
let prop2 =
let b,_ =
CicReduction.are_convertible
- ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
+ ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph
in
if b then 0
else 1
(fun e bag ->
let t = CicUtil.term_of_uri e in
let ty, _ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
in
Constr.UriManagerSet.union bag (Constr.constants_of ty))
s s
match t with
Cic.MutInd (uri,_,_)
| Cic.MutConstruct (uri,_,_,_) ->
- (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
Cic.InductiveDefinition(tl,_,_,_) ->
snd
(List.fold_left
let is_predicate u =
let ty, _ =
try CicTypeChecker.type_of_aux' [] []
- (CicUtil.term_of_uri u) CicUniv.empty_ugraph
+ (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
with CicTypeChecker.TypeCheckerFailure _ -> assert false
in
let rec check_last_pi = function
let only constants uri =
prerr_endline (UriManager.string_of_uri uri);
let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
- let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
let consts = Constr.constants_of ty in
(*
prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
(fun (i,acc) _ ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+ metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
let newty = types_of_equality ty in
(i+1,Constr.SetSet.union newty acc))
(1,all) context
| Some (main,_) ->
let ty, _ =
CicTypeChecker.type_of_aux'
- metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+ metasenv context (CicUtil.term_of_uri main)
+ CicUniv.oblivion_ugraph
in
Constr.constants_of ty
in
| None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
in
let ty_term,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac
List.map (function uri,t -> uri,aux n t)
in
let argty,_ =
- T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *)
+ T.type_of_aux' metasenv context arg CicUniv.oblivion_ugraph (* TASSI: FIXME *)
in
let fresh_name =
FreshNamesGenerator.mk_fresh_name ~subst:[]
=
let module C = Cic in
let params =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
CicUtil.params_of_obj o
in
let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
[],[] -> []
| uri::tl,[] ->
let ty =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Variable (_,_,ty,_,_) ->
CicSubstitution.subst_vars !exp_named_subst_diff ty
goal_arity in
let subst,newmetasenv',_ =
CicUnification.fo_unif_subst
- subst context newmetasenv consthead ty CicUniv.empty_ugraph
+ subst context newmetasenv consthead ty CicUniv.oblivion_ugraph
in
let t =
if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
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
(ProofEngineTypes.Fail (lazy
"You can't letin a term containing the current goal"));
let tty,_ =
- CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let fresh_name =
mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
- let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
if b then
begin
| None, [], Some cpattern -> cpattern
| _ -> raise (PET.Fail (lazy "not implemented"))
in
- let ugraph = CicUniv.empty_ugraph in
+ let ugraph = CicUniv.oblivion_ugraph in
let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
let conjecture = CicUtil.lookup_meta goal metasenv in
let metano, context, ty = conjecture in
let module C = Cic in
let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
let termty = CicReduction.whd context termty in
let (termty,metasenv',arguments,fresh_meta) =
TermUtil.saturate_term
| _ -> raise NotAnInductiveTypeToEliminate
in
let paramsno,itty,patterns,right_args =
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
| C.InductiveDefinition (tys,_,paramsno,_),_ ->
let _,left_parameters,right_args =
List.fold_right
let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
let refined_term,_,metasenv'',_ =
CicRefine.type_of_aux' metasenv' context term_to_refine
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
let new_goals =
ProofEngineHelpers.compare_metasenvs
with
Failure _ -> assert false)
| Cic.Const (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant (_,Some body,_,_,_) ->
CicReduction.head_beta_reduce
| Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
| Cic.Var (uri,exp_named_subst) as t ->
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
(match o with
Cic.Constant _ -> raise ReferenceToConstant
| Cic.CurrentProof _ -> raise ReferenceToCurrentProof
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant _ -> raise ReferenceToConstant
| C.CurrentProof _ -> raise ReferenceToCurrentProof
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
match o with
C.Constant (_,Some body,_,_,_) ->
if List.exists is_active l then
C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
| C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
let (arity, r) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+ let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
match o with
C.InductiveDefinition (tl,ingredients,r,_) ->
let (_,_,arity,_) = List.nth tl i in
prerr_endline (CicPp.ppterm t2 ^ "\n");
let subst1, _, _ =
CicUnification.fo_unif metasenv ctx t1 t2
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
in
prerr_endline "UNIFICANO\n\n\n";
subst := subst1;
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
(try
ignore
(CicTypeChecker.type_of_aux' metasenv context te
- CicUniv.empty_ugraph (* TASSI: FIXME *));
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
ignore
(CicTypeChecker.type_of_aux' metasenv context ty
- CicUniv.empty_ugraph (* TASSI: FIXME *));
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *));
with
_ ->
raise
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph (* TASSI: FIXME *)
+ CicUniv.oblivion_ugraph (* TASSI: FIXME *)
with
_ ->
raise
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise
(PET.Fail
let _,_ =
try
CicTypeChecker.type_of_aux' metasenv canonical_context' ty
- CicUniv.empty_ugraph
+ CicUniv.oblivion_ugraph
with _ ->
raise (PET.Fail (lazy ("Hypothesis " ^ hyp ^ " occurs in the goal")))
in
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern
in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph ~conjecture
~pattern in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
let context', metasenv, ugraph =
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
let b,_ = (*TASSI : FIXME*)
- are_convertible context t1'' t1 CicUniv.empty_ugraph in
+ are_convertible context t1'' t1 CicUniv.oblivion_ugraph in
if not b then begin
warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
let newstatus =
let status' =
let context = context_of_status status in
let b,_ = (* TASSI:FIXME *)
- are_convertible context t2'' t2 CicUniv.empty_ugraph
+ are_convertible context t2'' t2
+ CicUniv.oblivion_ugraph
in
if not b then begin
warn (lazy "t2'' and t2 are NOT CONVERTIBLE");
let argsno = List.length args' - rel.rel_quantifiers_no in
let args1 = list_sub args' 0 argsno in
let args2 = list_sub args' argsno rel.rel_quantifiers_no in
- if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1)) CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] rel.rel_a (Cic.Appl (he'::args1))
+ CicUniv.oblivion_ugraph) then
args2
else
raise_error rel.rel_quantifiers_no
| _ ->
- if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible [] rel.rel_a t CicUniv.empty_ugraph) then
+ if rel.rel_quantifiers_no = 0 && fst (CicReduction.are_convertible []
+ rel.rel_a t CicUniv.oblivion_ugraph) then
[]
else
begin
(*COQ
let evars,args,instantiated_rel_a =
- let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a CicUniv.empty_ugraph in
+ let ty = CicTypeChecker.type_of_aux' [] [] rel.rel_a
+ CicUniv.oblivion_ugraph in
let evd = Evd.create_evar_defs Evd.empty in
let evars,args,concl =
Clenv.clenv_environments_evars env evd
let unify_relation_class_carrier_with_type env rel t =
match rel with
Leibniz (Some t') ->
- if fst (CicReduction.are_convertible [] t t' CicUniv.empty_ugraph) then
+ if fst (CicReduction.are_convertible [] t t' CicUniv.oblivion_ugraph) then
rel
else
raise (ProofEngineTypes.Fail (lazy
prerr_endline "PRIMA DELLA PRIMA TYPE OF " ;
*)
let ty_sort1,u = (*TASSI: FIXME *)
- CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph in
+ CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph in
(*
prerr_endline (Printf.sprintf "PRIMA DELLA SECONDA TYPE OF %s \n### %s @@@%s " (CicMetaSubst.ppmetasenv metasenv []) (CicMetaSubst.ppcontext [] ey2) (CicMetaSubst.ppterm [] ty2));
*)
let remove_uri univ uri =
let term = CicUtil.term_of_uri uri in
- let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
remove univ [] term ty
(match hd with
(Some (_, C.Decl t)) when
fst (R.are_convertible context (S.lift n t) ty
- CicUniv.empty_ugraph) -> n
+ CicUniv.oblivion_ugraph) -> n
| (Some (_, C.Def (_,ty'))) when
fst (R.are_convertible context (S.lift n ty') ty
- CicUniv.empty_ugraph) -> n
+ CicUniv.oblivion_ugraph) -> n
| _ -> find (n+1) tl
)
| [] -> raise (PET.Fail (lazy "Assumption: No such assumption"))
let uri,metasenv,_subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern in
let context = CicMetaSubst.apply_subst_context subst context in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
projects / helm.git / commitdiff