summaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /interp/constrintern.ml
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml70
1 files changed, 41 insertions, 29 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b161d001..1dd735ad 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -166,6 +166,8 @@ let error_inductive_parameter_not_implicit loc =
(* Pre-computing the implicit arguments and arguments scopes needed *)
(* for interpretation *)
+let parsing_explicit = ref false
+
let empty_internalization_env = Idmap.empty
let compute_explicitable_implicit imps = function
@@ -408,12 +410,12 @@ let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,b
| LocalRawAssum(nal,bk,ty) ->
(match bk with
| Default k ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
- let ty = locate_if_isevar loc na (intern_type env ty) in
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
List.fold_left
- (fun (env,bl) na ->
- (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+ (fun (env,bl) (loc,na as locna) ->
+ (push_name_env lvar impls env locna,
+ (na,k,None,locate_if_isevar loc na ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -452,12 +454,12 @@ let iterate_binder intern lvar (env,bl) = function
let intern_type env = intern (set_type_scope env) in
(match bk with
| Default k ->
- let (loc,na) = List.hd nal in
- (* TODO: fail if several names with different implicit types *)
let ty = intern_type env ty in
- let ty = locate_if_isevar loc na ty in
+ let impls = impls_type_list ty in
List.fold_left
- (fun (env,bl) na -> (push_name_env lvar (impls_type_list ty) env na,(snd na,k,None,ty)::bl))
+ (fun (env,bl) (loc,na as locna) ->
+ (push_name_env lvar impls env locna,
+ (na,k,None,locate_if_isevar loc na ty)::bl))
(env,bl) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in
@@ -731,8 +733,9 @@ let apply_scope_env env = function
| [] -> {env with tmp_scope = None}, []
| sc::scl -> {env with tmp_scope = sc}, scl
-let rec simple_adjust_scopes n = function
- | [] -> if n=0 then [] else None :: simple_adjust_scopes (n-1) []
+let rec simple_adjust_scopes n scopes =
+ if n=0 then [] else match scopes with
+ | [] -> None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
let find_remaining_constructor_scopes pl1 pl2 (ind,j as cstr) =
@@ -809,9 +812,6 @@ let message_redundant_alias (id1,id2) =
(* Expanding notations *)
-let error_invalid_pattern_notation loc =
- user_err_loc (loc,"",str "Invalid notation for pattern.")
-
let chop_aconstr_constructor loc (ind,k) args =
if List.length args = 0 then (* Tolerance for a @id notation *) args else
begin
@@ -1293,7 +1293,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
find_appl_head_data c, args
| x -> (intern env f,[],[],[]), args in
let args =
- intern_impargs c env impargs args_scopes (merge_impargs l args) in
+ intern_impargs c env impargs args_scopes (merge_impargs l args) in
check_projection isproj (List.length args) c;
(match c with
(* Now compact "(f args') args" *)
@@ -1417,13 +1417,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
(tm',(snd na,typ)), na::ids
and iterate_prod loc2 env bk ty body nal =
- let rec default env bk = function
- | (loc1,na as locna)::nal ->
- if nal <> [] then check_capture loc1 ty na;
- let ty = locate_if_isevar loc1 na (intern_type env ty) in
- let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
- GProd (join_loc loc1 loc2, na, bk, ty, body)
- | [] -> intern_type env body
+ let default env bk = function
+ | (loc1,na)::nal' as nal ->
+ if nal' <> [] then check_capture loc1 ty na;
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
+ let env = List.fold_left (push_name_env lvar impls) env nal in
+ List.fold_right (fun (loc,na) c ->
+ GProd (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+ nal (intern_type env body)
+ | [] -> assert false
in
match bk with
| Default b -> default env b nal
@@ -1433,13 +1436,16 @@ let internalize sigma globalenv env allow_patvar lvar c =
it_mkGProd ibind body
and iterate_lam loc2 env bk ty body nal =
- let rec default env bk = function
- | (loc1,na as locna)::nal ->
- if nal <> [] then check_capture loc1 ty na;
- let ty = locate_if_isevar loc1 na (intern_type env ty) in
- let body = default (push_name_env lvar (impls_type_list ty) env locna) bk nal in
- GLambda (join_loc loc1 loc2, na, bk, ty, body)
- | [] -> intern env body
+ let default env bk = function
+ | (loc1,na)::nal' as nal ->
+ if nal' <> [] then check_capture loc1 ty na;
+ let ty = intern_type env ty in
+ let impls = impls_type_list ty in
+ let env = List.fold_left (push_name_env lvar impls) env nal in
+ List.fold_right (fun (loc,na) c ->
+ GLambda (join_loc loc loc2, na, bk, locate_if_isevar loc na ty, c))
+ nal (intern env body)
+ | [] -> assert false
in match bk with
| Default b -> default env b nal
| Generalized (b, b', t) ->
@@ -1450,6 +1456,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
and intern_impargs c env l subscopes args =
let l = select_impargs_size (List.length args) l in
let eargs, rargs = extract_explicit_arg l args in
+ if !parsing_explicit then
+ if eargs <> [] then
+ error "Arguments given by name or position not supported in explicit mode."
+ else
+ intern_args env subscopes rargs
+ else
let rec aux n impl subscopes eargs rargs =
let (enva,subscopes') = apply_scope_env env subscopes in
match (impl,rargs) with