From 57cb1648fcf7da18d74c28a4d63d59ea129ab136 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 12:49:34 +0000
Subject: Generalized implementation of generalization. - New constr_expr
 construct [CGeneralization of loc * binding_kind * abstraction_kind option *
 constr_expr] to generalize the free vars of the [constr_expr], binding these
 using [binding_kind] and making a lambda or a pi (or deciding from the scope)
 using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) -
 Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for
 implicit bindings (both "..(" and "_(" seem much more difficult to
 implement). Subject to discussion! A few examples added in a test-suite file.
 - Also add missing syntax for implicit/explicit combinations for _binders_:
 "{( )}" means implicit for the generalized (outer) vars, explicit for the
 (inner) variable itself. Subject to discussion as well :) - Factor much
 typeclass instance declaration code. We now just have to force generalization
 of the term after the : in instance declarations. One more step to using
 Instance for records.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 39 ++++++++++++++++++++++++++++-----------
 1 file changed, 28 insertions(+), 11 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9b8f62aa03..cfa88f3cd0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -696,17 +696,8 @@ let push_loc_name_env lvar (ids,unb,tmpsc,scopes as env) loc = function
 let intern_generalized_binder intern_type lvar (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty =
   let ty = 
     if t then ty else
-      let is_class =
-	try
-	  let (loc, r, _ as clapp) = Implicit_quantifiers.destClassAppExpl ty in
-	  let (loc, qid) = qualid_of_reference r in
-	  let gr = Nametab.locate qid in
-	    if Typeclasses.is_class gr then Some (clapp, gr) else None
-	with Not_found -> None
-      in 
-	match is_class with
-	| None -> ty
-	| Some (clapp, gr) -> Implicit_quantifiers.full_class_binder ids clapp gr
+      Implicit_quantifiers.implicit_application ids
+	Implicit_quantifiers.combine_params_freevar ty
   in
   let ty = intern_type (ids,true,tmpsc,sc) ty in
   let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids ty in
@@ -731,6 +722,30 @@ let intern_local_binder_aux intern intern_type lvar ((ids,unb,ts,sc as env),bl)
       ((name_fold Idset.add na ids,unb,ts,sc),
       (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl)
 
+let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c =
+  let c = intern (ids,true,tmp_scope,scopes) c in
+  let fvs = Implicit_quantifiers.free_vars_of_rawconstr ~bound:ids c in
+  let env', c' = 
+    let abs = 
+      let pi = 
+	match ak with
+	| Some AbsPi -> true
+	| None when tmp_scope = Some Notation.type_scope 
+	    || List.mem Notation.type_scope scopes -> true
+	| _ -> false
+      in 
+	if pi then
+	  (fun (id, loc') acc ->
+	    RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+	else
+	  (fun (id, loc') acc -> 
+	    RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc))
+    in
+      List.fold_right (fun (id, loc as lid) (env, acc) -> 
+	let env' = push_loc_name_env lvar env loc (Name id) in
+	  (env', abs lid acc)) fvs (env,c) 
+  in c'
+
 (**********************************************************************)
 (* Utilities for application                                          *)
 
@@ -897,6 +912,8 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CNotation (_,"( _ )",([a],[])) -> intern env a
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
+    | CGeneralization (loc,b,a,c) ->
+        intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
 	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
 	Dumpglob.dump_notation_location (fst (unloc loc)) df;
-- 
cgit v1.2.3