(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
the return type is a sort *)
(*CSC: cut&paste from nCicReduction.split_prods, but does not check that
the return type is a sort *)
-let rec my_split_prods ~subst context n te =
- match (n, NCicReduction.whd ~subst context te) with
+let rec my_split_prods status ~subst context n te =
+ match (n, NCicReduction.whd status ~subst context te) with
| (0, _) -> context,te
| (n, NCic.Prod (name,so,ta)) ->
| (0, _) -> context,te
| (n, NCic.Prod (name,so,ta)) ->
| (n, _) when n <= 0 -> context,te
| (_, _) -> raise (Failure "my_split_prods")
;;
| (n, _) when n <= 0 -> context,te
| (_, _) -> raise (Failure "my_split_prods")
;;
let _,ind_name,ty,cl = it in
let srec_name = ind_name ^ "_" ^ suffix in
let rec_name = mk_id srec_name in
let name_of_k id = mk_id ("H_" ^ id) in
let p_name = mk_id "Q_" in
let _,ind_name,ty,cl = it in
let srec_name = ind_name ^ "_" ^ suffix in
let rec_name = mk_id srec_name in
let name_of_k id = mk_id ("H_" ^ id) in
let p_name = mk_id "Q_" in
let args = List.rev_map (function name,_ -> mk_id name) args in
let rec_arg = mk_id (fresh_name ()) in
let p_ty =
let args = List.rev_map (function name,_ -> mk_id name) args in
let rec_arg = mk_id (fresh_name ()) in
let p_ty =
- let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
- let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
+ let _,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in
+ let cargs,ty= my_split_prods status ~subst:[] [] (-1) ty in
let cargs_and_recursive_args =
List.rev_map
(function
_,NCic.Def _ -> assert false
| name,NCic.Decl ty ->
let cargs_and_recursive_args =
List.rev_map
(function
_,NCic.Def _ -> assert false
| name,NCic.Decl ty ->
-let mk_elims (uri,_,_,_,obj) =
+let mk_elims status (uri,_,_,_,obj) =
match obj with
NCic.Inductive (true,leftno,[itl],_) ->
match obj with
NCic.Inductive (true,leftno,[itl],_) ->
(* this code should be unified with NTermCicContent.nast_of_cic0,
but the two contexts have different types *)
(* this code should be unified with NTermCicContent.nast_of_cic0,
but the two contexts have different types *)
let name = NUri.name_of_uri uri in
let case_indty = Some (name, None) in
let constructors, leftno =
let name = NUri.name_of_uri uri in
let case_indty = Some (name, None) in
let constructors, leftno =
- let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in
+ let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
let _,_,_,cl = List.nth tys n in
cl,leftno
in
let _,_,_,cl = List.nth tys n in
cl,leftno
in
with Invalid_argument _ -> assert false
in
NotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns)
with Invalid_argument _ -> assert false
in
NotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns)
let outtype= NotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
[arg, Some arg_ty], NotationPt.Case (arg,None,Some outtype,[branch])
| _,NCic.Prod (name,_,t) ->
let outtype= NotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
[arg, Some arg_ty], NotationPt.Case (arg,None,Some outtype,[branch])
| _,NCic.Prod (name,_,t) ->
(`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
;;
(`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection)
;;
-let mk_projections (_,_,_,_,obj) =
+let mk_projections status (_,_,_,_,obj) =
match obj with
NCic.Inductive
(true,leftno,[_,tyname,_,[_,consname,consty]],(_,`Record fields))
->
match obj with
NCic.Inductive
(true,leftno,[_,tyname,_,[_,consname,consty]],(_,`Record fields))
->