1 (* Copyright (C) 2004-2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 exception Value_not_found of string
32 | StringValue of string
34 | OptValue of value option
35 | ListValue of value list
41 | OptType of value_type
42 | ListType of value_type
44 type declaration = string * value_type
45 type binding = string * (value_type * value)
46 type env_type = (string * (value_type * value)) list
48 let lookup_value ~env name =
50 snd (List.assoc name env)
51 with Not_found -> raise (Value_not_found name)
53 let lookup_term ~env name =
54 match lookup_value ~env name with
56 | _ -> raise (Value_not_found name)
58 let lookup_num ~env name =
59 match lookup_value ~env name with
61 | _ -> raise (Value_not_found name)
63 let lookup_string ~env name =
64 match lookup_value ~env name with
66 | _ -> raise (Value_not_found name)
68 let unopt_names names env =
69 let rec aux acc = function
70 | (name, (ty, v)) :: tl when List.mem name names ->
72 | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl
74 | _ :: tl -> aux acc tl
79 let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v)))
80 let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None))
81 let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None))
82 let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue []))
83 let opt_declaration (n, ty) = (n, OptType ty)
84 let list_declaration (n, ty) = (n, ListType ty)
86 (* TODO ensure that names generated by fresh_var do not clash with user's *)
88 let index = ref ~-1 in
91 "fresh" ^ string_of_int !index
93 let meta_names_of term =
94 let rec names = ref [] in
96 if List.mem n !names then ()
97 else names := n :: !names
99 let rec aux = function
100 | AttributedTerm (_, term) -> aux term
101 | Appl terms -> List.iter aux terms
102 | Binder (_, _, body) -> aux body
103 | Case (term, indty, outty_opt, patterns) ->
106 List.iter aux_branch patterns
107 | LetIn (_, t1, t2) ->
110 | LetRec (_, definitions, body) ->
111 List.iter aux_definition definitions ;
113 | Uri (_, Some substs) -> aux_substs substs
114 | Ident (_, Some substs) -> aux_substs substs
115 | Meta (_, substs) -> aux_meta_substs substs
125 | Magic magic -> aux_magic magic
126 | Variable var -> aux_variable var
129 and aux_opt = function
130 | Some term -> aux term
132 and aux_capture_var (_, ty_opt) = aux_opt ty_opt
133 and aux_branch (pattern, term) =
134 aux_pattern pattern ;
136 and aux_pattern (head, vars) =
137 List.iter aux_capture_var vars
138 and aux_definition (var, term, i) =
139 aux_capture_var var ;
141 and aux_substs substs = List.iter (fun (_, term) -> aux term) substs
142 and aux_meta_substs meta_substs = List.iter aux_opt meta_substs
143 and aux_variable = function
144 | NumVar name -> add_name name
145 | IdentVar name -> add_name name
146 | TermVar name -> add_name name
148 | Ascription _ -> assert false
149 and aux_magic = function
150 | Fold (_, t1, _, t2) ->
153 | Default (t1, t2) ->
161 let instantiate ~env term =
162 let fresh_env = ref [] in
163 let lookup_fresh_name n =
165 List.assoc n !fresh_env
167 let new_name = fresh_var () in
168 fresh_env := (n, new_name) :: !fresh_env;
171 let rec aux env term =
173 | AttributedTerm (_, term) -> aux env term
174 | Appl terms -> Appl (List.map (aux env) terms)
175 | Binder (binder, var, body) ->
176 Binder (binder, aux_capture_var env var, aux env body)
177 | Case (term, indty, outty_opt, patterns) ->
178 Case (aux env term, indty, aux_opt env outty_opt,
179 List.map (aux_branch env) patterns)
180 | LetIn (var, t1, t2) ->
181 LetIn (aux_capture_var env var, aux env t1, aux env t2)
182 | LetRec (kind, definitions, body) ->
183 LetRec (kind, List.map (aux_definition env) definitions, aux env body)
184 | Uri (name, None) -> Uri (name, None)
185 | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs))
186 | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs))
187 | Meta (index, substs) -> Meta (index, aux_meta_substs env substs)
196 | Magic magic -> aux_magic env magic
197 | Variable var -> aux_variable env var
200 and aux_opt env = function
201 | Some term -> Some (aux env term)
203 and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt)
204 and aux_branch env (pattern, term) =
205 (aux_pattern env pattern, aux env term)
206 and aux_pattern env (head, vars) =
207 (head, List.map (aux_capture_var env) vars)
208 and aux_definition env (var, term, i) =
209 (aux_capture_var env var, aux env term, i)
210 and aux_substs env substs =
211 List.map (fun (name, term) -> (name, aux env term)) substs
212 and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
213 and aux_variable env = function
214 | NumVar name -> Num (lookup_num ~env name, 0)
215 | IdentVar name -> Ident (lookup_string ~env name, None)
216 | TermVar name -> lookup_term ~env name
217 | FreshVar name -> Ident (lookup_fresh_name name, None)
218 | Ascription (term, name) -> assert false
219 and aux_magic env = function
220 | Default (some_pattern, none_pattern) ->
221 (match meta_names_of some_pattern with
222 | [] -> assert false (* some pattern must contain at least 1 name *)
223 | (name :: _) as names ->
224 (match lookup_value ~env name with
225 | OptValue (Some _) ->
226 (* assumption: if "name" above is bound to Some _, then all
227 * names returned by "meta_names_of" are bound to Some _ as well
229 aux (unopt_names names env) some_pattern
230 | OptValue None -> aux env none_pattern
231 | _ -> assert false))
232 | Fold _ -> failwith "not yet implemented" (* TODO Fold *)