summaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml106
1 files changed, 80 insertions, 26 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 16447002..04429851 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -40,7 +40,7 @@ let names_of_local_assums bl =
List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl)
let names_of_local_binders bl =
- List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]) bl)
+ List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalPattern _ -> assert false) bl)
(**********************************************************************)
(* Functions on constr_expr *)
@@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 =
Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
| CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
eq_reference c1 c2 &&
- List.equal cases_pattern_expr_eq a1 a2 &&
+ Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
| CPatAtom(_,r1), CPatAtom(_,r2) ->
Option.equal eq_reference r1 r2
@@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 =
Option.equal Int.equal proj1 proj2 &&
constr_expr_eq e1 e2 &&
List.equal args_eq al1 al2
- | CRecord (_, e1, l1), CRecord (_, e2, l2) ->
+ | CRecord (_, l1), CRecord (_, l2) ->
let field_eq (r1, e1) (r2, e2) =
eq_reference r1 r2 && constr_expr_eq e1 e2
in
- Option.equal constr_expr_eq e1 e2 &&
List.equal field_eq l1 l2
| CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
(** Don't care about the case_style *)
@@ -178,7 +177,7 @@ and args_eq (a1,e1) (a2,e2) =
Option.equal (eq_located explicitation_eq) e1 e2 &&
constr_expr_eq a1 a2
-and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) =
+and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
constr_expr_eq e1 e2 &&
Option.equal (eq_located Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
@@ -238,7 +237,7 @@ let constr_loc = function
| CLetIn (loc,_,_,_) -> loc
| CAppExpl (loc,_,_) -> loc
| CApp (loc,_,_) -> loc
- | CRecord (loc,_,_) -> loc
+ | CRecord (loc,_) -> loc
| CCases (loc,_,_,_,_) -> loc
| CLetTuple (loc,_,_,_,_) -> loc
| CIf (loc,_,_,_,_) -> loc
@@ -261,6 +260,7 @@ let cases_pattern_expr_loc = function
| CPatRecord (loc, _) -> loc
| CPatPrim (loc,_) -> loc
| CPatDelimiters (loc,_,_) -> loc
+ | CPatCast(loc,_,_) -> loc
let raw_cases_pattern_expr_loc = function
| RCPatAlias (loc,_,_) -> loc
@@ -272,6 +272,7 @@ let local_binder_loc = function
| LocalRawAssum ((loc,_)::_,_,t)
| LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
| LocalRawAssum ([],_,_) -> assert false
+ | LocalPattern (loc,_,_) -> loc
let local_binders_loc bll = match bll with
| [] -> Loc.ghost
@@ -293,23 +294,74 @@ let mkAppC (f,l) =
| CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
| _ -> CApp (Loc.ghost, (None, f), l)
-let rec mkCProdN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CProdN (loc,[idl,bk,t],mkCProdN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCProdN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCProdN loc bll c
-
-let rec mkCLambdaN loc bll c =
- match bll with
- | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
- CLambdaN (loc,[idl,bk,t],mkCLambdaN (Loc.merge loc1 loc) bll c)
- | LocalRawDef ((loc1,_) as id,b) :: bll ->
- CLetIn (loc,id,b,mkCLambdaN (Loc.merge loc1 loc) bll c)
- | [] -> c
- | LocalRawAssum ([],_,_) :: bll -> mkCLambdaN loc bll c
+let add_name_in_env env n =
+ match snd n with
+ | Anonymous -> env
+ | Name id -> id :: env
+
+let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
+
+let expand_pattern_binders mkC bl c =
+ let rec loop bl c =
+ match bl with
+ | [] -> ([], [], c)
+ | b :: bl ->
+ let (env, bl, c) = loop bl c in
+ match b with
+ | LocalRawDef (n, _) ->
+ let env = add_name_in_env env n in
+ (env, b :: bl, c)
+ | LocalRawAssum (nl, _, _) ->
+ let env = List.fold_left add_name_in_env env nl in
+ (env, b :: bl, c)
+ | LocalPattern (loc, p, ty) ->
+ let ni = Hook.get fresh_var env c in
+ let id = (loc, Name ni) in
+ let b =
+ LocalRawAssum
+ ([id], Default Explicit,
+ match ty with
+ | Some ty -> ty
+ | None -> CHole (loc, None, IntroAnonymous, None))
+ in
+ let e = CRef (Libnames.Ident (loc, ni), None) in
+ let c =
+ CCases
+ (loc, LetPatternStyle, None, [(e,None,None)],
+ [(loc, [(loc,[p])], mkC loc bl c)])
+ in
+ (ni :: env, [b], c)
+ in
+ let (_, bl, c) = loop bl c in
+ (bl, c)
+
+let mkCProdN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
+
+let mkCLambdaN loc bll c =
+ let rec loop loc bll c =
+ match bll with
+ | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->
+ CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c)
+ | LocalRawDef ((loc1,_) as id,b) :: bll ->
+ CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c)
+ | [] -> c
+ | LocalRawAssum ([],_,_) :: bll -> loop loc bll c
+ | LocalPattern (loc,p,ty) :: bll -> assert false
+ in
+ let (bll, c) = expand_pattern_binders loop bll c in
+ loop loc bll c
let rec abstract_constr_expr c = function
| [] -> c
@@ -317,6 +369,7 @@ let rec abstract_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl
(abstract_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
let rec prod_constr_expr c = function
| [] -> c
@@ -324,22 +377,23 @@ let rec prod_constr_expr c = function
| LocalRawAssum (idl,bk,t)::bl ->
List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl
(prod_constr_expr c bl)
+ | LocalPattern _::_ -> assert false
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- Errors.user_err_loc (loc, "coerce_reference_to_id",
+ CErrors.user_err_loc (loc, "coerce_reference_to_id",
str "This expression should be a simple identifier.")
let coerce_to_id = function
| CRef (Ident (loc,id),_) -> (loc,id)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
| CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_,_,_) -> (loc,Anonymous)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 22:56:59 +0000