diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 70 |
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 |