diff options
Diffstat (limited to 'library/impargs.ml')
| -rw-r--r-- | library/impargs.ml | 190 |
1 files changed, 53 insertions, 137 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index 8a9429a4..08ae2aa5 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: impargs.ml,v 1.59.2.1 2004/07/16 19:30:35 herbelin Exp $ *) +(* $Id: impargs.ml 8672 2006-03-29 21:06:33Z herbelin $ *) open Util open Names @@ -27,63 +27,44 @@ open Topconstr (* les implicites sont stricts par défaut en v8 *) let implicit_args = ref false -let strict_implicit_args = ref (not !Options.v7) +let strict_implicit_args = ref true let contextual_implicit_args = ref false -let implicit_args_out = ref false -let strict_implicit_args_out = ref true -let contextual_implicit_args_out = ref false - let make_implicit_args flag = - implicit_args := flag; - if not !Options.v7_only then implicit_args_out := flag; - if !Options.translate_strict_impargs then - strict_implicit_args_out := not flag + implicit_args := flag let make_strict_implicit_args flag = - strict_implicit_args := flag; - if not !Options.v7_only then strict_implicit_args_out := flag + strict_implicit_args := flag let make_contextual_implicit_args flag = - contextual_implicit_args := flag; - if not !Options.v7_only then contextual_implicit_args_out := flag + contextual_implicit_args := flag let is_implicit_args () = !implicit_args -let is_implicit_args_out () = !implicit_args_out let is_strict_implicit_args () = !strict_implicit_args let is_contextual_implicit_args () = !contextual_implicit_args -type implicits_flags = (bool * bool * bool) * (bool * bool * bool) +type implicits_flags = bool * bool * bool + +let implicits_flags () = + (!implicit_args, !strict_implicit_args, !contextual_implicit_args) -let with_implicits ((a,b,c),(d,e,g)) f x = +let with_implicits (a,b,c) f x = let oa = !implicit_args in let ob = !strict_implicit_args in let oc = !contextual_implicit_args in - let od = !implicit_args_out in - let oe = !strict_implicit_args_out in - let og = !contextual_implicit_args_out in try implicit_args := a; strict_implicit_args := b; contextual_implicit_args := c; - implicit_args_out := d; - strict_implicit_args_out := e; - contextual_implicit_args_out := g; let rslt = f x in implicit_args := oa; strict_implicit_args := ob; contextual_implicit_args := oc; - implicit_args_out := od; - strict_implicit_args_out := oe; - contextual_implicit_args_out := og; rslt with e -> begin implicit_args := oa; strict_implicit_args := ob; contextual_implicit_args := oc; - implicit_args_out := od; - strict_implicit_args_out := oe; - contextual_implicit_args_out := og; raise e end @@ -135,7 +116,7 @@ let update pos rig (na,st) = | Some (DepFlexAndRigid (fpos,rpos) as x) -> if argument_less (pos,fpos) or pos=fpos then DepRigid pos else if argument_less (pos,rpos) then DepFlexAndRigid (fpos,pos) else x - | Some (DepFlex fpos as x) -> + | Some (DepFlex fpos) -> if argument_less (pos,fpos) or pos=fpos then DepRigid pos else DepFlexAndRigid (fpos,pos) | Some Manual -> assert false @@ -213,13 +194,9 @@ let compute_implicits_gen strict contextual env t = Array.to_list v | _ -> [] -let compute_implicits output env t = - let strict = - (not output & !strict_implicit_args) or - (output & !strict_implicit_args_out) in - let contextual = - (not output & !contextual_implicit_args) or - (output & !contextual_implicit_args_out) in +let compute_implicits env t = + let strict = !strict_implicit_args in + let contextual = !contextual_implicit_args in let l = compute_implicits_gen strict contextual env t in List.map (function | (Name id, Some imp) -> Some (id,imp) @@ -267,20 +244,11 @@ type implicits = | No_impl let auto_implicits env ty = - let impl = - if !implicit_args then - let l = compute_implicits false env ty in - Impl_auto (!strict_implicit_args,!contextual_implicit_args,l) - else - No_impl in - if Options.do_translate () then - impl, - if !implicit_args_out then - (let l = compute_implicits true env ty in - Impl_auto (!strict_implicit_args_out,!contextual_implicit_args_out,l)) - else No_impl - else - impl, impl + if !implicit_args then + let l = compute_implicits env ty in + Impl_auto (!strict_implicit_args,!contextual_implicit_args,l) + else + No_impl let list_of_implicits = function | Impl_auto (_,_,l) -> l @@ -289,7 +257,7 @@ let list_of_implicits = function (*s Constants. *) -let constants_table = ref KNmap.empty +let constants_table = ref Cmap.empty let compute_constant_implicits kn = let env = Global.env () in @@ -297,7 +265,7 @@ let compute_constant_implicits kn = auto_implicits env (body_of_type cb.const_type) let constant_implicits sp = - try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl + try Cmap.find sp !constants_table with Not_found -> No_impl (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -326,10 +294,11 @@ let compute_mib_implicits kn = Array.mapi imps_one_inductive mib.mind_packets let inductive_implicits indp = - try Indmap.find indp !inductives_table with Not_found -> No_impl,No_impl + try Indmap.find indp !inductives_table with Not_found -> No_impl let constructor_implicits consp = - try Constrmap.find consp !constructors_table with Not_found -> No_impl,No_impl + try Constrmap.find consp !constructors_table with Not_found -> No_impl + (*s Variables. *) let var_table = ref Idmap.empty @@ -340,7 +309,17 @@ let compute_var_implicits id = auto_implicits env ty let var_implicits id = - try Idmap.find id !var_table with Not_found -> No_impl,No_impl + try Idmap.find id !var_table with Not_found -> No_impl + +(* Implicits of a global reference. *) + +let compute_global_implicits = function + | VarRef id -> compute_var_implicits id + | ConstRef kn -> compute_constant_implicits kn + | IndRef (kn,i) -> + let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps + | ConstructRef ((kn,i),j) -> + let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) (* Caching implicits *) @@ -349,16 +328,19 @@ let cache_implicits_decl (r,imps) = | VarRef id -> var_table := Idmap.add id imps !var_table | ConstRef kn -> - constants_table := KNmap.add kn imps !constants_table + constants_table := Cmap.add kn imps !constants_table | IndRef indp -> inductives_table := Indmap.add indp imps !inductives_table; | ConstructRef consp -> constructors_table := Constrmap.add consp imps !constructors_table -let cache_implicits (_,l) = List.iter cache_implicits_decl l +let load_implicits _ (_,l) = List.iter cache_implicits_decl l + +let cache_implicits o = + load_implicits 1 o let subst_implicits_decl subst (r,imps as o) = - let r' = subst_global subst r in if r==r' then o else (r',imps) + let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (_,subst,l) = list_smartmap (subst_implicits_decl subst) l @@ -366,40 +348,27 @@ let subst_implicits (_,subst,l) = let (in_implicits, _) = declare_object {(default_object "IMPLICITS") with cache_function = cache_implicits; - load_function = (fun _ -> cache_implicits); + load_function = load_implicits; subst_function = subst_implicits; classify_function = (fun (_,x) -> Substitute x); export_function = (fun x -> Some x) } -(* Implicits of a global reference. *) - -let compute_global_implicits = function - | VarRef id -> compute_var_implicits id - | ConstRef kn -> compute_constant_implicits kn - | IndRef (kn,i) -> - let ((_,imps),_) = (compute_mib_implicits kn).(i) in imps - | ConstructRef ((kn,i),j) -> - let (_,cimps) = (compute_mib_implicits kn).(i) in snd cimps.(j-1) - let declare_implicits_gen r = add_anonymous_leaf (in_implicits [r,compute_global_implicits r]) let declare_implicits r = with_implicits - ((true,!strict_implicit_args,!contextual_implicit_args), - (true,!strict_implicit_args_out,!contextual_implicit_args_out)) + (true,!strict_implicit_args,!contextual_implicit_args) declare_implicits_gen r let declare_var_implicits id = - if !implicit_args or !implicit_args_out then - declare_implicits_gen (VarRef id) + if !implicit_args then declare_implicits_gen (VarRef id) let declare_constant_implicits kn = - if !implicit_args or !implicit_args_out then - declare_implicits_gen (ConstRef kn) + if !implicit_args then declare_implicits_gen (ConstRef kn) let declare_mib_implicits kn = - if !implicit_args or !implicit_args_out then + if !implicit_args then let imps = compute_mib_implicits kn in let imps = array_map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) imps in @@ -412,28 +381,10 @@ let implicits_of_global_gen = function | ConstructRef csp -> constructor_implicits csp let implicits_of_global r = - let (imp_in,imp_out) = implicits_of_global_gen r in - list_of_implicits imp_in - -let implicits_of_global_out r = - let (imp_in,imp_out) = implicits_of_global_gen r in - list_of_implicits imp_out + list_of_implicits (implicits_of_global_gen r) (* Declare manual implicits *) -(* -let check_range n = function - | loc,ExplByPos i -> - if i<1 or i>n then error ("Bad argument number: "^(string_of_int i)) - | loc,ExplByName id -> -() -*) - -let rec list_remove a = function - | b::l when a = b -> l - | b::l -> b::list_remove a l - | [] -> raise Not_found - let set_implicit id imp = Some (id,match imp with None -> Manual | Some imp -> imp) @@ -443,15 +394,13 @@ let declare_manual_implicits r l = let n = List.length autoimps in if not (list_distinct l) then error ("Some parameters are referred more than once"); -(* List.iter (check_range n) l;*) -(* let l = List.sort (-) l in*) (* Compare with automatic implicits to recover printing data and names *) let rec merge k l = function | (Name id,imp)::imps -> let l',imp = - try list_remove (ExplByPos k) l, set_implicit id imp + try list_remove_first (ExplByPos k) l, set_implicit id imp with Not_found -> - try list_remove (ExplByName id) l, set_implicit id imp + try list_remove_first (ExplByName id) l, set_implicit id imp with Not_found -> l, None in imp :: merge (k+1) l' imps @@ -470,8 +419,6 @@ let declare_manual_implicits r l = (str "Cannot set implicit argument number " ++ int i ++ str ": it has no name") in let l = Impl_manual (merge 1 l autoimps) in - let (_,oimp_out) = implicits_of_global_gen r in - let l = l, if !Options.v7_only then oimp_out else l in add_anonymous_leaf (in_implicits [r,l]) (* Tests if declared implicit *) @@ -481,11 +428,11 @@ let test = function | Impl_auto (s,c,_) -> true,s,c let test_if_implicit find a = - try let b,c = find a in test b, test c - with Not_found -> (false,false,false),(false,false,false) + try let b = find a in test b + with Not_found -> (false,false,false) let is_implicit_constant sp = - test_if_implicit (KNmap.find sp) !constants_table + test_if_implicit (Cmap.find sp) !constants_table let is_implicit_inductive_definition indp = test_if_implicit (Indmap.find (indp,0)) !inductives_table @@ -496,7 +443,7 @@ let is_implicit_var id = (*s Registration as global tables *) let init () = - constants_table := KNmap.empty; + constants_table := Cmap.empty; inductives_table := Indmap.empty; constructors_table := Constrmap.empty; var_table := Idmap.empty @@ -518,34 +465,3 @@ let _ = Summary.init_function = init; Summary.survive_module = false; Summary.survive_section = false } - -(* Remark: flags implicit_args, contextual_implicit_args - are synchronized by the general options mechanism - see Vernacentries *) - -let init () = - (* strict_implicit_args_out must be not !Options.v7 - but init is done before parsing *) - strict_implicit_args:=not !Options.v7; - implicit_args_out:=false; - (* strict_implicit_args_out needs to be not !Options.v7 or - Options.do_translate() but init is done before parsing *) - strict_implicit_args_out:=true; - contextual_implicit_args_out:=false - -let freeze () = - (!strict_implicit_args, - !implicit_args_out,!strict_implicit_args_out,!contextual_implicit_args_out) - -let unfreeze (b,d,e,f) = - strict_implicit_args := b; - implicit_args_out := d; - strict_implicit_args_out := e; - contextual_implicit_args_out := f - -let _ = - Summary.declare_summary "implicits-out-options" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = true } |