aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-09 15:06:44 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-09-09 15:06:44 +0000
commita580a7a07da8651887c6fb386bd9af55bbe673a2 (patch)
tree4233682720571f3fa09fba77bb31e446dc6203e1 /pretyping
parent51cd60453da3f1fe136904404046098d9c4f1cc3 (diff)
Ajout construction If primitive dans constr_expr et rawconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml20
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/indrec.ml16
-rw-r--r--pretyping/indrec.mli2
-rw-r--r--pretyping/pattern.ml3
-rw-r--r--pretyping/pretyping.ml169
-rw-r--r--pretyping/rawterm.ml32
-rw-r--r--pretyping/rawterm.mli3
8 files changed, 136 insertions, 111 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e2aa74cba..a79c2a523 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -130,10 +130,11 @@ let count_rec_arg j =
* [a_bar:A'_bar](lift k pred)
* where A'_bar = A_bar[p_bar <- globargs] *)
-let build_notdep_pred env sigma indf pred =
+let build_dep_pred env sigma indf pred =
let arsign,_ = get_arity env indf in
- let nar = List.length arsign in
- it_mkLambda_or_LetIn_name env (lift nar pred) arsign
+ let psign = (Anonymous,None,build_dependent_inductive env indf)::arsign in
+ let nar = List.length psign in
+ it_mkLambda_or_LetIn_name env (lift nar pred) psign
type ml_case_error =
| MlCaseAbsurd
@@ -157,10 +158,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
else
raise (NotInferable MlCaseDependent)
in
- if realargs = [] then
- pred
- else (* we try with [_:T1]..[_:Tn](lift n pred) *)
- build_notdep_pred env sigma indf pred
+ build_dep_pred env sigma indf pred
(************************************************************************)
(* Pattern-matching compilation (Cases) *)
@@ -597,9 +595,11 @@ let occur_rawconstr id =
or (List.exists occur_pattern pl)
| ROrderedCase (loc,b,tyopt,tm,bv,_) ->
(occur_option tyopt) or (occur tm) or (array_exists occur bv)
- | RLetTuple (loc,nal,(na,tyopt),b,c) ->
- (na <> Name id & occur_option tyopt)
+ | RLetTuple (loc,nal,rtntyp,b,c) ->
+ occur_return_type rtntyp id
or (occur b) or (not (List.mem (Name id) nal) & (occur c))
+ | RIf (loc,c,rtntyp,b1,b2) ->
+ occur_return_type rtntyp id or (occur c) or (occur b1) or (occur b2)
| RRec (loc,fk,idl,tyl,bv) ->
(array_exists occur tyl) or
(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
@@ -610,6 +610,8 @@ let occur_rawconstr id =
and occur_option = function None -> false | Some p -> occur p
+ and occur_return_type (na,tyopt) id = na <> Name id & occur_option tyopt
+
in occur
let occur_in_rhs na rhs =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 49034b1b1..00895a1f6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -276,6 +276,8 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
| _ -> (RApp (dummy_loc,p,[a]))) in
let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in
RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d)
+ else if not !Options.v7 && tag = IfStyle && aliastyp = None then
+ RIf (dummy_loc,tomatch,(alias,newpred),bl.(0),bl.(1))
else
let rec remove_type avoid args c =
match c,args with
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 78c23ae61..bf7e13158 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -464,29 +464,25 @@ let build_indrec env sigma ind =
(**********************************************************************)
(* To handle old Case/Match syntax in Pretyping *)
-(***********************************)
+(*****************************************)
(* To interpret Case and Match operators *)
+(* Expects a dependent predicate *)
-let type_rec_branches recursive env sigma indt pj c =
+let type_rec_branches recursive env sigma indt p c =
let IndType (indf,realargs) = indt in
- let p = pj.uj_val in
let (ind,params) = dest_ind_family indf in
let (mib,mip) = lookup_mind_specif env ind in
let recargs = mip.mind_recargs in
let tyi = snd ind in
- let is_rec = recursive && mis_is_recursive_subset [tyi] recargs in
- let dep = is_dependent_elimination env pj.uj_type indf in
- let init_depPvec i = if i = tyi then Some(dep,p) else None in
+ let init_depPvec i = if i = tyi then Some(true,p) else None in
let depPvec = Array.init mib.mind_ntypes init_depPvec in
let vargs = Array.of_list params in
let constructors = get_constructors env indf in
let lft =
array_map2
- (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi)
+ (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
constructors (dest_subterms recargs) in
- (lft,
- if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c]))
- else Reduction.beta_appvect p (Array.of_list realargs))
+ (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
(* Non recursive case. Pb: does not deal with unification
let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
(p,ra)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 65fefb83f..38d07d1d9 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -42,7 +42,7 @@ val build_mutual_indrec :
(* These are for old Case/Match typing *)
val type_rec_branches : bool -> env -> evar_map -> inductive_type
- -> unsafe_judgment -> constr -> constr array * constr
+ -> constr -> constr -> constr array * constr
val make_rec_branch_arg :
env -> evar_map ->
int * ('b * constr) option array * int ->
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index d3479a846..f453e911e 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -241,6 +241,9 @@ let rec pat_of_raw metas vars = function
PCase ((None,st),option_app (pat_of_raw metas vars) po,
pat_of_raw metas vars c,
Array.map (pat_of_raw metas vars) br)
+ | RIf (_,c,(_,None),b1,b2) ->
+ PCase ((None,IfStyle),None, pat_of_raw metas vars c,
+ [|pat_of_raw metas vars b1; pat_of_raw metas vars b2|])
| RCases (loc,(po,_),[c,_],brs) ->
let sp =
match brs with
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ffbca83ea..0dbcaef44 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -349,7 +349,9 @@ let rec pretype tycon env isevars lvar = function
let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
(List.rev nal) cs.cs_args in
let env_f = push_rels fsign env in
+ (* Make dependencies from arity signature impossible *)
let arsgn,_ = get_arity env indf in
+ let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
let psign = (na,None,build_dependent_inductive env indf)::arsgn in
let nar = List.length arsgn in
(match po with
@@ -410,7 +412,7 @@ let rec pretype tycon env isevars lvar = function
let pj = if dep then pj else make_dep_of_undep env indt pj in
let (bty,rsty) =
Indrec.type_rec_branches
- false env (evars_of isevars) indt pj cj.uj_val
+ false env (evars_of isevars) indt pj.uj_val cj.uj_val
in
if Array.length bty <> 1 then
error_number_branches_loc
@@ -443,6 +445,10 @@ let rec pretype tycon env isevars lvar = function
(* may be Type while Prop or Set would be expected *)
match tycon with
| Some pred ->
+ let arsgn = make_arity_signature env true indf in
+ let pred =
+ it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+ arsgn in
false,
Retyping.get_judgment_of env (evars_of isevars) pred
| None ->
@@ -461,19 +467,21 @@ let rec pretype tycon env isevars lvar = function
let pty =
Retyping.get_type_of env (evars_of isevars) pred in
let pj = { uj_val = pred; uj_type = pty } in
+(*
let _ =
option_app (the_conv_x_leq env isevars pred) tycon
in
+*)
true, pj
with Cases.NotInferable _ ->
use_constraint ()
in
let pj = j_nf_evar (evars_of isevars) pj in
- let pj = make_dep_of_undep env indt pj in
let (bty,rsty) =
Indrec.type_rec_branches
- false env (evars_of isevars) indt pj cj.uj_val
+ false env (evars_of isevars) indt pj.uj_val cj.uj_val
in
+ let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
let fj =
if ok then fj
else pretype (mk_tycon bty.(0)) env isevars lvar f
@@ -588,6 +596,80 @@ let rec pretype tycon env isevars lvar = function
(* End building the v8 syntax *)
j
+ | RIf (loc,c,(na,po),b1,b2) ->
+ let cj = pretype empty_tycon env isevars lvar c in
+ let (IndType (indf,realargs) as indt) =
+ try find_rectype env (evars_of isevars) cj.uj_type
+ with Not_found ->
+ let cloc = loc_of_rawconstr c in
+ error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+ (* Make dependencies from arity signature impossible *)
+ let arsgn,_ = get_arity env indf in
+ let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+ let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+ let nar = List.length arsgn in
+ let p =
+ match po with
+ | Some p ->
+ let env_p = push_rels psign env in
+ let pj = pretype_type empty_valcon env_p isevars lvar p in
+ let ccl = nf_evar (evars_of isevars) pj.utj_val in
+ it_mkLambda_or_LetIn ccl psign
+ | None ->
+ (* get type information from type of branches *)
+ let expbr = Cases.branch_scheme env isevars false indf in
+ try
+ let fj = pretype (mk_tycon expbr.(0)) env isevars lvar b1 in
+ let pred =
+ Cases.pred_case_ml
+ env (evars_of isevars) false indt (0,fj.uj_type) in
+ if has_undefined_isevars isevars pred then
+ raise Not_found
+ else
+(*
+ let _ = option_app (the_conv_x_leq env isevars pred) tycon in
+*)
+ pred
+ with Cases.NotInferable _ | Not_found ->
+ try
+ let fj = pretype (mk_tycon expbr.(1)) env isevars lvar b2 in
+ let pred =
+ Cases.pred_case_ml
+ env (evars_of isevars) false indt (1,fj.uj_type) in
+ if has_undefined_isevars isevars pred then
+ raise Not_found
+ else
+(*
+ let _ = option_app (the_conv_x_leq env isevars pred) tycon in
+*)
+ pred
+ with Cases.NotInferable _ | Not_found ->
+ (* get type information from constraint *)
+ (* warning: if the constraint comes from an evar type, it *)
+ (* may be Type while Prop or Set would be expected *)
+ match tycon with
+ | Some pred ->
+ let arsgn = make_arity_signature env true indf in
+ it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) arsgn
+ | None ->
+ let sigma = evars_of isevars in
+ error_cant_find_case_type_loc loc env sigma cj.uj_val in
+ let (bty,rsty) =
+ Indrec.type_rec_branches false
+ env (evars_of isevars) indt p cj.uj_val in
+ let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
+ if Array.length bty <> 2 then
+ user_err_loc (loc,"",
+ str "If is only for inductive types with two constructors");
+ let bj1 = pretype (mk_tycon bty.(0)) env isevars lvar b1 in
+ let bj2 = pretype (mk_tycon bty.(1)) env isevars lvar b2 in
+ let v =
+ let mis,_ = dest_ind_family indf in
+ let ci = make_default_case_info env IfStyle mis in
+ mkCase (ci, p, cj.uj_val, [|bj1.uj_val;bj2.uj_val|])
+ in
+ { uj_val = v; uj_type = rsty }
+
| ROrderedCase (loc,st,po,c,lf,x) ->
let isrec = (st = MatchStyle) in
let cj = pretype empty_tycon env isevars lvar c in
@@ -615,7 +697,11 @@ let rec pretype tycon env isevars lvar = function
(* may be Type while Prop or Set would be expected *)
match tycon with
| Some pred ->
- (false,
+ let arsgn = make_arity_signature env true indf in
+ let pred =
+ it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred)
+ arsgn in
+ (true,
Retyping.get_judgment_of env (evars_of isevars) pred)
| None ->
let sigma = evars_of isevars in
@@ -626,15 +712,18 @@ let rec pretype tycon env isevars lvar = function
let fj =
pretype (mk_tycon expti) env isevars lvar lf.(i) in
let pred =
- Cases.pred_case_ml
+ Cases.pred_case_ml (* eta-expanse *)
env (evars_of isevars) isrec indt (i,fj.uj_type) in
if has_undefined_isevars isevars pred then findtype (i+1)
else
let pty =
Retyping.get_type_of env (evars_of isevars) pred in
let pj = { uj_val = pred; uj_type = pty } in
+(*
let _ = option_app (the_conv_x_leq env isevars pred) tycon
- in (false,pj)
+ in
+*)
+ (true,pj)
with Cases.NotInferable _ -> findtype (i+1) in
findtype 0
in
@@ -642,7 +731,8 @@ let rec pretype tycon env isevars lvar = function
let pj = if dep then pj else make_dep_of_undep env indt pj in
let (bty,rsty) =
Indrec.type_rec_branches
- isrec env (evars_of isevars) indt pj cj.uj_val in
+ isrec env (evars_of isevars) indt pj.uj_val cj.uj_val in
+ let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
if Array.length bty <> Array.length lf then
error_number_branches_loc loc env (evars_of isevars)
cj (Array.length bty)
@@ -676,67 +766,6 @@ let rec pretype tycon env isevars lvar = function
Some (Detyping.detype env
(ids_of_context env) (names_of_rel_context env)
(nf_evar (evars_of isevars) v))
- (*
- let sigma = evars_of isevars in
- let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
- let depFvec = Array.init mib.mind_ntypes init_depFvec in
- (* build now the fixpoint *)
- let lnames,_ = get_arity env indf in
- let nar = List.length lnames in
- let nparams = mip.mind_nparams in
- let constrs = get_constructors env (lift_inductive_family (nar+2) indf) in
- let branches =
- array_map3
- (fun f t reca ->
- whd_beta
- (Indrec.make_rec_branch_arg env sigma
- (nparams,depFvec,nar+1)
- f t reca))
- (Array.map (lift (nar+2)) lfv) constrs (dest_subterms recargs)
- in
- let ci = make_default_case_info env RegularStyle ind in
- let deffix =
- it_mkLambda_or_LetIn_name env
- (lambda_create env
- (applist (mI,List.append (List.map (lift (nar+1)) params)
- (extended_rel_list 0 lnames)),
- mkCase (ci, lift (nar+2) pj.uj_val, mkRel 1, branches)))
- (lift_rel_context 1 lnames)
- in
- if noccurn 1 deffix then
- Some
- (Detyping.detype env [] (names_of_rel_context env)
- (whd_beta (applist (pop deffix,realargs@[cj.uj_val]))))
- else
- let ind = applist (mI,(List.append
- (List.map (lift nar) params)
- (extended_rel_list 0 lnames))) in
- let typPfix =
- let rec aux = function
- | (na,Some b,t)::l ->
- | (na,None,t)::l -> RProd (dummy_loc,na,
- | [] ->
- it_mkProd_or_LetIn_name env
- (prod_create env
- (ind,
- (if dep then
- let ext_lnames = (Anonymous,None,ind)::lnames in
- let args = extended_rel_list 0 ext_lnames in
- whd_beta (applist (lift (nar+1) p, args))
- else
- let args = extended_rel_list 1 lnames in
- whd_beta (applist (lift (nar+1) p, args)))))
- lnames in
- let fix =
- RRec (dummy_loc,RFix ([|nar|],0),
- ([|(id_of_string "F")|],[|typPfix|],[|deffix|])) in
- RApp (dummy_loc,fix,realargs@[c])
- (msgerrnl (str "Warning: could't translate Match"); None)
-*)
- else if st = IfStyle & po = None then
- (* Translate into a "if ... then ... else" *)
- (* TODO: translate into a "if" even if po is dependent *)
- None
else
(* Translate into a "match ... with" *)
let rtntypopt, indnalopt = match po with
@@ -762,10 +791,10 @@ let rec pretype tycon env isevars lvar = function
else [Anonymous],p,[] in
let args = List.map (fun _ -> Anonymous) params @ nal in
(Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in
- if st = IfStyle & po = None then
+ if st = IfStyle & snd indnalopt = None then
(* Translate into a "if ... then ... else" *)
(* TODO: translate into a "if" even if po is dependent *)
- None
+ Some (RIf (loc,c,(fst indnalopt,rtntypopt),lf.(0),lf.(1)))
else
let detype_eqn constr construct_nargs branch =
let name_cons = function
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index bdb6914c2..a1eb589ff 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -75,6 +75,7 @@ type rawconstr =
rawconstr array * rawconstr option ref
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
+ | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
@@ -97,24 +98,6 @@ let cases_predicate_names tml =
- boolean in POldCase means it is recursive
i*)
-let loc = function
- | RVar (loc,_) -> loc
- | RApp (loc,_,_) -> loc
- | RLambda (loc,_,_,_) -> loc
- | RProd (loc,_,_,_) -> loc
- | RLetIn (loc,_,_,_) -> loc
- | RCases (loc,_,_,_) -> loc
- | ROrderedCase (loc,_,_,_,_,_) -> loc
- | RLetTuple (loc,_,_,_,_) -> loc
- | RRec (loc,_,_,_,_) -> loc
- | RCast (loc,_,_) -> loc
- | RSort (loc,_) -> loc
- | RHole (loc,_) -> loc
- | RRef (loc,_) -> loc
- | REvar (loc,_) -> loc
- | RPatVar (loc,_) -> loc
- | RDynamic (loc,_) -> loc
-
let map_rawconstr f = function
| RVar (loc,id) -> RVar (loc,id)
| RApp (loc,g,args) -> RApp (loc,f g, List.map f args)
@@ -129,6 +112,8 @@ let map_rawconstr f = function
ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv,ref (option_app f !x))
| RLetTuple (loc,nal,(na,po),b,c) ->
RLetTuple (loc,nal,(na,option_app f po),f b,f c)
+ | RIf (loc,c,(na,po),b1,b2) ->
+ RIf (loc,f c,(na,option_app f po),f b1,f b2)
| RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
| RCast (loc,c,t) -> RCast (loc,f c,f t)
| (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
@@ -248,8 +233,16 @@ let rec subst_raw subst raw =
and b' = subst_raw subst b
and c' = subst_raw subst c in
if po' == po && b' == b && c' == c then raw else
- RLetTuple (loc,nal,(na,po),b,c)
+ RLetTuple (loc,nal,(na,po'),b',c')
+ | RIf (loc,c,(na,po),b1,b2) ->
+ let po' = option_smartmap (subst_raw subst) po
+ and b1' = subst_raw subst b1
+ and b2' = subst_raw subst b2
+ and c' = subst_raw subst c in
+ if c' == c & po' == po && b1' == b1 && b2' == b2 then raw else
+ RIf (loc,c',(na,po'),b1',b2')
+
| RRec (loc,fix,ida,ra1,ra2) ->
let ra1' = array_smartmap (subst_raw subst) ra1
and ra2' = array_smartmap (subst_raw subst) ra2 in
@@ -284,6 +277,7 @@ let loc_of_rawconstr = function
| RCases (loc,_,_,_) -> loc
| ROrderedCase (loc,_,_,_,_,_) -> loc
| RLetTuple (loc,_,_,_,_) -> loc
+ | RIf (loc,_,_,_,_) -> loc
| RRec (loc,_,_,_,_) -> loc
| RSort (loc,_) -> loc
| RHole (loc,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 27bb76b69..2718cf9bb 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -72,6 +72,7 @@ type rawconstr =
rawconstr array * rawconstr option ref
| RLetTuple of loc * name list * (name * rawconstr option) *
rawconstr * rawconstr
+ | RIf of loc * rawconstr * (name * rawconstr option) * rawconstr * rawconstr
| RRec of loc * fix_kind * identifier array *
rawconstr array * rawconstr array
| RSort of loc * rawsort
@@ -94,8 +95,6 @@ val cases_predicate_names :
- option in PHole tell if the "?" was apparent or has been implicitely added
i*)
-val loc : rawconstr -> loc
-
val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
(*