diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 96 |
1 files changed, 51 insertions, 45 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3675441353..57091ca898 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -175,6 +175,10 @@ let add_patt_for_params ind l = if !Flags.in_debugger then l else Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l +let add_cpatt_for_params ind l = + if !Flags.in_debugger then l else + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l + let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in let impl_data = extract_impargs_data impl_st in @@ -266,7 +270,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args = let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l) + if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in @@ -286,7 +290,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) + CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -299,7 +303,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol_pattern scopes vars pat + extern_notation_pattern scopes vars pat (uninterp_cases_pattern_notations pat) with No_match -> match pat with @@ -327,15 +331,15 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - if !Topconstr.oldfashion_patterns then + if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, c, [], args) - else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) + then CPatCstr (loc, c, None, args) + else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - |Some true_args -> CPatCstr (loc, c, [], true_args) - |None -> CPatCstr (loc, c, full_args, []) + |Some true_args -> CPatCstr (loc, c, None, true_args) + |None -> CPatCstr (loc, c, Some full_args, []) in insert_pat_alias loc p na and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -358,7 +362,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2 + let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -374,7 +378,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns then l2 + let l2' = if !Topconstr.asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args @@ -382,7 +386,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) in assert (List.is_empty substlist); mkPat loc qid (List.rev_append l1 l2') -and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function +and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try @@ -395,9 +399,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function | PatVar (loc,Anonymous) -> CPatAtom (loc, None) | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id))) with - No_match -> extern_symbol_pattern allscopes vars t rules + No_match -> extern_notation_pattern allscopes vars t rules -let rec extern_symbol_ind_pattern allscopes vars ind args = function +let rec extern_notation_ind_pattern allscopes vars ind args = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> try @@ -405,7 +409,7 @@ let rec extern_symbol_ind_pattern allscopes vars ind args = function apply_notation_to_pattern Loc.ghost (IndRef ind) (match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule with - No_match -> extern_symbol_ind_pattern allscopes vars ind args rules + No_match -> extern_notation_ind_pattern allscopes vars ind args rules let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = (* pboutill: There are letins in pat which is incompatible with notations and @@ -413,7 +417,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (Loc.ghost, c, add_patt_for_params ind args, []) + CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -425,14 +429,14 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = with No_match -> try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol_ind_pattern scopes vars ind args + extern_notation_ind_pattern scopes vars ind args (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args) - |None -> CPatCstr (Loc.ghost, c, args, []) + |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args) + |None -> CPatCstr (Loc.ghost, c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p @@ -477,15 +481,15 @@ let explicitize loc inctx impl (cf,f) args = (!print_implicits && !print_implicits_explicit_args) || (is_needed_for_correct_partial_application tail imp) || (!print_implicits_defensive && - is_significant_implicit a && - not (is_inferable_implicit inctx n imp)) + not (is_inferable_implicit inctx n imp) && + is_significant_implicit (Lazy.force a)) in if visible then - (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail + (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail else tail - | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl) - | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*) + | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) + | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*) | [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp -> (* The non-explicit application cannot be parsed back with the same type *) raise Expl @@ -512,7 +516,7 @@ let explicitize loc inctx impl (cf,f) args = with Expl -> let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in let ip = if !print_projections then ip else None in - CAppExpl (loc, (ip, f', us), args) + CAppExpl (loc, (ip, f', us), List.map Lazy.force args) let is_start_implicit = function | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp @@ -534,19 +538,21 @@ let extern_app loc inctx impl (cf,f) us args = (!print_implicits && not !print_implicits_explicit_args)) && List.exists is_status_implicit impl) then + let args = List.map Lazy.force args in CAppExpl (loc, (is_projection (List.length args) cf,f,us), args) else explicitize loc inctx impl (cf,CRef (f,us)) args -let rec extern_args extern scopes env args subscopes = - match args with - | [] -> [] - | a::args -> - let argscopes, subscopes = match subscopes with - | [] -> (None,scopes), [] - | scopt::subscopes -> (scopt,scopes), subscopes in - extern argscopes env a :: extern_args extern scopes env args subscopes +let rec fill_arg_scopes args subscopes scopes = match args, subscopes with +| [], _ -> [] +| a :: args, scopt :: subscopes -> + (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes +| a :: args, [] -> + (a, (None, scopes)) :: fill_arg_scopes args [] scopes +let extern_args extern env args = + let map (arg, argscopes) = lazy (extern argscopes env arg) in + List.map map args let match_coercion_app = function | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args) @@ -622,7 +628,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_symbol scopes vars r'' (uninterp_notations r'') + extern_notation scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | GRef (loc,ref,us) -> extern_global loc (select_stronger_impargs (implicits_of_global ref)) @@ -643,8 +649,7 @@ let rec extern inctx scopes vars r = (match f with | GRef (rloc,ref,us) -> let subscopes = find_arguments_scope ref in - let args = - extern_args (extern true) (snd scopes) vars args subscopes in + let args = fill_arg_scopes args subscopes (snd scopes) in begin try if !Flags.raw_print then raise Exit; @@ -679,12 +684,14 @@ let rec extern inctx scopes vars r = match args with | [] -> raise No_match (* we give up since the constructor is not complete *) - | head :: tail -> ip q locs' tail - ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) + | (arg, scopes) :: tail -> + let head = extern true scopes vars arg in + ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in CRecord (loc, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> + let args = extern_args (extern true) vars args in extern_app loc inctx (select_stronger_impargs (implicits_of_global ref)) (Some ref,extern_reference rloc vars ref) (extern_universes us) args @@ -692,7 +699,7 @@ let rec extern inctx scopes vars r = | _ -> explicitize loc inctx [] (None,sub_extern false scopes vars f) - (List.map (sub_extern true scopes vars) args)) + (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) | GLetIn (loc,na,t,c) -> CLetIn (loc,(loc,na),sub_extern false scopes vars t, @@ -730,9 +737,7 @@ let rec extern inctx scopes vars r = na', Option.map (fun (loc,ind,nal) -> let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in - let fullargs = - if !Flags.in_debugger then args else - Notation_ops.add_patterns_for_params ind args in + let fullargs = add_cpatt_for_params ind args in extern_ind_pattern_in_scope scopes vars ind fullargs ) x)) tml @@ -793,7 +798,7 @@ let rec extern inctx scopes vars r = Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = - extern true (Some Notation.type_scope,scopes) + extern true (Notation.current_type_scope_name (),scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) @@ -842,7 +847,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], extern inctx scopes vars c) -and extern_symbol (tmp_scope,scopes as allscopes) vars t = function +and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> let loc = Glob_ops.loc_of_glob_constr t in @@ -914,10 +919,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function if List.is_empty l then a else CApp (loc,(None,a),l) in if List.is_empty args then e else - let args = extern_args (extern true) scopes vars args argsscopes in + let args = fill_arg_scopes args argsscopes scopes in + let args = extern_args (extern true) vars args in explicitize loc false argsimpls (None,e) args with - No_match -> extern_symbol allscopes vars t rules + No_match -> extern_notation allscopes vars t rules and extern_recursion_order scopes vars = function GStructRec -> CStructRec |