From: Claudio Sacerdoti Coen Date: Mon, 28 Nov 2005 12:41:21 +0000 (+0000) Subject: 1. Bug fixed: compilation of "let corec" to a simple CoFix without a surrounding X-Git-Tag: make_still_working~8079 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c07a8ba5564610278faed3c86d9a21a9ee0c644e;p=helm.git 1. Bug fixed: compilation of "let corec" to a simple CoFix without a surrounding let...in was bugged (because of a missing delifting). Fixed. 2. Localization is no longer lost in the body of a "let rec" or a "let corec" --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index fd8e2a799..1bb8ac955 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -127,20 +127,21 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast ~localization_tbl = assert (uri = None); - let rec aux loc (context: Cic.name list) = function + let rec aux ~localize loc (context: Cic.name list) = function | CicNotationPt.AttributedTerm (`Loc loc, term) -> - let res = aux loc context term in - Cic.CicHash.add localization_tbl res loc; + let res = aux ~localize loc context term in + if localize then Cic.CicHash.add localization_tbl res loc; res - | CicNotationPt.AttributedTerm (_, term) -> aux loc context term + | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) -> - let cic_args = List.map (aux loc context) args in + let cic_args = List.map (aux ~localize loc context) args in resolve env (Symbol (symb, i)) ~args:cic_args () - | CicNotationPt.Appl terms -> Cic.Appl (List.map (aux loc context) terms) + | CicNotationPt.Appl terms -> + Cic.Appl (List.map (aux ~localize loc context) terms) | CicNotationPt.Binder (binder_kind, (var, typ), body) -> - let cic_type = aux_option loc context (Some `Type) typ in + let cic_type = aux_option ~localize loc context (Some `Type) typ in let cic_name = CicNotationUtil.cic_name_of_name var in - let cic_body = aux loc (cic_name :: context) body in + let cic_body = aux ~localize loc (cic_name :: context) body in (match binder_kind with | `Lambda -> Cic.Lambda (cic_name, cic_type, cic_body) | `Pi @@ -149,18 +150,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast resolve env (Symbol ("exists", 0)) ~args:[ cic_type; Cic.Lambda (cic_name, cic_type, cic_body) ] ()) | CicNotationPt.Case (term, indty_ident, outtype, branches) -> - let cic_term = aux loc context term in - let cic_outtype = aux_option loc context None outtype in + let cic_term = aux ~localize loc context term in + let cic_outtype = aux_option ~localize loc context None outtype in let do_branch ((head, _, args), term) = let rec do_branch' context = function - | [] -> aux loc context term + | [] -> aux ~localize loc context term | (name, typ) :: tl -> let cic_name = CicNotationUtil.cic_name_of_name name in let cic_body = do_branch' (cic_name :: context) tl in let typ = match typ with | None -> Cic.Implicit (Some `Type) - | Some typ -> aux loc context typ + | Some typ -> aux ~localize loc context typ in Cic.Lambda (cic_name, typ, cic_body) in @@ -194,18 +195,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) | CicNotationPt.Cast (t1, t2) -> - let cic_t1 = aux loc context t1 in - let cic_t2 = aux loc context t2 in + let cic_t1 = aux ~localize loc context t1 in + let cic_t2 = aux ~localize loc context t2 in Cic.Cast (cic_t1, cic_t2) | CicNotationPt.LetIn ((name, typ), def, body) -> - let cic_def = aux loc context def in + let cic_def = aux ~localize loc context def in let cic_name = CicNotationUtil.cic_name_of_name name in let cic_def = match typ with | None -> cic_def - | Some t -> Cic.Cast (cic_def, aux loc context t) + | Some t -> Cic.Cast (cic_def, aux ~localize loc context t) in - let cic_body = aux loc (cic_name :: context) body in + let cic_body = aux ~localize loc (cic_name :: context) body in Cic.LetIn (cic_name, cic_def, cic_body) | CicNotationPt.LetRec (kind, defs, body) -> let context' = @@ -214,12 +215,50 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast CicNotationUtil.cic_name_of_name name :: acc) context defs in - let cic_body = aux loc context' body in + let cic_body = + let unlocalized_body = aux ~localize:false loc context' body in + match unlocalized_body with + Cic.Rel 1 -> `AvoidLetInNoAppl + | Cic.Appl (Cic.Rel 1::l) -> + (try + let l' = + List.map + (function t -> + let t',subst,metasenv = + CicMetaSubst.delift_rels [] [] 1 t + in + assert (subst=[]); + assert (metasenv=[]); + t') l + in + (* We can avoid the LetIn. But maybe we need to recompute l' + so that it is localized *) + if localize then + match body with + CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) -> + let l' = List.map (aux ~localize loc context) l in + `AvoidLetIn l' + | _ -> assert false + else + `AvoidLetIn l' + with + CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body) + | _ -> + if localize then + `AddLetIn (aux ~localize loc context' body) + else + `AddLetIn unlocalized_body + in let inductiveFuns = List.map (fun ((name, typ), body, decr_idx) -> - let cic_body = aux loc context' body in - let cic_type = aux_option loc context (Some `Type) typ in + let cic_body = aux ~localize loc context' body in + let cic_type = + aux_option ~localize loc context (Some `Type) typ in let name = match CicNotationUtil.cic_name_of_name name with | Cic.Anonymous -> @@ -241,24 +280,11 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast incr counter; let fix = Cic.Fix (!counter,funs) in match cic with - Cic.Rel 1 -> fix - | (Cic.Appl (Cic.Rel 1::l)) -> - (try - let l' = - List.map - (function t -> - let t',subst,metasenv = - CicMetaSubst.delift_rels [] [] 1 t - in - assert (subst=[]); - assert (metasenv=[]); - t') l - in - Cic.Appl (fix::l') - with - CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - Cic.LetIn (Cic.Name var, fix, cic)) - | _ -> Cic.LetIn (Cic.Name var, fix, cic)) + `Recipe (`AddLetIn cic) -> + `Term (Cic.LetIn (Cic.Name var, fix, cic)) + | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (fix::l)) + | `Recipe `AvoidLetInNoAppl -> `Term fix + | `Term t -> `Term (Cic.LetIn (Cic.Name var, fix, t))) | `CoInductive -> let funs = List.map (fun (name, _, typ, body) -> (name, typ, body)) funs @@ -267,11 +293,18 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast incr counter; let cofix = Cic.CoFix (!counter,funs) in match cic with - Cic.Rel 1 -> cofix - | (Cic.Appl (Cic.Rel 1::l)) -> Cic.Appl (cofix::l) - | _ -> Cic.LetIn (Cic.Name var, cofix, cic)) + `Recipe (`AddLetIn cic) -> + `Term (Cic.LetIn (Cic.Name var, cofix, cic)) + | `Recipe (`AvoidLetIn l) -> `Term (Cic.Appl (cofix::l)) + | `Recipe `AvoidLetInNoAppl -> `Term cofix + | `Term t -> `Term (Cic.LetIn (Cic.Name var, cofix, t))) in - List.fold_right (build_term inductiveFuns) inductiveFuns cic_body + (match + List.fold_right (build_term inductiveFuns) inductiveFuns + (`Recipe cic_body) + with + `Recipe _ -> assert false + | `Term t -> t) | CicNotationPt.Ident _ | CicNotationPt.Uri _ when is_path -> raise PathNotWellFormed | CicNotationPt.Ident (name, subst) @@ -302,7 +335,7 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast List.map (fun (s, term) -> (try - List.assoc s ids_to_uris, aux loc context term + List.assoc s ids_to_uris, aux ~localize loc context term with Not_found -> raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))) subst @@ -358,7 +391,9 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | CicNotationPt.Meta (index, subst) -> let cic_subst = List.map - (function None -> None | Some term -> Some (aux loc context term)) + (function + None -> None + | Some term -> Some (aux ~localize loc context term)) subst in Cic.Meta (index, cic_subst) @@ -369,11 +404,11 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast | CicNotationPt.Symbol (symbol, instance) -> resolve env (Symbol (symbol, instance)) () | _ -> assert false (* god bless Bologna *) - and aux_option loc (context: Cic.name list) annotation = function + and aux_option ~localize loc (context: Cic.name list) annotation = function | None -> Cic.Implicit annotation - | Some term -> aux loc context term + | Some term -> aux ~localize loc context term in - aux dummy_floc context ast + aux ~localize:true dummy_floc context ast let interpretate_path ~context path = let localization_tbl = Cic.CicHash.create 23 in