diff options
Diffstat (limited to 'pretyping/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 236 |
1 files changed, 118 insertions, 118 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 5dd4772bcc..862865bd90 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -133,8 +133,8 @@ let add_name na b t (nenv, env) = add_name na nenv, push_rel (match b with | None -> LocalAssum (make_annot na r,t) | Some b -> LocalDef (make_annot na r,b,t) - ) - env + ) + env let add_name_opt na b t (nenv, env) = match t with @@ -199,7 +199,7 @@ module PrintingCasesIf = let member_message s b = str "Cases on elements of " ++ s ++ str - (if b then " are printed using a `if' form" + (if b then " are printed using a `if' form" else " are not printed using a `if' form") end) @@ -212,7 +212,7 @@ module PrintingCasesLet = let member_message s b = str "Cases on elements of " ++ s ++ str - (if b then " are printed using a `let' form" + (if b then " are printed using a `let' form" else " are not printed using a `let' form") end) @@ -227,11 +227,11 @@ let wildcard_value = ref true let force_wildcard () = !wildcard_value let () = declare_bool_option - { optdepr = false; - optname = "forced wildcard"; - optkey = ["Printing";"Wildcard"]; - optread = force_wildcard; - optwrite = (:=) wildcard_value } + { optdepr = false; + optname = "forced wildcard"; + optkey = ["Printing";"Wildcard"]; + optread = force_wildcard; + optwrite = (:=) wildcard_value } let fast_name_generation = ref false @@ -247,33 +247,33 @@ let synth_type_value = ref true let synthetize_type () = !synth_type_value let () = declare_bool_option - { optdepr = false; - optname = "pattern matching return type synthesizability"; - optkey = ["Printing";"Synth"]; - optread = synthetize_type; - optwrite = (:=) synth_type_value } + { optdepr = false; + optname = "pattern matching return type synthesizability"; + optkey = ["Printing";"Synth"]; + optread = synthetize_type; + optwrite = (:=) synth_type_value } let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value let () = declare_bool_option - { optdepr = false; - optname = "pattern-matching reversibility"; - optkey = ["Printing";"Matching"]; - optread = reverse_matching; - optwrite = (:=) reverse_matching_value } + { optdepr = false; + optname = "pattern-matching reversibility"; + optkey = ["Printing";"Matching"]; + optread = reverse_matching; + optwrite = (:=) reverse_matching_value } let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value let () = declare_bool_option - { optdepr = false; - optname = "printing of primitive projection parameters"; - optkey = ["Printing";"Primitive";"Projection";"Parameters"]; - optread = print_primproj_params; - optwrite = (:=) print_primproj_params_value } + { optdepr = false; + optname = "printing of primitive projection parameters"; + optkey = ["Printing";"Primitive";"Projection";"Parameters"]; + optread = print_primproj_params; + optwrite = (:=) print_primproj_params_value } + - (* Auxiliary function for MutCase printing *) (* [computable] tries to tell if the predicate typing the result is inferable*) @@ -304,11 +304,11 @@ let lookup_name_as_displayed env sigma t s = | Prod (name,_,c') -> (match compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | LetIn (name,_,_,c') -> (match Namegen.compute_displayed_name_in sigma RenamingForGoal avoid name.binder_name c' with | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c' - | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) + | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c')) | Cast (c,_,_) -> lookup avoid n c | _ -> None in lookup (Environ.ids_of_named_context_val (Environ.named_context_val env)) 1 t @@ -319,23 +319,23 @@ let lookup_index_as_renamed env sigma t n = (match Namegen.compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> - if Int.equal n 0 then - Some (d-1) - else if Int.equal n 1 then - Some d - else - lookup (n-1) (d+1) c') + if Int.equal n 0 then + Some (d-1) + else if Int.equal n 1 then + Some d + else + lookup (n-1) (d+1) c') | LetIn (name,_,_,c') -> (match Namegen.compute_displayed_name_in sigma RenamingForGoal Id.Set.empty name.binder_name c' with | (Name _,_) -> lookup n (d+1) c' | (Anonymous,_) -> - if Int.equal n 0 then - Some (d-1) - else if Int.equal n 1 then - Some d - else - lookup (n-1) (d+1) c' - ) + if Int.equal n 0 then + Some (d-1) + else if Int.equal n 1 then + Some d + else + lookup (n-1) (d+1) c' + ) | Cast (c,_,_) -> lookup n d c | _ -> if Int.equal n 0 then Some (d-1) else None in lookup n 1 t @@ -444,10 +444,10 @@ let rec decomp_branch tags nal flags (avoid,env as e) sigma c = | Lambda (na,t,c),false -> na.binder_name,c,true,None,Some t | LetIn (na,b,t,c),true -> na.binder_name,c,false,Some b,Some t - | _, false -> - Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), + | _, false -> + Name default_dependent_ident,(applist (lift 1 c, [mkRel 1])), false,None,None - | _, true -> + | _, true -> Anonymous,lift 1 c,false,None,None in let na',avoid' = compute_name sigma ~let_in ~pattern:true flags avoid env na c in @@ -468,14 +468,14 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with | Case (ci,p,c,cl) when eq_constr sigma c (mkRel (List.index Name.equal na (fst (snd e)))) && not (Int.equal (Array.length cl) 0) - && (* don't contract if p dependent *) - computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> - let clauses = build_tree na isgoal e sigma ci cl in - List.flatten + && (* don't contract if p dependent *) + computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> + let clauses = build_tree na isgoal e sigma ci cl in + List.flatten (List.map (fun (ids,pat,rhs) -> - let lines = align_tree nal isgoal rhs sigma in + let lines = align_tree nal isgoal rhs sigma in List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) - clauses) + clauses) | _ -> let na = update_name sigma na rhs in let pat = DAst.make @@ PatVar na in @@ -518,15 +518,15 @@ let it_destRLambda_or_LetIn_names l c = | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c | _, false::l -> (* eta-expansion *) - let next l = - let x = next_ident_away default_dependent_ident l in - (* Not efficient but unusual and no function to get free glob_vars *) + let next l = + let x = next_ident_away default_dependent_ident l in + (* Not efficient but unusual and no function to get free glob_vars *) (* if occur_glob_constr x c then next (x::l) else x in *) - x - in - let x = next (free_glob_vars c) in - let a = DAst.make @@ GVar x in - aux l (Name x :: nal) + x + in + let x = next (free_glob_vars c) in + let a = DAst.make @@ GVar x in + aux l (Name x :: nal) (match DAst.get c with | GApp (p,l) -> DAst.make ?loc:c.CAst.loc @@ GApp (p,l@[a]) | _ -> DAst.make @@ GApp (c,[a])) @@ -557,13 +557,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = if !Flags.raw_print then RegularStyle else if st == LetPatternStyle then - st + st else if PrintingLet.active indsp then - LetStyle + LetStyle else if PrintingIf.active indsp then - IfStyle + IfStyle else - st + st with Not_found -> st in match tag, aliastyp with @@ -574,13 +574,13 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = | IfStyle, None -> let bl' = Array.map detype bl in let nondepbrs = - Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in + Array.map3 (extract_nondep_branches testdep) bl bl' constagsl in if Array.for_all ((!=) None) nondepbrs then - GIf (tomatch,(alias,pred), + GIf (tomatch,(alias,pred), Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else - let eqnl = detype_eqns constructs constagsl bl in - GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) + let eqnl = detype_eqns constructs constagsl bl in + GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> let eqnl = detype_eqns constructs constagsl bl in GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl) @@ -712,7 +712,7 @@ let detype_level sigma l = let l = hack_qualid_of_univ_level sigma l in UNamed (GType l) -let detype_instance sigma l = +let detype_instance sigma l = let l = EInstance.kind sigma l in if Univ.Instance.is_empty l then None else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l))) @@ -737,37 +737,37 @@ and detype_r d flags avoid env sigma t = let s = "_UNBOUND_REL_"^(string_of_int n) in GVar (Id.of_string s)) | Meta n -> - (* Meta in constr are not user-parsable and are mapped to Evar *) + (* Meta in constr are not user-parsable and are mapped to Evar *) if n = Constr_matching.special_meta then (* Using a dash to be unparsable *) - GEvar (Id.of_string_soft "CONTEXT-HOLE", []) + GEvar (Id.of_string_soft "CONTEXT-HOLE", []) else - GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) + GEvar (Id.of_string_soft ("M" ^ string_of_int n), []) | Var id -> (* Discriminate between section variable and non-section variable *) (try let _ = Global.lookup_named id in GRef (GlobRef.VarRef id, None) - with Not_found -> GVar id) + with Not_found -> GVar id) | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s)) | Cast (c1,REVERTcast,c2) when not !Flags.raw_print -> DAst.get (detype d flags avoid env sigma c1) | Cast (c1,k,c2) -> let d1 = detype d flags avoid env sigma c1 in - let d2 = detype d flags avoid env sigma c2 in + let d2 = detype d flags avoid env sigma c2 in let cast = match k with | VMcast -> CastVM d2 | NATIVEcast -> CastNative d2 | _ -> CastConv d2 in - GCast(d1,cast) + GCast(d1,cast) | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c | App (f,args) -> - let mkapp f' args' = - match DAst.get f' with - | GApp (f',args'') -> - GApp (f',args''@args') - | _ -> GApp (f',args') + let mkapp f' args' = + match DAst.get f' with + | GApp (f',args'') -> + GApp (f',args''@args') + | _ -> GApp (f',args') in mkapp (detype d flags avoid env sigma f) (Array.map_to_list (detype d flags avoid env sigma) args) @@ -781,12 +781,12 @@ and detype_r d flags avoid env sigma t = (args @ [detype d flags avoid env sigma c])) in if flags.flg_lax || !Flags.in_debugger || !Flags.in_toplevel then - try noparams () - with _ -> - (* lax mode, used by debug printers only *) + try noparams () + with _ -> + (* lax mode, used by debug printers only *) GApp (DAst.make @@ GRef (GlobRef.ConstRef (Projection.constant p), None), - [detype d flags avoid env sigma c]) - else + [detype d flags avoid env sigma c]) + else if print_primproj_params () then try let c = Retyping.expand_projection (snd env) sigma p c [] in @@ -800,7 +800,7 @@ and detype_r d flags avoid env sigma t = | LocalDef _ -> true | LocalAssum (id,_) -> try let n = List.index Name.equal (Name id.binder_name) (fst env) in - isRelN sigma n c + isRelN sigma n c with Not_found -> isVarId sigma id.binder_name c in let id,l = @@ -824,12 +824,12 @@ and detype_r d flags avoid env sigma t = | Construct (cstr_sp,u) -> GRef (GlobRef.ConstructRef cstr_sp, detype_instance sigma u) | Case (ci,p,c,bl) -> - let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in - detype_case comp (detype d flags avoid env sigma) - (detype_eqns d flags avoid env sigma ci comp) - (is_nondep_branch sigma) avoid - (ci.ci_ind,ci.ci_pp_info.style, - ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) + let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in + detype_case comp (detype d flags avoid env sigma) + (detype_eqns d flags avoid env sigma ci comp) + (is_nondep_branch sigma) avoid + (ci.ci_ind,ci.ci_pp_info.style, + ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) p c bl | Fix (nvn,recdef) -> detype_fix (detype d) flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix (detype d) flags avoid env sigma n recdef @@ -870,20 +870,20 @@ and detype_eqn d flags avoid env sigma constr construct_nargs branch = buildrec new_ids (pat::patlist) new_avoid new_env l b' | Cast (c,_,_), l -> (* Oui, il y a parfois des cast *) - buildrec ids patlist avoid env l c + buildrec ids patlist avoid env l c | _, true::l -> - let pat = DAst.make @@ PatVar Anonymous in + let pat = DAst.make @@ PatVar Anonymous in buildrec ids (pat::patlist) avoid env l b | _, false::l -> (* eta-expansion : n'arrivera plus lorsque tous les termes seront construits à partir de la syntaxe Cases *) (* nommage de la nouvelle variable *) - let new_b = applist (lift 1 b, [mkRel 1]) in + let new_b = applist (lift 1 b, [mkRel 1]) in let pat,new_avoid,new_env,new_ids = - make_pat Anonymous avoid env new_b None mkProp ids in - buildrec new_ids (pat::patlist) new_avoid new_env l new_b + make_pat Anonymous avoid env new_b None mkProp ids in + buildrec new_ids (pat::patlist) new_avoid new_env l new_b in buildrec Id.Set.empty [] avoid env construct_nargs branch @@ -912,13 +912,13 @@ let detype_rel_context d flags where avoid env sigma sign = let na = get_name decl in let t = get_type decl in let na',avoid' = - match where with - | None -> na,avoid - | Some c -> + match where with + | None -> na,avoid + | Some c -> compute_name sigma ~let_in:(is_local_def decl) ~pattern:false flags avoid env na c in let b = match decl with - | LocalAssum _ -> None + | LocalAssum _ -> None | LocalDef (_,b,_) -> Some b in let b' = Option.map (detype d flags avoid env sigma) b in @@ -926,7 +926,7 @@ let detype_rel_context d flags where avoid env sigma sign = (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest in aux avoid env (List.rev sign) -let detype_names isgoal avoid nenv env sigma t = +let detype_names isgoal avoid nenv env sigma t = let flags = { flg_isgoal = isgoal; flg_lax = false } in let avoid = Avoid.make ~fast:!fast_name_generation avoid in detype Now flags avoid (nenv,env) sigma t @@ -1008,8 +1008,8 @@ let rec subst_cases_pattern subst = DAst.map (function | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in - if kn' == kn && cpl' == cpl then pat else - PatCstr (((kn',i),j),cpl',n) + if kn' == kn && cpl' == cpl then pat else + PatCstr (((kn',i),j),cpl',n) ) let (f_subst_genarg, subst_genarg_hook) = Hook.make () @@ -1034,25 +1034,25 @@ let rec subst_glob_constr env subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr env subst r and rl' = List.Smart.map (subst_glob_constr env subst) rl in - if r' == r && rl' == rl then raw else - GApp(r',rl') + if r' == r && rl' == rl then raw else + GApp(r',rl') | GLambda (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in - if r1' == r1 && r2' == r2 then raw else - GLambda (n,bk,r1',r2') + if r1' == r1 && r2' == r2 then raw else + GLambda (n,bk,r1',r2') | GProd (n,bk,r1,r2) as raw -> let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in - if r1' == r1 && r2' == r2 then raw else - GProd (n,bk,r1',r2') + if r1' == r1 && r2' == r2 then raw else + GProd (n,bk,r1',r2') | GLetIn (n,r1,t,r2) as raw -> let r1' = subst_glob_constr env subst r1 in let r2' = subst_glob_constr env subst r2 in let t' = Option.Smart.map (subst_glob_constr env subst) t in - if r1' == r1 && t == t' && r2' == r2 then raw else - GLetIn (n,r1',t',r2') + if r1' == r1 && t == t' && r2' == r2 then raw else + GLetIn (n,r1',t',r2') | GCases (sty,rtno,rl,branches) as raw -> let open CAst in @@ -1067,21 +1067,21 @@ let rec subst_glob_constr env subst = DAst.map (function if a == a' && topt == topt' then y else (a',(n,topt'))) rl and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> - let cpl' = + let cpl' = List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr env subst r in - if cpl' == cpl && r' == r then branch else + if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) - branches + branches in - if rtno' == rtno && rl' == rl && branches' == branches then raw else - GCases (sty,rtno',rl',branches') + if rtno' == rtno && rl' == rl && branches' == branches then raw else + GCases (sty,rtno',rl',branches') | GLetTuple (nal,(na,po),b,c) as raw -> let po' = Option.Smart.map (subst_glob_constr env subst) po and b' = subst_glob_constr env subst b and c' = subst_glob_constr env subst c in - if po' == po && b' == b && c' == c then raw else + if po' == po && b' == b && c' == c then raw else GLetTuple (nal,(na,po'),b',c') | GIf (c,(na,po),b1,b2) as raw -> @@ -1089,7 +1089,7 @@ let rec subst_glob_constr env subst = DAst.map (function and b1' = subst_glob_constr env subst b1 and b2' = subst_glob_constr env subst b2 and c' = subst_glob_constr env subst c in - if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else + if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else GIf (c',(na,po'),b1',b2') | GRec (fix,ida,bl,ra1,ra2) as raw -> @@ -1101,8 +1101,8 @@ let rec subst_glob_constr env subst = DAst.map (function let obd' = Option.Smart.map (subst_glob_constr env subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) bl in - if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else - GRec (fix,ida,bl',ra1',ra2') + if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else + GRec (fix,ida,bl',ra1',ra2') | GHole (knd, naming, solve) as raw -> let nknd = match knd with |