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 \
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 = \
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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 <name, type> 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:
+ * <name environment, term environment, pattern id>, 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
+
--- /dev/null
+(* 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 *)
+
+++ /dev/null
-(* 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
-
+++ /dev/null
-(* 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
-
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
(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 ->
projects / helm.git / commitdiff