From 724827ba7e5c1419229382487bed53f7dbb862db Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 31 May 2005 09:45:45 +0000 Subject: [PATCH] snapshot (the thing on the doorstep) --- helm/ocaml/cic_notation/.depend | 13 +- helm/ocaml/cic_notation/Makefile | 5 +- ...{cicNotationSubst.ml => cicNotationFwd.ml} | 9 +- ...icNotationSubst.mli => cicNotationFwd.mli} | 0 helm/ocaml/cic_notation/cicNotationRew.ml | 472 ++++++++++++++++++ helm/ocaml/cic_notation/cicNotationRew.mli | 31 ++ helm/ocaml/cic_notation/cicNotationUtil.ml | 32 ++ helm/ocaml/cic_notation/cicNotationUtil.mli | 27 + helm/ocaml/cic_notation/test_parser.ml | 2 +- 9 files changed, 578 insertions(+), 13 deletions(-) rename helm/ocaml/cic_notation/{cicNotationSubst.ml => cicNotationFwd.ml} (97%) rename helm/ocaml/cic_notation/{cicNotationSubst.mli => cicNotationFwd.mli} (100%) create mode 100644 helm/ocaml/cic_notation/cicNotationRew.ml create mode 100644 helm/ocaml/cic_notation/cicNotationRew.mli create mode 100644 helm/ocaml/cic_notation/cicNotationUtil.ml create mode 100644 helm/ocaml/cic_notation/cicNotationUtil.mli diff --git a/helm/ocaml/cic_notation/.depend b/helm/ocaml/cic_notation/.depend index d56deea07..9e2292de1 100644 --- a/helm/ocaml/cic_notation/.depend +++ b/helm/ocaml/cic_notation/.depend @@ -1,15 +1,22 @@ cicNotationEnv.cmi: cicNotationPt.cmo cicNotationPp.cmi: cicNotationPt.cmo cicNotationEnv.cmi -cicNotationSubst.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationFwd.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationRew.cmi: cicNotationPt.cmo cicNotationParser.cmi: cicNotationPt.cmo cicNotationEnv.cmi +cicNotationUtil.cmo: cicNotationUtil.cmi +cicNotationUtil.cmx: cicNotationUtil.cmi cicNotationLexer.cmo: cicNotationLexer.cmi cicNotationLexer.cmx: cicNotationLexer.cmi 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 +cicNotationFwd.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationEnv.cmi \ + cicNotationFwd.cmi +cicNotationFwd.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationEnv.cmx \ + cicNotationFwd.cmi +cicNotationRew.cmo: cicNotationUtil.cmi cicNotationPt.cmo cicNotationRew.cmi +cicNotationRew.cmx: cicNotationUtil.cmx cicNotationPt.cmx cicNotationRew.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 6af1968ec..b38315464 100644 --- a/helm/ocaml/cic_notation/Makefile +++ b/helm/ocaml/cic_notation/Makefile @@ -5,13 +5,16 @@ REQUIRES = \ helm-cic \ helm-utf8_macros \ camlp4.gramlib \ + helm-cic_proof_checking \ ulex \ $(NULL) INTERFACE_FILES = \ + cicNotationUtil.mli \ cicNotationLexer.mli \ cicNotationEnv.mli \ cicNotationPp.mli \ - cicNotationSubst.mli \ + cicNotationFwd.mli \ + cicNotationRew.mli \ cicNotationParser.mli \ $(NULL) IMPLEMENTATION_FILES = \ diff --git a/helm/ocaml/cic_notation/cicNotationSubst.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml similarity index 97% rename from helm/ocaml/cic_notation/cicNotationSubst.ml rename to helm/ocaml/cic_notation/cicNotationFwd.ml index 6effb66b2..b200de2ef 100644 --- a/helm/ocaml/cic_notation/cicNotationSubst.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -26,13 +26,6 @@ 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 = @@ -141,7 +134,7 @@ let instantiate_level2 env term = try List.assoc n !fresh_env with Not_found -> - let new_name = fresh_var () in + let new_name = CicNotationUtil.fresh_name () in fresh_env := (n, new_name) :: !fresh_env; new_name in diff --git a/helm/ocaml/cic_notation/cicNotationSubst.mli b/helm/ocaml/cic_notation/cicNotationFwd.mli similarity index 100% rename from helm/ocaml/cic_notation/cicNotationSubst.mli rename to helm/ocaml/cic_notation/cicNotationFwd.mli diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml new file mode 100644 index 000000000..8253efd16 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationRew.ml @@ -0,0 +1,472 @@ +(* 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/ + *) + +type pattern_id = int + +type term_info = + { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t; + uri: (Cic.id, string) Hashtbl.t; + } + +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 + +let (compiled32: (term_info -> Cic.annterm -> CicNotationPt.term) option ref) = + ref None + +let get_compiled32 () = + match !compiled32 with + | None -> assert false + | Some f -> f + +let set_compiled32 f = compiled32 := Some f + +let warning s = prerr_endline ("CicNotation WARNING: " ^ s) + +module Patterns = + struct + type row_t = CicNotationPt.cic_appl_pattern list * pattern_id + type t = row_t list + + let first_column t = List.map (fun (patterns, _) -> List.hd patterns) t + let pattern_ids t = List.map snd t + + let prepend_column t column = + try + List.map2 (fun elt (pl, pid) -> (elt :: pl), pid) column t + + with Invalid_argument _ -> assert false + + let prepend_columns t columns = + List.fold_right + (fun column rows -> prepend_column rows column) + columns t + + 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 = fst (List.hd t) = [] + (* if first row has an empty list of patterns, then others will as well *) + + (* return 2 lists of rows, first one containing homogeneous rows according + * to "compatible" below *) + let horizontal_split t = + let compatible ap1 ap2 = + match ap1, ap2 with + | CicNotationPt.UriPattern _, CicNotationPt.UriPattern _ + | CicNotationPt.ArgPattern _, CicNotationPt.ArgPattern _ + | CicNotationPt.ApplPattern _, CicNotationPt.ApplPattern _ -> true + | _ -> false + in + let ap = + match t with + | [] -> assert false + | ([], _) :: _ -> + assert false (* are_empty should have been invoked in advance *) + | (hd :: _ , _) :: _ -> 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 + aux [] t + + (* return 2 lists, first one representing first column, second one + * representing rows stripped of the first element *) + let vertical_split t = + let l = + List.map + (function + | (hd :: tl, pid) -> hd, (tl, pid) + | _ -> assert false) + t + in + List.split l + end + +let get_types uri = + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + match o with + | Cic.InductiveDefinition (l,_,_,_) -> l + | _ -> assert false + +let name_of_inductive_type uri i = + let types = get_types uri in + let (name, _, _, _) = try List.nth types i with Not_found -> assert false in + name + + (* returns pairs *) +let constructors_of_inductive_type uri i = + let types = get_types uri in + let (_, _, _, constructors) = + try List.nth types i with Not_found -> assert false + in + constructors + + (* returns name only *) +let constructor_of_inductive_type uri i j = + (try + fst (List.nth (constructors_of_inductive_type uri i) (j-1)) + with Not_found -> assert false) + +module Ast = CicNotationPt + +let string_of_name = function + | Cic.Name s -> s + | Cic.Anonymous -> "_" + +let ident_of_name n = Ast.Ident (string_of_name n, None) + +let ast_of_acic0 term_info acic k = + let k = k term_info in + let register_uri id uri = Hashtbl.add term_info.uri id uri in + let sort_of_id id = + try + Hashtbl.find term_info.sort id + with Not_found -> assert false + in + let idref id t = Ast.AttributedTerm (`IdRef id, t) in + let aux_substs substs = + Some + (List.map + (fun (uri, annterm) -> (UriManager.name_of_uri uri, k annterm)) + substs) + in + let aux_context context = + List.map + (function + | None -> None + | Some annterm -> Some (k annterm)) + context + in + let aux = function + | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None)) + | Cic.AVar (id,uri,substs) -> + register_uri id (UriManager.string_of_uri uri); + idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) + | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l)) + | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop) + | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set) + | Cic.ASort (id,Cic.Type _) -> idref id (Ast.Sort `Type) + | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp) + | Cic.AImplicit _ -> assert false + | Cic.AProd (id,n,s,t) -> + let binder_kind = + match sort_of_id id with + | `Set | `Type -> `Pi + | `Prop | `CProp -> `Forall + in + idref id (Ast.Binder (binder_kind, (ident_of_name n, Some (k s)), k t)) + | Cic.ACast (id,v,t) -> + idref id (Ast.Appl [idref id (Ast.Symbol ("cast", 0)); k v; k t]) + | Cic.ALambda (id,n,s,t) -> + idref id (Ast.Binder (`Lambda, (ident_of_name n, Some (k s)), k t)) + | Cic.ALetIn (id,n,s,t) -> + idref id (Ast.LetIn ((ident_of_name n, None), k s, k t)) + | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args)) + | Cic.AConst (id,uri,substs) -> + idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs)) + | Cic.AMutInd (id,uri,i,substs) -> + let name = name_of_inductive_type uri i in + idref id (Ast.Ident (name, aux_substs substs)) + | Cic.AMutConstruct (id,uri,i,j,substs) -> + let name = constructor_of_inductive_type uri i j in + idref id (Ast.Ident (name, aux_substs substs)) + | Cic.AMutCase (id,uri,typeno,ty,te,patterns) -> + let name = name_of_inductive_type uri typeno in + let constructors = constructors_of_inductive_type uri typeno in + let rec eat_branch ty pat = + match (ty, pat) with + | Cic.Prod (_, _, t), Cic.ALambda (_, name, s, t') -> + let (cv, rhs) = eat_branch t t' in + (ident_of_name name, Some (k s)) :: cv, rhs + | _, _ -> [], k pat + in + let patterns = + List.map2 + (fun (name, ty) pat -> + let (capture_variables, rhs) = eat_branch ty pat in + ((name, capture_variables), rhs)) + constructors patterns + in + idref id (Ast.Case (k te, Some name, Some (k ty), patterns)) + | Cic.AFix (id, no, funs) -> + let defs = + List.map + (fun (_, n, decr_idx, ty, bo) -> + ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx)) + funs + in + let name = + try + (match List.nth defs no with + | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _ -> assert false) + with Not_found -> assert false + in + idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None))) + | Cic.ACoFix (id, no, funs) -> + let defs = + List.map + (fun (_, n, ty, bo) -> ((Ast.Ident (n, None), Some (k ty)), k bo, 0)) + funs + in + let name = + try + (match List.nth defs no with + | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n + | _ -> assert false) + with Not_found -> assert false + in + idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None))) + in + aux acic + + (* "envl" is a list of triples: + * , where + * name environment: (string * string) list + * term environment: (string * Cic.annterm) list *) +let return_closure success_k = + (fun term_info terms envl -> + match terms with + | [] -> + (try + success_k term_info (List.hd envl) + with Failure _ -> assert false) + | _ -> assert false) + +let variable_closure names k = + (fun term_info terms envl -> + match terms with + | hd :: tl -> + let envl' = + List.map2 + (fun arg (name_env, term_env, pid) -> + let rec aux name_env term_env pid arg term = + match arg, term with + Ast.IdentArg name, _ -> + (name_env, (name, term) :: term_env, pid) + | Ast.EtaArg (Some name, arg'), + Cic.ALambda (_, name', ty, body) -> + aux ((name, (string_of_name name', Some ty)) :: name_env) + term_env pid arg' body + | Ast.EtaArg (Some name, arg'), _ -> + let name' = CicNotationUtil.fresh_name () in + aux ((name, (name', None)) :: name_env) + term_env pid arg' term + | Ast.EtaArg (None, arg'), Cic.ALambda (_, name, ty, body) -> + assert false + | Ast.EtaArg (None, arg'), _ -> + assert false + in + aux name_env term_env pid arg hd) + names envl + in + k term_info tl envl' + | _ -> assert false) + +let appl_closure ks k = + (fun term_info terms envl -> + (match terms with + | Cic.AAppl (_, args) :: tl -> + (try + let k' = List.assoc (List.length args) ks in + k' term_info (args @ tl) envl + with Not_found -> k term_info terms envl) + | [] -> assert false + | _ -> k term_info terms envl)) + +let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t) + +let uri_closure ks k = + (fun term_info terms envl -> + (match terms with + | [] -> assert false + | hd :: tl -> + begin + try + let k' = List.assoc (uri_of_term hd) ks in + k' term_info tl envl + with + | Invalid_argument _ (* raised by uri_of_term *) + | Not_found -> k term_info terms envl + end)) + + (* compiler from level 3 to level 2 *) +let compiler32 (t: Patterns.t) success_k fail_k = + let rec aux t k = (* k is a continuation *) + if t = [] then + k + else if Patterns.are_empty t then begin + (match t with + | _::_::_ -> warning "Ambiguous patterns" + | _ -> ()); + return_closure success_k + end else + match Patterns.horizontal_split t with + | t', [] -> + (match t' with + | [] + | ([], _) :: _ -> assert false + | (Ast.ArgPattern (Ast.IdentArg _) :: _, _) :: _ + | (Ast.ArgPattern (Ast.EtaArg _) :: _, _) :: _ -> + let first_column, t'' = Patterns.vertical_split t' in + let names = + List.map + (function + | Ast.ArgPattern arg -> arg + | _ -> assert false) + first_column + in + variable_closure names (aux t'' k) + | (Ast.ApplPattern _ :: _, _) :: _ -> + let pidl = + List.map + (function + | (Ast.ApplPattern args) :: _, _ -> List.length args + | _ -> assert false) + t' + in + (* arity partitioning *) + let clusters = Patterns.partition t' pidl in + let ks = (* k continuation list *) + List.map + (fun (len, cluster) -> + let cluster' = + List.map (* add args as patterns heads *) + (function + | (Ast.ApplPattern args) :: tl, pid -> + (* let's throw away "teste di cluster" *) + args @ tl, pid + | _ -> assert false) + cluster + in + len, aux cluster' k) + clusters + in + appl_closure ks k + | (Ast.UriPattern _ :: _, _) :: _ -> + let uidmap, pidl = + let urimap = ref [] in + let uidmap = ref [] in + let get_uri_id uri = + try + List.assoc uri !urimap + with + Not_found -> + let uid = List.length !urimap in + urimap := (uri, uid) :: !urimap ; + uidmap := (uid, uri) :: !uidmap ; + uid + in + let uidl = + List.map + (function + | (Ast.UriPattern uri) :: _, _ -> get_uri_id uri + | _ -> assert false) + t' + in + !uidmap, uidl + in + let clusters = Patterns.partition t' pidl in + let ks = + List.map + (fun (uid, cluster) -> + let cluster' = + List.map + (function + | (Ast.UriPattern uri) :: tl, pid -> tl, pid + | _ -> assert false) + cluster + in + List.assoc uid uidmap, aux cluster' k) + clusters + in + uri_closure ks k) + | t', tl -> aux t' (aux tl k) + in + let matcher = aux t (fun _ _ -> raise No_match) in + (fun term_info annterm -> + try + matcher term_info [annterm] (List.map (fun (_, pid) -> [], [], pid) t) + with No_match -> fail_k term_info annterm) + +let ast_of_acic1 term_info annterm = (get_compiled32 ()) term_info annterm + +let load_patterns t instantiate = + let ast_env_of_name_env term_info name_env = + List.map + (fun (name, (name', ty_opt)) -> + let ast_ty_opt = + match ty_opt with + | None -> None + | Some annterm -> Some (ast_of_acic1 term_info annterm) + in + (name, (name', ast_ty_opt))) + name_env + in + let ast_env_of_term_env term_info = + List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) + in + let fail_k term_info annterm = ast_of_acic0 term_info annterm ast_of_acic1 in + let success_k term_info (name_env, term_env, pid) = + instantiate + term_info + (ast_env_of_name_env term_info name_env) + (ast_env_of_term_env term_info term_env) + pid + in + let compiled32 = compiler32 t success_k fail_k in + set_compiled32 compiled32 + +let ast_of_acic id_to_sort annterm = + let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in + let ast = ast_of_acic1 term_info annterm in + ast, term_info.uri + diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli new file mode 100644 index 000000000..cac67cb21 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationRew.mli @@ -0,0 +1,31 @@ +(* 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/ + *) + +val ast_of_acic: + (Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) + Cic.annterm -> (* acic *) + CicNotationPt.term (* ast *) + * (Cic.id, string) Hashtbl.t (* id -> uri *) + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.ml b/helm/ocaml/cic_notation/cicNotationUtil.ml new file mode 100644 index 000000000..ff0b7fc73 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationUtil.ml @@ -0,0 +1,32 @@ +(* 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/ + *) + + (* TODO ensure that names generated by fresh_var do not clash with user's *) +let fresh_name = + let index = ref ~-1 in + fun () -> + incr index; + "fresh" ^ string_of_int !index + diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli new file mode 100644 index 000000000..14cec5826 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationUtil.mli @@ -0,0 +1,27 @@ +(* 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/ + *) + +val fresh_name: unit -> string + diff --git a/helm/ocaml/cic_notation/test_parser.ml b/helm/ocaml/cic_notation/test_parser.ml index d39c0ff94..6e0160e7a 100644 --- a/helm/ocaml/cic_notation/test_parser.ml +++ b/helm/ocaml/cic_notation/test_parser.ml @@ -85,7 +85,7 @@ let _ = (fun env loc -> prerr_endline "ENV"; prerr_endline (CicNotationPp.pp_env env); - CicNotationSubst.instantiate_level2 env l2))) + CicNotationFwd.instantiate_level2 env l2))) (* CicNotationParser.print_l2_pattern ()) *) | 1 -> ignore (CicNotationParser.parse_syntax_pattern istream) | 2 -> -- 2.39.2