open CicNotationPt
-exception Value_not_found of string
-
type value =
| TermValue of term
| StringValue of string
| 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 = (string * (value_type * value)) list
-let lookup_value ~env name =
+let lookup env name =
+ try
+ List.assoc name env
+ with Not_found -> raise (Value_not_found 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 lookup_num ~env name =
- match lookup_value ~env name with
- | NumValue x -> x
- | _ -> raise (Value_not_found name)
-
-let lookup_string ~env name =
- match lookup_value ~env name with
- | StringValue x -> x
- | _ -> raise (Value_not_found name)
-
-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
- | [] -> acc
- in
- aux [] env
+let remove env name = List.remove_assoc name env
+
+let lookup_term env name =
+ match lookup env name with
+ | _, TermValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_num env name =
+ match lookup env name with
+ | _, NumValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+let lookup_string env name =
+ match lookup env name with
+ | _, StringValue x -> x
+ | ty, _ -> raise (Type_mismatch (name, ty))
+
+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))
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
- | Fold (_, t1, _, t2) ->
- aux t1 ;
- aux t2
- | Default (t1, t2) ->
- aux t1 ;
- aux t2
- | _ -> assert false
- in
- aux term ;
- !names
-
-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
+ | NumVar s -> s, NumType
+ | IdentVar s -> s, StringType
+ | TermVar s -> s, TermType
+ | _ -> assert false
+
+let value_of_term = function
+ | Num (s, _) -> NumValue s
+ | Ident (s, None) -> StringValue s
+ | t -> TermValue t
+
+let term_of_value = function
+ | NumValue s -> Num (s, 0)
+ | StringValue s -> 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 _ -> failwith "not yet implemented" (* TODO Fold *)
- | _ -> 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