From: Stefano Zacchiroli Date: Tue, 31 May 2005 09:45:45 +0000 (+0000) Subject: snapshot (the thing on the doorstep) X-Git-Tag: PRE_INDEX_1~93 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=724827ba7e5c1419229382487bed53f7dbb862db;p=helm.git snapshot (the thing on the doorstep) --- 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/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml new file mode 100644 index 000000000..b200de2ef --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -0,0 +1,244 @@ +(* 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 + +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 = CicNotationUtil.fresh_name () 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/cicNotationFwd.mli b/helm/ocaml/cic_notation/cicNotationFwd.mli new file mode 100644 index 000000000..0cb0a8669 --- /dev/null +++ b/helm/ocaml/cic_notation/cicNotationFwd.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/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/cicNotationSubst.ml b/helm/ocaml/cic_notation/cicNotationSubst.ml deleted file mode 100644 index 6effb66b2..000000000 --- a/helm/ocaml/cic_notation/cicNotationSubst.ml +++ /dev/null @@ -1,251 +0,0 @@ -(* 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 deleted file mode 100644 index 0cb0a8669..000000000 --- a/helm/ocaml/cic_notation/cicNotationSubst.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* 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/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 ->