X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationFwd.ml;h=bf4b3e38e7beb17623542f91ed2ec1b2260696c6;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=8e955c0b10a8d562647833d501477c3aa87a28ff;hpb=c27b932e5adcf89dc9de0e28f65e3370fe3e6b05;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml index 8e955c0b1..bf4b3e38e 100644 --- a/helm/ocaml/cic_notation/cicNotationFwd.ml +++ b/helm/ocaml/cic_notation/cicNotationFwd.ml @@ -23,85 +23,19 @@ * 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 @@ -110,7 +44,8 @@ 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 + | 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 *) @@ -122,8 +57,8 @@ 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 + | 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 @@ -141,32 +76,36 @@ let instantiate_level2 env term = 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 @@ -175,33 +114,44 @@ let instantiate_level2 env term = 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) @@ -211,17 +161,19 @@ let instantiate_level2 env term = | [] -> assert false (* as above *) | (name :: _) as names -> let rec instantiate_fold_left acc env' = - 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) @@ -231,18 +183,36 @@ let instantiate_level2 env term = | [] -> assert false (* as above *) | (name :: _) as names -> let rec instantiate_fold_right env' = - 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 (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t)) - | Fail -> assert false + | 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 +