* http://helm.cs.unibo.it/
*)
-open CicNotationEnv
-open CicNotationPt
+open Printf
-(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
- * be removes as soon as we believe implementation are equivalent *)
-(* 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 *)
+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
- | OptType ty, OptValue (Some v) -> aux ((name, (ty, v)) :: acc) tl
+ | Env.OptType ty, Env.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 *)
+ | hd :: tl -> aux (hd :: acc) tl
| [] -> acc
in
aux [] 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
+ | 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 *)
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
+ | 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
new_name
in
let rec aux env term =
+(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *)
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,
+ | 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)
- | 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)
+ | 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)
- | Implicit
- | Ident _
- | Num _
- | Sort _
- | Symbol _
- | UserInput -> term
+ | Ast.Implicit
+ | Ast.Ident _
+ | Ast.Num _
+ | Ast.Sort _
+ | Ast.Symbol _
+ | Ast.UserInput -> term
- | Magic magic -> aux_magic env magic
- | Variable var -> aux_variable env var
+ | Ast.Magic magic -> aux_magic env magic
+ | Ast.Variable var -> aux_variable env var
| _ -> assert false
and aux_opt env = function
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_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
- | 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
+ | 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
- | Default (some_pattern, none_pattern) ->
- (match CicNotationUtil.names_of_term some_pattern with
+ | 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 lookup_value env name with
- | OptValue (Some _) ->
+ (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
- | OptValue None -> aux env none_pattern
- | _ -> assert false))
- | Fold (`Left, base_pattern, names, rec_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)
| [] -> 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 (_ :: _) ->
+ match Env.lookup_value env' name with
+ | Env.ListValue (_ :: _) ->
instantiate_fold_left
- (let acc_binding = acc_name, (TermType, TermValue acc) in
+ (let acc_binding =
+ acc_name, (Env.TermType, Env.TermValue acc)
+ in
aux (acc_binding :: head_names names env') rec_pattern)
(tail_names names env')
- | ListValue [] -> acc
+ | Env.ListValue [] -> acc
| _ -> assert false
in
instantiate_fold_left (aux env base_pattern) env)
- | Fold (`Right, base_pattern, names, rec_pattern) ->
+ | 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)
| [] -> 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 (_ :: _) ->
+ match Env.lookup_value env' name with
+ | Env.ListValue (_ :: _) ->
let acc = instantiate_fold_right (tail_names names env') in
- let acc_binding = acc_name, (TermType, TermValue acc) in
+ let acc_binding =
+ acc_name, (Env.TermType, Env.TermValue acc)
+ in
aux (acc_binding :: head_names names env') rec_pattern
- | ListValue [] -> aux env base_pattern
+ | Env.ListValue [] -> aux env base_pattern
| _ -> assert false
in
instantiate_fold_right env)
- | If (_, body)
- | Unless (_, body) -> aux env body
+ | 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