X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtksourceview%2Ftest%2Ftest.txt;h=083521327e64dc118be01078a8c8a2719c7b4898;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=08a4617f7c97cb672017e5215c9f9f4e2db78100;hpb=38e7f42c1f3eb0da34c25c281f6ba18ef91c970a;p=helm.git diff --git a/helm/DEVEL/lablgtksourceview/test/test.txt b/helm/DEVEL/lablgtksourceview/test/test.txt index 08a4617f7..083521327 100644 --- a/helm/DEVEL/lablgtksourceview/test/test.txt +++ b/helm/DEVEL/lablgtksourceview/test/test.txt @@ -1,373 +1,211 @@ -(* Copyright (C) 2004-2005, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. +/* CPU control. + * (C) 2001, 2002, 2003, 2004 Rusty Russell * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -open Printf - -module Pt = CicNotationPt -module Env = CicNotationEnv -module Util = CicNotationUtil - -type pattern_id = int - -exception No_match - -module OrderedInt = -struct - type t = int - let compare (x1:t) (x2:t) = Pervasives.compare x2 x1 (* reverse order *) -end - -module IntSet = Set.Make (OrderedInt) - -let int_set_of_int_list l = - List.fold_left (fun acc i -> IntSet.add i acc) IntSet.empty l - -type pattern_kind = Variable | Constructor -type tag_t = int - -module type PATTERN = -sig - type pattern_t - type term_t - val classify : pattern_t -> pattern_kind - val tag_of_pattern : pattern_t -> tag_t * pattern_t list - val tag_of_term : term_t -> tag_t * term_t list -end - -module Matcher (P: PATTERN) = -struct - type row_t = P.pattern_t list * P.pattern_t list * pattern_id - type t = row_t list - - let compatible p1 p2 = P.classify p1 = P.classify p2 - - let matched = List.map (fun (matched, _, pid) -> matched, pid) - - let partition t pidl = - let partitions = Hashtbl.create 11 in - let add pid row = Hashtbl.add partitions pid row in - (try - List.iter2 add pidl t - with Invalid_argument _ -> assert false); - let pidset = int_set_of_int_list pidl in - IntSet.fold - (fun pid acc -> - match Hashtbl.find_all partitions pid with - | [] -> acc - | patterns -> (pid, List.rev patterns) :: acc) - pidset [] - - let are_empty t = - match t with - | (_, [], _) :: _ -> true - (* if first row has an empty list of patterns, then others have as well *) - | _ -> false - - (* return 2 lists of rows, first one containing homogeneous rows according - * to "compatible" below *) - let horizontal_split t = - let ap, first_row, t', first_row_class = - match t with - | [] -> assert false - | (_, [], _) :: _ -> - assert false (* are_empty should have been invoked in advance *) - | ((_, hd :: _ , _) as row) :: tl -> hd, row, tl, P.classify hd - in - let rec aux prev_t = function - | [] -> List.rev prev_t, [] - | (_, [], _) :: _ -> assert false - | ((_, hd :: _, _) as row) :: tl when compatible ap hd -> - aux (row :: prev_t) tl - | t -> List.rev prev_t, t - in - let rows1, rows2 = aux [first_row] t' in - first_row_class, rows1, rows2 - - (* return 2 lists, first one representing first column, second one - * representing a new pattern matrix where matched patterns have been moved - * to decl *) - let vertical_split t = - List.map - (function - | decls, hd :: tl, pid -> hd :: decls, tl, pid - | _ -> assert false) - t - - let variable_closure k = - (fun matched_terms terms -> - prerr_endline "variable_closure"; - match terms with - | hd :: tl -> k (hd :: matched_terms) tl - | _ -> assert false) - - let constructor_closure ks k = - (fun matched_terms terms -> - prerr_endline "constructor_closure"; - match terms with - | t :: tl -> - (try - let tag, subterms = P.tag_of_term t in - let k' = List.assoc tag ks in - k' matched_terms (subterms @ tl) - with Not_found -> k matched_terms terms) - | [] -> assert false) - - let compiler rows match_cb fail_k = - let rec aux t k = - if t = [] then - k - else if are_empty t then - let res = match_cb (matched t) in - (fun matched_terms _ -> res matched_terms) - else - match horizontal_split t with - | _, [], _ -> assert false - | Variable, t', [] -> variable_closure (aux (vertical_split t') k) - | Constructor, t', [] -> - let tagl = - List.map - (function - | _, p :: _, _ -> fst (P.tag_of_pattern p) - | _ -> assert false) - t' - in - let clusters = partition t' tagl in - let ks = - List.map - (fun (tag, cluster) -> - let cluster' = - List.map (* add args as patterns heads *) - (function - | matched_p, p :: tl, pid -> - let _, subpatterns = P.tag_of_pattern p in - matched_p, subpatterns @ tl, pid - | _ -> assert false) - cluster - in - tag, aux cluster' k) - clusters - in - constructor_closure ks k - | _, t', t'' -> aux t' (aux t'' k) - in - let t = List.map (fun (p, pid) -> [], [p], pid) rows in - let matcher = aux t (fun _ _ -> fail_k ()) in - (fun term -> matcher [] [term]) -end - -module Matcher21 = -struct - module Pattern21 = - struct - type pattern_t = Pt.term - type term_t = Pt.term - let classify = function - | Pt.Variable _ -> Variable - | Pt.Magic _ - | Pt.Layout _ - | Pt.Literal _ as t -> - prerr_endline (CicNotationPp.pp_term t); - assert false - | _ -> Constructor - let tag_of_pattern = CicNotationTag.get_tag - let tag_of_term = CicNotationTag.get_tag - end - - module M = Matcher (Pattern21) - - let extract_magic term = - let magic_map = ref [] in - let add_magic m = - let name = Util.fresh_name () in - magic_map := (name, m) :: !magic_map; - Pt.Variable (Pt.TermVar name) - in - let rec aux = function - | Pt.AttributedTerm (_, t) -> aux t - | Pt.Literal _ - | Pt.Layout _ -> assert false - | Pt.Variable v -> Pt.Variable v - | Pt.Magic m -> add_magic m - | t -> Util.visit_ast aux t - in - let term' = aux term in - term', !magic_map - - let env_of_matched pl tl = - List.map2 - (fun p t -> - match p, t with - Pt.Variable (Pt.TermVar name), _ -> - name, (Env.TermType, Env.TermValue t) - | Pt.Variable (Pt.NumVar name), (Pt.Num (s, _)) -> - name, (Env.NumType, Env.NumValue s) - | Pt.Variable (Pt.IdentVar name), (Pt.Ident (s, None)) -> - name, (Env.StringType, Env.StringValue s) - | _ -> assert false) - pl tl - - let rec compiler rows = - let rows', magic_maps = - List.split - (List.map - (fun (p, pid) -> - let p', map = extract_magic p in - (p', pid), (pid, map)) - rows) - in - let magichecker map = - List.fold_left - (fun f (name, m) -> - let m_checker = compile_magic m in - (fun env -> - match m_checker (Env.lookup_term env name) env with - | None -> None - | Some env' -> f env')) - (fun env -> Some env) - map - in - let magichooser candidates = - List.fold_left - (fun f (pid, pl, checker) -> - (fun matched_terms -> - let env = env_of_matched pl matched_terms in - match checker env with - | None -> f matched_terms - | Some env -> Some (env, pid))) - (fun _ -> None) - candidates - in - let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); - let candidates = - List.map - (fun (pl, pid) -> - let magic_map = - try List.assoc pid magic_maps with Not_found -> assert false - in - pid, pl, magichecker magic_map) - rows - in - magichooser candidates - in - M.compiler rows' match_cb (fun _ -> None) - - and compile_magic = function - | Pt.Fold (kind, p_base, names, p_rec) -> - let p_rec_decls = Env.declarations_of_term p_rec in - let acc_name = try List.hd names with Failure _ -> assert false in - let compiled = compiler [p_base, 0; p_rec, 1] in - (fun term env -> - let rec aux term = - match compiled term with - | None -> None - | Some (env', 0) -> Some (env', []) - | Some (env', 1) -> - begin - let acc = Env.lookup_term env' acc_name in - let env'' = Env.remove env' acc_name in - match aux acc with - | None -> None - | Some (base_env, rec_envl) -> - Some (base_env, env'' :: rec_envl ) - end - | _ -> assert false - in - match aux term with - | None -> None - | Some (base_env, rec_envl) -> - Some (base_env @ Env.coalesce_env p_rec_decls rec_envl)) - | Pt.Default (p_some, p_none) -> (* p_none can't bound names *) - let p_some_decls = Env.declarations_of_term p_some in - let none_env = List.map Env.opt_binding_of_name p_some_decls in - let compiled = compiler [p_some, 0] in - (fun term env -> - match compiled term with - | None -> Some none_env - | Some (env', 0) -> Some (List.map Env.opt_binding_some env' @ env) - | _ -> assert false) - | _ -> assert false -end - -module Matcher32 = -struct - module Pattern32 = - struct - type cic_mask_t = - Blob - | Uri of string - | Appl of cic_mask_t list - - let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) - - let mask_of_cic = function - | Cic.AAppl (_, tl) -> Appl (List.map (fun _ -> Blob) tl), tl - | Cic.AConst (_, _, []) - | Cic.AVar (_, _, []) - | Cic.AMutInd (_, _, _, []) - | Cic.AMutConstruct (_, _, _, _, []) as t -> Uri (uri_of_term t), [] - | _ -> Blob, [] - - let tag_of_term t = - let mask, tl = mask_of_cic t in - Hashtbl.hash mask, tl - - let mask_of_appl_pattern = function - | Pt.UriPattern s -> Uri s, [] - | Pt.VarPattern _ -> Blob, [] - | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl - - let tag_of_pattern p = - let mask, pl = mask_of_appl_pattern p in - Hashtbl.hash mask, pl - - type pattern_t = Pt.cic_appl_pattern - type term_t = Cic.annterm - - let classify = function - | Pt.VarPattern _ -> Variable - | _ -> Constructor - end - - module M = Matcher (Pattern32) - - let compiler rows = - let match_cb rows = - prerr_endline (sprintf "match_cb on %d row(s)" (List.length rows)); - let pl, pid = try List.hd rows with Not_found -> assert false in - (fun matched_terms -> - let env = - List.map2 - (fun p t -> - match p with - | Pt.VarPattern name -> name, t - | _ -> assert false) - pl matched_terms - in - Some (env, pid)) - in - M.compiler rows match_cb (fun () -> None) -end - + * This code is licenced under the GPL. + */ +#include +#include +#include +#include +#include +#include +#include +#include +#include /* for hotplug_path */ +#include +#include +#include + +/* This protects CPUs going up and down... */ +DECLARE_MUTEX(cpucontrol); + +static struct notifier_block *cpu_chain; + +/* Need to know about CPUs going up/down? */ +int register_cpu_notifier(struct notifier_block *nb) +{ + int ret; + + if ((ret = down_interruptible(&cpucontrol)) != 0) + return ret; + ret = notifier_chain_register(&cpu_chain, nb); + up(&cpucontrol); + return ret; +} +EXPORT_SYMBOL(register_cpu_notifier); + +void unregister_cpu_notifier(struct notifier_block *nb) +{ + down(&cpucontrol); + notifier_chain_unregister(&cpu_chain, nb); + up(&cpucontrol); +} +EXPORT_SYMBOL(unregister_cpu_notifier); + +#ifdef CONFIG_HOTPLUG_CPU +static inline void check_for_tasks(int cpu) +{ + struct task_struct *p; + + write_lock_irq(&tasklist_lock); + for_each_process(p) { + if (task_cpu(p) == cpu && (p->utime != 0 || p->stime != 0)) + printk(KERN_WARNING "Task %s (pid = %d) is on cpu %d\ + (state = %ld, flags = %lx) \n", + p->comm, p->pid, cpu, p->state, p->flags); + } + write_unlock_irq(&tasklist_lock); +} + +/* Notify userspace when a cpu event occurs, by running '/sbin/hotplug + * cpu' with certain environment variables set. */ +static int cpu_run_sbin_hotplug(unsigned int cpu, const char *action) +{ + char *argv[3], *envp[5], cpu_str[12], action_str[32]; + int i; + + sprintf(cpu_str, "CPU=%d", cpu); + sprintf(action_str, "ACTION=%s", action); + /* FIXME: Add DEVPATH. --RR */ + + i = 0; + argv[i++] = hotplug_path; + argv[i++] = "cpu"; + argv[i] = NULL; + + i = 0; + /* minimal command environment */ + envp[i++] = "HOME=/"; + envp[i++] = "PATH=/sbin:/bin:/usr/sbin:/usr/bin"; + envp[i++] = cpu_str; + envp[i++] = action_str; + envp[i] = NULL; + + return call_usermodehelper(argv[0], argv, envp, 0); +} + +/* Take this CPU down. */ +static int take_cpu_down(void *unused) +{ + int err; + + /* Take offline: makes arch_cpu_down somewhat easier. */ + cpu_clear(smp_processor_id(), cpu_online_map); + + /* Ensure this CPU doesn't handle any more interrupts. */ + err = __cpu_disable(); + if (err < 0) + cpu_set(smp_processor_id(), cpu_online_map); + else + /* Force idle task to run as soon as we yield: it should + immediately notice cpu is offline and die quickly. */ + sched_idle_next(); + + return err; +} + +int cpu_down(unsigned int cpu) +{ + int err; + struct task_struct *p; + cpumask_t old_allowed, tmp; + + if ((err = lock_cpu_hotplug_interruptible()) != 0) + return err; + + if (num_online_cpus() == 1) { + err = -EBUSY; + goto out; + } + + if (!cpu_online(cpu)) { + err = -EINVAL; + goto out; + } + + /* Ensure that we are not runnable on dying cpu */ + old_allowed = current->cpus_allowed; + tmp = CPU_MASK_ALL; + cpu_clear(cpu, tmp); + set_cpus_allowed(current, tmp); + + p = __stop_machine_run(take_cpu_down, NULL, cpu); + if (IS_ERR(p)) { + err = PTR_ERR(p); + goto out_allowed; + } + + if (cpu_online(cpu)) + goto out_thread; + + /* Wait for it to sleep (leaving idle task). */ + while (!idle_cpu(cpu)) + yield(); + + /* This actually kills the CPU. */ + __cpu_die(cpu); + + /* Move it here so it can run. */ + kthread_bind(p, smp_processor_id()); + + /* CPU is completely dead: tell everyone. Too late to complain. */ + if (notifier_call_chain(&cpu_chain, CPU_DEAD, (void *)(long)cpu) + == NOTIFY_BAD) + BUG(); + + check_for_tasks(cpu); + + cpu_run_sbin_hotplug(cpu, "offline"); + +out_thread: + err = kthread_stop(p); +out_allowed: + set_cpus_allowed(current, old_allowed); +out: + unlock_cpu_hotplug(); + return err; +} +#else +static inline int cpu_run_sbin_hotplug(unsigned int cpu, const char *action) +{ + return 0; +} +#endif /*CONFIG_HOTPLUG_CPU*/ + +int __devinit cpu_up(unsigned int cpu) +{ + int ret; + void *hcpu = (void *)(long)cpu; + + if ((ret = down_interruptible(&cpucontrol)) != 0) + return ret; + + if (cpu_online(cpu) || !cpu_present(cpu)) { + ret = -EINVAL; + goto out; + } + ret = notifier_call_chain(&cpu_chain, CPU_UP_PREPARE, hcpu); + if (ret == NOTIFY_BAD) { + printk("%s: attempt to bring up CPU %u failed\n", + __FUNCTION__, cpu); + ret = -EINVAL; + goto out_notify; + } + + /* Arch-specific enabling code. */ + ret = __cpu_up(cpu); + if (ret != 0) + goto out_notify; + if (!cpu_online(cpu)) + BUG(); + + /* Now call notifier in preparation. */ + notifier_call_chain(&cpu_chain, CPU_ONLINE, hcpu); + +out_notify: + if (ret != 0) + notifier_call_chain(&cpu_chain, CPU_UP_CANCELED, hcpu); +out: + up(&cpucontrol); + return ret; +}