* 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
| 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))
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
projects / helm.git / blobdiff