2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
22 | GRef of string * string
25 | Prod of string * term * term
26 | Abst of string * term * term
27 | Abbr of string * term * term * term
28 | Case of term * term * term * term list
29 | Sigs of string list * term list * term list
31 (* internal functions *******************************************************)
34 let rec aux = function
37 if n = s then i, j else aux tl
41 let rec get_names ss j t =
42 if j <= 0 then ss else match t with
43 | Abst (s, _, t) -> get_names (s :: ss) (pred j) t
46 let rec trim_absts j t =
47 if j <= 0 then t else match t with
48 | Abst (_, _, t) -> trim_absts (pred j) t
51 let proc_appl ts = match ts with
52 | GRef (s, _) :: vs ->
53 let i, j = get_sigs s in
54 if L.length vs <> i + j || i = 0 || j = 0 then Appl ts else
55 let types, preds = X.split_at j vs in
56 let names = get_names [] j (L.hd preds) in
57 let preds = L.rev_map (trim_absts j) preds in
58 Sigs (names, types, preds)
61 let rec proc_term = function
63 | C.Implicit _ -> Meta
66 let s, name = K.resolve_reference c in
69 | C.Appl ts -> proc_appl (proc_terms ts)
70 | C.Prod (s, w, t) -> Prod (s, proc_term w, proc_term t)
71 | C.Lambda (s, w, t) -> Abst (s, proc_term w, proc_term t)
72 | C.LetIn (s, w, v, t) -> Abbr (s, proc_term w, proc_term v, proc_term t)
73 | C.Match (c, u, v, ts) -> Case (proc_term (C.Const c), proc_term u, proc_term v, proc_terms ts)
76 L.rev (L.rev_map proc_term ts)
78 (* interface functions ******************************************************)
80 let process = proc_term