let nuri_of_ouri o = NUri.uri_of_string (UriManager.string_of_uri o);;
+let mk_type n =
+ if n = 0 then
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
+ else
+ [false, NUri.uri_of_string ("cic:/matita/pts/Type"^string_of_int n^".univ")]
+;;
+
+let cprop = [false, NUri.uri_of_string ("cic:/matita/pts/CProp.univ")];;
+
(* porcatissima *)
type reference = Ref of NUri.uri * NReference.spec
let reference_of_ouri u indinfo =
| Cic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
| Cic.Appl l -> List.iter aux l
| Cic.MutCase (_,_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
- | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) -> aux ty; aux bo) fl
- | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) -> aux ty; aux bo) fl
+ | Cic.Fix (_, fl) -> List.iter (fun (_, _, ty, bo) -> aux ty; aux bo) fl; incr h
+ | Cic.CoFix (_, fl) -> List.iter (fun (_, ty, bo) -> aux ty; aux bo) fl; incr h
in
aux t;
1 + !h
UriManager.uri_of_string
(UriManager.buri_of_uri uri^"/"^
UriManager.name_of_uri uri ^ "___" ^ get_fresh () ^ ".con") in
- let height = height_of_term fix in
+ let height = height_of_term fix - 1 in
let bad_bctx, fixpoints_tys, tys, _ =
List.fold_right
(fun (name,recno,ty,_) (bctx, fixpoints, tys, idx) ->
let ty, fixpoints_ty = aux k octx ctx n_fix uri ty in
NCic.LetIn ("cast", ty, t, NCic.Rel 1), fixpoints_t @ fixpoints_ty
| Cic.Sort Cic.Prop -> NCic.Sort NCic.Prop,[]
- | Cic.Sort Cic.CProp -> NCic.Sort NCic.CProp,[]
+ | Cic.Sort Cic.CProp -> NCic.Sort (NCic.Type cprop),[]
| Cic.Sort (Cic.Type u) ->
- NCic.Sort (NCic.Type (CicUniv.get_rank u)),[]
- | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type 0),[]
+ NCic.Sort (NCic.Type (mk_type (CicUniv.get_rank u))),[]
+ | Cic.Sort Cic.Set -> NCic.Sort (NCic.Type (mk_type 0)),[]
(* calculate depth in the univ_graph*)
| Cic.Appl l ->
let l, fixpoints =
NCic.Const (reference_of_ouri curi Ref.Decl)
| _ -> assert false)
| Cic.MutInd (curi, tyno, ens) ->
- let is_inductive =
+ let is_inductive, lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false
in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno))))
| Cic.MutConstruct (curi, tyno, consno, ens) ->
+ let lno =
+ match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
+ Cic.InductiveDefinition (_,_,lno,_) -> lno
+ | _ -> assert false
+ in
aux_ens k curi octx ctx n_fix uri ens
- (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno))))
+ (NCic.Const (reference_of_ouri curi (Ref.Con (tyno,consno,lno))))
| Cic.Var (curi, ens) ->
(match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
Cic.Variable (_,Some bo,_,_,_) ->
aux k octx ctx n_fix uri (CicSubstitution.subst_vars ens bo)
| _ -> assert false)
| Cic.MutCase (curi, tyno, outty, t, branches) ->
- let is_inductive =
+ let is_inductive,lno =
match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph curi) with
- Cic.InductiveDefinition ([],_,_,_) -> true
- | Cic.InductiveDefinition ((_,b,_,_)::_,_,_,_) -> b
+ Cic.InductiveDefinition ([],_,lno,_) -> true, lno
+ | Cic.InductiveDefinition ((_,b,_,_)::_,_,lno,_) -> b, lno
| _ -> assert false in
- let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno)) in
+ let r = reference_of_ouri curi (Ref.Ind (is_inductive,tyno,lno)) in
let outty, fixpoints_outty = aux k octx ctx n_fix uri outty in
let t, fixpoints_t = aux k octx ctx n_fix uri t in
let branches, fixpoints =
aux varsno [] vars
;;
+let is_proof_irrelevant context ty =
+ match
+ CicReduction.whd context
+ (fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph))
+ with
+ Cic.Sort Cic.Prop -> true
+ | Cic.Sort _ -> false
+ | _ -> assert false
+;;
+
+exception InProp;;
+
+let get_relevance ty =
+ let rec aux context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) ->
+ not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t
+ | ty -> if is_proof_irrelevant context ty then raise InProp else []
+ in
+ try aux [] ty
+ with InProp -> []
+;;
+
let convert_obj_aux uri = function
| Cic.Constant (name, None, ty, vars, _) ->
let ty = cook `Pi vars ty in
let nty, fixpoints = convert_term uri ty in
assert(fixpoints = []);
- NCic.Constant ([], name, None, nty, (`Provided,`Theorem,`Regular)),
+ NCic.Constant (get_relevance ty, name, None, nty, (`Provided,`Theorem,`Regular)),
fixpoints
| Cic.Constant (name, Some bo, ty, vars, _) ->
let bo = cook `Lambda vars bo in
let nbo, fixpoints_bo = convert_term uri bo in
let nty, fixpoints_ty = convert_term uri ty in
assert(fixpoints_ty = []);
- NCic.Constant ([], name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
+ NCic.Constant (get_relevance ty, name, Some nbo, nty, (`Provided,`Theorem,`Regular)),
fixpoints_bo @ fixpoints_ty
| Cic.InductiveDefinition (itl,vars,leftno,_) ->
let ind = let _,x,_,_ = List.hd itl in x in
List.fold_right
(fun (name, _, ty, cl) (itl,acc) ->
let ty = cook `Pi vars ty in
- let ty, fix_ty = convert_term uri ty in
+ let nty, fix_ty = convert_term uri ty in
let cl, fix_cl =
List.fold_right
(fun (name, ty) (cl,acc) ->
let ty = cook `Pi vars ty in
- let ty, fix_ty = convert_term uri ty in
- ([], name, ty)::cl, acc @ fix_ty)
+ let nty, fix_ty = convert_term uri ty in
+ (get_relevance ty, name, nty)::cl, acc @ fix_ty)
cl ([],[])
in
- ([], name, ty, cl)::itl, fix_ty @ fix_cl @ acc)
+ (get_relevance ty, name, nty, cl)::itl, fix_ty @ fix_cl @ acc)
itl ([],[])
in
NCic.Inductive(ind, leftno + List.length
projects / helm.git / blobdiff