From: Stefano Zacchiroli Date: Fri, 27 May 2005 15:23:19 +0000 (+0000) Subject: refactored modules structure X-Git-Tag: PRE_INDEX_1~113 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9cfecee7dd7cf8388512ffd4aa223782c728eda;p=helm.git refactored modules structure --- diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index d75b3fe64..d56deea07 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,5 +1,6 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationSubst.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi cicNotationLexer.cmo: cicNotationLexer.cmi cicNotationLexer.cmx: cicNotationLexer.cmi @@ -7,6 +8,8 @@ cicNotationEnv.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationEnv.cmx: cicNotationPt.cmx cicNotationEnv.cmi cicNotationPp.cmo: cicNotationPt.cmo cicNotationEnv.cmi cicNotationPp.cmi cicNotationPp.cmx: cicNotationPt.cmx cicNotationEnv.cmx cicNotationPp.cmi +cicNotationSubst.cmo: cicNotationSubst.cmi +cicNotationSubst.cmx: cicNotationSubst.cmi cicNotationParser.cmo: cicNotationPt.cmo cicNotationPp.cmi \ cicNotationLexer.cmi cicNotationEnv.cmi cicNotationParser.cmi cicNotationParser.cmx: cicNotationPt.cmx cicNotationPp.cmx \ diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile index 53c39ee5e..6af1968ec 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -11,6 +11,7 @@ INTERFACE_FILES = \ cicNotationLexer.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ + cicNotationSubst.mli \ cicNotationParser.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index 79dfaf8be..13920157e 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -43,64 +43,28 @@ type value_type = type declaration = string * value_type type binding = string * (value_type * value) -type env_type = (string * (value_type * value)) list +type t = (string * (value_type * value)) list -let lookup_value ~env name = +let lookup_value env name = try snd (List.assoc name env) with Not_found -> raise (Value_not_found name) -let lookup_term ~env name = - match lookup_value ~env name with +let lookup_term env name = + match lookup_value env name with | TermValue x -> x | _ -> raise (Value_not_found name) -let lookup_num ~env name = - match lookup_value ~env name with +let lookup_num env name = + match lookup_value env name with | NumValue x -> x | _ -> raise (Value_not_found name) -let lookup_string ~env name = - match lookup_value ~env name with +let lookup_string env name = + match lookup_value env name with | StringValue x -> x | _ -> raise (Value_not_found name) -let unopt_names names env = - let rec aux acc = function - | (name, (ty, v)) :: tl when List.mem name names -> - (match ty, v with - | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl - | _ -> assert false) - | _ :: tl -> aux acc tl - (* some pattern may contain only meta names, thus we trash all others *) - | [] -> acc - in - aux [] env - -let head_names names env = - let rec aux acc = function - | (name, (ty, v)) :: tl when List.mem name names -> - (match ty, v with - | ListType ty, ListValue (v :: _) -> aux ((name, (ty, v)) :: acc) tl - | _ -> assert false) - | _ :: tl -> aux acc tl - (* base pattern may contain only meta names, thus we trash all others *) - | [] -> acc - in - aux [] env - -let tail_names names env = - let rec aux acc = function - | (name, (ty, v)) :: tl when List.mem name names -> - (match ty, v with - | ListType ty, ListValue (_ :: vtl) -> - aux ((name, (ListType ty, ListValue vtl)) :: acc) tl - | _ -> assert false) - | binding :: tl -> aux (binding :: acc) tl - | [] -> acc - in - aux [] env - let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) let opt_binding_of_name (n, ty) = (n, (OptType ty, OptValue None)) @@ -108,193 +72,3 @@ let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) let opt_declaration (n, ty) = (n, OptType ty) let list_declaration (n, ty) = (n, ListType ty) - (* TODO ensure that names generated by fresh_var do not clash with user's *) -let fresh_var = - let index = ref ~-1 in - fun () -> - incr index; - "fresh" ^ string_of_int !index - -let meta_names_of term = - let rec names = ref [] in - let add_name n = - if List.mem n !names then () - else names := n :: !names - in - let rec aux = function - | AttributedTerm (_, term) -> aux term - | Appl terms -> List.iter aux terms - | Binder (_, _, body) -> aux body - | Case (term, indty, outty_opt, patterns) -> - aux term ; - aux_opt outty_opt ; - List.iter aux_branch patterns - | LetIn (_, t1, t2) -> - aux t1 ; - aux t2 - | LetRec (_, definitions, body) -> - List.iter aux_definition definitions ; - aux body - | Uri (_, Some substs) -> aux_substs substs - | Ident (_, Some substs) -> aux_substs substs - | Meta (_, substs) -> aux_meta_substs substs - - | Implicit - | Ident _ - | Num _ - | Sort _ - | Symbol _ - | Uri _ - | UserInput -> () - - | Magic magic -> aux_magic magic - | Variable var -> aux_variable var - - | _ -> assert false - and aux_opt = function - | Some term -> aux term - | None -> () - and aux_capture_var (_, ty_opt) = aux_opt ty_opt - and aux_branch (pattern, term) = - aux_pattern pattern ; - aux term - and aux_pattern (head, vars) = - List.iter aux_capture_var vars - and aux_definition (var, term, i) = - aux_capture_var var ; - aux term - and aux_substs substs = List.iter (fun (_, term) -> aux term) substs - and aux_meta_substs meta_substs = List.iter aux_opt meta_substs - and aux_variable = function - | NumVar name -> add_name name - | IdentVar name -> add_name name - | TermVar name -> add_name name - | FreshVar _ -> () - | Ascription _ -> assert false - and aux_magic = function - | Default (t1, t2) - | Fold (_, t1, _, t2) -> - aux t1 ; - aux t2 - | _ -> assert false - in - aux term ; - !names - -let pp_term = ref (fun (t:CicNotationPt.term) -> assert false; "") -let set_pp_term f = pp_term := f - -let instantiate ~env term = - let fresh_env = ref [] in - let lookup_fresh_name n = - try - List.assoc n !fresh_env - with Not_found -> - let new_name = fresh_var () in - fresh_env := (n, new_name) :: !fresh_env; - new_name - in - let rec aux env term = - match term with - | AttributedTerm (_, term) -> aux env term - | Appl terms -> Appl (List.map (aux env) terms) - | Binder (binder, var, body) -> - Binder (binder, aux_capture_var env var, aux env body) - | Case (term, indty, outty_opt, patterns) -> - Case (aux env term, indty, aux_opt env outty_opt, - List.map (aux_branch env) patterns) - | LetIn (var, t1, t2) -> - LetIn (aux_capture_var env var, aux env t1, aux env t2) - | LetRec (kind, definitions, body) -> - LetRec (kind, List.map (aux_definition env) definitions, aux env body) - | Uri (name, None) -> Uri (name, None) - | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs)) - | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs)) - | Meta (index, substs) -> Meta (index, aux_meta_substs env substs) - - | Implicit - | Ident _ - | Num _ - | Sort _ - | Symbol _ - | UserInput -> term - - | Magic magic -> aux_magic env magic - | Variable var -> aux_variable env var - - | _ -> assert false - and aux_opt env = function - | Some term -> Some (aux env term) - | None -> None - and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt) - and aux_branch env (pattern, term) = - (aux_pattern env pattern, aux env term) - and aux_pattern env (head, vars) = - (head, List.map (aux_capture_var env) vars) - and aux_definition env (var, term, i) = - (aux_capture_var env var, aux env term, i) - and aux_substs env substs = - List.map (fun (name, term) -> (name, aux env term)) substs - and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs - and aux_variable env = function - | NumVar name -> Num (lookup_num ~env name, 0) - | IdentVar name -> Ident (lookup_string ~env name, None) - | TermVar name -> lookup_term ~env name - | FreshVar name -> Ident (lookup_fresh_name name, None) - | Ascription (term, name) -> assert false - and aux_magic env = function - | Default (some_pattern, none_pattern) -> - (match meta_names_of some_pattern with - | [] -> assert false (* some pattern must contain at least 1 name *) - | (name :: _) as names -> - (match lookup_value ~env name with - | OptValue (Some _) -> - (* assumption: if "name" above is bound to Some _, then all - * names returned by "meta_names_of" are bound to Some _ as well - *) - aux (unopt_names names env) some_pattern - | OptValue None -> aux env none_pattern - | _ -> assert false)) - | Fold (`Left, base_pattern, names, rec_pattern) -> - let acc_name = List.hd names in (* names can't be empty, cfr. parser *) - let meta_names = - List.filter ((<>) acc_name) (meta_names_of rec_pattern) - in - (match meta_names with - | [] -> assert false (* as above *) - | (name :: _) as names -> - let rec instantiate_fold_left acc env' = - prerr_endline "instantiate_fold_left"; - match lookup_value ~env:env' name with - | ListValue (_ :: _) -> - instantiate_fold_left - (let acc_binding = acc_name, (TermType, TermValue acc) in - aux (acc_binding :: head_names names env') rec_pattern) - (tail_names names env') - | ListValue [] -> acc - | _ -> assert false - in - instantiate_fold_left (aux env base_pattern) env) - | Fold (`Right, base_pattern, names, rec_pattern) -> - let acc_name = List.hd names in (* names can't be empty, cfr. parser *) - let meta_names = - List.filter ((<>) acc_name) (meta_names_of rec_pattern) - in - (match meta_names with - | [] -> assert false (* as above *) - | (name :: _) as names -> - let rec instantiate_fold_right env' = - prerr_endline "instantiate_fold_right"; - match lookup_value ~env:env' name with - | ListValue (_ :: _) -> - let acc = instantiate_fold_right (tail_names names env') in - let acc_binding = acc_name, (TermType, TermValue acc) in - aux (acc_binding :: head_names names env') rec_pattern - | ListValue [] -> aux env base_pattern - | _ -> assert false - in - instantiate_fold_right env) - | _ -> assert false - in - aux env term - diff --git a/helm/ocaml/cic_notation/cicNotationEnv.mli b/helm/ocaml/cic_notation/cicNotationEnv.mli index a5267b044..3059fc098 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.mli +++ b/helm/ocaml/cic_notation/cicNotationEnv.mli @@ -25,6 +25,8 @@ exception Value_not_found of string +(** {2 Types} *) + type value = | TermValue of CicNotationPt.term | StringValue of string @@ -41,10 +43,14 @@ type value_type = type declaration = string * value_type type binding = string * (value_type * value) -type env_type = binding list +type t = binding list + +(** {2 Environment lookup} *) - (** fills a term pattern instantiating variable magics *) -val instantiate: env:env_type -> CicNotationPt.term -> CicNotationPt.term +val lookup_value: t -> string -> value +val lookup_num: t -> string -> string +val lookup_string: t -> string -> string +val lookup_term: t -> string -> CicNotationPt.term (** {2 Bindings mangling} *) @@ -57,7 +63,3 @@ val list_binding_of_name: declaration -> binding (* [] binding *) val opt_declaration: declaration -> declaration (* t -> OptType t *) val list_declaration: declaration -> declaration (* t -> ListType t *) -(** {2 Debugging} *) - -val set_pp_term: (CicNotationPt.term -> string) -> unit - diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml index c7cc77be0..d282e3d70 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.ml +++ b/helm/ocaml/cic_notation/cicNotationParser.ml @@ -77,7 +77,7 @@ type binding = | Env of (string * value_type) list let make_action action bindings = - let rec aux (vl : env_type) = + let rec aux (vl : CicNotationEnv.t) = function [] -> prerr_endline "aux: make_action"; @@ -111,7 +111,7 @@ let make_action action bindings = aux ((name, (ListType t, (ListValue v))) :: vl) tl) | Env _ :: tl -> prerr_endline "aux: env"; - Gramext.action (fun (v:env_type) -> aux (v @ vl) tl) + Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl) (* LUCA: DEFCON 2 END *) in aux [] (List.rev bindings) @@ -160,7 +160,7 @@ let extract_term_production pattern = match magic with | Opt p -> let p_bindings, p_atoms, p_names, p_action = inner_pattern p in - let action (env_opt : env_type option) (loc : location) = + let action (env_opt : CicNotationEnv.t option) (loc : location) = match env_opt with | Some env -> List.map opt_binding_some env | None -> List.map opt_binding_of_name p_names @@ -188,7 +188,7 @@ let extract_term_production pattern = (fun env (n, (_, v)) -> grow_env_entry env n v) env env_i in - let action (env_list : env_type list) (loc : location) = + let action (env_list : CicNotationEnv.t list) (loc : location) = prerr_endline "list action"; List.fold_right grow_env env_list env0 in @@ -217,7 +217,8 @@ let extract_term_production pattern = let p_names = flatten_opt p_bindings in let _ = prerr_endline ("inner names: " ^ String.concat " " (List.map fst p_names)) in let action = - make_action (fun (env : env_type) (loc : location) -> prerr_endline "inner action"; env) p_bindings + make_action (fun (env : CicNotationEnv.t) (loc : location) -> env) + p_bindings in p_bindings, p_atoms, p_names, action in @@ -247,7 +248,7 @@ let extend level1_pattern ?(precedence = default_precedence) associativity, [ p_atoms, (make_action - (fun (env: env_type) (loc: location) -> (action env loc)) + (fun (env: CicNotationEnv.t) (loc: location) -> (action env loc)) p_bindings) ]]] in p_atoms diff --git a/helm/ocaml/cic_notation/cicNotationParser.mli b/helm/ocaml/cic_notation/cicNotationParser.mli index b619606d0..6192bf05b 100644 --- a/helm/ocaml/cic_notation/cicNotationParser.mli +++ b/helm/ocaml/cic_notation/cicNotationParser.mli @@ -48,7 +48,7 @@ val extend: CicNotationPt.term -> ?precedence:int -> ?associativity:Gramext.g_assoc -> - (CicNotationEnv.env_type -> CicNotationPt.location -> CicNotationPt.term) -> + (CicNotationEnv.t -> CicNotationPt.location -> CicNotationPt.term) -> rule_id val delete: rule_id -> unit diff --git a/helm/ocaml/cic_notation/cicNotationPp.mli b/helm/ocaml/cic_notation/cicNotationPp.mli index 77f65bf5f..ca22765f8 100644 --- a/helm/ocaml/cic_notation/cicNotationPp.mli +++ b/helm/ocaml/cic_notation/cicNotationPp.mli @@ -25,7 +25,7 @@ val pp_term: CicNotationPt.term -> string -val pp_env: CicNotationEnv.env_type -> string +val pp_env: CicNotationEnv.t -> string val pp_value: CicNotationEnv.value -> string val pp_value_type: CicNotationEnv.value_type -> string diff --git a/helm/ocaml/cic_notation/cicNotationSubst.ml b/helm/ocaml/cic_notation/cicNotationSubst.ml new file mode 100644 index 000000000..6effb66b2 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationSubst.ml @@ -0,0 +1,251 @@ +(* 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. + * + * 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 CicNotationEnv +open CicNotationPt + + (* TODO ensure that names generated by fresh_var do not clash with user's *) +let fresh_var = + let index = ref ~-1 in + fun () -> + incr index; + "fresh" ^ string_of_int !index + +let meta_names_of term = + let rec names = ref [] in + let add_name n = + if List.mem n !names then () + else names := n :: !names + in + let rec aux = function + | AttributedTerm (_, term) -> aux term + | Appl terms -> List.iter aux terms + | Binder (_, _, body) -> aux body + | Case (term, indty, outty_opt, patterns) -> + aux term ; + aux_opt outty_opt ; + List.iter aux_branch patterns + | LetIn (_, t1, t2) -> + aux t1 ; + aux t2 + | LetRec (_, definitions, body) -> + List.iter aux_definition definitions ; + aux body + | Uri (_, Some substs) -> aux_substs substs + | Ident (_, Some substs) -> aux_substs substs + | Meta (_, substs) -> aux_meta_substs substs + + | Implicit + | Ident _ + | Num _ + | Sort _ + | Symbol _ + | Uri _ + | UserInput -> () + + | Magic magic -> aux_magic magic + | Variable var -> aux_variable var + + | _ -> assert false + and aux_opt = function + | Some term -> aux term + | None -> () + and aux_capture_var (_, ty_opt) = aux_opt ty_opt + and aux_branch (pattern, term) = + aux_pattern pattern ; + aux term + and aux_pattern (head, vars) = + List.iter aux_capture_var vars + and aux_definition (var, term, i) = + aux_capture_var var ; + aux term + and aux_substs substs = List.iter (fun (_, term) -> aux term) substs + and aux_meta_substs meta_substs = List.iter aux_opt meta_substs + and aux_variable = function + | NumVar name -> add_name name + | IdentVar name -> add_name name + | TermVar name -> add_name name + | FreshVar _ -> () + | Ascription _ -> assert false + and aux_magic = function + | Default (t1, t2) + | Fold (_, t1, _, t2) -> + aux t1 ; + aux t2 + | _ -> assert false + in + aux term ; + !names + +let unopt_names names env = + let rec aux acc = function + | (name, (ty, v)) :: tl when List.mem name names -> + (match ty, v with + | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl + | _ -> assert false) + | _ :: tl -> aux acc tl + (* some pattern may contain only meta names, thus we trash all others *) + | [] -> acc + in + aux [] env + +let head_names names env = + let rec aux acc = function + | (name, (ty, v)) :: tl when List.mem name names -> + (match ty, v with + | ListType ty, ListValue (v :: _) -> aux ((name, (ty, v)) :: acc) tl + | _ -> assert false) + | _ :: tl -> aux acc tl + (* base pattern may contain only meta names, thus we trash all others *) + | [] -> acc + in + aux [] env + +let tail_names names env = + let rec aux acc = function + | (name, (ty, v)) :: tl when List.mem name names -> + (match ty, v with + | ListType ty, ListValue (_ :: vtl) -> + aux ((name, (ListType ty, ListValue vtl)) :: acc) tl + | _ -> assert false) + | binding :: tl -> aux (binding :: acc) tl + | [] -> acc + in + aux [] env + +let instantiate_level2 env term = + let fresh_env = ref [] in + let lookup_fresh_name n = + try + List.assoc n !fresh_env + with Not_found -> + let new_name = fresh_var () in + fresh_env := (n, new_name) :: !fresh_env; + new_name + in + let rec aux env term = + match term with + | AttributedTerm (_, term) -> aux env term + | Appl terms -> Appl (List.map (aux env) terms) + | Binder (binder, var, body) -> + Binder (binder, aux_capture_var env var, aux env body) + | Case (term, indty, outty_opt, patterns) -> + Case (aux env term, indty, aux_opt env outty_opt, + List.map (aux_branch env) patterns) + | LetIn (var, t1, t2) -> + LetIn (aux_capture_var env var, aux env t1, aux env t2) + | LetRec (kind, definitions, body) -> + LetRec (kind, List.map (aux_definition env) definitions, aux env body) + | Uri (name, None) -> Uri (name, None) + | Uri (name, Some substs) -> Uri (name, Some (aux_substs env substs)) + | Ident (name, Some substs) -> Ident (name, Some (aux_substs env substs)) + | Meta (index, substs) -> Meta (index, aux_meta_substs env substs) + + | Implicit + | Ident _ + | Num _ + | Sort _ + | Symbol _ + | UserInput -> term + + | Magic magic -> aux_magic env magic + | Variable var -> aux_variable env var + + | _ -> assert false + and aux_opt env = function + | Some term -> Some (aux env term) + | None -> None + and aux_capture_var env (name, ty_opt) = (aux env name, aux_opt env ty_opt) + and aux_branch env (pattern, term) = + (aux_pattern env pattern, aux env term) + and aux_pattern env (head, vars) = + (head, List.map (aux_capture_var env) vars) + and aux_definition env (var, term, i) = + (aux_capture_var env var, aux env term, i) + and aux_substs env substs = + List.map (fun (name, term) -> (name, aux env term)) substs + and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs + and aux_variable env = function + | NumVar name -> Num (lookup_num env name, 0) + | IdentVar name -> Ident (lookup_string env name, None) + | TermVar name -> lookup_term env name + | FreshVar name -> Ident (lookup_fresh_name name, None) + | Ascription (term, name) -> assert false + and aux_magic env = function + | Default (some_pattern, none_pattern) -> + (match meta_names_of some_pattern with + | [] -> assert false (* some pattern must contain at least 1 name *) + | (name :: _) as names -> + (match lookup_value env name with + | OptValue (Some _) -> + (* assumption: if "name" above is bound to Some _, then all + * names returned by "meta_names_of" are bound to Some _ as well + *) + aux (unopt_names names env) some_pattern + | OptValue None -> aux env none_pattern + | _ -> assert false)) + | Fold (`Left, base_pattern, names, rec_pattern) -> + let acc_name = List.hd names in (* names can't be empty, cfr. parser *) + let meta_names = + List.filter ((<>) acc_name) (meta_names_of rec_pattern) + in + (match meta_names with + | [] -> assert false (* as above *) + | (name :: _) as names -> + let rec instantiate_fold_left acc env' = + prerr_endline "instantiate_fold_left"; + match lookup_value env' name with + | ListValue (_ :: _) -> + instantiate_fold_left + (let acc_binding = acc_name, (TermType, TermValue acc) in + aux (acc_binding :: head_names names env') rec_pattern) + (tail_names names env') + | ListValue [] -> acc + | _ -> assert false + in + instantiate_fold_left (aux env base_pattern) env) + | Fold (`Right, base_pattern, names, rec_pattern) -> + let acc_name = List.hd names in (* names can't be empty, cfr. parser *) + let meta_names = + List.filter ((<>) acc_name) (meta_names_of rec_pattern) + in + (match meta_names with + | [] -> assert false (* as above *) + | (name :: _) as names -> + let rec instantiate_fold_right env' = + prerr_endline "instantiate_fold_right"; + match lookup_value env' name with + | ListValue (_ :: _) -> + let acc = instantiate_fold_right (tail_names names env') in + let acc_binding = acc_name, (TermType, TermValue acc) in + aux (acc_binding :: head_names names env') rec_pattern + | ListValue [] -> aux env base_pattern + | _ -> assert false + in + instantiate_fold_right env) + | _ -> assert false + in + aux env term + diff --git a/helm/ocaml/cic_notation/cicNotationSubst.mli b/helm/ocaml/cic_notation/cicNotationSubst.mli new file mode 100644 index 000000000..0cb0a8669 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationSubst.mli @@ -0,0 +1,30 @@ +(* 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. + * + * 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/ + *) + + (** fills a term pattern instantiating variable magics *) +val instantiate_level2: + CicNotationEnv.t -> CicNotationPt.term -> + CicNotationPt.term + diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index bcb7e661b..d39c0ff94 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -26,7 +26,6 @@ open Printf let _ = - CicNotationEnv.set_pp_term CicNotationPp.pp_term; let module P = CicNotationPt in let level = ref ~-1 in let arg_spec = [ "-level", Arg.Set_int level, "set the notation level" ] in @@ -86,7 +85,7 @@ let _ = (fun env loc -> prerr_endline "ENV"; prerr_endline (CicNotationPp.pp_env env); - CicNotationEnv.instantiate env l2))) + CicNotationSubst.instantiate_level2 env l2))) (* CicNotationParser.print_l2_pattern ()) *) | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream) | 2 ->