-let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
-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.oblivion_ugraph in
- is_propositional context sort
-;;
-
-exception NotConvertible;;
-
-let check_proof_is_valid proof metasenv context goalty =
- if debug then
- begin
- try
- 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 raise NotConvertible else b
- with _ ->
- let names =
- List.map (function None -> None | Some (x,_) -> Some x) context
- in
- debug_print (lazy ("PROOF:" ^ CicPp.pp proof names));
- (* debug_print (lazy ("PROOFTY:" ^ CicPp.pp ty names)); *)
- debug_print (lazy ("GOAL:" ^ CicPp.pp goalty names));
- debug_print (lazy ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv));
- false
- end
- else true
-;;
-
-let assert_proof_is_valid proof metasenv context goalty =
- assert (check_proof_is_valid proof metasenv context goalty)
-;;
-
-let assert_subst_are_disjoint subst subst' =
- if debug then
- assert(List.for_all
- (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
- subst)
- else ()
-;;
-
-let split_goals_in_prop metasenv subst gl =
- List.partition
- (fun g ->
- let _,context,ty = CicUtil.lookup_meta g metasenv in
- try
- let sort,u = typeof ~subst metasenv context ty ugraph in
- is_propositional context sort
- with
- | CicTypeChecker.AssertFailure s
- | CicTypeChecker.TypeCheckerFailure s ->
- debug_print
- (lazy ("NON TIPA" ^ ppterm context (CicMetaSubst.apply_subst subst ty)));
- debug_print s;
- false)
- (* FIXME... they should type! *)
- gl
-;;
-
-let split_goals_with_metas metasenv subst gl =
- List.partition
- (fun g ->
- let _,context,ty = CicUtil.lookup_meta g metasenv in
- let ty = CicMetaSubst.apply_subst subst ty in
- CicUtil.is_meta_closed ty)
- gl
-;;
-
-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) (open_prop @ closed_prop))
- @
- (List.map (fun x -> x,T) (open_type @ closed_type))
- in
- let tys =
- List.map
- (fun (i,sort) ->
- let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty,sort) open_goals
- in
- debug_print (lazy (" OPEN: "^
- String.concat "\n"
- (List.map
- (function
- | (i,t,P) -> string_of_int i ^ ":"^ppterm t^ "Prop"
- | (i,t,T) -> string_of_int i ^ ":"^ppterm t^ "Type")
- tys)));
- open_goals
-;;