+++ /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 Printf
-
-module Ast = CicNotationPt
-module Env = CicNotationEnv
-
-let unopt_names names env =
- let rec aux acc = function
- | (name, (ty, v)) :: tl when List.mem name names ->
- (match ty, v with
- | Env.OptType ty, Env.OptValue (Some v) ->
- aux ((name, (ty, v)) :: acc) tl
- | _ -> assert false)
- | hd :: tl -> aux (hd :: acc) tl
- | [] -> 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
- | Env.ListType ty, Env.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
- | Env.ListType ty, Env.ListValue (_ :: vtl) ->
- aux ((name, (Env.ListType ty, Env.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 =
-(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
- match term with
- | Ast.AttributedTerm (_, term) -> aux env term
- | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
- | Ast.Binder (binder, var, body) ->
- Ast.Binder (binder, aux_capture_var env var, aux env body)
- | Ast.Case (term, indty, outty_opt, patterns) ->
- Ast.Case (aux env term, indty, aux_opt env outty_opt,
- List.map (aux_branch env) patterns)
- | Ast.LetIn (var, t1, t2) ->
- Ast.LetIn (aux_capture_var env var, aux env t1, aux env t2)
- | Ast.LetRec (kind, definitions, body) ->
- Ast.LetRec (kind, List.map (aux_definition env) definitions,
- aux env body)
- | Ast.Uri (name, None) -> Ast.Uri (name, None)
- | Ast.Uri (name, Some substs) ->
- Ast.Uri (name, Some (aux_substs env substs))
- | Ast.Ident (name, Some substs) ->
- Ast.Ident (name, Some (aux_substs env substs))
- | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
-
- | Ast.Implicit
- | Ast.Ident _
- | Ast.Num _
- | Ast.Sort _
- | Ast.Symbol _
- | Ast.UserInput -> term
-
- | Ast.Magic magic -> aux_magic env magic
- | Ast.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, hrefs, vars) =
- (head, hrefs, 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
- | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
- | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
- | Ast.TermVar name -> Env.lookup_term env name
- | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
- | Ast.Ascription (term, name) -> assert false
- and aux_magic env = function
- | Ast.Default (some_pattern, none_pattern) ->
- let some_pattern_names = CicNotationUtil.names_of_term some_pattern in
- let none_pattern_names = CicNotationUtil.names_of_term none_pattern in
- let opt_names =
- List.filter
- (fun name -> not (List.mem name none_pattern_names))
- some_pattern_names
- in
- (match opt_names with
- | [] -> assert false (* some pattern must contain at least 1 name *)
- | (name :: _) as names ->
- (match Env.lookup_value env name with
- | Env.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
- | Env.OptValue None -> aux env none_pattern
- | _ ->
- prerr_endline (sprintf
- "lookup of %s in env %s did not return an optional value"
- name (CicNotationPp.pp_env env));
- assert false))
- | Ast.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)
- (CicNotationUtil.names_of_term rec_pattern)
- in
- (match meta_names with
- | [] -> assert false (* as above *)
- | (name :: _) as names ->
- let rec instantiate_fold_left acc env' =
- match Env.lookup_value env' name with
- | Env.ListValue (_ :: _) ->
- instantiate_fold_left
- (let acc_binding =
- acc_name, (Env.TermType, Env.TermValue acc)
- in
- aux (acc_binding :: head_names names env') rec_pattern)
- (tail_names names env')
- | Env.ListValue [] -> acc
- | _ -> assert false
- in
- instantiate_fold_left (aux env base_pattern) env)
- | Ast.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)
- (CicNotationUtil.names_of_term rec_pattern)
- in
- (match meta_names with
- | [] -> assert false (* as above *)
- | (name :: _) as names ->
- let rec instantiate_fold_right env' =
- match Env.lookup_value env' name with
- | Env.ListValue (_ :: _) ->
- let acc = instantiate_fold_right (tail_names names env') in
- let acc_binding =
- acc_name, (Env.TermType, Env.TermValue acc)
- in
- aux (acc_binding :: head_names names env') rec_pattern
- | Env.ListValue [] -> aux env base_pattern
- | _ -> assert false
- in
- instantiate_fold_right env)
- | Ast.If (_, p_true, p_false) as t ->
- aux env (CicNotationUtil.find_branch (Ast.Magic t))
- | Ast.Fail -> assert false
- | _ -> assert false
- in
- aux env term
-
-let instantiate_appl_pattern env appl_pattern =
- let lookup name =
- try List.assoc name env
- with Not_found ->
- prerr_endline (sprintf "Name %s not found" name);
- assert false
- in
- let rec aux = function
- | Ast.UriPattern uri -> CicUtil.term_of_uri uri
- | Ast.ImplicitPattern -> Cic.Implicit None
- | Ast.VarPattern name -> lookup name
- | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
- in
- aux appl_pattern
-
projects / helm.git / blobdiff