X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationEnv.ml;h=62212f92fba871d7462d1b3ac80bb13d0574a193;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=79dfaf8be4b8dfd59da2332430add45e146f88ca;hpb=b19ee5bd8a25151b78eb1c78f98e6ab1f4b325ff;p=helm.git diff --git a/helm/ocaml/cic_notation/cicNotationEnv.ml b/helm/ocaml/cic_notation/cicNotationEnv.ml index 79dfaf8be..62212f92f 100644 --- a/helm/ocaml/cic_notation/cicNotationEnv.ml +++ b/helm/ocaml/cic_notation/cicNotationEnv.ml @@ -23,12 +23,10 @@ * http://helm.cs.unibo.it/ *) -open CicNotationPt - -exception Value_not_found of string +module Ast = CicNotationPt type value = - | TermValue of term + | TermValue of Ast.term | StringValue of string | NumValue of string | OptValue of value option @@ -41,65 +39,52 @@ type value_type = | OptType of value_type | ListType of value_type +exception Value_not_found of string +exception Type_mismatch of string * value_type + type declaration = string * value_type type binding = string * (value_type * value) -type env_type = (string * (value_type * value)) list +type t = binding list + +let lookup env name = + try + List.assoc name env + with Not_found -> raise (Value_not_found name) -let lookup_value ~env name = +let lookup_value env name = try snd (List.assoc name env) with Not_found -> raise (Value_not_found name) -let lookup_term ~env name = - match lookup_value ~env name with - | TermValue x -> x - | _ -> raise (Value_not_found name) +let remove_name env name = List.remove_assoc name env -let lookup_num ~env name = - match lookup_value ~env name with - | NumValue x -> x - | _ -> raise (Value_not_found name) +let remove_names env names = + List.filter (fun name, _ -> not (List.mem name names)) env -let lookup_string ~env name = - match lookup_value ~env name with - | StringValue x -> x - | _ -> raise (Value_not_found name) +let lookup_term env name = + match lookup env name with + | _, TermValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) -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 lookup_num env name = + match lookup env name with + | _, NumValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) -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 lookup_string env name = + match lookup env name with + | _, StringValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) -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 lookup_opt env name = + match lookup env name with + | _, OptValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) + +let lookup_list env name = + match lookup env name with + | _, ListValue x -> x + | ty, _ -> raise (Type_mismatch (name, ty)) let opt_binding_some (n, (ty, v)) = (n, (OptType ty, OptValue (Some v))) let opt_binding_none (n, (ty, v)) = (n, (OptType ty, OptValue None)) @@ -108,193 +93,59 @@ let list_binding_of_name (n, ty) = (n, (ListType ty, ListValue [])) let opt_declaration (n, ty) = (n, OptType ty) let list_declaration (n, ty) = (n, ListType ty) - (* 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 pp_term = ref (fun (t:CicNotationPt.term) -> assert false; "") -let set_pp_term f = pp_term := f - -let instantiate ~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 +let declaration_of_var = function + | Ast.NumVar s -> s, NumType + | Ast.IdentVar s -> s, StringType + | Ast.TermVar s -> s, TermType + | _ -> assert false + +let value_of_term = function + | Ast.Num (s, _) -> NumValue s + | Ast.Ident (s, None) -> StringValue s + | t -> TermValue t + +let term_of_value = function + | NumValue s -> Ast.Num (s, 0) + | StringValue s -> Ast.Ident (s, None) + | TermValue t -> t + | _ -> assert false (* TO BE UNDERSTOOD *) + +let rec well_typed ty value = + match ty, value with + | TermType, TermValue _ + | StringType, StringValue _ + | OptType _, OptValue None + | NumType, NumValue _ -> true + | OptType ty', OptValue (Some value') -> well_typed ty' value' + | ListType ty', ListValue vl -> + List.for_all (fun value' -> well_typed ty' value') vl + | _ -> false + +let declarations_of_env = List.map (fun (name, (ty, _)) -> (name, ty)) +let declarations_of_term p = + List.map declaration_of_var (CicNotationUtil.variables_of_term p) + +let rec combine decls values = + match decls, values with + | [], [] -> [] + | (name, ty) :: decls, v :: values -> + (name, (ty, v)) :: (combine decls values) + | _ -> assert false + +let coalesce_env declarations env_list = + let env0 = List.map list_binding_of_name declarations in + let grow_env_entry env n v = + List.map + (function + | (n', (ty, ListValue vl)) as entry -> + if n' = n then n', (ty, ListValue (v :: vl)) else entry + | _ -> assert false) + env 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: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: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 + let grow_env env_i env = + List.fold_left + (fun env (n, (_, v)) -> grow_env_entry env n v) + env env_i in - aux env term + List.fold_right grow_env env_list env0